From eb9858daa0582fc4fd2a7bbda8aa7088833d5001 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 22 Mar 2019 11:49:19 +0100
Subject: [PATCH] Initial prophecy variables support.

- Add rules for prophecy variables for the RHS
  (basically no-ops).
- Prove the late/early choice refinement.
---
 _CoqProject                 |  1 +
 theories/logic/rules.v      | 32 +++++++++++++++++++++++++++++
 theories/logic/spec_rules.v | 41 +++++++++++++++++++++++++++++++++++++
 3 files changed, 74 insertions(+)

diff --git a/_CoqProject b/_CoqProject
index 469934c..5d5fbca 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -42,3 +42,4 @@ theories/examples/stack/CG_stack.v
 theories/examples/stack/FG_stack.v
 theories/examples/stack/refinement.v
 theories/examples/various.v
+theories/examples/lateearlychoice.v
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 44bfb80..6136170 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -109,6 +109,38 @@ Section rules.
     by iApply "Hlog".
   Qed.
 
+  Lemma refines_newproph_r E K t A
+    (Hmasked : nclose specN ⊆ E) :
+    (∀ (p : proph_id), REL t << fill K (of_val #p) @ E : A)%I
+    -∗ REL t << fill K NewProph @ E : A.
+  Proof.
+    iIntros "Hlog".
+    pose (Φ := (fun w => ∃ (p : proph_id), ⌜w = (# p)⌝ : iProp Σ)%I).
+    iApply (refines_step_r Φ); simpl; auto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      iMod (step_newproph with "[$Hs $Hj]") as (p) "Hj". done.
+      iModIntro. iExists _. iFrame. iExists _. iFrame. eauto. }
+    iIntros (v') "He'". iDestruct "He'" as (p) "%". subst.
+    by iApply "Hlog".
+  Qed.
+
+  Lemma refines_resolveproph_r E K t (p : proph_id) w A
+    (Hmasked : nclose specN ⊆ E) :
+    (REL t << fill K (of_val #()) @ E : A)%I
+    -∗ REL t << fill K (ResolveProph #p (of_val w)) @ E : A.
+  Proof.
+    iIntros "Hlog".
+    pose (Φ := (fun w => ⌜w = #()⌝ : iProp Σ)%I).
+    iApply (refines_step_r Φ); simpl; auto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      iMod (step_resolveproph with "[$Hs $Hj]") as "Hj". done.
+      iModIntro. iExists _. iFrame. eauto. }
+    iIntros (v') "He'". iDestruct "He'" as %->.
+    by iApply "Hlog".
+  Qed.
+
   Lemma refines_alloc_r E K e v t A
     (Hmasked : nclose specN ⊆ E) :
     IntoVal e v →
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 34df826..dc3d786 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -95,6 +95,47 @@ Section rules.
       { apply list_lookup_insert. apply lookup_lt_is_Some; eauto. }
   Qed.
 
+  (** Prophecy variables (at this point those are just noops) *)
+  Lemma step_newproph E ρ j K :
+    nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K NewProph ={E}=∗
+    ∃ (p : proph_id), j ⤇ fill K #p.
+  Proof.
+    iIntros (?) "[#Hinv Hj]".
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iInv specN as (tp σ) ">[Hown %]" "Hclose".
+    iDestruct (own_valid_2 with "Hown Hj")
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+    destruct (exist_fresh (used_proph_id σ)) as [p Hp].
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+    { by eapply auth_update, prod_local_update_1,
+         singleton_local_update, (exclusive_local_update _ (Excl (fill K #p))). }
+    iExists p. iFrame. iApply "Hclose". iNext.
+    iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪) σ).
+    rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+  Qed.
+
+  Lemma step_resolveproph E ρ j K (p : proph_id) w :
+    nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (ResolveProph #p (of_val w)) ={E}=∗
+    j ⤇ fill K #().
+  Proof.
+    iIntros (?) "[#Hinv Hj]".
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iInv specN as (tp σ) ">[Hown %]" "Hclose".
+    iDestruct (own_valid_2 with "Hown Hj")
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+    { by eapply auth_update, prod_local_update_1,
+         singleton_local_update, (exclusive_local_update _ (Excl (fill K #()))). }
+    iFrame. iApply "Hclose". iNext.
+    iExists (<[j:=fill K #()]> tp), σ.
+    rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    eapply rtc_r, step_insert_no_fork; eauto.
+    eapply (ResolveProphS #p _ (of_val w)); eauto.
+  Qed.
+
   (** Alloc, load, and store *)
   Lemma step_alloc E ρ j K e v :
     IntoVal e v →
-- 
GitLab