diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index cc7d4cc32..f1ec5e868 100644
--- a/bedrock2/src/bedrock2/ProgramLogic.v
+++ b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -210,7 +210,7 @@ Ltac straightline :=
     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;
-    cbv match beta delta [WeakestPrecondition.func]
+    left; cbv match beta delta [WeakestPrecondition.func]
   | |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
     unfold1_cmd_goal; cbv beta match delta [cmd_body];
     let x := ident_of_string s in
diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index 428f1db69..ca77dede8 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -122,6 +122,12 @@ Section WeakestPrecondition.
         list_map (get l) outnames (fun rets =>
         post t m rets)).
 
+  Definition execfunc e '(innames, outnames, c) (t : trace) (m : mem) (args : list word) (post : trace -> mem -> list word -> Prop) :=
+    exists lf, map.of_list_zip innames args = Some lf /\
+    forall mc, exec e c t m lf mc (fun t m l _ =>
+      exists retvs, map.getmany_of_list l outnames = Some retvs /\
+      post t m retvs).
+
   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 :=
@@ -130,6 +136,7 @@ Section WeakestPrecondition.
     | cons (f, decl) functions =>
       if String.eqb f fname
       then func (rec functions) decl t m args post
+        \/ execfunc (map.of_list functions) decl t m args post
       else rec functions fname t m args post
     end.
   Fixpoint call functions := call_body call functions.
@@ -173,10 +180,10 @@ Ltac unfold1_list_map_goal :=
 
 Ltac unfold1_call e :=
   lazymatch e with
-    @call ?width ?BW ?word ?mem ?locals ?ext_spec ?fs ?fname ?t ?m ?l ?post =>
+    @call ?width ?BW ?word ?mem ?locals ?env ?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)
+    constr:(@call_body width BW word mem locals env ext_spec
+                       (@call width BW word mem locals env ext_spec) fs fname t m l post)
   end.
 Ltac unfold1_call_goal :=
   let G := lazymatch goal with |- ?G => G end in
diff --git a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
index 03f85ae08..cd0d73b03 100644
--- a/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+++ b/bedrock2/src/bedrock2/WeakestPreconditionProperties.v
@@ -180,10 +180,16 @@ Section WeakestPrecondition.
     cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list (String.string * (list String.string * list String.string * Syntax.cmd.cmd)));
       cbn in *; intuition (try typeclasses eauto with core).
     destruct a.
-    destruct (String.eqb s a1); eauto.
-    eapply Proper_func;
+    destruct (String.eqb s a1); intuition eauto.
+    1: left; eapply Proper_func;
       cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
       eauto.
+    right.
+    cbv [WeakestPrecondition.execfunc] in *; destruct p as ((?&?)&?).
+    destruct H2 as (?&?&?).
+    eexists; split; eauto; intros.
+    eapply Semantics.exec.weaken; eauto; intros.
+    destruct H3 as (?&?&?); eauto.
   Qed.
 
   Global Instance Proper_program :
@@ -282,6 +288,11 @@ Section WeakestPrecondition.
     { eapply sound_args in H; t. }
   Qed.
 
+  Lemma exec_weaken_locals_of_list l E Z t m x mc post :
+    Semantics.exec.exec (map.of_list l) Z t m x mc post ->
+    List.Forall (fun '(k, v) => map.get E k = Some v) l ->
+    Semantics.exec.exec E Z t m x mc post.
+  Admitted.
 
   Section WithE.
     Context fs (E: env) (HE: List.Forall (fun '(k, v) => map.get E k = Some v) fs).
@@ -295,15 +306,23 @@ Section WeakestPrecondition.
       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.
+      destruct H0; t. {
+        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. }
+      { eexists; eauto.
+        eexists; eauto.
+        intros.
+        eapply Semantics.exec.weaken.
+        { specialize (H1 mc'). inversion HE; subst.
+          eapply exec_weaken_locals_of_list; eauto. }
+        { cbv beta; intros; t; eauto. } }
     Qed.
 
     Lemma sound_cmd'' c t m l mc post
diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
index b5cd8d28f..7ef2a70d8 100644
--- a/bedrock2/src/bedrock2Examples/memequal.v
+++ b/bedrock2/src/bedrock2Examples/memequal.v
@@ -30,6 +30,7 @@ Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
   Context {word: word.word width} {mem: map.map word byte} {locals: map.map string word}.
+  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: ExtSpec}.
   Import ProgramLogic.Coercions.
 
@@ -41,8 +42,7 @@ Section WithParameters.
                        (r  = 1 :>Z <-> xs  = ys) }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
-    {ext_spec_ok : ext_spec.ok ext_spec}.
+    {env_ok : map.ok env} {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
   Require Import coqutil.Word.Properties coqutil.Map.Properties.
diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
index e292dfd60..a7938ded0 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -32,7 +32,7 @@ Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
   Context {word: word.word width} {mem: map.map word byte} {locals: map.map string word}.
-  Context {ext_spec: ExtSpec}.
+  Context {env : map.map string (list string * list string * Syntax.cmd)} {ext_spec: ExtSpec}.
   Import ProgramLogic.Coercions.
 
   Global Instance spec_of_memswap : spec_of "memswap" :=
@@ -42,8 +42,7 @@ Section WithParameters.
       ensures t' m := m =* ys$@x * xs$@y * R /\ t=t' }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
-    {ext_spec_ok : ext_spec.ok ext_spec}.
+    {env_ok : map.ok env} {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
   Require Import coqutil.Word.Properties coqutil.Map.Properties.