Wp is really exec

src/Rupicola/Examples/Arithmetic.v

@@ -6,19 +6,17 @@ From bedrock2 Require BasicC32Semantics BasicC64Semantics.
 Module Type FNV1A_params.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Parameter prime : word.
   Parameter offset : word.
 End FNV1A_params.
 
 Module FNV1A (Import P: FNV1A_params).
 #[global]
-  Existing Instances BW word locals mem env ext_spec wordok mapok localsok envok ext_spec_ok.
+  Existing Instances BW word locals mem ext_spec wordok mapok localsok ext_spec_ok.
   Import SizedListArrayCompiler.
 
   Definition update (hash data : word) :=

src/Rupicola/Examples/Arrays.v

@@ -7,11 +7,9 @@ Require Import coqutil.Word.LittleEndianList.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Section GetPut.

src/Rupicola/Examples/CMove/CMove.v

@@ -8,22 +8,20 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section __.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Section Gallina.
-    
+
     Definition all_1s : word := word.of_Z (-1).
 
     Definition is_mask mask : Prop :=
       mask = all_1s \/ mask = word.of_Z 0.
 
     Definition mask_of_bool (b : bool) :=
       if b then all_1s else word.of_Z 0.
-      
+
     (*idea: if b then true_val else false_val *)
     Definition select_word (mask : word) true_val false_val :=
       let/n nmask := (word.sub (word.of_Z (-1)) mask) in
@@ -49,11 +47,11 @@ Section __.
       let/n c2 := put r in
       (c1,c2).
 
-    
+
     Instance HasDefault_word : HasDefault word :=
       word.of_Z 0.
 
-    Definition cmove_array mask len 
+    Definition cmove_array mask len
                (a1: ListArray.t word.rep)
                (a2: ListArray.t word.rep) :=
       let/n from := word.of_Z 0 in
@@ -91,14 +89,14 @@ Section __.
       (a1, a2).
   End Gallina.
 
-  
+
   Lemma z_lt_width : 0 <= width.
   Proof.
     destruct width_cases; lia.
   Qed.
-
 
-
+
+
   Lemma all_1s_and : forall x, word.and all_1s x = x.
   Proof.
     intros.
@@ -119,7 +117,7 @@ Section __.
   Proof.
     rewrite <- (word.of_Z_signed (word.not all_1s)).
     rewrite word.signed_not.
-    unfold all_1s.    
+    unfold all_1s.
     rewrite word.signed_of_Z.
     rewrite !word.swrap_inrange.
     change (-1) with (-(1)).
@@ -132,7 +130,7 @@ Section __.
       destruct width_cases as [H|H]; rewrite !H; lia.
       destruct width_cases as [H|H]; rewrite !H; lia.
     }
-  Qed.    
+  Qed.
 
   Lemma zero_and (x : word)
     : word.and (word.of_Z 0) x = word.of_Z 0.
@@ -143,7 +141,7 @@ Section __.
     reflexivity.
   Qed.
 
-  
+
   Lemma zero_or (x : word)
     : word.or (word.of_Z 0) x = x.
   Proof.
@@ -163,7 +161,7 @@ Section __.
     rewrite word.morph_or.
     reflexivity.
   Qed.
-    
+
   Lemma cmove_word_is_conditional mask c1 c2
     : is_mask mask ->
       cmove_word mask c1 c2 = if word.eqb mask (word.of_Z 0) then c2 else c1.
@@ -246,7 +244,7 @@ Section __.
         tr' = tr /\
         (cell_value ptr1 (cmove_word mask c1 c2)
          * cell_value ptr2 c2 * R)%sep mem' }.
-  
+
   Derive cmove_word_br2fn SuchThat
          (defn! "cmove_word" ("mask", "c1", "c2") { cmove_word_br2fn },
           implements cmove_word)
@@ -265,7 +263,7 @@ Section __.
         let (c1',c2') := (cswap_word mask c1 c2) in
         (cell_value ptr1 c1'
          * cell_value ptr2 c2' * R)%sep mem' }.
-  
+
   Derive cswap_word_br2fn SuchThat
          (defn! "cswap_word" ("mask", "c1", "c2") { cswap_word_br2fn },
           implements cswap_word)
@@ -275,7 +273,7 @@ Section __.
   Qed.
 
 
-  
+
   Instance spec_of_cmove_array : spec_of "cmove_array" :=
     fnspec! "cmove_array" mask len ptr1 ptr2 / n c1 c2 R,
     (*TODO: if b then bw should be all 1s*)

src/Rupicola/Examples/CRC32/CRC32.v

@@ -12,11 +12,9 @@ Require Import
 Section __.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition crc_table : list word :=

src/Rupicola/Examples/CapitalizeThird/Properties.v

@@ -15,7 +15,7 @@ Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Z.PushPullMod.
 Require Import coqutil.Tactics.Tactics.
 Require Import Rupicola.Examples.CapitalizeThird.CapitalizeThird.
-Require bedrock2.WeakestPrecondition.
+Require bedrock2.WeakestPrecondition bedrock2.Loops.
 Require bedrock2.Semantics.
 Require Import bedrock2.BasicC64Semantics.
 From coqutil.Tactics Require Import destr.
@@ -174,7 +174,7 @@ Ltac listsimplify :=
          end.
 
 Section Proofs.
-  Context (functions' : list (string * func))
+  Context (functions' : Semantics.env)
           (toupper_body : Byte.byte -> Byte.byte).
 
   Local Definition byte_to_word : Byte.byte -> word :=
@@ -303,11 +303,11 @@ Section Proofs.
     forall tr mem R,
       sep (String addr s) R mem ->
       len s = length (chars s) ->
-      let functions := (("capitalize_String",capitalize_String) :: functions') in
+      map.get functions' "capitalize_String" = Some capitalize_String ->
       let caps :=
           Gallina.capitalize_String (toupper:=toupper_body) s in
       WeakestPrecondition.call
-        functions "capitalize_String" tr mem [addr]
+        functions' "capitalize_String" tr mem [addr]
         (fun tr' mem' rets =>
            let success := word.unsigned (hd (word.of_Z 0) rets) in
            tr = tr' /\
@@ -318,18 +318,8 @@ Section Proofs.
              (success = 1 /\ sep (String addr caps) R mem'))).
   Proof.
     cbv zeta. intros.
-
-    (* finding the function to call *)
-    cbn [WeakestPrecondition.call
-           WeakestPrecondition.call_body
-           capitalize_String fst].
-    match goal with |- if String.eqb ?x ?x then _ else _ =>
-                    destr (String.eqb x x) end;
-      [ | congruence ].
-
-    (* load arguments as initial local variables *)
-    cbn [WeakestPrecondition.func].
-    eexists; split; [ reflexivity | ].
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -358,7 +348,8 @@ Section Proofs.
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
     match goal with |- dlet.dlet ?locals _ =>
                     cbv [dlet.dlet];
-                      exists nat, lt, (loop_invariant s tr locals addr R)
+                    eapply Loops.wp_while;
+                    exists nat, lt, (loop_invariant s tr locals addr R)
     end.
     split; [ exact lt_wf | ].
     cbv [loop_invariant]; split.
@@ -664,7 +655,9 @@ Section Proofs.
 
       (* ret = 1 *)
       eexists; split; [ solve [constructor] | ].
-      eexists; split; [ rewrite map.get_put_same; reflexivity | ].
+      eexists; split.
+      { cbn [map.getmany_of_list List.option_all List.map].
+        rewrite map.get_put_same; reflexivity. }
       cbn [WeakestPrecondition.list_map WeakestPrecondition.list_map_body].
 
       (* take care of easy postconditions *)
@@ -706,12 +699,12 @@ Section Proofs.
       Forall (fun s => len s = length (chars s)) strings ->
       (* there are at least 3 strings *)
       (3 <= length strings)%nat ->
-      let functions :=
-          (pair "capitalize_3rd" capitalize_3rd :: pair "capitalize_String" capitalize_String :: functions') in
+      map.get functions' "capitalize_3rd" = Some capitalize_3rd ->
+      map.get functions' "capitalize_String" = Some capitalize_String ->
       let caps :=
           Gallina.capitalize_3rd (toupper:=toupper_body) strings in
       WeakestPrecondition.call
-        functions "capitalize_3rd" tr mem [inp]
+        functions' "capitalize_3rd" tr mem [inp]
         (fun tr' mem' rets =>
            let success := word.unsigned (hd (word.of_Z 0) rets) in
            tr = tr' /\
@@ -726,18 +719,8 @@ Section Proofs.
                   R mem'))).
   Proof.
     cbv zeta. intros.
-
-    (* finding the function to call *)
-    cbn [WeakestPrecondition.call].
-    cbn [WeakestPrecondition.call_body
-           capitalize_3rd fst].
-    match goal with |- if String.eqb ?x ?x then _ else _ =>
-                    destr (String.eqb x x) end;
-      [ | congruence ].
-
-    (* load arguments as initial local variables *)
-    cbn [WeakestPrecondition.func].
-    eexists; split; [ reflexivity | ].
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -783,6 +766,7 @@ Section Proofs.
     eapply Proper_call.
     2:{
       apply capitalize_String_correct.
+      3: eassumption.
       { (* identify string that matches argument *)
         match goal with
           H : sep _ _ _ |- _ =>
@@ -811,9 +795,9 @@ Section Proofs.
           destruct x as [|? x]; [|cbn [length] in H; congruence]
     end.
     eexists; split; [ reflexivity | ].
-    eexists; split;
-      [ rewrite ?map.get_put_diff, map.get_put_same by congruence;
-        reflexivity | ].
+    eexists; split.
+    { cbn [map.getmany_of_list List.option_all List.map].
+      rewrite map.get_put_same; reflexivity. }
 
     (* prove postcondition *)
     repeat (split; [ reflexivity | ]).

src/Rupicola/Examples/Cells/Cells.v

@@ -4,11 +4,9 @@ Record  cell {width: Z} {BW: Bitwidth width} {word: word.word width} := { data :
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Local Notation cell := (@cell width BW word).
 

src/Rupicola/Examples/Cells/Incr.v

@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition incr_gallina (c: cell) :=

src/Rupicola/Examples/Cells/IndirectAdd.v

@@ -5,11 +5,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {wordok : word.ok word} {mapok : map.ok mem}.
   Context {localsok : map.ok locals}.
-  Context {envok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
   Local Notation cell := (@cell width BW word).
 

src/Rupicola/Examples/Cells/Swap.v

@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.Cells.Cells.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition swap_gallina (c1 c2: cell) :=

src/Rupicola/Examples/Conditionals.v

@@ -3,11 +3,9 @@ Require Import Rupicola.Lib.Api.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Implicit Type R : mem -> Prop.

src/Rupicola/Examples/DownTo.v

@@ -22,11 +22,9 @@ Section Compilation.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width}.
   Context {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Instance spec_of_popcount : spec_of "popcount" :=

src/Rupicola/Examples/Expr.v

@@ -3,11 +3,9 @@ Require Import Rupicola.Lib.Api.
 Section with_parameters.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition example (x: word) (y: word) :=

src/Rupicola/Examples/IO/Echo.v

@@ -4,11 +4,9 @@ Require Import Rupicola.Examples.IO.IO.
 Section Echo.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
   Context {locals: map.map String.string word}.
-  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
   Context {ext_spec: bedrock2.Semantics.ExtSpec}.
   Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
   Context {locals_ok : map.ok locals}.
-  Context {env_ok : map.ok env}.
   Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
 
   Definition readw_trace (w: word) : trace_entry :=