Skip to content
Snippets Groups Projects
Commit 1be9e3c6 authored by Marianna Rapoport's avatar Marianna Rapoport Committed by Ralf Jung
Browse files

Making prophecy-related examples work with the new prophecy support 

- Removing admitted prophecy spec and making prophecy-related examples (coin-flip and atomic-pair-snapshot) work with the new prophecy support in heap_lang
- Adjusting heap_lang tactics for automation of substitution, closedness, etc. to support prophecy syntax
- Adding notation for prophecy syntax
parent 20c479dd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 0
− 1
View file @ 1be9e3c6
......@@ -88,7 +88,6 @@ 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
theories/heap_lang/lib/assert.v
......
theories/heap_lang/lib/atomic_snapshot.v
+ 11
− 13
View file @ 1be9e3c6
......@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par prophecy.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
......@@ -100,15 +100,15 @@ Section atomic_snapshot.
then (Fst "x", Fst "y")
else "readPair" "l".
Definition readPair_proph pr : val :=
Definition readPair_proph : val :=
rec: "readPair" "l" :=
let: "xv1" := readX "l" in
let: "proph" := new_prophecy pr #() in
let: "proph" := new prophecy in
let: "y" := readY "l" in
let: "xv2" := readX "l" in
let: "v2" := Snd "xv2" in
let: "v_eq" := Snd "xv1" = "v2" in
resolve_prophecy pr "proph" "v_eq" ;;
resolve "proph" to "v_eq" ;;
if: "v_eq"
then (Fst "xv1", "y")
else "readPair" "l".
......@@ -368,18 +368,16 @@ Section atomic_snapshot.
wp_load. eauto.
Qed.
Definition val_to_bool (v:val) : bool :=
Definition val_to_bool (v : option val) : bool :=
match v with
| LitV (LitBool b) => b
| _ => false
| Some (LitV (LitBool b)) => b
| _ => false
end.
Variable pr: prophecy.
Lemma readPair_spec γ p :
is_pair γ p -∗
<<< ∀ v1 v2 : val, pair_content γ (v1, v2) >>>
readPair_proph pr p
readPair_proph p
@ ⊤∖↑N
<<< pair_content γ (v1, v2), RET (v1, v2) >>>.
Proof.
......@@ -405,7 +403,7 @@ Section atomic_snapshot.
}
wp_load. wp_let.
(* ************ new prophecy ********** *)
wp_apply new_prophecy_spec; first done.
wp_apply wp_new_proph; first done.
iIntros (proph) "Hpr". iDestruct "Hpr" as (proph_val) "Hpr".
wp_let.
(* ************ readY ********** *)
......@@ -447,7 +445,7 @@ Section atomic_snapshot.
iNext. unfold pair_inv. eauto 8 with iFrame.
}
wp_load. wp_let. wp_proj. wp_let. wp_proj. wp_op.
case_bool_decide; wp_let; wp_apply (resolve_prophecy_spec with "Hpr");
case_bool_decide; wp_let; wp_apply (wp_resolve_proph with "Hpr");
iIntros (->); wp_seq; wp_if.
+ inversion H; subst; clear H. wp_proj.
assert (v_x2 = v_y) as ->. {
......@@ -483,7 +481,7 @@ Section atomic_snapshot.
iNext. unfold pair_inv. eauto 8 with iFrame.
}
wp_load. repeat (wp_let; wp_proj). wp_op. wp_let.
wp_apply (resolve_prophecy_spec with "Hpr").
wp_apply (wp_resolve_proph with "Hpr").
iIntros (Heq). subst.
case_bool_decide.
+ inversion H; subst; clear H. inversion Hproph.
......
theories/heap_lang/lib/atomic_snapshot_spec.v
+ 1
− 1
View file @ 1be9e3c6
......@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par prophecy.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
......
theories/heap_lang/lib/coin_flip.v
+ 21
− 21
View file @ 1be9e3c6
......@@ -4,7 +4,6 @@ From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
From iris.heap_lang Require Import prophecy.
Set Default Proof Using "Type".
(** Nondeterminism and Speculation:
......@@ -29,19 +28,19 @@ Section coinflip.
λ: "x",
"x" <- #0 ;;
rand #().
Context `{!heapG Σ} (N: namespace).
Lemma rand_spec :
{{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
Proof using N.
iIntros (Φ) "_ HP".
wp_lam. wp_alloc l as "Hl". wp_lam.
iMod (inv_alloc N _ (∃ (b: bool), l ↦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
wp_apply wp_fork. iSplitL.
wp_apply wp_fork.
- iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
- wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
iApply "HP". done.
- iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
Qed.
Lemma earlyChoice_spec (x: loc) :
......@@ -50,7 +49,7 @@ Section coinflip.
@ ⊤
<<< ∃ (b: bool), x ↦ #0, RET #b >>>.
Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_bind (rand _)%E. iApply rand_spec; first done.
iIntros (b) "!> _". wp_let.
wp_bind (_ <- _)%E.
......@@ -78,47 +77,48 @@ Section coinflip.
iMod ("Hclose" $! true with "[Hl]") as "AU"; first by eauto.
iModIntro. wp_seq.
iApply rand_spec; first done.
iIntros (b) "!> _".
iIntros (b) "!> _".
Abort.
End coinflip.
Section coinflip_with_prophecy.
Context `{!heapG Σ} `{pr: prophecy} (N: namespace).
Section coinflip_with_prophecy.
Context `{!heapG Σ} (N: namespace).
Definition val_to_bool v : bool :=
match v with
| LitV (LitBool b) => b
| _ => true
| Some (LitV (LitBool b)) => b
| _ => true
end.
Definition lateChoice_proph: val :=
λ: "x",
let: "p" := new_prophecy pr #() in
let: "p" := new prophecy in
"x" <- #0 ;;
let: "r" := rand #() in
resolve_prophecy pr "p" "r".
resolve "p" to "r" ;;
"r".
Lemma lateChoice_proph_spec (x: loc) :
<<< x ↦ - >>>
lateChoice_proph #x
@ ⊤
<<< ∃ (b: bool), x ↦ #0, RET #b >>>.
<<< ∃ (b: bool), x ↦ #0, RET #b >>>.
Proof using N.
iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
wp_apply new_prophecy_spec; first done.
wp_apply wp_new_proph; first done.
iIntros (p) "Hp". iDestruct "Hp" as (v) "Hp".
wp_let.
wp_let.
wp_bind (_ <- _)%E.
iMod "AU" as "[Hl [_ Hclose]]".
iDestruct "Hl" as (v') "Hl".
wp_store.
iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
iModIntro. wp_seq. wp_apply rand_spec; try done.
iIntros (b') "_". wp_let.
iApply (resolve_prophecy_spec with "Hp").
iNext. iIntros (->). done.
iIntros (b') "_". wp_let. wp_bind (resolve _ to _)%E.
iApply (wp_resolve_proph with "Hp").
iNext. iIntros (->). wp_seq. done.
Qed.
End coinflip_with_prophecy.
theories/heap_lang/notation.v
+ 3
− 0
View file @ 1be9e3c6
......@@ -157,3 +157,6 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'new' 'prophecy'" := NewProph (at level 100) : expr_scope.
Notation "'resolve' p 'to' v" := (ResolveProph p v) (at level 100) : expr_scope.
theories/heap_lang/prophecy.v deleted 100644 → 0
+ 0
− 27
View file @ 20c479dd
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
Section prophecy.
Context `{!heapG Σ} (N: namespace).
Record prophecy {Σ} `{!heapG Σ} := Prophecy {
(* -- operations -- *)
new_prophecy : val;
resolve_prophecy : val;
(* -- predicates -- *)
is_prophecy : proph -> val -> iProp Σ;
(* -- general properties -- *)
new_prophecy_spec:
{{{ True }}} new_prophecy #() {{{ p, RET #p; ∃ v, is_prophecy p v }}};
resolve_prophecy_spec p v e w:
IntoVal e w ->
{{{ is_prophecy p v }}} resolve_prophecy #p e {{{ RET w; ⌜v = w⌝ }}}
}.
End prophecy.
theories/heap_lang/tactics.v
+ 18
− 4
View file @ 1be9e3c6
......@@ -35,7 +35,9 @@ 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)
| NewProph
| ResolveProph (e1 : expr) (e2 : expr).
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
......@@ -60,6 +62,8 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
| NewProph => heap_lang.NewProph
| ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
end.
Ltac of_expr e :=
......@@ -93,7 +97,11 @@ Ltac of_expr e :=
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| heap_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| heap_lang.NewProph =>
constr:(NewProph)
| heap_lang.ResolveProph ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
......@@ -108,10 +116,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| Val _ _ _ | ClosedExpr _ => true
| 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
......@@ -171,6 +179,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.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
......@@ -190,6 +200,8 @@ Definition is_atomic (e : expr) :=
| Fork _ => true
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| NewProph => true
| ResolveProph e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
| _ => false
end.
Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
......@@ -293,4 +305,6 @@ Ltac reshape_expr e tac :=
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
| ResolveProph ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (ProphLCtx v2 :: K) e1)
| ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
end in go (@nil ectx_item) e.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment