update to a rupicola/bedrock2 where wp is complete wrt exec

README.md

@@ -20,10 +20,9 @@ Building
 [pkg.go-shield]: https://pkg.go.dev/badge/github.com/mit-plv/fiat-crypto/fiat-go.svg
 [pkg.go-link]: https://pkg.go.dev/github.com/mit-plv/fiat-crypto/fiat-go
 
-This repository requires [Coq](https://coq.inria.fr/) [8.15](https://github.com/coq/coq/releases/tag/V8.15.0) or later.
+This repository requires [Coq](https://coq.inria.fr/) [8.16](https://github.com/coq/coq/releases/tag/V8.16.0) or later.
 Note that if you install Coq from Ubuntu aptitude packages, you need `libcoq-ocaml-dev` in addition to `coq`.
 Note that in some cases (such as installing Coq via homebrew on Mac), you may also need to install `ocaml-findlib` (for `ocamlfind`).
-If you want to build the bedrock2 code, you need [Coq 8.15](https://github.com/coq/coq/releases/tag/V8.15.0) or later (otherwise this code will be skipped automatically; you can skip this code on newer versions of Coq by passing `SKIP_BEDROCK2=1` to `make`).
 The extracted OCaml code for the standalone binaries requires [OCaml](https://ocaml.org/) [4.08](https://ocaml.org/p/ocaml/4.08.0) or later.
 We suggest downloading [the latest version of Coq](https://github.com/coq/coq/wiki#coq-installation).
 Generation of JSON code via the Makefile also requires `jq`.

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,15 +100,18 @@ 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;
     fe1305_square;
     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.
 *)

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.