From 8fa2cc3bfbc939653ad9f3bb60e123aa73dcc13a Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Mon, 31 Jul 2023 21:27:24 -0400
Subject: [PATCH] hardcode env implementation in bedrock2.Semantics,

and update compiler, LiveVerif, end2end
---
 LiveVerif/src/LiveVerif/LiveProgramLogic.v    | 26 +++++-----
 LiveVerif/src/LiveVerif/LiveRules.v           | 47 ++++++-------------
 bedrock2/src/bedrock2/FrameRule.v             |  1 -
 bedrock2/src/bedrock2/ProgramLogic.v          |  4 +-
 bedrock2/src/bedrock2/Semantics.v             | 18 +++++--
 bedrock2/src/bedrock2/WP.v                    | 31 ++++++++----
 bedrock2/src/bedrock2Examples/Trace.v         |  4 --
 bedrock2/src/bedrock2Examples/memequal.v      |  1 -
 bedrock2/src/bedrock2Examples/memmove.v       |  1 -
 bedrock2/src/bedrock2Examples/memswap.v       |  1 -
 compiler/src/compiler/ExprImp.v               |  2 -
 compiler/src/compiler/ExprImpEventLoopSpec.v  |  2 +-
 compiler/src/compiler/FlattenExpr.v           |  2 -
 compiler/src/compiler/FlattenExprDef.v        |  3 +-
 compiler/src/compiler/Pipeline.v              | 21 +++++----
 compiler/src/compiler/ToplevelLoop.v          |  2 +
 .../src/compilerExamples/SoftmulCompile.v     |  4 +-
 end2end/src/end2end/End2EndLightbulb.v        | 34 +++++++++-----
 end2end/src/end2end/End2EndPipeline.v         | 10 ++--
 19 files changed, 108 insertions(+), 106 deletions(-)

diff --git a/LiveVerif/src/LiveVerif/LiveProgramLogic.v b/LiveVerif/src/LiveVerif/LiveProgramLogic.v
index cac63dcd..5265ba42 100644
--- a/LiveVerif/src/LiveVerif/LiveProgramLogic.v
+++ b/LiveVerif/src/LiveVerif/LiveProgramLogic.v
@@ -42,22 +42,24 @@ Require Import bedrock2.LogSidecond.
 
 Definition functions_correct
   (* universally quantified abstract function list containing all functions: *)
-  (qfs: list (string * func)):
+  (qfs: Semantics.env):
   (* specs of a subset of functions for which to assert correctness *)
-  list (list (string * func) -> Prop (* spec_of mentioning function name *)) -> Prop :=
+  list (Semantics.env -> Prop (* spec_of mentioning function name *)) -> Prop :=
   List.Forall (fun spec => spec qfs).
 
 Definition function_with_callees: Type :=
-  func * list (list (string * func) -> Prop (* spec_of mentioning function name *)).
+  func * list (Semantics.env -> Prop (* spec_of mentioning function name *)).
 
 Definition program_logic_goal_for(name: string)(f: function_with_callees)
   {spec: bedrock2.ProgramLogic.spec_of name}: Prop :=
   match f with
   | (impl, callees) => forall functions,
-      functions_correct functions callees -> spec (cons (name, impl) functions)
+      map.get functions name = Some impl ->
+      functions_correct functions callees ->
+      spec functions
   end.
 
-Definition nth_spec(specs: list (list (string * func) -> Prop))(n: nat) :=
+Definition nth_spec(specs: list (Semantics.env -> Prop))(n: nat) :=
   Eval unfold List.nth in (List.nth n specs (fun _ => True)).
 
 Lemma nth_function_correct: forall fs n specs spec,
@@ -143,22 +145,18 @@ Ltac start :=
       subst evar;
       unfold program_logic_goal_for, spec;
       let fs := fresh "fs" in
+      let G := fresh "EnvContains" in
       let fs_ok := fresh "fs_ok" in
-      intros fs fs_ok;
+      intros fs G fs_ok;
       let nP := fresh "Scope0" in pose proof (mk_scope_marker FunctionParams) as nP;
       intros_until_trace;
       let nB := fresh "Scope0" in pose proof (mk_scope_marker FunctionBody) as nB;
       lazymatch goal with
       | |- forall (t : trace) (m : @map.rep (@word.rep _ _) Init.Byte.byte _), _ => intros
       end;
-      WeakestPrecondition.unfold1_call_goal;
-      cbv match beta delta [WeakestPrecondition.call_body];
-      lazymatch goal with
-      | |- if ?test then ?T else _ =>
-        replace test with true by reflexivity; change T
-      end;
       eapply prove_func;
-      [ lazymatch goal with
+      [ exact G
+      | lazymatch goal with
         | |- map.of_list_zip ?argnames_evar ?argvalues = Some ?locals_evar =>
              let argnames := map_with_ltac varconstr_to_string argvalues in
              unify argnames_evar argnames;
@@ -166,7 +164,7 @@ Ltac start :=
              unify locals_evar (map.of_list kvs);
              reflexivity
         end
-      | ];
+      | clear G ];
       first [eapply simplify_no_return_post | eapply simplify_1retval_post];
       pose_state stepping
   | |- _ => fail "goal needs to be of shape (@program_logic_goal_for ?fname ?evar ?spec)"
diff --git a/LiveVerif/src/LiveVerif/LiveRules.v b/LiveVerif/src/LiveVerif/LiveRules.v
index d67b558d..69d83d6c 100644
--- a/LiveVerif/src/LiveVerif/LiveRules.v
+++ b/LiveVerif/src/LiveVerif/LiveRules.v
@@ -356,31 +356,18 @@ Section WithParams.
     - assumption.
   Qed.
 
-  Ltac pose_env :=
-    let env := fresh "env" in
-    unshelve epose (env := _ : map.map string (list string * list string * cmd));
-    [ eapply SortedListString.map
-    | assert (env_ok: map.ok env) by apply SortedListString.ok; clearbody env ].
-
   Lemma WP_weaken_cmd: forall fs c t m l (post1 post2: _->_->_->Prop),
-      WeakestPrecondition.cmd (call fs) c t m l post1 ->
+      WeakestPrecondition.cmd fs c t m l post1 ->
       (forall t m l, post1 t m l -> post2 t m l) ->
-      WeakestPrecondition.cmd (call fs) c t m l post2.
-  Proof.
-    pose_env. intros.
-    eapply WeakestPreconditionProperties.Proper_cmd. 3: eassumption.
-    1: eapply WeakestPreconditionProperties.Proper_call.
-    cbv [RelationClasses.Reflexive Morphisms.pointwise_relation
-         Morphisms.respectful Basics.impl].
-    assumption.
-  Qed.
+      WeakestPrecondition.cmd fs c t m l post2.
+  Proof. eapply WeakestPreconditionProperties.weaken_cmd. Qed.
 
-  Inductive wp_cmd(fs: list (string * (list string * list string * cmd)))
+  Inductive wp_cmd(fs: Semantics.env)
             (c: cmd)(t: trace)(m: mem)(l: locals)(post: trace -> mem -> locals -> Prop):
-    Prop := mk_wp_cmd(_: WeakestPrecondition.cmd (call fs) c t m l post).
+    Prop := mk_wp_cmd(_: WeakestPrecondition.cmd fs c t m l post).
 
   Lemma invert_wp_cmd: forall fs c t m l post,
-      wp_cmd fs c t m l post -> WeakestPrecondition.cmd (call fs) c t m l post.
+      wp_cmd fs c t m l post -> WeakestPrecondition.cmd fs c t m l post.
   Proof. intros. inversion H; assumption. Qed.
 
   Lemma weaken_wp_cmd: forall fs c t m l (post1 post2: _->_->_->Prop),
@@ -568,7 +555,7 @@ Section WithParams.
     all: eauto using weaken_wp_cmd.
   Qed.
 
-  Definition after_loop: list (string * (list string * list string * cmd)) ->
+  Definition after_loop: Semantics.env ->
     cmd -> trace -> mem -> locals -> (trace -> mem -> locals -> Prop) -> Prop := wp_cmd.
 
   Lemma wp_set: forall fs x e v t m l rest post,
@@ -762,7 +749,7 @@ Section WithParams.
                   True)
     : wp_cmd fs (cmd.seq (cmd.while e c) rest) t m l post.
   Proof.
-    econstructor. cbn. exists measure, lt, invariant.
+    econstructor. cbn. eapply wp_while. exists measure, lt, invariant.
     split. 1: assumption.
     split. 1: eauto.
     clear Hpre v0 t m l.
@@ -805,7 +792,6 @@ Section WithParams.
   Proof.
     eapply wp_seq.
     econstructor. cbn.
-    pose_env.
     eapply tailrec_localsmap_1ghost with
       (P := fun v g t m l => pre (g, v, t, m, l))
       (Q := fun v g t m l => post (g, v, t, m, l)).
@@ -1000,9 +986,6 @@ Section WithParams.
     specialize (H Pre). clear Pre.
     eapply wp_seq.
     eapply wp_call0. 1: eassumption.
-    unshelve epose (env := _ : map.map string func).
-    1: eapply SortedListString.map.
-    assert (env_ok: map.ok env) by apply SortedListString.ok. clearbody env.
     eapply WeakestPreconditionProperties.Proper_call. 2: eassumption. exact Impl.
   Qed.
 
@@ -1017,20 +1000,18 @@ Section WithParams.
       eapply IHretnames; eassumption.
   Qed.
 
-  Lemma prove_func: forall fs argnames retnames body t m argvals l post,
+  Lemma prove_func: forall fs f argnames retnames body t m argvals l post,
+      map.get fs f = Some (argnames, retnames, body) ->
       map.of_list_zip argnames argvals = Some l ->
       wp_cmd fs body t m l (fun t' m' l' => exists retvals,
                                 map.getmany_of_list l' retnames = Some retvals /\
                                   post t' m' retvals) ->
-      WeakestPrecondition.func (call fs) (argnames, retnames, body) t m argvals post.
+      WeakestPrecondition.call fs f t m argvals post.
   Proof.
     intros.
-    unfold func.
-    eexists. split. 1: eassumption.
-    eapply invert_wp_cmd.
-    eapply weaken_wp_cmd. 1: eassumption.
-    cbv beta. intros. fwd.
-    eapply cpsify_getmany_of_list; eassumption.
+    eapply WP.WP_Impl.mk_wp_call. 1,2: eassumption. eapply WP.WP_Impl.mk_wp_cmd.
+    intros. eapply invert_wp_cmd in H1. eapply WeakestPreconditionProperties.sound_cmd.
+    assumption.
   Qed.
 
   (* applied at beginning of void functions *)
diff --git a/bedrock2/src/bedrock2/FrameRule.v b/bedrock2/src/bedrock2/FrameRule.v
index 370f7139..6a621014 100644
--- a/bedrock2/src/bedrock2/FrameRule.v
+++ b/bedrock2/src/bedrock2/FrameRule.v
@@ -16,7 +16,6 @@ Require Import Coq.Lists.List.
 Section semantics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
   Context {mem_ok: map.ok mem} {word_ok: word.ok word}.
 
diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v
index dca598f5..96adbc64 100644
--- a/bedrock2/src/bedrock2/ProgramLogic.v
+++ b/bedrock2/src/bedrock2/ProgramLogic.v
@@ -7,7 +7,7 @@ Require Import bedrock2.WeakestPreconditionProperties.
 Require Import bedrock2.Loops.
 Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.
 
-Definition spec_of (procname:String.string) := env -> Prop.
+Definition spec_of (procname:String.string) := Semantics.env -> Prop.
 Existing Class spec_of.
 
 Module Import Coercions.
@@ -57,7 +57,7 @@ Ltac program_logic_goal_for_function proc :=
   let __ := constr:(proc : Syntax.func) in
   constr_string_basename_of_constr_reference_cps ltac:(Tactics.head proc) ltac:(fun fname =>
   let spec := lazymatch constr:(_:spec_of fname) with ?s => s end in
-  exact (forall (functions : @map.rep _ _ env) (EnvContains : map.get functions fname = Some proc), ltac:(
+  exact (forall (functions : @map.rep _ _ Semantics.env) (EnvContains : map.get functions fname = Some proc), ltac:(
     let callees := eval cbv in (callees (snd proc)) in
     let s := assuming_correctness_of_in callees functions (spec functions) in
     exact s))).
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
index 1820df16..ffec59ea 100644
--- a/bedrock2/src/bedrock2/Semantics.v
+++ b/bedrock2/src/bedrock2/Semantics.v
@@ -3,6 +3,7 @@ Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList.
 Require Import coqutil.Decidable.
 Require Import coqutil.Tactics.fwd.
 Require Import coqutil.Map.Properties.
+Require coqutil.Map.SortedListString.
 Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.MetricLogging.
@@ -78,10 +79,12 @@ Section binops.
     end.
 End binops.
 
+#[export] Instance env: map.map String.string Syntax.func := SortedListString.map _.
+#[export] Instance env_ok: map.ok env := SortedListString.ok _.
+
 Section semantics.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
   Local Notation metrics := MetricLog.
@@ -157,11 +160,11 @@ Section semantics.
   End WithMemAndLocals.
 End semantics.
 
-Module exec. Section WithEnv.
+Module exec. Section WithParams.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
+  Section WithEnv.
   Context (e: env).
 
   Local Notation metrics := MetricLog.
@@ -369,4 +372,13 @@ Module exec. Section WithEnv.
   Qed.
 
   End WithEnv.
+
+  Lemma extend_env: forall e1 e2,
+      map.extends e2 e1 ->
+      forall c t m l mc post,
+      exec e1 c t m l mc post ->
+      exec e2 c t m l mc post.
+  Proof. induction 2; try solve [econstructor; eauto]. Qed.
+
+  End WithParams.
 End exec. Notation exec := exec.exec.
diff --git a/bedrock2/src/bedrock2/WP.v b/bedrock2/src/bedrock2/WP.v
index 45d3d1ef..5588d201 100644
--- a/bedrock2/src/bedrock2/WP.v
+++ b/bedrock2/src/bedrock2/WP.v
@@ -1,12 +1,8 @@
 Require Import Coq.ZArith.ZArith.
 Require Import coqutil.Map.Interface.
-Require coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.Syntax bedrock2.Semantics.
 
-#[export] Instance env: map.map String.string Syntax.func := SortedListString.map _.
-#[export] Instance env_ok: map.ok env := SortedListString.ok _.
-
 (* We want to make the definitions opaque to `hnf` (unfolds any definition, so a plain
    definition doesn't work) and to `repeat split` (applies constructors of all
    1-constructor inductives, so a 1-constructor inductive wrapping exec doesn't
@@ -99,10 +95,9 @@ Section WithParams.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width}
     {mem: map.map word Byte.byte}
     {locals: map.map String.string word}
-    {ext_spec: ExtSpec}
-    (e: env).
+    {ext_spec: ExtSpec}.
 
-  Lemma weaken_wp_cmd: forall c t m l (post1 post2: trace -> mem -> locals -> Prop),
+  Lemma weaken_wp_cmd: forall e c t m l (post1 post2: trace -> mem -> locals -> Prop),
       (forall t' m' l', post1 t' m' l' -> post2 t' m' l') ->
       wp_cmd e t m l c post1 -> wp_cmd e t m l c post2.
   Proof.
@@ -110,7 +105,7 @@ Section WithParams.
     eapply exec.weaken. 1: eassumption. eauto.
   Qed.
 
-  Lemma weaken_wp_call: forall f t m args (post1 post2: trace -> mem -> list word -> Prop),
+  Lemma weaken_wp_call: forall e f t m args (post1 post2: trace -> mem -> list word -> Prop),
       (forall t' m' rets, post1 t' m' rets -> post2 t' m' rets) ->
       wp_call e f t m args post1 -> wp_call e f t m args post2.
   Proof.
@@ -119,4 +114,24 @@ Section WithParams.
     eapply weaken_wp_cmd. 2: eassumption. firstorder eauto.
   Qed.
 
+  Lemma extend_env_wp_cmd: forall e1 e2,
+      map.extends e2 e1 ->
+      forall c t m l post,
+      wp_cmd e1 t m l c post ->
+      wp_cmd e2 t m l c post.
+  Proof.
+    intros. eapply mk_wp_cmd. intros. eapply invert_wp_cmd in H0.
+    eapply exec.extend_env; eassumption.
+  Qed.
+
+  Lemma extend_env_wp_call: forall e1 e2,
+      map.extends e2 e1 ->
+      forall f t m args post,
+      wp_call e1 f t m args post ->
+      wp_call e2 f t m args post.
+  Proof.
+    intros. eapply invert_wp_call in H0. destruct H0 as (? & ? & ? & ? & ? & ? & ?).
+    eapply mk_wp_call; eauto.
+    eapply extend_env_wp_cmd; eauto.
+  Qed.
 End WithParams.
diff --git a/bedrock2/src/bedrock2Examples/Trace.v b/bedrock2/src/bedrock2Examples/Trace.v
index 39d44aa3..f7ebc23a 100644
--- a/bedrock2/src/bedrock2Examples/Trace.v
+++ b/bedrock2/src/bedrock2Examples/Trace.v
@@ -139,7 +139,6 @@ Module SpiEth.
         write_byte b (((m, MMInput, [word.of_Z spi_tx_fifo]), (m, [x])) :: rest).
 
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Instance ext_spec: ExtSpec :=
       fun t mGive action (argvals: list word) (post: (mem -> list word -> Prop)) =>
@@ -238,7 +237,6 @@ Module Syscalls.
                        (m, [ret1; ret2; err]))].
 
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Instance ext_spec: ExtSpec :=
       fun t m action (argvals: list word) (post: (mem -> list word -> Prop)) =>
@@ -298,7 +296,6 @@ Module MMIOUsage.
     Context {word: word.word 32} {mem: map.map word Byte.byte} {mem_ok: map.ok mem}.
     Context {word_ok: word.ok word}.
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Definition squarer_correct := @squarer_correct SpiEth.MMIOMacros.
     (*Check squarer_correct.*)
@@ -311,7 +308,6 @@ Module SyscallsUsage.
     Context {word: word.word 32} {mem: map.map word Byte.byte} {mem_ok: map.ok mem}.
     Context {word_ok: word.ok word}.
     Context {locals: map.map String.string word}.
-    Context {funname_env: forall T, map.map String.string T}.
 
     Definition squarer_correct := @squarer_correct Syscalls.SyscallIOMacros.
     (*Check squarer_correct.*)
diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
index c1886784..41629648 100644
--- a/bedrock2/src/bedrock2Examples/memequal.v
+++ b/bedrock2/src/bedrock2Examples/memequal.v
@@ -38,7 +38,6 @@ Section WithParameters.
                        (r  = 1 :>Z <-> xs  = ys) }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
index ae0af189..75713954 100644
--- a/bedrock2/src/bedrock2Examples/memmove.v
+++ b/bedrock2/src/bedrock2Examples/memmove.v
@@ -53,7 +53,6 @@ Section WithParameters.
 
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
index cd3af9e9..7292d7e7 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -41,7 +41,6 @@ Section WithParameters.
       ensures t' m := m =* ys$@x * xs$@y * R /\ t=t' }.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
-    {env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
     {ext_spec_ok : ext_spec.ok ext_spec}.
 
   Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
diff --git a/compiler/src/compiler/ExprImp.v b/compiler/src/compiler/ExprImp.v
index 60015aea..899b8cb7 100644
--- a/compiler/src/compiler/ExprImp.v
+++ b/compiler/src/compiler/ExprImp.v
@@ -20,7 +20,6 @@ Open Scope Z_scope.
 Section ExprImp1.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
   Notation var := String.string (only parsing).
@@ -377,7 +376,6 @@ Ltac invert_eval_cmd :=
 Section ExprImp2.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * cmd)}.
   Context {ext_spec: ExtSpec}.
 
   Notation var := String.string (only parsing).
diff --git a/compiler/src/compiler/ExprImpEventLoopSpec.v b/compiler/src/compiler/ExprImpEventLoopSpec.v
index 777cd0a9..3b9ca998 100644
--- a/compiler/src/compiler/ExprImpEventLoopSpec.v
+++ b/compiler/src/compiler/ExprImpEventLoopSpec.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Coq.Strings.String.
 Require Import coqutil.Map.Interface coqutil.Word.Interface.
 Require Import bedrock2.MetricLogging.
+Require Import bedrock2.Semantics.
 Require Import compiler.SeparationLogic.
 Require Import compiler.LowerPipeline.
 Require Import compiler.Pipeline.
@@ -9,7 +10,6 @@ Require Import compiler.Pipeline.
 Section Params1.
   Context {width} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: Semantics.ExtSpec}.
 
   Set Implicit Arguments.
diff --git a/compiler/src/compiler/FlattenExpr.v b/compiler/src/compiler/FlattenExpr.v
index bc2e4611..a5dd4234 100644
--- a/compiler/src/compiler/FlattenExpr.v
+++ b/compiler/src/compiler/FlattenExpr.v
@@ -25,14 +25,12 @@ Section FlattenExpr1.
           {word_ok: word.ok word}
           {locals: map.map String.string word}
           {mem: map.map word Byte.byte}
-          {ExprImp_env: map.map string (list string * list string * cmd)}
           {FlatImp_env: map.map string (list string * list string * FlatImp.stmt string)}
           {ext_spec: ExtSpec}
           {NGstate: Type}
           {NG: NameGen String.string NGstate}
           {locals_ok: map.ok locals}
           {mem_ok: map.ok mem}
-          {ExprImp_env_ok: map.ok ExprImp_env}
           {FlatImp_env_ok: map.ok FlatImp_env}
           {ext_spec_ok: ext_spec.ok ext_spec}.
 
diff --git a/compiler/src/compiler/FlattenExprDef.v b/compiler/src/compiler/FlattenExprDef.v
index 2fd8a8f4..41ab0ee5 100644
--- a/compiler/src/compiler/FlattenExprDef.v
+++ b/compiler/src/compiler/FlattenExprDef.v
@@ -21,7 +21,6 @@ Section FlattenExpr1.
           {word_ok: word.ok word}
           {locals: map.map String.string word}
           {mem: map.map word byte}
-          {ExprImp_env: map.map string (list string * list string * cmd)}
           {FlatImp_env: map.map string (list string * list string * FlatImp.stmt string)}
           {ext_spec: ExtSpec}
           {NGstate: Type}
@@ -159,7 +158,7 @@ Section FlattenExpr1.
       let body' := fst (flattenStmt (freshNameGenState avoid) body) in
       Success (argnames, retnames, body').
 
-  Definition flatten_functions: ExprImp_env -> result FlatImp_env :=
+  Definition flatten_functions: Semantics.env -> result FlatImp_env :=
     map.try_map_values flatten_function.
 
 End FlattenExpr1.
diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v
index 6dd84f8b..6996e63b 100644
--- a/compiler/src/compiler/Pipeline.v
+++ b/compiler/src/compiler/Pipeline.v
@@ -140,10 +140,11 @@ Section WithWordAndMem.
       andb (Z.leb (-2048) x) (Z.ltb x 2048).
 
     Definition locals_based_call_spec{Var Cmd: Type}{locals: map.map Var word}
-               (Exec: string_keyed_map (list Var * list Var * Cmd) ->
+               {string_keyed_map: forall T: Type, map.map string T}
+               (Exec: string_keyed_map (list Var * list Var * Cmd)%type ->
                       Cmd -> trace -> mem -> locals -> MetricLog ->
                       (trace -> mem -> locals -> MetricLog -> Prop) -> Prop)
-               (e: string_keyed_map (list Var * list Var * Cmd))(f: string)
+               (e: string_keyed_map (list Var * list Var * Cmd)%type)(f: string)
                (t: trace)(m: mem)(argvals: list word)
                (post: trace -> mem -> list word -> Prop): Prop :=
       exists argnames retnames fbody l,
@@ -157,7 +158,7 @@ Section WithWordAndMem.
       fun '(argnames, retnames, body) => NoDup argnames /\ NoDup retnames.
 
     Definition SrcLang: Lang := {|
-      Program := string_keyed_map (list string * list string * Syntax.cmd);
+      Program := Semantics.env;
       Valid := map.forall_values ExprImp.valid_fun;
       Call := locals_based_call_spec Semantics.exec;
     |}.
@@ -220,7 +221,7 @@ Section WithWordAndMem.
     Lemma flattening_correct: phase_correct SrcLang FlatWithStrVars flatten_functions.
     Proof.
       unfold SrcLang, FlatWithStrVars.
-      split; cbn.
+      split; cbn -[flatten_functions].
       { unfold map.forall_values, ParamsNoDup.
         intros. destruct v as ((argnames & retnames) & body).
         eapply flatten_functions_NoDup; try eassumption.
@@ -434,7 +435,7 @@ Section WithWordAndMem.
     Qed.
 
     Definition composed_compile:
-      string_keyed_map (list string * list string * cmd) ->
+      Semantics.env ->
       result (list Instruction * string_keyed_map Z * Z) :=
       (compose_phases flatten_functions
       (compose_phases (useimmediate_functions is5BitImmediate is12BitImmediate)
@@ -481,8 +482,8 @@ Section WithWordAndMem.
         ExprImp.valid_funs (map.of_list fs).
     Proof.
       unfold valid_funs. induction fs; intros.
-      - simpl in H0. rewrite map.get_empty in H0. discriminate.
-      - destruct a as (name & body). simpl in H0. rewrite map.get_put_dec in H0. fwd.
+      - cbn [map.of_list] in H0. rewrite map.get_empty in H0. discriminate.
+      - destruct a as (name & body). cbn [map.of_list] in H0. rewrite map.get_put_dec in H0. fwd.
         destruct_one_match_hyp.
         + fwd. eapply valid_src_fun_correct. eassumption.
         + eapply IHfs; eassumption.
@@ -501,7 +502,8 @@ Section WithWordAndMem.
         valid_src_funs functions = true ->
         compile functions = Success (instrs, finfo, req_stack_size) ->
         (exists (argnames retnames: list string) (fbody: cmd) l,
-            map.get (map.of_list functions) fname = Some (argnames, retnames, fbody) /\
+            map.get (map.of_list (map := Semantics.env) functions) fname =
+              Some (argnames, retnames, fbody) /\
             map.of_list_zip argnames argvals = Some l /\
             forall mc,
               Semantics.exec (map.of_list functions) fbody t mH l mc
@@ -573,7 +575,7 @@ Section WithWordAndMem.
         valid_src_funs fs = true ->
         NoDup (map fst fs) ->
         compile fs = Success (instrs, finfo, req_stack_size) ->
-        WeakestPrecondition.call fs fname t mH argvals post ->
+        WeakestPrecondition.call (map.of_list fs) fname t mH argvals post ->
         map.get (map.of_list finfo) fname = Some f_rel_pos ->
         req_stack_size <= word.unsigned (word.sub stack_hi stack_lo) / bytes_per_word ->
         word.unsigned (word.sub stack_hi stack_lo) mod bytes_per_word = 0 ->
@@ -594,7 +596,6 @@ Section WithWordAndMem.
       intros.
       let H := hyp WeakestPrecondition.call in rename H into WP.
       eapply WeakestPreconditionProperties.sound_call' in WP.
-      2: { eapply map.all_gets_from_map_of_NoDup_list; assumption. }
       fwd.
       edestruct compiler_correct with (argvals := argvals) (post := post) as (f_rel_pos' & G & C);
         try eassumption.
diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v
index 590fac9f..7b82edff 100644
--- a/compiler/src/compiler/ToplevelLoop.v
+++ b/compiler/src/compiler/ToplevelLoop.v
@@ -221,6 +221,8 @@ Section Pipeline1.
     apply Zmod_0_l.
   Qed.
 
+  Local Arguments map.get : simpl never.
+
   Lemma establish_ll_inv: forall (initial: MetricRiscvMachine),
       initial_conditions initial ->
       ll_inv initial.
diff --git a/compiler/src/compilerExamples/SoftmulCompile.v b/compiler/src/compilerExamples/SoftmulCompile.v
index f583afc3..9b4fb45c 100644
--- a/compiler/src/compilerExamples/SoftmulCompile.v
+++ b/compiler/src/compilerExamples/SoftmulCompile.v
@@ -649,9 +649,9 @@ Section Riscv.
       unfold isXAddr4, isXAddr1. ssplit; eapply In_word_seq; try ZnWords.
   Qed.
 
-  Lemma link_softmul_bedrock2: spec_of_softmul funimplsList.
+  Lemma link_softmul_bedrock2: spec_of_softmul (map.of_list funimplsList).
   Proof.
-    eapply softmul_ok. eapply rpmul.rpmul_ok.
+    eapply softmul_ok. 1: reflexivity. eapply rpmul.rpmul_ok. reflexivity.
   Qed.
 
   Import FunctionalExtensionality PropExtensionality.
diff --git a/end2end/src/end2end/End2EndLightbulb.v b/end2end/src/end2end/End2EndLightbulb.v
index 1bb255cf..7b93641a 100644
--- a/end2end/src/end2end/End2EndLightbulb.v
+++ b/end2end/src/end2end/End2EndLightbulb.v
@@ -76,13 +76,13 @@ Definition loop :=
   ("loop", ([]: list string, []: list string,
            (cmd.call ["err"] "lightbulb_loop" [expr.literal buffer_addr]))).
 
-Definition prog := init :: loop :: lightbulb.function_impls.
+Definition prog := map.putmany_of_list (init :: loop :: nil) lightbulb.function_impls.
 
 (* Before running this command, it might be a good idea to do
    "Print Assumptions lightbulb_insts_unevaluated."
    and to check if there are any axioms which could block the computation. *)
 Definition lightbulb_compiled: list Decode.Instruction * list (string * Z) * Z.
-  let r := eval cbv in (ToplevelLoop.compile_prog MMIO.compile_ext_call ml prog) in
+  let r := eval cbv in (ToplevelLoop.compile_prog MMIO.compile_ext_call ml (map.tuples prog)) in
   lazymatch r with
   | Success ?x => exact x
   end.
@@ -110,7 +110,7 @@ Definition required_stack_space: Z.
 Defined.
 
 Definition compilation_result:
-  ToplevelLoop.compile_prog MMIO.compile_ext_call ml prog =
+  ToplevelLoop.compile_prog MMIO.compile_ext_call ml (map.tuples prog) =
   Success (lightbulb_insts, function_positions, required_stack_space).
 Proof. reflexivity. Qed.
 
@@ -182,7 +182,7 @@ Proof.
   intros *. intro KB.
   specialize Q with (stack_size_in_bytes := stack_size_in_bytes).
   specialize_first Q mem0.
-  specialize_first Q prog.
+  specialize_first Q (map.tuples prog).
   specialize_first Q open_constr:(eq_refl).
   specialize_first Q open_constr:(eq_refl).
   specialize_first Q open_constr:(eq_refl).
@@ -190,7 +190,7 @@ Proof.
   specialize_first Q (Zkeyed_map (KamiWord.word 32)).
   specialize_first Q (Zkeyed_map_ok (KamiWord.word 32)).
   specialize_first Q mem_ok.
-  specialize Q with (13 := KB). (* TODO add bigger numbers to coqutil.Tactics.forward.specialize_first *)
+  specialize Q with (12 := KB). (* TODO add bigger numbers to coqutil.Tactics.forward.specialize_first *)
   (* specialize_first Q KB. *)
   specialize_first Q compilation_result.
 
@@ -216,8 +216,6 @@ Proof.
   }
   eapply Q; clear Q.
   - cbv. intuition discriminate.
-  - clear. cbv.
-    repeat econstructor; intro; repeat match goal with H: In _ _|-_=> destruct H end; discriminate.
   - intros. clear KB mem0. simp.
     unfold SPI.mmio_trace_abstraction_relation in *.
     unfold id in *.
@@ -225,9 +223,14 @@ Proof.
   - reflexivity.
   - (* establish invariant *)
     repeat ProgramLogic.straightline.
-    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _);
-      [|exact (link_lightbulb_init m nil)].
-
+    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _).
+    2: {
+      unfold prog. eapply WP.extend_env_wp_call. 2: exact (link_lightbulb_init m nil).
+      rewrite map.of_list_tuples.
+      intros k f G. unfold map.putmany_of_list, init, loop.
+      rewrite ?map.get_put_dec.
+      repeat destruct_one_match; subst; try discriminate G. assumption.
+    }
     intros ? ? ? ?.
     repeat ProgramLogic.straightline.
     unfold LowerPipeline.mem_available, hl_inv, isReady, goodTrace, goodHlTrace, buffer_addr, ml, End2EndPipeline.ml, code_start, heap_start, heap_pastend, Lift1Prop.ex1 in *; Simp.simp.
@@ -266,9 +269,14 @@ Proof.
     specialize_first P Hp0p0.
     specialize_first P t0.
     specialize_first P Hp0p1.
-    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _);
-      [|exact P]; clear P.
-
+    refine (WeakestPreconditionProperties.Proper_call _ _ _ _ _ _ _ _ _).
+    2: {
+      unfold prog. eapply WP.extend_env_wp_call. 2: exact P.
+      rewrite map.of_list_tuples.
+      intros k f G. unfold map.putmany_of_list, init, loop.
+      rewrite ?map.get_put_dec.
+      repeat destruct_one_match; subst; try discriminate G. assumption.
+    }
     intros ? ? ? ?.
     Simp.simp.
     repeat ProgramLogic.straightline.
diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v
index 428d9766..a6652ba4 100644
--- a/end2end/src/end2end/End2EndPipeline.v
+++ b/end2end/src/end2end/End2EndPipeline.v
@@ -199,8 +199,6 @@ Section Connect.
 
   Definition bedrock2Inv := (fun t m l => forall mc, hl_inv spec t m l mc).
 
-  Let funspecs := WeakestPrecondition.call funimplsList.
-
   Hypothesis goodTrace_implies_related_to_Events: forall (t: list LogItem),
       spec.(goodTrace) t -> exists t': list Event, traces_related t' t.
 
@@ -298,10 +296,10 @@ Section Connect.
     forall init_code loop_body,
     map.get (map.of_list funimplsList) "init"%string = Some ([], [], init_code) ->
     (forall m, LowerPipeline.mem_available ml.(heap_start) ml.(heap_pastend) m ->
-               WeakestPrecondition.cmd funspecs init_code [] m map.empty bedrock2Inv) ->
+               WeakestPrecondition.cmd (map.of_list funimplsList) init_code [] m map.empty bedrock2Inv) ->
     map.get (map.of_list funimplsList) "loop"%string = Some ([], [], loop_body) ->
     (forall t m l, bedrock2Inv t m l ->
-                   WeakestPrecondition.cmd funspecs loop_body t m l bedrock2Inv) ->
+                   WeakestPrecondition.cmd (map.of_list funimplsList) loop_body t m l bedrock2Inv) ->
     (* Assumptions on the compiler level: *)
     forall (instrs: list Instruction) positions (required_stack_space: Z),
     compile_prog compile_ext_call ml funimplsList = Success (instrs, positions, required_stack_space) ->
@@ -371,12 +369,12 @@ Section Connect.
                rewrite heap_start_agree in H;
                rewrite heap_pastend_agree in H
              end.
-             refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _ _); eauto.
+             refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _); eauto.
           -- simpl. clear. intros. unfold bedrock2Inv in *. eauto.
         * exact GetLoop.
         * intros. unfold bedrock2Inv in *.
           eapply ExprImp.weaken_exec.
-          -- refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _ _); eauto.
+          -- refine (WeakestPreconditionProperties.sound_cmd _ _ _ _ _ _ _ _); eauto.
           -- simpl. clear. intros. eauto.
       + assumption.
       + assumption.