update to bedrock2 where Module WP is gone

mit-plv · Aug 6, 2023 · 0c5ee4d · 0c5ee4d
1 parent 87d29e3
commit 0c5ee4d
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 12 deletions.
diff --git a/bedrock2 b/bedrock2
diff --git a/src/Rupicola/Examples/CapitalizeThird/Properties.v b/src/Rupicola/Examples/CapitalizeThird/Properties.v
@@ -297,8 +297,6 @@ Section Proofs.
                      try congruence)]
     end.
 
-  Import WP.
-
   (* TODO: try to use ProgramLogic *)
   Lemma capitalize_String_correct
         (addr : word) (s : Gallina.String) :
@@ -320,8 +318,8 @@ Section Proofs.
              (success = 1 /\ sep (String addr caps) R mem'))).
   Proof.
     cbv zeta. intros.
-    eapply mk_wp_call. 1: eassumption. 1: reflexivity.
-    eapply cmd_sound.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -721,8 +719,8 @@ Section Proofs.
                   R mem'))).
   Proof.
     cbv zeta. intros.
-    eapply mk_wp_call. 1: eassumption. 1: reflexivity.
-    eapply cmd_sound.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].

diff --git a/src/Rupicola/Lib/Compiler.v b/src/Rupicola/Lib/Compiler.v
@@ -385,8 +385,7 @@ Section with_parameters.
         rewrite map.put_idemp in H0; assumption.
       - eapply WeakestPrecondition_weaken, IHcmd1; eauto;
           intros; eapply WeakestPrecondition_weaken, IHcmd2; eauto.
-      - eapply WP.WP_Impl.mk_wp_cmd. eapply WP.WP_Impl.invert_wp_cmd in H.
-        eapply refinement_while. 2: eassumption.
+      - eapply refinement_while. 2: eassumption.
         unfold refinement. intros.
         eapply sound_cmd. eapply IHcmd. eapply complete_cmd. assumption.
     Qed.
@@ -427,7 +426,7 @@ Section with_parameters.
       clear; firstorder eauto using getmany_list_map.
     Qed.
 
-    Import bedrock2.Semantics bedrock2.WP.
+    Import bedrock2.Semantics.
 
     Lemma compile_setup_WeakestPrecondition_call_first {tr mem locals}
           name argnames retvars body args functions post:
@@ -444,8 +443,8 @@ Section with_parameters.
       WeakestPrecondition.call functions name tr mem args post.
     Proof.
       intros.
-      eapply mk_wp_call. 1,2: eassumption.
-      eapply cmd_sound.
+      do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
+      eapply sound_cmd.
       eapply WeakestPrecondition_weaken; try eassumption.
       clear; firstorder eauto using getmany_list_map.
     Qed.
+3 −2		LiveVerif/src/LiveVerif/LiveRules.v
+3 −4		bedrock2/src/bedrock2/Loops.v
+25 −0		bedrock2/src/bedrock2/MetricSemantics.v
+0 −1		bedrock2/src/bedrock2/ProgramLogic.v
+25 −1		bedrock2/src/bedrock2/Semantics.v
+0 −126		bedrock2/src/bedrock2/WP.v
+3 −4		bedrock2/src/bedrock2/WeakestPrecondition.v
+9 −37		bedrock2/src/bedrock2/WeakestPreconditionProperties.v
+9 −0		bedrock2/src/bedrock2Examples/LAN9250.v
+0 −1		compiler/src/compiler/Pipeline.v
+2 −2		end2end/src/end2end/End2EndLightbulb.v