From 63445f8caeaff791b048668992679d8664b81c77 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Sun, 6 Aug 2023 18:34:13 -0400
Subject: [PATCH] wip updating to bedrock2 where WeakestPrecondition.cmd is
 exec

---
 bedrock2                    |  2 +-
 src/Rupicola/Lib/Compiler.v | 18 ++++++++----------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/bedrock2 b/bedrock2
index 6faf7a0e..5062f79b 160000
--- a/bedrock2
+++ b/bedrock2
@@ -1 +1 @@
-Subproject commit 6faf7a0e064aab66feb1e32e44e5d2a901adc01e
+Subproject commit 5062f79b2200ef49b7d38cf08c67c77daa752e67
diff --git a/src/Rupicola/Lib/Compiler.v b/src/Rupicola/Lib/Compiler.v
index c7c21af7..fb4e8382 100644
--- a/src/Rupicola/Lib/Compiler.v
+++ b/src/Rupicola/Lib/Compiler.v
@@ -112,7 +112,7 @@ Section CompilerBasics.
          Functions := functions }>
       cmd.seq c0 c1
       <{ pred1 }>.
-  Proof. intros; cbn; eapply WeakestPrecondition_weaken; eauto. Qed.
+  Proof. intros; econstructor; eauto. Qed.
 
   (* FIXME find a way to automate the application of these copy lemmas *)
   (* N.B. should only be added to compilation tactics that solve their subgoals,
@@ -318,8 +318,8 @@ Section with_parameters.
           cmd tr mem locals post.
     Proof.
       unfold program. split; intros.
-      - eapply complete_cmd. eapply sound_cmd in H. eapply noskips_correct_bw. assumption.
-      - eapply complete_cmd. eapply sound_cmd in H. eapply noskips_correct_fw. assumption.
+      - eapply noskips_correct_bw. assumption.
+      - eapply noskips_correct_fw. assumption.
     Qed.
 
     Definition compile_setup_remove_skips := noskips_correct.
@@ -367,6 +367,7 @@ Section with_parameters.
         WeakestPrecondition.program functions
           (noreassign cmd) tr mem locals post.
     Proof.
+      unfold program.
       all: induction cmd;
         repeat match goal with
                | _ => apply IHcmd
@@ -376,18 +377,16 @@ Section with_parameters.
                  let h := fresh in intros h; specialize (H _ _ _ _ h)
                | [ H: exists _, _ |- _ ] => destruct H
                | [  |- exists _, _ ] => eexists
-               | [ H: context[WeakestPrecondition.cmd] |- context[WeakestPrecondition.cmd] ] => solve [eapply H; eauto]
+               | [ H: context[Semantics.exec] |- context[Semantics.exec] ] => solve [inversion H; econstructor; eauto]
                | _ => unfold WeakestPrecondition.program in * || cbn || intros ? || eauto
                end.
 
       - destruct (is_var_expr_spec rhs lhs); simpl in *; subst; eauto; [].
-        destruct H as (xx & Hxx & ->).
-        rewrite map.put_idemp in H0; assumption.
-      - eapply WeakestPrecondition_weaken, IHcmd1; eauto;
-          intros; eapply WeakestPrecondition_weaken, IHcmd2; eauto.
+        inversion H; subst. inversion H2. rewrite map.put_idemp in *; try assumption.
+        econstructor. assumption.
       - eapply refinement_while. 2: eassumption.
         unfold refinement. intros.
-        eapply sound_cmd. eapply IHcmd. eapply complete_cmd. assumption.
+        eapply IHcmd. assumption.
     Qed.
 
     Definition compile_setup_remove_reassigns := noreassign_correct.
@@ -444,7 +443,6 @@ Section with_parameters.
     Proof.
       intros.
       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.