Late choice refines early choice

F_mu_ref_conc/examples/lateearlychoice.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth.
+From iris.base_logic Require Import lib.auth.
+From iris_logrel.F_mu_ref_conc Require Export examples.lock.
+From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary relational_properties.
+From iris.program_logic Require Import adequacy.
+
+From iris_logrel.F_mu_ref_conc Require Import hax.
+
+Notation "'let:' x := e1 'in' e2" := (Let x%bind e1%E e2%E)
+  (at level 102, x at level 1, e1, e2 at level 200,
+   format "'[' '[hv' 'let:'  x  :=  '[' e1 ']'  'in'  ']' '/' e2 ']'") : expr_scope.
+Notation "e $! v" := (lamsubst e%E v%V) (at level 80) : expr_scope.
+
+Definition rand : val := λ: <>,
+  let: "y" := (ref (#♭ false))
+  in Fork ("y" <- #♭ true);;
+     !"y".
+Definition lateChoice : val := λ: "x",
+  "x" <- #n 0;; rand #().
+Definition earlyChoice : val := λ: "x",
+  let: "r" := rand #() in "x" <- #n 0;; "r".
+
+Section Refinement.
+  Context `{heapIG Σ, cfgSG Σ}.
+
+  Definition choiceN : namespace := nroot .@ "choice".
+
+  Definition choice_inv y y' : iProp Σ :=
+    (∃ f, y ↦ᵢ (#♭v f) ∗ y' ↦ₛ (#♭v f))%I.
+
+  Lemma wp_rand :
+    (WP rand #() {{ v, ⌜v = #♭v true⌝ ∨ ⌜v = #♭v false⌝}})%I.
+  Proof.
+    iStartProof.
+    unfold rand. unlock.
+    iApply wp_rec; eauto. solve_closed. iNext. simpl.
+    wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy".
+    iMod (inv_alloc choiceN _ (y ↦ᵢ (#♭v false) ∨ y ↦ᵢ (#♭v true))%I with "[Hy]") as "#Hinv"; eauto.
+    iApply wp_rec; eauto. solve_closed. iNext. simpl.
+    wp_bind (Fork _). iApply wp_fork. iNext.
+    iSplitL.
+    - iModIntro. iApply wp_rec; eauto. solve_closed. iNext; simpl.
+      iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_load with "Hy"); eauto; iNext;
+        iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
+    - iInv choiceN as "[Hy | Hy]" "Hcl"; iApply (wp_store with "Hy"); eauto; iNext;
+        iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
+  Qed.
+
+  Lemma rand_l Γ E1 K ρ t τ :
+    ↑choiceN ⊆ E1 →
+    spec_ctx ρ -∗ (∀ b, {E1,E1;Γ} ⊨ fill K (#♭ b) ≤log≤ t : τ)
+    -∗ {E1,E1;Γ} ⊨ fill K (rand #())%E ≤log≤ t : τ.
+  Proof.
+    iIntros (?) "#Hs Hlog".
+    unfold rand at 1. unlock. simpl.
+    iApply (bin_log_related_rec_l Γ E1 K BAnon BAnon _ #()%E); first done.
+    iNext. simpl.
+    rel_bind_l (Alloc _).
+    iApply bin_log_related_alloc_l'; first eauto. iIntros (y) "Hy". simpl.
+    iApply (bin_log_related_rec_l _ _ K); first eauto. iNext. simpl.
+    iMod (inv_alloc choiceN _ (∃ b, y ↦ᵢ (#♭v b))%I with "[Hy]") as "#Hinv".
+    { iNext. eauto. }
+    rel_bind_l (Fork _).
+    iApply bin_log_related_fork_l. iModIntro.
+    iSplitR.
+    - iNext.
+      iInv choiceN as (b) "Hy" "Hcl".
+      iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
+      iMod ("Hcl" with "[Hy]").
+      { iNext. iExists true. by iFrame. }
+      done.
+    - simpl.
+      iApply (bin_log_related_rec_l _ _ K); first eauto. iNext. simpl.
+      iApply (bin_log_related_load_l _ _ _ K).
+      iInv choiceN as (b) "Hy" "Hcl". iModIntro.
+      iExists (#♭v b). iFrame. iIntros "Hy".
+      iMod ("Hcl" with "[Hy]").
+      { iNext. iExists b. iFrame. }
+      done. 
+  Qed.
+ 
+  Lemma lateChoice_l Γ x v ρ t :
+    spec_ctx ρ -∗ x ↦ᵢ v -∗
+    (x ↦ᵢ (#nv 0) -∗ ∀ b, Γ ⊨ (#♭ b) ≤log≤ t : TBool) -∗
+    Γ ⊨ lateChoice #x ≤log≤ t : TBool.
+  Proof.  
+    iIntros "#Hs Hx Hlog".
+    unfold lateChoice. unlock.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rewrite !Closed_subst_id.
+    rel_bind_l (#x <- _)%E.
+    iApply (bin_log_related_store_l' with "Hx"); eauto. iIntros "Hx".
+    simpl.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+    
+    unfold rand at 1. unlock.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+    rel_bind_l (Alloc _).
+    iApply bin_log_related_alloc_l'; eauto. iIntros (y) "Hy". simpl.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+    
+    iMod (inv_alloc choiceN _ (∃ b, y ↦ᵢ (#♭v b))%I with "[Hy]") as "#Hinv".
+    { iNext. eauto. }
+    rel_bind_l (Fork _).
+    iApply bin_log_related_fork_l. iModIntro.
+    iSplitR.
+    - iNext.
+      iInv choiceN as (b) "Hy" "Hcl".
+      iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
+      iMod ("Hcl" with "[Hy]").
+      { iNext. iExists true. by iFrame. }
+      done.
+    - simpl.
+      iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+      iApply (bin_log_related_load_l _ _ _ []).
+      iInv choiceN as (b) "Hy" "Hcl". iModIntro.
+      iExists (#♭v b). iFrame. iIntros "Hy".
+      iMod ("Hcl" with "[Hy]").
+      { iNext. iExists b. iFrame. }
+      simpl. iApply ("Hlog" with "Hx").
+  Qed.
+  
+  Lemma prerefinement Γ x x' n ρ :
+    (spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗
+      Γ ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool)%I.
+  Proof.
+    iIntros "#Hspec Hx Hx'".
+    unfold lateChoice, earlyChoice. unlock.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rewrite !Closed_subst_id.
+    iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
+
+    rel_bind_l (#x <- _)%E.
+    iApply (bin_log_related_store_l' with "Hx"); eauto. iIntros "Hx".
+    simpl.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+
+    unfold rand at 1. unlock.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+    rel_bind_l (Alloc _).
+    iApply bin_log_related_alloc_l'; eauto. iIntros (y) "Hy". simpl.
+    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+
+    rel_bind_r (rand #())%E. unfold rand. unlock.
+    iApply (bin_log_related_rec_r _ _); eauto. simpl.
+    rel_bind_r (Alloc _).
+    iApply bin_log_related_alloc_r; eauto. iIntros (y') "Hy'". simpl.
+    rel_bind_r (App _ #y')%E.
+    iApply (bin_log_related_rec_r _ _); eauto. simpl.
+
+    iAssert (choice_inv y y') with "[Hy Hy']" as "Hinv".
+    { iExists false. by iFrame. }
+    iMod (inv_alloc choiceN with "[Hinv]") as "#Hinv".
+    { iNext. iApply "Hinv". }
+    rel_bind_r (Fork _).
+    iApply bin_log_related_fork_r; eauto. iIntros (i) "Hi".
+
+    rel_bind_l (Fork _).
+    iApply bin_log_related_fork_l. iModIntro.
+    iSplitL "Hi".
+    - iNext.
+      iInv choiceN as (f) "[Hy Hy']" "Hcl".
+      iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
+      tp_store i.
+      iMod ("Hcl" with "[Hy Hy']").
+      { iNext. iExists true. by iFrame. }
+      done.
+    - simpl.
+      iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
+      rel_bind_r (App _ #())%E.
+      iApply bin_log_related_rec_r; eauto. simpl.
+      rel_bind_r (Load #y')%E.
+      iApply (bin_log_related_load_l _ _ _ []).
+      iInv choiceN as (f) "[Hy >Hy']" "Hcl". iModIntro.
+      iExists (#♭v f). iFrame. iIntros "Hy".
+      iApply (bin_log_related_load_r with "Hy'"). { solve_ndisj. }
+      iIntros "Hy'". 
+      iMod ("Hcl" with "[Hy Hy']").
+      { iNext. iExists f. iFrame. }
+      simpl.
+
+      iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl.
+      rel_bind_r (Store _ _).
+      iApply (bin_log_related_store_r with "Hx'"); eauto. iIntros "Hx'". simpl.
+      iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl.
+      iApply bin_log_related_val; eauto.
+      { iIntros (Δ). iModIntro. simpl. eauto. }
+  Qed.
+
+  Lemma refinement Γ ρ :
+    (spec_ctx ρ -∗
+      Γ ⊨ lateChoice ≤log≤ earlyChoice : TArrow (Tref TNat) TBool)%I.
+  Proof.
+    iIntros "#Hspec".
+    unfold lateChoice in *. unfold earlyChoice in *. unlock.
+    iApply bin_log_related_arrow.
+    iAlways. iIntros (Δ (l,l')) "Hxx'". simpl.
+    iDestruct "Hxx'" as ([x x']) "[% #Hxx']". inversion H1; subst. simpl.    
+    replace (λ: "x", "x" <- Nat 0 ;; rand #())%E
+      with (of_val lateChoice); last first.
+    { unfold lateChoice. unlock. reflexivity. }
+    replace (λ: "x", (λ: "r", "x" <- Nat 0 ;; "r") (rand #()))%E
+      with (of_val earlyChoice); last first.
+    { unfold earlyChoice. unlock. reflexivity. }
+    Abort.
+    (* iApply prerefinement; eauto. *)
+    
+End Refinement.

_CoqProject

@@ -22,6 +22,7 @@ F_mu_ref_conc/tactics.v
 F_mu_ref_conc/notation.v
 F_mu_ref_conc/examples/lock.v
 F_mu_ref_conc/examples/counter.v
+F_mu_ref_conc/examples/lateearlychoice.v
 #F_mu_ref_conc/examples/stack/stack_rules.v
 #F_mu_ref_conc/examples/stack/CG_stack.v
 #F_mu_ref_conc/examples/stack/FG_stack.v