diff --git a/bedrock2 b/bedrock2
index 7f2d764e..5062f79b 160000
--- a/bedrock2
+++ b/bedrock2
@@ -1 +1 @@
-Subproject commit 7f2d764ed79f394fe715505a04301d0fb502407f
+Subproject commit 5062f79b2200ef49b7d38cf08c67c77daa752e67
diff --git a/src/Rupicola/Examples/Arithmetic.v b/src/Rupicola/Examples/Arithmetic.v
index 3dd2f4d2..262b0ce7 100644
--- a/src/Rupicola/Examples/Arithmetic.v
+++ b/src/Rupicola/Examples/Arithmetic.v
@@ -6,11 +6,9 @@ From bedrock2 Require BasicC32Semantics BasicC64Semantics.
 Module Type FNV1A_params.
   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: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Parameter prime : word.
   Parameter offset : word.
@@ -18,7 +16,7 @@ End FNV1A_params.
 
 Module FNV1A (Import P: FNV1A_params).
 #[global]
-  Existing Instances BW word locals mem env ext_spec wordok mapok localsok envok ext_spec_ok.
+  Existing Instances BW word locals mem ext_spec wordok mapok localsok ext_spec_ok.
   Import SizedListArrayCompiler.
 
   Definition update (hash data : word) :=
diff --git a/src/Rupicola/Examples/Arrays.v b/src/Rupicola/Examples/Arrays.v
index f4a91de1..cc108854 100644
--- a/src/Rupicola/Examples/Arrays.v
+++ b/src/Rupicola/Examples/Arrays.v
@@ -7,11 +7,9 @@ Require Import coqutil.Word.LittleEndianList.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Section GetPut.
diff --git a/src/Rupicola/Examples/CMove/CMove.v b/src/Rupicola/Examples/CMove/CMove.v
index 289f26b9..8a4f7f38 100644
--- a/src/Rupicola/Examples/CMove/CMove.v
+++ b/src/Rupicola/Examples/CMove/CMove.v
@@ -8,14 +8,12 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section __.
   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: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Section Gallina.
-    
+
     Definition all_1s : word := word.of_Z (-1).
 
     Definition is_mask mask : Prop :=
@@ -23,7 +21,7 @@ Section __.
 
     Definition mask_of_bool (b : bool) :=
       if b then all_1s else word.of_Z 0.
-      
+
     (*idea: if b then true_val else false_val *)
     Definition select_word (mask : word) true_val false_val :=
       let/n nmask := (word.sub (word.of_Z (-1)) mask) in
@@ -49,11 +47,11 @@ Section __.
       let/n c2 := put r in
       (c1,c2).
 
-    
+
     Instance HasDefault_word : HasDefault word :=
       word.of_Z 0.
 
-    Definition cmove_array mask len 
+    Definition cmove_array mask len
                (a1: ListArray.t word.rep)
                (a2: ListArray.t word.rep) :=
       let/n from := word.of_Z 0 in
@@ -91,14 +89,14 @@ Section __.
       (a1, a2).
   End Gallina.
 
-  
+
   Lemma z_lt_width : 0 <= width.
   Proof.
     destruct width_cases; lia.
   Qed.
-  
 
-  
+
+
   Lemma all_1s_and : forall x, word.and all_1s x = x.
   Proof.
     intros.
@@ -119,7 +117,7 @@ Section __.
   Proof.
     rewrite <- (word.of_Z_signed (word.not all_1s)).
     rewrite word.signed_not.
-    unfold all_1s.    
+    unfold all_1s.
     rewrite word.signed_of_Z.
     rewrite !word.swrap_inrange.
     change (-1) with (-(1)).
@@ -132,7 +130,7 @@ Section __.
       destruct width_cases as [H|H]; rewrite !H; lia.
       destruct width_cases as [H|H]; rewrite !H; lia.
     }
-  Qed.    
+  Qed.
 
   Lemma zero_and (x : word)
     : word.and (word.of_Z 0) x = word.of_Z 0.
@@ -143,7 +141,7 @@ Section __.
     reflexivity.
   Qed.
 
-  
+
   Lemma zero_or (x : word)
     : word.or (word.of_Z 0) x = x.
   Proof.
@@ -163,7 +161,7 @@ Section __.
     rewrite word.morph_or.
     reflexivity.
   Qed.
-    
+
   Lemma cmove_word_is_conditional mask c1 c2
     : is_mask mask ->
       cmove_word mask c1 c2 = if word.eqb mask (word.of_Z 0) then c2 else c1.
@@ -246,7 +244,7 @@ Section __.
         tr' = tr /\
         (cell_value ptr1 (cmove_word mask c1 c2)
          * cell_value ptr2 c2 * R)%sep mem' }.
-  
+
   Derive cmove_word_br2fn SuchThat
          (defn! "cmove_word" ("mask", "c1", "c2") { cmove_word_br2fn },
           implements cmove_word)
@@ -265,7 +263,7 @@ Section __.
         let (c1',c2') := (cswap_word mask c1 c2) in
         (cell_value ptr1 c1'
          * cell_value ptr2 c2' * R)%sep mem' }.
-  
+
   Derive cswap_word_br2fn SuchThat
          (defn! "cswap_word" ("mask", "c1", "c2") { cswap_word_br2fn },
           implements cswap_word)
@@ -275,7 +273,7 @@ Section __.
   Qed.
 
 
-  
+
   Instance spec_of_cmove_array : spec_of "cmove_array" :=
     fnspec! "cmove_array" mask len ptr1 ptr2 / n c1 c2 R,
     (*TODO: if b then bw should be all 1s*)
diff --git a/src/Rupicola/Examples/CRC32/CRC32.v b/src/Rupicola/Examples/CRC32/CRC32.v
index 8ec1456d..88c563fa 100644
--- a/src/Rupicola/Examples/CRC32/CRC32.v
+++ b/src/Rupicola/Examples/CRC32/CRC32.v
@@ -12,11 +12,9 @@ Require Import
 Section __.
   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: bedrock2.Semantics.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}.
 
   Definition crc_table : list word :=
diff --git a/src/Rupicola/Examples/CapitalizeThird/Properties.v b/src/Rupicola/Examples/CapitalizeThird/Properties.v
index cfc8f3f8..1fdab987 100644
--- a/src/Rupicola/Examples/CapitalizeThird/Properties.v
+++ b/src/Rupicola/Examples/CapitalizeThird/Properties.v
@@ -15,7 +15,7 @@ Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Z.PushPullMod.
 Require Import coqutil.Tactics.Tactics.
 Require Import Rupicola.Examples.CapitalizeThird.CapitalizeThird.
-Require bedrock2.WeakestPrecondition.
+Require bedrock2.WeakestPrecondition bedrock2.Loops.
 Require bedrock2.Semantics.
 Require Import bedrock2.BasicC64Semantics.
 From coqutil.Tactics Require Import destr.
@@ -174,7 +174,7 @@ Ltac listsimplify :=
          end.
 
 Section Proofs.
-  Context (functions' : list (string * func))
+  Context (functions' : Semantics.env)
           (toupper_body : Byte.byte -> Byte.byte).
 
   Local Definition byte_to_word : Byte.byte -> word :=
@@ -303,11 +303,11 @@ Section Proofs.
     forall tr mem R,
       sep (String addr s) R mem ->
       len s = length (chars s) ->
-      let functions := (("capitalize_String",capitalize_String) :: functions') in
+      map.get functions' "capitalize_String" = Some capitalize_String ->
       let caps :=
           Gallina.capitalize_String (toupper:=toupper_body) s in
       WeakestPrecondition.call
-        functions "capitalize_String" tr mem [addr]
+        functions' "capitalize_String" tr mem [addr]
         (fun tr' mem' rets =>
            let success := word.unsigned (hd (word.of_Z 0) rets) in
            tr = tr' /\
@@ -318,18 +318,8 @@ Section Proofs.
              (success = 1 /\ sep (String addr caps) R mem'))).
   Proof.
     cbv zeta. intros.
-
-    (* finding the function to call *)
-    cbn [WeakestPrecondition.call
-           WeakestPrecondition.call_body
-           capitalize_String fst].
-    match goal with |- if String.eqb ?x ?x then _ else _ =>
-                    destr (String.eqb x x) end;
-      [ | congruence ].
-
-    (* load arguments as initial local variables *)
-    cbn [WeakestPrecondition.func].
-    eexists; split; [ reflexivity | ].
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -358,7 +348,8 @@ Section Proofs.
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
     match goal with |- dlet.dlet ?locals _ =>
                     cbv [dlet.dlet];
-                      exists nat, lt, (loop_invariant s tr locals addr R)
+                    eapply Loops.wp_while;
+                    exists nat, lt, (loop_invariant s tr locals addr R)
     end.
     split; [ exact lt_wf | ].
     cbv [loop_invariant]; split.
@@ -664,7 +655,9 @@ Section Proofs.
 
       (* ret = 1 *)
       eexists; split; [ solve [constructor] | ].
-      eexists; split; [ rewrite map.get_put_same; reflexivity | ].
+      eexists; split.
+      { cbn [map.getmany_of_list List.option_all List.map].
+        rewrite map.get_put_same; reflexivity. }
       cbn [WeakestPrecondition.list_map WeakestPrecondition.list_map_body].
 
       (* take care of easy postconditions *)
@@ -706,12 +699,12 @@ Section Proofs.
       Forall (fun s => len s = length (chars s)) strings ->
       (* there are at least 3 strings *)
       (3 <= length strings)%nat ->
-      let functions :=
-          (pair "capitalize_3rd" capitalize_3rd :: pair "capitalize_String" capitalize_String :: functions') in
+      map.get functions' "capitalize_3rd" = Some capitalize_3rd ->
+      map.get functions' "capitalize_String" = Some capitalize_String ->
       let caps :=
           Gallina.capitalize_3rd (toupper:=toupper_body) strings in
       WeakestPrecondition.call
-        functions "capitalize_3rd" tr mem [inp]
+        functions' "capitalize_3rd" tr mem [inp]
         (fun tr' mem' rets =>
            let success := word.unsigned (hd (word.of_Z 0) rets) in
            tr = tr' /\
@@ -726,18 +719,8 @@ Section Proofs.
                   R mem'))).
   Proof.
     cbv zeta. intros.
-
-    (* finding the function to call *)
-    cbn [WeakestPrecondition.call].
-    cbn [WeakestPrecondition.call_body
-           capitalize_3rd fst].
-    match goal with |- if String.eqb ?x ?x then _ else _ =>
-                    destr (String.eqb x x) end;
-      [ | congruence ].
-
-    (* load arguments as initial local variables *)
-    cbn [WeakestPrecondition.func].
-    eexists; split; [ reflexivity | ].
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -783,6 +766,7 @@ Section Proofs.
     eapply Proper_call.
     2:{
       apply capitalize_String_correct.
+      3: eassumption.
       { (* identify string that matches argument *)
         match goal with
           H : sep _ _ _ |- _ =>
@@ -811,9 +795,9 @@ Section Proofs.
           destruct x as [|? x]; [|cbn [length] in H; congruence]
     end.
     eexists; split; [ reflexivity | ].
-    eexists; split;
-      [ rewrite ?map.get_put_diff, map.get_put_same by congruence;
-        reflexivity | ].
+    eexists; split.
+    { cbn [map.getmany_of_list List.option_all List.map].
+      rewrite map.get_put_same; reflexivity. }
 
     (* prove postcondition *)
     repeat (split; [ reflexivity | ]).
diff --git a/src/Rupicola/Examples/Cells/Cells.v b/src/Rupicola/Examples/Cells/Cells.v
index 42e42aa8..ab0420e0 100644
--- a/src/Rupicola/Examples/Cells/Cells.v
+++ b/src/Rupicola/Examples/Cells/Cells.v
@@ -4,11 +4,9 @@ Record  cell {width: Z} {BW: Bitwidth width} {word: word.word width} := { data :
 Section with_parameters.
   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: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Local Notation cell := (@cell width BW word).
 
diff --git a/src/Rupicola/Examples/Cells/Incr.v b/src/Rupicola/Examples/Cells/Incr.v
index ea8d78ab..7cfec943 100644
--- a/src/Rupicola/Examples/Cells/Incr.v
+++ b/src/Rupicola/Examples/Cells/Incr.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Definition incr_gallina (c: cell) :=
diff --git a/src/Rupicola/Examples/Cells/IndirectAdd.v b/src/Rupicola/Examples/Cells/IndirectAdd.v
index 00c1171a..25746260 100644
--- a/src/Rupicola/Examples/Cells/IndirectAdd.v
+++ b/src/Rupicola/Examples/Cells/IndirectAdd.v
@@ -5,11 +5,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   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: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Local Notation cell := (@cell width BW word).
 
diff --git a/src/Rupicola/Examples/Cells/Swap.v b/src/Rupicola/Examples/Cells/Swap.v
index 6412542c..439048f5 100644
--- a/src/Rupicola/Examples/Cells/Swap.v
+++ b/src/Rupicola/Examples/Cells/Swap.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Definition swap_gallina (c1 c2: cell) :=
diff --git a/src/Rupicola/Examples/Conditionals.v b/src/Rupicola/Examples/Conditionals.v
index 19984b16..641efdb2 100644
--- a/src/Rupicola/Examples/Conditionals.v
+++ b/src/Rupicola/Examples/Conditionals.v
@@ -3,11 +3,9 @@ Require Import Rupicola.Lib.Api.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Implicit Type R : mem -> Prop.
diff --git a/src/Rupicola/Examples/DownTo.v b/src/Rupicola/Examples/DownTo.v
index 85ed554f..b7b86f91 100644
--- a/src/Rupicola/Examples/DownTo.v
+++ b/src/Rupicola/Examples/DownTo.v
@@ -22,11 +22,9 @@ Section Compilation.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width}.
   Context {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.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}.
 
   Instance spec_of_popcount : spec_of "popcount" :=
diff --git a/src/Rupicola/Examples/Expr.v b/src/Rupicola/Examples/Expr.v
index 6ef6feb2..79d27522 100644
--- a/src/Rupicola/Examples/Expr.v
+++ b/src/Rupicola/Examples/Expr.v
@@ -3,11 +3,9 @@ Require Import Rupicola.Lib.Api.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Definition example (x: word) (y: word) :=
diff --git a/src/Rupicola/Examples/IO/Echo.v b/src/Rupicola/Examples/IO/Echo.v
index 294cc94c..577b4fdf 100644
--- a/src/Rupicola/Examples/IO/Echo.v
+++ b/src/Rupicola/Examples/IO/Echo.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.IO.IO.
 Section Echo.
   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: bedrock2.Semantics.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}.
 
   Definition readw_trace (w: word) : trace_entry :=
diff --git a/src/Rupicola/Examples/IO/IO.v b/src/Rupicola/Examples/IO/IO.v
index f2074788..37b5c888 100644
--- a/src/Rupicola/Examples/IO/IO.v
+++ b/src/Rupicola/Examples/IO/IO.v
@@ -108,11 +108,9 @@ Import Writer.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Context {T: Type}.
diff --git a/src/Rupicola/Examples/IO/Stdout.v b/src/Rupicola/Examples/IO/Stdout.v
index a9abb976..251af6c9 100644
--- a/src/Rupicola/Examples/IO/Stdout.v
+++ b/src/Rupicola/Examples/IO/Stdout.v
@@ -6,11 +6,9 @@ Import Writer.
 Section Stdout.
   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: bedrock2.Semantics.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}.
 
   Notation Writer := (Writer.M string).
diff --git a/src/Rupicola/Examples/IO/Writer.v b/src/Rupicola/Examples/IO/Writer.v
index fa80c1ba..eb062b21 100644
--- a/src/Rupicola/Examples/IO/Writer.v
+++ b/src/Rupicola/Examples/IO/Writer.v
@@ -33,11 +33,9 @@ Import Writer.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Context {Evt: Type}.
diff --git a/src/Rupicola/Examples/KVStore/Automated.v b/src/Rupicola/Examples/KVStore/Automated.v
index ec1eefa0..dc21945b 100644
--- a/src/Rupicola/Examples/KVStore/Automated.v
+++ b/src/Rupicola/Examples/KVStore/Automated.v
@@ -22,11 +22,9 @@ Notation "'let/o'  x  :=  val  'goto_fail' default 'in'  body" :=
 Section KVSwap.
   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: bedrock2.Semantics.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 {ops} {key value : Type} {Value}
           {dummy_value : value}
@@ -496,8 +494,8 @@ Section KVSwap.
 
   Instance spec_of_kvswap : spec_of "kvswap" :=
     fun functions =>
-      spec_of_map_get (List.tl functions) -> (* FIXME *)
-      spec_of_map_put (List.tl functions) -> (* FIXME *)
+      spec_of_map_get functions -> (* FIXME *)
+      spec_of_map_put functions -> (* FIXME *)
       forall pm m pk1 k1 pk2 k2 R tr mem,
         k1 <> k2 -> (* TODO: try removing *)
         (Map pm m * Key pk1 k1 * Key pk2 k2 * R)%sep mem ->
diff --git a/src/Rupicola/Examples/KVStore/KVStore.v b/src/Rupicola/Examples/KVStore/KVStore.v
index e07ffce0..02351d0f 100644
--- a/src/Rupicola/Examples/KVStore/KVStore.v
+++ b/src/Rupicola/Examples/KVStore/KVStore.v
@@ -10,11 +10,9 @@ Inductive annotation {width: Z} {BW: Bitwidth width} {word: word.word width} : T
 Section KVStore.
   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: bedrock2.Semantics.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}.
   Local Notation annotation := (@annotation _ BW word).
 
diff --git a/src/Rupicola/Examples/KVStore/Manual.v b/src/Rupicola/Examples/KVStore/Manual.v
index a00de191..021ca14e 100644
--- a/src/Rupicola/Examples/KVStore/Manual.v
+++ b/src/Rupicola/Examples/KVStore/Manual.v
@@ -10,11 +10,9 @@ Local Open Scope nat_scope.
 Section examples.
   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: bedrock2.Semantics.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}.
 
   Section put_sum.
diff --git a/src/Rupicola/Examples/KVStore/Properties.v b/src/Rupicola/Examples/KVStore/Properties.v
index 4393327f..96d97497 100644
--- a/src/Rupicola/Examples/KVStore/Properties.v
+++ b/src/Rupicola/Examples/KVStore/Properties.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.KVStore.KVStore.
 Section properties.
   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: bedrock2.Semantics.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 {ops key value Value}
           {kvp : kv_parameters}
diff --git a/src/Rupicola/Examples/LinkedList/Find.v b/src/Rupicola/Examples/LinkedList/Find.v
index 93411aca..22c26c78 100644
--- a/src/Rupicola/Examples/LinkedList/Find.v
+++ b/src/Rupicola/Examples/LinkedList/Find.v
@@ -26,11 +26,9 @@ End Gallina.
 Section Compile.
   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: bedrock2.Semantics.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}.
 
   (* TODO: generalize *)
diff --git a/src/Rupicola/Examples/LinkedList/LinkedList.v b/src/Rupicola/Examples/LinkedList/LinkedList.v
index 8e6c4251..a9ad63bc 100644
--- a/src/Rupicola/Examples/LinkedList/LinkedList.v
+++ b/src/Rupicola/Examples/LinkedList/LinkedList.v
@@ -11,11 +11,9 @@ End Gallina.
 Section Separation.
   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: bedrock2.Semantics.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 {element : Type} {element_size : access_size}
           {Element : word -> element -> mem -> Prop}.
@@ -55,11 +53,9 @@ End Separation.
 Section Compile.
   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: bedrock2.Semantics.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}.
   (* TODO: generalize
   Context {element : Type}
@@ -168,11 +164,9 @@ End Compile.
 Section Helpers.
   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: bedrock2.Semantics.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 {element : Type} {element_size : access_size}
           {Element : word -> element -> mem -> Prop}.
diff --git a/src/Rupicola/Examples/Loops.v b/src/Rupicola/Examples/Loops.v
index 81f97d66..60788b73 100644
--- a/src/Rupicola/Examples/Loops.v
+++ b/src/Rupicola/Examples/Loops.v
@@ -7,11 +7,9 @@ Import LoopCompiler.
 Section Ex.
   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: bedrock2.Semantics.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}.
 
   Program Definition vect_memcpy {n1 n2} (len: word)
diff --git a/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v b/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v
index 2b436c22..38246919 100644
--- a/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v
+++ b/src/Rupicola/Examples/Nondeterminism/NonDeterminism.v
@@ -53,11 +53,9 @@ Proof. unfold ndspec, mbindn, mbind. simpl. firstorder idtac. Qed.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   Definition ndspec_k {A} (pred: A -> predicate) (c: M A) : predicate :=
diff --git a/src/Rupicola/Examples/Nondeterminism/Peek.v b/src/Rupicola/Examples/Nondeterminism/Peek.v
index 1f2bf25f..2739339c 100644
--- a/src/Rupicola/Examples/Nondeterminism/Peek.v
+++ b/src/Rupicola/Examples/Nondeterminism/Peek.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.Nondeterminism.NonDeterminism.
 Section Peek.
   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: bedrock2.Semantics.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}.
 
   Definition Bag := list word.
diff --git a/src/Rupicola/Examples/Nondeterminism/StackAlloc.v b/src/Rupicola/Examples/Nondeterminism/StackAlloc.v
index 3480057e..a71f7864 100644
--- a/src/Rupicola/Examples/Nondeterminism/StackAlloc.v
+++ b/src/Rupicola/Examples/Nondeterminism/StackAlloc.v
@@ -6,11 +6,9 @@ Require Import coqutil.Byte.
 Section Alloc.
   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: bedrock2.Semantics.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}.
 
   Definition stack_alloc (nbytes: nat) : ND.M (list byte) :=
diff --git a/src/Rupicola/Examples/Tree/Tree.v b/src/Rupicola/Examples/Tree/Tree.v
index ff1f7d1b..a5e81c58 100644
--- a/src/Rupicola/Examples/Tree/Tree.v
+++ b/src/Rupicola/Examples/Tree/Tree.v
@@ -3,7 +3,6 @@ Require Import Rupicola.Lib.Api.
 Section Tree.
   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: bedrock2.Semantics.ExtSpec}.
   Notation address := word.
 
@@ -134,7 +133,6 @@ Section Tree.
       Context
         {word_ok : word.ok word} {mem_ok : map.ok mem}
         {locals_ok : map.ok locals}
-        {env_ok : map.ok env}
         {ext_spec_ok : Semantics.ext_spec.ok ext_spec}
         {Alpha : word -> alpha -> mem -> Prop}
         {word_size_in_bytes : Z}.
diff --git a/src/Rupicola/Lib/Alloc.v b/src/Rupicola/Lib/Alloc.v
index 6d6021e9..612c02b4 100644
--- a/src/Rupicola/Lib/Alloc.v
+++ b/src/Rupicola/Lib/Alloc.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Lib.Notations.
 Section with_parameters.
   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: bedrock2.Semantics.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}.
 
   (* To enable allocation of A terms via the predicate P, implement this class *)
@@ -63,7 +61,7 @@ Section with_parameters.
     (R * (fun mem => pred v tr' mem locals'))%sep mem'.
 
   (* identity used as a marker to indicate when something should be allocated *)
-  Definition stack {A} (a : A) := a. 
+  Definition stack {A} (a : A) := a.
 
   Lemma compile_stack {tr m l functions A} (v : A):
     forall {P} {pred: P v -> predicate} {k: nlet_eq_k P v} {k_impl}
@@ -106,7 +104,7 @@ Arguments stack : simpl never.
 Arguments size_in_bytes : simpl never.
 
 (*TODO: speed up by combining pred_seps first and using 1 proper/ecancel_assumption?*)
-Ltac clear_pred_seps :=   
+Ltac clear_pred_seps :=
   unfold pred_sep;
   repeat change (fun x => ?h x) with h;
   repeat match goal with
@@ -116,7 +114,7 @@ Ltac clear_pred_seps :=
          end.
 
 (* FIXME I don't think eassumption is needed, and there might actually be multiple ?R m *)
-(* must be applied before compile_simple_alloc 
+(* must be applied before compile_simple_alloc
    TODO: understand why
  *)
 #[export] Hint Extern 10 =>
diff --git a/src/Rupicola/Lib/Arrays.v b/src/Rupicola/Lib/Arrays.v
index d8d9ef43..4912d8a6 100644
--- a/src/Rupicola/Lib/Arrays.v
+++ b/src/Rupicola/Lib/Arrays.v
@@ -79,11 +79,9 @@ End ListArray.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Section GenericArray.
diff --git a/src/Rupicola/Lib/Compiler.v b/src/Rupicola/Lib/Compiler.v
index d8c3cb42..fb4e8382 100644
--- a/src/Rupicola/Lib/Compiler.v
+++ b/src/Rupicola/Lib/Compiler.v
@@ -1,15 +1,14 @@
 Require Import Rupicola.Lib.Core.
 Require Import Rupicola.Lib.Notations.
 Require Import Rupicola.Lib.Tactics.
+Require Import bedrock2.Refinement.
 
 Section CompilerBasics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Lemma compile_dlet_as_nlet_eq {tr mem locals functions} {A} {vars: list string} (v: A):
@@ -113,7 +112,7 @@ Section CompilerBasics.
          Functions := functions }>
       cmd.seq c0 c1
       <{ pred1 }>.
-  Proof. intros; eapply WeakestPrecondition_weaken; eauto. Qed.
+  Proof. intros; econstructor; eauto. Qed.
 
   (* FIXME find a way to automate the application of these copy lemmas *)
   (* N.B. should only be added to compilation tactics that solve their subgoals,
@@ -219,11 +218,9 @@ End CompilerBasics.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Section NoSkips.
@@ -259,6 +256,60 @@ Section with_parameters.
       | _ => c
       end.
 
+    Lemma noskips_correct_fw:
+      forall cmd {tr mem locals functions} post,
+        Semantics.exec functions cmd tr mem locals post ->
+        Semantics.exec functions (noskips cmd) tr mem locals post.
+    Proof.
+      induction 1; cbn; try solve [econstructor; eauto].
+      destruct (is_skip (noskips c1)) eqn:Sk1.
+      - apply is_skip_sound in Sk1; rewrite Sk1 in *.
+        inversion IHexec. subst. eapply H1. assumption.
+      - apply is_skip_complete in Sk1.
+        destruct (is_skip (noskips c2)) eqn:Sk2.
+        + apply is_skip_sound in Sk2. rewrite Sk2 in *.
+          eapply Semantics.exec.weaken. 1: eassumption.
+          intros * Hmid. specialize H1 with (1 := Hmid). inversion H1. subst. assumption.
+        + eapply Semantics.exec.seq; eassumption.
+    Qed.
+
+    Lemma noskips_correct_bw:
+      forall cmd {functions tr mem locals} post,
+        Semantics.exec functions (noskips cmd) tr mem locals post ->
+        Semantics.exec functions cmd tr mem locals post.
+    Proof.
+      induction cmd; intros;
+        match goal with
+        | H: Semantics.exec.exec _ (noskips ?c) _ _ _ _ |- _ =>
+            lazymatch c with
+            | cmd.while _ _ => idtac
+            | cmd.seq _ _ => idtac
+            | _ => inversion H; clear H; subst
+            end
+        end;
+        try solve [econstructor; eauto].
+      { cbn in *. destruct (is_skip (noskips cmd1)) eqn: E1.
+        { eapply is_skip_sound in E1.
+          eapply Semantics.exec.seq.
+          { eapply IHcmd1. rewrite E1.
+            eapply Semantics.exec.skip with
+              (post := fun t m l => t = tr /\ m = mem /\ l = locals).
+            auto. }
+          cbv beta. intros * (? & ? & ?); subst.
+          eapply IHcmd2. assumption. }
+        destruct (is_skip (noskips cmd2)) eqn: E2.
+        { eapply is_skip_sound in E2.
+          eapply Semantics.exec.seq.
+          { eapply IHcmd1. eassumption. }
+          intros. eapply IHcmd2. rewrite E2. eapply Semantics.exec.skip. assumption. }
+        inversion H. subst.
+        eapply Semantics.exec.seq.
+        { eapply IHcmd1. eassumption. }
+        { intros. eapply IHcmd2. eauto. } }
+      { cbn in *. eapply refinement_while. 2: exact H.
+        unfold refinement. intros *. eapply IHcmd. }
+    Qed.
+
     Lemma noskips_correct:
       forall cmd {tr mem locals functions} post,
         WeakestPrecondition.program functions
@@ -266,39 +317,9 @@ Section with_parameters.
         WeakestPrecondition.program functions
           cmd tr mem locals post.
     Proof.
-      split; revert tr mem locals post.
-      all: induction cmd;
-        repeat match goal with
-               | _ => eassumption
-               | _ => apply IHcmd
-               | [ H: _ /\ _ |- _ ] => destruct H
-               | [  |- _ /\ _ ] => split
-               | [ H: forall v t m l, ?P v t m l -> exists _, _ |- ?P _ _ _ _ -> _ ] =>
-                 let h := fresh in intros h; specialize (H _ _ _ _ h)
-               | [ H: exists _, _ |- _ ] => destruct H
-               | [  |- exists _, _ ] => eexists
-               | [ H: context[WeakestPrecondition.cmd] |- context[WeakestPrecondition.cmd] ] => solve [eapply H; eauto]
-               | _ => unfold WeakestPrecondition.program in * || cbn || intros ? || eauto
-               end.
-
-      all: destruct (is_skip (noskips cmd1)) eqn:H1;
-        [ apply is_skip_sound in H1; rewrite H1 in * |
-          apply is_skip_complete in H1;
-           (destruct (is_skip (noskips cmd2)) eqn:H2;
-            [ apply is_skip_sound in H2; rewrite H2 in * |
-              apply is_skip_complete in H2 ]) ].
-
-      - apply IHcmd1, IHcmd2; eassumption.
-      - eapply WeakestPrecondition_weaken, IHcmd1; eauto.
-      - eapply WeakestPrecondition_weaken.
-        * intros * H0. eapply IHcmd2. apply H0.
-        * eapply IHcmd1. eassumption.
-
-      - eapply IHcmd1 in H. eapply IHcmd2. eassumption.
-      - eapply IHcmd1 in H. eapply WeakestPrecondition_weaken in H; [ apply H |].
-        intros; eapply IHcmd2; eauto.
-      - apply IHcmd1 in H. eapply WeakestPrecondition_weaken in H; [ apply H |].
-        intros * H0%IHcmd2. apply H0.
+      unfold program. split; intros.
+      - eapply noskips_correct_bw. assumption.
+      - eapply noskips_correct_fw. assumption.
     Qed.
 
     Definition compile_setup_remove_skips := noskips_correct.
@@ -346,6 +367,7 @@ Section with_parameters.
         WeakestPrecondition.program functions
           (noreassign cmd) tr mem locals post.
     Proof.
+      unfold program.
       all: induction cmd;
         repeat match goal with
                | _ => apply IHcmd
@@ -355,15 +377,16 @@ Section with_parameters.
                  let h := fresh in intros h; specialize (H _ _ _ _ h)
                | [ H: exists _, _ |- _ ] => destruct H
                | [  |- exists _, _ ] => eexists
-               | [ H: context[WeakestPrecondition.cmd] |- context[WeakestPrecondition.cmd] ] => solve [eapply H; eauto]
+               | [ H: context[Semantics.exec] |- context[Semantics.exec] ] => solve [inversion H; econstructor; eauto]
                | _ => unfold WeakestPrecondition.program in * || cbn || intros ? || eauto
                end.
 
       - destruct (is_var_expr_spec rhs lhs); simpl in *; subst; eauto; [].
-        destruct H as (xx & Hxx & ->).
-        rewrite map.put_idemp in H0; assumption.
-      - eapply WeakestPrecondition_weaken, IHcmd1; eauto;
-          intros; eapply WeakestPrecondition_weaken, IHcmd2; eauto.
+        inversion H; subst. inversion H2. rewrite map.put_idemp in *; try assumption.
+        econstructor. assumption.
+      - eapply refinement_while. 2: eassumption.
+        unfold refinement. intros.
+        eapply IHcmd. assumption.
     Qed.
 
     Definition compile_setup_remove_reassigns := noreassign_correct.
@@ -374,11 +397,9 @@ End with_parameters.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Section Setup.
@@ -404,8 +425,11 @@ Section with_parameters.
       clear; firstorder eauto using getmany_list_map.
     Qed.
 
+    Import bedrock2.Semantics.
+
     Lemma compile_setup_WeakestPrecondition_call_first {tr mem locals}
           name argnames retvars body args functions post:
+      map.get functions name = Some (argnames, retvars, body) ->
       map.of_list_zip argnames args = Some locals ->
       <{ Trace := tr;
          Memory := mem;
@@ -415,13 +439,10 @@ Section with_parameters.
       <{ wp_bind_retvars
            retvars
            (fun rets tr' mem' local' => post tr' mem' rets)  }> ->
-      WeakestPrecondition.call
-        ((name, (argnames, retvars, body)) :: functions)
-        name tr mem args post.
+      WeakestPrecondition.call functions name tr mem args post.
     Proof.
-      intros; WeakestPrecondition.unfold1_call_goal.
-      red. rewrite String.eqb_refl.
-      red. eexists; split; eauto.
+      intros.
+      do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
       eapply WeakestPrecondition_weaken; try eassumption.
       clear; firstorder eauto using getmany_list_map.
     Qed.
@@ -530,7 +551,10 @@ Tactic Notation "step_with_db" ident(db) :=
 Ltac compile_setup :=
   cbv [program_logic_goal_for];
   compile_setup_unfold_spec_of;
-  eapply compile_setup_WeakestPrecondition_call_first;
+  match goal with
+  | H: map.get ?fs ?name = Some _ |- WeakestPrecondition.call ?fs ?name _ _ _ _ =>
+      eapply compile_setup_WeakestPrecondition_call_first; [exact H | clear H..]
+  end;
   [ try reflexivity (* Arity check *)
   | repeat step_with_db compiler_setup;
     (step_with_db compiler_setup_post ||
diff --git a/src/Rupicola/Lib/Conditionals.v b/src/Rupicola/Lib/Conditionals.v
index 4c73a01e..4f3f37a0 100644
--- a/src/Rupicola/Lib/Conditionals.v
+++ b/src/Rupicola/Lib/Conditionals.v
@@ -7,11 +7,9 @@ Require Import Rupicola.Lib.Invariants.
 Section Conditionals.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition nlet_id {A} {v: A} : nlet_eq_k (fun _ => A) v := fun x _ => x.
diff --git a/src/Rupicola/Lib/ControlFlow/CondSwap.v b/src/Rupicola/Lib/ControlFlow/CondSwap.v
index d1c5e17e..0934b709 100644
--- a/src/Rupicola/Lib/ControlFlow/CondSwap.v
+++ b/src/Rupicola/Lib/ControlFlow/CondSwap.v
@@ -9,11 +9,9 @@ End Gallina.
 Section Compile.
   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: bedrock2.Semantics.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}.
 
   (* FIXME cswap should be compilable as-is; no need for a lemma. *)
@@ -115,11 +113,9 @@ End Compile.
 Section Helpers.
   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: bedrock2.Semantics.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}.
 
   Lemma cswap_iff1
diff --git a/src/Rupicola/Lib/ControlFlow/DownTo.v b/src/Rupicola/Lib/ControlFlow/DownTo.v
index 5d5f7638..cfe42416 100644
--- a/src/Rupicola/Lib/ControlFlow/DownTo.v
+++ b/src/Rupicola/Lib/ControlFlow/DownTo.v
@@ -64,11 +64,9 @@ Definition cmd_downto_fresh i_var i_expr step_impl k_impl :=
 Section Compilation.
   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: bedrock2.Semantics.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}.
   Implicit Types (x : word).
 
@@ -156,6 +154,7 @@ Section Compilation.
 
     (* handle while *)
     WeakestPrecondition.unfold1_cmd_goal; (cbv beta match delta [WeakestPrecondition.cmd_body]).
+    eapply Loops.wp_while.
 
     exists nat, lt.
     exists (fun i t m l =>
@@ -365,11 +364,9 @@ End DownToCompiler.
 Section GhostCompilation.
   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: bedrock2.Semantics.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}.
   Implicit Types (x : word).
 
@@ -457,6 +454,7 @@ Section GhostCompilation.
     (* handle while *)
     WeakestPrecondition.unfold1_cmd_goal;
       (cbv beta match delta [WeakestPrecondition.cmd_body]).
+    eapply Loops.wp_while.
     exists nat, lt.
     exists (fun i t m l =>
               let stgst :=
diff --git a/src/Rupicola/Lib/Core.v b/src/Rupicola/Lib/Core.v
index 43997165..59b87140 100644
--- a/src/Rupicola/Lib/Core.v
+++ b/src/Rupicola/Lib/Core.v
@@ -1213,11 +1213,9 @@ End Aliasing.
 Section Semantics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: bedrock2.Semantics.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}.
 
   Definition trace_entry :=
diff --git a/src/Rupicola/Lib/ExprCompiler.v b/src/Rupicola/Lib/ExprCompiler.v
index a5861948..49810d2a 100644
--- a/src/Rupicola/Lib/ExprCompiler.v
+++ b/src/Rupicola/Lib/ExprCompiler.v
@@ -11,7 +11,6 @@ Section ExprCompiler.
   Context {word: word.word width} {word_ok : word.ok word}.
   Context {mem: map.map word Byte.byte} {mem_ok : map.ok mem}.
   Context {locals: map.map String.string word} {locals_ok : map.ok locals}.
-  Context {env: map.map string (list string * list string * cmd)}.
 
   Section WordLemmas.
     Lemma word_not_xor (w: word):
@@ -571,7 +570,6 @@ Section Tests.
   Context {mem: map.map word Byte.byte} {locals: map.map String.string word}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env: map.map string (list string * list string * cmd)}.
 
   Context (m: mem).
 
diff --git a/src/Rupicola/Lib/ExprReflection.v b/src/Rupicola/Lib/ExprReflection.v
index 398b9182..caa78a60 100644
--- a/src/Rupicola/Lib/ExprReflection.v
+++ b/src/Rupicola/Lib/ExprReflection.v
@@ -4,11 +4,9 @@ Module ExprReflection.
   Section with_parameters.
     Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
     Context {localsT: map.map String.string word}.
-    Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
     Context {ext_spec: bedrock2.Semantics.ExtSpec}.
     Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
     Context {locals_ok : map.ok localsT}.
-    Context {env_ok : map.ok env}.
     Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
     Section Core.
diff --git a/src/Rupicola/Lib/InlineTables.v b/src/Rupicola/Lib/InlineTables.v
index 91b2c0a1..6c53dbf3 100644
--- a/src/Rupicola/Lib/InlineTables.v
+++ b/src/Rupicola/Lib/InlineTables.v
@@ -20,11 +20,9 @@ End InlineTable.
 Section __.
   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: bedrock2.Semantics.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 {K: Type}.
diff --git a/src/Rupicola/Lib/Loops.v b/src/Rupicola/Lib/Loops.v
index 0f5ff40f..4ccfd04c 100644
--- a/src/Rupicola/Lib/Loops.v
+++ b/src/Rupicola/Lib/Loops.v
@@ -1323,12 +1323,10 @@ Section with_parameters.
   Qed.
 
   Context {BW: Bitwidth width}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {mem: map.map word Byte.byte}.
   Context {mem_ok : map.ok mem}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Ltac _split_conj :=
@@ -1423,6 +1421,7 @@ Section with_parameters.
         unfold cmd_loop.
       repeat straightline.
       _split_conj.
+      eapply Loops.wp_while.
 
       destruct (Z_gt_le_dec from to).
       { (* Loop won't run at all *)
@@ -1450,8 +1449,6 @@ Section with_parameters.
                        (from' < to -> ExitToken.get (fst a) = false) /\
                        loop_pred from' (snd a) tr mem locals)).
 
-      red. red.
-
       eexists nat, lt, inv; split.
       { apply lt_wf. }
       { split.
@@ -2123,7 +2120,7 @@ Section with_parameters.
   Section ranged_for_words.
     Context {A: Type}
             {tr : Semantics.trace} {m : mem} {l : locals}
-            {functions : list (string * (list string * list string * cmd))}
+            {functions : Semantics.env}
             (from to : word).
 
     Definition compile_ranged_for_u :=
diff --git a/src/Rupicola/Lib/NoExprReflection.v b/src/Rupicola/Lib/NoExprReflection.v
index 4a02eba8..c9947174 100644
--- a/src/Rupicola/Lib/NoExprReflection.v
+++ b/src/Rupicola/Lib/NoExprReflection.v
@@ -5,11 +5,9 @@ Require Import Rupicola.Lib.Tactics.
 Section CompilerBasics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {memT: map.map word Byte.byte}.
   Context {localsT: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok memT}.
   Context {locals_ok : map.ok localsT}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Lemma compile_word_of_Z_constant {tr mem locals functions} (z: Z) :
diff --git a/src/Rupicola/Lib/Notations.v b/src/Rupicola/Lib/Notations.v
index 97224e86..875d19a9 100644
--- a/src/Rupicola/Lib/Notations.v
+++ b/src/Rupicola/Lib/Notations.v
@@ -197,7 +197,7 @@ Notation "[[ locals ]]" := {| value := locals; _value_ok := _ |} (only printing)
 
 Notation "<{ 'Trace' := tr ; 'Memory' := mem ; 'Locals' := locals ; 'Functions' := functions }> cmd <{ post }>" :=
   (WeakestPrecondition.cmd
-     (WeakestPrecondition.call functions)
+     functions
      cmd tr mem locals post)
     (at level 0,
      format "'[hv' <{  '[' '[' 'Trace'  :=  tr ']' ;  '/' '[' 'Memory'  :=  mem ']' ;  '/' '[' 'Locals'  :=  locals ']' ;  '/' '[' 'Functions'  :=  functions ']' ']'  }>  '/  ' cmd  '/' <{  '[' post ']'  }> ']'").
diff --git a/src/Rupicola/Lib/SepLocals.v b/src/Rupicola/Lib/SepLocals.v
index 6fb4af80..5f56f5be 100644
--- a/src/Rupicola/Lib/SepLocals.v
+++ b/src/Rupicola/Lib/SepLocals.v
@@ -4,11 +4,9 @@ Require Import Rupicola.Lib.Api.
 Section Var.
   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: bedrock2.Semantics.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}.
 
   Definition Var (name : string) (value : word)
diff --git a/src/Rupicola/Lib/Tactics.v b/src/Rupicola/Lib/Tactics.v
index fc6878d7..4d960bd5 100644
--- a/src/Rupicola/Lib/Tactics.v
+++ b/src/Rupicola/Lib/Tactics.v
@@ -216,10 +216,9 @@ Ltac program_logic_goal_for_function fname proc callees :=
   (* We do not evaluate callees since in this version they are typically already a value
      and it adds a noticeable performance overhead at declaration and Qed. *)
   let spec := lazymatch constr:(_:spec_of fname) with ?s => s end in
-  constr:(forall functions : list (string * func),
-             ltac:(let s := assuming_correctness_of_in
-                              callees functions
-                              (spec (cons (fname, proc) functions)) in
+  constr:(forall (functions : @map.rep _ _ Semantics.env)
+                 (EnvContains : map.get functions fname = Some proc),
+             ltac:(let s := assuming_correctness_of_in callees functions (spec functions) in
                    exact s)).
 
 Ltac use_hyp_with_matching_cmd :=
@@ -227,8 +226,7 @@ Ltac use_hyp_with_matching_cmd :=
            | H: context [WeakestPrecondition.cmd _ ?impl]
              |- WeakestPrecondition.cmd _ ?impl _ _ _ _ => H end in
   eapply Proper_cmd;
-  [ solve [apply Proper_call]
-  | repeat intro | eapply H ].
+  [ repeat intro | eapply H ].
 
 Ltac push_map_remove :=
   repeat first [ rewrite map.remove_put_diff by congruence