From 7a43f3ad93fb8c583a19faa92beff2ee6b14a35d Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Tue, 25 Jul 2023 21:47:05 -0400
Subject: [PATCH 1/8] define a WP.cmd' in terms of exec, might soon replace
 WP.cmd

and rules for cmd' whose premises are copied from WP.cmd.
This one is "fs everywhere" (ie list of functions everywhere).
The wp_call rule requires a NoDup, which would be cumbersome to
carry around.
---
 bedrock2/src/bedrock2/WeakestPrecondition.v | 364 +++++++++++++++++++-
 1 file changed, 362 insertions(+), 2 deletions(-)

diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index ce45aa805..de6409fd9 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -42,6 +42,28 @@ Section WeakestPrecondition.
     Fixpoint expr e := expr_body expr e.
   End WithMemAndLocals.
 
+  Ltac t :=
+    repeat match goal with
+      | |- forall _, _ => progress intros
+      | H: exists _, _ |- _ => destruct H
+      | H: and _ _ |- _ => destruct H
+      | H: eq _ ?y |- _ => subst y
+      | _ => progress cbn 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.
+  Proof.
+    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. }
+    { eapply IHe1 in H; t. rewrite H. Tactics.destruct_one_match.
+      { eapply IHe3 in H0; t. }
+      { eapply IHe2 in H0; t. } }
+  Qed.
+
   Section WithF.
     Context {A B} (f: A -> (B -> Prop) -> Prop).
     Definition list_map_body rec (xs : list A) (post : list B -> Prop) : Prop :=
@@ -55,10 +77,348 @@ Section WeakestPrecondition.
     Fixpoint list_map xs := list_map_body list_map xs.
   End WithF.
 
+  Lemma exprs_sound : forall m l args mc P,
+      list_map (expr m l) args P ->
+      exists x mc', Semantics.evaluate_call_args_log m l args mc = Some (x, mc') /\ P x.
+  Proof.
+    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.
+  Qed.
+
+  Lemma getmany_sound: forall a l P,
+      list_map (get l) a P -> exists vs, map.getmany_of_list l a = Some vs /\ P vs.
+  Proof.
+    cbv [map.getmany_of_list].
+    induction a; cbn; repeat (subst; t).
+    cbv [WeakestPrecondition.get] in H; t.
+    epose proof (IHa _ _ H0); clear IHa; t.
+    rewrite H. erewrite H1. eexists; split; eauto.
+  Qed.
+
+  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).
+
+  (* TODO move *)
+  Lemma map__invert_get_of_list{env_ok: map.ok env}: forall ksvs k v,
+      map.get (map.of_list (map := env) ksvs) k = Some v ->
+      List.In k (List.map fst ksvs).
+  Proof.
+    induction ksvs; cbn; intros.
+    - rewrite map.get_empty in H. discriminate H.
+    - destruct a as (k' & v'). rewrite Properties.map.get_put_dec in H.
+      destr.destr (String.eqb k' k).
+      + left. reflexivity.
+      + right. eapply IHksvs. eassumption.
+  Qed.
+
+  Lemma exec_cons_env{env_ok: map.ok env}: forall fname fimpl fs c t m l mc post,
+      ~ List.In fname (List.map fst fs) ->
+      exec (map.of_list fs) c t m l mc post ->
+      exec (map.of_list ((fname, fimpl) :: fs)) c t m l mc post.
+  Proof.
+    induction 2; try solve [econstructor; eauto].
+    econstructor; try eassumption.
+    cbn. rewrite map.get_put_diff. 1: eassumption.
+    intro C. subst fname0.
+    apply H.
+    eapply map__invert_get_of_list.
+    eassumption.
+  Qed.
+
+  Section WithFunctionList1.
+    Context (fs: list (String.string * (list String.string * list String.string * cmd))).
+
+    Inductive cmd' (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
+      (post : (trace -> mem -> locals -> Prop)) : Prop :=
+    | mk_cmd' (_ : forall mc, exec (map.of_list fs) c t m l mc
+                                (fun t' m' l' mc' => post t' m' l')).
+
+    Lemma invert_cmd': forall c t m l post,
+        cmd' c t m l post ->
+        forall mc, exec (map.of_list fs) c t m l mc (fun t' m' l' mc' => post t' m' l').
+    Proof. intros. inversion H. apply H0. Qed.
+
+    Definition func' '(innames, outnames, c) (t : trace) (m : mem) (args : list word)
+      (post : trace -> mem -> list word -> Prop) :=
+      exists l, map.of_list_zip innames args = Some l /\
+      cmd' c t m l (fun t m l =>
+        list_map (get l) outnames (fun rets =>
+        post t m rets)).
+  End WithFunctionList1.
+
+  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' functions decl t m args post
+        else rec functions fname t m args post
+    end.
+  Fixpoint call' functions := call_body' call' functions.
+
+  Section Dedup.
+    Context [A: Type] (aeq: A -> A -> bool).
+
+    (* dedup on (x :: xs) with x having a duplicate in xs discards x, whereas
+     head_prio_dedup keeps x but removes its duplicate from xs *)
+    Fixpoint List__head_prio_dedup (xs : list A) : list A :=
+      match xs with
+      | nil => nil
+      | cons h t => let t' := List__head_prio_dedup t in
+                    cons h (List.removeb aeq h t')
+      end.
+  End Dedup.
+
+  Lemma NoDup_head_prio_dedup[V: Type]: forall (l: list (String.string * V)),
+      List.NoDup (List.map fst (List__head_prio_dedup
+                                  (fun '(f1, _) '(f2, _) => String.eqb f1 f2) l)).
+  Proof.
+    induction l; cbn. 1: constructor.
+    destruct a as (k, v). cbn.
+    constructor.
+    - intro C. eapply List.in_map_iff in C.
+      destruct C as [[k' v'] [E C]]. cbn in E. subst k'.
+      unfold List.removeb in *.
+      eapply List.filter_In in C. apply proj2 in C. rewrite String.eqb_refl in C.
+      discriminate C.
+    -
+  Admitted. (* hopefully holds *)
+
+  Lemma map__get_of_list_filter_diff{env_ok: map.ok env}: forall k k' kvs,
+      k <> k' ->
+      map.get (map.of_list (map := env) kvs) k' =
+      map.get (map.of_list (List.filter
+                      (fun p => negb (let '(kj, _) := p in String.eqb k kj)) kvs)) k'.
+  Proof.
+    induction kvs; cbn; intros. 1: reflexivity.
+    destruct a as (kj & v).
+    rewrite Properties.map.get_put_dec. destr.destr (String.eqb kj k').
+    - destr.destr (String.eqb k k'). 1: contradiction.
+      cbn. rewrite map.get_put_same. reflexivity.
+    - destr.destr (String.eqb k kj); cbn.
+      + eapply IHkvs. assumption.
+      + rewrite map.get_put_diff by congruence. eapply IHkvs. assumption.
+  Qed.
+
+  Lemma map__of_list_ignores_head_prio_dedup{env_ok: map.ok env}: forall ksvs,
+      map.of_list (map := env) ksvs =
+      map.of_list (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) ksvs).
+  Proof.
+    induction ksvs; cbn. 1: reflexivity.
+    destruct a as (k & v).
+    eapply map.map_ext.
+    intros k'. rewrite? Properties.map.get_put_dec. destr.destr (String.eqb k k').
+    1: reflexivity.
+    rewrite IHksvs.
+    unfold List.removeb.
+    remember (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) ksvs) as L.
+    apply map__get_of_list_filter_diff. assumption.
+  Qed.
+
+  Lemma call'_ignores_head_prio_dedup_otherdirection{env_ok: map.ok env}:
+    forall fs fname t m args post,
+      call' (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) fs)
+            fname t m args post ->
+      call' fs fname t m args post.
+  Proof.
+    induction fs; cbn; intros. 1: assumption.
+    destruct a as (f, decl). destr.destr (String.eqb f fname).
+    - unfold func' in *. destruct decl as ((argnames, retnames), body).
+      destruct H as (l & Hl & Hbody). exists l. split. 1: exact Hl.
+      inversion Hbody. constructor. intro mc. specialize (H mc).
+      rewrite map__of_list_ignores_head_prio_dedup in H.
+  Abort.
+
+  Lemma call'_ignores_head_prio_dedup{env_ok: map.ok env}:
+    forall fs fname t m args post,
+      call' fs fname t m args post ->
+      call' (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) fs)
+            fname t m args post.
+  Proof.
+    induction fs; cbn; intros. 1: assumption.
+    destruct a as (f, decl). destr.destr (String.eqb f fname).
+    - unfold func' in *. destruct decl as ((argnames, retnames), body).
+      destruct H as (l & Hl & Hbody). exists l. split. 1: exact Hl.
+      constructor. intro mc. eapply invert_cmd' in Hbody.
+      rewrite map__of_list_ignores_head_prio_dedup in Hbody.
+  Admitted. (* TODO probably DOES NOT HOLD because recursive call of call' is made
+               on smaller env with current function removed *)
+
+  Section WithFunctionList2.
+    Implicit Type post : trace -> mem -> locals -> Prop.
+    Context (fs: list (String.string * (list String.string * list String.string * cmd))).
+
+    Notation cmd' := (cmd' fs).
+
+    Ltac step :=
+      match reverse goal with
+      | H: _ /\ _ |- _ => destruct H
+      | H: exists x, _ |- _ => let n := fresh x in destruct H as [n H]
+      | |- _ => progress unfold dlet, dexpr, store in *
+      | H: cmd' _ _ _ _ _ |- _ => pose proof (invert_cmd' _ _ _ _ _ _ H); clear H
+      | |- _ => constructor
+      | |- _ => assumption
+      | H: forall _: MetricLogging.MetricLog, _ |- _ => apply H
+      | |- _ => progress intros
+      | |- _ => progress subst
+      (* creates an evar for metrics, therefore needs to be applied from top to bottom,
+         so we need `match reverse` instead of `match` *)
+      | H: expr _ _ _ _ |- _ => eapply expr_sound in H
+      | |- _ => solve [econstructor; eauto]
+      end.
+    Ltac tac := repeat step.
+
+    Lemma wp_skip: forall t m l post, post t m l -> cmd' cmd.skip t m l post.
+    Proof. tac. Qed.
+
+    Lemma wp_set: forall x ev t m l post,
+        (exists v, dexpr m l ev v /\
+        dlet! l := map.put l x v in
+        post t m l) ->
+        cmd' (cmd.set x ev) t m l post.
+    Proof. tac. Qed.
+
+    Lemma wp_unset: forall x t m l post,
+        (dlet! l := map.remove l x in
+         post t m l) ->
+        cmd' (cmd.unset x) t m l post.
+    Proof. tac. Qed.
+
+    Lemma wp_store: forall sz ea ev t m l post,
+       (exists a, dexpr m l ea a /\
+        exists v, dexpr m l ev v /\
+        store sz m a v (fun m =>
+        post t m l)) ->
+       cmd' (cmd.store sz ea ev) t m l post.
+    Proof. tac. Qed.
+
+    Lemma wp_stackalloc: forall x n c t m l post,
+        (Z.modulo n (bytes_per_word width) = 0 /\
+        forall a mStack mCombined,
+          anybytes a n mStack -> map.split mCombined m mStack ->
+          dlet! l := map.put l x a in
+          cmd' c t mCombined l (fun t' mCombined' l' =>
+          exists m' mStack',
+          anybytes a n mStack' /\ map.split mCombined' m' mStack' /\
+          post t' m' l')) ->
+          cmd' (cmd.stackalloc x n c) t m l post.
+    Proof. tac. specialize H0 with (1 := H1) (2 := H2). tac. Qed.
+
+    Lemma wp_cond: forall br ct cf t m l post,
+        (exists v, dexpr m l br v /\
+        (word.unsigned v <> 0%Z -> cmd' ct t m l post) /\
+        (word.unsigned v = 0%Z -> cmd' cf t m l post)) ->
+        cmd' (cmd.cond br ct cf) t m l post.
+    Proof.
+      tac. destr.destr (Z.eqb (word.unsigned v0) 0).
+      - specialize H1 with (1 := E). tac.
+      - specialize H0 with (1 := E). tac.
+    Qed.
+
+    Lemma wp_seq: forall c1 c2 t m l post,
+        cmd' c1 t m l (fun t m l => cmd' c2 t m l post) ->
+        cmd' (cmd.seq c1 c2) t m l post.
+    Proof.
+      tac. eapply exec.weaken.
+      { econstructor. 1: eapply H0. tac. }
+      tac.
+    Qed.
+
+    Lemma wp_while: forall e c t m l post,
+       (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' 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' (cmd.while e c) t m l post.
+    Proof.
+      intros. destruct H as (measure & lt & inv & Hwf & HInit & Hbody).
+      destruct HInit as (v0 & HInit).
+      econstructor. intros.
+      revert t m l mc 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' & mc' & 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). inversion Ht. clear Ht.
+        eapply exec.while_true; eauto.
+        cbv beta. intros * (v' & HInv & HLt). eauto.
+    Qed.
+
+    Lemma wp_call0{env_ok: map.ok env}
+      (Hnd : List.NoDup (List.map fst fs)): (* <--------- *)
+      forall binds fname arges t m l post,
+       (exists args, dexprs m l arges args /\
+        call' fs 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' (cmd.call binds fname arges) t m l post.
+    Proof.
+      tac.
+      unfold dexprs in *.
+      eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
+      unfold call' in *.
+      revert fname H0. induction fs; intros.
+      - cbn in H0. contradiction.
+      - rename l0 into fs0.
+        destruct a as (fnameHere & ((argnames & retnames) & fbody)).
+        inversion Hnd. subst.
+        cbn in H0.
+        destr.destr (String.eqb fnameHere fname).
+        + destruct H0 as (l1 & Hl1 & Hbody).
+          inversion Hbody. clear Hbody. rename H into Hbody.
+          eapply exec.call.
+          * cbn. rewrite map.get_put_same. reflexivity.
+          * eassumption.
+          * eassumption.
+          * eapply exec_cons_env. 1: assumption. apply Hbody.
+          * cbv beta. intros. eapply getmany_sound. assumption.
+        + eapply exec_cons_env. 1: assumption.
+          eapply IHl0; assumption.
+    Qed.
+
+    Lemma wp_interact: forall binds action arges t m l post,
+       (exists args, dexprs m l arges args /\
+        exists mKeep mGive, map.split m mKeep mGive /\
+        ext_spec t mGive action args (fun mReceive rets =>
+          exists l', map.putmany_of_list_zip binds rets l = Some l' /\
+          forall m', map.split m' mKeep mReceive ->
+          post (cons ((mGive, action, args), (mReceive, rets)) t) m' l')) ->
+       cmd' (cmd.interact binds action arges) t m l post.
+    Proof.
+      tac.
+      eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
+      tac.
+    Qed.
+  End WithFunctionList2.
+
+  (* without NoDup assumption, but probably doesn't hold *)
+  Lemma wp_call{env_ok: map.ok env}: forall fs binds fname arges t m l post,
+      (exists args, dexprs m l arges args /\
+       call' fs 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' fs (cmd.call binds fname arges) t m l post.
+  Proof.
+    intros. destruct H as (args & Hargs & H).
+    constructor. rewrite map__of_list_ignores_head_prio_dedup. eapply invert_cmd'.
+    eapply (wp_call0 _ (env_ok := env_ok)).
+    1: eapply NoDup_head_prio_dedup.
+    eexists. split. 1: eassumption.
+    eapply call'_ignores_head_prio_dedup. assumption.
+  Qed.
+
   Section WithFunctions.
     Context (call : String.string -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
-    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).
     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 *)

From 4b3e91715d82c8d79a3bd3407da7e665eba6c5bb Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Tue, 25 Jul 2023 22:11:43 -0400
Subject: [PATCH 2/8] dead simple `call` based on `map.get`

---
 bedrock2/src/bedrock2/WeakestPrecondition.v | 137 ++------------------
 1 file changed, 14 insertions(+), 123 deletions(-)

diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index de6409fd9..e45fe7926 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -147,19 +147,13 @@ Section WeakestPrecondition.
       cmd' c t m l (fun t m l =>
         list_map (get l) outnames (fun rets =>
         post t m rets)).
-  End WithFunctionList1.
 
-  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' functions decl t m args post
-        else rec functions fname t m args post
-    end.
-  Fixpoint call' functions := call_body' call' functions.
+    Definition call' (fname: String.string) :=
+      match map.get (map.of_list fs) fname with
+      | Some fimpl => func' fimpl
+      | None => fun _ _ _ _ => False
+      end.
+  End WithFunctionList1.
 
   Section Dedup.
     Context [A: Type] (aeq: A -> A -> bool).
@@ -174,81 +168,6 @@ Section WeakestPrecondition.
       end.
   End Dedup.
 
-  Lemma NoDup_head_prio_dedup[V: Type]: forall (l: list (String.string * V)),
-      List.NoDup (List.map fst (List__head_prio_dedup
-                                  (fun '(f1, _) '(f2, _) => String.eqb f1 f2) l)).
-  Proof.
-    induction l; cbn. 1: constructor.
-    destruct a as (k, v). cbn.
-    constructor.
-    - intro C. eapply List.in_map_iff in C.
-      destruct C as [[k' v'] [E C]]. cbn in E. subst k'.
-      unfold List.removeb in *.
-      eapply List.filter_In in C. apply proj2 in C. rewrite String.eqb_refl in C.
-      discriminate C.
-    -
-  Admitted. (* hopefully holds *)
-
-  Lemma map__get_of_list_filter_diff{env_ok: map.ok env}: forall k k' kvs,
-      k <> k' ->
-      map.get (map.of_list (map := env) kvs) k' =
-      map.get (map.of_list (List.filter
-                      (fun p => negb (let '(kj, _) := p in String.eqb k kj)) kvs)) k'.
-  Proof.
-    induction kvs; cbn; intros. 1: reflexivity.
-    destruct a as (kj & v).
-    rewrite Properties.map.get_put_dec. destr.destr (String.eqb kj k').
-    - destr.destr (String.eqb k k'). 1: contradiction.
-      cbn. rewrite map.get_put_same. reflexivity.
-    - destr.destr (String.eqb k kj); cbn.
-      + eapply IHkvs. assumption.
-      + rewrite map.get_put_diff by congruence. eapply IHkvs. assumption.
-  Qed.
-
-  Lemma map__of_list_ignores_head_prio_dedup{env_ok: map.ok env}: forall ksvs,
-      map.of_list (map := env) ksvs =
-      map.of_list (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) ksvs).
-  Proof.
-    induction ksvs; cbn. 1: reflexivity.
-    destruct a as (k & v).
-    eapply map.map_ext.
-    intros k'. rewrite? Properties.map.get_put_dec. destr.destr (String.eqb k k').
-    1: reflexivity.
-    rewrite IHksvs.
-    unfold List.removeb.
-    remember (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) ksvs) as L.
-    apply map__get_of_list_filter_diff. assumption.
-  Qed.
-
-  Lemma call'_ignores_head_prio_dedup_otherdirection{env_ok: map.ok env}:
-    forall fs fname t m args post,
-      call' (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) fs)
-            fname t m args post ->
-      call' fs fname t m args post.
-  Proof.
-    induction fs; cbn; intros. 1: assumption.
-    destruct a as (f, decl). destr.destr (String.eqb f fname).
-    - unfold func' in *. destruct decl as ((argnames, retnames), body).
-      destruct H as (l & Hl & Hbody). exists l. split. 1: exact Hl.
-      inversion Hbody. constructor. intro mc. specialize (H mc).
-      rewrite map__of_list_ignores_head_prio_dedup in H.
-  Abort.
-
-  Lemma call'_ignores_head_prio_dedup{env_ok: map.ok env}:
-    forall fs fname t m args post,
-      call' fs fname t m args post ->
-      call' (List__head_prio_dedup (fun '(f1, _) '(f2, _) => String.eqb f1 f2) fs)
-            fname t m args post.
-  Proof.
-    induction fs; cbn; intros. 1: assumption.
-    destruct a as (f, decl). destr.destr (String.eqb f fname).
-    - unfold func' in *. destruct decl as ((argnames, retnames), body).
-      destruct H as (l & Hl & Hbody). exists l. split. 1: exact Hl.
-      constructor. intro mc. eapply invert_cmd' in Hbody.
-      rewrite map__of_list_ignores_head_prio_dedup in Hbody.
-  Admitted. (* TODO probably DOES NOT HOLD because recursive call of call' is made
-               on smaller env with current function removed *)
-
   Section WithFunctionList2.
     Implicit Type post : trace -> mem -> locals -> Prop.
     Context (fs: list (String.string * (list String.string * list String.string * cmd))).
@@ -354,9 +273,7 @@ Section WeakestPrecondition.
         cbv beta. intros * (v' & HInv & HLt). eauto.
     Qed.
 
-    Lemma wp_call0{env_ok: map.ok env}
-      (Hnd : List.NoDup (List.map fst fs)): (* <--------- *)
-      forall binds fname arges t m l post,
+    Lemma wp_call{env_ok: map.ok env}: forall binds fname arges t m l post,
        (exists args, dexprs m l arges args /\
         call' fs fname t m args (fun t m rets =>
           exists l', map.putmany_of_list_zip binds rets l = Some l' /\
@@ -367,23 +284,13 @@ Section WeakestPrecondition.
       unfold dexprs in *.
       eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
       unfold call' in *.
-      revert fname H0. induction fs; intros.
-      - cbn in H0. contradiction.
-      - rename l0 into fs0.
-        destruct a as (fnameHere & ((argnames & retnames) & fbody)).
-        inversion Hnd. subst.
-        cbn in H0.
-        destr.destr (String.eqb fnameHere fname).
-        + destruct H0 as (l1 & Hl1 & Hbody).
-          inversion Hbody. clear Hbody. rename H into Hbody.
-          eapply exec.call.
-          * cbn. rewrite map.get_put_same. reflexivity.
-          * eassumption.
-          * eassumption.
-          * eapply exec_cons_env. 1: assumption. apply Hbody.
-          * cbv beta. intros. eapply getmany_sound. assumption.
-        + eapply exec_cons_env. 1: assumption.
-          eapply IHl0; assumption.
+      Tactics.destruct_one_match_hyp. 2: contradiction.
+      unfold func' in *.
+      destruct p as ((argnames & retnames) & fbody).
+      destruct H0 as (l1 & Hl1 & Hbody).
+      inversion Hbody. clear Hbody. rename H into Hbody.
+      eapply exec.call; eauto.
+      cbv beta. intros. eapply getmany_sound. assumption.
     Qed.
 
     Lemma wp_interact: forall binds action arges t m l post,
@@ -401,22 +308,6 @@ Section WeakestPrecondition.
     Qed.
   End WithFunctionList2.
 
-  (* without NoDup assumption, but probably doesn't hold *)
-  Lemma wp_call{env_ok: map.ok env}: forall fs binds fname arges t m l post,
-      (exists args, dexprs m l arges args /\
-       call' fs 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' fs (cmd.call binds fname arges) t m l post.
-  Proof.
-    intros. destruct H as (args & Hargs & H).
-    constructor. rewrite map__of_list_ignores_head_prio_dedup. eapply invert_cmd'.
-    eapply (wp_call0 _ (env_ok := env_ok)).
-    1: eapply NoDup_head_prio_dedup.
-    eexists. split. 1: eassumption.
-    eapply call'_ignores_head_prio_dedup. assumption.
-  Qed.
-
   Section WithFunctions.
     Context (call : String.string -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
     Definition cmd_body (rec:_->_->_->_->_->Prop) (c : cmd) (t : trace) (m : mem) (l : locals)

From b98be1f7eab54e0e11349709cfda0c479f3e38fa Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Tue, 25 Jul 2023 22:17:22 -0400
Subject: [PATCH 3/8] convert from "fs everywhere" to "env everywhere"

---
 bedrock2/src/bedrock2/WeakestPrecondition.v | 62 +++------------------
 1 file changed, 8 insertions(+), 54 deletions(-)

diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index e45fe7926..f4cd7ac80 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -101,44 +101,16 @@ Section WeakestPrecondition.
   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).
 
-  (* TODO move *)
-  Lemma map__invert_get_of_list{env_ok: map.ok env}: forall ksvs k v,
-      map.get (map.of_list (map := env) ksvs) k = Some v ->
-      List.In k (List.map fst ksvs).
-  Proof.
-    induction ksvs; cbn; intros.
-    - rewrite map.get_empty in H. discriminate H.
-    - destruct a as (k' & v'). rewrite Properties.map.get_put_dec in H.
-      destr.destr (String.eqb k' k).
-      + left. reflexivity.
-      + right. eapply IHksvs. eassumption.
-  Qed.
-
-  Lemma exec_cons_env{env_ok: map.ok env}: forall fname fimpl fs c t m l mc post,
-      ~ List.In fname (List.map fst fs) ->
-      exec (map.of_list fs) c t m l mc post ->
-      exec (map.of_list ((fname, fimpl) :: fs)) c t m l mc post.
-  Proof.
-    induction 2; try solve [econstructor; eauto].
-    econstructor; try eassumption.
-    cbn. rewrite map.get_put_diff. 1: eassumption.
-    intro C. subst fname0.
-    apply H.
-    eapply map__invert_get_of_list.
-    eassumption.
-  Qed.
-
-  Section WithFunctionList1.
-    Context (fs: list (String.string * (list String.string * list String.string * cmd))).
+  Section WithFunctionEnv.
+    Context (e: env).
 
     Inductive cmd' (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
       (post : (trace -> mem -> locals -> Prop)) : Prop :=
-    | mk_cmd' (_ : forall mc, exec (map.of_list fs) c t m l mc
-                                (fun t' m' l' mc' => post t' m' l')).
+    | mk_cmd' (_ : forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')).
 
     Lemma invert_cmd': forall c t m l post,
         cmd' c t m l post ->
-        forall mc, exec (map.of_list fs) c t m l mc (fun t' m' l' mc' => post t' m' l').
+        forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l').
     Proof. intros. inversion H. apply H0. Qed.
 
     Definition func' '(innames, outnames, c) (t : trace) (m : mem) (args : list word)
@@ -149,37 +121,19 @@ Section WeakestPrecondition.
         post t m rets)).
 
     Definition call' (fname: String.string) :=
-      match map.get (map.of_list fs) fname with
+      match map.get e fname with
       | Some fimpl => func' fimpl
       | None => fun _ _ _ _ => False
       end.
-  End WithFunctionList1.
 
-  Section Dedup.
-    Context [A: Type] (aeq: A -> A -> bool).
-
-    (* dedup on (x :: xs) with x having a duplicate in xs discards x, whereas
-     head_prio_dedup keeps x but removes its duplicate from xs *)
-    Fixpoint List__head_prio_dedup (xs : list A) : list A :=
-      match xs with
-      | nil => nil
-      | cons h t => let t' := List__head_prio_dedup t in
-                    cons h (List.removeb aeq h t')
-      end.
-  End Dedup.
-
-  Section WithFunctionList2.
     Implicit Type post : trace -> mem -> locals -> Prop.
-    Context (fs: list (String.string * (list String.string * list String.string * cmd))).
-
-    Notation cmd' := (cmd' fs).
 
     Ltac step :=
       match reverse goal with
       | H: _ /\ _ |- _ => destruct H
       | H: exists x, _ |- _ => let n := fresh x in destruct H as [n H]
       | |- _ => progress unfold dlet, dexpr, store in *
-      | H: cmd' _ _ _ _ _ |- _ => pose proof (invert_cmd' _ _ _ _ _ _ H); clear H
+      | H: cmd' _ _ _ _ _ |- _ => pose proof (invert_cmd' _ _ _ _ _ H); clear H
       | |- _ => constructor
       | |- _ => assumption
       | H: forall _: MetricLogging.MetricLog, _ |- _ => apply H
@@ -275,7 +229,7 @@ Section WeakestPrecondition.
 
     Lemma wp_call{env_ok: map.ok env}: forall binds fname arges t m l post,
        (exists args, dexprs m l arges args /\
-        call' fs fname t m args (fun t m rets =>
+        call' 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' (cmd.call binds fname arges) t m l post.
@@ -306,7 +260,7 @@ Section WeakestPrecondition.
       eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
       tac.
     Qed.
-  End WithFunctionList2.
+  End WithFunctionEnv.
 
   Section WithFunctions.
     Context (call : String.string -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).

From 867c49ba219b5721edcb7a2ed02207af51bc8046 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Thu, 27 Jul 2023 20:56:50 -0400
Subject: [PATCH 4/8] instead of unfold1_cmd_goal, eapply
 lemma_corresponding_to_command

In an "env everywhere" setting, where program_logic_goal_for!
adds a (map.get fs fname = Some fimpl) hypothesis.
Surprise #1: There's no case in straightline that handles if-then-else
Surprise #2: unfold1_... tactics are not the only place that depend
on conversion: There also exists a letexists in SPI that turns a
(WP (cmd.cond e _ _) ...) into an (exists v, eval e v /\ ...), and
probably more elsewhere.
---
 bedrock2/src/bedrock2/Loops.v                 |  96 +++++-----
 bedrock2/src/bedrock2/ProgramLogic.v          |  24 ++-
 bedrock2/src/bedrock2/WeakestPrecondition.v   | 176 +++++-------------
 .../bedrock2/WeakestPreconditionProperties.v  | 113 ++---------
 bedrock2/src/bedrock2Examples/SPI.v           |  11 ++
 bedrock2/src/bedrock2Examples/swap_by_add.v   |   2 +-
 6 files changed, 134 insertions(+), 288 deletions(-)

diff --git a/bedrock2/src/bedrock2/Loops.v b/bedrock2/src/bedrock2/Loops.v
index 11950acc1..b36f2896f 100644
--- a/bedrock2/src/bedrock2/Loops.v
+++ b/bedrock2/src/bedrock2/Loops.v
@@ -11,15 +11,12 @@ 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}.
 
   Lemma tailrec_localsmap_1ghost
     {e c t} {m: mem} {l} {post : trace -> mem -> locals -> Prop}
@@ -32,15 +29,16 @@ Section Loops.
     (Hbody: forall v g t m l,
       P v g t m l ->
       exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
+      (word.unsigned br <> 0%Z -> cmd fs c t m l
         (fun t' m' l' => exists v' g',
           P v' g' t' m' l' /\
           lt v' v /\
           (forall t'' m'' l'', Q v' g' t'' m'' l'' -> Q v g t'' m'' l''))) /\
       (word.unsigned br = 0%Z -> Q v g t m l))
     (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.
+    : cmd fs (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 +48,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.
@@ -67,16 +64,17 @@ Section Loops.
     (Hbody: forall v g t m l,
       P v g t m l ->
       exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
+      (word.unsigned br <> 0%Z -> cmd fs c t m l
         (fun t' m' l' => exists v' g',
           P v' g' t' m' l' /\
           lt v' v /\
           (forall t'' m'' l'', Q v' g' t'' m'' l'' -> Q v g t'' m'' l''))) /\
-      (word.unsigned br = 0%Z -> cmd call rest t m l (Q v g)))
-    : cmd call (cmd.seq (cmd.while e c) rest) t m l (Q v0 g0).
+      (word.unsigned br = 0%Z -> cmd fs rest t m l (Q v g)))
+    : cmd fs (cmd.seq (cmd.while e c) rest) t m l (Q v0 g0).
   Proof.
+    eapply wp_seq.
     cbn. eapply tailrec_localsmap_1ghost with
-      (Q := fun v g t m l => cmd call rest t m l (Q v g)).
+      (Q := fun v g t m l => cmd fs rest t m l (Q v g)).
     1: eassumption.
     1: exact Hpre.
     2: intros *; exact id.
@@ -85,14 +83,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 +162,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.
@@ -190,13 +187,13 @@ Section Loops.
       let l := reconstruct variables localstuple in
       exists br, expr m l e (eq br) /\
          (word.unsigned br <> 0 ->
-          cmd call c t m l (fun t m l =>
+          cmd fs c t m l (fun t m l =>
             Markers.unique (Markers.left (tuple.existss (fun localstuple =>
               enforce variables localstuple l /\
               Markers.right (Markers.unique (exists v',
                 tuple.apply (invariant v' t m) localstuple /\ 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 (while_localsmap (fun v t m l =>
       exists localstuple, enforce variables localstuple l /\
@@ -210,7 +207,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).
@@ -234,7 +231,7 @@ Section Loops.
       match tuple.apply (hlist.apply (spec v) g t m) l with S_ =>
       S_.(1) ->
       Markers.unique (Markers.left (exists br, expr m localsmap e (eq br) /\ Markers.right (
-      (word.unsigned br <> 0%Z -> cmd call c t m localsmap
+      (word.unsigned br <> 0%Z -> cmd fs c t m localsmap
         (fun t' m' localsmap' =>
           Markers.unique (Markers.left (hlist.existss (fun l' => enforce variables l' localsmap' /\ Markers.right (
           Markers.unique (Markers.left (hlist.existss (fun g' => exists v',
@@ -244,9 +241,10 @@ Section Loops.
             forall T M, hlist.foralls (fun L => tuple.apply (S'.(2) T M) L -> tuple.apply (S_.(2) T M) L)) end))))))))) /\
       (word.unsigned br = 0%Z -> tuple.apply (S_.(2) t m) l))))end))))
     (Hpost : match (tuple.apply (hlist.apply (spec v0) g0 t m) l0).(2) with Q0 => forall t m, hlist.foralls (fun l =>  tuple.apply (Q0 t m) l -> post t m (reconstruct variables l))end)
-    , cmd call (cmd.while e c) t m localsmap post ).
+    , cmd fs (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 +257,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).
@@ -279,7 +276,7 @@ Section Loops.
       let S := spec v t m l in let (P, Q) := S in
       P ->
       exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
+      (word.unsigned br <> 0%Z -> cmd fs c t m l
         (fun t' m' l' => exists v',
           let S' := spec v' t' m' l' in let '(P', Q') := S' in
           P' /\
@@ -287,8 +284,9 @@ Section Loops.
           forall T M L, Q' T M L -> Q T M L)) /\
       (word.unsigned br = 0%Z -> Q t m l))
     (Hpost : forall t m l, Q0 t m l -> 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, (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 +297,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.
@@ -328,12 +325,13 @@ Section Loops.
     (Henter : exists br, expr m l e (eq br) /\ (word.unsigned br = 0%Z -> post t m l))
     (v0 : measure) (Hpre : invariant v0 t m l)
     (Hbody : forall v t m l, invariant v t m l ->
-       cmd call c t m l (fun t m l =>
+       cmd fs c t m l (fun t m l =>
          exists br, expr m l e (eq br) /\
          (word.unsigned br <> 0 -> 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 (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 +347,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.
@@ -374,7 +372,7 @@ Section Loops.
       let S := spec v t m l in let (P, Q) := S in
       P ->
       exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
+      (word.unsigned br <> 0%Z -> cmd fs c t m l
         (fun t' m' l' =>
           (exists br, expr m' l' e (eq br) /\ word.unsigned br = 0 /\ Q t' m' l') \/
           exists v', let S' := spec v' t' m' l' in let '(P', Q') := S' in
@@ -383,8 +381,9 @@ Section Loops.
           forall T M L, Q' T M L -> Q T M L)) /\
       (word.unsigned br = 0%Z -> Q t m l))
     (Hpost : forall t m l, Q0 t m l -> 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 (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 +398,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.
@@ -423,7 +421,7 @@ Section Loops.
       match tuple.apply (hlist.apply (spec v) g t m) l with S_ =>
       S_.(1) ->
       Markers.unique (Markers.left (exists br, expr m localsmap e (eq br) /\ Markers.right (
-      (word.unsigned br <> 0%Z -> cmd call c t m localsmap
+      (word.unsigned br <> 0%Z -> cmd fs c t m localsmap
         (fun t' m' localsmap' =>
           Markers.unique (Markers.left (hlist.existss (fun l' => enforce variables l' localsmap' /\ Markers.right (
           Markers.unique (Markers.left (exists br, expr m' localsmap' e (eq br) /\ Markers.right ( word.unsigned br = 0 /\ tuple.apply (S_.(2) t' m') l') ) ) \/
@@ -434,9 +432,10 @@ Section Loops.
             forall T M, hlist.foralls (fun L => tuple.apply (S'.(2) T M) L -> tuple.apply (S_.(2) T M) L)) end))))))))) /\
       (word.unsigned br = 0%Z -> tuple.apply (S_.(2) t m) l))))end))))
     (Hpost : match (tuple.apply (hlist.apply (spec v0) g0 t m) l0).(2) with Q0 => forall t m, hlist.foralls (fun l =>  tuple.apply (Q0 t m) l -> post t m (reconstruct variables l))end)
-    , cmd call (cmd.while e c) t m localsmap post ).
+    , cmd fs (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 +454,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].
@@ -480,11 +478,11 @@ Section Loops.
     (v0 : measure) (Hpre : tuple.apply (invariant v0 t m) localstuple)
     (Hbody : forall v t m, tuple.foralls (fun localstuple =>
       tuple.apply (invariant v t m) localstuple ->
-       cmd call c t m (reconstruct variables localstuple) (fun t m l =>
+       cmd fs c t m (reconstruct variables localstuple) (fun t m l =>
          exists br, expr m l e (eq br) /\
          (word.unsigned br <> 0 -> Markers.unique (Markers.left (tuple.existss (fun localstuple => enforce variables localstuple l /\ Markers.right (Markers.unique (exists v', tuple.apply (invariant v' t m) localstuple /\ 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 (atleastonce_localsmap (fun v t m l => exists localstuple, Logic.and (enforce variables localstuple l) (tuple.apply (invariant v t m) localstuple))); eauto.
     intros vi ti mi li (?&X&Y).
@@ -492,7 +490,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.
@@ -504,7 +502,7 @@ Section Loops.
   Lemma while_zero_iterations {e c t l} {m : mem} {post : _->_->_-> Prop}
     (HCond: expr m l e (eq (word.of_Z 0)))
     (HPost: 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 (while_localsmap (fun n t' m' l' => t' = t /\ m' = m /\ l' = l) (PeanoNat.Nat.lt_wf 0) 0%nat).
     1: unfold split; auto. intros *. intros (? & ? & ?). subst.
@@ -525,14 +523,15 @@ Section Loops.
     (Hpre : (P v0 t l * R0) m)
     (Hbody : forall v t m l R, (P v t l * R) m ->
       exists br, expr m l e (eq br) /\
-      (word.unsigned br <> 0%Z -> cmd call c t m l
+      (word.unsigned br <> 0%Z -> cmd fs c t m l
         (fun t' m' l' => exists v' dR, (P v' t' l' * (R * dR)) m' /\
           lt v' v /\
           forall T L, Q v' T L * dR ==> Q v T L)) /\
       (word.unsigned br = 0%Z -> (Q v t l * R) m))
     (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.
+    : cmd fs (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 +540,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/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index b0a5b6e63..a40d8f4bc 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) := 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 : env, 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.
 
@@ -228,13 +229,16 @@ Ltac straightline :=
   match goal with
   | _ => 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;
+    enter f;
+    cbv beta delta [call];
+    lazymatch goal with
+    | H: map.get ?functions ?fname = Some _ |- context[map.get ?functions ?fname] =>
+        rewrite H; clear H
+    end;
+    intros;
     cbv match beta delta [WeakestPrecondition.func]
   | |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
-    unfold1_cmd_goal; cbv beta match delta [cmd_body];
+    eapply wp_set;
     let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in
     ident_of_constr_string_cps s ltac:(fun x =>
       ensure_free x;
@@ -246,7 +250,7 @@ Ltac straightline :=
     | cmd.while _ _ => fail
     | cmd.cond _ _ _ => fail
     | cmd.interact _ _ _ => fail
-    | _ => unfold1_cmd_goal; cbv beta match delta [cmd_body]
+    | _ => apply_rule_for_command c
     end
   | |- @list_map _ _ (get _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
   | |- @list_map _ _ (expr _ _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index f4cd7ac80..6287c8a61 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -2,10 +2,15 @@ Require Import coqutil.Macros.subst coqutil.Macros.unique coqutil.Map.Interface
 Require Import Coq.ZArith.BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import coqutil.dlet bedrock2.Syntax bedrock2.Semantics.
 
+Require Import coqutil.Map.Interface.
+Require coqutil.Map.SortedListString.
+
+#[export] Instance env: map.map String.string (list String.string * list String.string * Syntax.cmd.cmd) := SortedListString.map _.
+#[export] Instance env_ok: map.ok env := SortedListString.ok _.
+
 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).
 
@@ -104,25 +109,25 @@ Section WeakestPrecondition.
   Section WithFunctionEnv.
     Context (e: env).
 
-    Inductive cmd' (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
+    Inductive cmd (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
       (post : (trace -> mem -> locals -> Prop)) : Prop :=
-    | mk_cmd' (_ : forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')).
+    | mk_cmd (_ : forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')).
 
-    Lemma invert_cmd': forall c t m l post,
-        cmd' c t m l post ->
+    Lemma invert_cmd: forall c t m l post,
+        cmd c t m l post ->
         forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l').
     Proof. intros. inversion H. apply H0. Qed.
 
-    Definition func' '(innames, outnames, c) (t : trace) (m : mem) (args : list word)
+    Definition func '(innames, outnames, c) (t : trace) (m : mem) (args : list word)
       (post : trace -> mem -> list word -> Prop) :=
       exists l, map.of_list_zip innames args = Some l /\
-      cmd' c t m l (fun t m l =>
+      cmd c t m l (fun t m l =>
         list_map (get l) outnames (fun rets =>
         post t m rets)).
 
-    Definition call' (fname: String.string) :=
+    Definition call (fname: String.string) :=
       match map.get e fname with
-      | Some fimpl => func' fimpl
+      | Some fimpl => func fimpl
       | None => fun _ _ _ _ => False
       end.
 
@@ -133,7 +138,7 @@ Section WeakestPrecondition.
       | H: _ /\ _ |- _ => destruct H
       | H: exists x, _ |- _ => let n := fresh x in destruct H as [n H]
       | |- _ => progress unfold dlet, dexpr, store in *
-      | H: cmd' _ _ _ _ _ |- _ => pose proof (invert_cmd' _ _ _ _ _ H); clear H
+      | H: cmd _ _ _ _ _ |- _ => pose proof (invert_cmd _ _ _ _ _ H); clear H
       | |- _ => constructor
       | |- _ => assumption
       | H: forall _: MetricLogging.MetricLog, _ |- _ => apply H
@@ -146,20 +151,20 @@ Section WeakestPrecondition.
       end.
     Ltac tac := repeat step.
 
-    Lemma wp_skip: forall t m l post, post t m l -> cmd' cmd.skip t m l post.
+    Lemma wp_skip: forall t m l post, post t m l -> cmd cmd.skip t m l post.
     Proof. tac. Qed.
 
     Lemma wp_set: forall x ev t m l post,
         (exists v, dexpr m l ev v /\
         dlet! l := map.put l x v in
         post t m l) ->
-        cmd' (cmd.set x ev) t m l post.
+        cmd (cmd.set x ev) t m l post.
     Proof. tac. Qed.
 
     Lemma wp_unset: forall x t m l post,
         (dlet! l := map.remove l x in
          post t m l) ->
-        cmd' (cmd.unset x) t m l post.
+        cmd (cmd.unset x) t m l post.
     Proof. tac. Qed.
 
     Lemma wp_store: forall sz ea ev t m l post,
@@ -167,7 +172,7 @@ Section WeakestPrecondition.
         exists v, dexpr m l ev v /\
         store sz m a v (fun m =>
         post t m l)) ->
-       cmd' (cmd.store sz ea ev) t m l post.
+       cmd (cmd.store sz ea ev) t m l post.
     Proof. tac. Qed.
 
     Lemma wp_stackalloc: forall x n c t m l post,
@@ -175,18 +180,18 @@ Section WeakestPrecondition.
         forall a mStack mCombined,
           anybytes a n mStack -> map.split mCombined m mStack ->
           dlet! l := map.put l x a in
-          cmd' c t mCombined l (fun t' mCombined' l' =>
+          cmd c t mCombined l (fun t' mCombined' l' =>
           exists m' mStack',
           anybytes a n mStack' /\ map.split mCombined' m' mStack' /\
           post t' m' l')) ->
-          cmd' (cmd.stackalloc x n c) t m l post.
+          cmd (cmd.stackalloc x n c) t m l post.
     Proof. tac. specialize H0 with (1 := H1) (2 := H2). tac. Qed.
 
     Lemma wp_cond: forall br ct cf t m l post,
         (exists v, dexpr m l br v /\
-        (word.unsigned v <> 0%Z -> cmd' ct t m l post) /\
-        (word.unsigned v = 0%Z -> cmd' cf t m l post)) ->
-        cmd' (cmd.cond br ct cf) t m l post.
+        (word.unsigned v <> 0%Z -> cmd ct t m l post) /\
+        (word.unsigned v = 0%Z -> cmd cf t m l post)) ->
+        cmd (cmd.cond br ct cf) t m l post.
     Proof.
       tac. destr.destr (Z.eqb (word.unsigned v0) 0).
       - specialize H1 with (1 := E). tac.
@@ -194,8 +199,8 @@ Section WeakestPrecondition.
     Qed.
 
     Lemma wp_seq: forall c1 c2 t m l post,
-        cmd' c1 t m l (fun t m l => cmd' c2 t m l post) ->
-        cmd' (cmd.seq c1 c2) t m l post.
+        cmd c1 t m l (fun t m l => cmd c2 t m l post) ->
+        cmd (cmd.seq c1 c2) t m l post.
     Proof.
       tac. eapply exec.weaken.
       { econstructor. 1: eapply H0. tac. }
@@ -208,10 +213,10 @@ Section WeakestPrecondition.
         (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' c t m l (fun t' m l =>
+          (word.unsigned b <> 0%Z -> cmd 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' (cmd.while e c) t m l post.
+       cmd (cmd.while e c) t m l post.
     Proof.
       intros. destruct H as (measure & lt & inv & Hwf & HInit & Hbody).
       destruct HInit as (v0 & HInit).
@@ -227,19 +232,19 @@ Section WeakestPrecondition.
         cbv beta. intros * (v' & HInv & HLt). eauto.
     Qed.
 
-    Lemma wp_call{env_ok: map.ok env}: forall binds fname arges t m l post,
+    Lemma wp_call: forall binds fname arges t m l post,
        (exists args, dexprs m l arges args /\
-        call' fname t m args (fun t m rets =>
+        call 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' (cmd.call binds fname arges) t m l post.
+       cmd (cmd.call binds fname arges) t m l post.
     Proof.
       tac.
       unfold dexprs in *.
       eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
-      unfold call' in *.
+      unfold call in *.
       Tactics.destruct_one_match_hyp. 2: contradiction.
-      unfold func' in *.
+      unfold func in *.
       destruct p as ((argnames & retnames) & fbody).
       destruct H0 as (l1 & Hl1 & Hbody).
       inversion Hbody. clear Hbody. rename H into Hbody.
@@ -254,105 +259,28 @@ Section WeakestPrecondition.
           exists l', map.putmany_of_list_zip binds rets l = Some l' /\
           forall m', map.split m' mKeep mReceive ->
           post (cons ((mGive, action, args), (mReceive, rets)) t) m' l')) ->
-       cmd' (cmd.interact binds action arges) t m l post.
+       cmd (cmd.interact binds action arges) t m l post.
     Proof.
       tac.
       eapply exprs_sound in H. destruct H as (argvs & mc' & HEv & ?). subst argvs.
       tac.
     Qed.
   End WithFunctionEnv.
-
-  Section WithFunctions.
-    Context (call : String.string -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
-    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 *)
-      match c with
-      | cmd.skip => post t m l
-      | cmd.set x ev =>
-        exists v, dexpr m l ev v /\
-        dlet! l := map.put l x v in
-        post t m l
-      | cmd.unset x =>
-        dlet! l := map.remove l x in
-        post t m l
-      | cmd.store sz ea ev =>
-        exists a, dexpr m l ea a /\
-        exists v, dexpr m l ev v /\
-        store sz m a v (fun m =>
-        post t m l)
-      | cmd.stackalloc x n c =>
-        Z.modulo n (bytes_per_word width) = 0 /\
-        forall a mStack mCombined,
-          anybytes a n mStack -> map.split mCombined m mStack ->
-          dlet! l := map.put l x a in
-          rec c t mCombined l (fun t' mCombined' l' =>
-          exists m' mStack',
-          anybytes a n mStack' /\ map.split mCombined' m' mStack' /\
-          post t' m' l')
-      | cmd.cond br ct cf =>
-        exists v, dexpr m l br v /\
-        (word.unsigned v <> 0%Z -> rec ct t m l post) /\
-        (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.call binds fname arges =>
-        exists args, dexprs m l arges args /\
-        call 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 =>
-        exists args, dexprs m l arges args /\
-        exists mKeep mGive, map.split m mKeep mGive /\
-        ext_spec t mGive action args (fun mReceive rets =>
-          exists l', map.putmany_of_list_zip binds rets l = Some l' /\
-          forall m', map.split m' mKeep mReceive ->
-          post (cons ((mGive, action, args), (mReceive, rets)) t) m' l')
-      end.
-    Fixpoint cmd c := cmd_body cmd c.
-  End WithFunctions.
-
-  Definition func call '(innames, outnames, c) (t : trace) (m : mem) (args : list word) (post : trace -> mem -> list word -> Prop) :=
-      exists l, map.of_list_zip innames args = Some l /\
-      cmd call c t m l (fun t m l =>
-        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.
 End WeakestPrecondition.
 
-Ltac unfold1_cmd e :=
-  lazymatch e with
-    @cmd ?width ?BW ?word ?mem ?locals ?ext_spec ?CA ?c ?t ?m ?l ?post =>
-    let c := eval hnf in c in
-    constr:(@cmd_body width BW word mem locals ext_spec CA
-                      (@cmd width BW word mem locals ext_spec CA) c t m l post)
+Ltac apply_rule_for_command c :=
+  lazymatch c with
+  | cmd.skip => eapply wp_skip
+  | cmd.set ?x ?ev => eapply wp_set
+  | cmd.unset ?x => eapply wp_unset
+  | cmd.store ?sz ?ea ?ev => eapply wp_store
+  | cmd.stackalloc ?x ?n ?c => eapply wp_stackalloc
+  | cmd.cond ?br ?ct ?cf => eapply wp_cond
+  | cmd.seq ?c1 ?c2 => eapply wp_seq
+  | cmd.while ?e ?c => eapply wp_while
+  | cmd.call ?binds ?fname ?arges => eapply wp_call
+  | cmd.interact ?binds ?action ?arges => eapply wp_interact
   end.
-Ltac unfold1_cmd_goal :=
-  let G := lazymatch goal with |- ?G => G end in
-  let G := unfold1_cmd G in
-  change G.
 
 Ltac unfold1_expr e :=
   lazymatch e with
@@ -376,18 +304,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..e67b30da0 100644
--- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
@@ -74,14 +74,15 @@ Section WeakestPrecondition.
 
   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.
+     Basics.impl))))))) WeakestPrecondition.cmd.
   Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Admitted. (*
     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.
@@ -136,18 +137,19 @@ Section WeakestPrecondition.
         split; [assumption|].
         eapply Semantics.ext_spec.weaken; [|solve[eassumption]].
         intros ? ? (?&?&?); eauto 10. } }
-  Qed.
+  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 _ (pointwise_relation _ Basics.impl))) ==>
-     Basics.impl)))))) WeakestPrecondition.func.
+     Basics.impl))))))) WeakestPrecondition.func.
   Proof using word_ok mem_ok locals_ok ext_spec_ok env_ok.
+  Admitted. (*
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func]; intros.
     destruct a. destruct p.
     destruct H1; intuition idtac.
@@ -165,7 +167,7 @@ Section WeakestPrecondition.
         cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
         eauto.
     - eauto.
-  Qed.
+  Qed. *)
 
   Global Instance Proper_call :
     Proper (
@@ -177,6 +179,7 @@ Section WeakestPrecondition.
      (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.
+  Admitted. (*
     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.
@@ -184,27 +187,7 @@ Section WeakestPrecondition.
     eapply Proper_func;
       cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
       eauto.
-  Qed.
-
-  Global Instance Proper_program :
-    Proper (
-     pointwise_relation _ (
-     pointwise_relation _ (
-     pointwise_relation _ (
-     pointwise_relation _ (
-     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.
-    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.
+  Qed. *)
 
   Ltac t :=
       repeat match goal with
@@ -293,77 +276,10 @@ 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').
-  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. }
-    { eapply sound_args in H; t. }
-  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 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 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').
-  Proof.
-    eapply sound_cmd'';
-      try eapply Properties.map.all_gets_from_map_of_NoDup_list; eauto.
-  Qed.
+    (H : WeakestPrecondition.cmd fs c t m l post)
+    : Semantics.exec fs c t m l mc (fun t' m' l' mc' => post t' m' l').
+  Proof. eapply WeakestPrecondition.invert_cmd. exact H. Qed.
 
   (** Ad-hoc lemmas here? *)
 
@@ -376,6 +292,7 @@ Section WeakestPrecondition.
            post (cons (map.empty, binds, args, (map.empty, rets)) t) m l0))
     : WeakestPrecondition.cmd call (cmd.interact action binds arges) t m l post.
   Proof using word_ok mem_ok ext_spec_ok.
+  Admitted. (*
     exists args; split; [exact Hargs|].
     exists m.
     exists map.empty.
@@ -383,7 +300,7 @@ Section WeakestPrecondition.
     eapply ext_spec.weaken; [|eapply Hext]; intros ? ? [? [? []]]. subst a; subst.
     eexists; split; [eassumption|].
     intros. eapply Properties.map.split_empty_r in H. subst. assumption.
-  Qed.
+  Qed. *)
 
   Lemma intersect_expr: forall m l e (post1 post2: word -> Prop),
       WeakestPrecondition.expr m l e post1 ->
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/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. *)

From 36882d9842a42da4d09788750ac98be607e9042a Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Fri, 28 Jul 2023 20:30:52 -0400
Subject: [PATCH 5/8] wip "env everywhere" approach

---
 bedrock2/src/bedrock2/ProgramLogic.v            |  4 ++--
 bedrock2/src/bedrock2/WeakestPrecondition.v     | 17 +++++++++++------
 .../bedrock2/WeakestPreconditionProperties.v    |  9 +++------
 .../src/bedrock2Examples/FE310CompilerDemo.v    |  4 ++--
 .../bedrock2Examples/indirect_add_heapletwise.v |  6 ++++--
 bedrock2/src/bedrock2Examples/memconst.v        | 11 ++++++-----
 bedrock2/src/bedrock2Examples/swap.v            |  2 +-
 7 files changed, 29 insertions(+), 24 deletions(-)

diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index a40d8f4bc..378a28054 100644
--- a/bedrock2/src/bedrock2/ProgramLogic.v
+++ b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -56,7 +56,7 @@ 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 : env, map.get functions fname = Some proc -> ltac:(
+  exact (forall (functions : @map.rep _ _ 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 functions) in
     exact s))).
@@ -238,7 +238,7 @@ Ltac straightline :=
     intros;
     cbv match beta delta [WeakestPrecondition.func]
   | |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
-    eapply wp_set;
+    unfold1_cmd_goal;
     let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in
     ident_of_constr_string_cps s ltac:(fun x =>
       ensure_free x;
diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index 6287c8a61..b8468911b 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -5,7 +5,7 @@ Require Import coqutil.dlet bedrock2.Syntax bedrock2.Semantics.
 Require Import coqutil.Map.Interface.
 Require coqutil.Map.SortedListString.
 
-#[export] Instance env: map.map String.string (list String.string * list String.string * Syntax.cmd.cmd) := SortedListString.map _.
+#[export] Instance env: map.map String.string Syntax.func := SortedListString.map _.
 #[export] Instance env_ok: map.ok env := SortedListString.ok _.
 
 Section WeakestPrecondition.
@@ -56,13 +56,13 @@ Section WeakestPrecondition.
       | _ => progress cbn in *
       end; eauto.
 
-  Lemma expr_sound: forall m l e mc post (H : WeakestPrecondition.expr m l e post),
+  Lemma expr_sound: forall m l e mc post (H : expr m l e post),
     exists v mc', Semantics.eval_expr m l e mc = Some (v, mc') /\ post v.
   Proof.
     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 IHe in H; t. cbv [load] in H0; t. rewrite H. rewrite H0. eauto. }
+    { eapply IHe in H; t. cbv [load] in H0; t. rewrite H. rewrite H0. eauto. }
     { eapply IHe1 in H; t. eapply IHe2 in H0; t. rewrite H, H0; eauto. }
     { eapply IHe1 in H; t. rewrite H. Tactics.destruct_one_match.
       { eapply IHe3 in H0; t. }
@@ -98,7 +98,7 @@ Section WeakestPrecondition.
   Proof.
     cbv [map.getmany_of_list].
     induction a; cbn; repeat (subst; t).
-    cbv [WeakestPrecondition.get] in H; t.
+    cbv [get] in H; t.
     epose proof (IHa _ _ H0); clear IHa; t.
     rewrite H. erewrite H1. eexists; split; eauto.
   Qed.
@@ -245,7 +245,7 @@ Section WeakestPrecondition.
       unfold call in *.
       Tactics.destruct_one_match_hyp. 2: contradiction.
       unfold func in *.
-      destruct p as ((argnames & retnames) & fbody).
+      destruct f as ((argnames & retnames) & fbody).
       destruct H0 as (l1 & Hl1 & Hbody).
       inversion Hbody. clear Hbody. rename H into Hbody.
       eapply exec.call; eauto.
@@ -282,6 +282,11 @@ Ltac apply_rule_for_command c :=
   | cmd.interact ?binds ?action ?arges => eapply wp_interact
   end.
 
+Ltac unfold1_cmd_goal :=
+  lazymatch goal with
+  | |- cmd _ ?c _ _ _ ?post => let c := eval hnf in c in apply_rule_for_command c
+  end.
+
 Ltac unfold1_expr e :=
   lazymatch e with
     @expr ?width ?word ?mem ?locals ?m ?l ?arg ?post =>
diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
index e67b30da0..29ffd9017 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,7 +67,6 @@ 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 :
@@ -81,7 +78,7 @@ Section WeakestPrecondition.
      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.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
   Admitted. (*
     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).
@@ -148,7 +145,7 @@ Section WeakestPrecondition.
      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.
+  Proof using word_ok mem_ok locals_ok ext_spec_ok.
   Admitted. (*
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func]; intros.
     destruct a. destruct p.
@@ -178,7 +175,7 @@ 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.
+  Proof using word_ok mem_ok locals_ok ext_spec_ok.
   Admitted. (*
     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).
diff --git a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
index d5ad2241c..ad4135054 100644
--- a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
+++ b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
@@ -158,7 +158,7 @@ Local Instance mapok: map.ok mem := SortedListWord.ok Naive.word32 _.
 Local Instance wordok: word.ok word := Naive.word32_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.
@@ -242,7 +242,7 @@ 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.
diff --git a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
index d6f8e2334..788588e65 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.
   *)
 
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/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. *)

From 36780ed3db16e9d9a4830bfbc125024a30784450 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Fri, 28 Jul 2023 20:37:07 -0400
Subject: [PATCH 6/8] make the new `cmd` opaque to `hnf` and `repeat split`

---
 bedrock2/src/bedrock2/WeakestPrecondition.v   | 71 +++++++++++++++----
 .../bedrock2/WeakestPreconditionProperties.v  |  2 +-
 2 files changed, 59 insertions(+), 14 deletions(-)

diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index b8468911b..2c0fa80bf 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -8,7 +8,7 @@ Require coqutil.Map.SortedListString.
 #[export] Instance env: map.map String.string Syntax.func := SortedListString.map _.
 #[export] Instance env_ok: map.ok env := SortedListString.ok _.
 
-Section WeakestPrecondition.
+Section WeakestPreconditionExprs.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
   Context {ext_spec: ExtSpec}.
@@ -105,18 +105,62 @@ Section WeakestPrecondition.
 
   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).
-
-  Section WithFunctionEnv.
-    Context (e: env).
-
-    Inductive cmd (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
+End WeakestPreconditionExprs.
+
+(* We need to make `cmd` opaque to `hnf` (unfolds any definition, so a plain
+   definition doesn't work) and to `repeat split` (applies constructors of all
+   1-constructor inductives, so a 1-constructor inductive wrapping exec doesn't
+   work). *)
+Module Type cmd_SIG.
+  Section WithParams.
+    Context {width: Z} {BW: Bitwidth width} {word: word.word width}
+      {mem: map.map word Byte.byte}
+      {locals: map.map String.string word}.
+
+    Parameter cmd : forall {ext_spec: ExtSpec} (e: env),
+        Syntax.cmd -> trace -> mem -> locals ->
+        (trace -> mem -> locals -> Prop) -> Prop.
+    Parameter mk : forall {ext_spec: ExtSpec} (e: env) c t m l post,
+        (forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')) ->
+        cmd e c t m l post.
+    Parameter invert: forall {ext_spec: ExtSpec} [e c t m l post],
+        cmd e c t m l post ->
+        forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l').
+  End WithParams.
+End cmd_SIG.
+
+Module cmd : cmd_SIG.
+  Section WithParams.
+    Context {width: Z} {BW: Bitwidth width} {word: word.word width}
+      {mem: map.map word Byte.byte}
+      {locals: map.map String.string word}
+      {ext_spec: ExtSpec}
+      (e: env).
+
+    Definition cmd (c : Syntax.cmd) (t : trace) (m : mem) (l : locals)
       (post : (trace -> mem -> locals -> Prop)) : Prop :=
-    | mk_cmd (_ : forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')).
+      (forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')).
+
+    Lemma mk c t m l post:
+      (forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l')) ->
+      cmd c t m l post.
+    Proof. exact id. Qed.
 
-    Lemma invert_cmd: forall c t m l post,
+    Lemma invert c t m l post:
         cmd c t m l post ->
         forall mc, exec e c t m l mc (fun t' m' l' mc' => post t' m' l').
-    Proof. intros. inversion H. apply H0. Qed.
+    Proof. exact id. Qed.
+  End WithParams.
+End cmd.
+Notation cmd := cmd.cmd.
+
+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 {ext_spec: ExtSpec}.
+
+  Section WithFunctionEnv.
+    Context (e: env). Notation cmd := (cmd e).
 
     Definition func '(innames, outnames, c) (t : trace) (m : mem) (args : list word)
       (post : trace -> mem -> list word -> Prop) :=
@@ -138,7 +182,8 @@ Section WeakestPrecondition.
       | H: _ /\ _ |- _ => destruct H
       | H: exists x, _ |- _ => let n := fresh x in destruct H as [n H]
       | |- _ => progress unfold dlet, dexpr, store in *
-      | H: cmd _ _ _ _ _ |- _ => pose proof (invert_cmd _ _ _ _ _ H); clear H
+      | H: cmd _ _ _ _ _ |- _ => pose proof (cmd.invert H); clear H
+      | |- cmd _ _ _ _ _ => apply cmd.mk
       | |- _ => constructor
       | |- _ => assumption
       | H: forall _: MetricLogging.MetricLog, _ |- _ => apply H
@@ -220,14 +265,14 @@ Section WeakestPrecondition.
     Proof.
       intros. destruct H as (measure & lt & inv & Hwf & HInit & Hbody).
       destruct HInit as (v0 & HInit).
-      econstructor. intros.
+      apply cmd.mk. intros.
       revert t m l mc 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' & mc' & 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). inversion Ht. clear Ht.
+      - specialize Ht with (1 := E). eapply cmd.invert in Ht.
         eapply exec.while_true; eauto.
         cbv beta. intros * (v' & HInv & HLt). eauto.
     Qed.
@@ -247,7 +292,7 @@ Section WeakestPrecondition.
       unfold func in *.
       destruct f as ((argnames & retnames) & fbody).
       destruct H0 as (l1 & Hl1 & Hbody).
-      inversion Hbody. clear Hbody. rename H into Hbody.
+      eapply cmd.invert in Hbody.
       eapply exec.call; eauto.
       cbv beta. intros. eapply getmany_sound. assumption.
     Qed.
diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
index 29ffd9017..fdf948ba8 100644
--- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
@@ -276,7 +276,7 @@ Section WeakestPrecondition.
   Lemma sound_cmd fs c t m l mc post
     (H : WeakestPrecondition.cmd fs c t m l post)
     : Semantics.exec fs c t m l mc (fun t' m' l' mc' => post t' m' l').
-  Proof. eapply WeakestPrecondition.invert_cmd. exact H. Qed.
+  Proof. eapply WeakestPrecondition.cmd.invert. exact H. Qed.
 
   (** Ad-hoc lemmas here? *)
 

From 978d785a57a925d5d80753905f2284ca49e4b438 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Fri, 28 Jul 2023 20:38:58 -0400
Subject: [PATCH 7/8] trying to pretend the new `cmd` is unfoldable by

sneaking an `apply_rules_until_propositional` call into
`letexists`, `eexists`, `esplit`, and inserting `unfold1_cmd_goal`
where still needed.
Gave up on memmove because it seems too hard to simulate a `cbn`
that happens under exists and ands by applying wp rules under
these exists and ands.
---
 bedrock2/src/bedrock2/ProgramLogic.v          |  9 ++++++++
 .../src/bedrock2Examples/ARPResponderProofs.v |  6 ++---
 .../src/bedrock2Examples/FE310CompilerDemo.v  |  9 +++++++-
 bedrock2/src/bedrock2Examples/FlatConstMem.v  |  1 -
 bedrock2/src/bedrock2Examples/LAN9250.v       |  8 ++++++-
 bedrock2/src/bedrock2Examples/SPI.v           | 12 ----------
 bedrock2/src/bedrock2Examples/bsearch.v       |  2 +-
 bedrock2/src/bedrock2Examples/indirect_add.v  |  2 +-
 .../indirect_add_heapletwise.v                |  2 +-
 bedrock2/src/bedrock2Examples/insertionsort.v |  2 +-
 bedrock2/src/bedrock2Examples/ipow.v          |  2 +-
 bedrock2/src/bedrock2Examples/lightbulb.v     |  2 +-
 bedrock2/src/bedrock2Examples/memconst.v      |  2 +-
 bedrock2/src/bedrock2Examples/memequal.v      |  3 ++-
 bedrock2/src/bedrock2Examples/memmove.v       | 23 ++++++++++++++++---
 bedrock2/src/bedrock2Examples/memswap.v       |  2 +-
 bedrock2/src/bedrock2Examples/rpmul.v         |  2 +-
 bedrock2/src/bedrock2Examples/stackalloc.v    |  2 +-
 bedrock2/src/bedrock2Examples/swap.v          |  2 +-
 bedrock2/src/bedrock2Examples/swap_by_add.v   |  2 +-
 deps/coqutil                                  |  2 +-
 21 files changed, 62 insertions(+), 35 deletions(-)

diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index 378a28054..08f8c9ceb 100644
--- a/bedrock2/src/bedrock2/ProgramLogic.v
+++ b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -347,6 +347,15 @@ Ltac straightline_call :=
       [ .. | intros ? ? ? ?]
   end.
 
+(* not as eager as it might look, because each rule only has one premise,
+   and it is of the form (_ /\ _) or (exists _, _),
+   except wp_seq, which has another cmd as its premise, but there, we
+   indeed want to unfold the head cmd again *)
+Ltac apply_rules_until_propositional := repeat unfold1_cmd_goal.
+
+Export coqutil.Tactics.letexists.
+Ltac expose_exists_for_letexists ::= hnf; apply_rules_until_propositional.
+
 Ltac current_trace_mem_locals :=
   lazymatch goal with
   | |- WeakestPrecondition.cmd _  _ ?t ?m ?l _ => constr:((t, m, l))
diff --git a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
index 008081c0a..a796b5c23 100644
--- a/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
+++ b/bedrock2/src/bedrock2Examples/ARPResponderProofs.v
@@ -10,7 +10,7 @@ Import Datatypes List ListNotations.
 Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope Z_scope.
 
 From bedrock2 Require Import Array Scalars Separation.
-From coqutil.Tactics Require Import letexists rdelta.
+From coqutil.Tactics Require Import rdelta.
 Local Notation bytes := (array scalar8 (word.of_Z 1)).
 
 Ltac seplog_use_array_load1 H i :=
@@ -29,8 +29,8 @@ Local Instance spec_of_arp : spec_of "arp" := fun functions =>
 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.
+  WeakestPrecondition.unfold1_cmd_goal.
   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 ad4135054..f1e65097d 100644
--- a/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
+++ b/bedrock2/src/bedrock2Examples/FE310CompilerDemo.v
@@ -126,7 +126,8 @@ From coqutil Require Import Z.div_mod_to_equations.
 
 Ltac t :=
   match goal with
-  | |- WeakestPrecondition.cmd _ (cmd.interact _ _ _) _ _ _ _ => eexists; split; [solve[repeat straightline]|]
+  | |- WeakestPrecondition.cmd _ (cmd.interact _ _ _) _ _ _ _ =>
+      WeakestPrecondition.unfold1_cmd_goal; eexists; split; [solve[repeat straightline]|]
   | |- map.split _ _ _ => eapply Properties.map.split_empty_r; reflexivity
   | H: map.of_list_zip ?ks ?vs = Some ?m |- _ => cbn in H; injection H; clear H; intro H; symmetry in H
   | H: map.putmany_of_list_zip ?ks ?vs ?m0 = Some ?m |- _ => cbn in H; injection H; clear H; intro H; symmetry in H
@@ -162,9 +163,13 @@ Lemma swap_chars_over_uart_correct m :
   (fun t m l => True).
 Proof.
   repeat t.
+  WeakestPrecondition.unfold1_cmd_goal.
   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.
+  WeakestPrecondition.unfold1_cmd_goal.
   eexists _, _, (fun v t _ l => exists rxv, map.putmany_of_list_zip ["polling"; "rx"]%string [v; rxv] l0 = Some l); repeat t.
+  WeakestPrecondition.unfold1_cmd_goal.
   eexists _, _, (fun v t _ l => exists txv, map.putmany_of_list_zip ["polling"; "tx"]%string [v; txv] l0 = Some l); repeat t.
+  WeakestPrecondition.unfold1_cmd_goal.
   eexists; split; repeat t.
 Defined.
 
@@ -246,8 +251,10 @@ Lemma echo_server_correct m :
   (fun t m l => echo_server_spec t None).
 Proof.
   repeat t.
+  WeakestPrecondition.unfold1_cmd_goal.
   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*) }
+  WeakestPrecondition.unfold1_cmd_goal.
   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/FlatConstMem.v b/bedrock2/src/bedrock2Examples/FlatConstMem.v
index 7071208c0..b8e4d8752 100644
--- a/bedrock2/src/bedrock2Examples/FlatConstMem.v
+++ b/bedrock2/src/bedrock2Examples/FlatConstMem.v
@@ -18,7 +18,6 @@ Require Import bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 Require Import Coq.Lists.List coqutil.Map.OfListWord.
 Require Import coqutil.Z.Lia.
 Require Import coqutil.Tactics.Tactics.
-Require Import coqutil.Tactics.letexists.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Word.Bitwidth32.
 Import Map.Interface Interface.map OfFunc.map OfListWord.map.
diff --git a/bedrock2/src/bedrock2Examples/LAN9250.v b/bedrock2/src/bedrock2Examples/LAN9250.v
index aa52b4f31..c83d68c92 100644
--- a/bedrock2/src/bedrock2Examples/LAN9250.v
+++ b/bedrock2/src/bedrock2Examples/LAN9250.v
@@ -2,7 +2,6 @@ Require Import bedrock2.Syntax bedrock2.NotationsCustomEntry.
 Require Import coqutil.Z.prove_Zeq_bitwise.
 Require Import bedrock2Examples.SPI.
 
-From coqutil Require Import letexists.
 Require Import bedrock2.AbsintWordToZ.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Z.div_mod_to_equations.
@@ -781,6 +780,13 @@ Section WithParameters.
 
   Import symmetry autoforward.
 
+  Local Ltac original_esplit := esplit.
+  Local Ltac esplit := hnf; apply_rules_until_propositional; original_esplit.
+
+  Local Ltac original_eexists := eexists.
+  Local Tactic Notation "eexists" :=
+    hnf; apply_rules_until_propositional; original_eexists.
+
   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 e15ea518f..bd458f6da 100644
--- a/bedrock2/src/bedrock2Examples/SPI.v
+++ b/bedrock2/src/bedrock2Examples/SPI.v
@@ -84,7 +84,6 @@ Section WithParameters.
          morphism (Properties.word.ring_morph (word := word)),
          constants [Properties.word_cst]).
 
-  Import coqutil.Tactics.letexists.
   Import Loops.
   Lemma spi_write_ok : program_logic_goal_for_function! spi_write.
   Proof.
@@ -130,17 +129,6 @@ 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/bsearch.v b/bedrock2/src/bedrock2Examples/bsearch.v
index 2e452db74..8d518f037 100644
--- a/bedrock2/src/bedrock2Examples/bsearch.v
+++ b/bedrock2/src/bedrock2Examples/bsearch.v
@@ -42,7 +42,7 @@ Import HList List.
       ((*sorted*)False -> True)
       ).
 
-From coqutil.Tactics Require Import eabstract letexists rdelta.
+From coqutil.Tactics Require Import eabstract rdelta.
 From coqutil.Macros Require Import symmetry.
 Import PrimitivePair.
 Require Import bedrock2.ZnWords.
diff --git a/bedrock2/src/bedrock2Examples/indirect_add.v b/bedrock2/src/bedrock2Examples/indirect_add.v
index e59ef10d0..33c0a2dc1 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add.v
@@ -17,7 +17,7 @@ Require Import coqutil.Word.Interface coqutil.Map.Interface bedrock2.Map.Separat
 Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import letexists eabstract.
+From coqutil.Tactics Require Import eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars.
 
 Section WithParameters.
diff --git a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
index 788588e65..4228b6de4 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
@@ -23,7 +23,7 @@ Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 Require Import coqutil.Macros.WithBaseName.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import letexists eabstract.
+From coqutil.Tactics Require Import eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars bedrock2.Array.
 
 Section WithParameters.
diff --git a/bedrock2/src/bedrock2Examples/insertionsort.v b/bedrock2/src/bedrock2Examples/insertionsort.v
index e6fac4532..1777366da 100644
--- a/bedrock2/src/bedrock2Examples/insertionsort.v
+++ b/bedrock2/src/bedrock2Examples/insertionsort.v
@@ -31,7 +31,7 @@ Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import letexists eabstract.
+From coqutil.Tactics Require Import eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars bedrock2.Array bedrock2.Loops.
 Require Import bedrock2.ZnWords.
 Require Import coqutil.Sorting.Permutation.
diff --git a/bedrock2/src/bedrock2Examples/ipow.v b/bedrock2/src/bedrock2Examples/ipow.v
index bdfb950c4..331188ce0 100644
--- a/bedrock2/src/bedrock2Examples/ipow.v
+++ b/bedrock2/src/bedrock2Examples/ipow.v
@@ -14,7 +14,7 @@ Definition ipow := func! (x, e) ~> ret {
 }.
 
 From bedrock2 Require Import Semantics BasicC64Semantics WeakestPrecondition ProgramLogic.
-From coqutil Require Import Word.Properties Word.Interface Tactics.letexists.
+From coqutil Require Import Word.Properties Word.Interface.
 Import Interface.word.
 
 #[export] Instance spec_of_ipow : spec_of "ipow" :=
diff --git a/bedrock2/src/bedrock2Examples/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v
index 009a5f63f..a703c9ee3 100644
--- a/bedrock2/src/bedrock2Examples/lightbulb.v
+++ b/bedrock2/src/bedrock2Examples/lightbulb.v
@@ -8,7 +8,7 @@ Require Import bedrock2Examples.SPI.
 Require Import bedrock2Examples.LAN9250.
 From coqutil Require Import Z.div_mod_to_equations.
 From coqutil Require Import Word.Interface Map.Interface.
-From coqutil.Tactics Require Import letexists eabstract.
+From coqutil.Tactics Require Import eabstract.
 From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars.
 From bedrock2.Map Require Import Separation SeparationLogic.
 Require bedrock2.SepAutoArray bedrock2.SepCalls.
diff --git a/bedrock2/src/bedrock2Examples/memconst.v b/bedrock2/src/bedrock2Examples/memconst.v
index 4c2167540..6b60b2356 100644
--- a/bedrock2/src/bedrock2Examples/memconst.v
+++ b/bedrock2/src/bedrock2Examples/memconst.v
@@ -35,7 +35,7 @@ Section WithParameters.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
-  Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
+  Import coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
   Local Ltac normalize_body_of_function f ::= f.
diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
index c18867845..858be3953 100644
--- a/bedrock2/src/bedrock2Examples/memequal.v
+++ b/bedrock2/src/bedrock2Examples/memequal.v
@@ -41,7 +41,7 @@ Section WithParameters.
     {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.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
   Local Ltac ZnWords := destruct width_cases; bedrock2.ZnWords.ZnWords.
@@ -160,6 +160,7 @@ Section WithParameters.
         eapply byte.unsigned_inj in HH; trivial. }
 
       intuition idtac. case H6 as (?&?&?). subst. subst r.
+      WeakestPrecondition.unfold1_cmd_goal.
       eapply WeakestPreconditionProperties.dexpr_expr.
       letexists; split; cbn.
       { rewrite ?Properties.map.get_put_dec; cbn; exact eq_refl. }
diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
index 4aa826831..89c77a0a2 100644
--- a/bedrock2/src/bedrock2Examples/memmove.v
+++ b/bedrock2/src/bedrock2Examples/memmove.v
@@ -56,7 +56,7 @@ Section WithParameters.
     {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.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
   Local Ltac ZnWords := destruct width_cases; bedrock2.ZnWords.ZnWords.
@@ -76,7 +76,7 @@ Section WithParameters.
     repeat straightline.
 
     set (x := word.sub src dst) in *.
-    unfold1_cmd_goal; cbv beta match delta [cmd_body].
+    unfold1_cmd_goal.
     eapply WeakestPreconditionProperties.dexpr_expr.
     letexists; split.
     { subst l0; rewrite ?Properties.map.get_put_dec; exact eq_refl. }
@@ -85,6 +85,7 @@ Section WithParameters.
     (* x = 0 *)
     split; intros Hx; cycle 1.
     { replace src with dst in * by ZnWords.
+      unfold1_cmd_goal.
       cbn; ssplit; eauto.
       eexists _, _; ssplit; eauto.
       eapply map.split_same_footprint; eauto.
@@ -92,7 +93,7 @@ Section WithParameters.
       rewrite 2map.get_of_list_word_at, 2List.nth_error_None.
       Morphisms.f_equiv. ZnWords. }
 
-    unfold1_cmd_goal; cbv beta match delta [cmd_body].
+    unfold1_cmd_goal.
     eapply WeakestPreconditionProperties.dexpr_expr.
     letexists; split.
     { subst l0; rewrite ?Properties.map.get_put_dec; exact eq_refl. }
@@ -161,6 +162,21 @@ Section WithParameters.
           repeat straightline.
 
           cbv [WeakestPrecondition.load load load_Z]; cbn.
+
+          assert (forall (T: Type) (A B B': T -> Prop),
+                     (forall x, B x -> B' x) ->
+                     (exists x, A x /\ B x) ->
+                     (exists x, A x /\ B' x)) as Helper.
+          { clear. firstorder idtac. }
+          eapply Helper; clear Helper.
+          { intros w Hw.
+            eapply WeakestPreconditionProperties.Proper_store.
+            { cbv [Morphisms.pointwise_relation Basics.impl].
+              intros mm Hmm.
+              apply_rules_until_propositional.
+              exact Hmm. }
+            exact Hw. }
+
           destruct s0 as [|b s0], d0 as [|B d0]; try (cbn in *; congruence); [].
           exists (word.of_Z (byte.unsigned b)).
           pose proof map.get_split src0 _ _ _ H6.
@@ -177,6 +193,7 @@ Section WithParameters.
           eexists. rewrite H16. split.
           { rewrite word.unsigned_of_Z, Scalars.wrap_byte_unsigned.
             rewrite byte.of_Z_unsigned; trivial. }
+          apply_rules_until_propositional.
 
           eapply map.split_remove_put in H6; [|eapply H14].
           eapply map.split_remove_put in H8; [|eapply H16].
diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
index cd3af9e99..1295080f1 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -44,7 +44,7 @@ Section WithParameters.
     {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.Tactics.Tactics coqutil.Tactics.autoforward.
   Import coqutil.Word.Properties coqutil.Map.Properties.
 
   Local Ltac ZnWords := destruct width_cases; bedrock2.ZnWords.ZnWords.
diff --git a/bedrock2/src/bedrock2Examples/rpmul.v b/bedrock2/src/bedrock2Examples/rpmul.v
index 79e0b31bb..75e418590 100644
--- a/bedrock2/src/bedrock2Examples/rpmul.v
+++ b/bedrock2/src/bedrock2Examples/rpmul.v
@@ -17,7 +17,7 @@ Definition rpmul := func! (x, e) ~> ret {
 }.
 
 From bedrock2 Require Import Semantics BasicC32Semantics WeakestPrecondition ProgramLogic.
-From coqutil Require Import Word.Properties Word.Interface Tactics.letexists.
+From coqutil Require Import Word.Properties Word.Interface.
 
 #[export] Instance spec_of_rpmul : spec_of "rpmul" := fnspec! "rpmul" x e ~> v,
   { requires t m := True;
diff --git a/bedrock2/src/bedrock2Examples/stackalloc.v b/bedrock2/src/bedrock2Examples/stackalloc.v
index 2920be2d2..bf99e0e32 100644
--- a/bedrock2/src/bedrock2Examples/stackalloc.v
+++ b/bedrock2/src/bedrock2Examples/stackalloc.v
@@ -23,7 +23,7 @@ Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import letexists eabstract.
+From coqutil.Tactics Require Import eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars.
 Require Import coqutil.Word.Interface.
 From coqutil.Tactics Require Import reference_to_string .
diff --git a/bedrock2/src/bedrock2Examples/swap.v b/bedrock2/src/bedrock2Examples/swap.v
index 36878febc..06d3e8885 100644
--- a/bedrock2/src/bedrock2Examples/swap.v
+++ b/bedrock2/src/bedrock2Examples/swap.v
@@ -24,7 +24,7 @@ Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import Tactics letexists eabstract.
+From coqutil.Tactics Require Import Tactics eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Tactics.rdelta.
diff --git a/bedrock2/src/bedrock2Examples/swap_by_add.v b/bedrock2/src/bedrock2Examples/swap_by_add.v
index b7ac64911..6b2390daf 100644
--- a/bedrock2/src/bedrock2Examples/swap_by_add.v
+++ b/bedrock2/src/bedrock2Examples/swap_by_add.v
@@ -19,7 +19,7 @@ Require Import bedrock2.Semantics bedrock2.FE310CSemantics.
 Require Import coqutil.Map.Interface bedrock2.Map.Separation bedrock2.Map.SeparationLogic.
 
 Require bedrock2.WeakestPreconditionProperties.
-From coqutil.Tactics Require Import Tactics letexists eabstract.
+From coqutil.Tactics Require Import Tactics eabstract.
 Require Import bedrock2.ProgramLogic bedrock2.Scalars.
 Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Word.Naive.
 Require Import coqutil.Tactics.eplace Coq.setoid_ring.Ring_tac.
diff --git a/deps/coqutil b/deps/coqutil
index b3e96d731..691dce45a 160000
--- a/deps/coqutil
+++ b/deps/coqutil
@@ -1 +1 @@
-Subproject commit b3e96d731d50bb372dee48484cbeb73ab82d5be5
+Subproject commit 691dce45a2433b4df74079b31ee9f82620da903c

From b46e864bfd04d36fc78fc4767f0399c6f6dbefec Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 1 Aug 2023 02:51:00 +0000
Subject: [PATCH 8/8] port more examples from wp to exec

---
 bedrock2/src/bedrock2Examples/indirect_add.v |  2 +-
 bedrock2/src/bedrock2Examples/lightbulb.v    |  4 +-
 bedrock2/src/bedrock2Examples/memmove.v      | 40 +++++++-------------
 bedrock2/src/bedrock2Examples/memswap.v      |  4 +-
 4 files changed, 20 insertions(+), 30 deletions(-)

diff --git a/bedrock2/src/bedrock2Examples/indirect_add.v b/bedrock2/src/bedrock2Examples/indirect_add.v
index 33c0a2dc1..b28360bc2 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/lightbulb.v b/bedrock2/src/bedrock2Examples/lightbulb.v
index a703c9ee3..82740a299 100644
--- a/bedrock2/src/bedrock2Examples/lightbulb.v
+++ b/bedrock2/src/bedrock2Examples/lightbulb.v
@@ -615,14 +615,14 @@ Section WithParameters.
     lightbulb_loop; lightbulb_handle; recvEthernet;  lan9250_writeword; lan9250_readword;
     spi_xchg; spi_write; spi_read].
 
-  Lemma link_lightbulb_loop : spec_of_lightbulb_loop function_impls.
+  Lemma link_lightbulb_loop : spec_of_lightbulb_loop (map.of_list 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).
   Qed.
-  Lemma link_lightbulb_init : spec_of_lightbulb_init function_impls.
+  Lemma link_lightbulb_init : spec_of_lightbulb_init (map.of_list function_impls).
   Proof.
     eapply lightbulb_init_ok; eapply lan9250_init_ok;
     try (eapply lan9250_wait_for_boot_ok || eapply lan9250_mac_write_ok);
diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
index 89c77a0a2..258d9d950 100644
--- a/bedrock2/src/bedrock2Examples/memmove.v
+++ b/bedrock2/src/bedrock2Examples/memmove.v
@@ -211,18 +211,12 @@ Section WithParameters.
           eexists.
           eexists.
           { eauto. }
-          eexists.
-          repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn).
-          eexists.
-          { eauto. }
-          eexists.
-          eexists.
-          { eauto. }
-          eexists _, _, _, _.
-          split.
+          repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn).
+          { subst l.
+            repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn). }
           { cbv [Loops.enforce]; cbn.
-            repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split.
-            { exact eq_refl. }
+            subst l0 l.
+            repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn).
             { eapply map.map_ext; intros k.
               repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]).
               repeat (destruct String.eqb; trivial). } }
@@ -242,8 +236,8 @@ Section WithParameters.
         { cbn. intuition idtac. eexists _, _; ssplit; eauto. } }
 
     { assert (n <= x) by ZnWords.
+      repeat straightline.
 
-      unfold1_cmd_goal; cbv beta match delta [cmd_body].
       eapply WeakestPreconditionProperties.dexpr_expr.
       repeat straightline.
       letexists; split.
@@ -349,21 +343,14 @@ Section WithParameters.
 
           cbv [get literal dlet.dlet].
           repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn).
-          eexists.
-          eexists.
-          { eauto. }
-          eexists.
-          repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn).
-          eexists.
-          { eauto. }
-          eexists.
-          eexists.
-          { eauto. }
-          eexists _, _, _, _.
-          split.
+          repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn).
+          { subst l.
+            repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn). }
+          { subst l l0.
+            repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn). }
           { cbv [Loops.enforce]; cbn.
-            repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split.
-            { exact eq_refl. }
+            subst l1 l0 l.
+            repeat (straightline || rewrite map.get_put_dec || rewrite map.get_remove_dec || eexists (_ : word) || apply conj || cbn).
             { eapply map.map_ext; intros k.
               repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]).
               repeat (destruct String.eqb; trivial). } }
@@ -402,6 +389,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 *.
+    { trivial. }
     { 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 1295080f1..3087494c3 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -141,10 +141,12 @@ Section WithParameters.
         letexists; split.
         { subst l l0 l1 l2. rewrite ?Properties.map.get_put_dec; cbn. exact eq_refl. }
 
+        repeat straightline.
         eexists _, _, _.
         split.
         { cbv [Loops.enforce l l0 l1 l2]; cbn.
-          repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn); split.
+          subst l5 l4 l3 l2 l1 l0 l.
+          repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn || apply conj).
           { exact eq_refl. }
           { eapply map.map_ext; intros k.
             repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]).