From 20c479dda38f3e34430187268151c73d33077665 Mon Sep 17 00:00:00 2001
From: Marianna Rapoport <mrapoport@uwaterloo.ca>
Date: Wed, 18 Jul 2018 13:58:38 +0200
Subject: [PATCH] Adding support for prophecy variables to heap_lang
---
_CoqProject | 1 +
theories/heap_lang/adequacy.v | 23 +++--
theories/heap_lang/lang.v | 81 ++++++++++-----
theories/heap_lang/lifting.v | 123 +++++++++++++++++-----
theories/heap_lang/proph_map.v | 183 +++++++++++++++++++++++++++++++++
5 files changed, 346 insertions(+), 65 deletions(-)
create mode 100644 theories/heap_lang/proph_map.v
diff --git a/_CoqProject b/_CoqProject
index e85ee72a6..610855d37 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,6 +87,7 @@ theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
+theories/heap_lang/proph_map.v
theories/heap_lang/prophecy.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index d477c462f..486186e68 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,24 +1,27 @@
From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation proph_map.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Class heapPreG Σ := HeapPreG {
- heap_preG_iris :> invPreG Σ;
- heap_preG_heap :> gen_heapPreG loc val Σ
+Class heap_prophPreG Σ := HeapProphPreG {
+ heap_proph_preG_iris :> invPreG Σ;
+ heap_proph_preG_heap :> gen_heapPreG loc val Σ;
+ heap_proph_preG_proph :> proph_mapPreG proph val Σ
}.
-Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
-Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph val].
+Instance subG_heapPreG {Σ} : subG heapΣ Σ → heap_prophPreG Σ.
Proof. solve_inG. Qed.
-Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
+Definition heap_adequacy Σ `{heap_prophPreG Σ} s e σ φ :
(∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌠}}%I) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
- iMod (gen_heap_init σ) as (?) "Hh".
- iModIntro. iExists (fun σ _ => gen_heap_ctx σ). iFrame "Hh".
- iApply (Hwp (HeapG _ _ _)).
+ iMod (gen_heap_init σ.1) as (?) "Hh".
+ iMod (proph_map_init κs σ.2) as (?) "Hp".
+ iModIntro.
+ iExists (fun σ κs => (gen_heap_ctx σ.1 ∗ proph_map_ctx κs σ.2)%I). iFrame.
+ iApply (Hwp (HeapG _ _ _ _)).
Qed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index a5ae44a3b..2630b441e 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -76,7 +76,10 @@ Inductive expr :=
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
- | FAA (e1 : expr) (e2 : expr).
+ | FAA (e1 : expr) (e2 : expr)
+ (* Prophecy *)
+ | NewProph
+ | ResolveProph (e1 : expr) (e2 : expr).
Bind Scope expr_scope with expr.
@@ -84,10 +87,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x ∈ X)
| Rec f x e => is_closed (f :b: x :b: X) e
- | Lit _ => true
+ | Lit _ | NewProph => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
is_closed X e
- | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
+ | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -108,7 +111,7 @@ Inductive val :=
Bind Scope val_scope with val.
-Definition observation := Empty val.
+Definition observation : Set := proph * val.
Fixpoint of_val (v : val) : expr :=
match v with
@@ -163,7 +166,7 @@ Definition val_is_unboxed (v : val) : Prop :=
end.
(** The state: heaps of vals. *)
-Definition state := gmap loc val.
+Definition state : Type := gmap loc val * gset proph.
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -230,12 +233,12 @@ Instance expr_countable : Countable expr.
Proof.
set (enc := fix go e :=
match e with
- | Var x => GenLeaf (inl (inl x))
- | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+ | Var x => GenLeaf (Some (inl (inl x)))
+ | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
| App e1 e2 => GenNode 1 [go e1; go e2]
- | Lit l => GenLeaf (inr (inl l))
- | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
- | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
+ | Lit l => GenLeaf (Some (inr (inl l)))
+ | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
+ | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
| If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
| Pair e1 e2 => GenNode 5 [go e1; go e2]
| Fst e => GenNode 6 [go e]
@@ -249,15 +252,17 @@ Proof.
| Store e1 e2 => GenNode 14 [go e1; go e2]
| CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
| FAA e1 e2 => GenNode 16 [go e1; go e2]
+ | NewProph => GenLeaf None
+ | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
end).
set (dec := fix go e :=
match e with
- | GenLeaf (inl (inl x)) => Var x
- | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
+ | GenLeaf (Some(inl (inl x))) => Var x
+ | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
| GenNode 1 [e1; e2] => App (go e1) (go e2)
- | GenLeaf (inr (inl l)) => Lit l
- | GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
- | GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
+ | GenLeaf (Some (inr (inl l))) => Lit l
+ | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
+ | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
| GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
| GenNode 5 [e1; e2] => Pair (go e1) (go e2)
| GenNode 6 [e] => Fst (go e)
@@ -271,6 +276,8 @@ Proof.
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
| GenNode 16 [e1; e2] => FAA (go e1) (go e2)
+ | GenLeaf None => NewProph
+ | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
| _ => Lit LitUnit (* dummy *)
end).
refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
@@ -308,7 +315,9 @@ Inductive ectx_item :=
| CasMCtx (e0 : expr) (v2 : val)
| CasRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
- | FaaRCtx (e1 : expr).
+ | FaaRCtx (e1 : expr)
+ | ProphLCtx (v2 : val)
+ | ProphRCtx (e1 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
@@ -334,6 +343,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| CasRCtx e0 e1 => CAS e0 e1 e
| FaaLCtx v2 => FAA e (of_val v2)
| FaaRCtx e1 => FAA e1 e
+ | ProphLCtx v2 => ResolveProph e (of_val v2)
+ | ProphRCtx e1 => ResolveProph e1 e
end.
(** Substitution *)
@@ -359,6 +370,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+ | NewProph => NewProph
+ | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
end.
Definition subst' (mx : binder) (es : expr) : expr → expr :=
@@ -450,28 +463,35 @@ Inductive head_step : expr → state → option observation -> expr → state
| ForkS e σ:
head_step (Fork e) σ None (Lit LitUnit) σ [e]
| AllocS e v σ l :
- to_val e = Some v → σ !! l = None →
- head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ) []
+ to_val e = Some v → σ.1 !! l = None →
+ head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ.1, σ.2) []
| LoadS l v σ :
- σ !! l = Some v →
+ σ.1 !! l = Some v →
head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
| StoreS l e v σ :
- to_val e = Some v → is_Some (σ !! l) →
- head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ) []
+ to_val e = Some v → is_Some (σ.1 !! l) →
+ head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- σ !! l = Some vl → vl ≠v1 →
+ σ.1 !! l = Some vl → vl ≠v1 →
vals_cas_compare_safe vl v1 →
head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- σ !! l = Some v1 →
+ σ.1 !! l = Some v1 →
vals_cas_compare_safe v1 v1 →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ) []
+ head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
| FaaS l i1 e2 i2 σ :
to_val e2 = Some (LitV (LitInt i2)) →
- σ !! l = Some (LitV (LitInt i1)) →
- head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
+ σ.1 !! l = Some (LitV (LitInt i1)) →
+ head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ.1, σ.2) []
+ | NewProphS σ p :
+ p ∉ σ.2 →
+ head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]} ∪ σ.2) []
+ | ResolveProphS e1 p e2 v σ :
+ to_val e1 = Some (LitV $ LitProphecy p) →
+ to_val e2 = Some v →
+ head_step (ResolveProph e1 e2) σ (Some (p, v)) (Lit LitUnit) σ [].
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -499,10 +519,15 @@ Proof.
Qed.
Lemma alloc_fresh e v σ :
- let l := fresh (dom (gset loc) σ) in
- to_val e = Some v → head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ) [].
+ let l := fresh (dom (gset loc) σ.1) in
+ to_val e = Some v → head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ.1, σ.2) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
+Lemma new_proph_fresh σ :
+ let p := fresh σ.2 in
+ head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]} ∪ σ.2) [].
+Proof. constructor. apply is_fresh. Qed.
+
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
to_val (Rec f x e) = Some (RecV f x e).
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 3f2f29dd4..8c3191a4d 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,7 +1,8 @@
+From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
-From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Export lang proph_map.
From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
@@ -9,12 +10,14 @@ Set Default Proof Using "Type".
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
- heapG_gen_heapG :> gen_heapG loc val Σ
+ heapG_gen_heapG :> gen_heapG loc val Σ;
+ heapG_proph_mapG :> proph_mapG proph val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
- state_interp σ κs := gen_heap_ctx σ
+ state_interp σ κs :=
+ (gen_heap_ctx σ.1 ∗ proph_map_ctx κs σ.2)%I
}.
(** Override the notations so that scopes and coercions work out *)
@@ -26,6 +29,9 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
+Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope.
+Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope.
+
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
@@ -127,7 +133,9 @@ Lemma wp_alloc s E e v :
{{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
Proof.
iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+ iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by apply alloc_fresh. }
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -137,7 +145,9 @@ Lemma twp_alloc s E e v :
[[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
Proof.
iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+ iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by apply alloc_fresh. }
iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -147,7 +157,7 @@ Lemma wp_load s E l q v :
{{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -156,7 +166,7 @@ Lemma twp_load s E l q v :
[[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto.
iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -168,10 +178,13 @@ Lemma wp_store s E l v' e v :
Proof.
iIntros (<- Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto 6. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. constructor; eauto. }
+ iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_store s E l v' e v :
IntoVal e v →
@@ -179,10 +192,13 @@ Lemma twp_store s E l v' e v :
Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto 6. iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. constructor; eauto. }
+ iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
@@ -192,7 +208,7 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
Proof.
iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -203,7 +219,7 @@ Lemma twp_cas_fail s E l q v' e1 v1 e2 :
Proof.
iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
@@ -215,10 +231,13 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Proof.
iIntros (<- <- ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by econstructor. }
+ iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
@@ -227,10 +246,13 @@ Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Proof.
iIntros (<- <- ? Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by econstructor. }
+ iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma wp_faa s E l i1 e2 i2 :
@@ -240,10 +262,13 @@ Lemma wp_faa s E l i1 e2 i2 :
Proof.
iIntros (<- Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by constructor. }
+ iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_faa s E l i1 e2 i2 :
IntoVal e2 (LitV (LitInt i2)) →
@@ -252,9 +277,53 @@ Lemma twp_faa s E l i1 e2 i2 :
Proof.
iIntros (<- Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
- iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
- iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+ iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+ iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by constructor. }
+ iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
- iModIntro. iSplit=>//. by iApply "HΦ".
+ iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
+
+(** Lifting lemmas for creating and resolving prophecy variables *)
+Lemma wp_new_proph :
+ {{{ True }}} NewProph {{{ (p : proph), RET (LitV (LitProphecy p)); p ⥱ - }}}.
+Proof.
+ iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by apply new_proph_fresh. }
+ unfold cons_obs. simpl.
+ iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
+ iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
+ { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
+ iModIntro; iSplit=> //. iFrame. iSplitL "HR".
+ - iExists _. iSplit; last done.
+ iPureIntro. split.
+ + apply first_resolve_insert; auto.
+ + rewrite dom_insert_L. by apply union_mono_l.
+ - iApply "HΦ". by iExists _.
+Qed.
+
+Lemma wp_resolve_proph e1 e2 p v w:
+ IntoVal e1 (LitV (LitProphecy p)) →
+ IntoVal e2 w →
+ {{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌠}}}.
+Proof.
+ iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+ iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
+ (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+ { iPureIntro. repeat eexists. by constructor. }
+ unfold cons_obs. simpl.
+ iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
+ iSplit=> //. iFrame.
+ iMod ((@proph_map_remove _ _ _ _ _ _ _ p0) with "HR Hp") as "Hp". iModIntro.
+ iSplitR "HΦ".
+ - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
+ rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
+ - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
+Qed.
+
End lifting.
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
new file mode 100644
index 000000000..fab888a47
--- /dev/null
+++ b/theories/heap_lang/proph_map.v
@@ -0,0 +1,183 @@
+From iris.algebra Require Import auth gmap.
+From iris.base_logic.lib Require Export own.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
+Definition proph_val_list (P V : Type) := list (P * V).
+
+Section first_resolve.
+
+ Context {P V : Type} `{Countable P}.
+ Implicit Type pvs : proph_val_list P V.
+ Implicit Type p : P.
+ Implicit Type v : V.
+ Implicit Type R : proph_map P V.
+
+ (** The first resolve for [p] in [pvs] *)
+ Definition first_resolve pvs p :=
+ (map_of_list pvs : gmap P V) !! p.
+
+ Definition first_resolve_in_list R pvs :=
+ forall p v, p ∈ dom (gset _) R →
+ first_resolve pvs p = Some v →
+ R !! p = Some (Some v).
+
+ Lemma first_resolve_insert pvs p R :
+ first_resolve_in_list R pvs →
+ p ∉ dom (gset _) R →
+ first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
+ Proof.
+ intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
+ erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
+ - by rewrite lookup_insert.
+ - rewrite lookup_insert_ne; first auto. by intros ->.
+ Qed.
+
+ Lemma first_resolve_delete pvs p v R :
+ first_resolve_in_list R ((p, v) :: pvs) →
+ first_resolve_in_list (delete p R) pvs.
+ Proof.
+ intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
+ apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
+ erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
+ Qed.
+
+ Lemma first_resolve_eq R p v w pvs :
+ first_resolve_in_list R ((p, v) :: pvs) →
+ R !! p = Some w →
+ w = Some v.
+ Proof.
+ intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
+ rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
+ inversion Hlookup. done.
+ Qed.
+
+End first_resolve.
+
+Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
+ gmapUR P $ exclR $ optionC $ leibnizC V.
+
+Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
+ fmap (λ v, Excl (v : option (leibnizC V))) pvs.
+
+(** The CMRA we need. *)
+Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
+ proph_map_inG :> inG Σ (authR (proph_mapUR P V));
+ proph_map_name : gname
+}.
+Arguments proph_map_name {_ _ _ _ _} _ : assert.
+
+Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
+ { proph_map_preG_inG :> inG Σ (authR (proph_mapUR P V)) }.
+
+Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
+ #[GFunctor (authR (proph_mapUR P V))].
+
+Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
+ subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+ Context `{pG : proph_mapG P V Σ}.
+
+ Definition proph_map_auth (R : proph_map P V) : iProp Σ :=
+ own (proph_map_name pG) (â— (to_proph_map R)).
+
+ Definition proph_map_ctx (pvs : proph_val_list P V) (ps : gset P) : iProp Σ :=
+ (∃ R, ⌜first_resolve_in_list R pvs ∧
+ dom (gset _) R ⊆ ps⌠∗
+ proph_map_auth R)%I.
+
+ Definition p_mapsto_def (p : P) (v: option V) : iProp Σ :=
+ own (proph_map_name pG) (â—¯ {[ p := Excl (v : option $ leibnizC V) ]}).
+ Definition p_mapsto_aux : seal (@p_mapsto_def). by eexists. Qed.
+ Definition p_mapsto := p_mapsto_aux.(unseal).
+ Definition p_mapsto_eq : @p_mapsto = @p_mapsto_def := p_mapsto_aux.(seal_eq).
+
+End definitions.
+
+Local Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope.
+Local Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope.
+
+Section to_proph_map.
+ Context (P V : Type) `{Countable P}.
+ Implicit Types p : P.
+ Implicit Types R : proph_map P V.
+
+ Lemma to_proph_map_valid R : ✓ to_proph_map R.
+ Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
+
+ Lemma to_proph_map_insert p v R :
+ to_proph_map (<[p := v]> R) = <[p := Excl (v: option (leibnizC V))]> (to_proph_map R).
+ Proof. by rewrite /to_proph_map fmap_insert. Qed.
+
+ Lemma to_proph_map_delete p R :
+ to_proph_map (delete p R) = delete p (to_proph_map R).
+ Proof. by rewrite /to_proph_map fmap_delete. Qed.
+
+ Lemma lookup_to_proph_map_None R p :
+ R !! p = None → to_proph_map R !! p = None.
+ Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
+
+ Lemma proph_map_singleton_included R p v :
+ {[p := Excl v]} ≼ to_proph_map R → R !! p = Some v.
+ Proof.
+ rewrite singleton_included=> -[v' []].
+ rewrite /to_proph_map lookup_fmap fmap_Some_equiv=> -[v'' [Hp ->]].
+ intros [=->]%Some_included_exclusive%leibniz_equiv_iff; first done; last done.
+ apply excl_exclusive.
+ Qed.
+End to_proph_map.
+
+
+
+Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
+ (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
+Proof.
+ iMod (own_alloc (◠to_proph_map ∅)) as (γ) "Hh".
+ { apply: auth_auth_valid. exact: to_proph_map_valid. }
+ iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
+ iPureIntro. split =>//.
+Qed.
+
+Section proph_map.
+ Context `{proph_mapG P V Σ}.
+ Implicit Types p : P.
+ Implicit Types v : option V.
+ Implicit Types R : proph_map P V.
+
+ (** General properties of mapsto *)
+ Global Instance p_mapsto_timeless p v : Timeless (p ⥱ v).
+ Proof. rewrite p_mapsto_eq /p_mapsto_def. apply _. Qed.
+
+ Lemma proph_map_alloc R p v :
+ p ∉ dom (gset _) R →
+ proph_map_auth R ==∗ proph_map_auth (<[p := v]> R) ∗ p ⥱ v.
+ Proof.
+ iIntros (?) "HR". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def.
+ iMod (own_update with "HR") as "[HR Hl]".
+ {
+ eapply auth_update_alloc,
+ (alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
+ apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) H1).
+ }
+ iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
+ Qed.
+
+ Lemma proph_map_remove R p v :
+ proph_map_auth R -∗ p ⥱ v ==∗ proph_map_auth (delete p R).
+ Proof.
+ iIntros "HR Hp". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def.
+ rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp").
+ apply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+ Qed.
+
+ Lemma proph_map_valid R p v : proph_map_auth R -∗ p ⥱ v -∗ ⌜R !! p = Some vâŒ.
+ Proof.
+ iIntros "HR Hp". rewrite /proph_map_ctx p_mapsto_eq /p_mapsto_def.
+ iDestruct (own_valid_2 with "HR Hp")
+ as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
+ Qed.
+End proph_map.
--
GitLab