make WeakestPrecondition.cmd complete wrt Semantics.exec (#361)

* define a WP.cmd' in terms of exec, might soon replace WP.cmd

and rules for cmd' whose premises are copied from WP.cmd.
This one is "fs everywhere" (ie list of functions everywhere).
The wp_call rule requires a NoDup, which would be cumbersome to
carry around.

* dead simple `call` based on `map.get`

* convert from "fs everywhere" to "env everywhere"

* instead of unfold1_cmd_goal, eapply lemma_corresponding_to_command

In an "env everywhere" setting, where program_logic_goal_for!
adds a (map.get fs fname = Some fimpl) hypothesis.
Surprise #1: There's no case in straightline that handles if-then-else
Surprise #2: unfold1_... tactics are not the only place that depend
on conversion: There also exists a letexists in SPI that turns a
(WP (cmd.cond e _ _) ...) into an (exists v, eval e v /\ ...), and
probably more elsewhere.

* wip "env everywhere" approach

* make WeakestPrecondition.cmd complete wrt exec

by leaving the structurally recursive cases of cmd_body unchanged,
and defining the two non-structurally recursive cases (loop and call)
directly in terms of exec.
This seems to be the only approach that does not break proofs in
bedrock2Examples too badly.

* hardcode env implementation in bedrock2.Semantics,

and update compiler, LiveVerif, end2end

* add back program/Proper_program because it's used by rupicola

* cp Semantics.v MetricSemantics.v

* bedrock2.Semantics is now metrics-free, and metrics are in MetricSemantics

* refinement lemmas for induction over command syntax

* delete WP.v (opaque Module), only LAN9250 needed fixing

* LiveVerif: wp_cmd is exec instead of WeakestPrecondition.cmd

* env doesn't really need to be an Instance, it seems

* fix argument order in refinement

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