hardcode env implementation in bedrock2.Semantics,

and update compiler, LiveVerif, end2end

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,30 +145,26 @@ 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;
              let kvs := eval unfold List.combine in (List.combine argnames argvalues) in
              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)"

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 *)

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}.
 

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))).

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.

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,18 +95,17 @@ 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.
     intros. eapply mk_wp_cmd. intros. eapply invert_wp_cmd in H0.
     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.

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.*)

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.

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.

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.

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).

compiler/src/compiler/ExprImpEventLoopSpec.v

@@ -2,14 +2,14 @@ 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.
 
 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.