update to rupicola/bedrock2 where Module WP is gone

mit-plv · Aug 6, 2023 · 1eb8db0 · 1eb8db0
1 parent 783c095
commit 1eb8db0
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 3 deletions.
diff --git a/rupicola b/rupicola
diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -105,7 +105,7 @@ Proof.
   assert (spec_of_montladder (map.of_list funcs)). {
     unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
     intros.
-    eapply WP.extend_env_wp_call.
+    eapply Semantics.extend_env_call.
     2: { eapply link_montladder. eassumption. }
     clear. unfold funcs.
     (* TODO this could be more computational *)

diff --git a/src/Bedrock/Field/Synthesis/Examples/redc.v b/src/Bedrock/Field/Synthesis/Examples/redc.v
@@ -60,7 +60,7 @@ Section WithParameters.
 
   (* redc_step ought to take in small arrays B and S, and value a, and output an array S' *)
   (* S' should be small, and should eval to the same as (a * B + S) * ri modulo the prime *)
- 
+
   Instance spec_of_redc_step : spec_of "redc_step" :=
     fnspec! "redc_step" a Bstart Sstart len / B (bval: Z) S (sval: Z) R,
       { requires t m :=
@@ -159,6 +159,15 @@ Section WithParameters.
   Proof.
     Admitted.
 
+  Local Ltac no_call :=
+    lazymatch goal with
+    | |- Semantics.call _ _ _ _ _ _ => fail
+    | |- _ => idtac
+    end.
+
+  Local Ltac original_eexists := eexists.
+  Local Tactic Notation "eexists" := no_call; original_eexists.
+
  Theorem redc_alt_ok :
       program_logic_goal_for_function! redc_alt.
  Proof.