Skip to content
Snippets Groups Projects
Commit 734bc0ab authored by Ralf Jung's avatar Ralf Jung
Browse files

use 'proph' instead of a notation, and rename type of prophecy variables to proph_id

parent cc712c90
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/adequacy.v
+ 4
− 4
View file @ 734bc0ab
......@@ -7,10 +7,10 @@ Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ;
heap_preG_proph :> proph_mapPreG proph val Σ
heap_preG_proph :> proph_mapPreG proph_id val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph val].
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.
......@@ -20,8 +20,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init κs σ.(used_proph)) as (?) "Hp".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph))%I). iFrame.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
theories/heap_lang/lang.v
+ 15
− 14
View file @ 734bc0ab
......@@ -29,10 +29,11 @@ Open Scope Z_scope.
(** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *)
Definition proph := positive.
Definition proph_id := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitProphecy (p: proph).
| LitInt (n : Z) | LitBool (b : bool) | LitUnit
| LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
......@@ -117,7 +118,7 @@ Inductive val :=
Bind Scope val_scope with val.
Definition observation : Set := proph * val.
Definition observation : Set := proph_id * val.
Fixpoint of_val (v : val) : expr :=
match v with
......@@ -174,7 +175,7 @@ Definition val_is_unboxed (v : val) : Prop :=
(** The state: heaps of vals. *)
Record state : Type := {
heap: gmap loc val;
used_proph: gset proph;
used_proph_id: gset proph_id;
}.
(** Equality and other typeclass stuff *)
......@@ -295,7 +296,7 @@ Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; used_proph := inhabitant |}.
populate {| heap := inhabitant; used_proph_id := inhabitant |}.
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
......@@ -442,11 +443,11 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
Arguments vals_cas_compare_safe !_ !_ /.
Definition state_upd_heap (f: gmap loc val → gmap loc val) (σ: state) :=
{| heap := f σ.(heap); used_proph := σ.(used_proph) |}.
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Arguments state_upd_heap _ !_ /.
Definition state_upd_used_proph (f: gset proph → gset proph) (σ: state) :=
{| heap := σ.(heap); used_proph := f σ.(used_proph) |}.
Arguments state_upd_used_proph _ !_ /.
Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: state) :=
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.
Inductive head_step : expr → state → list observation → expr → state → list (expr) → Prop :=
| BetaS f x e1 e2 v2 e' σ :
......@@ -516,10 +517,10 @@ Inductive head_step : expr → state → list observation → expr → state →
(Lit $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]> σ)
[]
| NewProphS σ p :
p ∉ σ.(used_proph) →
p ∉ σ.(used_proph_id) →
head_step NewProph σ
[]
(Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ)
(Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
[]
| ResolveProphS e1 p e2 v σ :
to_val e1 = Some (LitV $ LitProphecy p) →
......@@ -557,9 +558,9 @@ Lemma alloc_fresh e v σ :
head_step (Alloc e) σ [] (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
Lemma new_proph_fresh σ :
let p := fresh σ.(used_proph) in
head_step NewProph σ [] (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ) [].
Lemma new_proph_id_fresh σ :
let p := fresh σ.(used_proph_id) in
head_step NewProph σ [] (Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ) [].
Proof. constructor. apply is_fresh. Qed.
(* Misc *)
......
theories/heap_lang/lifting.v
+ 5
− 8
View file @ 734bc0ab
......@@ -11,13 +11,13 @@ Set Default Proof Using "Type".
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ;
heapG_proph_mapG :> proph_mapG proph val Σ
heapG_proph_mapG :> proph_mapG proph_id val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs :=
(gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph))%I
(gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I
}.
(** Override the notations so that scopes and coercions work out *)
......@@ -29,9 +29,6 @@ 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" := (proph_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
......@@ -56,7 +53,7 @@ Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_fresh.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
Local Hint Resolve to_of_val.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
......@@ -270,7 +267,7 @@ Qed.
(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
{{{ True }}} NewProph {{{ v (p : proph), RET (LitV (LitProphecy p)); p ⥱ v }}}.
{{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
......@@ -289,7 +286,7 @@ 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⌝ }}}.
{{{ proph 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".
......
theories/heap_lang/notation.v
+ 1
− 1
View file @ 734bc0ab
......@@ -8,7 +8,7 @@ Delimit Scope val_scope with V.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit.
Coercion LitProphecy : proph >-> base_lit.
Coercion LitProphecy : proph_id >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
......
theories/heap_lang/proph_map.v
+ 13
− 16
View file @ 734bc0ab
......@@ -89,18 +89,15 @@ Section definitions.
dom (gset _) R ⊆ ps⌝ ∗
proph_map_auth R)%I.
Definition proph_mapsto_def (p : P) (v: option V) : iProp Σ :=
Definition proph_def (p : P) (v: option V) : iProp Σ :=
own (proph_map_name pG) (◯ {[ p := Excl (v : option $ leibnizC V) ]}).
Definition proph_mapsto_aux : seal (@proph_mapsto_def). by eexists. Qed.
Definition proph_mapsto := proph_mapsto_aux.(unseal).
Definition proph_mapsto_eq :
@proph_mapsto = @proph_mapsto_def := proph_mapsto_aux.(seal_eq).
Definition proph_aux : seal (@proph_def). by eexists. Qed.
Definition proph := proph_aux.(unseal).
Definition proph_eq :
@proph = @proph_def := proph_aux.(seal_eq).
End definitions.
Local Notation "p ⥱ v" := (proph_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.
......@@ -148,14 +145,14 @@ Section proph_map.
Implicit Types R : proph_map P V.
(** General properties of mapsto *)
Global Instance p_mapsto_timeless p v : Timeless (p ⥱ v).
Proof. rewrite proph_mapsto_eq /proph_mapsto_def. apply _. Qed.
Global Instance proph_timeless p v : Timeless (proph p v).
Proof. rewrite proph_eq /proph_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.
proph_map_auth R ==∗ proph_map_auth (<[p := v]> R) ∗ proph p v.
Proof.
iIntros (Hp) "HR". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def.
iIntros (Hp) "HR". rewrite /proph_map_ctx proph_eq /proph_def.
iMod (own_update with "HR") as "[HR Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
......@@ -164,16 +161,16 @@ Section proph_map.
Qed.
Lemma proph_map_remove R p v :
proph_map_auth R -∗ p ⥱ v ==∗ proph_map_auth (delete p R).
proph_map_auth R -∗ proph p v ==∗ proph_map_auth (delete p R).
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_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⌝.
Lemma proph_map_valid R p v : proph_map_auth R -∗ proph p v -∗ ⌜R !! p = Some v⌝.
Proof.
iIntros "HR Hp". rewrite /proph_map_ctx proph_mapsto_eq /proph_mapsto_def.
iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
iDestruct (own_valid_2 with "HR Hp")
as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
Qed.
......
theories/heap_lang/total_adequacy.v
+ 2
− 2
View file @ 734bc0ab
......@@ -10,8 +10,8 @@ Definition heap_total Σ `{heapPreG Σ} s e σ φ :
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph)) as (?) "Hp".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph))%I). iFrame.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
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