From 783c09526619434776da13747fbe0e8e04fec084 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Fri, 4 Aug 2023 21:15:38 -0400
Subject: [PATCH] update to a rupicola/bedrock2 where wp is complete wrt exec

---
 rupicola                                      |   2 +-
 src/Bedrock/End2End/Poly1305/Field1305.v      |  30 ++--
 .../End2End/RupicolaCrypto/Broadcast.v        |  45 +++---
 src/Bedrock/End2End/RupicolaCrypto/Low.v      |  30 ++--
 src/Bedrock/End2End/X25519/Field25519.v       | 101 +++++++------
 src/Bedrock/End2End/X25519/GarageDoorTop.v    |  99 ++++++++----
 .../X25519/MontgomeryLadderProperties.v       | 102 ++-----------
 src/Bedrock/Field/Common/Arrays/ByteBounds.v  |   6 +-
 .../Field/Common/Arrays/MakeAccessSizes.v     |   6 +-
 .../Field/Common/Arrays/MakeListLengths.v     |   6 +-
 src/Bedrock/Field/Common/Arrays/MaxBounds.v   |   6 +-
 src/Bedrock/Field/Common/Names/MakeNames.v    |   6 +-
 src/Bedrock/Field/Common/Types.v              |  18 +--
 src/Bedrock/Field/Common/Util.v               |   6 +-
 src/Bedrock/Field/Interface/Compilation2.v    |  14 +-
 src/Bedrock/Field/Interface/Representation.v  |   8 +-
 .../Field/Stringification/Stringification.v   |  11 +-
 .../Field/Synthesis/Examples/p224_64_new.v    |  46 ++++--
 src/Bedrock/Field/Synthesis/New/ComputedOp.v  |   6 +-
 src/Bedrock/Field/Synthesis/New/Signature.v   | 121 +++++++--------
 .../Field/Synthesis/New/UnsaturatedSolinas.v  | 143 ++++++++++--------
 .../Synthesis/New/WordByWordMontgomery.v      | 130 ++++++++--------
 src/Bedrock/Field/Translation/Cmd.v           |   6 +-
 src/Bedrock/Field/Translation/Expr.v          |   6 +-
 src/Bedrock/Field/Translation/Flatten.v       |   6 +-
 src/Bedrock/Field/Translation/Func.v          |   6 +-
 src/Bedrock/Field/Translation/LoadStoreList.v |   6 +-
 src/Bedrock/Field/Translation/Proofs/Cmd.v    |  29 ++--
 .../Field/Translation/Proofs/Equivalence.v    |  12 +-
 .../Proofs/EquivalenceProperties.v            |  12 +-
 src/Bedrock/Field/Translation/Proofs/Expr.v   |   6 +-
 .../Field/Translation/Proofs/Flatten.v        |   8 +-
 src/Bedrock/Field/Translation/Proofs/Func.v   |  31 ++--
 .../Field/Translation/Proofs/LoadStoreList.v  |  48 +++---
 .../Field/Translation/Proofs/UsedVarnames.v   |   6 +-
 .../Translation/Proofs/ValidComputable/Cmd.v  |   6 +-
 .../Translation/Proofs/ValidComputable/Expr.v |   6 +-
 .../Translation/Proofs/ValidComputable/Func.v |   6 +-
 .../Field/Translation/Proofs/VarnameSet.v     |   6 +-
 src/Bedrock/Group/AdditionChains.v            |   6 +-
 src/Bedrock/Group/Point.v                     |   2 -
 src/Bedrock/Group/ScalarMult/CSwap.v          |   4 +-
 src/Bedrock/Group/ScalarMult/LadderStep.v     |   4 +-
 .../Group/ScalarMult/MontgomeryLadder.v       |  16 +-
 src/Bedrock/Group/ScalarMult/ScalarMult.v     |  15 +-
 src/Bedrock/Specs/Field.v                     |  10 +-
 src/Bedrock/Specs/Group.v                     |   1 -
 47 files changed, 605 insertions(+), 601 deletions(-)

diff --git a/rupicola b/rupicola
index 3f59b3d240..87d29e3bb6 160000
--- a/rupicola
+++ b/rupicola
@@ -1 +1 @@
-Subproject commit 3f59b3d2404ce425ddf4fd55ad2314996a573dc3
+Subproject commit 87d29e3bb6389f6abfe4347686827504ba815667
diff --git a/src/Bedrock/End2End/Poly1305/Field1305.v b/src/Bedrock/End2End/Poly1305/Field1305.v
index 2be9606bed..9e65932f28 100644
--- a/src/Bedrock/End2End/Poly1305/Field1305.v
+++ b/src/Bedrock/End2End/Poly1305/Field1305.v
@@ -38,51 +38,60 @@ Section Field.
   (**** Translate each field operation into bedrock2 and apply bedrock2 backend
         field pipeline proofs to prove the bedrock2 functions are correct. ****)
 
+  Local Notation functions_contain functions f :=
+    (Interface.map.get functions (fst f) = Some (snd f)).
+
   Derive fe1305_from_bytes
          SuchThat (forall functions,
+                      functions_contain functions fe1305_from_bytes ->
                       spec_of_from_bytes
                         (field_representation:=field_representation n s c)
-                        (fe1305_from_bytes :: functions))
+                        functions)
          As fe1305_from_bytes_correct.
   Proof. Time derive_bedrock2_func from_bytes_op. Qed.
 
   Derive fe1305_to_bytes
          SuchThat (forall functions,
+                      functions_contain functions fe1305_to_bytes ->
                       spec_of_to_bytes
                         (field_representation:=field_representation n s c)
-                        (fe1305_to_bytes :: functions))
+                        functions)
          As fe1305_to_bytes_correct.
   Proof. Time derive_bedrock2_func to_bytes_op. Qed.
 
   Derive fe1305_mul
          SuchThat (forall functions,
+                      functions_contain functions fe1305_mul ->
                       spec_of_BinOp bin_mul
                         (field_representation:=field_representation n s c)
-                        (fe1305_mul :: functions))
+                        functions)
          As fe1305_mul_correct.
   Proof. Time derive_bedrock2_func mul_op. Qed.
 
   Derive fe1305_square
          SuchThat (forall functions,
+                      functions_contain functions fe1305_square ->
                       spec_of_UnOp un_square
                         (field_representation:=field_representation n s c)
-                        (fe1305_square :: functions))
+                        functions)
          As fe1305_square_correct.
   Proof. Time derive_bedrock2_func square_op. Qed.
 
   Derive fe1305_add
          SuchThat (forall functions,
+                      functions_contain functions fe1305_add ->
                       spec_of_BinOp bin_add
                         (field_representation:=field_representation n s c)
-                        (fe1305_add :: functions))
+                        functions)
          As fe1305_add_correct.
   Proof. Time derive_bedrock2_func add_op. Qed.
 
   Derive fe1305_sub
          SuchThat (forall functions,
+                      functions_contain functions fe1305_sub ->
                       spec_of_BinOp bin_sub
                         (field_representation:=field_representation n s c)
-                        (fe1305_sub :: functions))
+                        functions)
          As fe1305_sub_correct.
   Proof. Time derive_bedrock2_func sub_op. Qed.
 End Field.
@@ -91,9 +100,9 @@ End Field.
 (*
 Require Import bedrock2.Syntax.
 Require Import compiler.Pipeline.
-Require Import compilerExamples.MMIO.
+Require Import compiler.MMIO.
 
-Definition funcs : list func :=
+Definition funcs : list (string * func) :=
   [ fe1305_mul;
     fe1305_add;
     fe1305_sub;
@@ -101,5 +110,8 @@ Definition funcs : list func :=
     fe1305_to_bytes;
     fe1305_from_bytes ].
 
-Compute compile (compile_ext_call (funname_env:=SortedListString.map)) (map.of_list funcs).
+#[local]
+Instance BWM_RV32IM : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.
+
+Compute compile (compile_ext_call (funname_env:=SortedListString.map)) funcs.
 *)
diff --git a/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v b/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
index eda65c911c..c8680322cc 100644
--- a/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
+++ b/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
@@ -1,4 +1,3 @@
-
 Require Import Coq.Unicode.Utf8.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Loops.
@@ -143,11 +142,9 @@ 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}.
 
 
@@ -242,7 +239,7 @@ Section with_parameters.
   Lemma ranged_for'_length_helper (from' : nat) scratch lst
     :  length (snd (ranged_for' 0 from'
                       (λ (acc : list T) (tok : ExitToken.t) (idx : Z) (_ : 0 - 1 < idx < from'),
-                        (tok, upd acc (Z.to_nat idx) (nth (Z.to_nat idx) lst default))) scratch : 
+                        (tok, upd acc (Z.to_nat idx) (nth (Z.to_nat idx) lst default))) scratch :
                    ExitToken.t * list T)) = length scratch.
   Proof.
     revert scratch lst.
@@ -263,8 +260,8 @@ Section with_parameters.
     }
   Qed.
 
-  
-  
+
+
   Lemma ranged_for'_invariant {A} n m (f : _ -> _ -> _ -> _) acc (P : A -> Prop)
     : (forall acc' tok idx, fst (f acc' tok idx) = tok) ->
       P acc ->
@@ -278,7 +275,7 @@ Section with_parameters.
     revert acc H0.
     pose proof (z_range_sound n m) as H'; revert H'.
     generalize ((z_range n m)).
-    
+
     induction l; simpl; intros; eauto.
     specialize (IHl ltac:(eauto)).
     specialize (H' a ltac:(tauto)).
@@ -288,7 +285,7 @@ Section with_parameters.
     eapply Hn; eauto.
   Qed.
 
-  
+
   Lemma skipn_ranged_for'_upd (from' : nat) scratch lst
     : skipn from'
         (snd
@@ -311,7 +308,7 @@ Section with_parameters.
     }
     lia.
   Qed.
-  
+
   Lemma map_predT_to_truncated_word ptr t
     : Lift1Prop.iff1 (t$@ptr) (array (truncated_word szT) sz_word ptr (map word_of_T t)).
   Proof.
@@ -335,8 +332,8 @@ Section with_parameters.
     }
   Qed.
 
-  
-  Lemma map_upd A B (f : A -> B) i (a : A) l 
+
+  Lemma map_upd A B (f : A -> B) i (a : A) l
     : map f (upd l i a) = upd (map f l) i (f a).
   Proof.
     eapply nth_error_ext;
@@ -360,7 +357,7 @@ Section with_parameters.
     {
       repeat rewrite ?nth_upd_diff, ?map_nth
         by (repeat rewrite ?List.map_length, ?List.upd_length; lia).
-      auto. 
+      auto.
     }
   Qed.
 
@@ -401,7 +398,7 @@ Section with_parameters.
     rewrite nd_as_ranged_for_all.
     rewrite ranged_for_all_as_ranged_for.
     repeat compile_step.
-    
+
     assert (~ a_var = to_var).
     {
       intro; subst.
@@ -487,7 +484,7 @@ Section with_parameters.
         assert (from' <= length acc).
         {
           unfold acc.
-          unfold a. 
+          unfold a.
           replace (from') with (Z.of_nat (Z.to_nat from')) by lia.
           rewrite ranged_for'_length_helper.
           lia.
@@ -505,11 +502,11 @@ Section with_parameters.
         apply skipn_ranged_for'_upd.
       }
       {
-        
+
         seprewrite_in map_predT_to_truncated_word H12.
         eapply array_store_of_sep in H12.
         destruct H12 as [? [? ?]].
-        
+
         eexists; split.
         { apply H11. }
         {
@@ -534,7 +531,7 @@ Section with_parameters.
           lia.
         }
         {
-          intros.          
+          intros.
           seprewrite map_predT_to_truncated_word.
           rewrite <- map_upd in H11.
           eauto.
@@ -586,7 +583,7 @@ Section with_parameters.
              lst_expr)
           k_impl
       <{ pred (nlet_eq [a_var] v k) }>.
-  Proof using T_Fits_ok env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using T_Fits_ok ext_spec_ok locals_ok mem_ok word_ok.
     eauto using compile_broadcast_expr'.
   Qed.
 
@@ -686,14 +683,14 @@ Section with_parameters.
     reflexivity.
   Qed.
 
-  
+
   Lemma split_hd_tl {A} (a:A) (l:list A)
     : 0 < length l ->
       l = hd a l :: tl l.
   Proof.
     destruct l; simpl in *; [lia | auto].
   Qed.
-          
+
   Lemma broadcast_var l idx_var scratch a_ptr b_ptr a_var a_data R' R
     : Lift1Prop.iff1 R' (a_data$@a_ptr * R)%sep ->
       map.get l a_var = Some a_ptr ->
@@ -739,7 +736,7 @@ Section with_parameters.
     seprewrite_in map_predT_to_truncated_word H5.
     seprewrite_in map_predT_to_truncated_word H5.
     rewrite <- (firstn_skipn (length lstl) a_data) in H5.
-    rewrite map_app in H5.   
+    rewrite map_app in H5.
     seprewrite_in (array_append (T:=word)) H5.
     rewrite map_length in H5.
     rewrite firstn_length in H5.
@@ -818,7 +815,7 @@ Section with_parameters.
       rewrite word.byte_of_Z_unsigned in H.
       ecancel_assumption.
       apply byte_in_word_bounds.
-    }          
+    }
   Qed.
 
 
@@ -831,7 +828,7 @@ Section with_parameters.
 
   (*TODO: where to get this fact from?*)
   Axiom width_mul_8 : exists x, width = x * 8.
-  
+
   Instance word_ac_ok : FitsInLocal_ok word word_ac.
   Proof.
     constructor; unfold word_of_T, szT, predT, word_ac.
@@ -897,7 +894,7 @@ Section with_parameters.
     instantiate (1:= fun _ => True).
 
     exists (map.put map.empty (word.of_Z (Z.of_nat (length lstl))) (nth (length lstl) const_list x00)).
-    exists (map.remove (OfListWord.map.of_list_word const_list) (word.of_Z (Z.of_nat (length lstl)))). 
+    exists (map.remove (OfListWord.map.of_list_word const_list) (word.of_Z (Z.of_nat (length lstl)))).
     intuition idtac.
     {
       eapply map.split_comm.
diff --git a/src/Bedrock/End2End/RupicolaCrypto/Low.v b/src/Bedrock/End2End/RupicolaCrypto/Low.v
index 6449ee89fb..c8c0ab6d84 100644
--- a/src/Bedrock/End2End/RupicolaCrypto/Low.v
+++ b/src/Bedrock/End2End/RupicolaCrypto/Low.v
@@ -157,7 +157,7 @@ Definition buf_pad {T} (buf: buffer_t T) (len: nat) (t: T) : buffer_t T := buf +
 Require Import bedrock2.NotationsCustomEntry.
 Section CompileBufPolymorphic.
   Import ProgramLogic.Coercions WeakestPrecondition.
-  Context (e : list (String.string * Syntax.func)).
+  Context (e : env).
   Context (T : Type) (sz : word) (pT : word -> T -> mem -> Prop).
 
   Declare Scope word_scope.
@@ -228,7 +228,7 @@ Section CompileBufPolymorphic.
     replace a with (word.add a (word.of_Z 0)) in HA by ring; eassumption.
   Qed.
 
-  
+
     Lemma buffer_at_full_capacity' (a : word) c (b : list T)
       :   length b = c ->
           Lift1Prop.iff1
@@ -356,7 +356,7 @@ Section CompileBufPolymorphic.
            assert (length stack = n :> Z) by Lia.lia)
   end.
   repeat straightline.
-  eapply Proper_cmd; [eapply Proper_call | intros ? ? ? ? | eapply H1 ]; cbn [app]; eauto; cycle 1.
+  eapply Proper_cmd; [ intros ? ? ? ? | eapply H1 ]; cbn [app]; eauto; cycle 1.
   { cbv [buffer_at]; cbn.
     sepsimpl; trivial.
     exists stack; cbn.
@@ -434,7 +434,7 @@ Section CompileBufPolymorphic.
     rewrite <-(firstn_skipn (Z.to_nat sz * length arr) pad) in H3.
     seprewrite_in @bytearray_append H3.
     unfold nlet_eq in H2.
-    eapply Proper_cmd; [eapply Proper_call| |eapply H2].
+    eapply Proper_cmd; [ |eapply H2].
     2: ecancel_assumption.
     2: {
       pose proof word.unsigned_range sz.
@@ -498,7 +498,7 @@ Section CompileBufPolymorphic.
     all: try eassumption.
     intros.
     eapply Proper_cmd;
-      [eapply Proper_call| |eapply H2].
+      [ |eapply H2].
     2:{ ecancel_assumption. }
     2:{ cbn [length] in *; lia. }
     intros t1 m1 l1 [Hm Hk].
@@ -626,7 +626,7 @@ Section CompileBufPolymorphic.
     rename x into pad.
     rewrite <-(firstn_skipn (Z.to_nat sz * length arr) pad) in H2.
     seprewrite_in @bytearray_append H2.
-    eapply Proper_cmd; [eapply Proper_call| |eapply H1].
+    eapply Proper_cmd; [ |eapply H1].
     2: ecancel_assumption.
     2: {
       pose proof word.unsigned_range sz.
@@ -669,7 +669,7 @@ Section CompileBufPolymorphic.
   Proof using dealloc_T.
     intros.  eapply deprecated_do_not_use_compile_buf_append with (arr:=[x]).  {
     ecancel_assumption. } { eassumption. } intros.  eapply Proper_cmd;
-    [eapply Proper_call| |eapply H1].  2:{ ecancel_assumption. } 2:{ cbn
+    [ |eapply H1].  2:{ ecancel_assumption. } 2:{ cbn
   [length] in *; lia. } intros t1 m1 l1 [Hm Hk].  cbv [nlet_eq] in *.  cbn
   [array] in *.  split; sepsimpl.  { ecancel_assumption. } eapply Hk.  Qed.
   End Deprecated.
@@ -1057,10 +1057,10 @@ Lemma compile_byte_memcpy (n : nat) (bs bs2 : list byte) :
     }
   Qed.
 
-  
+
 Lemma compile_word_memcpy (n : nat) (bs bs2 : list word) :
   let v := copy bs in
-  forall (e : list (String.string  * Syntax.func)) P (pred: P v -> predicate) (k: nlet_eq_k P v) k_impl
+  forall (e : env) P (pred: P v -> predicate) (k: nlet_eq_k P v) k_impl
          len a a2 len_expr a_expr a2_var t m l (R: mem -> Prop),
 
     map.get l a2_var = Some a2 ->
@@ -1109,12 +1109,12 @@ Proof using Type.
   rewrite !memcpy_identity in H10; eauto.
 Qed.
 
-  
+
 End CompileBufPolymorphic.
 
 
 
-  
+
 
 Ltac compile_buf_append:=
   lazymatch goal with
@@ -1129,7 +1129,7 @@ Hint Extern 8 (WeakestPrecondition.cmd _ _ _ _ _ (_ (nlet_eq _ (buf_append _ _)
        compile_buf_append; shelve : compiler.
 
 Section CompileBufByte.
-  Context (e : list (String.string * Syntax.func)).
+  Context (e : env).
   Context (T := byte) (sz : word := word.of_Z 1) (pT := ptsto(map:=mem)).
 
   Declare Scope word_scope.
@@ -1228,7 +1228,7 @@ Section CompileBufByte.
 End CompileBufByte.
 
 Section CompileBufWord32.
-  Context (e : list (String.string  * Syntax.func)).
+  Context (e : env).
   Context (T := word) (sz : word := word.of_Z 4) (pT := scalar32(word:=word)).
 
   Declare Scope word_scope.
@@ -1757,7 +1757,7 @@ Proof.
 
   unfold *)
    *)
-  
+
   Abort.
 (*  lia.
   admit.
@@ -1784,7 +1784,7 @@ Proof.
   repeat compile_step.
   rewrite poly1305_loop_nil.
   unfold nlet at 1.*)
-  
+
 
 (** ** Equivalence proof **)
 
diff --git a/src/Bedrock/End2End/X25519/Field25519.v b/src/Bedrock/End2End/X25519/Field25519.v
index b9a892d016..f3afef1cd0 100644
--- a/src/Bedrock/End2End/X25519/Field25519.v
+++ b/src/Bedrock/End2End/X25519/Field25519.v
@@ -58,76 +58,85 @@ Section Field.
         field pipeline proofs to prove the bedrock2 functions are correct. ****)
 
   Derive fe25519_from_bytes
-         SuchThat (forall functions,
-                      spec_of_from_bytes
-                        (ext_spec:=ext_spec)
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_from_bytes :: functions))
-         As fe25519_from_bytes_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_from_bytes" = Some fe25519_from_bytes ->
+      spec_of_from_bytes
+        (ext_spec:=ext_spec)
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_from_bytes_correct.
   Proof. Time derive_bedrock2_func from_bytes_op. Qed.
 
   Derive fe25519_to_bytes
-         SuchThat (forall functions,
-                      spec_of_to_bytes
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_to_bytes :: functions))
-         As fe25519_to_bytes_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_to_bytes" = Some fe25519_to_bytes ->
+      spec_of_to_bytes
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_to_bytes_correct.
   Proof. Time derive_bedrock2_func to_bytes_op. Qed.
 
   Derive fe25519_copy
-         SuchThat (forall functions,
-                      spec_of_felem_copy
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_copy :: functions))
-         As fe25519_copy_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_copy" = Some fe25519_copy ->
+      spec_of_felem_copy
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_copy_correct.
   Proof. Time derive_bedrock2_func felem_copy_op. Qed.
 
   Derive fe25519_from_word
-         SuchThat (forall functions,
-                      spec_of_from_word
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_from_word :: functions))
-         As fe25519_from_word_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_from_word" = Some fe25519_from_word ->
+      spec_of_from_word
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_from_word_correct.
   Proof. Time derive_bedrock2_func from_word_op. Qed.
 
   Derive fe25519_mul
-         SuchThat (forall functions,
-                      spec_of_BinOp bin_mul
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_mul :: functions))
-         As fe25519_mul_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_mul" = Some fe25519_mul ->
+      spec_of_BinOp bin_mul
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_mul_correct.
   Proof. Time derive_bedrock2_func mul_op. Qed.
 
   Derive fe25519_square
-         SuchThat (forall functions,
-                      spec_of_UnOp un_square
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_square :: functions))
-         As fe25519_square_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_square" = Some fe25519_square ->
+      spec_of_UnOp un_square
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_square_correct.
   Proof. Time derive_bedrock2_func square_op. Qed.
 
   Derive fe25519_add
-         SuchThat (forall functions,
-                      spec_of_BinOp bin_add
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_add :: functions))
-         As fe25519_add_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_add" = Some fe25519_add ->
+      spec_of_BinOp bin_add
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_add_correct.
   Proof. Time derive_bedrock2_func add_op. Qed.
 
   Derive fe25519_sub
-         SuchThat (forall functions,
-                      spec_of_BinOp bin_sub
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_sub :: functions))
-         As fe25519_sub_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_sub" = Some fe25519_sub ->
+      spec_of_BinOp bin_sub
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_sub_correct.
   Proof. Time derive_bedrock2_func sub_op. Qed.
 
   Derive fe25519_scmula24
-         SuchThat (forall functions,
-                      spec_of_UnOp un_scmula24
-                        (field_representation:=field_representation n s c)
-                        (&,fe25519_scmula24 :: functions))
-         As fe25519_scmula24_correct.
+    SuchThat (forall functions,
+      Interface.map.get functions "fe25519_scmula24" = Some fe25519_scmula24 ->
+      spec_of_UnOp un_scmula24
+        (field_representation:=field_representation n s c)
+        functions)
+    As fe25519_scmula24_correct.
   Proof. Time derive_bedrock2_func scmula24_op. Qed.
 
   #[export] Instance frep25519_ok : FieldRepresentation_ok(field_representation:=field_representation n s c).
diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
index 8829a959da..a412768b72 100644
--- a/src/Bedrock/End2End/X25519/GarageDoorTop.v
+++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -64,27 +64,62 @@ Compute (length funcs-3 - (length MontgomeryLadder.funcs - 2 + 3))%nat. (* handw
 Compute bedrock2.ToCString.c_module funcs.
 *)
 
-Lemma chacha20_ok: forall functions, ChaCha20.spec_of_chacha20 (&,ChaCha20.chacha20_block::&,ChaCha20.quarter::functions).
+Lemma chacha20_ok: forall functions,
+    map.get functions "chacha20_block" = Some ChaCha20.chacha20_block ->
+    map.get functions "quarter" = Some ChaCha20.quarter ->
+    ChaCha20.spec_of_chacha20 functions.
+Proof.
   intros.
-  simple eapply ChaCha20.chacha20_block_body_correct.
-  constructor.
-  eapply ChaCha20.quarter_body_correct.
-  constructor.
+  simple eapply ChaCha20.chacha20_block_body_correct; [constructor | eassumption | ].
+  eapply ChaCha20.quarter_body_correct; [constructor | eassumption ].
 Qed.
 
+Ltac pose_correctness lem :=
+  let H := fresh in
+  pose proof (lem (map.of_list funcs)) as H;
+  unfold program_logic_goal_for in H;
+  repeat lazymatch type of H with
+    | map.get (map.of_list _) _ = Some _ -> _ => specialize (H eq_refl)
+    end.
+
 Import SPI.
-Lemma link_loopfn : spec_of_loopfn funcs.
+Lemma link_loopfn : spec_of_loopfn (map.of_list funcs).
 Proof.
-  eapply loopfn_ok; try eapply memswap.memswap_ok; try eapply memequal_ok.
-    repeat (eapply recvEthernet_ok || eapply lightbulb_handle_ok);
-        eapply lan9250_readword_ok; eapply spi_xchg_ok;
-        (eapply spi_write_ok || eapply spi_read_ok).
-    eapply ip_checksum_br2fn_ok; exact I.
-    eapply x25519_base_ok; try eapply fe25519_from_word_correct; try eapply link_montladder; try eapply fe25519_to_bytes_correct.
-    eapply lan9250_tx_ok; try eapply lan9250_writeword_ok; try eapply spi_xchg_ok; (eapply spi_write_ok || eapply spi_read_ok).
-    eapply x25519_ok; try eapply fe25519_from_bytes_correct; try eapply link_montladder; try eapply fe25519_to_bytes_correct.
-    eapply chacha20_ok.
-Qed. Optimize Heap.
+  pose_correctness loopfn_ok.
+  pose_correctness memswap.memswap_ok.
+  pose_correctness memequal_ok.
+  pose_correctness recvEthernet_ok.
+  pose_correctness lan9250_readword_ok.
+  pose_correctness spi_xchg_ok.
+  pose_correctness spi_write_ok.
+  pose_correctness spi_read_ok.
+  pose_correctness (ip_checksum_br2fn_ok I).
+  pose_correctness x25519_base_ok.
+  pose_correctness fe25519_from_word_correct.
+  pose_correctness fe25519_to_bytes_correct.
+  pose_correctness lan9250_tx_ok.
+  pose_correctness lan9250_writeword_ok.
+  pose_correctness x25519_ok.
+  pose_correctness fe25519_from_bytes_correct.
+  pose_correctness chacha20_ok.
+  assert (spec_of_montladder (map.of_list funcs)). {
+    unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
+    intros.
+    eapply WP.extend_env_wp_call.
+    2: { eapply link_montladder. eassumption. }
+    clear. unfold funcs.
+    (* TODO this could be more computational *)
+    intros k v G.
+    unfold MontgomeryLadder.funcs, map.of_list in G.
+    rewrite ?map.get_put_dec in G.
+    repeat (destruct_one_match_hyp; [inversion G; subst; reflexivity | ]).
+    rewrite map.get_empty in G. discriminate G.
+  }
+  repeat match goal with
+         | HI: ?A -> _, HA: ?A |- _ => specialize (HI HA)
+         end.
+  assumption.
+Qed.
 
 Require compiler.ToplevelLoop.
 Definition ml: MemoryLayout.MemoryLayout(word:=Naive.word32) := {|
@@ -147,15 +182,23 @@ Proof.
   case H as (?&?&?&?&?&H); eauto.
 Qed.
 
-Lemma link_initfn : spec_of_initfn funcs.
+Lemma link_initfn : spec_of_initfn (map.of_list funcs).
 Proof.
-  eapply initfn_ok.
-  eapply memconst_ok.
-  eapply lan9250_init_ok;
-    try (eapply lan9250_wait_for_boot_ok || eapply lan9250_mac_write_ok);
-    (eapply lan9250_readword_ok || eapply lan9250_writeword_ok);
-        eapply spi_xchg_ok;
-        (eapply spi_write_ok || eapply spi_read_ok).
+  pose_correctness initfn_ok.
+  pose_correctness lan9250_init_ok.
+  pose_correctness lan9250_wait_for_boot_ok.
+  pose_correctness lan9250_mac_write_ok.
+  pose_correctness lan9250_readword_ok.
+  pose_correctness lan9250_writeword_ok.
+  pose_correctness spi_xchg_ok.
+  pose_correctness spi_write_ok.
+  pose_correctness spi_read_ok.
+  unfold spec_of_memconst_pk in *.
+  pose_correctness (memconst_ok "memconst_pk" garageowner).
+  repeat match goal with
+         | HI: ?A -> _, HA: ?A |- _ => specialize (HI HA)
+         end.
+  assumption.
 Qed. Optimize Heap.
 
 Import ToplevelLoop GoFlatToRiscv regs_initialized LowerPipeline.
@@ -202,12 +245,10 @@ Proof.
   1: instantiate (1:=snd init).
   3: instantiate (1:=snd loop).
   1,3: exact eq_refl.
-  1,2: cbv [hl_inv]; intros; eapply WeakestPreconditionProperties.sound_cmd.
-  1,3: eapply Crypto.Util.Bool.Reflect.reflect_bool; vm_compute; reflexivity.
+  1,2: cbv [hl_inv]; intros; eapply MetricSemantics.of_metrics_free; eapply WeakestPreconditionProperties.sound_cmd.
 
   all : repeat straightline; subst args.
-  { repeat straightline.
-    cbv [LowerPipeline.mem_available LowerPipeline.ptsto_bytes] in *.
+  { cbv [LowerPipeline.mem_available LowerPipeline.ptsto_bytes] in *.
     cbv [datamem_pastend datamem_start garagedoor_spec heap_start heap_pastend ml] in H6.
     SeparationLogic.extract_ex1_and_emp_in H6.
     change (BinIntDef.Z.of_nat (Datatypes.length anybytes) = 0x2000) in H6_emp0.
@@ -257,5 +298,5 @@ Qed.
 
 (*
 Print Assumptions link_loopfn. (* Closed under the global context *)
-Print Assumptions invariant_proof. (* propositional_extensionality, functional_extensionality_dep *)
+Print Assumptions garagedoor_invariant_proof. (* propositional_extensionality, functional_extensionality_dep *)
 *)
diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v b/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
index 2b0cef4ee2..cf491b9cea 100644
--- a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
+++ b/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
@@ -54,110 +54,40 @@ Local Instance Registers : map.map Z (@word.rep 32 Naive.word32)
 
 Require Import riscv.Spec.Decode.
 
-(* TODO: does something like this already exist? *)
-(* when the function name being called is not first in the list of functions,
-   peel off non-matching names *)
-Local Ltac prepare_call_step :=
-  lazymatch goal with
-  | |- ?call (?f :: ?funcs) ?fname ?t ?m ?args ?post =>
-    assert_fails (unify (fst f) fname);
-    let H := fresh in
-    assert (call funcs fname t m args post) as H;
-    [ | remember funcs; rewrite (surjective_pairing f);
-        cbn [WeakestPrecondition.call WeakestPrecondition.call_body ];
-        lazymatch goal with |- context[if (String.eqb ?x ?y) then _ else _] =>
-          let x' := (eval vm_compute in x) in change x with x';
-          let y' := (eval vm_compute in y) in change y with y';
-          destr (String.eqb x' y'); [ congruence | ]
-        end; exact H ]
-  end.
-Local Ltac prepare_call := repeat prepare_call_step.
-
-(* TODO: move to Spec.Field? *)
-Section Generic.
-  Context {width : Z} {BW : Bitwidth width} {word : word width}
-          {mem : map.map word.rep (Init.Byte.byte : Type)}
-          {locals : map.map string (word.rep (word:=word))}
-          {ext_spec : Semantics.ExtSpec}
-          {field_parameters : FieldParameters}
-          {field_representation : FieldRepresentation}.
-
-  Lemma peel_func_binop
-      {name} (op : BinOp name) funcs0 funcs :
-    fst funcs0 <> name ->
-    spec_of_BinOp op funcs ->
-    spec_of_BinOp op (funcs0 :: funcs).
-  Proof.
-    cbv [spec_of_BinOp binop_spec]; intros.
-    cbn [WeakestPrecondition.call WeakestPrecondition.call_body ].
-    destruct funcs0; cbn [fst snd] in *.
-    lazymatch goal with |- context[if (String.eqb ?x ?y) then _ else _] =>
-      destr (String.eqb x y); [ congruence | ]
-    end.
-    eauto.
-  Qed.
-
-  Lemma peel_func_unop
-      {name} (op : UnOp name) funcs0 funcs :
-    fst funcs0 <> name ->
-    spec_of_UnOp op funcs ->
-    spec_of_UnOp op (funcs0 :: funcs).
-  Proof.
-    cbv [spec_of_UnOp unop_spec]; intros.
-    cbn [WeakestPrecondition.call WeakestPrecondition.call_body ].
-    destruct funcs0; cbn [fst snd] in *.
-    lazymatch goal with |- context[if (String.eqb ?x ?y) then _ else _] =>
-      destr (String.eqb x y); [ congruence | ]
-    end.
-    eauto.
-  Qed.
-
-End Generic.
-
 Local Instance naive_word_riscv_ok :
   RiscvWordProperties.word.riscv_ok Naive.word32 := naive_word_riscv_ok 5.
 
-Lemma link_montladder : spec_of_montladder funcs.
+Lemma link_montladder : spec_of_montladder (map.of_list funcs).
 Proof.
     unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
     unfold funcs.
-    (* montladder is not at the front of the function list; remove everything
-       that doesn't match the name *)
-    prepare_call.
     (* use montladder correctness proof *)
     rewrite montladder_defn.
     eapply @montladder_correct; try (typeclasses eauto).
     { reflexivity. }
     { cbv [Core.__rupicola_program_marker]. tauto. }
     { exact I. }
-    { eapply CSwap.cswap_body_correct; [|exact I].
+    { reflexivity. }
+    { eapply CSwap.cswap_body_correct; [|exact I|reflexivity].
       unfold field_representation, Signature.field_representation, Representation.frep; cbn; unfold n; cbv; trivial. }
-    { eapply fe25519_copy_correct. }
-    { eapply fe25519_from_word_correct. }
+    { eapply fe25519_copy_correct. reflexivity. }
+    { eapply fe25519_from_word_correct. reflexivity. }
     {
       cbv [LadderStep.spec_of_ladderstep]; intros.
-      prepare_call. rewrite ladderstep_defn.
+      rewrite ladderstep_defn.
       eapply @LadderStep.ladderstep_correct; try (typeclasses eauto).
       { cbv [Core.__rupicola_program_marker]; tauto. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_mul_correct. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_add_correct. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_sub_correct. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_square_correct. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_scmula24_correct. }
+      { reflexivity. }
+      { apply fe25519_mul_correct. reflexivity. }
+      { apply fe25519_add_correct. reflexivity. }
+      { apply fe25519_sub_correct. reflexivity. }
+      { apply fe25519_square_correct. reflexivity. }
+      { apply fe25519_scmula24_correct. reflexivity. }
       { ecancel_assumption. } }
-    { repeat (apply peel_func_unop; [ lazy; congruence | ]).
-      unshelve eapply AdditionChains.fe25519_inv_correct_exp; try exact I.
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_square_correct. }
-      { repeat (apply peel_func_binop; [ lazy; congruence | ]).
-        apply fe25519_mul_correct. } }
-    { repeat (apply peel_func_unop; [ lazy; congruence | ]).
-      apply fe25519_mul_correct. }
+    { unshelve eapply AdditionChains.fe25519_inv_correct_exp; [exact I|reflexivity| | ].
+      { apply fe25519_square_correct. reflexivity. }
+      { apply fe25519_mul_correct. reflexivity. } }
+    { apply fe25519_mul_correct. reflexivity. }
 Qed.
 
 Lemma montladder_compiles_correctly :
diff --git a/src/Bedrock/Field/Common/Arrays/ByteBounds.v b/src/Bedrock/Field/Common/Arrays/ByteBounds.v
index e61c8afed6..ee56119832 100644
--- a/src/Bedrock/Field/Common/Arrays/ByteBounds.v
+++ b/src/Bedrock/Field/Common/Arrays/ByteBounds.v
@@ -20,9 +20,9 @@ Import ListNotations.
 Import Partition.
 
 Section ByteBounds.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Context (n : nat).
 
diff --git a/src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v b/src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v
index 62fc258708..69f5974335 100644
--- a/src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v
+++ b/src/Bedrock/Field/Common/Arrays/MakeAccessSizes.v
@@ -22,9 +22,9 @@ Import AbstractInterpretation.Compilers.
 Import Types.Notations.
 
 Section __.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Existing Instances rep.Z rep.listZ_mem.
 
   Let all_access_sizes :=
diff --git a/src/Bedrock/Field/Common/Arrays/MakeListLengths.v b/src/Bedrock/Field/Common/Arrays/MakeListLengths.v
index a6dc4192b1..cde86dca51 100644
--- a/src/Bedrock/Field/Common/Arrays/MakeListLengths.v
+++ b/src/Bedrock/Field/Common/Arrays/MakeListLengths.v
@@ -11,9 +11,9 @@ Import Types.Notations.
 Existing Instances rep.Z rep.listZ_mem.
 
 Section with_parameters.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
 
   Fixpoint list_lengths_repeat_base (n : nat) t : base_listonly nat t :=
     match t as t0 return base_listonly nat t0 with
diff --git a/src/Bedrock/Field/Common/Arrays/MaxBounds.v b/src/Bedrock/Field/Common/Arrays/MaxBounds.v
index dfab750aa9..a1037573f1 100644
--- a/src/Bedrock/Field/Common/Arrays/MaxBounds.v
+++ b/src/Bedrock/Field/Common/Arrays/MaxBounds.v
@@ -19,9 +19,9 @@ Local Open Scope Z_scope.
 Import ListNotations.
 
 Section MaxBounds.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Context (n : nat).
 
diff --git a/src/Bedrock/Field/Common/Names/MakeNames.v b/src/Bedrock/Field/Common/Names/MakeNames.v
index c7cd34a74b..dbcf17a350 100644
--- a/src/Bedrock/Field/Common/Names/MakeNames.v
+++ b/src/Bedrock/Field/Common/Names/MakeNames.v
@@ -19,9 +19,9 @@ Import ListNotations.
 Existing Instances rep.Z rep.listZ_mem.
 
 Section with_parameters.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {inname_gen outname_gen : nat -> string}.
 
   Fixpoint make_names
diff --git a/src/Bedrock/Field/Common/Types.v b/src/Bedrock/Field/Common/Types.v
index f257844d07..fac2dbeefb 100644
--- a/src/Bedrock/Field/Common/Types.v
+++ b/src/Bedrock/Field/Common/Types.v
@@ -35,16 +35,15 @@ End Notations.
 Class parameters
   {width: Z} {BW: Bitwidth.Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}
   {locals: map.map String.string word}
-  {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}
   {ext_spec: bedrock2.Semantics.ExtSpec}
   {varname_gen : nat -> String.string}
   {error : Syntax.expr.expr} := parameters_sentinel : unit.
 
 Section WithParameters.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
    `{parameters_sentinel : @parameters
-     width BW word mem locals env ext_spec varname_gen error}.
+     width BW word mem locals ext_spec varname_gen error}.
   Local Notation parameters := (ltac:(let t := type of parameters_sentinel in exact t)) (only parsing).
   Class ok {parameters_sentinel : parameters} :=
     {
@@ -52,7 +51,6 @@ Section WithParameters.
       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;
 
       varname_gen_unique :
@@ -68,10 +66,10 @@ End WithParameters.
 
 Module rep.
   Section rep.
-    Context 
-      {width BW word mem locals env ext_spec varname_gen error}
+    Context
+      {width BW word mem locals ext_spec varname_gen error}
      `{parameters_sentinel : @parameters
-       width BW word mem locals env ext_spec varname_gen error}.
+       width BW word mem locals ext_spec varname_gen error}.
     Local Notation parameters := (ltac:(let t := type of parameters_sentinel in exact t)) (only parsing).
 
     Class rep {parameters_sentinel : parameters} (t : base.type) :=
@@ -161,9 +159,9 @@ End rep.
 
 Section defs.
   Context
-    {width BW word mem locals env ext_spec varname_gen error}
+    {width BW word mem locals ext_spec varname_gen error}
    `{parameters_sentinel : @parameters
-     width BW word mem locals env ext_spec varname_gen error}.
+     width BW word mem locals ext_spec varname_gen error}.
   Local Notation parameters := (ltac:(let t := type of parameters_sentinel in exact t)) (only parsing).
   Context
           (* list representation -- could be local or in-memory *)
diff --git a/src/Bedrock/Field/Common/Util.v b/src/Bedrock/Field/Common/Util.v
index 0f9fcd8b0a..1b4a3130ac 100644
--- a/src/Bedrock/Field/Common/Util.v
+++ b/src/Bedrock/Field/Common/Util.v
@@ -796,11 +796,9 @@ Section WeakestPrecondition.
   Import Bitwidth bedrock2.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 * 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}.
 
   (* "expr" should not be Compilers.expr; can remove once upstreamed *)
@@ -993,8 +991,8 @@ Section WeakestPrecondition.
                        match goal with
                        | |- expr m l e _ => idtac
                        | _ =>
-                         apply expr_sound with (mc:=MetricLogging.EmptyMetricLog) in H;
-                         destruct H as [? [_ [_ H] ] ]
+                         apply expr_sound in H;
+                         destruct H as [? [_ H] ]
                        end
                      end).
 
diff --git a/src/Bedrock/Field/Interface/Compilation2.v b/src/Bedrock/Field/Interface/Compilation2.v
index ddb5fe74ea..c666a029bc 100644
--- a/src/Bedrock/Field/Interface/Compilation2.v
+++ b/src/Bedrock/Field/Interface/Compilation2.v
@@ -7,11 +7,9 @@ Local Open Scope Z_scope.
 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}.
   Context {field_parameters : FieldParameters}
           {field_representaton : FieldRepresentation}
@@ -137,7 +135,7 @@ Section Compile.
         (cmd.call [] name [expr.var out_var; expr.var x_var; expr.var y_var])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     unfold FElem in *.
     sepsimpl.
@@ -182,7 +180,7 @@ Section Compile.
         (cmd.call [] name [expr.var out_var; expr.var x_var])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     unfold FElem in *.
     sepsimpl.
@@ -262,7 +260,7 @@ Section Compile.
         (cmd.call [] felem_copy [expr.var out_var; expr.var x_var])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     unfold FElem in *.
     sepsimpl.
@@ -304,7 +302,7 @@ Section Compile.
                   [expr.var out_var; expr.literal x])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     unfold FElem in *.
     extract_ex1_and_emp_in H1.
@@ -347,7 +345,7 @@ Section Compile.
         (cmd.call [] from_bytes [expr.var out_var; expr.var x_var])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     unfold FElem in *.
     sepsimpl.
@@ -389,7 +387,7 @@ Section Compile.
         (cmd.call [] to_bytes [expr.var out_var; expr.var x_var])
         k_impl
       <{ pred (nlet_eq [out_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     subst v.
     unfold FElem in *.
diff --git a/src/Bedrock/Field/Interface/Representation.v b/src/Bedrock/Field/Interface/Representation.v
index 48c1671281..774c2f3f5b 100644
--- a/src/Bedrock/Field/Interface/Representation.v
+++ b/src/Bedrock/Field/Interface/Representation.v
@@ -17,9 +17,9 @@ Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 
 Section Representation.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {field_parameters : FieldParameters}
           {p_ok : Types.ok}.
   Context (n n_bytes : nat) (weight : nat -> Z)
@@ -43,7 +43,7 @@ Section Representation.
     fun bs =>
       F.of_Z _ (Positional.eval
                            (ModOps.weight 8 1)
-                           n_bytes 
+                           n_bytes
                            (map byte.unsigned bs)).
 
   Local Instance frep : FieldRepresentation := {
diff --git a/src/Bedrock/Field/Stringification/Stringification.v b/src/Bedrock/Field/Stringification/Stringification.v
index 1614a80e57..9ae50c049b 100644
--- a/src/Bedrock/Field/Stringification/Stringification.v
+++ b/src/Bedrock/Field/Stringification/Stringification.v
@@ -28,9 +28,9 @@ Local Open Scope string_scope.
 Local Open Scope list_scope.
 
 Section with_parameters.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
 
   Fixpoint make_base_var_data {t}
     : base_ltype t -> list_lengths (type.base t) ->
@@ -114,8 +114,8 @@ Definition bedrock_func_to_lines (f : string * func)
   [c_func f].
 
 Definition wrap_call
-  {width BW word mem locals env ext_spec varname_gen error}
-  `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}
+  {width BW word mem locals ext_spec varname_gen error}
+  `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}
            {t}
            (indata : type.for_each_lhs_of_arrow var_data t)
            (outdata : base_var_data (type.final_codomain t))
@@ -185,7 +185,6 @@ Definition Bedrock2_ToFunctionLines
         (word:=Naive.word width)
         (locals:=SortedListString.map _)
         (mem:=SortedListWord.map(word_ok:=Naive.ok width width_pos) _ _)
-        (env:=SortedListString.map _)
         (ext_spec:=fun _ _ _ _ _ => False)
         (varname_gen := default_varname_gen)
         (error := expr.var Defaults.ERROR)
diff --git a/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v b/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v
index 25dc8f6ebc..ecb743e162 100644
--- a/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v
+++ b/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v
@@ -46,7 +46,7 @@ Section Field.
   Definition from_mont_string := prefix ++ "from_mont".
 
   (* Call fiat-crypto pipeline on all field operations *)
-  Instance p224_ops : @word_by_word_Montgomery_ops from_mont_string to_mont_string _ _ _ _ _ _ _ _ _ _ _ (WordByWordMontgomery.n m machine_wordsize) m.
+  Instance p224_ops : @word_by_word_Montgomery_ops from_mont_string to_mont_string _ _ _ _ _ _ _ _ _ _ (WordByWordMontgomery.n m machine_wordsize) m.
   Proof using Type. Time constructor; make_computed_op. Defined.
 
 
@@ -65,7 +65,16 @@ Section Field.
         | |- context [spec_of_to_bytes] => eapply to_bytes_func_correct
         end.
 
-      Ltac derive_bedrock2_func op :=
+        Ltac epair :=
+          lazymatch goal with
+          | f := _ : string * Syntax.func |- _ =>
+            let p := open_constr:((_, _)) in
+            unify f p;
+            subst f
+          end.
+
+        Ltac derive_bedrock2_func op :=
+        epair;
         begin_derive_bedrock2_func;
         (* this goal fills in the evar, so do it first for [abstract] to be happy *)
         try lazymatch goal with
@@ -81,62 +90,73 @@ Section Field.
         | |- (_ = _)%Z => vm_compute; reflexivity
         end.
 
+  Local Notation functions_contain functions f :=
+    (Interface.map.get functions (fst f) = Some (snd f)).
+
   Derive p224_from_bytes
          SuchThat (forall functions,
+                      functions_contain functions p224_from_bytes ->
                       spec_of_from_bytes
                         (field_representation:=field_representation_raw m)
-                        (p224_from_bytes :: functions))
+                        functions)
          As p224_from_bytes_correct.
   Proof. Time derive_bedrock2_func from_bytes_op. Qed.
 
   Derive p224_to_bytes
          SuchThat (forall functions,
+                      functions_contain functions p224_to_bytes ->
                       spec_of_to_bytes
                         (field_representation:=field_representation_raw m)
-                        (p224_to_bytes :: functions))
+                        functions)
          As p224_to_bytes_correct.
   Proof. Time derive_bedrock2_func to_bytes_op. Qed.
 
   Derive p224_mul
          SuchThat (forall functions,
+                      functions_contain functions p224_mul ->
                       spec_of_BinOp bin_mul
                         (field_representation:=field_representation m)
-                        (p224_mul :: functions))
+                        functions)
          As p224_mul_correct.
   Proof. Time derive_bedrock2_func mul_op. Qed.
 
   Derive p224_square
          SuchThat (forall functions,
+                      functions_contain functions p224_square ->
                       spec_of_UnOp un_square
                         (field_representation:=field_representation m)
-                        (p224_square :: functions))
+                        functions)
          As p224_square_correct.
   Proof. Time derive_bedrock2_func square_op. Qed.
 
   Derive p224_add
          SuchThat (forall functions,
+                      functions_contain functions p224_add ->
                       spec_of_BinOp bin_add
                         (field_representation:=field_representation m)
-                        (p224_add :: functions))
+                        functions)
          As p224_add_correct.
   Proof. Time derive_bedrock2_func add_op. Qed.
 
   Derive p224_sub
          SuchThat (forall functions,
+                      functions_contain functions p224_sub ->
                       spec_of_BinOp bin_sub
                         (field_representation:=field_representation m)
-                        (p224_sub :: functions))
+                        functions)
          As p224_sub_correct.
   Proof. Time derive_bedrock2_func sub_op. Qed.
 
   (*TODO: adapt derive_bedrock2_func to also derive the remaining functions.*)
   Derive p224_from_mont
          SuchThat (forall functions,
+                      functions_contain functions p224_from_mont ->
                       spec_of_UnOp un_from_mont
                         (field_representation:=field_representation m)
-                        (p224_from_mont :: functions))
+                        functions)
          As p224_from_mont_correct.
   Proof.
+    epair.
     eapply (from_mont_func_correct _ _ _ from_mont_string to_mont_string).
         - vm_compute; reflexivity.
         - eapply Func.valid_func_bool_iff. abstract vm_cast_no_check (eq_refl true).
@@ -147,11 +167,13 @@ Section Field.
 
   Derive p224_to_mont
          SuchThat (forall functions,
+                      functions_contain functions p224_to_mont ->
                       spec_of_UnOp un_to_mont
                         (field_representation:=field_representation m)
-                        (p224_to_mont :: functions))
+                        functions)
          As to_from_mont_correct.
   Proof.
+    epair.
     eapply (to_mont_func_correct _ _ _ from_mont_string to_mont_string).
         - vm_compute; reflexivity.
         - eapply Func.valid_func_bool_iff. abstract vm_cast_no_check (eq_refl true).
@@ -160,11 +182,13 @@ Section Field.
 
   Derive p224_select_znz
            SuchThat (forall functions,
+                      functions_contain functions p224_select_znz ->
                       spec_of_selectznz
                         (field_representation:=field_representation m)
-                        (p224_select_znz :: functions))
+                        functions)
          As select_znz_correct.
   Proof.
+    epair.
     eapply select_znz_func_correct. 1,2:auto.
         - vm_compute; reflexivity.
         - eapply Func.valid_func_bool_iff. abstract vm_cast_no_check (eq_refl true).
diff --git a/src/Bedrock/Field/Synthesis/New/ComputedOp.v b/src/Bedrock/Field/Synthesis/New/ComputedOp.v
index faf87855e9..05771d0f8c 100644
--- a/src/Bedrock/Field/Synthesis/New/ComputedOp.v
+++ b/src/Bedrock/Field/Synthesis/New/ComputedOp.v
@@ -6,8 +6,8 @@ Require Import Crypto.Language.API.
 Import API.Compilers.
 
 Record computed_op
-      {width BW word mem locals env ext_spec varname_gen error}
-      {parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}
+      {width BW word mem locals ext_spec varname_gen error}
+      {parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}
       {t} {op : Pipeline.ErrorT (API.Expr t)}
       {name : String.string}
       {insizes outsizes inlengths}
@@ -17,7 +17,7 @@ Record computed_op
     res_eq : op = ErrorT.Success res;
     func_eq : b2_func = make_bedrock_func insizes outsizes inlengths res;
   }.
-Global Arguments computed_op {_ _ _ _ _ _ _ _ _ _ t}.
+Global Arguments computed_op {_ _ _ _ _ _ _ _ _ t}.
 
 Ltac make_computed_op :=
   eapply Build_computed_op;
diff --git a/src/Bedrock/Field/Synthesis/New/Signature.v b/src/Bedrock/Field/Synthesis/New/Signature.v
index 0e5a567f72..1aaac6b308 100644
--- a/src/Bedrock/Field/Synthesis/New/Signature.v
+++ b/src/Bedrock/Field/Synthesis/New/Signature.v
@@ -36,9 +36,9 @@ Import Syntax.Coercions.
 Local Open Scope Z_scope.
 
 Section Generic.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Definition make_bedrock_func {t} insizes outsizes inlengths (res : API.Expr t)
   : func :=
     let innames := make_innames (inname_gen:=default_inname_gen) _ in
@@ -80,9 +80,9 @@ Local Hint Resolve MakeAccessSizes.bits_per_word_le_width
   : translate_func_preconditions.
 
 Section WithParameters.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : Types.ok}
           {field_parameters : FieldParameters}.
   Context (n n_bytes : nat) (weight : nat -> Z)
@@ -187,26 +187,30 @@ Section WithParameters.
 
   Ltac compute_names :=
     repeat lazymatch goal with
-           | |- context [@make_innames ?w ?B ?W ?M ?L ?E ?X ?G ?R ?p ?gen ?t] =>
-             let x := constr:(@make_innames w B W M L E X G R p gen t) in
+           | |- context [@make_innames ?w ?B ?W ?M ?L ?X ?G ?R ?p ?gen ?t] =>
+             let x := constr:(@make_innames w B W M L X G R p gen t) in
              let y := (eval compute in x) in
              change x with y
-           | |- context [@make_outnames  ?w ?B ?W ?M ?L ?E ?X ?G ?R ?p ?gen ?t] =>
-             let x := constr:(@make_outnames w B W M L E X G R p gen t) in
+           | |- context [@make_outnames  ?w ?B ?W ?M ?L ?X ?G ?R ?p ?gen ?t] =>
+             let x := constr:(@make_outnames w B W M L X G R p gen t) in
              let y := (eval compute in x) in
              change x with y
            end.
 
   Ltac use_translate_func_correct b2_args R_ :=
-    let arg_ptrs :=
-        lazymatch goal with
-          |- WeakestPrecondition.call _ _ _ _ ?args _ =>
-          args end in
-    let out_ptr := (eval compute in (hd (word.of_Z 0) arg_ptrs)) in
-    let in_ptrs := (eval compute in (tl arg_ptrs)) in
-    eapply (translate_func_correct (parameters_sentinel:=parameters_sentinel))
-    with (out_ptrs:=[out_ptr]) (flat_args:=in_ptrs)
-         (args:=b2_args) (R:=R_).
+    lazymatch goal with
+    | H: map.get ?functions ?name =
+           Some (fst (translate_func ?e0 ?argns ?argls ?argszs ?retns ?retszs))
+      |- WeakestPrecondition.call ?functions ?name _ _ ?arg_ptrs _ =>
+        let out_ptr := (eval compute in (hd (word.of_Z 0) arg_ptrs)) in
+        let in_ptrs := (eval compute in (tl arg_ptrs)) in
+        eapply (translate_func_correct (parameters_sentinel:=parameters_sentinel))
+          with (out_ptrs:=[out_ptr]) (flat_args:=in_ptrs)
+               (e:=e0) (argnames:=argns) (arglengths:=argls) (argsizes:=argszs)
+               (retnames:=retns) (retsizes:=retszs)
+               (args:=b2_args) (R:=R_);
+        [ .. | exact H]
+    end.
 
   Ltac types_autounfold :=
     repeat first [ progress autounfold with types pairs
@@ -259,7 +263,7 @@ Section WithParameters.
       sepsimpl; crush_sep; solve [solve_equivalence_side_conditions]
     | |- LoadStoreList.within_access_sizes_args _ _ =>
       autounfold with types access_sizes; cbn; ssplit; trivial;
-      solve_equivalence_side_conditions 
+      solve_equivalence_side_conditions
     | |- LoadStoreList.within_base_access_sizes _ _ =>
       autounfold with types access_sizes;
       first [ eapply MaxBounds.max_bounds_range_iff
@@ -379,11 +383,11 @@ Section WithParameters.
 
     Lemma list_binop_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions, (binop_spec _ ((name, f) :: functions)).
+      forall functions, map.get functions name = Some f -> (binop_spec _ functions).
     Proof.
       subst inlengths insizes outsizes.
       cbv [binop_spec list_binop_insizes list_binop_outsizes list_binop_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta. intros. subst f. cbv [make_bedrock_func] in *.
       cleanup. eapply Proper_call.
       2: {
         use_translate_func_correct
@@ -463,13 +467,13 @@ Section WithParameters.
 
     Lemma list_unop_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions, unop_spec _ ((name, f) :: functions).
+      forall functions, map.get functions name = Some f -> unop_spec _ functions.
     Proof using inname_gen_varname_gen_disjoint outbounds_length
           outbounds_tighter_than_max outname_gen_varname_gen_disjoint
           ok relax_bounds res_Wf res_bounds res_eq res_valid.
       subst inlengths insizes outsizes.
       cbv [unop_spec list_unop_insizes list_unop_outsizes list_unop_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup. eapply Proper_call.
       2: {
         use_translate_func_correct constr:((map word.unsigned x, tt)) Rr.
@@ -537,30 +541,18 @@ Section WithParameters.
 
     Lemma from_word_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions,
-        spec_of_from_word ((from_word, f) :: functions).
+      forall functions, map.get functions from_word = Some f ->
+                        spec_of_from_word functions.
     Proof using inname_gen_varname_gen_disjoint
           outname_gen_varname_gen_disjoint ok relax_bounds res_Wf
           res_bounds res_eq res_valid tight_bounds_tighter_than_max.
       subst inlengths insizes outsizes. cbv [spec_of_from_word].
       cbv [from_word_insizes from_word_outsizes from_word_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup.
       eapply Proper_call.
       2:{
-        (* inlined [use_translate_func_correct constr:((word.unsigned x, tt)) R] and edited R0 *)
-        let b2_args := constr:((word.unsigned x, tt)) in
-        let R_ := R in
-        let arg_ptrs :=
-          lazymatch goal with
-          |- WeakestPrecondition.call _ _ _ _ ?args _ =>
-          args end in
-          let out_ptr := (eval compute in (hd (word.of_Z 0) arg_ptrs)) in
-          let in_ptrs := (eval compute in (tl arg_ptrs)) in
-          eapply (translate_func_correct (parameters_sentinel:=parameters_sentinel))
-          with (out_ptrs:=[out_ptr]) (flat_args:=in_ptrs)
-          (args:=b2_args).
-        16:instantiate (1:=R).
+        use_translate_func_correct constr:((word.unsigned x, tt)) R.
         all:try translate_func_precondition_hammer.
         1:reflexivity.
         { cbv [Equivalence.equivalent_flat_args]; eexists 1%nat; split; [eexists|reflexivity].
@@ -645,11 +637,12 @@ Section WithParameters.
 
     Lemma felem_copy_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions, spec_of_felem_copy ((felem_copy, f) :: functions).
+      forall functions, map.get functions felem_copy = Some f ->
+                        spec_of_felem_copy functions.
     Proof.
       subst inlengths insizes outsizes.
       cbv [spec_of_felem_copy felem_copy_insizes felem_copy_outsizes felem_copy_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup. eapply Proper_call.
       2: {
         rename R into Rr.
@@ -661,7 +654,7 @@ Section WithParameters.
           cbn [type.app_curried fst snd].
           apply res_bounds.
           rewrite max_bounds_range_iff.
-          seprewrite_in @FElem_array_truncated_scalar_iff1 H0; extract_ex1_and_emp_in H0.
+          seprewrite_in @FElem_array_truncated_scalar_iff1 H1; extract_ex1_and_emp_in H1.
           ssplit; rewrite ?map_length; trivial.
           eapply List.Forall_map, Forall_forall; intros.
           rewrite MakeAccessSizes.bits_per_word_eq_width.
@@ -669,8 +662,8 @@ Section WithParameters.
         { (* lists_reserved_with_initial_context *)
           lists_reserved_simplify pout.
           all:try solve_equivalence_side_conditions;
-          seprewrite_in (FElem_array_truncated_scalar_iff1 pout) H0; extract_ex1_and_emp_in H0; try eassumption.
-          seprewrite_in (FElem_array_truncated_scalar_iff1 px) H0; extract_ex1_and_emp_in H0.
+          seprewrite_in (FElem_array_truncated_scalar_iff1 pout) H1; extract_ex1_and_emp_in H1; try eassumption.
+          seprewrite_in (FElem_array_truncated_scalar_iff1 px) H1; extract_ex1_and_emp_in H1.
           setoid_rewrite max_bounds_range_iff in res_bounds.
           rewrite (fun x pf => proj1 (res_bounds x pf)), ?map_length; trivial.
           ssplit; rewrite ?map_length; trivial.
@@ -684,9 +677,9 @@ Section WithParameters.
       cbn [List.hd] in *. rewrite MakeAccessSizes.bytes_per_word_eq.
       extract_ex1_and_emp_in_goal; ssplit;
         try (use_sep_assumption; cancel; cbv [seps]);
-        seprewrite_in (FElem_array_truncated_scalar_iff1 px) H0; extract_ex1_and_emp_in H0; trivial.
+        seprewrite_in (FElem_array_truncated_scalar_iff1 px) H1; extract_ex1_and_emp_in H1; trivial.
       Morphisms.f_equiv.
-      rewrite H4.
+      rewrite H5.
       rewrite <-(res_eq x) at 2 by trivial.
       rewrite Util.map_unsigned_of_Z.
       erewrite map_word_wrap_bounded; trivial.
@@ -755,15 +748,15 @@ Section WithParameters.
     Import coqutil.Macros.symmetry.
     Lemma from_bytes_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions,
-        spec_of_from_bytes ((from_bytes, f) :: functions).
+      forall functions, map.get functions from_bytes = Some f ->
+                        spec_of_from_bytes functions.
     Proof using inname_gen_varname_gen_disjoint
           outname_gen_varname_gen_disjoint ok relax_bounds res_Wf
           res_bounds res_eq res_valid tight_bounds_length
           tight_bounds_tighter_than_max byte_bounds_length.
       subst inlengths insizes outsizes. cbv [spec_of_from_bytes].
       cbv [from_bytes_insizes from_bytes_outsizes from_bytes_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup.
       eapply Proper_call.
       2:{
@@ -895,15 +888,15 @@ Section WithParameters.
     Import coqutil.Macros.symmetry.
     Lemma to_bytes_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions,
-        spec_of_to_bytes ((to_bytes, f) :: functions).
+      forall functions, map.get functions to_bytes = Some f ->
+                        spec_of_to_bytes functions.
     Proof using byte_bounds_length byte_bounds_tighter_than_max
           inname_gen_varname_gen_disjoint
           outname_gen_varname_gen_disjoint ok res_Wf
           res_eq res_valid res_bounds.
       subst inlengths insizes outsizes. cbv [spec_of_to_bytes].
       cbv [to_bytes_insizes to_bytes_outsizes to_bytes_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup.
       eapply Proper_call.
       2:{
@@ -926,7 +919,7 @@ Section WithParameters.
       { lists_autounfold; cbn[type.app_curried fst snd];
         cbv[Equivalence.equivalent_listexcl_flat_base
         Equivalence.equivalent_listonly_flat_base
-        Equivalence.equivalent_flat_base]; lists_autounfold; 
+        Equivalence.equivalent_flat_base]; lists_autounfold;
         cbn[hd]; repeat intro;
         cbv[Core.postcondition_func_norets Core.postcondition_func];
         sepsimpl; try congruence;
@@ -944,8 +937,8 @@ Section WithParameters.
           | |- _ /\ _ => eexists
           end;
         change Field.tight_bounds with tight_bounds in *.
-        { seprewrite_in (@Util.array_truncated_scalar_ptsto_iff1) H10; cbn in H10.
-          rewrite H7, res_eq, partition_le_split in *; trivial. }
+        { seprewrite_in (@Util.array_truncated_scalar_ptsto_iff1) H11; cbn in H11.
+          rewrite H8, res_eq, partition_le_split in *; trivial. }
         rewrite <-partition_le_split, <-res_eq; eauto. }
     Qed.
   End ToBytes.
@@ -964,7 +957,7 @@ Context
       list_Z_bounded_by (@max_bounds width n) (map word.unsigned x) ->
       list_Z_bounded_by (@max_bounds width n) (map word.unsigned y) ->
       ZRange.is_bounded_by_bool (word.unsigned c) bit_range = true ->
-                 (API.interp (res _)    
+                 (API.interp (res _)
                              (word.unsigned c)
                              (map word.unsigned x)
                              (map word.unsigned y))
@@ -1014,26 +1007,26 @@ Context
               apply Expr.is_bounded_by_bool_width_range.
               eauto.
               pose proof Properties.word.unsigned_range. auto.
-    Qed. 
+    Qed.
 
     Lemma FElem_max_bounds : forall px x m R, (FElem px x * R)%sep m -> list_Z_bounded_by (@max_bounds width n) (map word.unsigned x).
     Proof.
       intros. eapply max_bounds_words. cbv [FElem Bignum.Bignum] in H. sepsimpl. eauto.
-    Qed. 
+    Qed.
 
     Lemma select_znz_correct f :
       f = make_bedrock_func insizes outsizes inlengths res ->
-      forall functions,
-        spec_of_selectznz ((select_znz, f) :: functions).
+      forall functions, map.get functions select_znz = Some f ->
+                        spec_of_selectznz functions.
     Proof using inname_gen_varname_gen_disjoint
           outname_gen_varname_gen_disjoint ok res_Wf
           res_eq res_valid.
       subst inlengths insizes outsizes. cbv [spec_of_selectznz].
       cbv [list_selectznz_insizes list_selectznz_outsizes list_selectznz_inlengths].
-      cbv beta; intros; subst f. cbv [make_bedrock_func].
+      cbv beta; intros; subst f. cbv [make_bedrock_func] in *.
       cleanup.
-      pose proof (FElem_max_bounds _ _ _ _ H0) as Hxbounds.
-      pose proof (FElem_max_bounds _ _ _ _ H1) as Hybounds.
+      pose proof (FElem_max_bounds _ _ _ _ H1) as Hxbounds.
+      pose proof (FElem_max_bounds _ _ _ _ H2) as Hybounds.
       match goal with
       | H : ZRange.is_bounded_by_bool _ _ = _ |- _ => rename H into Hbound
       | _ => idtac
diff --git a/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v b/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
index a245c75e17..f2a6719dd1 100644
--- a/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
+++ b/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v
@@ -27,8 +27,8 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
 Import ListNotations API.Compilers Types.Notations.
 
 Class unsaturated_solinas_ops
-  {width BW word mem locals env ext_spec varname_gen error}
-  {parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}
+  {width BW word mem locals ext_spec varname_gen error}
+  {parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}
   {field_parameters : FieldParameters}
   {n s c} : Type :=
   { mul_op :
@@ -78,15 +78,15 @@ Class unsaturated_solinas_ops
         Field.to_bytes
         to_bytes_insizes to_bytes_outsizes (to_bytes_inlengths n);
   }.
-Arguments unsaturated_solinas_ops {_ _ _ _ _ _ _ _ _ _ _} n.
+Arguments unsaturated_solinas_ops {_ _ _ _ _ _ _ _ _ _} n.
 
 (** We need to tell [check_args] that we are requesting these functions in order to get the relevant properties out *)
 Notation necessary_requests := ["to_bytes"; "from_bytes"]%string (only parsing).
 
 Section UnsaturatedSolinas.
   Context
-  {width BW word mem locals env ext_spec error}
-  {parameters_sentinel : @parameters width BW word mem locals env ext_spec default_varname_gen error}
+  {width BW word mem locals ext_spec error}
+  {parameters_sentinel : @parameters width BW word mem locals ext_spec default_varname_gen error}
   {field_parameters : FieldParameters}
   {ok : Types.ok}.
 
@@ -306,15 +306,15 @@ Section UnsaturatedSolinas.
 
   Lemma mul_func_correct :
     valid_func (res mul_op _) ->
-    forall functions,
-      spec_of_BinOp bin_mul ((mul,mul_func) :: functions).
+    forall functions, Interface.map.get functions mul = Some mul_func ->
+                      spec_of_BinOp bin_mul functions.
   Proof using M_eq check_args_ok mul_func_eq ok
         tight_bounds_tighter_than.
-    intros. cbv [spec_of_BinOp bin_mul]. rewrite mul_func_eq.
+    cbv [spec_of_BinOp bin_mul]. rewrite mul_func_eq. intros.
     pose proof carry_mul_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq mul_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res mul_op);
+    eapply list_binop_correct with (res:=res mul_op); [ .. | eassumption ];
     handle_side_conditions; [ | | loosen_bounds | bounds_length ].
     { (* output *value* is correct *)
       intros.
@@ -327,15 +327,15 @@ Section UnsaturatedSolinas.
 
   Lemma square_func_correct :
     valid_func (res square_op _) ->
-    forall functions,
-      spec_of_UnOp un_square ((square,square_func) :: functions).
+    forall functions, Interface.map.get functions square = Some square_func ->
+                      spec_of_UnOp un_square functions.
   Proof using M_eq check_args_ok ok square_func_eq
         tight_bounds_tighter_than.
-    intros. cbv [spec_of_UnOp un_square]. rewrite square_func_eq.
+    cbv [spec_of_UnOp un_square]. rewrite square_func_eq. intros.
     pose proof carry_square_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq square_op)
       as Hcorrect.
-    eapply list_unop_correct with (res:=res square_op);
+    eapply list_unop_correct with (res:=res square_op); [ .. | eassumption ];
       handle_side_conditions; [ | | loosen_bounds| bounds_length ].
     { (* output *value* is correct *)
       intros. specialize_correctness_hyp Hcorrect.
@@ -347,15 +347,15 @@ Section UnsaturatedSolinas.
 
   Lemma add_func_correct :
     valid_func (res add_op _) ->
-    forall functions,
-      spec_of_BinOp bin_add ((Field.add,add_func) :: functions).
+    forall functions, Interface.map.get functions Field.add = Some add_func ->
+                      spec_of_BinOp bin_add functions.
   Proof using M_eq check_args_ok add_func_eq ok
         tight_bounds_tighter_than loose_bounds_tighter_than.
-    intros. cbv [spec_of_BinOp bin_add]. rewrite add_func_eq.
+    cbv [spec_of_BinOp bin_add]. rewrite add_func_eq. intros.
     pose proof add_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq add_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res add_op);
+    eapply list_binop_correct with (res:=res add_op); [ .. | eassumption ];
     handle_side_conditions; [ | | loosen_bounds | bounds_length ].
     { (* output *value* is correct *)
       intros.
@@ -368,15 +368,15 @@ Section UnsaturatedSolinas.
 
   Lemma sub_func_correct :
     valid_func (res sub_op _) ->
-    forall functions,
-      spec_of_BinOp bin_sub ((Field.sub,sub_func) :: functions).
+    forall functions, Interface.map.get functions Field.sub = Some sub_func ->
+                      spec_of_BinOp bin_sub functions.
   Proof using M_eq check_args_ok sub_func_eq ok
         tight_bounds_tighter_than loose_bounds_tighter_than.
-    intros. cbv [spec_of_BinOp bin_sub]. rewrite sub_func_eq.
+    cbv [spec_of_BinOp bin_sub]. rewrite sub_func_eq. intros.
     pose proof sub_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq sub_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res sub_op);
+    eapply list_binop_correct with (res:=res sub_op); [ .. | eassumption ];
     handle_side_conditions; [ | | loosen_bounds | bounds_length ].
     { (* output *value* is correct *)
       intros.
@@ -389,15 +389,15 @@ Section UnsaturatedSolinas.
 
   Lemma opp_func_correct :
     valid_func (res opp_op _) ->
-    forall functions,
-      spec_of_UnOp un_opp ((Field.opp, opp_func) :: functions).
+    forall functions, Interface.map.get functions Field.opp = Some opp_func ->
+                      spec_of_UnOp un_opp functions.
   Proof using M_eq check_args_ok loose_bounds_tighter_than opp_func_eq ok.
-    intros. cbv [spec_of_UnOp un_opp]. rewrite opp_func_eq.
+    cbv [spec_of_UnOp un_opp]. rewrite opp_func_eq. intros.
     pose proof opp_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq opp_op)
       as Hcorrect.
 
-    eapply list_unop_correct with (res:=res opp_op);
+    eapply list_unop_correct with (res:=res opp_op); [ .. | eassumption ];
       handle_side_conditions; [ | | loosen_bounds | bounds_length ].
     { (* output *value* is correct *)
       intros. specialize_correctness_hyp Hcorrect.
@@ -409,17 +409,17 @@ Section UnsaturatedSolinas.
 
   Lemma scmula24_func_correct :
     valid_func (res scmula24_op _) ->
-    forall functions,
-      spec_of_UnOp un_scmula24 ((scmula24, scmula24_func) :: functions).
+    forall functions, Interface.map.get functions scmula24 = Some scmula24_func ->
+                      spec_of_UnOp un_scmula24 functions.
   Proof using M_eq check_args_ok ok scmula24_func_eq
         tight_bounds_tighter_than.
-    intros. cbv [spec_of_UnOp un_scmula24]. rewrite scmula24_func_eq.
+    cbv [spec_of_UnOp un_scmula24]. rewrite scmula24_func_eq. intros.
     pose proof carry_scmul_const_correct
          _ _ _ _ _ (ltac:(eassumption)) (F.to_Z a24) _
          (res_eq scmula24_op)
       as Hcorrect.
 
-    eapply list_unop_correct with (res:=res scmula24_op);
+    eapply list_unop_correct with (res:=res scmula24_op); [ .. | eassumption ];
       handle_side_conditions; [ | | loosen_bounds | bounds_length ].
     { (* output *value* is correct *)
       intros. specialize_correctness_hyp Hcorrect.
@@ -444,66 +444,66 @@ Section UnsaturatedSolinas.
 
   Lemma felem_copy_func_correct :
     valid_func (res felem_copy_op _) ->
-    forall functions,
-      spec_of_felem_copy ((felem_copy, felem_copy_func) :: functions).
+    forall functions, Interface.map.get functions felem_copy = Some felem_copy_func ->
+                      spec_of_felem_copy functions.
   Proof using M_eq check_args_ok ok felem_copy_func_eq
         tight_bounds_tighter_than parameters_sentinel ok
 to_bytes_func_eq to_bytes_func sub_func_eq sub_func square_func_eq
 square_func scmula24_func_eq scmula24_func opp_func_eq opp_func mul_func_eq
 mul_func loose_bounds_tighter_than from_word_func_eq from_word_func
 from_bytes_func_eq from_bytes_func add_func_eq.
-    intros. cbv [spec_of_felem_copy]. rewrite felem_copy_func_eq.
+    cbv [spec_of_felem_copy]. rewrite felem_copy_func_eq. intros.
     pose proof copy_correct _ _ _ _ _ ltac:(eassumption) _ (res_eq felem_copy_op)
       as Hcorrect.
 
-    eapply felem_copy_correct;
+    eapply felem_copy_correct; [ .. | eassumption | eassumption ];
       repeat handle_side_conditions; [ | ]; intros.
     { (* output *value* is correct *)
       unshelve erewrite (proj1 (Hcorrect _ _)); cycle 1.
       { rewrite map_map, List.map_ext_id; trivial; intros.
         rewrite ?Word.Interface.word.of_Z_unsigned; trivial. }
-      { subst n. exact (list_Z_bounded_by_unsigned x). } }
+      { rewrite <- H2. exact (list_Z_bounded_by_unsigned x0). } }
     { (* output *bounds* are correct *)
       intros. apply Hcorrect; auto. }
   Qed.
 
   Lemma from_word_func_correct :
     valid_func (res from_word_op _) ->
-    forall functions,
-      spec_of_from_word ((from_word, from_word_func) :: functions).
+    forall functions, Interface.map.get functions from_word = Some from_word_func ->
+                      spec_of_from_word functions.
   Proof using M_eq check_args_ok from_word_func_eq ok
         tight_bounds_tighter_than.
-    intros. cbv [spec_of_from_word]. rewrite from_word_func_eq.
+    cbv [spec_of_from_word]. rewrite from_word_func_eq. intros.
     epose proof encode_word_correct _ _ _ _ _ ltac:(eassumption) _ (res_eq from_word_op)
       as Hcorrect.
     cbv [expr.Interp] in *; autounfold with solinas_specs in *; cbn [ZRange.lower ZRange.upper] in *.
 
-    eapply from_word_correct;
+    eapply from_word_correct; [ .. | eassumption | eassumption ];
       repeat handle_side_conditions.
     { (* value *)
       intros.
       destruct (Hcorrect (Interface.word.unsigned w)); clear Hcorrect.
       { pose proof Properties.word.unsigned_range w.
         eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; Lia.lia. }
-      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H0.
-      rewrite <-H0.
+      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H2.
+      rewrite <-H2.
       unfold feval.
       unfold Signature.field_representation.
       unfold Representation.eval_words, Representation.frep.
       cbv [Representation.eval_words].
       Morphisms.f_equiv. Morphisms.f_equiv.
       rewrite map_unsigned_of_Z, List.map_ext_id; trivial.
-      intros x Hx.
-      eapply relax_list_Z_bounded_by, MaxBounds.max_bounds_range_iff in H1;
-        try eapply tight_bounds_tighter_than; destruct H1.
-      eapply List.Forall_In in H2; eauto.
-      rewrite MakeAccessSizes.bits_per_word_eq_width in H2.
+      intros y Hy.
+      eapply relax_list_Z_bounded_by, MaxBounds.max_bounds_range_iff in H3;
+        try eapply tight_bounds_tighter_than; destruct H3.
+      eapply List.Forall_In in H4; eauto.
+      rewrite MakeAccessSizes.bits_per_word_eq_width in H4.
       unfold Interface.word.wrap; rewrite Z.mod_small; trivial. }
     { intros.
       destruct (Hcorrect (Interface.word.unsigned w)); clear Hcorrect.
       { pose proof Properties.word.unsigned_range w.
         eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; Lia.lia. }
-      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H0.
+      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H2.
       trivial. }
     { eauto using relax_list_Z_bounded_by, tight_bounds_tighter_than. }
   Qed.
@@ -511,15 +511,17 @@ from_bytes_func_eq from_bytes_func add_func_eq.
   Lemma from_bytes_func_correct :
     valid_func (res from_bytes_op _) ->
     forall functions,
-      spec_of_from_bytes ((Field.from_bytes,from_bytes_func) :: functions).
+      Interface.map.get functions Field.from_bytes = Some from_bytes_func ->
+      spec_of_from_bytes functions.
   Proof using M_eq check_args_ok from_bytes_func_eq ok
         tight_bounds_tighter_than.
-    intros. cbv [spec_of_from_bytes]. rewrite from_bytes_func_eq.
+    cbv [spec_of_from_bytes]. rewrite from_bytes_func_eq. intros.
     pose proof UnsaturatedSolinas.from_bytes_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq from_bytes_op) (eq_refl true)
       as Hcorrect.
 
     eapply Signature.from_bytes_correct with (res:=res from_bytes_op);
+      [ .. | eassumption | eassumption ];
       handle_side_conditions; [ loosen_bounds | bounds_length | | | ].
     { intros. erewrite length_list_Z_bounded_by, length_byte_bounds; trivial. }
     { (* output *value* is correct *)
@@ -532,15 +534,16 @@ from_bytes_func_eq from_bytes_func add_func_eq.
 
   Lemma to_bytes_func_correct :
     valid_func (res to_bytes_op _) ->
-    forall functions,
-      spec_of_to_bytes ((Field.to_bytes, to_bytes_func) :: functions).
+    forall functions, Interface.map.get functions Field.to_bytes = Some to_bytes_func ->
+                      spec_of_to_bytes functions.
   Proof using M_eq check_args_ok ok to_bytes_func_eq.
-    intros. cbv [spec_of_to_bytes]. rewrite to_bytes_func_eq.
+    cbv [spec_of_to_bytes]. rewrite to_bytes_func_eq. intros.
     pose proof UnsaturatedSolinas.to_bytes_correct
          _ _ _ _ _ ltac:(eassumption) _ (res_eq to_bytes_op) (eq_refl true)
       as Hcorrect.
 
     eapply Signature.to_bytes_correct with (res:=res to_bytes_op);
+      [ .. | eassumption | eassumption ];
       handle_side_conditions; [ | | | ].
     {
       intros. eapply relax_list_Z_bounded_by; [| eauto]. apply byte_bounds_tighter_than.
@@ -606,7 +609,17 @@ Local Ltac begin_derive_bedrock2_func :=
   | |- context [spec_of_from_word] => rapply from_word_func_correct
   end.
 
+Ltac epair :=
+  lazymatch goal with
+  | f := _ : string * Syntax.func |- _ =>
+    let p := open_constr:((_, _)) in
+    unify f p;
+    subst f
+  | f := _ : Syntax.func |- _ => idtac
+  end.
+
 Ltac derive_bedrock2_func op :=
+  epair;
   begin_derive_bedrock2_func;
   (* this goal fills in the evar, so do it first for [abstract] to be happy *)
   try lazymatch goal with
@@ -650,68 +663,78 @@ Section Tests.
   Instance fe25519_ops : unsaturated_solinas_ops n s c.
   Proof using Type. Time constructor; make_computed_op. Defined.
 
+  Local Notation functions_contain functions f :=
+    (Interface.map.get functions (fst f) = Some (snd f)).
+
   Derive fe25519_mul
          SuchThat (forall functions,
+                      functions_contain functions fe25519_mul ->
                       spec_of_BinOp bin_mul
                         (field_representation:=field_representation n s c)
-                        (fe25519_mul :: functions))
+                        functions)
          As fe25519_mul_correct.
   Proof. Time derive_bedrock2_func mul_op. Qed.
 
   Derive fe25519_square
          SuchThat (forall functions,
+                      functions_contain functions fe25519_square ->
                       spec_of_UnOp un_square
                         (field_representation:=field_representation n s c)
-                        (fe25519_square :: functions))
+                        functions)
          As fe25519_square_correct.
   Proof. Time derive_bedrock2_func square_op. Qed.
 
   Derive fe25519_add
          SuchThat (forall functions,
+                      functions_contain functions fe25519_add ->
                       spec_of_BinOp bin_add
                         (field_representation:=field_representation n s c)
-                        (fe25519_add :: functions))
+                        functions)
          As fe25519_add_correct.
   Proof. Time derive_bedrock2_func add_op. Qed.
 
-
   Derive fe25519_sub
          SuchThat (forall functions,
+                      functions_contain functions fe25519_sub ->
                       spec_of_BinOp bin_sub
                         (field_representation:=field_representation n s c)
-                        (fe25519_sub :: functions))
+                        functions)
          As fe25519_sub_correct.
   Proof. Time derive_bedrock2_func sub_op. Qed.
 
   Derive fe25519_opp
          SuchThat (forall functions,
+                      functions_contain functions fe25519_opp ->
                       spec_of_UnOp un_opp
                         (field_representation:=field_representation n s c)
-                        (fe25519_opp :: functions))
+                        functions)
          As fe25519_opp_correct.
   Proof. Time derive_bedrock2_func opp_op. Qed.
 
   Derive fe25519_scmula24
          SuchThat (forall functions,
+                      functions_contain functions fe25519_scmula24 ->
                       spec_of_UnOp un_scmula24
                         (field_representation:=field_representation n s c)
-                        (fe25519_scmula24 :: functions))
+                        functions)
          As fe25519_scmula24_correct.
   Proof. Time derive_bedrock2_func scmula24_op. Qed.
 
   Derive fe25519_from_bytes
          SuchThat (forall functions,
+                      functions_contain functions fe25519_from_bytes ->
                       spec_of_from_bytes
                         (field_representation:=field_representation n s c)
-                        (fe25519_from_bytes :: functions))
+                        functions)
          As fe25519_from_bytes_correct.
   Proof. Time derive_bedrock2_func from_bytes_op. Qed.
 
   Derive fe25519_to_bytes
          SuchThat (forall functions,
+                      functions_contain functions fe25519_to_bytes ->
                       spec_of_to_bytes
                         (field_representation:=field_representation n s c)
-                        (fe25519_to_bytes :: functions))
+                        functions)
          As fe25519_to_bytes_correct.
   Proof. Time derive_bedrock2_func to_bytes_op. Qed.
 End Tests.
diff --git a/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v b/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v
index 170c39f165..9a5813ae47 100644
--- a/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v
+++ b/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v
@@ -30,8 +30,8 @@ Import ListNotations API.Compilers Types.Notations.
 
 Class word_by_word_Montgomery_ops
   {from_mont to_mont : string}
-  {width BW word mem locals env ext_spec varname_gen error}
-  {parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}
+  {width BW word mem locals ext_spec varname_gen error}
+  {parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}
   {field_parameters : FieldParameters}
   {n m} : Type :=
   { mul_op :
@@ -83,15 +83,15 @@ Class word_by_word_Montgomery_ops
         list_selectznz_insizes list_selectznz_outsizes (list_selectznz_inlengths n)
   }.
 
-Arguments word_by_word_Montgomery_ops {_ _ _ _ _ _ _ _ _ _ _ _ _} n.
+Arguments word_by_word_Montgomery_ops {_ _ _ _ _ _ _ _ _ _ _ _} n.
 
 (** We need to tell [check_args] that we are requesting these functions in order to get the relevant properties out *)
 Notation necessary_requests := ["to_bytes"; "from_bytes"]%string (only parsing).
 
 Section WordByWordMontgomery.
   Context
-  {width BW word mem locals env ext_spec error}
-  {parameters_sentinel : @parameters width BW word mem locals env ext_spec default_varname_gen error}
+  {width BW word mem locals ext_spec error}
+  {parameters_sentinel : @parameters width BW word mem locals ext_spec default_varname_gen error}
   {field_parameters : FieldParameters}
   {field_parameters_ok : FieldParameters_ok}
   {ok : Types.ok}.
@@ -176,7 +176,7 @@ Section WordByWordMontgomery.
           (to_bytes_func_eq : to_bytes_func = b2_func to_bytes_op)
           (from_mont_func_eq : from_mont_func = b2_func from_mont_op)
           (to_mont_func_eq : to_mont_func = b2_func to_mont_op)
-          (select_znz_func_eq : select_znz_func = b2_func (@select_znz_op from_mont to_mont _ _ _ _ _ _ _ _ _ _ _ _ _ _)).
+          (select_znz_func_eq : select_znz_func = b2_func (@select_znz_op from_mont to_mont _ _ _ _ _ _ _ _ _ _ _ _ _)).
 
   Local Notation weight := (uweight width) (only parsing).
   Definition eval_trans := (WordByWordMontgomery.from_montgomerymod width n m (WordByWordMontgomery.m' m width)).
@@ -332,15 +332,15 @@ Qed.
 
   Lemma mul_func_correct :
     valid_func (res mul_op _) ->
-    forall functions,
-      spec_of_BinOp bin_mul ((Field.mul, mul_func) :: functions). Set Printing All.
+    forall functions, Interface.map.get functions Field.mul = Some mul_func ->
+                      spec_of_BinOp bin_mul functions.
   Proof using M_eq check_args_ok mul_func_eq ok.
         (* tight_bounds_tighter_than. *)
-    intros. cbv [spec_of_BinOp bin_mul]. rewrite mul_func_eq.
+    cbv [spec_of_BinOp bin_mul]. rewrite mul_func_eq. intros.
     pose proof mul_correct
          m width _ ltac:(eassumption) _ (res_eq mul_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res mul_op);
+    eapply list_binop_correct with (res:=res mul_op); [ .. | eassumption ];
     try handle_side_conditions; [| | eapply valid_max_bounds; eauto | apply valid_length].
     {
     (* output *value* is correct *)
@@ -352,7 +352,7 @@ Qed.
                bin_model bin_xbounds bin_ybounds
                un_model un_xbounds eval_trans
       ] in *.
-      specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H0 H1).
+      specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H1 H2).
       FtoZ. rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
       2: {
         eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -365,14 +365,14 @@ Qed.
 
   Lemma square_func_correct :
     valid_func (res square_op _) ->
-    forall functions,
-      spec_of_UnOp un_square ((Field.square, square_func) :: functions).
+    forall functions, Interface.map.get functions Field.square = Some square_func ->
+                      spec_of_UnOp un_square functions.
   Proof using M_eq check_args_ok ok square_func_eq.
-    intros. cbv [spec_of_UnOp un_square]. rewrite square_func_eq.
+    cbv [spec_of_UnOp un_square]. rewrite square_func_eq. intros.
     pose proof square_correct
          _ _ _ ltac:(eassumption) _ (res_eq square_op)
       as Hcorrect.
-    eapply list_unop_correct with (res:=res square_op);
+    eapply list_unop_correct with (res:=res square_op); [ .. | eassumption ];
       handle_side_conditions; [ | | apply valid_max_bounds | apply valid_length ].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -383,7 +383,7 @@ Qed.
              bin_model bin_xbounds bin_ybounds
              un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Interface.word.unsigned x) H0).
+    specialize (Hcorrect (map Interface.word.unsigned x) H1).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -398,14 +398,14 @@ Qed.
 
   Lemma add_func_correct :
     valid_func (res add_op _) ->
-    forall functions,
-      spec_of_BinOp bin_add ((Field.add, add_func) :: functions).
+    forall functions, Interface.map.get functions Field.add = Some add_func ->
+                      spec_of_BinOp bin_add functions.
   Proof using M_eq check_args_ok add_func_eq ok.
-    intros. cbv [spec_of_BinOp bin_add]. rewrite add_func_eq.
+    cbv [spec_of_BinOp bin_add]. rewrite add_func_eq. intros.
     pose proof add_correct
          _ _ _ ltac:(eassumption) _ (res_eq add_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res add_op);
+    eapply list_binop_correct with (res:=res add_op); [ .. | eassumption ];
     handle_side_conditions; [ | | apply valid_max_bounds | apply valid_length ].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -416,7 +416,7 @@ Qed.
              bin_model bin_xbounds bin_ybounds
              un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H0 H1).
+    specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H1 H2).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -430,14 +430,14 @@ Qed.
 
   Lemma sub_func_correct :
     valid_func (res sub_op _) ->
-    forall functions,
-      spec_of_BinOp bin_sub ((Field.sub, sub_func) :: functions).
+    forall functions, Interface.map.get functions Field.sub = Some sub_func ->
+                      spec_of_BinOp bin_sub functions.
   Proof using M_eq check_args_ok sub_func_eq ok.
-    intros. cbv [spec_of_BinOp bin_sub]. rewrite sub_func_eq.
+    cbv [spec_of_BinOp bin_sub]. rewrite sub_func_eq. intros.
     pose proof sub_correct
          _ _ _ ltac:(eassumption) _ (res_eq sub_op)
       as Hcorrect.
-    eapply list_binop_correct with (res:=res sub_op);
+    eapply list_binop_correct with (res:=res sub_op); [ .. | eassumption ];
     handle_side_conditions; [ | | apply valid_max_bounds| apply valid_length ].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -448,7 +448,7 @@ Qed.
              bin_model bin_xbounds bin_ybounds
              un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H0 H1).
+    specialize (Hcorrect (map Interface.word.unsigned x) (map Interface.word.unsigned y) H1 H2).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -461,15 +461,15 @@ Qed.
 
   Lemma opp_func_correct :
     valid_func (res opp_op _) ->
-    forall functions,
-      spec_of_UnOp un_opp ((Field.opp, opp_func) :: functions).
+    forall functions, Interface.map.get functions Field.opp = Some opp_func ->
+                      spec_of_UnOp un_opp functions.
   Proof using M_eq check_args_ok opp_func_eq ok.
-    intros. cbv [spec_of_UnOp un_opp]. rewrite opp_func_eq.
+    cbv [spec_of_UnOp un_opp]. rewrite opp_func_eq. intros.
     pose proof opp_correct
          _ _ _ ltac:(eassumption) _ (res_eq opp_op)
       as Hcorrect.
 
-    eapply list_unop_correct with (res:=res opp_op);
+    eapply list_unop_correct with (res:=res opp_op); [ .. | eassumption ];
       handle_side_conditions; [ | | apply valid_max_bounds | apply valid_length ].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -480,7 +480,7 @@ Qed.
              bin_model bin_xbounds bin_ybounds
              un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Interface.word.unsigned x) H0).
+    specialize (Hcorrect (map Interface.word.unsigned x) H1).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -495,18 +495,20 @@ Qed.
   Lemma from_bytes_func_correct :
     valid_func (res from_bytes_op _) ->
     forall functions,
-      (@spec_of_from_bytes _ _ _ _ _ _ _ field_representation_raw) ((Field.from_bytes, from_bytes_func) :: functions).
+      Interface.map.get functions Field.from_bytes = Some from_bytes_func ->
+      (@spec_of_from_bytes _ _ _ _ _ _ _ field_representation_raw) functions.
   Proof using M_eq check_args_ok from_bytes_func_eq ok.
-    intros. cbv [spec_of_from_bytes]. rewrite from_bytes_func_eq.
+    cbv [spec_of_from_bytes]. rewrite from_bytes_func_eq. intros.
     pose proof from_bytes_correct
          _ _ _ ltac:(eassumption) _ (res_eq from_bytes_op)
       as Hcorrect.
 
     eapply Signature.from_bytes_correct with (res:=res from_bytes_op);
+      [ .. | eassumption | eassumption ];
       handle_side_conditions; [ apply valid_max_bounds | apply valid_length | | | ].
     { (* output length *)
       cbv [list_in_bounds WordByWordMontgomery.valid WordByWordMontgomery.small ] in *.
-      intuition idtac. rewrite H1. rewrite Partition.length_partition; trivial. }
+      intuition idtac. rewrite H5. rewrite Partition.length_partition; trivial. }
 
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -517,7 +519,7 @@ Qed.
              bin_model bin_xbounds bin_ybounds
              un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Byte.byte.unsigned bs) H0).
+    specialize (Hcorrect (map Byte.byte.unsigned bs0) H2).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
@@ -532,23 +534,25 @@ Qed.
   Lemma to_bytes_func_correct :
     valid_func (res to_bytes_op _) ->
     forall functions,
-      (@spec_of_to_bytes _ _ _ _ _ _ _ field_representation_raw) ((Field.to_bytes, to_bytes_func) :: functions).
+      Interface.map.get functions Field.to_bytes = Some to_bytes_func ->
+      (@spec_of_to_bytes _ _ _ _ _ _ _ field_representation_raw) functions.
   Proof using M_eq check_args_ok ok to_bytes_func_eq.
-    intros. cbv [spec_of_to_bytes]. rewrite to_bytes_func_eq.
+    cbv [spec_of_to_bytes]. rewrite to_bytes_func_eq. intros.
     pose proof to_bytes_correct
          _ _ _ ltac:(eassumption) _ (res_eq to_bytes_op)
       as Hcorrect.
 
     eapply Signature.to_bytes_correct with (res:=res to_bytes_op);
+      [ .. | eassumption | eassumption ];
       handle_side_conditions; cbv [list_in_bounds]; [ | | | ].
     {
       intros. apply byte_bounds_range_iff; split; eauto.
-        - destruct H0. eapply WordByWordMontgomery.length_small; eauto.
-        - destruct H0. cbv [WordByWordMontgomery.small] in *.
-          rewrite H0. apply partition_bytes_range.
+        - destruct H2. eapply WordByWordMontgomery.length_small; eauto.
+        - destruct H2. cbv [WordByWordMontgomery.small] in *.
+          rewrite H2. apply partition_bytes_range.
     }
     {
-      intros. destruct H0. apply WordByWordMontgomery.length_small in H0. rewrite H0. eauto.
+      intros. destruct H2. apply WordByWordMontgomery.length_small in H2. rewrite H2. eauto.
     }
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl.
@@ -560,7 +564,7 @@ Qed.
              un_model un_xbounds eval_trans
     ] in *.
 
-    specialize (Hcorrect (map Interface.word.unsigned x) H0).
+    specialize (Hcorrect (map Interface.word.unsigned x0) H2).
     rewrite Hcorrect. cbv [M] in M_eq. rewrite M_eq. auto.
      }
     { (* output *bounds* are correct *)
@@ -579,16 +583,16 @@ Qed.
             apply uwprops. lia.
           }
         rewrite Zmod_small.
-        2: { destruct H0. unfold WordByWordMontgomery.eval in H1. auto. }
+        2: { destruct H2. unfold WordByWordMontgomery.eval in H3. auto. }
           cbv [uweight].
           rewrite Zmod_small; auto. split.
-            + destruct H0. cbv [WordByWordMontgomery.eval] in H1. cbv [uweight] in H1. lia.
-            + destruct H0. cbv [WordByWordMontgomery.eval] in H1. cbv [uweight] in H1. destruct H1.
+            + destruct H2. cbv [WordByWordMontgomery.eval] in H3. cbv [uweight] in H3. lia.
+            + destruct H2. cbv [WordByWordMontgomery.eval] in H3. cbv [uweight] in H3. destruct H3.
               assert ( m < ModOps.weight 8 1 (n_bytes m))%Z.
               {
-                pose proof (use_curve_good _ _ _ check_args_ok).
+                pose proof (use_curve_good _ _ _ check_args_ok) as U.
                 assert (m < s m)%Z by lia.
-                cbv [uweight] in H3. lia.
+                cbv [uweight] in U. lia.
               }
             lia.
           - cbv [WordByWordMontgomery.eval]. rewrite Partition.eval_partition.
@@ -622,15 +626,16 @@ Qed.
   Lemma from_mont_func_correct :
   valid_func (res from_mont_op _) ->
   forall functions,
-    (@spec_of_UnOp _ _ _ _ _ _ _ _ from_mont) un_from_mont ((from_mont, from_mont_func) :: functions).
+    Interface.map.get functions from_mont = Some from_mont_func ->
+    (@spec_of_UnOp _ _ _ _ _ _ _ _ from_mont) un_from_mont functions.
     Proof using M_eq check_args_ok ok from_mont_func_eq.
     clear field_parameters_ok.
-    intros. cbv [spec_of_UnOp un_from_mont]. rewrite from_mont_func_eq.
+    cbv [spec_of_UnOp un_from_mont]. rewrite from_mont_func_eq. intros.
     pose proof from_montgomery_correct
         _ _ _ ltac:(eassumption) _ (res_eq from_mont_op)
       as Hcorrect.
 
-    eapply list_unop_correct with (res:=res from_mont_op);
+    eapply list_unop_correct with (res:=res from_mont_op); [ .. | eassumption ];
       handle_side_conditions; [ | | apply valid_max_bounds | apply valid_length ].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -641,17 +646,17 @@ Qed.
             bin_model bin_xbounds bin_ybounds
             un_model un_xbounds eval_trans
     ] in *.
-    specialize (Hcorrect (map Interface.word.unsigned x) H0).
+    specialize (Hcorrect (map Interface.word.unsigned x) H1).
     rewrite map_unsigned_of_Z. erewrite (MaxBounds.map_word_wrap_bounded).
     2: {
       eapply valid_max_bounds; eauto. destruct Hcorrect; eauto.
     }
     destruct Hcorrect. FtoZ. pose proof (WordByWordMontgomery.from_montgomerymod_correct width n m (@Field.r' width field_parameters) (m' m width)) as Hcorrect.
     cbv [WordByWordMontgomery.eval] in *.
-    edestruct Hcorrect as [Hvalue Hvalid]; [| | | | | | eapply H2| ]; try eapply use_curve_good; try eassumption; [pose proof r'_correct as Htemp; cbv [r' M] in Htemp; rewrite M_eq in Htemp; eauto |].
-    rewrite Hvalue. rewrite Z.mul_mod; try apply m_nz. rewrite H1. rewrite <- Z.mul_mod; try apply m_nz.
-    symmetry. rewrite Z.mul_mod; try apply m_nz. cbv [list_in_bounds] in *. clear H2.
-    edestruct Hcorrect as [Hvalue' _]; [| | | | | | eapply H0 |]; try eapply use_curve_good; try eassumption; [pose proof r'_correct as Htemp; cbv [r' M] in Htemp; rewrite M_eq in Htemp; eauto |].
+    edestruct Hcorrect as [Hvalue Hvalid]; [| | | | | | eapply H3| ]; try eapply use_curve_good; try eassumption; [pose proof r'_correct as Htemp; cbv [r' M] in Htemp; rewrite M_eq in Htemp; eauto |].
+    rewrite Hvalue. rewrite Z.mul_mod; try apply m_nz. rewrite H2. rewrite <- Z.mul_mod; try apply m_nz.
+    symmetry. rewrite Z.mul_mod; try apply m_nz. cbv [list_in_bounds] in *. clear H3.
+    edestruct Hcorrect as [Hvalue' _]; [| | | | | | eapply H1 |]; try eapply use_curve_good; try eassumption; [pose proof r'_correct as Htemp; cbv [r' M] in Htemp; rewrite M_eq in Htemp; eauto |].
     rewrite Hvalue'. rewrite <- Z.mul_mod; try apply m_nz.
     cbv [Field.r' PushButtonSynthesis.WordByWordMontgomery.r' Field.r r M felem_size_in_words]. rewrite M_eq.
     auto.
@@ -663,14 +668,15 @@ Qed.
   Lemma to_mont_func_correct :
   valid_func (res to_mont_op _) ->
   forall functions,
-    (@spec_of_UnOp _ _ _ _ _ _ _ _ to_mont) un_to_mont ((to_mont, to_mont_func) :: functions).
+    Interface.map.get functions to_mont = Some to_mont_func ->
+    (@spec_of_UnOp _ _ _ _ _ _ _ _ to_mont) un_to_mont functions.
     Proof using M_eq check_args_ok ok to_mont_func_eq.
-    intros. cbv [spec_of_UnOp un_to_mont]. rewrite to_mont_func_eq.
+    cbv [spec_of_UnOp un_to_mont]. rewrite to_mont_func_eq. intros ? ? GetF.
     pose proof to_montgomery_correct
         _ _ _ ltac:(eassumption) _ (res_eq to_mont_op)
       as Hcorrect.
 
-    eapply list_unop_correct with (res:=res to_mont_op);
+    eapply list_unop_correct with (res:=res to_mont_op); [ .. | eassumption ];
       handle_side_conditions; [ | | apply valid_max_bounds | apply valid_length].
     { (* output *value* is correct *)
     intros. cbv [feval]. simpl. cbv [Representation.eval_words]. simpl.
@@ -717,14 +723,16 @@ Qed.
 
   Lemma select_znz_func_correct :
   valid_func (res select_znz_op _) ->
-  forall functions,
-    spec_of_selectznz ((select_znz, select_znz_func) :: functions).
+  forall functions, Interface.map.get functions select_znz = Some select_znz_func ->
+                    spec_of_selectznz functions.
 Proof using M_eq check_args_ok select_znz_func_eq ok.
-  intros. cbv [spec_of_selectznz]. rewrite select_znz_func_eq.
+  cbv [spec_of_selectznz]. rewrite select_znz_func_eq. intros ? ? GetF * HH.
+  rename x into x', y into y'.
   pose proof selectznz_correct
        _ _ _ ltac:(eassumption) _ (res_eq select_znz_op)
     as Hcorrect.
   eapply Signature.select_znz_correct with (res:=res select_znz_op);
+    [ .. | eassumption | eassumption ];
     handle_side_conditions. intros x y c H0 H1 H2.
     unfold COperationSpecifications.WordByWordMontgomery.selectznz_correct in Hcorrect.
     edestruct (bit_range_eq 1 (fun n => 1%Z) _ H2) as [Hbit | Hbit].
diff --git a/src/Bedrock/Field/Translation/Cmd.v b/src/Bedrock/Field/Translation/Cmd.v
index cc1c8fd5cb..80f4ec191c 100644
--- a/src/Bedrock/Field/Translation/Cmd.v
+++ b/src/Bedrock/Field/Translation/Cmd.v
@@ -15,9 +15,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Cmd.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Existing Instance Types.rep.Z.
   Existing Instance Types.rep.listZ_local. (* local list representation *)
 
diff --git a/src/Bedrock/Field/Translation/Expr.v b/src/Bedrock/Field/Translation/Expr.v
index 56e956e416..e87516a669 100644
--- a/src/Bedrock/Field/Translation/Expr.v
+++ b/src/Bedrock/Field/Translation/Expr.v
@@ -10,9 +10,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Expr.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Existing Instance Types.rep.Z.
   Existing Instance Types.rep.listZ_local. (* local list representation *)
diff --git a/src/Bedrock/Field/Translation/Flatten.v b/src/Bedrock/Field/Translation/Flatten.v
index cb8fe5f20b..c10e4bc104 100644
--- a/src/Bedrock/Field/Translation/Flatten.v
+++ b/src/Bedrock/Field/Translation/Flatten.v
@@ -16,9 +16,9 @@ Import Types.Notations.
    conversions between the two. *)
 
 Section Flatten.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   (* these conversions should happen before loading arguments and after
        storing return values, so they use in-memory lists *)
   Local Existing Instance rep.listZ_mem.
diff --git a/src/Bedrock/Field/Translation/Func.v b/src/Bedrock/Field/Translation/Func.v
index 738ca7983a..aaef1dbb29 100644
--- a/src/Bedrock/Field/Translation/Func.v
+++ b/src/Bedrock/Field/Translation/Func.v
@@ -14,9 +14,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Func.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Existing Instance rep.Z.
 
   (* Feeds arguments to function one by one and then calls translate_cmd *)
diff --git a/src/Bedrock/Field/Translation/LoadStoreList.v b/src/Bedrock/Field/Translation/LoadStoreList.v
index aba10a1f78..ef5c8ea03a 100644
--- a/src/Bedrock/Field/Translation/LoadStoreList.v
+++ b/src/Bedrock/Field/Translation/LoadStoreList.v
@@ -27,9 +27,9 @@ Import Types.Notations.
    then returns local variables which we store. This file handles the
    loading/storing part of that process. *)
 Section Lists.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Local Existing Instance rep.Z.
 
   Fixpoint extract_listnames {t}
diff --git a/src/Bedrock/Field/Translation/Proofs/Cmd.v b/src/Bedrock/Field/Translation/Proofs/Cmd.v
index b78c44a159..f5e55e561d 100644
--- a/src/Bedrock/Field/Translation/Proofs/Cmd.v
+++ b/src/Bedrock/Field/Translation/Proofs/Cmd.v
@@ -33,9 +33,9 @@ Import Wf.Compilers.expr.
 Import Types.Notations.
 
 Section Cmd.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance Types.rep.Z.
@@ -91,7 +91,7 @@ Section Cmd.
       let nvars := fst (fst out) in
       let lhs := snd (fst out) in
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (snd out)
         tr mem locals
         (fun tr' mem' locals' =>
@@ -118,7 +118,7 @@ Section Cmd.
       cbn [rep.equiv rep.Z] in *. sepsimpl.
       repeat straightline.
       eexists; split; [ eapply expr_empty; eassumption | ].
-      eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2:{
         eapply IHrhs; eauto.
         { eapply Forall2_impl_strong; eauto.
@@ -178,7 +178,7 @@ Section Cmd.
       let nvars := fst (fst out) in
       let lhs := snd (fst out) in
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (snd out) tr mem locals
         (fun tr' mem' locals' =>
            tr = tr'
@@ -213,10 +213,9 @@ Section Cmd.
               | f_equal; lia ]. }
     { (* prod *)
       repeat straightline.
-      eapply Proper_cmd; [ solve [apply Proper_call]
-                         | repeat intro | eapply IHt1; solve [eauto] ].
+      eapply Proper_cmd; [ repeat intro | eapply IHt1; solve [eauto] ].
       cbv beta in *; cleanup; subst.
-      eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2:{
         eapply IHt2; eauto; [ | ].
          { eapply equivalent_only_differ_undef; eauto;
@@ -267,7 +266,7 @@ Section Cmd.
       let nvars := fst (fst out) in
       let lhs := snd (fst out) in
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (snd out) tr mem locals
         (fun tr' mem' locals' =>
            tr = tr'
@@ -405,7 +404,7 @@ Section Cmd.
         context_equiv G locals ->
         (* executing translation output is equivalent to interpreting e *)
         WeakestPrecondition.cmd
-          (WeakestPrecondition.call functions)
+          functions
           body tr mem locals
           (fun tr' mem' locals' =>
              tr = tr' /\
@@ -444,14 +443,14 @@ Section Cmd.
                                                   WeakestPrecondition.cmd
                                                   WeakestPrecondition.cmd_body] in *
                | _ => eapply Proper_cmd;
-                        [ eapply Proper_call | repeat intro
+                        [ repeat intro
                           | eapply assign_correct; eauto;
                             eapply translate_expr_correct; solve [eauto] ]
                | _ => progress cbn [invert_expr.invert_pair_cps invert_expr.invert_AppIdent2_cps Option.bind invert_expr.invert_App2_cps invert_expr.invert_App_cps invert_expr.invert_Ident invert_expr.is_pair Compilers.invertIdent Option.bind translate_ident2_for_cmd Crypto.Util.Option.bind]
                end.
 
     { (* let-in (product of base types) *)
-      eapply Proper_cmd; [ eapply Proper_call | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2: {
         eapply IHe1_valid; clear IHe1_valid;
         repeat match goal with
@@ -468,7 +467,7 @@ Section Cmd.
         etransitivity; [ eassumption | ].
         apply used_varnames_shift. } }
     { (* let-in (base type) *)
-      eapply Proper_cmd; [ eapply Proper_call | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2: {
         eapply IHe1_valid; clear IHe1_valid;
         repeat match goal with
@@ -485,7 +484,7 @@ Section Cmd.
         etransitivity; [ eassumption | ].
         apply used_varnames_shift. } }
     { (* cons *)
-      eapply Proper_cmd; [ eapply Proper_call | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2: {
         eapply IHe1_valid with (G:=G); clear IHe1_valid;
         repeat match goal with
diff --git a/src/Bedrock/Field/Translation/Proofs/Equivalence.v b/src/Bedrock/Field/Translation/Proofs/Equivalence.v
index 7e39d04320..ada12d545e 100644
--- a/src/Bedrock/Field/Translation/Proofs/Equivalence.v
+++ b/src/Bedrock/Field/Translation/Proofs/Equivalence.v
@@ -14,10 +14,10 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Equivalent.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
    `{parameters_sentinel : @parameters
-     width BW word mem locals env ext_spec varname_gen error}.
+     width BW word mem locals ext_spec varname_gen error}.
   Local Notation parameters := (ltac:(let t := type of parameters_sentinel in exact t)) (only parsing).
   Context {listZ : rep.rep base_listZ}.
   Existing Instance rep.Z.
@@ -119,10 +119,10 @@ End Equivalent.
 
 (* equivalence with flat lists of words *)
 Section EquivalentFlat.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
    `{parameters_sentinel : @parameters
-     width BW word mem locals env ext_spec varname_gen error}.
+     width BW word mem locals ext_spec varname_gen error}.
   Local Notation parameters := (ltac:(let t := type of parameters_sentinel in exact t)) (only parsing).
   Existing Instances rep.listZ_mem rep.Z.
 
diff --git a/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v b/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
index 2496eacfff..259d4fd799 100644
--- a/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
+++ b/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
@@ -20,9 +20,9 @@ Import API.Compilers.
 Import ListNotations Types.Notations.
 
 Section OnlyDiffer.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Local Existing Instance Types.rep.Z.
 
@@ -341,9 +341,9 @@ Global Hint Resolve
      equiv_listZ_only_differ_mem : equiv.
 
 Section ContextEquivalence.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Local Existing Instance Types.rep.Z.
 
diff --git a/src/Bedrock/Field/Translation/Proofs/Expr.v b/src/Bedrock/Field/Translation/Proofs/Expr.v
index 9b19f359ff..3fffc6fb67 100644
--- a/src/Bedrock/Field/Translation/Proofs/Expr.v
+++ b/src/Bedrock/Field/Translation/Proofs/Expr.v
@@ -30,9 +30,9 @@ Import Wf.Compilers.expr.
 Import Types.Notations.
 
 Section Expr.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance Types.rep.Z.
diff --git a/src/Bedrock/Field/Translation/Proofs/Flatten.v b/src/Bedrock/Field/Translation/Proofs/Flatten.v
index b1797c5daa..5294a76d0a 100644
--- a/src/Bedrock/Field/Translation/Proofs/Flatten.v
+++ b/src/Bedrock/Field/Translation/Proofs/Flatten.v
@@ -29,9 +29,9 @@ Import Types.Notations.
    conversions between the two. *)
 
 Section Flatten.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   (* these conversions should happen before loading arguments and after
        storing return values, so they use in-memory lists *)
@@ -183,7 +183,7 @@ Section Flatten.
       (varname_set_listonly names).
   Proof.
     induction t;
-      cbn [extract_listnames fst snd varname_set_listonly 
+      cbn [extract_listnames fst snd varname_set_listonly
                              flatten_listonly_base_ltype];
       break_match; intros; rewrite ?of_list_nil; try reflexivity;
         [ | ].
diff --git a/src/Bedrock/Field/Translation/Proofs/Func.v b/src/Bedrock/Field/Translation/Proofs/Func.v
index 86364aabc5..3e259d2ff0 100644
--- a/src/Bedrock/Field/Translation/Proofs/Func.v
+++ b/src/Bedrock/Field/Translation/Proofs/Func.v
@@ -36,9 +36,9 @@ Import Wf.Compilers.expr.
 Import Types.Notations.
 
 Section Func.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance rep.Z.
@@ -88,7 +88,7 @@ Section Func.
       forall (tr : Semantics.trace)
              (locals : locals)
              (mem : mem)
-             (functions : list (string*func)),
+             functions,
         (* locals doesn't contain variables we could overwrite *)
         (forall n nvars,
             (nextn <= n)%nat ->
@@ -100,7 +100,7 @@ Section Func.
         context_equiv G locals ->
         (* executing translation output is equivalent to interpreting e *)
         WeakestPrecondition.cmd
-          (WeakestPrecondition.call functions)
+          functions
           body tr mem locals
           (fun tr' mem' locals' =>
              tr = tr' /\
@@ -142,7 +142,7 @@ Section Func.
       inversion 1; cleanup_wf;
       cbv [translate_func']; intros.
       all:eapply Proper_cmd;
-        [solve [apply Proper_call] | repeat intro
+         [ repeat intro
          | eapply (translate_cmd_correct (t:=type.base _));
            solve [eauto] ];
         cbv beta in *; cleanup; subst; tauto. }
@@ -505,14 +505,12 @@ Section Func.
          (function arguments, function return variable names, body) *)
       let out := translate_func
                    e argnames arglengths argsizes retnames retsizes in
-      let f : string*func := (fname, fst out) in
-      let lengths := snd out in
       forall tr
              (mem : mem)
              (flat_args : list word)
              (out_ptrs : list word)
              (argvalues : list word)
-             (functions : list (string*func))
+             (functions : Semantics.env)
              (R : _ -> Prop),
         (* argument values are the concatenation of true argument values
            and output pointer values *)
@@ -544,9 +542,10 @@ Section Func.
         (* seplogic frame for return values *)
         sep (lists_reserved_with_initial_context
                retlengths argnames retnames retsizes argvalues) R mem ->
+        map.get functions fname = Some (fst out) ->
         (* translated function produces equivalent results *)
         WeakestPrecondition.call
-          (f :: functions) fname tr mem argvalues
+          functions fname tr mem argvalues
           (fun tr' mem' flat_rets =>
              tr = tr' /\
              (* lengths of output lists match *)
@@ -559,10 +558,8 @@ Section Func.
                  R mem').
   Proof.
     cbv [translate_func]; intros. subst.
-    cbn [fst snd
-             WeakestPrecondition.call
-             WeakestPrecondition.call_body WeakestPrecondition.func].
-    rewrite eqb_refl.
+    eapply start_func. 1: eassumption.
+    cbn [fst snd WeakestPrecondition.func].
     match goal with
       |- exists l, map.of_list_zip ?ks ?vs = Some l /\ _ =>
       assert (NoDup ks);
@@ -592,11 +589,11 @@ Section Func.
         cbv [Option.bind] in *; repeat break_match_hyps; try congruence; [ ]
     end.
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
-    eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+    eapply Proper_cmd; [ repeat intro | ].
     2 : { eapply load_arguments_correct; try eassumption; eauto.
           eapply equivalent_flat_args_iff1; eauto. }
     cbv beta in *. cleanup; subst.
-    eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+    eapply Proper_cmd; [ repeat intro | ].
     2 : { eapply @translate_func'_correct with (args:=args);
           cbv [context_equiv]; intros; try apply Wf3_of_Wf; eauto; [ ].
           eapply only_differ_disjoint_undef_on; eauto;
@@ -613,7 +610,7 @@ Section Func.
           eapply disjoint_sym.
           eapply disjoint_used_varnames_lt; eauto with lia. }
     cbv beta in *. cleanup; subst.
-    eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+    eapply Proper_cmd; [ repeat intro | ].
     2 : {
       cbv [lists_reserved_with_initial_context] in *.
       break_match_hyps; try congruence; [ ].
diff --git a/src/Bedrock/Field/Translation/Proofs/LoadStoreList.v b/src/Bedrock/Field/Translation/Proofs/LoadStoreList.v
index 8fb5e655dc..8e45c8835e 100644
--- a/src/Bedrock/Field/Translation/Proofs/LoadStoreList.v
+++ b/src/Bedrock/Field/Translation/Proofs/LoadStoreList.v
@@ -34,9 +34,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section LoadStoreList.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance rep.Z.
@@ -316,7 +316,7 @@ Section LoadStoreList.
                       (listZ:=rep.listZ_mem) base_listZ)
            (locals : locals)
            (mem : mem)
-           (functions : list _)
+           functions
            (R : _ -> Prop),
       (forall (n : nat) (H : nextn <= n), name <> varname_gen n) ->
       base_access_sizes_good sizes ->
@@ -329,7 +329,7 @@ Section LoadStoreList.
       let names' : base_ltype (listZ:=rep.listZ_local) base_listZ
           := snd (fst out) in
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (snd out)
         tr mem locals
         (fun tr' mem' locals' =>
@@ -359,7 +359,7 @@ Section LoadStoreList.
       eexists; split; cbv [dlet.dlet].
       { eapply load_list_item_correct; try eassumption.
         cbn [Datatypes.length]; lia. }
-      eapply Proper_cmd; [ solve [apply Proper_call] | | ].
+      eapply Proper_cmd.
       2:{
         eapply IHrem; eauto with lia.
         eapply Proper_sep_iff1; [ | reflexivity | eassumption ].
@@ -414,7 +414,7 @@ Section LoadStoreList.
     forall (argnames : base_ltype t)
            (argsizes : base_access_sizes t)
            (args : base.interp t)
-           (functions : list _)
+           functions
            tr
            (locals : locals)
            (mem : mem)
@@ -441,7 +441,7 @@ Section LoadStoreList.
         let argvalues' := base_rtype_of_ltype argnames' in
         (* translated function produces equivalent results *)
         WeakestPrecondition.cmd
-          (WeakestPrecondition.call functions)
+          functions
           (snd out)
           tr mem locals
           (fun tr' mem' locals' =>
@@ -470,7 +470,7 @@ Section LoadStoreList.
         eauto using only_differ_zero with lia. }
     { (* product *)
       straightline.
-      eapply Proper_cmd; [ solve [apply Proper_call] | | ].
+      eapply Proper_cmd.
       2:{ eapply IHt1; eauto.
           { intros.
             match goal with
@@ -482,7 +482,7 @@ Section LoadStoreList.
             cancel_seps_at_indices 0%nat 0%nat; trivial.
             ecancel_done. } }
       repeat intro. cleanup; subst.
-      eapply Proper_cmd; [ solve [apply Proper_call] | | ].
+      eapply Proper_cmd.
       2:{ eapply IHt2; eauto.
           { intros.
             match goal with
@@ -522,8 +522,7 @@ Section LoadStoreList.
     clear IHt.
      cbn [flatten_base_rtype base_rtype_of_ltype] in *.
     eapply Proper_cmd;
-      [ solve [apply Proper_call]
-      | | eapply load_list_correct; eauto; reflexivity ].
+      [ | eapply load_list_correct; eauto; reflexivity ].
     repeat intro. cleanup; subst.
     repeat match goal with |- _ /\ _ => split end;
       eauto using only_differ_step. }
@@ -533,7 +532,7 @@ Section LoadStoreList.
     forall (argnames : type.for_each_lhs_of_arrow ltype t)
            (argsizes : type.for_each_lhs_of_arrow access_sizes t)
            (args : type.for_each_lhs_of_arrow API.interp_type t)
-           (functions : list _)
+           functions
            tr
            (locals : locals)
            (mem : mem)
@@ -561,7 +560,7 @@ Section LoadStoreList.
             type.map_for_each_lhs_of_arrow rtype_of_ltype argnames' in
         (* translated function produces equivalent results *)
         WeakestPrecondition.cmd
-          (WeakestPrecondition.call functions)
+          functions
           (snd out)
           tr mem locals
           (fun tr' mem' locals' =>
@@ -590,7 +589,7 @@ Section LoadStoreList.
     { (* arrow (base _) _ *)
       cleanup. straightline.
       eapply Proper_cmd.
-      3:{
+      2:{
         eapply load_all_lists_correct; eauto; [ ].
         intros.
         match goal with
@@ -598,9 +597,8 @@ Section LoadStoreList.
           setoid_rewrite not_union_iff in H;
             apply H; eauto
         end. }
-      { apply Proper_call. }
       { repeat intro; cleanup; subst.
-        eapply Proper_cmd; [ solve [apply Proper_call] | | ].
+        eapply Proper_cmd.
         2:{
           eapply IHt2; eauto.
         { intros.
@@ -640,7 +638,7 @@ Section LoadStoreList.
   Lemma store_list_correct :
     forall (size : access_size)
            (start : string)
-           (functions : list _)
+           functions
            (value_names2 value_names1 : list string)
            (rets1 rets2 rets : base.interp base_listZ)
            (i : nat)
@@ -674,7 +672,7 @@ Section LoadStoreList.
                           rets1 (expr.var start) size locals)
                (lists_reserved retlengths loc' size locals)) R m ->
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (store_list (width:=width) size (expr.var start) values2 i) tr m locals
         (fun tr' mem' locals' =>
            tr = tr' /\
@@ -776,7 +774,7 @@ Section LoadStoreList.
              | H : Forall _ (_ :: _) |- _ => inversion H; subst; clear H
              end.
 
-      eapply Proper_cmd; [ solve [apply Proper_call] | repeat intro | ].
+      eapply Proper_cmd; [ repeat intro | ].
       2:{
         let s :=
             lazymatch goal with
@@ -870,7 +868,7 @@ Section LoadStoreList.
            (retsizes : base_access_sizes t)
            (vset : set string)
            (rets : base.interp t)
-           (functions : list _)
+           functions
            tr
            (locals : locals)
            (mem : mem)
@@ -898,7 +896,7 @@ Section LoadStoreList.
       base_access_sizes_good retsizes ->
       (* translated function produces equivalent results *)
       WeakestPrecondition.cmd
-        (WeakestPrecondition.call functions)
+        functions
         (snd out)
         tr mem locals
         (fun tr' mem' locals' =>
@@ -950,13 +948,13 @@ Section LoadStoreList.
                apply undef_on_union_iff in H
              end.
       eapply Proper_cmd;
-        [ solve [apply Proper_call] | repeat intro
+          [ repeat intro
           | eapply IHt1; try ecancel_assumption;
             try (apply undef_on_union_iff; split);
             solve [eauto] ].
       cbv beta in *. cleanup; subst.
       eapply Proper_cmd;
-        [ solve [apply Proper_call] | repeat intro | ].
+        [ repeat intro | ].
       2:{ eapply IHt2 with
               (vset:=union vset (varname_set_listexcl (fst retnames_mem)));
           try ecancel_assumption; eauto.
@@ -993,7 +991,7 @@ Section LoadStoreList.
       cbn [rep.Z rep.listZ_mem rep.equiv rep.rtype_of_ltype] in *.
       sepsimpl.
       eapply Proper_cmd;
-        [ solve [apply Proper_call] | repeat intro | ].
+        [ repeat intro | ].
       2:{
         eapply store_list_correct with
             (rets:=rets) (rets1:=[]) (rets2:=rets)
diff --git a/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v b/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
index 8c7b93fc75..e0f1c4831b 100644
--- a/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
+++ b/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
@@ -23,9 +23,9 @@ Import API.Compilers.
 Import ListNotations Types.Notations.
 
 Section UsedVarnames.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
   Local Existing Instance Types.rep.Z.
   Local Instance varname_eqb_spec x y : BoolSpec _ _ _
diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
index f5c26ea960..4227898e52 100644
--- a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
+++ b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
@@ -24,9 +24,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Cmd.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance Types.rep.Z.
diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
index e511e486d3..e2fb50f6a4 100644
--- a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
+++ b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
@@ -22,9 +22,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Expr.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok}.
 
   Local Existing Instance Types.rep.Z.
diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
index 485765a312..bf3620edc0 100644
--- a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
+++ b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Func.v
@@ -23,9 +23,9 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section Func.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
-   `{parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}.
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
+   `{parameters_sentinel : @parameters width BW word mem locals ext_spec varname_gen error}.
   Context {ok : ok }.
   Local Existing Instance Types.rep.Z.
 
diff --git a/src/Bedrock/Field/Translation/Proofs/VarnameSet.v b/src/Bedrock/Field/Translation/Proofs/VarnameSet.v
index 764bf40d44..ac81fd7207 100644
--- a/src/Bedrock/Field/Translation/Proofs/VarnameSet.v
+++ b/src/Bedrock/Field/Translation/Proofs/VarnameSet.v
@@ -7,10 +7,10 @@ Import API.Compilers.
 Import Types.Notations.
 
 Section VarnameSet.
-  Context 
-    {width BW word mem locals env ext_spec varname_gen error}
+  Context
+    {width BW word mem locals ext_spec varname_gen error}
    `{parameters_sentinel : @parameters
-     width BW word mem locals env ext_spec varname_gen error}.
+     width BW word mem locals ext_spec varname_gen error}.
   Context {listZ : rep.rep base_listZ}.
   Existing Instance rep.Z.
 
diff --git a/src/Bedrock/Group/AdditionChains.v b/src/Bedrock/Group/AdditionChains.v
index 0d5804a6a3..a96432a515 100644
--- a/src/Bedrock/Group/AdditionChains.v
+++ b/src/Bedrock/Group/AdditionChains.v
@@ -29,11 +29,9 @@ Section FElems.
 
   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 Impl.
@@ -498,7 +496,7 @@ Section FElems.
               cmd.seq (cmd.call [] "fe25519_inv" [expr.var out_var; expr.var x_var]) k_impl
 
               <{ pred (let/n x as out_var eq:Heq := v in k x Heq) }>.
-      Proof using F_M_pos env_ok ext_spec_ok field_representation_ok locals_ok mem_ok word_ok.
+      Proof using F_M_pos ext_spec_ok field_representation_ok locals_ok mem_ok word_ok.
         repeat straightline.
         repeat (eexists; split; eauto).
         straightline_call.
@@ -636,7 +634,7 @@ Section FElems.
     Lemma fe_inv_correct :
       Z.pos M_pos = 2^255-19 ->
       program_logic_goal_for_function! fe25519_inv.
-    Proof using env_ok ext_spec_ok field_representation_ok locals_ok mem_ok word_ok.
+    Proof using ext_spec_ok field_representation_ok locals_ok mem_ok word_ok.
       intros Hm HmPrime ? ** ? **.
       eapply Proper_call; [|eapply fe25519_inv_correct_exp; eauto 1; exact I].
       intros ? ** ? ** ? ** ?; intuition idtac.
diff --git a/src/Bedrock/Group/Point.v b/src/Bedrock/Group/Point.v
index 3c8f5cfbfd..0f7ba7c4a0 100644
--- a/src/Bedrock/Group/Point.v
+++ b/src/Bedrock/Group/Point.v
@@ -10,11 +10,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}.
   Context {field_parameters : FieldParameters}
           {field_representation : FieldRepresentation}.
diff --git a/src/Bedrock/Group/ScalarMult/CSwap.v b/src/Bedrock/Group/ScalarMult/CSwap.v
index be4291ee52..5cb176ab3c 100644
--- a/src/Bedrock/Group/ScalarMult/CSwap.v
+++ b/src/Bedrock/Group/ScalarMult/CSwap.v
@@ -24,11 +24,9 @@ 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 {field_parameters : FieldParameters}.
   Context {field_representaton : FieldRepresentation}.
@@ -586,7 +584,7 @@ Section __.
           (cmd.call [] "felem_cswap" [expr.var mask_var; expr.var lhs_var; expr.var rhs_var])
           k_impl
         <{ pred (nlet_eq [lhs_var; rhs_var] v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     unfold FElem, Field.FElem.
     rewrite !Bignum_as_array.
     repeat straightline' locals.
diff --git a/src/Bedrock/Group/ScalarMult/LadderStep.v b/src/Bedrock/Group/ScalarMult/LadderStep.v
index 3313e7af92..e5e5263a39 100644
--- a/src/Bedrock/Group/ScalarMult/LadderStep.v
+++ b/src/Bedrock/Group/ScalarMult/LadderStep.v
@@ -33,11 +33,9 @@ End Gallina.
 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 {field_parameters : FieldParameters}
           {field_representaton : FieldRepresentation}
@@ -115,7 +113,7 @@ Section __.
       <{ pred (nlet_eq
                  [X2_var; Z2_var; X3_var; Z3_var]
                  v k) }>.
-  Proof using env_ok ext_spec_ok locals_ok mem_ok word_ok.
+  Proof using ext_spec_ok locals_ok mem_ok word_ok.
     repeat straightline'.
     handle_call.
     apply H6.
diff --git a/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v b/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
index 4410de585b..fa6f90ad80 100644
--- a/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
+++ b/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
@@ -75,11 +75,9 @@ 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 {field_parameters : FieldParameters}.
   Context {field_representaton : FieldRepresentation}.
@@ -220,26 +218,26 @@ Section __.
   Hint Extern 1 (spec_of "ladderstep") =>
   (simple refine (@spec_of_ladderstep _ _ _ _ _ _ _ _)) : typeclass_instances.
 
-  
+
   Hint Extern 1 (spec_of "cswap") =>
   (simple refine (spec_of_cswap)) : typeclass_instances.
-    
+
   (* TODO: this seems a bit delicate*)
   Ltac compile_cswap :=
     eapply compile_felem_cswap;
     [solve[repeat compile_step] ..
     | repeat compile_step;
       rewrite cswap_same;
-      compile_step;      
+      compile_step;
       match goal with
       | [|- (WeakestPrecondition.cmd _ _ _ _ _ (_ (let (_,_) := ?v in _)))] =>
         destruct v
       end].
-  
+
   Hint Extern 8 (WeakestPrecondition.cmd _ _ _ _ _ (_ (nlet_eq _ (cswap _ _ _) _))) =>
   compile_cswap; shelve : compiler.
-  
-  
+
+
   Lemma word_unsigned_of_Z_eq z
     : 0 <= z < 2 ^ width -> word.unsigned (word.of_Z z : word) = z.
   Proof using word_ok.
@@ -303,7 +301,7 @@ Section __.
 
   Hint Extern 1 (spec_of "fe25519_inv") => (simple refine (spec_of_exp_large)) : typeclass_instances.
   Hint Extern 1 (spec_of "felem_cswap") => (simple refine (spec_of_cswap)) : typeclass_instances.
-  
+
     Derive montladder_body SuchThat
            (defn! "montladder" ("OUT", "K", "U")
                 { montladder_body },
diff --git a/src/Bedrock/Group/ScalarMult/ScalarMult.v b/src/Bedrock/Group/ScalarMult/ScalarMult.v
index 7481fd3f90..549170c033 100644
--- a/src/Bedrock/Group/ScalarMult/ScalarMult.v
+++ b/src/Bedrock/Group/ScalarMult/ScalarMult.v
@@ -17,11 +17,9 @@ Module M.
   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 {field_parameters : FieldParameters}
             {field_parameters_ok : FieldParameters_ok}
@@ -223,18 +221,15 @@ Module M.
       (* speedier proof if straightline doesn't try to compute the stack
          allocation sizes *)
       Local Opaque felem_size_in_bytes.
-      Lemma scmul_func_correct : forall functions, spec_of_scmul ((scmul, scmul_func)::functions).
+      Lemma scmul_func_correct : forall functions,
+          map.get functions scmul = Some scmul_func ->
+          spec_of_scmul functions.
       Proof.
         (* straightline doesn't work properly for setup, so the first step
            is inlined and changed here *)
         enter scmul_func. intros.
-        WeakestPrecondition.unfold1_call_goal.
-        (cbv beta match delta [WeakestPrecondition.call_body]).
-        lazymatch goal with
-        | |- if ?test then ?T else _ =>
-          replace test with true by (rewrite String.eqb_refl; reflexivity);
-            change_no_check T
-        end; (cbv beta match delta [WeakestPrecondition.func]).
+        eapply start_func. 1: eassumption.
+        cbv beta match delta [WeakestPrecondition.func].
 
         cbv [GElem x_representation grepresents xrepresents] in *.
         sepsimpl.
diff --git a/src/Bedrock/Specs/Field.v b/src/Bedrock/Specs/Field.v
index 30d668fdcf..9f8d763ac8 100644
--- a/src/Bedrock/Specs/Field.v
+++ b/src/Bedrock/Specs/Field.v
@@ -116,11 +116,9 @@ End BignumToFieldRepresentationAdapterLemmas.
 Section FunctionSpecs.
   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 {field_parameters : FieldParameters}
           {field_representation : FieldRepresentation}.
@@ -249,13 +247,13 @@ Section FunctionSpecs.
     Definition r := 2 ^ width.
     Definition m' := Z.modinv (- M) r.
     Definition r' := Z.modinv (r) M.
-  
+
     Definition from_mont_model x := F.mul x (@F.of_Z M_pos (r' ^ (Z.of_nat felem_size_in_words)%Z)).
     Definition to_mont_model x := F.mul x (@F.of_Z M_pos (r ^ (Z.of_nat felem_size_in_words)%Z)).
-  
+
     Instance un_from_mont {from_mont : string} : UnOp from_mont :=
       {| un_model := from_mont_model; un_xbounds := tight_bounds; un_outbounds := loose_bounds |}.
-  
+
     Instance un_to_mont {to_mont : string} : UnOp to_mont :=
       {| un_model := to_mont_model; un_xbounds := tight_bounds; un_outbounds := loose_bounds|}.
 
@@ -268,11 +266,9 @@ Existing Instances spec_of_UnOp spec_of_BinOp bin_mul un_square bin_add bin_sub
 Section SpecProperties.
   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 {field_parameters : FieldParameters}
           {field_representation : FieldRepresentation}
diff --git a/src/Bedrock/Specs/Group.v b/src/Bedrock/Specs/Group.v
index a611c32908..1e09758e33 100644
--- a/src/Bedrock/Specs/Group.v
+++ b/src/Bedrock/Specs/Group.v
@@ -32,7 +32,6 @@ Class GroupRepresentation {G : Type} {width} {BW:Bitwidth.Bitwidth width} {word
 Section FunctionSpecs.
   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 {group_parameters : GroupParameters}
           {group_representaton : GroupRepresentation (G:=G)}