diff --git a/LiveVerif/src/LiveVerif/LiveProgramLogic.v b/LiveVerif/src/LiveVerif/LiveProgramLogic.v
index cac63dcd0..5265ba42f 100644
--- a/LiveVerif/src/LiveVerif/LiveProgramLogic.v
+++ b/LiveVerif/src/LiveVerif/LiveProgramLogic.v
@@ -42,22 +42,24 @@ Require Import bedrock2.LogSidecond.
 
 Definition functions_correct
   (* universally quantified abstract function list containing all functions: *)
-  (qfs: list (string * func)):
+  (qfs: Semantics.env):
   (* specs of a subset of functions for which to assert correctness *)
-  list (list (string * func) -> Prop (* spec_of mentioning function name *)) -> Prop :=
+  list (Semantics.env -> Prop (* spec_of mentioning function name *)) -> Prop :=
   List.Forall (fun spec => spec qfs).
 
 Definition function_with_callees: Type :=
-  func * list (list (string * func) -> Prop (* spec_of mentioning function name *)).
+  func * list (Semantics.env -> Prop (* spec_of mentioning function name *)).
 
 Definition program_logic_goal_for(name: string)(f: function_with_callees)
   {spec: bedrock2.ProgramLogic.spec_of name}: Prop :=
   match f with
   | (impl, callees) => forall functions,
-      functions_correct functions callees -> spec (cons (name, impl) functions)
+      map.get functions name = Some impl ->
+      functions_correct functions callees ->
+      spec functions
   end.
 
-Definition nth_spec(specs: list (list (string * func) -> Prop))(n: nat) :=
+Definition nth_spec(specs: list (Semantics.env -> Prop))(n: nat) :=
   Eval unfold List.nth in (List.nth n specs (fun _ => True)).
 
 Lemma nth_function_correct: forall fs n specs spec,
@@ -143,22 +145,18 @@ Ltac start :=
       subst evar;
       unfold program_logic_goal_for, spec;
       let fs := fresh "fs" in
+      let G := fresh "EnvContains" in
       let fs_ok := fresh "fs_ok" in
-      intros fs fs_ok;
+      intros fs G fs_ok;
       let nP := fresh "Scope0" in pose proof (mk_scope_marker FunctionParams) as nP;
       intros_until_trace;
       let nB := fresh "Scope0" in pose proof (mk_scope_marker FunctionBody) as nB;
       lazymatch goal with
       | |- forall (t : trace) (m : @map.rep (@word.rep _ _) Init.Byte.byte _), _ => intros
       end;
-      WeakestPrecondition.unfold1_call_goal;
-      cbv match beta delta [WeakestPrecondition.call_body];
-      lazymatch goal with
-      | |- if ?test then ?T else _ =>
-        replace test with true by reflexivity; change T
-      end;
       eapply prove_func;
-      [ lazymatch goal with
+      [ exact G
+      | lazymatch goal with
         | |- map.of_list_zip ?argnames_evar ?argvalues = Some ?locals_evar =>
              let argnames := map_with_ltac varconstr_to_string argvalues in
              unify argnames_evar argnames;
@@ -166,7 +164,7 @@ Ltac start :=
              unify locals_evar (map.of_list kvs);
              reflexivity
         end
-      | ];
+      | clear G ];
       first [eapply simplify_no_return_post | eapply simplify_1retval_post];
       pose_state stepping
   | |- _ => fail "goal needs to be of shape (@program_logic_goal_for ?fname ?evar ?spec)"
diff --git a/LiveVerif/src/LiveVerif/LiveRules.v b/LiveVerif/src/LiveVerif/LiveRules.v
index d67b558d0..f402f90cd 100644
--- a/LiveVerif/src/LiveVerif/LiveRules.v
+++ b/LiveVerif/src/LiveVerif/LiveRules.v
@@ -15,6 +15,8 @@ Require Import bedrock2.ZnWords.
 Require Import bedrock2.SepLib.
 Require Import bedrock2.enable_frame_trick.
 
+Notation wp_cmd := Semantics.exec (only parsing).
+
 (* A let-binding using an equality instead of :=, living in Prop.
    Equivalent to (exists x, x = rhs /\ body x).
    We don't use regular exists to make the intention recognizable by tactics.
@@ -356,39 +358,6 @@ Section WithParams.
     - assumption.
   Qed.
 
-  Ltac pose_env :=
-    let env := fresh "env" in
-    unshelve epose (env := _ : map.map string (list string * list string * cmd));
-    [ eapply SortedListString.map
-    | assert (env_ok: map.ok env) by apply SortedListString.ok; clearbody env ].
-
-  Lemma WP_weaken_cmd: forall fs c t m l (post1 post2: _->_->_->Prop),
-      WeakestPrecondition.cmd (call fs) c t m l post1 ->
-      (forall t m l, post1 t m l -> post2 t m l) ->
-      WeakestPrecondition.cmd (call fs) c t m l post2.
-  Proof.
-    pose_env. intros.
-    eapply WeakestPreconditionProperties.Proper_cmd. 3: eassumption.
-    1: eapply WeakestPreconditionProperties.Proper_call.
-    cbv [RelationClasses.Reflexive Morphisms.pointwise_relation
-         Morphisms.respectful Basics.impl].
-    assumption.
-  Qed.
-
-  Inductive wp_cmd(fs: list (string * (list string * list string * cmd)))
-            (c: cmd)(t: trace)(m: mem)(l: locals)(post: trace -> mem -> locals -> Prop):
-    Prop := mk_wp_cmd(_: WeakestPrecondition.cmd (call fs) c t m l post).
-
-  Lemma invert_wp_cmd: forall fs c t m l post,
-      wp_cmd fs c t m l post -> WeakestPrecondition.cmd (call fs) c t m l post.
-  Proof. intros. inversion H; assumption. Qed.
-
-  Lemma weaken_wp_cmd: forall fs c t m l (post1 post2: _->_->_->Prop),
-      wp_cmd fs c t m l post1 ->
-      (forall t m l, post1 t m l -> post2 t m l) ->
-      wp_cmd fs c t m l post2.
-  Proof. intros. constructor. inversion H. eapply WP_weaken_cmd; eassumption. Qed.
-
   Lemma wp_skip: forall fs t m l (post: trace -> mem -> locals -> Prop),
       post t m l ->
       wp_cmd fs cmd.skip t m l post.
@@ -397,11 +366,7 @@ Section WithParams.
   Lemma wp_seq: forall fs c1 c2 t m l post,
       wp_cmd fs c1 t m l (fun t' m' l' => wp_cmd fs c2 t' m' l' post) ->
       wp_cmd fs (cmd.seq c1 c2) t m l post.
-  Proof.
-    intros. constructor. cbn. inversion H. clear H.
-    eapply WP_weaken_cmd. 1: eassumption. cbv beta. intros.
-    inversion H. assumption.
-  Qed.
+  Proof. intros. econstructor; eauto. Qed.
 
   Fixpoint update_locals(keys: list string)(vals: list word)
     (l: locals)(post: locals -> Prop) :=
@@ -429,8 +394,9 @@ Section WithParams.
       post t m (map.put l x v) ->
       wp_cmd fs (cmd.set x e) t m l post.
   Proof.
-    intros. inversion H; clear H. econstructor.
-    cbn -[map.put]. eexists. split. 1: eassumption. unfold dlet.dlet. assumption.
+    intros. inversion H; clear H.
+    eapply WeakestPreconditionProperties.expr_sound in H1. fwd.
+    econstructor; eassumption.
   Qed.
 
   Lemma wp_set0: forall fs x e v t m l rest post,
@@ -449,14 +415,20 @@ Section WithParams.
       wp_cmd fs (cmd.seq (cmd.store access_size.word ea ev) rest) t m l post.
   Proof.
     intros. inversion H; clear H. inversion H0; clear H0.
-    constructor. hnf.
-    eexists. split. 1: eassumption.
+    eapply WeakestPreconditionProperties.expr_sound in H3. fwd.
+    eapply WeakestPreconditionProperties.expr_sound in H. fwd.
+    eapply exec.seq with (mid := fun t' m' l' => t' = t /\ l' = l /\ _).
+    2: {
+      intros * (? & ? & HM). subst. eapply H2. exact HM.
+    }
     unfold anyval in H1. eapply sep_ex1_l in H1. destruct H1 as (v_old & H1).
-    eexists. split. 1: eassumption.
-    unfold store.
     unfold uintptr, Scalars.scalar in *.
-    eapply Scalars.store_of_sep. 1: eassumption.
-    intros. eapply H2. assumption.
+    eapply Scalars.store_of_sep in H1.
+    { destruct H1 as (m' & ? & HP).
+      econstructor; try eassumption.
+      ssplit. 1,2: reflexivity.
+      exact HP. }
+    intros ?. exact id.
   Qed.
 
   Lemma wp_store_uint0: forall fs sz ea ev a v R t m l rest (post: _->_->_->Prop),
@@ -469,26 +441,39 @@ Section WithParams.
       wp_cmd fs (cmd.seq (cmd.store sz ea ev) rest) t m l post.
   Proof.
     intros. inversion H; clear H. inversion H0; clear H0.
-    constructor. hnf.
-    eexists. split. 1: eassumption.
+    eapply WeakestPreconditionProperties.expr_sound in H4. fwd.
+    eapply WeakestPreconditionProperties.expr_sound in H. fwd.
+    eapply exec.seq with (mid := fun t' m' l' => t' = t /\ l' = l /\ _).
+    2: {
+      intros * (? & ? & HM). subst. eapply H3. exact HM.
+    }
     unfold anyval in H2. eapply sep_ex1_l in H2. destruct H2 as (v_old & H2).
-    eexists. split. 1: eassumption.
-    unfold store.
     unfold uint in H2. eapply sep_assoc in H2. eapply sep_emp_l in H2.
     destruct H2 as (B & M).
-    eapply Scalars.store_of_sep.
-    - unfold Scalars.truncated_word, Scalars.truncated_scalar.
-      destruct sz; cbn in *;
-      rewrite <- (word.unsigned_of_Z_nowrap v_old) in M
-        by (destruct width_cases as [W|W]; rewrite W in *; lia);
-      try exact M.
-      eqapply M. f_equal.
-      destruct width_cases as [W|W]; rewrite W in *; reflexivity.
-    - intros. eapply H3. unfold uint. eapply sep_assoc. eapply sep_emp_l.
+    pose proof Scalars.store_of_sep as P.
+    unfold Scalars.truncated_word, Scalars.truncated_scalar in P.
+    specialize (P sz v0 (word.of_Z v_old)).
+    replace (Z.to_nat (nbits_to_nbytes (access_size_to_nbits sz))) with
+      (bytes_per (width := width) sz) in M.
+    2: {
+      destruct sz; cbn; try reflexivity.
+      destruct width_cases as [W | W]; rewrite W; reflexivity.
+    }
+    rewrite word.unsigned_of_Z_nowrap in P.
+    2: {
+      destruct width_cases as [W|W]; rewrite W in *; destruct sz; lia.
+    }
+    eapply P in M.
+    { destruct M as (m' & ? & HP).
+      econstructor; try eassumption.
+      ssplit. 1,2: reflexivity.
+      exact HP. }
+    { clear P.
+      intros. unfold uint. eapply sep_assoc. eapply sep_emp_l.
       split. 1: assumption. unfold Scalars.truncated_word, Scalars.truncated_scalar in *.
       destruct sz; try assumption.
-      eqapply H0. clear -BW word_ok.
-      destruct width_cases as [W|W]; subst width; reflexivity.
+      eqapply H. clear -BW word_ok.
+      destruct width_cases as [W|W]; subst width; reflexivity. }
   Qed.
 
   Definition merge_locals(c: bool):
@@ -544,12 +529,11 @@ Section WithParams.
       (word.unsigned b =  0 -> wp_cmd fs els t m l post) ->
       wp_cmd fs (cmd.cond c thn els) t m l post.
   Proof.
-    intros. inversion H; clear H. constructor. hnf.
-    eexists. split. 1: eassumption.
-    split; intro A;
-      match goal with
-      | H: _ -> _ |- _ => specialize (H A); inversion H; clear H; assumption
-      end.
+    intros. inversion H; clear H.
+    eapply WeakestPreconditionProperties.expr_sound in H2. fwd.
+    destr (word.unsigned v =? 0).
+    - eapply exec.if_false; eauto.
+    - eapply exec.if_true; eauto.
   Qed.
 
   Lemma wp_if0: forall fs c thn els rest b Q1 Q2 t m l post,
@@ -565,10 +549,10 @@ Section WithParams.
     all: intro A; match goal with
       | H: _ -> _ |- _ => specialize (H A)
       end.
-    all: eauto using weaken_wp_cmd.
+    all: eauto using exec.weaken.
   Qed.
 
-  Definition after_loop: list (string * (list string * list string * cmd)) ->
+  Definition after_loop: Semantics.env ->
     cmd -> trace -> mem -> locals -> (trace -> mem -> locals -> Prop) -> Prop := wp_cmd.
 
   Lemma wp_set: forall fs x e v t m l rest post,
@@ -595,7 +579,7 @@ Section WithParams.
       wp_cmd fs rest t m l (fun t' m' l' => post t' m' (map.remove l' x)) ->
       wp_cmd fs (cmd.seq rest (cmd.unset x)) t m l post.
   Proof.
-    intros. eapply wp_seq. eapply weaken_wp_cmd. 1: eassumption.
+    intros. eapply wp_seq. eapply exec.weaken. 1: eassumption.
     cbv beta. intros. eapply wp_unset00. assumption.
   Qed.
 
@@ -762,7 +746,7 @@ Section WithParams.
                   True)
     : wp_cmd fs (cmd.seq (cmd.while e c) rest) t m l post.
   Proof.
-    econstructor. cbn. exists measure, lt, invariant.
+    eapply wp_seq. eapply wp_while. exists measure, lt, invariant.
     split. 1: assumption.
     split. 1: eauto.
     clear Hpre v0 t m l.
@@ -772,9 +756,10 @@ Section WithParams.
     inversion Hbody. subst. clear Hbody. inversion H. clear H.
     eexists. split. 1: eassumption.
     unfold bool_expr_branches in *. apply proj1 in H1. split.
-    - intro NE. rewrite word.eqb_ne in H1. 1: eapply H1. intro C. subst v0.
+    - intro NE. eapply WeakestPreconditionProperties.complete_cmd.
+      rewrite word.eqb_ne in H1. 1: eapply H1. intro C. subst v0.
       apply NE. apply word.unsigned_of_Z_0.
-    - intro E. rewrite word.eqb_eq in H1. 1: eapply invert_wp_cmd; eapply H1.
+    - intro E. rewrite word.eqb_eq in H1. 1: eapply H1.
       eapply word.unsigned_inj. rewrite word.unsigned_of_Z_0. exact E.
   Qed.
 
@@ -803,9 +788,7 @@ Section WithParams.
     (Hrest: forall t m l, post (g0, v0, t, m, l) -> wp_cmd fs rest t m l finalpost)
     : wp_cmd fs (cmd.seq (cmd.while e c) rest) t0 m0 l0 finalpost.
   Proof.
-    eapply wp_seq.
-    econstructor. cbn.
-    pose_env.
+    eapply wp_seq. eapply WeakestPreconditionProperties.sound_cmd.
     eapply tailrec_localsmap_1ghost with
       (P := fun v g t m l => pre (g, v, t, m, l))
       (Q := fun v g t m l => post (g, v, t, m, l)).
@@ -821,8 +804,7 @@ Section WithParams.
     eexists. split. 1: eassumption.
     unfold loop_body_marker in *.
     split; intro Hv; destruct_one_match_hyp.
-    - apply proj1 in HAgain. inversion HAgain. eapply WP_weaken_cmd. 1: eassumption.
-      cbv beta. intros *. exact id.
+    - apply proj1 in HAgain. eapply WeakestPreconditionProperties.complete_cmd. assumption.
     - exfalso. apply Hv. apply word.unsigned_of_Z_0.
     - exfalso. apply E. eapply word.unsigned_inj. rewrite Hv. symmetry.
       apply word.unsigned_of_Z_0.
@@ -918,7 +900,7 @@ Section WithParams.
         1: assumption.
         split. 1: constructor. apply proj2 in H3. unfold loop_body_marker in *.
         apply proj1 in H3. split. 2: constructor.
-        eapply weaken_wp_cmd. 1: eassumption.
+        eapply Semantics.exec.weaken. 1: eassumption.
         cbv beta. clear H3. intros. fwd. inversion H2. subst. clear H2.
         unfold bool_expr_branches in *. apply proj1 in H5.
         destr (word.eqb v2 (word.of_Z 0)); simpl in *.
@@ -939,9 +921,6 @@ Section WithParams.
       { assumption. }
   Qed.
 
-  Definition dexprs(m: mem)(l: locals): list expr -> list word -> Prop :=
-    List.Forall2 (dexpr m l).
-
   Inductive dexprs1(m: mem)(l: locals)(es: list expr)(vs: list word)(P: Prop): Prop :=
   | mk_dexprs1(Hde: dexprs m l es vs)(Hp: P).
 
@@ -954,19 +933,12 @@ Section WithParams.
   Proof.
     intros.
     inversion H; clear H. inversion Hp. clear Hp.
-    constructor. 2: assumption. constructor. 1: assumption. assumption.
-  Qed.
-
-  Lemma cpsify_dexprs: forall m l es vs (post: list word -> Prop),
-      dexprs m l es vs ->
-      post vs ->
-      list_map (WeakestPrecondition.expr m l) es post.
-  Proof.
-    induction es; intros.
-    - cbn in *. inversion H. subst. assumption.
-    - cbn in *. inversion H. subst. clear H.
-      inversion H3. clear H3. unfold WeakestPrecondition.dexpr in H.
-      eapply weaken_expr. 1: eassumption. intros. subst. eapply IHes; eassumption.
+    constructor. 2: assumption. inversion Hde. unfold WeakestPrecondition.dexpr in *.
+    cbn. eapply weaken_expr. 1: eassumption. intros. subst.
+    unfold dexprs in Hde0. eapply WeakestPreconditionProperties.Proper_list_map.
+    3: eassumption.
+    { intros ? ? ? ? ? . eapply weaken_expr. 1: eassumption. assumption. }
+    { intros ? ?. subst. reflexivity. }
   Qed.
 
   Lemma wp_call0 fs t m l fname resnames es vs (post: trace -> mem -> locals -> Prop):
@@ -975,9 +947,11 @@ Section WithParams.
         exists l', map.putmany_of_list_zip resnames rets l = Some l' /\ post t' m' l') ->
       wp_cmd fs (cmd.call resnames fname es) t m l post.
   Proof.
-    intros.
-    constructor. cbn. exists vs. split. 2: assumption.
-    unfold WeakestPrecondition.dexprs. eapply cpsify_dexprs. 1: eassumption. reflexivity.
+    intros. unfold call in *. fwd.
+    unfold dexprs, WeakestPrecondition.dexprs in *.
+    eapply WeakestPreconditionProperties.sound_args in H. fwd.
+    econstructor; try eassumption.
+    cbv beta. intros *. exact id.
   Qed.
 
   Lemma wp_call: forall fs fname t m resnames arges argvs l rest
@@ -1000,9 +974,6 @@ Section WithParams.
     specialize (H Pre). clear Pre.
     eapply wp_seq.
     eapply wp_call0. 1: eassumption.
-    unshelve epose (env := _ : map.map string func).
-    1: eapply SortedListString.map.
-    assert (env_ok: map.ok env) by apply SortedListString.ok. clearbody env.
     eapply WeakestPreconditionProperties.Proper_call. 2: eassumption. exact Impl.
   Qed.
 
@@ -1017,20 +988,17 @@ Section WithParams.
       eapply IHretnames; eassumption.
   Qed.
 
-  Lemma prove_func: forall fs argnames retnames body t m argvals l post,
+  Lemma prove_func: forall fs f argnames retnames body t m argvals l post,
+      map.get fs f = Some (argnames, retnames, body) ->
       map.of_list_zip argnames argvals = Some l ->
       wp_cmd fs body t m l (fun t' m' l' => exists retvals,
                                 map.getmany_of_list l' retnames = Some retvals /\
                                   post t' m' retvals) ->
-      WeakestPrecondition.func (call fs) (argnames, retnames, body) t m argvals post.
+      WeakestPrecondition.call fs f t m argvals post.
   Proof.
     intros.
-    unfold func.
-    eexists. split. 1: eassumption.
-    eapply invert_wp_cmd.
-    eapply weaken_wp_cmd. 1: eassumption.
-    cbv beta. intros. fwd.
-    eapply cpsify_getmany_of_list; eassumption.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
+    assumption.
   Qed.
 
   (* applied at beginning of void functions *)
@@ -1041,7 +1009,7 @@ Section WithParams.
         map.getmany_of_list l' nil = Some retvals /\
         (retvals = nil /\ P t' m')).
   Proof.
-    intros. eapply weaken_wp_cmd. 1: eassumption.
+    intros. eapply Semantics.exec.weaken. 1: eassumption.
     cbv beta. intros. fwd. eexists.
     split. 1: reflexivity. auto.
   Qed.
@@ -1060,7 +1028,7 @@ Section WithParams.
         map.getmany_of_list l' (cons RETNAME nil) = Some retvals /\
         (exists retv, retvals = cons retv nil /\ P t' m' retv)).
   Proof.
-    intros. eapply weaken_wp_cmd. 1: eassumption.
+    intros. eapply Semantics.exec.weaken. 1: eassumption.
     intros. inversion H0. subst. clear H0. eexists.
     split. {
       simpl. unfold map.getmany_of_list. simpl. rewrite G. reflexivity.
diff --git a/PyLevelLang/src/PyLevelLang/Compile.v b/PyLevelLang/src/PyLevelLang/Compile.v
index 6c0eef5ad..9bae55529 100644
--- a/PyLevelLang/src/PyLevelLang/Compile.v
+++ b/PyLevelLang/src/PyLevelLang/Compile.v
@@ -136,8 +136,8 @@ Section WithMap.
 
   Lemma eval_map_extends_locals : forall e (m : mem) (l l' : locals') w,
     map.extends l' l ->
-    eval_expr_old m l e = Some w ->
-    eval_expr_old m l' e = Some w.
+    eval_expr m l e = Some w ->
+    eval_expr m l' e = Some w.
   Proof.
     induction e; intros m l l' w H Hl.
     - (* Syntax.expr.literal *)
@@ -148,47 +148,47 @@ Section WithMap.
     - (* Syntax.expr.inlinetable *)
       simpl in Hl. simpl.
       specialize IHe with (m := m) (1 := H).
-      destruct (eval_expr_old m l e); try easy.
+      destruct (eval_expr m l e); try easy.
       specialize IHe with (w := r) (1 := eq_refl).
       now rewrite IHe.
     - (* Syntax.expr.load *)
       simpl in Hl. simpl.
       specialize IHe with (m := m) (1 := H).
-      destruct (eval_expr_old m l e); try easy.
+      destruct (eval_expr m l e); try easy.
       specialize IHe with (w := r) (1 := eq_refl).
       now rewrite IHe.
     - (* Syntax.expr.op *)
       simpl in Hl. simpl.
-      destruct (eval_expr_old m l e1) as [r1 |] eqn:H1; try easy.
-      destruct (eval_expr_old m l e2) as [r2 |] eqn:H2; try easy.
+      destruct (eval_expr m l e1) as [r1 |] eqn:H1; try easy.
+      destruct (eval_expr m l e2) as [r2 |] eqn:H2; try easy.
       specialize IHe1 with (m := m) (w := r1) (1 := H) (2 := H1).
       specialize IHe2 with (m := m) (w := r2) (1 := H) (2 := H2).
       now rewrite IHe1, IHe2.
     - (* Syntax.expr.ite *)
       simpl in Hl. simpl.
-      destruct (eval_expr_old m l e1) as [r1 |] eqn:H1; try easy.
+      destruct (eval_expr m l e1) as [r1 |] eqn:H1; try easy.
       specialize IHe1 with (m := m) (w := r1) (1 := H) (2 := H1).
       rewrite IHe1.
       destruct word.eqb.
-      + destruct (eval_expr_old m l e3) as [r3 |] eqn:H3; try easy.
+      + destruct (eval_expr m l e3) as [r3 |] eqn:H3; try easy.
         apply IHe3 with (l' := l') in H3; try assumption.
         now rewrite H3.
-      + destruct (eval_expr_old m l e2) as [r2 |] eqn:H2; try easy.
+      + destruct (eval_expr m l e2) as [r2 |] eqn:H2; try easy.
         apply IHe2 with (l' := l') in H2; try assumption.
         now rewrite H2.
   Qed.
 
   Lemma compile_correct : forall {t} (e : expr t) (c : Syntax.cmd) (e' : Syntax.expr),
     wf map.empty e ->
-    compile_expr e = Success (c, e') -> forall tr m l mc,
-    exec map.empty c tr m l mc (fun tr' m' l' mc' => exists (w : word),
-      eval_expr_old m' l' e' = Some w /\
+    compile_expr e = Success (c, e') -> forall tr m l,
+    exec map.empty c tr m l (fun tr' m' l' => exists (w : word),
+      eval_expr m' l' e' = Some w /\
       value_relation (interp_expr map.empty e) w /\
       m' = m /\
       map.extends l' l
     ).
   Proof.
-    intros t. induction e; intros c e' He He' tr m l mc; try easy.
+    intros t. induction e; intros c e' He He' tr m l; try easy.
     - (* EAtom a *)
       unfold compile_expr in He'.
       fwd.
@@ -218,7 +218,7 @@ Section WithMap.
         specialize IHe with (2 := eq_refl);
         eapply exec.weaken; [ now apply IHe |];
         cbv beta;
-        intros tr' m' l' mc' Hw;
+        intros tr' m' l' Hw;
         fwd;
         eexists;
         ssplit;
@@ -253,11 +253,11 @@ Section WithMap.
         specialize IHe2 with (2 := eq_refl);
         eapply exec.seq; [ now apply IHe1 |];
         cbv beta;
-        intros tr' m' l' mc' Hw;
+        intros tr' m' l' Hw;
         fwd;
         eapply exec.weaken; [ now apply IHe2 |];
         cbv beta;
-        intros tr'' m'' l'' mc'' Hw';
+        intros tr'' m'' l'' Hw';
         fwd;
         eexists;
         ssplit;
@@ -265,7 +265,7 @@ Section WithMap.
           apply eval_map_extends_locals with (l' := l'') in Hwp0;
           [| assumption];
           now rewrite Hwp0
-        | 
+        |
         | reflexivity
         | now apply extends_trans with l' ].
       1-9:
diff --git a/bedrock2/src/bedrock2/FrameRule.v b/bedrock2/src/bedrock2/FrameRule.v
index 370f71397..7ca6b059f 100644
--- a/bedrock2/src/bedrock2/FrameRule.v
+++ b/bedrock2/src/bedrock2/FrameRule.v
@@ -8,7 +8,7 @@ Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWo
 Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.MetricLogging.
 Require Import bedrock2.Memory bedrock2.ptsto_bytes bedrock2.Map.Separation.
-Require Import bedrock2.Semantics.
+Require Import bedrock2.Semantics bedrock2.MetricSemantics.
 Require Import bedrock2.Map.DisjointUnion bedrock2.Map.split_alt.
 
 Require Import Coq.Lists.List.
@@ -16,7 +16,6 @@ Require Import Coq.Lists.List.
 Section semantics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
   Context {mem_ok: map.ok mem} {word_ok: word.ok word}.
 
@@ -127,8 +126,8 @@ Section semantics.
   Lemma frame_evaluate_call_args_log: forall l mSmall mBig mAdd arges
                                              mc (args: list word) mc',
       mmap.split mBig mSmall mAdd ->
-      evaluate_call_args_log mSmall l arges mc = Some (args, mc') ->
-      evaluate_call_args_log mBig   l arges mc = Some (args, mc').
+      eval_call_args mSmall l arges mc = Some (args, mc') ->
+      eval_call_args mBig   l arges mc = Some (args, mc').
   Proof.
     induction arges; cbn; intros.
     - assumption.
diff --git a/bedrock2/src/bedrock2/Loops.v b/bedrock2/src/bedrock2/Loops.v
index 11950acc1..e2bc84e9c 100644
--- a/bedrock2/src/bedrock2/Loops.v
+++ b/bedrock2/src/bedrock2/Loops.v
@@ -11,15 +11,37 @@ From bedrock2 Require Import WeakestPrecondition WeakestPreconditionProperties.
 Section Loops.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
-  Context {functions : list (String.string * (list String.string * list String.string * Syntax.cmd))}.
-  Let call := WeakestPrecondition.call functions.
+  Context {fs : env}.
+  Let call := fs.
+
+  Lemma wp_while: forall e c t m l (post: _ -> _ -> _ -> Prop),
+     (exists measure (lt:measure->measure->Prop) (inv:measure->trace->mem->locals->Prop),
+      Coq.Init.Wf.well_founded lt /\
+      (exists v, inv v t m l) /\
+      (forall v t m l, inv v t m l ->
+        exists b, dexpr m l e b /\
+        (word.unsigned b <> 0%Z -> cmd call c t m l (fun t' m l =>
+          exists v', inv v' t' m l /\ lt v' v)) /\
+        (word.unsigned b = 0%Z -> post t m l))) ->
+     cmd call (cmd.while e c) t m l post.
+  Proof.
+    intros. destruct H as (measure & lt & inv & Hwf & HInit & Hbody).
+    destruct HInit as (v0 & HInit).
+    revert t m l HInit. pattern v0. revert v0.
+    eapply (well_founded_ind Hwf). intros.
+    specialize Hbody with (1 := HInit). destruct Hbody as (b & Hb & Ht & Hf).
+    eapply expr_sound in Hb. destruct Hb as (b' & Hb & ?). subst b'.
+    destr.destr (Z.eqb (word.unsigned b) 0).
+    - specialize Hf with (1 := E). eapply exec.while_false; eassumption.
+    - specialize Ht with (1 := E). eapply sound_cmd in Ht.
+      eapply exec.while_true; eauto.
+      cbv beta. intros * (v' & HInv & HLt). eapply sound_cmd. eauto.
+  Qed.
 
   Lemma tailrec_localsmap_1ghost
     {e c t} {m: mem} {l} {post : trace -> mem -> locals -> Prop}
@@ -41,6 +63,7 @@ Section Loops.
     (Hpost: forall t m l, Q v0 g0 t m l -> post t m l)
     : cmd call (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists measure, lt, (fun v t m l =>
       exists g, P v g t m l /\ forall t'' m'' l'', Q v g t'' m'' l'' -> Q v0 g0 t'' m'' l'').
     split; [assumption|].
@@ -50,8 +73,7 @@ Section Loops.
     destruct Hbody as (br & ? & Hbody). exists br; split; [assumption|].
     destruct Hbody as (Htrue & Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lj (vj& gj & HPj & Hlt & Qji); eauto 9. }
     { eauto. }
   Qed.
@@ -85,14 +107,12 @@ Section Loops.
     destruct Hbody as (br & ? & Hbody). exists br; split; [assumption|].
     destruct Hbody as (Htrue & Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lj (vj& gj & HPj & Hlt & Qji). do 2 eexists.
       split. 1: eassumption. split. 1: assumption.
       intros.
-      eapply Proper_cmd; [reflexivity..| | | ].
-      3: eassumption.
-      { eapply Proper_call; firstorder idtac. }
+      eapply Proper_cmd.
+      2: eassumption.
       intros tk mk lk HH. eapply Qji. assumption. }
     eapply Hpc.
   Qed.
@@ -166,10 +186,11 @@ Section Loops.
       invariant v t m l ->
       exists br, expr m l e (eq br) /\
          (word.unsigned br <> 0 ->
-          cmd call c t m l (fun t m l => exists v', invariant v' t m l /\ lt v' v)) /\
+          cmd fs c t m l (fun t m l => exists v', invariant v' t m l /\ lt v' v)) /\
          (word.unsigned br = 0 -> post t m l))
-    : cmd call (cmd.while e c) t m l post.
+    : cmd fs (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists measure, lt, invariant.
     split. 1: exact Hwf.
     split. 1: eauto.
@@ -210,7 +231,7 @@ Section Loops.
     destruct Hbody as (br & Cond & Again & Done).
     exists br. split; [exact Cond|]. split; [|exact Done].
     intro NE. specialize (Again NE).
-    eapply Proper_cmd; [eapply Proper_call| |eapply Again].
+    eapply Proper_cmd; [ |eapply Again].
     cbv [Morphisms.pointwise_relation Basics.impl Markers.right Markers.unique Markers.left] in *.
     intros t' m' l' Ex.
     eapply hlist.existss_exists in Ex. cbv beta in Ex. destruct Ex as (ls & E & v' & Inv' & LT).
@@ -247,6 +268,7 @@ Section Loops.
     , cmd call (cmd.while e c) t m localsmap post ).
   Proof.
     eapply hlist_forall_foralls; intros g0 **.
+    eapply wp_while.
     eexists measure, lt, (fun vi ti mi localsmapi =>
       exists gi li, localsmapi = reconstruct variables li /\
       match tuple.apply (hlist.apply (spec vi) gi ti mi) li with S_ =>
@@ -259,8 +281,7 @@ Section Loops.
     destruct (hlist.foralls_forall (hlist.foralls_forall (Hbody vi) gi ti mi) _ ltac:(eassumption)) as (br&?&X).
     exists br; split; [assumption|]. destruct X as (Htrue&Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lmapj Hlj; eapply hlist.existss_exists in Hlj.
       destruct Hlj as (lj&Elj&HE); eapply reconstruct_enforce in Elj; subst lmapj.
       eapply hlist.existss_exists in HE. destruct HE as (l&?&?&?&HR).
@@ -289,6 +310,7 @@ Section Loops.
     (Hpost : forall t m l, Q0 t m l -> post t m l)
     : cmd call (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists measure, lt, (fun v t m l =>
       let S := spec v t m l in let '(P, Q) := S in
       P /\ forall T M L, Q T M L -> Q0 T M L).
@@ -299,8 +321,7 @@ Section Loops.
     destruct (Hbody _ _ _ _ ltac:(eassumption)) as (br&?&X); exists br; split; [assumption|].
     destruct X as (Htrue&Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lj (vj&dP&?&dQ); eauto 9. }
     { eauto. }
   Qed.
@@ -334,6 +355,7 @@ Section Loops.
          (word.unsigned br =  0 -> post t m l)))
     : cmd call (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists (option measure), (with_bottom lt), (fun ov t m l =>
       exists br, expr m l e (eq br) /\
       ((word.unsigned br <> 0 -> exists v, ov = Some v /\ invariant v t m l) /\
@@ -349,7 +371,7 @@ Section Loops.
     intros vi ti mi li (br&Ebr&Hcontinue&Hexit).
     eexists; split; [eassumption|]; split.
     { intros Hc; destruct (Hcontinue Hc) as (v&?&Hinv); subst.
-      eapply Proper_cmd; [| |eapply Hbody; eassumption]; [eapply Proper_call|].
+      eapply Proper_cmd; [ |eapply Hbody; eassumption].
       intros t' m' l' (br'&Ebr'&Hinv'&Hpost').
       destruct (BinInt.Z.eq_dec (word.unsigned br') 0).
       { exists None; split; try constructor.
@@ -385,6 +407,7 @@ Section Loops.
     (Hpost : forall t m l, Q0 t m l -> post t m l)
     : cmd call (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists (option measure), (with_bottom lt), (fun v t m l =>
       match v with
       | None => exists br, expr m l e (eq br) /\ word.unsigned br = 0 /\ Q0 t m l
@@ -399,8 +422,7 @@ Section Loops.
     { destruct (Hbody _ _ _ _ ltac:(eassumption)) as (br&?&X); exists br; split; [assumption|].
       destruct X as (Htrue&Hfalse). split; intros Hbr;
         [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; eauto.
-      eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+      eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lj [(br'&Hbr'&Hz&HQ)|(vj&dP&?&dQ)];
           [exists None | exists (Some vj)]; cbn [with_bottom]; eauto 9. }
     repeat esplit || eauto || intros; contradiction.
@@ -437,6 +459,7 @@ Section Loops.
     , cmd call (cmd.while e c) t m localsmap post ).
   Proof.
     eapply hlist_forall_foralls; intros g0 **.
+    eapply wp_while.
     eexists (option measure), (with_bottom lt), (fun vi ti mi localsmapi =>
       exists li, localsmapi = reconstruct variables li /\
       match vi with None => exists br, expr mi localsmapi e (eq br) /\ word.unsigned br = 0 /\ tuple.apply ((tuple.apply (hlist.apply (spec v0) g0 t m) l0).(2) ti mi) li | Some vi =>
@@ -455,8 +478,7 @@ Section Loops.
     destruct (hlist.foralls_forall (hlist.foralls_forall (Hbody vi) gi ti mi) _ ltac:(eassumption)) as (br&?&X).
     exists br; split; [assumption|]. destruct X as (Htrue&Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lmapj Hlj; eapply hlist.existss_exists in Hlj.
       destruct Hlj as (lj&Elj&HE); eapply reconstruct_enforce in Elj; subst lmapj.
       destruct HE as [(br'&Hevalr'&Hz'&Hdone)|HE].
@@ -492,7 +514,7 @@ Section Loops.
     eapply hlist.foralls_forall in Hbody.
     specialize (Hbody Y).
     rewrite <-(reconstruct_enforce _ _ _ X) in Hbody.
-    eapply Proper_cmd; [eapply Proper_call| |eapply Hbody].
+    eapply Proper_cmd; [ |eapply Hbody].
     intros t' m' l' (?&?&HH&?).
     eexists; split; eauto.
     split; intros; eauto.
@@ -533,6 +555,7 @@ Section Loops.
     (Hpost : forall t m l, (Q v0 t l * R0) m -> post t m l)
     : cmd call (cmd.while e c) t m l post.
   Proof.
+    eapply wp_while.
     eexists measure, lt, (fun v t m l => exists R, (P v t l * R) m /\
                           forall T L, Q v T L * R ==> Q v0 T L * R0).
     split; [assumption|].
@@ -541,8 +564,7 @@ Section Loops.
     destruct (Hbody _ _ _ _ _ ltac:(eassumption)) as (br&?&X); exists br; split; [assumption|].
     destruct X as (Htrue&Hfalse). split; intros Hbr;
       [pose proof(Htrue Hbr)as Hpc|pose proof(Hfalse Hbr)as Hpc]; clear Hbr Htrue Hfalse.
-    { eapply Proper_cmd; [reflexivity..| | |eapply Hpc].
-      { eapply Proper_call; firstorder idtac. }
+    { eapply Proper_cmd; [ |eapply Hpc].
       intros tj mj lj (vj&dR&dP&?&dQ).
       exists vj; split; [|assumption].
       exists (Ri * dR); split; [assumption|].
diff --git a/bedrock2/src/bedrock2/MetricSemantics.v b/bedrock2/src/bedrock2/MetricSemantics.v
new file mode 100644
index 000000000..51565d555
--- /dev/null
+++ b/bedrock2/src/bedrock2/MetricSemantics.v
@@ -0,0 +1,449 @@
+Require Import coqutil.sanity coqutil.Byte.
+Require Import coqutil.Tactics.fwd.
+Require Import coqutil.Map.Properties.
+Require coqutil.Map.SortedListString.
+Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
+Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
+Require Export bedrock2.Memory.
+Require Import Coq.Lists.List.
+Require Import bedrock2.MetricLogging.
+Require Import bedrock2.Semantics.
+Require Import Coq.Lists.List.
+
+Section semantics.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec}.
+
+  Local Notation metrics := MetricLog.
+
+  Section WithMemAndLocals.
+    Context (m : mem) (l : locals).
+
+    Local Notation "' x <- a | y ; f" := (match a with x => f | _ => y end)
+      (right associativity, at level 70, x pattern).
+
+    Fixpoint eval_expr (e : expr) (mc : metrics) : option (word * metrics) :=
+      match e with
+      | expr.literal v => Some (word.of_Z v, addMetricInstructions 8
+                                             (addMetricLoads 8 mc))
+      | expr.var x => match map.get l x with
+                      | Some v => Some (v, addMetricInstructions 1
+                                           (addMetricLoads 2 mc))
+                      | None => None
+                      end
+      | expr.inlinetable aSize t index =>
+          'Some (index', mc') <- eval_expr index mc | None;
+          'Some v <- load aSize (map.of_list_word t) index' | None;
+          Some (v, (addMetricInstructions 3
+                   (addMetricLoads 4
+                   (addMetricJumps 1 mc'))))
+      | expr.load aSize a =>
+          'Some (a', mc') <- eval_expr a mc | None;
+          'Some v <- load aSize m a' | None;
+          Some (v, addMetricInstructions 1
+                   (addMetricLoads 2 mc'))
+      | expr.op op e1 e2 =>
+          'Some (v1, mc') <- eval_expr e1 mc | None;
+          'Some (v2, mc'') <- eval_expr e2 mc' | None;
+          Some (interp_binop op v1 v2, addMetricInstructions 2
+                                       (addMetricLoads 2 mc''))
+      | expr.ite c e1 e2 =>
+          'Some (vc, mc') <- eval_expr c mc | None;
+          eval_expr (if word.eqb vc (word.of_Z 0) then e2 else e1)
+                    (addMetricInstructions 2
+                       (addMetricLoads 2
+                       (addMetricJumps 1 mc')))
+      end.
+
+    Fixpoint eval_call_args (arges : list expr) (mc : metrics) :=
+      match arges with
+      | e :: tl =>
+        'Some (v, mc') <- eval_expr e mc | None;
+        'Some (args, mc'') <- eval_call_args tl mc' | None;
+        Some (v :: args, mc'')
+      | _ => Some (nil, mc)
+      end.
+
+  End WithMemAndLocals.
+End semantics.
+
+Module exec. Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec}.
+  Section WithEnv.
+  Context (e: env).
+
+  Local Notation metrics := MetricLog.
+
+  Implicit Types post : trace -> mem -> locals -> metrics -> Prop. (* COQBUG: unification finds Type instead of Prop and fails to downgrade *)
+  Inductive exec :
+    cmd -> trace -> mem -> locals -> metrics ->
+    (trace -> mem -> locals -> metrics -> Prop) -> Prop :=
+  | skip
+    t m l mc post
+    (_ : post t m l mc)
+    : exec cmd.skip t m l mc post
+  | set x e
+    t m l mc post
+    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
+    (_ : post t m (map.put l x v) (addMetricInstructions 1
+                                  (addMetricLoads 1 mc')))
+    : exec (cmd.set x e) t m l mc post
+  | unset x
+    t m l mc post
+    (_ : post t m (map.remove l x) mc)
+    : exec (cmd.unset x) t m l mc post
+  | store sz ea ev
+    t m l mc post
+    a mc' (_ : eval_expr m l ea mc = Some (a, mc'))
+    v mc'' (_ : eval_expr m l ev mc' = Some (v, mc''))
+    m' (_ : store sz m a v = Some m')
+    (_ : post t m' l (addMetricInstructions 1
+                     (addMetricLoads 1
+                     (addMetricStores 1 mc''))))
+    : exec (cmd.store sz ea ev) t m l mc post
+  | stackalloc x n body
+    t mSmall l mc post
+    (_ : Z.modulo n (bytes_per_word width) = 0)
+    (_ : forall a mStack mCombined,
+        anybytes a n mStack ->
+        map.split mCombined mSmall mStack ->
+        exec body t mCombined (map.put l x a) (addMetricInstructions 1 (addMetricLoads 1 mc))
+          (fun t' mCombined' l' mc' =>
+            exists mSmall' mStack',
+              anybytes a n mStack' /\
+              map.split mCombined' mSmall' mStack' /\
+              post t' mSmall' l' mc'))
+     : exec (cmd.stackalloc x n body) t mSmall l mc post
+  | if_true t m l mc e c1 c2 post
+    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
+    (_ : word.unsigned v <> 0)
+    (_ : exec c1 t m l (addMetricInstructions 2
+                       (addMetricLoads 2
+                       (addMetricJumps 1 mc'))) post)
+    : exec (cmd.cond e c1 c2) t m l mc post
+  | if_false e c1 c2
+    t m l mc post
+    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
+    (_ : word.unsigned v = 0)
+    (_ : exec c2 t m l (addMetricInstructions 2
+                       (addMetricLoads 2
+                       (addMetricJumps 1 mc'))) post)
+    : exec (cmd.cond e c1 c2) t m l mc post
+  | seq c1 c2
+    t m l mc post
+    mid (_ : exec c1 t m l mc mid)
+    (_ : forall t' m' l' mc', mid t' m' l' mc' -> exec c2 t' m' l' mc' post)
+    : exec (cmd.seq c1 c2) t m l mc post
+  | while_false e c
+    t m l mc post
+    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
+    (_ : word.unsigned v = 0)
+    (_ : post t m l (addMetricInstructions 1
+                    (addMetricLoads 1
+                    (addMetricJumps 1 mc'))))
+    : exec (cmd.while e c) t m l mc post
+  | while_true e c
+      t m l mc post
+      v mc' (_ : eval_expr m l e mc = Some (v, mc'))
+      (_ : word.unsigned v <> 0)
+      mid (_ : exec c t m l mc' mid)
+      (_ : forall t' m' l' mc'', mid t' m' l' mc'' ->
+                                 exec (cmd.while e c) t' m' l' (addMetricInstructions 2
+                                                               (addMetricLoads 2
+                                                               (addMetricJumps 1 mc''))) post)
+    : exec (cmd.while e c) t m l mc post
+  | call binds fname arges
+      t m l mc post
+      params rets fbody (_ : map.get e fname = Some (params, rets, fbody))
+      args mc' (_ : eval_call_args m l arges mc = Some (args, mc'))
+      lf (_ : map.of_list_zip params args = Some lf)
+      mid (_ : exec fbody t m lf (addMetricInstructions 100 (addMetricJumps 100 (addMetricLoads 100 (addMetricStores 100 mc')))) mid)
+      (_ : forall t' m' st1 mc'', mid t' m' st1 mc'' ->
+          exists retvs, map.getmany_of_list st1 rets = Some retvs /\
+          exists l', map.putmany_of_list_zip binds retvs l = Some l' /\
+          post t' m' l'  (addMetricInstructions 100 (addMetricJumps 100 (addMetricLoads 100 (addMetricStores 100 mc'')))))
+    : exec (cmd.call binds fname arges) t m l mc post
+  | interact binds action arges
+      t m l mc post
+      mKeep mGive (_: map.split m mKeep mGive)
+      args mc' (_ :  eval_call_args m l arges mc = Some (args, mc'))
+      mid (_ : ext_spec t mGive action args mid)
+      (_ : forall mReceive resvals, mid mReceive resvals ->
+          exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
+          forall m', map.split m' mKeep mReceive ->
+          post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l'
+            (addMetricInstructions 1
+            (addMetricStores 1
+            (addMetricLoads 2 mc'))))
+    : exec (cmd.interact binds action arges) t m l mc post
+  .
+
+  Context {word_ok: word.ok word} {mem_ok: map.ok mem} {ext_spec_ok: ext_spec.ok ext_spec}.
+
+  Lemma weaken: forall t l m mc s post1,
+      exec s t m l mc post1 ->
+      forall post2: _ -> _ -> _ -> _ -> Prop,
+        (forall t' m' l' mc', post1 t' m' l' mc' -> post2 t' m' l' mc') ->
+        exec s t m l mc post2.
+  Proof.
+    induction 1; intros; try solve [econstructor; eauto].
+    - eapply stackalloc. 1: assumption.
+      intros.
+      eapply H1; eauto.
+      intros. fwd. eauto 10.
+    - eapply call.
+      4: eapply IHexec.
+      all: eauto.
+      intros.
+      edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
+      eauto 10.
+    - eapply interact; try eassumption.
+      intros.
+      edestruct H2 as (? & ? & ?); [eassumption|].
+      eauto 10.
+  Qed.
+
+  Lemma intersect: forall t l m mc s post1,
+      exec s t m l mc post1 ->
+      forall post2,
+        exec s t m l mc post2 ->
+        exec s t m l mc (fun t' m' l' mc' => post1 t' m' l' mc' /\ post2 t' m' l' mc').
+  Proof.
+    induction 1;
+      intros;
+      match goal with
+      | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H
+      end;
+      try match goal with
+      | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ =>
+        replace x2 with x1 in * by congruence;
+          replace y2 with y1 in * by congruence;
+          replace z2 with z1 in * by congruence;
+          clear x2 y2 z2 H2
+      end;
+      repeat match goal with
+             | H1: ?e = Some (?v1, ?mc1), H2: ?e = Some (?v2, ?mc2) |- _ =>
+               replace v2 with v1 in * by congruence;
+               replace mc2 with mc1 in * by congruence; clear H2
+             end;
+      repeat match goal with
+             | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+               replace v2 with v1 in * by congruence; clear H2
+             end;
+      try solve [econstructor; eauto | exfalso; congruence].
+
+    - econstructor. 1: eassumption.
+      intros.
+      rename H0 into Ex1, H12 into Ex2.
+      eapply weaken. 1: eapply H1. 1,2: eassumption.
+      1: eapply Ex2. 1,2: eassumption.
+      cbv beta.
+      intros. fwd.
+      lazymatch goal with
+      | A: map.split _ _ _, B: map.split _ _ _ |- _ =>
+        specialize @map.split_diff with (4 := A) (5 := B) as P
+      end.
+      edestruct P; try typeclasses eauto. 2: subst; eauto 10.
+      eapply anybytes_unique_domain; eassumption.
+    - econstructor.
+      + eapply IHexec. exact H5. (* not H *)
+      + simpl. intros *. intros [? ?]. eauto.
+    - eapply while_true. 1, 2: eassumption.
+      + eapply IHexec. exact H9. (* not H1 *)
+      + simpl. intros *. intros [? ?]. eauto.
+    - eapply call. 1, 2, 3: eassumption.
+      + eapply IHexec. exact H16. (* not H2 *)
+      + simpl. intros *. intros [? ?].
+        edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
+        edestruct H17 as (? & ? & ? & ? & ?); [eassumption|].
+        repeat match goal with
+               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+                 replace v2 with v1 in * by congruence; clear H2
+               end.
+        eauto 10.
+    - pose proof ext_spec.unique_mGive_footprint as P.
+      specialize P with (1 := H1) (2 := H14).
+      destruct (map.split_diff P H H7). subst mKeep0 mGive0. clear H7.
+      eapply interact. 1,2: eassumption.
+      + eapply ext_spec.intersect; [ exact H1 | exact H14 ].
+      + simpl. intros *. intros [? ?].
+        edestruct H2 as (? & ? & ?); [eassumption|].
+        edestruct H15 as (? & ? & ?); [eassumption|].
+        repeat match goal with
+               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+                 replace v2 with v1 in * by congruence; clear H2
+               end.
+        eauto 10.
+  Qed.
+
+  End WithEnv.
+
+  Lemma extend_env: forall e1 e2,
+      map.extends e2 e1 ->
+      forall c t m l mc post,
+      exec e1 c t m l mc post ->
+      exec e2 c t m l mc post.
+  Proof. induction 2; try solve [econstructor; eauto]. Qed.
+
+  End WithParams.
+End exec. Notation exec := exec.exec.
+
+Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec}.
+
+  Implicit Types (l: locals) (m: mem).
+
+  Definition call e fname t m args mc post :=
+    exists argnames retnames body,
+      map.get e fname = Some (argnames, retnames, body) /\
+      exists l, map.of_list_zip argnames args = Some l /\
+        exec e body t m l mc (fun t' m' l' mc' => exists rets,
+          map.getmany_of_list l' retnames = Some rets /\ post t' m' rets mc').
+
+  Lemma weaken_call: forall e fname t m args mc post1,
+      call e fname t m args mc post1 ->
+      forall (post2: trace -> mem -> list word -> MetricLog -> Prop),
+      (forall t' m' rets mc', post1 t' m' rets mc' -> post2 t' m' rets mc') ->
+      call e fname t m args mc post2.
+  Proof.
+    unfold call. intros. fwd.
+    do 4 eexists. 1: eassumption.
+    do 2 eexists. 1: eassumption.
+    eapply exec.weaken. 1: eassumption.
+    cbv beta. clear -H0. intros. fwd. eauto.
+  Qed.
+
+  Lemma extend_env_call: forall e1 e2,
+      map.extends e2 e1 ->
+      forall f t m rets mc post,
+      call e1 f t m rets mc post ->
+      call e2 f t m rets mc post.
+  Proof.
+    unfold call. intros. fwd. repeat eexists.
+    - eapply H. eassumption.
+    - eassumption.
+    - eapply exec.extend_env; eassumption.
+  Qed.
+
+  Lemma of_metrics_free_eval_expr: forall m l e v,
+      Semantics.eval_expr m l e = Some v ->
+      forall mc, exists mc', MetricSemantics.eval_expr m l e mc = Some (v, mc').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | H: _ = Some _ |- _ => rewrite H
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _: MetricLog, exists _: MetricLog, eval_expr ?m ?l ?e _ = Some _
+          |- context[eval_expr ?m ?l ?e ?mc] => specialize (IH mc)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma to_metrics_free_eval_expr: forall m l e mc v mc',
+      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
+      Semantics.eval_expr m l e = Some v.
+  Proof.
+    induction e; cbn; intros; fwd;
+      repeat match goal with
+        | IH: forall _ _ _, eval_expr _ _ _ _ = _ -> _, H: eval_expr _ _ _ _ = _ |- _ =>
+          specialize IH with (1 := H)
+        | H: _ = Some _ |- _ => rewrite H
+        | |- _ => Tactics.destruct_one_match
+        end;
+    try congruence.
+  Qed.
+
+  Lemma of_metrics_free_eval_call_args: forall m l arges args,
+      Semantics.eval_call_args m l arges = Some args ->
+      forall mc, exists mc', MetricSemantics.eval_call_args m l arges mc = Some (args, mc').
+  Proof.
+    induction arges; cbn; intros.
+    - eapply Option.eq_of_eq_Some in H. subst. eauto.
+    - fwd.
+      eapply of_metrics_free_eval_expr in E. destruct E as (mc' & E). rewrite E.
+      specialize IHarges with (1 := eq_refl). specialize (IHarges mc').
+      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Lemma to_metrics_free_eval_call_args: forall m l arges mc args mc',
+      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
+      Semantics.eval_call_args m l arges = Some args.
+  Proof.
+    induction arges; cbn; intros.
+    - congruence.
+    - fwd.
+      eapply to_metrics_free_eval_expr in E. rewrite E.
+      specialize IHarges with (1 := E0). rewrite IHarges. reflexivity.
+  Qed.
+
+  Context (e: env).
+
+  Lemma of_metrics_free: forall c t m l post,
+      Semantics.exec e c t m l post ->
+      forall mc, MetricSemantics.exec e c t m l mc (fun t' m' l' _ => post t' m' l').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
+            eapply of_metrics_free_eval_expr in H; destruct H as (? & H)
+        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
+            eapply of_metrics_free_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+
+  Lemma to_metrics_free: forall c t m l mc post,
+      MetricSemantics.exec e c t m l mc post ->
+      Semantics.exec e c t m l (fun t' m' l' => exists mc', post t' m' l' mc').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: eval_expr _ _ _ _ = Some _ |- _ =>
+            eapply to_metrics_free_eval_expr in H
+        | H: eval_call_args _ _ _ _ = Some _ |- _ =>
+            eapply to_metrics_free_eval_call_args in H
+        end;
+      try solve [econstructor; eauto].
+    { econstructor. 1: eauto.
+      intros.
+      eapply Semantics.exec.weaken. 1: eapply H1. all: eauto.
+      cbv beta.
+      clear. firstorder idtac. }
+    { econstructor.
+      1: eapply IHexec.
+      cbv beta. intros.
+      fwd.
+      eapply H1. eassumption. }
+    { econstructor; [ eassumption .. | ].
+      cbv beta. intros. fwd. eapply H3. eassumption. }
+    { econstructor. 1-4: eassumption.
+      cbv beta. intros. fwd. specialize H3 with (1 := H4). fwd. eauto 10. }
+    { econstructor. 1-3: eassumption.
+      intros. specialize H2 with (1 := H3). fwd. eauto. }
+  Qed.
+
+  Lemma of_metrics_free_call: forall f t m args post,
+      Semantics.call e f t m args post ->
+      forall mc, call e f t m args mc (fun t' m' rets _ => post t' m' rets).
+  Proof.
+    unfold call, Semantics.call. intros. fwd. eauto 10 using of_metrics_free.
+  Qed.
+
+  Lemma to_metrics_free_call: forall f t m args mc post,
+      call e f t m args mc post ->
+      Semantics.call e f t m args (fun t' m' rets => exists mc', post t' m' rets mc').
+  Proof.
+    unfold call, Semantics.call. intros. fwd.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
+    eapply Semantics.exec.weaken. 1: eapply to_metrics_free. 1: eassumption.
+    cbv beta. clear. firstorder idtac.
+  Qed.
+End WithParams.
diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index b0a5b6e63..009f465a4 100644
--- a/bedrock2/src/bedrock2/ProgramLogic.v
+++ b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -1,11 +1,12 @@
 From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string.
+Require Import coqutil.Map.Interface.
 Require Import bedrock2.Syntax.
 Require Import bedrock2.WeakestPrecondition.
 Require Import bedrock2.WeakestPreconditionProperties.
 Require Import bedrock2.Loops.
 Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.
 
-Definition spec_of (procname:String.string) := list (String.string * (list String.string * list String.string * Syntax.cmd.cmd)) -> Prop.
+Definition spec_of (procname:String.string) := Semantics.env -> Prop.
 Existing Class spec_of.
 
 Module Import Coercions.
@@ -55,9 +56,9 @@ Ltac program_logic_goal_for_function proc :=
   let __ := constr:(proc : Syntax.func) in
   constr_string_basename_of_constr_reference_cps ltac:(Tactics.head proc) ltac:(fun fname =>
   let spec := lazymatch constr:(_:spec_of fname) with ?s => s end in
-  exact (forall functions : list (string * Syntax.func), ltac:(
+  exact (forall (functions : @map.rep _ _ Semantics.env) (EnvContains : map.get functions fname = Some proc), ltac:(
     let callees := eval cbv in (callees (snd proc)) in
-    let s := assuming_correctness_of_in callees functions (spec (cons (fname, proc) functions)) in
+    let s := assuming_correctness_of_in callees functions (spec functions) in
     exact s))).
 Definition program_logic_goal_for (_ : Syntax.func) (P : Prop) := P.
 
@@ -84,7 +85,7 @@ Ltac bind_body_of_function f_ :=
 
 (* note: f might have some implicit parameters (eg a record of constants) *)
 Ltac enter f :=
-  cbv beta delta [program_logic_goal_for]; intros;
+  cbv beta delta [program_logic_goal_for];
   bind_body_of_function f;
   lazymatch goal with |- ?s ?p => let s := rdelta s in change (s p); cbv beta end.
 
@@ -229,9 +230,10 @@ Ltac straightline :=
   | _ => straightline_cleanup
   | |- program_logic_goal_for ?f _ =>
     enter f; intros;
-    unfold1_call_goal; cbv match beta delta [call_body];
-    lazymatch goal with |- if ?test then ?T else _ =>
-      replace test with true by reflexivity; change T end;
+    match goal with
+    | H: map.get ?functions ?fname = Some _ |- _ =>
+        eapply start_func; [exact H | clear H]
+    end;
     cbv match beta delta [WeakestPrecondition.func]
   | |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
     unfold1_cmd_goal; cbv beta match delta [cmd_body];
diff --git a/bedrock2/src/bedrock2/Refinement.v b/bedrock2/src/bedrock2/Refinement.v
new file mode 100644
index 000000000..236866e3b
--- /dev/null
+++ b/bedrock2/src/bedrock2/Refinement.v
@@ -0,0 +1,46 @@
+(* These lemmas can be useful when proving a refinement and induction over the
+   statement rather than over its exec derivation is preferred *)
+
+Require Import Coq.ZArith.ZArith.
+Require Import coqutil.Word.Bitwidth.
+Require Import coqutil.Map.Interface.
+Require Import bedrock2.Syntax bedrock2.Semantics.
+
+Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width}.
+  Context {mem: map.map word Byte.byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: bedrock2.Semantics.ExtSpec}.
+
+  Definition refines(c2 c1: cmd) := forall functions t m l post,
+      Semantics.exec.exec functions c1 t m l post ->
+      Semantics.exec.exec functions c2 t m l post.
+
+  Lemma refinement_while: forall test body1 body2,
+      refines body2 body1 ->
+      refines (cmd.while test body2) (cmd.while test body1).
+  Proof.
+    unfold refines. intros * R *.
+    remember (cmd.while test body1) as c1. intros. revert Heqc1.
+    induction H; intros; subst; inversion Heqc1; subst.
+    - eapply Semantics.exec.while_false; eassumption.
+    - eapply Semantics.exec.while_true; try eassumption.
+      { unfold refines in R.
+        eapply R. eassumption. }
+      intros.
+      eapply H3; eauto.
+  Qed.
+
+  Lemma refinement_seq: forall c1 c2 c1' c2',
+      refines c1' c1 ->
+      refines c2' c2 ->
+      refines (cmd.seq c1' c2') (cmd.seq c1 c2).
+  Proof.
+    intros * R1 R2 functions t m l post H.
+    unfold refines in *.
+    inversion H. subst. clear H.
+    eapply Semantics.exec.seq.
+    - eapply R1. eassumption.
+    - intros * Hmid. eapply R2. eauto.
+  Qed.
+End WithParams.
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
index 1820df16e..28f773eb9 100644
--- a/bedrock2/src/bedrock2/Semantics.v
+++ b/bedrock2/src/bedrock2/Semantics.v
@@ -1,13 +1,10 @@
-Require Import coqutil.sanity coqutil.Macros.subst coqutil.Macros.unique coqutil.Byte.
-Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList.
-Require Import coqutil.Decidable.
+Require Import coqutil.sanity coqutil.Byte.
 Require Import coqutil.Tactics.fwd.
 Require Import coqutil.Map.Properties.
+Require coqutil.Map.SortedListString.
 Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
-Require Import bedrock2.MetricLogging.
 Require Export bedrock2.Memory.
-
 Require Import Coq.Lists.List.
 
 (* BW is not needed on the rhs, but helps infer width *)
@@ -78,205 +75,142 @@ Section binops.
     end.
 End binops.
 
+Definition env: map.map String.string Syntax.func := SortedListString.map _.
+#[export] Instance env_ok: map.ok env := SortedListString.ok _.
+
 Section semantics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
-  Local Notation metrics := MetricLog.
-
   (* this is the expr evaluator that is used to verify execution time, the just-correctness-oriented version is below *)
   Section WithMemAndLocals.
     Context (m : mem) (l : locals).
 
-    Local Notation "' x <- a | y ; f" := (match a with x => f | _ => y end)
-      (right associativity, at level 70, x pattern).
+    Local Notation "x <- a ; f" := (match a with Some x => f | None => None end)
+      (right associativity, at level 70).
 
-    Fixpoint eval_expr (e : expr) (mc : metrics) : option (word * metrics) :=
-      match e with
-      | expr.literal v => Some (word.of_Z v, addMetricInstructions 8
-                                             (addMetricLoads 8 mc))
-      | expr.var x => match map.get l x with
-                      | Some v => Some (v, addMetricInstructions 1
-                                           (addMetricLoads 2 mc))
-                      | None => None
-                      end
-      | expr.inlinetable aSize t index =>
-          'Some (index', mc') <- eval_expr index mc | None;
-          'Some v <- load aSize (map.of_list_word t) index' | None;
-          Some (v, (addMetricInstructions 3
-                   (addMetricLoads 4
-                   (addMetricJumps 1 mc'))))
-      | expr.load aSize a =>
-          'Some (a', mc') <- eval_expr a mc | None;
-          'Some v <- load aSize m a' | None;
-          Some (v, addMetricInstructions 1
-                   (addMetricLoads 2 mc'))
-      | expr.op op e1 e2 =>
-          'Some (v1, mc') <- eval_expr e1 mc | None;
-          'Some (v2, mc'') <- eval_expr e2 mc' | None;
-          Some (interp_binop op v1 v2, addMetricInstructions 2
-                                       (addMetricLoads 2 mc''))
-      | expr.ite c e1 e2 =>
-          'Some (vc, mc') <- eval_expr c mc | None;
-          eval_expr (if word.eqb vc (word.of_Z 0) then e2 else e1)
-                    (addMetricInstructions 2
-                       (addMetricLoads 2
-                       (addMetricJumps 1 mc')))
-      end.
-
-    Fixpoint eval_expr_old (e : expr) : option word :=
+    Fixpoint eval_expr (e : expr) : option word :=
       match e with
       | expr.literal v => Some (word.of_Z v)
       | expr.var x => map.get l x
       | expr.inlinetable aSize t index =>
-          'Some index' <- eval_expr_old index | None;
+          index' <- eval_expr index;
           load aSize (map.of_list_word t) index'
       | expr.load aSize a =>
-          'Some a' <- eval_expr_old a | None;
+          a' <- eval_expr a;
           load aSize m a'
       | expr.op op e1 e2 =>
-          'Some v1 <- eval_expr_old e1 | None;
-          'Some v2 <- eval_expr_old e2 | None;
+          v1 <- eval_expr e1;
+          v2 <- eval_expr e2;
           Some (interp_binop op v1 v2)
       | expr.ite c e1 e2 =>
-          'Some vc <- eval_expr_old c | None;
-          eval_expr_old (if word.eqb vc (word.of_Z 0) then e2 else e1)
+          vc <- eval_expr c;
+          eval_expr (if word.eqb vc (word.of_Z 0) then e2 else e1)
       end.
 
-    Fixpoint evaluate_call_args_log (arges : list expr) (mc : metrics) :=
+    Fixpoint eval_call_args (arges : list expr) :=
       match arges with
       | e :: tl =>
-        'Some (v, mc') <- eval_expr e mc | None;
-        'Some (args, mc'') <- evaluate_call_args_log tl mc' | None;
-        Some (v :: args, mc'')
-      | _ => Some (nil, mc)
+        v <- eval_expr e;
+        args <- eval_call_args tl;
+        Some (v :: args)
+      | _ => Some nil
       end.
 
   End WithMemAndLocals.
 End semantics.
 
-Module exec. Section WithEnv.
+Module exec. Section WithParams.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
+  Section WithEnv.
   Context (e: env).
 
-  Local Notation metrics := MetricLog.
-
-  Implicit Types post : trace -> mem -> locals -> metrics -> Prop. (* COQBUG(unification finds Type instead of Prop and fails to downgrade *)
-  Inductive exec :
-    cmd -> trace -> mem -> locals -> metrics ->
-    (trace -> mem -> locals -> metrics -> Prop) -> Prop :=
-  | skip
-    t m l mc post
-    (_ : post t m l mc)
-    : exec cmd.skip t m l mc post
-  | set x e
-    t m l mc post
-    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
-    (_ : post t m (map.put l x v) (addMetricInstructions 1
-                                  (addMetricLoads 1 mc')))
-    : exec (cmd.set x e) t m l mc post
-  | unset x
-    t m l mc post
-    (_ : post t m (map.remove l x) mc)
-    : exec (cmd.unset x) t m l mc post
-  | store sz ea ev
-    t m l mc post
-    a mc' (_ : eval_expr m l ea mc = Some (a, mc'))
-    v mc'' (_ : eval_expr m l ev mc' = Some (v, mc''))
-    m' (_ : store sz m a v = Some m')
-    (_ : post t m' l (addMetricInstructions 1
-                     (addMetricLoads 1
-                     (addMetricStores 1 mc''))))
-    : exec (cmd.store sz ea ev) t m l mc post
-  | stackalloc x n body
-    t mSmall l mc post
-    (_ : Z.modulo n (bytes_per_word width) = 0)
-    (_ : forall a mStack mCombined,
+  Implicit Types post : trace -> mem -> locals -> Prop. (* COQBUG: unification finds Type instead of Prop and fails to downgrade *)
+  Inductive exec: cmd -> trace -> mem -> locals ->
+                  (trace -> mem -> locals -> Prop) -> Prop :=
+  | skip: forall t m l post,
+      post t m l ->
+      exec cmd.skip t m l post
+  | set: forall x e t m l post v,
+      eval_expr m l e = Some v ->
+      post t m (map.put l x v) ->
+      exec (cmd.set x e) t m l post
+  | unset: forall x t m l post,
+      post t m (map.remove l x) ->
+      exec (cmd.unset x) t m l post
+  | store: forall sz ea ev t m l post a v m',
+      eval_expr m l ea = Some a ->
+      eval_expr m l ev = Some v ->
+      store sz m a v = Some m' ->
+      post t m' l ->
+      exec (cmd.store sz ea ev) t m l post
+  | stackalloc: forall x n body t mSmall l post,
+      Z.modulo n (bytes_per_word width) = 0 ->
+      (forall a mStack mCombined,
         anybytes a n mStack ->
         map.split mCombined mSmall mStack ->
-        exec body t mCombined (map.put l x a) (addMetricInstructions 1 (addMetricLoads 1 mc))
-          (fun t' mCombined' l' mc' =>
+        exec body t mCombined (map.put l x a)
+          (fun t' mCombined' l' =>
             exists mSmall' mStack',
               anybytes a n mStack' /\
               map.split mCombined' mSmall' mStack' /\
-              post t' mSmall' l' mc'))
-     : exec (cmd.stackalloc x n body) t mSmall l mc post
-  | if_true t m l mc e c1 c2 post
-    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
-    (_ : word.unsigned v <> 0)
-    (_ : exec c1 t m l (addMetricInstructions 2
-                       (addMetricLoads 2
-                       (addMetricJumps 1 mc'))) post)
-    : exec (cmd.cond e c1 c2) t m l mc post
-  | if_false e c1 c2
-    t m l mc post
-    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
-    (_ : word.unsigned v = 0)
-    (_ : exec c2 t m l (addMetricInstructions 2
-                       (addMetricLoads 2
-                       (addMetricJumps 1 mc'))) post)
-    : exec (cmd.cond e c1 c2) t m l mc post
-  | seq c1 c2
-    t m l mc post
-    mid (_ : exec c1 t m l mc mid)
-    (_ : forall t' m' l' mc', mid t' m' l' mc' -> exec c2 t' m' l' mc' post)
-    : exec (cmd.seq c1 c2) t m l mc post
-  | while_false e c
-    t m l mc post
-    v mc' (_ : eval_expr m l e mc = Some (v, mc'))
-    (_ : word.unsigned v = 0)
-    (_ : post t m l (addMetricInstructions 1
-                    (addMetricLoads 1
-                    (addMetricJumps 1 mc'))))
-    : exec (cmd.while e c) t m l mc post
-  | while_true e c
-      t m l mc post
-      v mc' (_ : eval_expr m l e mc = Some (v, mc'))
-      (_ : word.unsigned v <> 0)
-      mid (_ : exec c t m l mc' mid)
-      (_ : forall t' m' l' mc'', mid t' m' l' mc'' ->
-                                 exec (cmd.while e c) t' m' l' (addMetricInstructions 2
-                                                               (addMetricLoads 2
-                                                               (addMetricJumps 1 mc''))) post)
-    : exec (cmd.while e c) t m l mc post
-  | call binds fname arges
-      t m l mc post
-      params rets fbody (_ : map.get e fname = Some (params, rets, fbody))
-      args mc' (_ : evaluate_call_args_log m l arges mc = Some (args, mc'))
-      lf (_ : map.of_list_zip params args = Some lf)
-      mid (_ : exec fbody t m lf (addMetricInstructions 100 (addMetricJumps 100 (addMetricLoads 100 (addMetricStores 100 mc')))) mid)
-      (_ : forall t' m' st1 mc'', mid t' m' st1 mc'' ->
+              post t' mSmall' l')) ->
+      exec (cmd.stackalloc x n body) t mSmall l post
+  | if_true: forall t m l e c1 c2 post v,
+      eval_expr m l e = Some v ->
+      word.unsigned v <> 0 ->
+      exec c1 t m l post ->
+      exec (cmd.cond e c1 c2) t m l post
+  | if_false: forall e c1 c2 t m l post v,
+      eval_expr m l e = Some v ->
+      word.unsigned v = 0 ->
+      exec c2 t m l post ->
+      exec (cmd.cond e c1 c2) t m l post
+  | seq: forall c1 c2 t m l post mid,
+      exec c1 t m l mid ->
+      (forall t' m' l', mid t' m' l' -> exec c2 t' m' l' post) ->
+      exec (cmd.seq c1 c2) t m l post
+  | while_false: forall e c t m l post v,
+      eval_expr m l e = Some v ->
+      word.unsigned v = 0 ->
+      post t m l ->
+      exec (cmd.while e c) t m l post
+  | while_true: forall e c t m l post v mid,
+      eval_expr m l e = Some v ->
+      word.unsigned v <> 0 ->
+      exec c t m l mid ->
+      (forall t' m' l', mid t' m' l' -> exec (cmd.while e c) t' m' l' post) ->
+      exec (cmd.while e c) t m l post
+  | call: forall binds fname arges t m l post params rets fbody args lf mid,
+      map.get e fname = Some (params, rets, fbody) ->
+      eval_call_args m l arges = Some args ->
+      map.of_list_zip params args = Some lf ->
+      exec fbody t m lf mid ->
+      (forall t' m' st1, mid t' m' st1 ->
           exists retvs, map.getmany_of_list st1 rets = Some retvs /\
           exists l', map.putmany_of_list_zip binds retvs l = Some l' /\
-          post t' m' l'  (addMetricInstructions 100 (addMetricJumps 100 (addMetricLoads 100 (addMetricStores 100 mc'')))))
-    : exec (cmd.call binds fname arges) t m l mc post
-  | interact binds action arges
-      t m l mc post
-      mKeep mGive (_: map.split m mKeep mGive)
-      args mc' (_ :  evaluate_call_args_log m l arges mc = Some (args, mc'))
-      mid (_ : ext_spec t mGive action args mid)
-      (_ : forall mReceive resvals, mid mReceive resvals ->
+          post t' m' l') ->
+      exec (cmd.call binds fname arges) t m l post
+  | interact: forall binds action arges args t m l post mKeep mGive mid,
+      map.split m mKeep mGive ->
+      eval_call_args m l arges = Some args ->
+      ext_spec t mGive action args mid ->
+      (forall mReceive resvals, mid mReceive resvals ->
           exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
           forall m', map.split m' mKeep mReceive ->
-          post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l'
-            (addMetricInstructions 1
-            (addMetricStores 1
-            (addMetricLoads 2 mc'))))
-    : exec (cmd.interact binds action arges) t m l mc post
-  .
+          post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
+      exec (cmd.interact binds action arges) t m l post.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {ext_spec_ok: ext_spec.ok ext_spec}.
 
-  Lemma weaken: forall t l m mc s post1,
-      exec s t m l mc post1 ->
-      forall post2: _ -> _ -> _ -> _ -> Prop,
-        (forall t' m' l' mc', post1 t' m' l' mc' -> post2 t' m' l' mc') ->
-        exec s t m l mc post2.
+  Lemma weaken: forall t l m s post1,
+      exec s t m l post1 ->
+      forall post2,
+        (forall t' m' l', post1 t' m' l' -> post2 t' m' l') ->
+        exec s t m l post2.
   Proof.
     induction 1; intros; try solve [econstructor; eauto].
     - eapply stackalloc. 1: assumption.
@@ -295,16 +229,16 @@ Module exec. Section WithEnv.
       eauto 10.
   Qed.
 
-  Lemma intersect: forall t l m mc s post1,
-      exec s t m l mc post1 ->
+  Lemma intersect: forall t l m s post1,
+      exec s t m l post1 ->
       forall post2,
-        exec s t m l mc post2 ->
-        exec s t m l mc (fun t' m' l' mc' => post1 t' m' l' mc' /\ post2 t' m' l' mc').
+        exec s t m l post2 ->
+        exec s t m l (fun t' m' l' => post1 t' m' l' /\ post2 t' m' l').
   Proof.
     induction 1;
       intros;
       match goal with
-      | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H
+      | H: exec _ _ _ _ _ |- _ => inversion H; subst; clear H
       end;
       try match goal with
       | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ =>
@@ -314,9 +248,8 @@ Module exec. Section WithEnv.
           clear x2 y2 z2 H2
       end;
       repeat match goal with
-             | H1: ?e = Some (?v1, ?mc1), H2: ?e = Some (?v2, ?mc2) |- _ =>
-               replace v2 with v1 in * by congruence;
-               replace mc2 with mc1 in * by congruence; clear H2
+             | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+               replace v2 with v1 in * by congruence; clear H2
              end;
       repeat match goal with
              | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
@@ -326,7 +259,7 @@ Module exec. Section WithEnv.
 
     - econstructor. 1: eassumption.
       intros.
-      rename H0 into Ex1, H12 into Ex2.
+      rename H0 into Ex1, H11 into Ex2.
       eapply weaken. 1: eapply H1. 1,2: eassumption.
       1: eapply Ex2. 1,2: eassumption.
       cbv beta.
@@ -344,23 +277,23 @@ Module exec. Section WithEnv.
       + eapply IHexec. exact H9. (* not H1 *)
       + simpl. intros *. intros [? ?]. eauto.
     - eapply call. 1, 2, 3: eassumption.
-      + eapply IHexec. exact H16. (* not H2 *)
+      + eapply IHexec. exact H15. (* not H2 *)
       + simpl. intros *. intros [? ?].
         edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
-        edestruct H17 as (? & ? & ? & ? & ?); [eassumption|].
+        edestruct H16 as (? & ? & ? & ? & ?); [eassumption|].
         repeat match goal with
                | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
                  replace v2 with v1 in * by congruence; clear H2
                end.
         eauto 10.
     - pose proof ext_spec.unique_mGive_footprint as P.
-      specialize P with (1 := H1) (2 := H14).
+      specialize P with (1 := H1) (2 := H13).
       destruct (map.split_diff P H H7). subst mKeep0 mGive0. clear H7.
       eapply interact. 1,2: eassumption.
-      + eapply ext_spec.intersect; [ exact H1 | exact H14 ].
+      + eapply ext_spec.intersect; [ exact H1 | exact H13 ].
       + simpl. intros *. intros [? ?].
         edestruct H2 as (? & ? & ?); [eassumption|].
-        edestruct H15 as (? & ? & ?); [eassumption|].
+        edestruct H14 as (? & ? & ?); [eassumption|].
         repeat match goal with
                | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
                  replace v2 with v1 in * by congruence; clear H2
@@ -369,4 +302,52 @@ Module exec. Section WithEnv.
   Qed.
 
   End WithEnv.
+
+  Lemma extend_env: forall e1 e2,
+      map.extends e2 e1 ->
+      forall c t m l post,
+      exec e1 c t m l post ->
+      exec e2 c t m l post.
+  Proof. induction 2; try solve [econstructor; eauto]. Qed.
+
+  End WithParams.
 End exec. Notation exec := exec.exec.
+
+Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec}.
+
+  Implicit Types (l: locals) (m: mem) (post: trace -> mem -> list word -> Prop).
+
+  Definition call e fname t m args post :=
+    exists argnames retnames body,
+      map.get e fname = Some (argnames, retnames, body) /\
+      exists l, map.of_list_zip argnames args = Some l /\
+        exec e body t m l (fun t' m' l' => exists rets,
+          map.getmany_of_list l' retnames = Some rets /\ post t' m' rets).
+
+  Lemma weaken_call: forall e fname t m args post1,
+      call e fname t m args post1 ->
+      forall post2, (forall t' m' rets, post1 t' m' rets -> post2 t' m' rets) ->
+      call e fname t m args post2.
+  Proof.
+    unfold call. intros. fwd.
+    do 4 eexists. 1: eassumption.
+    do 2 eexists. 1: eassumption.
+    eapply exec.weaken. 1: eassumption.
+    cbv beta. clear -H0. intros. fwd. eauto.
+  Qed.
+
+  Lemma extend_env_call: forall e1 e2,
+      map.extends e2 e1 ->
+      forall f t m rets post,
+      call e1 f t m rets post ->
+      call e2 f t m rets post.
+  Proof.
+    unfold call. intros. fwd. repeat eexists.
+    - eapply H. eassumption.
+    - eassumption.
+    - eapply exec.extend_env; eassumption.
+  Qed.
+End WithParams.
diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index ce45aa805..af40307cd 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -5,7 +5,6 @@ Require Import coqutil.dlet bedrock2.Syntax bedrock2.Semantics.
 Section WeakestPrecondition.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
   Implicit Types (t : trace) (m : mem) (l : locals).
 
@@ -56,9 +55,12 @@ Section WeakestPrecondition.
   End WithF.
 
   Section WithFunctions.
-    Context (call : String.string -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
+    Context (e: env).
     Definition dexpr m l e v := expr m l e (eq v).
     Definition dexprs m l es vs := list_map (expr m l) es (eq vs).
+    (* All cases except cmd.while and cmd.call can be denoted by structural recursion
+       over the syntax.
+       For cmd.while and cmd.call, we fall back to the operational semantics *)
     Definition cmd_body (rec:_->_->_->_->_->Prop) (c : cmd) (t : trace) (m : mem) (l : locals)
              (post : trace -> mem -> locals -> Prop) : Prop :=
       (* give value of each pure expression when stating its subproof *)
@@ -91,18 +93,10 @@ Section WeakestPrecondition.
         (word.unsigned v = 0%Z -> rec cf t m l post)
       | cmd.seq c1 c2 =>
         rec c1 t m l (fun t m l => rec c2 t m l post)
-      | cmd.while e c =>
-        exists measure (lt:measure->measure->Prop) (inv:measure->trace->mem->locals->Prop),
-        Coq.Init.Wf.well_founded lt /\
-        (exists v, inv v t m l) /\
-        (forall v t m l, inv v t m l ->
-          exists b, dexpr m l e b /\
-          (word.unsigned b <> 0%Z -> rec c t m l (fun t' m l =>
-            exists v', inv v' t' m l /\ lt v' v)) /\
-          (word.unsigned b = 0%Z -> post t m l))
+      | cmd.while _ _ => Semantics.exec e c t m l post
       | cmd.call binds fname arges =>
         exists args, dexprs m l arges args /\
-        call fname t m args (fun t m rets =>
+        Semantics.call e fname t m args (fun t m rets =>
           exists l', map.putmany_of_list_zip binds rets l = Some l' /\
           post t m l')
       | cmd.interact binds action arges =>
@@ -122,20 +116,9 @@ Section WeakestPrecondition.
         list_map (get l) outnames (fun rets =>
         post t m rets)).
 
-  Definition call_body rec (functions : list (String.string * (list String.string * list String.string * cmd.cmd)))
-                (fname : String.string) (t : trace) (m : mem) (args : list word)
-                (post : trace -> mem -> list word -> Prop) : Prop :=
-    match functions with
-    | nil => False
-    | cons (f, decl) functions =>
-      if String.eqb f fname
-      then func (rec functions) decl t m args post
-      else rec functions fname t m args post
-    end.
-  Fixpoint call functions := call_body call functions.
-
-  Definition program funcs main t m l post : Prop := cmd (call funcs) main t m l post.
+  Definition program := cmd.
 End WeakestPrecondition.
+Notation call := Semantics.call (only parsing).
 
 Ltac unfold1_cmd e :=
   lazymatch e with
@@ -171,18 +154,6 @@ Ltac unfold1_list_map_goal :=
   let G := unfold1_list_map G in
   change G.
 
-Ltac unfold1_call e :=
-  lazymatch e with
-    @call ?width ?BW ?word ?mem ?locals ?ext_spec ?fs ?fname ?t ?m ?l ?post =>
-    let fs := eval hnf in fs in
-    constr:(@call_body width BW word mem locals ext_spec
-                       (@call width BW word mem locals ext_spec) fs fname t m l post)
-  end.
-Ltac unfold1_call_goal :=
-  let G := lazymatch goal with |- ?G => G end in
-  let G := unfold1_call G in
-  change G.
-
 Import Coq.ZArith.ZArith.
 
 Notation "'fnspec!' name a0 .. an '/' g0 .. gn '~>' r0 .. rn ',' '{' 'requires' tr mem := pre ';' 'ensures' tr' mem' ':=' post '}'" :=
diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
index bb0a69516..d8a36d614 100644
--- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
@@ -7,7 +7,6 @@ Require Import Coq.Classes.Morphisms.
 Section WeakestPrecondition.
   Context {width} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: Semantics.ExtSpec}.
 
   Ltac ind_on X :=
@@ -23,7 +22,6 @@ Section WeakestPrecondition.
        we'd get a typechecking failure at Qed time. *)
     repeat match goal with x : ?T |- _ => first
        [ constr_eq T X; move x before ext_spec
-       | constr_eq T X; move x before env
        | constr_eq T X; move x before locals
        | constr_eq T X; move x at top
        | revert x ] end;
@@ -69,19 +67,19 @@ Section WeakestPrecondition.
 
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Global Instance Proper_cmd :
     Proper (
-     (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ (pointwise_relation _ Basics.impl))) ==> Basics.impl)))) ==>
+     (pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
-     Basics.impl)))))) WeakestPrecondition.cmd.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+     Basics.impl))))))) WeakestPrecondition.cmd.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
+    pose proof I. (* to keep naming *)
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl]; ind_on Syntax.cmd.cmd;
       cbn in *; cbv [dlet.dlet] in *; intuition (try typeclasses eauto with core).
     { destruct H1 as (?&?&?). eexists. split.
@@ -97,32 +95,18 @@ Section WeakestPrecondition.
           { cbv [pointwise_relation Basics.impl]; intuition eauto 2. }
           { eauto. } }
         { eapply Proper_store; eauto; cbv [pointwise_relation Basics.impl]; eauto. } } }
-    { eapply H1; [ | | eapply H3; eassumption ].
-      2 : intros ? ? ? (?&?&?&?&?). all : eauto 7. }
+    { eapply H1. 2: eapply H3; eassumption.
+      intros ? ? ? (?&?&?&?&?). eauto 7. }
     { destruct H1 as (?&?&?). eexists. split.
       { eapply Proper_expr.
         { cbv [pointwise_relation Basics.impl]; intuition eauto 2. }
         { eauto. } }
       { intuition eauto 6. } }
-    { destruct H1 as (?&?&?&?&?&HH).
-      eassumption || eexists.
-      eassumption || eexists.
-      eassumption || eexists.
-      eassumption || eexists. { eassumption || eexists. }
-      eassumption || eexists. { eassumption || eexists. }
-      intros X Y Z T W.
-      specialize (HH X Y Z T W).
-      destruct HH as (?&?&?). eexists. split.
-      1: eapply Proper_expr.
-      1: cbv [pointwise_relation Basics.impl].
-      all:intuition eauto 2.
-      - eapply H2; eauto; cbn; intros.
-        match goal with H:_ |- _ => destruct H as (?&?&?); solve[eauto] end.
-      - intuition eauto. }
+    { eapply Semantics.exec.weaken; eassumption. }
     { destruct H1 as (?&?&?). eexists. split.
       { eapply Proper_list_map; eauto; try exact H4; cbv [respectful pointwise_relation Basics.impl]; intuition eauto 2.
         eapply Proper_expr; eauto. }
-      { eapply H. 2: eauto.
+      { eapply Semantics.weaken_call. 1: eassumption. cbv beta.
         (* COQBUG (performance), measured in Coq 8.9:
            "firstorder eauto" works, but takes ~100s and increases memory usage by 1.8GB.
            On the other hand, the line below takes just 5ms *)
@@ -138,35 +122,6 @@ Section WeakestPrecondition.
         intros ? ? (?&?&?); eauto 10. } }
   Qed.
 
-  Global Instance Proper_func :
-    Proper (
-     (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ (pointwise_relation _ Basics.impl))) ==> Basics.impl)))) ==>
-     pointwise_relation _ (
-     pointwise_relation _ (
-     pointwise_relation _ (
-     pointwise_relation _ (
-     (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
-     Basics.impl)))))) WeakestPrecondition.func.
-  Proof using word_ok mem_ok locals_ok ext_spec_ok env_ok.
-    cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func]; intros.
-    destruct a. destruct p.
-    destruct H1; intuition idtac.
-    eexists.
-    split; [eauto|].
-    eapply Proper_cmd;
-      cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
-      try solve [typeclasses eauto with core].
-    intros.
-    eapply Proper_list_map;
-      cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
-      try solve [typeclasses eauto with core].
-    - intros.
-      eapply Proper_get;
-        cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
-        eauto.
-    - eauto.
-  Qed.
-
   Global Instance Proper_call :
     Proper (
      (pointwise_relation _ (
@@ -176,14 +131,9 @@ Section WeakestPrecondition.
      pointwise_relation _ (
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
      Basics.impl)))))))) WeakestPrecondition.call.
-  Proof using word_ok mem_ok locals_ok ext_spec_ok env_ok.
-    cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list (String.string * (list String.string * list String.string * Syntax.cmd.cmd)));
-      cbn in *; intuition (try typeclasses eauto with core).
-    destruct a.
-    destruct (String.eqb s a1); eauto.
-    eapply Proper_func;
-      cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
-      eauto.
+  Proof using word_ok mem_ok locals_ok ext_spec_ok.
+    cbv [Proper respectful pointwise_relation Basics.impl].
+    intros. eapply Semantics.weaken_call; eassumption.
   Qed.
 
   Global Instance Proper_program :
@@ -195,15 +145,11 @@ Section WeakestPrecondition.
      pointwise_relation _ (
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
      Basics.impl)))))) WeakestPrecondition.program.
-  Proof using word_ok mem_ok locals_ok ext_spec_ok env_ok.
+  Proof using word_ok mem_ok locals_ok ext_spec_ok.
     cbv [Proper respectful pointwise_relation Basics.impl  WeakestPrecondition.program]; intros.
     eapply Proper_cmd;
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
     try solve [typeclasses eauto with core].
-    intros.
-    eapply Proper_call;
-    cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
-    solve [typeclasses eauto with core].
   Qed.
 
   Ltac t :=
@@ -217,11 +163,10 @@ Section WeakestPrecondition.
              | _ => progress cbv [dlet.dlet WeakestPrecondition.dexpr WeakestPrecondition.dexprs WeakestPrecondition.store] in *
              end; eauto.
 
-  Lemma expr_sound: forall m l e mc post (H : WeakestPrecondition.expr m l e post),
-    exists v mc', Semantics.eval_expr m l e mc = Some (v, mc') /\ post v.
+  Lemma expr_sound: forall m l e post (H : WeakestPrecondition.expr m l e post),
+    exists v, Semantics.eval_expr m l e = Some v /\ post v.
   Proof using word_ok.
     induction e; t.
-    { destruct H. destruct H. eexists. eexists. rewrite H. eauto. }
     { eapply IHe in H; t. cbv [WeakestPrecondition.load] in H0; t. rewrite H. rewrite H0. eauto. }
     { eapply IHe in H; t. cbv [WeakestPrecondition.load] in H0; t. rewrite H. rewrite H0. eauto. }
     { eapply IHe1 in H; t. eapply IHe2 in H0; t. rewrite H, H0; eauto. }
@@ -232,48 +177,43 @@ Section WeakestPrecondition.
 
   Import ZArith coqutil.Tactics.Tactics.
 
-  Lemma expr_complete: forall m l e mc v mc',
-    Semantics.eval_expr m l e mc = Some (v, mc') ->
+  Lemma expr_complete: forall m l e v,
+    Semantics.eval_expr m l e = Some v ->
     WeakestPrecondition.dexpr m l e v.
   Proof using word_ok.
     induction e; cbn; intros.
     - inversion_clear H. reflexivity.
-    - destruct_one_match_hyp. 2: discriminate. inversion H. subst r.
-      eexists. eauto.
+    - eexists. eauto.
     - repeat (destruct_one_match_hyp; try discriminate; []).
-      inversion H. subst r0 mc'. clear H.
       eapply Proper_expr.
-      2: { eapply IHe. eassumption. }
+      2: { eapply IHe. reflexivity. }
       intros addr ?. subst r. unfold WeakestPrecondition.load. eauto.
     - repeat (destruct_one_match_hyp; try discriminate; []).
-      inversion H. subst r0 mc'. clear H.
       eapply Proper_expr.
-      2: { eapply IHe. eassumption. }
+      2: { eapply IHe. reflexivity. }
       intros addr ?. subst r. unfold WeakestPrecondition.load. eauto.
     - repeat (destruct_one_match_hyp; try discriminate; []).
-      inversion H. subst v mc'. clear H.
       eapply Proper_expr.
-      2: { eapply IHe1. eassumption. }
+      2: { eapply IHe1. reflexivity. }
       intros v1 ?. subst r.
       eapply Proper_expr.
-      2: { eapply IHe2. eassumption. }
+      2: { eapply IHe2. reflexivity. }
       intros v2 ?. subst r0.
-      reflexivity.
+      congruence.
     - repeat (destruct_one_match_hyp; try discriminate; []).
       eapply Proper_expr.
-      2: { eapply IHe1. eassumption. }
+      2: { eapply IHe1. reflexivity. }
       intros vc ?. subst r.
       destr (word.eqb vc (word.of_Z 0)).
       + eapply IHe3. eassumption.
       + eapply IHe2. eassumption.
   Qed.
 
-  Lemma sound_args : forall m l args mc P,
+  Lemma sound_args : forall m l args P,
       WeakestPrecondition.list_map (WeakestPrecondition.expr m l) args P ->
-      exists x mc', Semantics.evaluate_call_args_log m l args mc = Some (x, mc') /\ P x.
+      exists x, Semantics.eval_call_args m l args = Some x /\ P x.
   Proof using word_ok.
     induction args; cbn; repeat (subst; t).
-    unfold Semantics.eval_expr in *.
     eapply expr_sound in H; t; rewrite H.
     eapply IHargs in H0; t; rewrite H0.
     eauto.
@@ -293,76 +233,96 @@ Section WeakestPrecondition.
     all : cbv [respectful pointwise_relation Basics.impl WeakestPrecondition.get]; intros; cbv beta; t.
   Qed.
 
-  Local Notation semantics_call := (fun e n t m args post =>
-    exists params rets fbody, map.get e n = Some (params, rets, fbody) /\
-    exists lf, map.putmany_of_list_zip params args map.empty = Some lf /\
-    forall mc', Semantics.exec e fbody t m lf mc' (fun t' m' st1 mc'' =>
-      exists retvs, map.getmany_of_list st1 rets = Some retvs /\
-      post t' m' retvs)).
-
   Local Hint Constructors Semantics.exec : core.
-  Lemma sound_cmd' e c t m l mc post
-        (H:WeakestPrecondition.cmd (semantics_call e) c t m l post)
-    : Semantics.exec e c t m l mc (fun t' m' l' mc' => post t' m' l').
+  Lemma sound_cmd e c t m l post (H: WeakestPrecondition.cmd e c t m l post)
+    : Semantics.exec e c t m l post.
   Proof.
     ind_on Syntax.cmd; repeat (t; try match reverse goal with H : WeakestPrecondition.expr _ _ _ _ |- _ => eapply expr_sound in H end).
     { destruct (BinInt.Z.eq_dec (Interface.word.unsigned x) (BinNums.Z0)) as [Hb|Hb]; cycle 1.
       { econstructor; t. }
       { eapply Semantics.exec.if_false; t. } }
-    { revert dependent l; revert dependent m; revert dependent t; revert dependent mc; pattern x2.
-      eapply (well_founded_ind H); t.
-      pose proof (H1 _ _ _ _ ltac:(eassumption));
-        repeat (t; try match goal with H : WeakestPrecondition.expr _ _ _ _ |- _ => eapply expr_sound in H end).
-      { destruct (BinInt.Z.eq_dec (Interface.word.unsigned x4) (BinNums.Z0)) as [Hb|Hb].
-        { eapply Semantics.exec.while_false; t. }
-        { eapply Semantics.exec.while_true; t. t. } } }
-    { eapply sound_args in H; t. }
+    { inversion H0. t. eapply sound_args in H; t. }
     { eapply sound_args in H; t. }
   Qed.
 
+  Lemma weaken_cmd: forall e c t m l (post1 post2: _->_->_->Prop),
+      WeakestPrecondition.cmd e c t m l post1 ->
+      (forall t m l, post1 t m l -> post2 t m l) ->
+      WeakestPrecondition.cmd e c t m l post2.
+  Proof.
+    intros.
+    eapply Proper_cmd. 2: eassumption.
+    cbv [RelationClasses.Reflexive Morphisms.pointwise_relation
+         Morphisms.respectful Basics.impl].
+    assumption.
+  Qed.
 
-  Section WithE.
-    Context fs (E: env) (HE: List.Forall (fun '(k, v) => map.get E k = Some v) fs).
-    Import coqutil.Tactics.Tactics.
-    Lemma sound_call' n t m args post
-      (H : WeakestPrecondition.call fs n t m args post)
-      : semantics_call E n t m args post.
-    Proof.
-      revert H; revert post args m t n; induction HE; intros.
-      { contradiction H. }
-      destruct x as [n' ((X&Y)&Z)]; t.
-      destr (String.eqb n' n); t.
-      eexists X, Y, Z; split; [assumption|].
-      eexists; eauto.
-      eexists; eauto.
-      intros.
-      eapply sound_cmd'.
-      eapply Proper_cmd; try eapply H0.
-      all : cbv [respectful pointwise_relation Basics.impl]; intros; cbv beta.
-      1: eapply IHf, Proper_call; eauto.
-      2: eassumption.
-      eauto using sound_getmany.
-    Qed.
+  Lemma complete_args : forall m l args vs,
+      Semantics.eval_call_args m l args = Some vs ->
+      WeakestPrecondition.dexprs m l args vs.
+  Proof using word_ok.
+    induction args; cbn; repeat (subst; t).
+    1: inversion H; reflexivity.
+    destruct_one_match_hyp. 2: discriminate.
+    destruct_one_match_hyp. 2: discriminate.
+    inversion H. subst vs. clear H.
+    eapply Proper_expr. 2: eapply expr_complete. 2: eassumption.
+    intros x ?. subst x.
+    eapply Proper_list_map. 3: eapply IHargs; reflexivity.
+    { eapply Proper_expr. }
+    { intros ? ?. subst. reflexivity. }
+  Qed.
 
-    Lemma sound_cmd'' c t m l mc post
-      (H : WeakestPrecondition.cmd (WeakestPrecondition.call fs) c t m l post)
-      : Semantics.exec E c t m l mc (fun t' m' l' mc' => post t' m' l').
-    Proof.
-      eapply Proper_cmd in H; [ .. | reflexivity ].
-      1: apply sound_cmd'; exact H.
-      cbv [respectful pointwise_relation Basics.impl]; intros; cbv beta.
-      eapply sound_call', Proper_call, H1.
-      cbv [respectful pointwise_relation Basics.impl]; eauto.
-    Qed.
-  End WithE.
+  Lemma complete_cmd: forall e c t m l post,
+      Semantics.exec e c t m l post ->
+      WeakestPrecondition.cmd e c t m l post.
+  Proof.
+    induction 1.
+    { eassumption. }
+    { eapply expr_complete in H. eexists. split. 1: exact H.
+      eassumption. }
+    { eauto. }
+    { eapply expr_complete in H.
+      eapply expr_complete in H0.
+      eexists. split. 1: eassumption.
+      eexists. split. 1: eassumption.
+      eexists. eauto. }
+    { split. 1: assumption.
+      intros * HA HSp. specialize H1 with (1 := HA) (2 := HSp).
+      unfold dlet.dlet. eapply weaken_cmd. 1: eapply H1. cbv beta.
+      clear. intros * (? & ? & ? & ? & ?). eauto 8. }
+    { eexists. ssplit; intros; eauto using expr_complete; congruence. }
+    { eexists. ssplit; intros; eauto using expr_complete; congruence. }
+    { cbn. eapply weaken_cmd.
+      { eapply IHexec. }
+      cbv beta. intros.
+      eapply H1. eassumption. }
+    { cbn. eapply Semantics.exec.while_false; eauto. }
+    { rename IHexec into IH1, H3 into IH2.
+      cbn. eapply Semantics.exec.while_true; eassumption. }
+    { cbn. eexists. split.
+      { eapply complete_args. eassumption. }
+      unfold Semantics.call. do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
+      eapply Semantics.exec.weaken.
+      { eassumption. }
+      cbv beta. intros.
+      specialize H3 with (1 := H4). destruct H3 as (retvs & G & ? & ? & ?). eauto 8. }
+    { cbn. eexists. split.
+      { eapply complete_args. eassumption. }
+      eexists _, _. split. 1: eassumption.
+      eapply Semantics.ext_spec.weaken. 2: eassumption.
+      intros m0 args0 Hmid. specialize H2 with (1 := Hmid). destruct H2 as (? & ? & ?).
+      eauto 8. }
+  Qed.
 
-  Lemma sound_cmd fs c t m l mc post
-    (Hnd : List.NoDup (List.map fst fs))
-    (H : WeakestPrecondition.cmd (WeakestPrecondition.call fs) c t m l post)
-    : Semantics.exec (map.of_list fs) c t m l mc (fun t' m' l' mc' => post t' m' l').
+  Lemma start_func: forall e fname fimpl t m args post,
+      map.get e fname = Some fimpl ->
+      WeakestPrecondition.func e fimpl t m args post ->
+      WeakestPrecondition.call e fname t m args post.
   Proof.
-    eapply sound_cmd'';
-      try eapply Properties.map.all_gets_from_map_of_NoDup_list; eauto.
+    intros * G. destruct fimpl as [[argnames retnames] body]. intros (? & ? & ?).
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption. eapply sound_cmd.
+    eapply weaken_cmd. 1: eassumption. cbv beta. intros. eapply sound_getmany. assumption.
   Qed.
 
   (** Ad-hoc lemmas here? *)
diff --git a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
index 008081c0a..d4f52115a 100644
--- a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
+++ b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
@@ -11,6 +11,7 @@ Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope Z_s
 
 From bedrock2 Require Import Array Scalars Separation.
 From coqutil.Tactics Require Import letexists rdelta.
+Require Import bedrock2.WeakestPrecondition.
 Local Notation bytes := (array scalar8 (word.of_Z 1)).
 
 Ltac seplog_use_array_load1 H i :=
@@ -20,17 +21,16 @@ Ltac seplog_use_array_load1 H i :=
   change ((word.unsigned (word.of_Z 1) * Z.of_nat iNat)%Z) with i in *.
 
 
-Local Instance spec_of_arp : spec_of "arp" := fun functions =>
-  forall t m packet ethbuf len R,
-    (sep (array scalar8 (word.of_Z 1) ethbuf packet) R) m ->
-    word.unsigned len = Z.of_nat (length packet) ->
-  WeakestPrecondition.call functions "arp" t m [ethbuf; len] (fun T M rets => True).
+Local Instance spec_of_arp : spec_of "arp" :=
+  fnspec! "arp" ethbuf len / packet R,
+  { requires t m := (sep (array scalar8 (word.of_Z 1) ethbuf packet) R) m /\
+                    word.unsigned len = Z.of_nat (length packet);
+    ensures T M := True }.
 
 Local Hint Mode Word.Interface.word - : typeclass_instances.
 
 Goal program_logic_goal_for_function! arp.
-  eexists; split; repeat straightline.
-  1: exact eq_refl.
+  repeat straightline.
   letexists; split; [solve[repeat straightline]|]; split; [|solve[repeat straightline]]; repeat straightline.
   eapply Properties.word.if_nonzero in H1.
   rewrite word.unsigned_ltu, word.unsigned_of_Z in H1. cbv [word.wrap] in H1.
diff --git a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
index d5ad2241c..08033dc22 100644
--- a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
+++ b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
@@ -50,6 +50,32 @@ Definition uart0_rxdata := 0x10013004. Definition uart0_txdata  := 0x10013000.
       False
     end%list%bool.
 
+Ltac u :=
+  repeat match goal with
+    | H: exists _, _ |- _ => destruct H
+    | H: _ /\ _ |- _ => destruct H
+    | H: False |- _ => destruct H
+    end.
+
+#[global] Instance ext_spec_ok : ext_spec.ok ext_spec.
+Proof.
+  split; cbv [ext_spec Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl]; intros.
+    all : repeat u; subst; eauto 8 using Properties.map.same_domain_refl.
+    { destr.destr (String.eqb act "MMInput");
+      try destr.destr (String.eqb act "MMOutput").
+      3: {
+        exfalso.
+        repeat (Tactics.destruct_one_match_hyp; try (assumption || congruence)). }
+      { repeat ((Tactics.destruct_one_match_hyp; repeat u; eauto)). }
+      { repeat ((Tactics.destruct_one_match_hyp; repeat u; eauto)). } }
+    { destr.destr (String.eqb a "MMInput");
+      try destr.destr (String.eqb a "MMOutput").
+      3: {
+        exfalso.
+        repeat (Tactics.destruct_one_match_hyp; try (assumption || congruence)). }
+      { repeat ((Tactics.destruct_one_match_hyp; repeat u; eauto)). }
+      { repeat ((Tactics.destruct_one_match_hyp; repeat u; eauto)). } }
+Qed.
 
 Require Import bedrock2.NotationsCustomEntry.
 
@@ -157,13 +183,18 @@ Local Instance mapok: map.ok mem := SortedListWord.ok Naive.word32 _.
 
 Local Instance wordok: word.ok word := Naive.word32_ok.
 
+Local Instance localsok: map.ok locals := SortedListString.ok _.
+
 Lemma swap_chars_over_uart_correct m :
-  WeakestPrecondition.cmd (fun _ _ _ _ _ => False) swap_chars_over_uart nil m map.empty
+  WeakestPrecondition.cmd map.empty swap_chars_over_uart nil m map.empty
   (fun t m l => True).
 Proof.
   repeat t.
+  eapply Loops.wp_while.
   eexists _, _, (fun v t _ l => exists p, map.of_list_zip ["running"; "prev"; "one"; "dot"]%string [v; p; word.of_Z(1); word.of_Z(46)] = Some l ); repeat t.
+  eapply Loops.wp_while.
   eexists _, _, (fun v t _ l => exists rxv, map.putmany_of_list_zip ["polling"; "rx"]%string [v; rxv] l0 = Some l); repeat t.
+  eapply Loops.wp_while.
   eexists _, _, (fun v t _ l => exists txv, map.putmany_of_list_zip ["polling"; "tx"]%string [v; txv] l0 = Some l); repeat t.
   eexists; split; repeat t.
 Defined.
@@ -242,12 +273,14 @@ Definition echo_server: cmd :=
   ).
 
 Lemma echo_server_correct m :
-  WeakestPrecondition.cmd (fun _ _ _ _ _ => False) echo_server nil m map.empty
+  WeakestPrecondition.cmd map.empty echo_server nil m map.empty
   (fun t m l => echo_server_spec t None).
 Proof.
   repeat t.
+  eapply Loops.wp_while.
   eexists _, _, (fun v t _ l => map.of_list_zip ["running"; "one"]%string [v; word.of_Z(1)] = Some l /\ echo_server_spec t None ); repeat t.
   { repeat split. admit. (* hfrosccfg*) }
+  eapply Loops.wp_while.
   eexists _, _, (fun v t _ l => exists rxv, map.putmany_of_list_zip ["polling"; "rx"]%string [v; rxv] l0 = Some l /\
                                             if Z.eq_dec (word.unsigned (word.and rxv (word.of_Z (2^31)))) 0
                                             then echo_server_spec t (Some rxv)
diff --git a/bedrock2/src/bedrock2Examples/LAN9250.v b/bedrock2/src/bedrock2Examples/LAN9250.v
index aa52b4f31..75a7852f3 100644
--- a/bedrock2/src/bedrock2Examples/LAN9250.v
+++ b/bedrock2/src/bedrock2Examples/LAN9250.v
@@ -781,6 +781,15 @@ Section WithParameters.
 
   Import symmetry autoforward.
 
+  Local Ltac no_call :=
+    lazymatch goal with
+    | |- Semantics.call _ _ _ _ _ _ => fail
+    | |- _ => idtac
+    end.
+
+  Local Ltac original_esplit := esplit.
+  Local Ltac esplit := no_call; original_esplit.
+
   Lemma lan9250_tx_ok : program_logic_goal_for_function! lan9250_tx.
   Proof.
 
diff --git a/bedrock2/src/bedrock2Examples/SPI.v b/bedrock2/src/bedrock2Examples/SPI.v
index d484dc554..e15ea518f 100644
--- a/bedrock2/src/bedrock2Examples/SPI.v
+++ b/bedrock2/src/bedrock2Examples/SPI.v
@@ -130,6 +130,17 @@ Section WithParameters.
       cbv [isMMIOAddr addr].
       ZnWords. }
     repeat straightline.
+    (* The hnf inside this letexists used to substitute
+
+         c := cmd.cond (expr.op bopname.sru "busy" 31) cmd.skip
+                (cmd.set "i" (expr.op bopname.xor "i" "i")) : cmd.cmd
+
+       and also unfolded WeakestPrecondition.cmd of c into
+
+         WeakestPrecondition.dexpr m l0 cond letboundEvar /\
+         ThenCorrectness /\
+         ElseCorrectness
+    *)
     letexists. split.
     { repeat straightline. }
     split; intros.
diff --git a/bedrock2/src/bedrock2Examples/Trace.v b/bedrock2/src/bedrock2Examples/Trace.v
index 39d44aa31..495cf29d5 100644
--- a/bedrock2/src/bedrock2Examples/Trace.v
+++ b/bedrock2/src/bedrock2Examples/Trace.v
@@ -6,7 +6,7 @@ Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Tactics.Tactics.
 Require Import Coq.Strings.String.
 Require Import bedrock2.TracePredicate. Import TracePredicateNotations.
-Require Import bedrock2.Semantics.
+Require Import bedrock2.Semantics bedrock2.MetricSemantics.
 Require Import bedrock2.Syntax.
 Require Import bedrock2.NotationsCustomEntry.
 
@@ -20,7 +20,6 @@ Module Import IOMacros.
     word :> Word.Interface.word width;
     mem :> map.map word Byte.byte;
     locals :> map.map String.string word;
-    env :> map.map String.string (list String.string * list String.string * cmd);
     ext_spec :> ExtSpec;
 
     (* macros to be inlined to read or write a word
@@ -139,7 +138,6 @@ Module SpiEth.
         write_byte b (((m, MMInput, [word.of_Z spi_tx_fifo]), (m, [x])) :: rest).
 
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Instance ext_spec: ExtSpec :=
       fun t mGive action (argvals: list word) (post: (mem -> list word -> Prop)) =>
@@ -238,7 +236,6 @@ Module Syscalls.
                        (m, [ret1; ret2; err]))].
 
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Instance ext_spec: ExtSpec :=
       fun t m action (argvals: list word) (post: (mem -> list word -> Prop)) =>
@@ -298,7 +295,6 @@ Module MMIOUsage.
     Context {word: word.word 32} {mem: map.map word Byte.byte} {mem_ok: map.ok mem}.
     Context {word_ok: word.ok word}.
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Definition squarer_correct := @squarer_correct SpiEth.MMIOMacros.
     (*Check squarer_correct.*)
@@ -311,7 +307,6 @@ Module SyscallsUsage.
     Context {word: word.word 32} {mem: map.map word Byte.byte} {mem_ok: map.ok mem}.
     Context {word_ok: word.ok word}.
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Definition squarer_correct := @squarer_correct Syscalls.SyscallIOMacros.
     (*Check squarer_correct.*)
diff --git a/bedrock2/src/bedrock2Examples/indirect_add.v b/bedrock2/src/bedrock2Examples/indirect_add.v
index e59ef10d0..d17ce9116 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add.v
@@ -50,7 +50,7 @@ Section WithParameters.
     cbv [f]. ecancel_assumption.
   Qed.
 
-  Example link_both : spec_of_indirect_add_twice (("indirect_add_twice",indirect_add_twice)::("indirect_add",indirect_add)::nil).
+  Example link_both : spec_of_indirect_add_twice (map.of_list  (("indirect_add_twice",indirect_add_twice)::("indirect_add",indirect_add)::nil)).
   Proof. auto using indirect_add_twice_ok, indirect_add_ok. Qed.
 
   (*
diff --git a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
index d6f8e2334..58f19e5e1 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
@@ -20,6 +20,7 @@ Require Import bedrock2.HeapletwiseHyps.
 Require Import bedrock2.enable_frame_trick.
 Require Import bedrock2.PurifySep.
 Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
+Require Import coqutil.Macros.WithBaseName.
 
 Require bedrock2.WeakestPreconditionProperties.
 From coqutil.Tactics Require Import letexists eabstract.
@@ -75,11 +76,12 @@ Section WithParameters.
     { cbv [f]. ecancel_assumption. }
   Qed.
 
-  Example link_both : spec_of_indirect_add_twice (("indirect_add_twice",indirect_add_twice)::("indirect_add",indirect_add)::nil).
+  Example link_both : spec_of_indirect_add_twice
+                        (map.of_list &[,indirect_add_twice; indirect_add]).
   Proof. auto using indirect_add_twice_ok, indirect_add_ok. Qed.
 
   (*
-  Require Import bedrock2.ToCString bedrock2.PrintString coqutil.Macros.WithBaseName.
+  Require Import bedrock2.ToCString bedrock2.PrintString.
   Goal True. print_string (c_module &[,indirect_add_twice; indirect_add]). Abort.
   *)
 
@@ -175,12 +177,12 @@ H15 : (scalar a0 (word.add va vb) ⋆ (scalar out vout ⋆ R))%sep a2
       (calleePre: Prop)
       (calleePost callerPost: trace -> mem -> list word -> Prop),
       (* definition-site format: *)
-      (calleePre -> call funs f t m args calleePost) ->
+      (calleePre -> WeakestPrecondition.call funs f t m args calleePost) ->
       (* use-site format: *)
       (calleePre /\ enable_frame_trick
                       (forall t' m' rets, calleePost t' m' rets -> callerPost t' m' rets)) ->
       (* conclusion: *)
-      call funs f t m args callerPost.
+      WeakestPrecondition.call funs f t m args callerPost.
   Proof.
     intros. destruct H0. eapply WeakestPreconditionProperties.Proper_call; eauto.
   Qed.
diff --git a/bedrock2/src/bedrock2Examples/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v
index 009a5f63f..de8b9f63c 100644
--- a/bedrock2/src/bedrock2Examples/lightbulb.v
+++ b/bedrock2/src/bedrock2Examples/lightbulb.v
@@ -610,24 +610,26 @@ Section WithParameters.
 
   Import SPI.
 
-  Definition function_impls :=
+  Definition function_impls := map.of_list
     &[,lightbulb_init; lan9250_init; lan9250_wait_for_boot; lan9250_mac_write;
     lightbulb_loop; lightbulb_handle; recvEthernet;  lan9250_writeword; lan9250_readword;
     spi_xchg; spi_write; spi_read].
 
+  Local Ltac specapply s := eapply s; [reflexivity|..].
+
   Lemma link_lightbulb_loop : spec_of_lightbulb_loop function_impls.
   Proof.
-    eapply lightbulb_loop_ok;
-    (eapply recvEthernet_ok || eapply lightbulb_handle_ok);
-        eapply lan9250_readword_ok; eapply spi_xchg_ok;
-        (eapply spi_write_ok || eapply spi_read_ok).
+    specapply lightbulb_loop_ok;
+    (specapply recvEthernet_ok || specapply lightbulb_handle_ok);
+        specapply lan9250_readword_ok; specapply spi_xchg_ok;
+        (specapply spi_write_ok || specapply spi_read_ok).
   Qed.
   Lemma link_lightbulb_init : spec_of_lightbulb_init function_impls.
   Proof.
-    eapply lightbulb_init_ok; eapply lan9250_init_ok;
-    try (eapply lan9250_wait_for_boot_ok || eapply lan9250_mac_write_ok);
-    (eapply lan9250_readword_ok || eapply lan9250_writeword_ok);
-        eapply spi_xchg_ok;
-        (eapply spi_write_ok || eapply spi_read_ok).
+    specapply lightbulb_init_ok; specapply lan9250_init_ok;
+    try (specapply lan9250_wait_for_boot_ok || specapply lan9250_mac_write_ok);
+    (specapply lan9250_readword_ok || specapply lan9250_writeword_ok);
+        specapply spi_xchg_ok;
+        (specapply spi_write_ok || specapply spi_read_ok).
   Qed.
 End WithParameters.
diff --git a/bedrock2/src/bedrock2Examples/memconst.v b/bedrock2/src/bedrock2Examples/memconst.v
index 81e246be4..4c2167540 100644
--- a/bedrock2/src/bedrock2Examples/memconst.v
+++ b/bedrock2/src/bedrock2Examples/memconst.v
@@ -33,20 +33,21 @@ Section WithParameters.
       ensures t' m := m =* bs$@p * R /\ t=t' }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
+  Local Ltac normalize_body_of_function f ::= f.
+
   Local Ltac ZnWords := destruct width_cases; bedrock2.ZnWords.ZnWords.
   Lemma memconst_ok ident bs functions :
-    spec_of_memconst ident bs ((ident, memconst bs) :: functions).
+    program_logic_goal_for
+      (memconst bs)
+      (map.get functions ident = Some (memconst bs) ->
+       spec_of_memconst ident bs functions).
   Proof.
     cbv [spec_of_memconst memconst]; repeat straightline.
-    unfold1_call_goal; cbv beta match delta [call_body]; rewrite String.eqb_refl.
-    cbv beta match delta [func].
-    repeat straightline.
     refine ((Loops.tailrec
       (HList.polymorphic_list.cons _
       (HList.polymorphic_list.cons _
diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
index c18867845..41629648b 100644
--- a/bedrock2/src/bedrock2Examples/memequal.v
+++ b/bedrock2/src/bedrock2Examples/memequal.v
@@ -38,7 +38,6 @@ Section WithParameters.
                        (r  = 1 :>Z <-> xs  = ys) }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
index 4aa826831..757139543 100644
--- a/bedrock2/src/bedrock2Examples/memmove.v
+++ b/bedrock2/src/bedrock2Examples/memmove.v
@@ -53,7 +53,6 @@ Section WithParameters.
 
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
@@ -385,6 +384,7 @@ Section WithParameters.
     cbv [program_logic_goal_for spec_of_memmove_array]; intros.
     eapply WeakestPreconditionProperties.Proper_call; cycle 1; [eapply memmove_ok|];
         cbv [sepclause_of_map] in *.
+    { eassumption. }
     { intuition idtac.
       - seprewrite_in_by @ptsto_bytes.array1_iff_eq_of_list_word_at H0 ZnWords; eassumption.
       - seprewrite_in_by @ptsto_bytes.array1_iff_eq_of_list_word_at H ZnWords; eassumption.
diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
index cd3af9e99..7292d7e76 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -41,7 +41,6 @@ Section WithParameters.
       ensures t' m := m =* ys$@x * xs$@y * R /\ t=t' }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
diff --git a/bedrock2/src/bedrock2Examples/swap.v b/bedrock2/src/bedrock2Examples/swap.v
index 9c3eaf5f6..36878febc 100644
--- a/bedrock2/src/bedrock2Examples/swap.v
+++ b/bedrock2/src/bedrock2Examples/swap.v
@@ -66,7 +66,7 @@ Section WithParameters.
   Lemma swap_swap_ok : program_logic_goal_for_function! swap_swap.
   Proof. repeat (straightline || straightline_call); eauto. Qed.
 
-  Lemma link_swap_swap_swap_swap : spec_of_swap_swap &[,swap_swap; swap].
+  Lemma link_swap_swap_swap_swap : spec_of_swap_swap (map.of_list &[,swap_swap; swap]).
   Proof. eauto using swap_swap_ok, swap_ok. Qed.
 
   (* Print Assumptions link_swap_swap_swap_swap. *)
diff --git a/bedrock2/src/bedrock2Examples/swap_by_add.v b/bedrock2/src/bedrock2Examples/swap_by_add.v
index 81e7898be..b7ac64911 100644
--- a/bedrock2/src/bedrock2Examples/swap_by_add.v
+++ b/bedrock2/src/bedrock2Examples/swap_by_add.v
@@ -56,7 +56,7 @@ Section WithParameters.
     repeat (straightline || straightline_call); eauto.
   Qed.
 
-  Lemma link_swap_swap_swap_swap : spec_of_swap_swap &[,swap_swap; swap].
+  Lemma link_swap_swap_swap_swap : spec_of_swap_swap (map.of_list &[,swap_swap; swap]).
   Proof. eauto using swap_swap_ok, swap_ok. Qed.
 
   (* Print Assumptions link_swap_swap_swap_swap. *)
diff --git a/compiler/src/compiler/ExprImp.v b/compiler/src/compiler/ExprImp.v
index 60015aeab..fc08821ab 100644
--- a/compiler/src/compiler/ExprImp.v
+++ b/compiler/src/compiler/ExprImp.v
@@ -11,7 +11,7 @@ Require Import coqutil.Decidable.
 Require Import coqutil.Datatypes.PropSet.
 Require Import riscv.Platform.MetricLogging.
 Require Import coqutil.Tactics.Simp.
-Import Semantics.
+Require Import bedrock2.Semantics bedrock2.MetricSemantics.
 
 (*Local Set Ltac Profiling.*)
 
@@ -20,7 +20,6 @@ Open Scope Z_scope.
 Section ExprImp1.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
   Notation var := String.string (only parsing).
@@ -42,7 +41,7 @@ Section ExprImp1.
     Context (e: env).
 
     Definition eval_expr(m: mem)(st: locals)(e: expr): result word :=
-      match eval_expr_old m st e with
+      match Semantics.eval_expr m st e with
       | Some v => Success v
       | None => error:("evaluation of expression" e "failed")
       end.
@@ -156,8 +155,8 @@ Section ExprImp1.
 
     Lemma invert_eval_store: forall fuel initialSt initialM a v final aSize,
       eval_cmd (S fuel) initialSt initialM (cmd.store aSize a v) = Success final ->
-      exists av vv finalM, eval_expr_old initialM initialSt a = Some av /\
-                           eval_expr_old initialM initialSt v = Some vv /\
+      exists av vv finalM, Semantics.eval_expr initialM initialSt a = Some av /\
+                           Semantics.eval_expr initialM initialSt v = Some vv /\
                            store aSize initialM av vv = Some finalM /\
                            final = (initialSt, finalM).
     Proof. inversion_lemma. Qed.
@@ -169,7 +168,7 @@ Section ExprImp1.
 
     Lemma invert_eval_set: forall f st1 m1 p2 x e,
       eval_cmd (S f) st1 m1 (cmd.set x e) = Success p2 ->
-      exists v, eval_expr_old m1 st1 e = Some v /\ p2 = (map.put st1 x v, m1).
+      exists v, Semantics.eval_expr m1 st1 e = Some v /\ p2 = (map.put st1 x v, m1).
     Proof. inversion_lemma. Qed.
 
     Lemma invert_eval_unset: forall f st1 m1 p2 x,
@@ -180,7 +179,7 @@ Section ExprImp1.
     Lemma invert_eval_cond: forall f st1 m1 p2 cond bThen bElse,
       eval_cmd (S f) st1 m1 (cmd.cond cond bThen bElse) = Success p2 ->
       exists cv,
-        eval_expr_old m1 st1 cond = Some cv /\
+        Semantics.eval_expr m1 st1 cond = Some cv /\
         (cv <> word.of_Z 0 /\ eval_cmd f st1 m1 bThen = Success p2 \/
          cv = word.of_Z 0  /\ eval_cmd f st1 m1 bElse = Success p2).
     Proof. inversion_lemma. Qed.
@@ -188,7 +187,7 @@ Section ExprImp1.
     Lemma invert_eval_while: forall st1 m1 p3 f cond body,
       eval_cmd (S f) st1 m1 (cmd.while cond body) = Success p3 ->
       exists cv,
-        eval_expr_old m1 st1 cond = Some cv /\
+        Semantics.eval_expr m1 st1 cond = Some cv /\
         (cv <> word.of_Z 0 /\ (exists st2 m2, eval_cmd f st1 m1 body = Success (st2, m2) /\
                                      eval_cmd f st2 m2 (cmd.while cond body) = Success p3) \/
          cv = word.of_Z 0 /\ p3 = (st1, m1)).
@@ -377,7 +376,6 @@ Ltac invert_eval_cmd :=
 Section ExprImp2.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
   Notation var := String.string (only parsing).
diff --git a/compiler/src/compiler/ExprImpEventLoopSpec.v b/compiler/src/compiler/ExprImpEventLoopSpec.v
index 777cd0a90..9fd056417 100644
--- a/compiler/src/compiler/ExprImpEventLoopSpec.v
+++ b/compiler/src/compiler/ExprImpEventLoopSpec.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Coq.Strings.String.
 Require Import coqutil.Map.Interface coqutil.Word.Interface.
 Require Import bedrock2.MetricLogging.
+Require Import bedrock2.Semantics.
 Require Import compiler.SeparationLogic.
 Require Import compiler.LowerPipeline.
 Require Import compiler.Pipeline.
@@ -9,7 +10,6 @@ Require Import compiler.Pipeline.
 Section Params1.
   Context {width} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: Semantics.ExtSpec}.
 
   Set Implicit Arguments.
@@ -37,15 +37,15 @@ Section Params1.
   {
     funs_valid: valid_src_funs e = true;
     init_code: Syntax.cmd.cmd;
-    get_init_code: map.get (map.of_list e) init_f = Some (nil, nil, init_code);
+    get_init_code: map.get (map.of_list e : env) init_f = Some (nil, nil, init_code);
     init_code_correct: forall m0 mc0,
         mem_available spec.(datamem_start) spec.(datamem_pastend) m0 ->
-        Semantics.exec (map.of_list e) init_code nil m0 map.empty mc0 (hl_inv spec);
+        MetricSemantics.exec (map.of_list e) init_code nil m0 map.empty mc0 (hl_inv spec);
     loop_body: Syntax.cmd.cmd;
-    get_loop_body: map.get (map.of_list e) loop_f = Some (nil, nil, loop_body);
+    get_loop_body: map.get (map.of_list e : env) loop_f = Some (nil, nil, loop_body);
     loop_body_correct: forall t m l mc,
         hl_inv spec t m l mc ->
-        Semantics.exec (map.of_list e) loop_body t m l mc (hl_inv spec);
+        MetricSemantics.exec (map.of_list e) loop_body t m l mc (hl_inv spec);
   }.
 
 End Params1.
diff --git a/compiler/src/compiler/FlattenExpr.v b/compiler/src/compiler/FlattenExpr.v
index bc2e4611e..39ac81e16 100644
--- a/compiler/src/compiler/FlattenExpr.v
+++ b/compiler/src/compiler/FlattenExpr.v
@@ -7,7 +7,7 @@ Require Import coqutil.Decidable.
 Require Import coqutil.Word.Bitwidth.
 Require Import bedrock2.Syntax.
 Require Import bedrock2.MetricLogging.
-Require Import bedrock2.Semantics.
+Require Import bedrock2.Semantics bedrock2.MetricSemantics.
 Require Import coqutil.Macros.unique.
 Require Import Coq.Bool.Bool.
 Require Import coqutil.Datatypes.PropSet.
@@ -25,14 +25,12 @@ Section FlattenExpr1.
           {word_ok: word.ok word}
           {locals: map.map String.string word}
           {mem: map.map word Byte.byte}
-          {ExprImp_env: map.map string (list string * list string * cmd)}
           {FlatImp_env: map.map string (list string * list string * FlatImp.stmt string)}
           {ext_spec: ExtSpec}
           {NGstate: Type}
           {NG: NameGen String.string NGstate}
           {locals_ok: map.ok locals}
           {mem_ok: map.ok mem}
-          {ExprImp_env_ok: map.ok ExprImp_env}
           {FlatImp_env_ok: map.ok FlatImp_env}
           {ext_spec_ok: ext_spec.ok ext_spec}.
 
@@ -523,7 +521,7 @@ Section FlattenExpr1.
     map.extends lL lH ->
     map.undef_on lH (allFreshVars ngs1) ->
     disjoint (ExprImp.allVars_exprs es) (allFreshVars ngs1) ->
-    evaluate_call_args_log m lH es initialMcH = Some (resVals, finalMcH) ->
+    eval_call_args m lH es initialMcH = Some (resVals, finalMcH) ->
     (* List.option_all (List.map (eval_expr m lH) es) = Some resVals -> *)
     FlatImp.exec fenv s t m lL initialMcL (fun t' m' lL' finalMcL =>
       t' = t /\ m' = m /\
@@ -685,7 +683,7 @@ Section FlattenExpr1.
   Lemma flattenStmt_correct_aux: forall eH eL,
       flatten_functions eH = Success eL ->
       forall eH0 sH t m mcH lH post,
-      Semantics.exec eH0 sH t m lH mcH post ->
+      MetricSemantics.exec eH0 sH t m lH mcH post ->
       eH0 = eH ->
       forall ngs ngs' sL lL mcL,
       flattenStmt ngs sH = (sL, ngs') ->
@@ -931,7 +929,7 @@ Section FlattenExpr1.
   Lemma flattenStmt_correct: forall eH eL sH sL lL t m mc post,
       flatten_functions eH = Success eL ->
       ExprImp2FlatImp sH = sL ->
-      Semantics.exec eH sH t m map.empty mc post ->
+      MetricSemantics.exec eH sH t m map.empty mc post ->
       FlatImp.exec eL sL t m lL mc (fun t' m' lL' mcL' => exists lH' mcH',
         post t' m' lH' mcH' /\
         map.extends lL' lH' /\
diff --git a/compiler/src/compiler/FlattenExprDef.v b/compiler/src/compiler/FlattenExprDef.v
index 2fd8a8f4a..41ab0ee5d 100644
--- a/compiler/src/compiler/FlattenExprDef.v
+++ b/compiler/src/compiler/FlattenExprDef.v
@@ -21,7 +21,6 @@ Section FlattenExpr1.
           {word_ok: word.ok word}
           {locals: map.map String.string word}
           {mem: map.map word byte}
-          {ExprImp_env: map.map string (list string * list string * cmd)}
           {FlatImp_env: map.map string (list string * list string * FlatImp.stmt string)}
           {ext_spec: ExtSpec}
           {NGstate: Type}
@@ -159,7 +158,7 @@ Section FlattenExpr1.
       let body' := fst (flattenStmt (freshNameGenState avoid) body) in
       Success (argnames, retnames, body').
 
-  Definition flatten_functions: ExprImp_env -> result FlatImp_env :=
+  Definition flatten_functions: Semantics.env -> result FlatImp_env :=
     map.try_map_values flatten_function.
 
 End FlattenExpr1.
diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v
index 6dd84f8b4..338c5d72d 100644
--- a/compiler/src/compiler/Pipeline.v
+++ b/compiler/src/compiler/Pipeline.v
@@ -140,10 +140,11 @@ Section WithWordAndMem.
       andb (Z.leb (-2048) x) (Z.ltb x 2048).
 
     Definition locals_based_call_spec{Var Cmd: Type}{locals: map.map Var word}
-               (Exec: string_keyed_map (list Var * list Var * Cmd) ->
+               {string_keyed_map: forall T: Type, map.map string T}
+               (Exec: string_keyed_map (list Var * list Var * Cmd)%type ->
                       Cmd -> trace -> mem -> locals -> MetricLog ->
                       (trace -> mem -> locals -> MetricLog -> Prop) -> Prop)
-               (e: string_keyed_map (list Var * list Var * Cmd))(f: string)
+               (e: string_keyed_map (list Var * list Var * Cmd)%type)(f: string)
                (t: trace)(m: mem)(argvals: list word)
                (post: trace -> mem -> list word -> Prop): Prop :=
       exists argnames retnames fbody l,
@@ -157,9 +158,9 @@ Section WithWordAndMem.
       fun '(argnames, retnames, body) => NoDup argnames /\ NoDup retnames.
 
     Definition SrcLang: Lang := {|
-      Program := string_keyed_map (list string * list string * Syntax.cmd);
+      Program := Semantics.env;
       Valid := map.forall_values ExprImp.valid_fun;
-      Call := locals_based_call_spec Semantics.exec;
+      Call := locals_based_call_spec MetricSemantics.exec;
     |}.
     (* |                 *)
     (* | FlattenExpr     *)
@@ -220,7 +221,7 @@ Section WithWordAndMem.
     Lemma flattening_correct: phase_correct SrcLang FlatWithStrVars flatten_functions.
     Proof.
       unfold SrcLang, FlatWithStrVars.
-      split; cbn.
+      split; cbn -[flatten_functions].
       { unfold map.forall_values, ParamsNoDup.
         intros. destruct v as ((argnames & retnames) & body).
         eapply flatten_functions_NoDup; try eassumption.
@@ -434,7 +435,7 @@ Section WithWordAndMem.
     Qed.
 
     Definition composed_compile:
-      string_keyed_map (list string * list string * cmd) ->
+      Semantics.env ->
       result (list Instruction * string_keyed_map Z * Z) :=
       (compose_phases flatten_functions
       (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate)
@@ -481,8 +482,8 @@ Section WithWordAndMem.
         ExprImp.valid_funs (map.of_list fs).
     Proof.
       unfold valid_funs. induction fs; intros.
-      - simpl in H0. rewrite map.get_empty in H0. discriminate.
-      - destruct a as (name & body). simpl in H0. rewrite map.get_put_dec in H0. fwd.
+      - cbn [map.of_list] in H0. rewrite map.get_empty in H0. discriminate.
+      - destruct a as (name & body). cbn [map.of_list] in H0. rewrite map.get_put_dec in H0. fwd.
         destruct_one_match_hyp.
         + fwd. eapply valid_src_fun_correct. eassumption.
         + eapply IHfs; eassumption.
@@ -501,10 +502,11 @@ Section WithWordAndMem.
         valid_src_funs functions = true ->
         compile functions = Success (instrs, finfo, req_stack_size) ->
         (exists (argnames retnames: list string) (fbody: cmd) l,
-            map.get (map.of_list functions) fname = Some (argnames, retnames, fbody) /\
+            map.get (map.of_list (map := Semantics.env) functions) fname =
+              Some (argnames, retnames, fbody) /\
             map.of_list_zip argnames argvals = Some l /\
             forall mc,
-              Semantics.exec (map.of_list functions) fbody t mH l mc
+              MetricSemantics.exec (map.of_list functions) fbody t mH l mc
                 (fun t' m' l' mc' => exists retvals: list word,
                      map.getmany_of_list l' retnames = Some retvals /\
                      post t' m' retvals)) ->
@@ -573,7 +575,7 @@ Section WithWordAndMem.
         valid_src_funs fs = true ->
         NoDup (map fst fs) ->
         compile fs = Success (instrs, finfo, req_stack_size) ->
-        WeakestPrecondition.call fs fname t mH argvals post ->
+        WeakestPrecondition.call (map.of_list fs) fname t mH argvals post ->
         map.get (map.of_list finfo) fname = Some f_rel_pos ->
         req_stack_size <= word.unsigned (word.sub stack_hi stack_lo) / bytes_per_word ->
         word.unsigned (word.sub stack_hi stack_lo) mod bytes_per_word = 0 ->
@@ -593,14 +595,13 @@ Section WithWordAndMem.
     Proof.
       intros.
       let H := hyp WeakestPrecondition.call in rename H into WP.
-      eapply WeakestPreconditionProperties.sound_call' in WP.
-      2: { eapply map.all_gets_from_map_of_NoDup_list; assumption. }
-      fwd.
-      edestruct compiler_correct with (argvals := argvals) (post := post) as (f_rel_pos' & G & C);
+      edestruct compiler_correct with (fname := fname) (argvals := argvals) (post := post) as (f_rel_pos' & G & C);
         try eassumption.
-      - intros.
-        unfold map.of_list_zip in *. eauto 10.
-      - eapply C; clear C; try assumption; try congruence.
+      2: { eapply C; clear C; try assumption; try congruence; try eassumption. }
+      intros.
+      unfold Semantics.call in WP. fwd.
+      do 5 eexists. 1: eassumption. split. 1: eassumption.
+      intros. eapply MetricSemantics.of_metrics_free. assumption.
     Qed.
 
   End WithMoreParams.
diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v
index 590fac9f0..7b82edff5 100644
--- a/compiler/src/compiler/ToplevelLoop.v
+++ b/compiler/src/compiler/ToplevelLoop.v
@@ -221,6 +221,8 @@ Section Pipeline1.
     apply Zmod_0_l.
   Qed.
 
+  Local Arguments map.get : simpl never.
+
   Lemma establish_ll_inv: forall (initial: MetricRiscvMachine),
       initial_conditions initial ->
       ll_inv initial.
diff --git a/compiler/src/compilerExamples/SoftmulCompile.v b/compiler/src/compilerExamples/SoftmulCompile.v
index f583afc32..81cab55d2 100644
--- a/compiler/src/compilerExamples/SoftmulCompile.v
+++ b/compiler/src/compilerExamples/SoftmulCompile.v
@@ -649,9 +649,9 @@ Section Riscv.
       unfold isXAddr4, isXAddr1. ssplit; eapply In_word_seq; try ZnWords.
   Qed.
 
-  Lemma link_softmul_bedrock2: spec_of_softmul funimplsList.
+  Lemma link_softmul_bedrock2: spec_of_softmul (map.of_list funimplsList).
   Proof.
-    eapply softmul_ok. eapply rpmul.rpmul_ok.
+    eapply softmul_ok. 1: reflexivity. eapply rpmul.rpmul_ok. reflexivity.
   Qed.
 
   Import FunctionalExtensionality PropExtensionality.
@@ -727,7 +727,7 @@ Section Riscv.
                                     initial.(pc);
           getLog := []
         |};
-        getMetrics := MetricLogging.EmptyMetricLog
+        getMetrics := riscv.Platform.MetricLogging.EmptyMetricLog
       |}).
       2: reflexivity.
       2: {
diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v
index 1bb255cf4..dd1299817 100644
--- a/end2end/src/end2end/End2EndLightbulb.v
+++ b/end2end/src/end2end/End2EndLightbulb.v
@@ -76,13 +76,13 @@ Definition loop :=
   ("loop", ([]: list string, []: list string,
            (cmd.call ["err"] "lightbulb_loop" [expr.literal buffer_addr]))).
 
-Definition prog := init :: loop :: lightbulb.function_impls.
+Definition prog := map.putmany_of_list (init :: loop :: nil) lightbulb.function_impls.
 
 (* Before running this command, it might be a good idea to do
    "Print Assumptions lightbulb_insts_unevaluated."
    and to check if there are any axioms which could block the computation. *)
 Definition lightbulb_compiled: list Decode.Instruction * list (string * Z) * Z.
-  let r := eval cbv in (ToplevelLoop.compile_prog MMIO.compile_ext_call ml prog) in
+  let r := eval cbv in (ToplevelLoop.compile_prog MMIO.compile_ext_call ml (map.tuples prog)) in
   lazymatch r with
   | Success ?x => exact x
   end.
@@ -110,7 +110,7 @@ Definition required_stack_space: Z.
 Defined.
 
 Definition compilation_result:
-  ToplevelLoop.compile_prog MMIO.compile_ext_call ml prog =
+  ToplevelLoop.compile_prog MMIO.compile_ext_call ml (map.tuples prog) =
   Success (lightbulb_insts, function_positions, required_stack_space).
 Proof. reflexivity. Qed.
 
@@ -182,7 +182,7 @@ Proof.
   intros *. intro KB.
   specialize Q with (stack_size_in_bytes := stack_size_in_bytes).
   specialize_first Q mem0.
-  specialize_first Q prog.
+  specialize_first Q (map.tuples prog).
   specialize_first Q open_constr:(eq_refl).
   specialize_first Q open_constr:(eq_refl).
   specialize_first Q open_constr:(eq_refl).
@@ -190,7 +190,7 @@ Proof.
   specialize_first Q (Zkeyed_map (KamiWord.word 32)).
   specialize_first Q (Zkeyed_map_ok (KamiWord.word 32)).
   specialize_first Q mem_ok.
-  specialize Q with (13 := KB). (* TODO add bigger numbers to coqutil.Tactics.forward.specialize_first *)
+  specialize Q with (12 := KB). (* TODO add bigger numbers to coqutil.Tactics.forward.specialize_first *)
   (* specialize_first Q KB. *)
   specialize_first Q compilation_result.
 
@@ -216,8 +216,6 @@ Proof.
   }
   eapply Q; clear Q.
   - cbv. intuition discriminate.
-  - clear. cbv.
-    repeat econstructor; intro; repeat match goal with H: In _ _|-_=> destruct H end; discriminate.
   - intros. clear KB mem0. simp.
     unfold SPI.mmio_trace_abstraction_relation in *.
     unfold id in *.
@@ -225,9 +223,14 @@ Proof.
   - reflexivity.
   - (* establish invariant *)
     repeat ProgramLogic.straightline.
-    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _);
-      [|exact (link_lightbulb_init m nil)].
-
+    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _).
+    2: {
+      unfold prog. eapply Semantics.extend_env_call. 2: exact (link_lightbulb_init m nil).
+      rewrite map.of_list_tuples.
+      intros k f G. unfold map.putmany_of_list, init, loop.
+      rewrite ?map.get_put_dec.
+      repeat destruct_one_match; subst; try discriminate G. assumption.
+    }
     intros ? ? ? ?.
     repeat ProgramLogic.straightline.
     unfold LowerPipeline.mem_available, hl_inv, isReady, goodTrace, goodHlTrace, buffer_addr, ml, End2EndPipeline.ml, code_start, heap_start, heap_pastend, Lift1Prop.ex1 in *; Simp.simp.
@@ -266,9 +269,14 @@ Proof.
     specialize_first P Hp0p0.
     specialize_first P t0.
     specialize_first P Hp0p1.
-    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _);
-      [|exact P]; clear P.
-
+    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _).
+    2: {
+      unfold prog. eapply Semantics.extend_env_call. 2: exact P.
+      rewrite map.of_list_tuples.
+      intros k f G. unfold map.putmany_of_list, init, loop.
+      rewrite ?map.get_put_dec.
+      repeat destruct_one_match; subst; try discriminate G. assumption.
+    }
     intros ? ? ? ?.
     Simp.simp.
     repeat ProgramLogic.straightline.
diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v
index 428d97667..abee97136 100644
--- a/end2end/src/end2end/End2EndPipeline.v
+++ b/end2end/src/end2end/End2EndPipeline.v
@@ -199,8 +199,6 @@ Section Connect.
 
   Definition bedrock2Inv := (fun t m l => forall mc, hl_inv spec t m l mc).
 
-  Let funspecs := WeakestPrecondition.call funimplsList.
-
   Hypothesis goodTrace_implies_related_to_Events: forall (t: list LogItem),
       spec.(goodTrace) t -> exists t': list Event, traces_related t' t.
 
@@ -298,10 +296,10 @@ Section Connect.
     forall init_code loop_body,
     map.get (map.of_list funimplsList) "init"%string = Some ([], [], init_code) ->
     (forall m, LowerPipeline.mem_available ml.(heap_start) ml.(heap_pastend) m ->
-               WeakestPrecondition.cmd funspecs init_code [] m map.empty bedrock2Inv) ->
+               WeakestPrecondition.cmd (map.of_list funimplsList) init_code [] m map.empty bedrock2Inv) ->
     map.get (map.of_list funimplsList) "loop"%string = Some ([], [], loop_body) ->
     (forall t m l, bedrock2Inv t m l ->
-                   WeakestPrecondition.cmd funspecs loop_body t m l bedrock2Inv) ->
+                   WeakestPrecondition.cmd (map.of_list funimplsList) loop_body t m l bedrock2Inv) ->
     (* Assumptions on the compiler level: *)
     forall (instrs: list Instruction) positions (required_stack_space: Z),
     compile_prog compile_ext_call ml funimplsList = Success (instrs, positions, required_stack_space) ->
@@ -371,12 +369,14 @@ Section Connect.
                rewrite heap_start_agree in H;
                rewrite heap_pastend_agree in H
              end.
-             refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _ _); eauto.
+             eapply MetricSemantics.of_metrics_free.
+             eapply WeakestPreconditionProperties.sound_cmd; eauto.
           -- simpl. clear. intros. unfold bedrock2Inv in *. eauto.
         * exact GetLoop.
         * intros. unfold bedrock2Inv in *.
           eapply ExprImp.weaken_exec.
-          -- refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _ _); eauto.
+          -- eapply MetricSemantics.of_metrics_free.
+             eapply WeakestPreconditionProperties.sound_cmd; eauto.
           -- simpl. clear. intros. eauto.
       + assumption.
       + assumption.