Skip to content

GitLab

Commit ed2a50a1 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

Get rid of the second mask in the refinement judgement

parent 45c61194
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 685 additions and 903 deletions
theories/examples/Y.v
View file @ ed2a50a1
......@@ -16,7 +16,7 @@ Definition F : val := rec: "f" "g" :=
Section contents.
Context `{logrelG Σ}.
Lemma Y_semtype Δ Γ A :
{⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ Y : TArrow (TArrow A A) A.
{Δ;Γ} ⊨ Y ≤log≤ Y : TArrow (TArrow A A) A.
Proof.
unlock Y. simpl.
iApply bin_log_related_arrow; eauto.
......@@ -29,7 +29,7 @@ Section contents.
Qed.
Lemma KNOT_Y Δ Γ A :
{⊤,⊤;Δ;Γ} ⊨ Knot ≤log≤ Y : TArrow (TArrow A A) A.
{Δ;Γ} ⊨ Knot ≤log≤ Y : TArrow (TArrow A A) A.
Proof.
unlock Y Knot. simpl.
iApply bin_log_related_arrow; eauto.
......@@ -46,7 +46,7 @@ Section contents.
Qed.
Lemma Y_KNOT Δ Γ A :
{⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ Knot : TArrow (TArrow A A) A.
{Δ;Γ} ⊨ Y ≤log≤ Knot : TArrow (TArrow A A) A.
Proof.
unlock Y Knot. simpl.
iApply bin_log_related_arrow; eauto.
......@@ -63,7 +63,7 @@ Section contents.
Qed.
Lemma FIX_Y Δ Γ A :
{⊤,⊤;Δ;Γ} ⊨ F ≤log≤ Y : TArrow (TArrow A A) A.
{Δ;Γ} ⊨ F ≤log≤ Y : TArrow (TArrow A A) A.
Proof.
unlock Y F. simpl.
iApply bin_log_related_arrow; eauto.
......@@ -76,7 +76,7 @@ Section contents.
Qed.
Lemma Y_FIX Δ Γ A :
{⊤,⊤;Δ;Γ} ⊨ Y ≤log≤ F : TArrow (TArrow A A) A.
{Δ;Γ} ⊨ Y ≤log≤ F : TArrow (TArrow A A) A.
Proof.
unlock Y F. simpl.
iApply bin_log_related_arrow; eauto.
......
theories/examples/bit.v
View file @ ed2a50a1
......@@ -60,11 +60,11 @@ Section bit_refinement.
Instance bitτi_persistent ww : Persistent (bitτi ww).
Proof. apply _. Qed.
Lemma bit_prerefinement Γ E :
{E;Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ.
Lemma bit_prerefinement Γ :
{Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ.
Proof.
unfold bit_bool, bit_nat; simpl. (* we need this to compute the coercion from values to expression *)
iApply (bin_log_related_pack _ bitτi).
iApply (bin_log_related_pack bitτi).
repeat iApply bin_log_related_pair.
- rel_vals; simpl; eauto. (* TODO: make a rel_finish tactic or change rel_vals *)
- unfold flip_nat.
......@@ -115,14 +115,13 @@ Section heapify_refinement.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Notation D := (prodC valC valC -n> iProp Σ).
Lemma heapify_refinement_ez Γ E1 b1 b2 :
↑logrelN ⊆ E1 →
{E1;Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗
{E1;Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ.
Lemma heapify_refinement_ez Γ b1 b2 :
{Δ;Γ} ⊨ b1 ≤log≤ b2 : bitτ -∗
{Δ;Γ} ⊨ heapify b1 ≤log≤ heapify b2 : bitτ.
Proof.
iIntros (?) "Hb1b2".
iIntros "Hb1b2".
iApply bin_log_related_app; eauto.
iApply binary_fundamental_masked; eauto with typeable.
iApply binary_fundamental; eauto with typeable.
Qed.
End heapify_refinement.
......
theories/examples/bot.v
View file @ ed2a50a1
......@@ -10,8 +10,8 @@ Hint Resolve bot_typed : typeable.
Section contents.
Context `{logrelG Σ}.
Lemma bot_l Δ Γ E K t τ :
{E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ.
Lemma bot_l Δ Γ K t τ :
{Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ.
Proof.
iLöb as "IH".
rel_rec_l.
......
theories/examples/coqpl.v
View file @ ed2a50a1
......@@ -44,7 +44,7 @@ Section refinement.
{Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitT.
Proof.
unlock bit_bool bit_nat; simpl.
iApply (bin_log_related_pack _ R).
iApply (bin_log_related_pack R).
repeat iApply bin_log_related_pair.
- rel_finish.
- rel_arrow_val. simpl.
......
theories/examples/counter.v
View file @ ed2a50a1
......@@ -37,12 +37,12 @@ Section CG_Counter.
Hint Resolve CG_increment_type : typeable.
Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) :
nclose specN ⊆ E1 →
Lemma bin_log_related_CG_increment_r Γ K E t τ (x l : loc) (n : nat) :
nclose specN ⊆ E →
(x ↦ₛ # n -∗ l ↦ₛ #false -∗
(x ↦ₛ # (S n) -∗ l ↦ₛ #false -∗
({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ)) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
({E;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ)) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_increment. unlock. simpl_subst/=.
......@@ -60,11 +60,11 @@ Section CG_Counter.
by iApply ("Hlog" with "Hx Hl").
Qed.
Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
(Hspec : nclose specN ⊆ E1) :
Lemma bin_log_counter_read_r Γ E K x (n : nat) t τ
(Hspec : nclose specN ⊆ E) :
x ↦ₛ #n -∗
(x ↦ₛ #n -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
(x ↦ₛ #n -∗ {E;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
Proof.
iIntros "Hx Hlog".
unfold counter_read. unlock. simpl.
......@@ -92,12 +92,12 @@ Section CG_Counter.
Hint Resolve FG_increment_type : typeable.
Lemma bin_log_related_FG_increment_r Γ K E1 E2 t τ (x : loc) (n : nat) :
nclose specN ⊆ E1 →
Lemma bin_log_related_FG_increment_r Γ K E t τ (x : loc) (n : nat) :
nclose specN ⊆ E →
(x ↦ₛ # n -∗
(x ↦ₛ #(S n) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
{E;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unlock FG_increment. simpl_subst/=.
......@@ -123,13 +123,13 @@ Section CG_Counter.
(* A logically atomic specification for
a fine-grained increment with a baked in frame. *)
(* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
Lemma bin_log_FG_increment_logatomic R P Γ E1 E2 K x t τ :
Lemma bin_log_FG_increment_logatomic R P Γ E K x t τ :
P -∗
□ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧
□ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧
(∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗
{E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-∗ ({E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ).
{E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-∗ ({Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ).
Proof.
iIntros "HP #H".
iLöb as "IH".
......@@ -166,13 +166,13 @@ Section CG_Counter.
Qed.
(* A similar atomic specification for the counter_read fn *)
Lemma bin_log_counter_read_atomic_l R P Γ E1 E2 K x t τ :
Lemma bin_log_counter_read_atomic_l R P Γ E K x t τ :
P -∗
□ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧
□ (|={⊤,E}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧
(∀ m : nat, x ↦ᵢ #m ∗ R m -∗ P -∗
{E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-∗ {E1;Δ;Γ} ⊨ fill K ((counter_read $/ LitV (Loc x)) #()) ≤log≤ t : τ.
{E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-∗ {Δ;Γ} ⊨ fill K ((counter_read $/ LitV (Loc x)) #()) ≤log≤ t : τ.
Proof.
iIntros "HP #H".
unfold counter_read. unlock. simpl.
......
theories/examples/generative.v
View file @ ed2a50a1
......@@ -73,7 +73,7 @@ Section namegen_refinement.
iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
{ iNext. iExists 0, ∅. iFrame.
by rewrite big_sepS_empty. }
iApply (bin_log_related_pack _ (ngR γ)).
iApply (bin_log_related_pack (ngR γ)).
iApply bin_log_related_pair.
- (* New name *)
iApply bin_log_related_arrow_val; eauto.
......@@ -219,7 +219,7 @@ Section cell_refinement.
unlock cell2 cell1 cellτ.
iApply bin_log_related_tlam; auto.
iIntros (R HR) "!#".
iApply (bin_log_related_pack _ (cellR R)).
iApply (bin_log_related_pack (cellR R)).
repeat iApply bin_log_related_pair.
- (* New cell *)
iApply bin_log_related_arrow_val; eauto.
......
theories/examples/lateearlychoice.v
View file @ ed2a50a1
......@@ -36,12 +36,11 @@ Section Refinement.
iIntros "Hy"; iMod ("Hcl" with "[Hy]"); eauto.
Qed.
Lemma rand_l Δ Γ E1 K ρ t τ :
↑choiceN ⊆ E1 →
spec_ctx ρ -∗ (∀ b : bool, {E1;Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗
{E1;Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ.
Lemma rand_l Δ Γ K ρ t τ :
spec_ctx ρ -∗ (∀ b : bool, {Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗
{Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ.
Proof.
iIntros (?) "#Hs Hlog".
iIntros "#Hs Hlog".
unfold rand. unlock. simpl.
rel_rec_l.
rel_alloc_l as y "Hy". simpl.
......@@ -67,12 +66,12 @@ Section Refinement.
done.
Qed.
Lemma rand_r (b : bool) Δ Γ E1 E2 K ρ t τ :
Lemma rand_r (b : bool) Δ Γ E1 K ρ t τ :
↑specN ⊆ E1 →
↑choiceN ⊆ E1 →
spec_ctx ρ -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #b : τ -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #()) : τ.
{E1;Δ;Γ} ⊨ t ≤log≤ fill K #b : τ -∗
{E1;Δ;Γ} ⊨ t ≤log≤ fill K (rand #()) : τ.
Proof.
iIntros (??) "#Hs Hlog".
unfold rand. unlock.
......@@ -89,8 +88,8 @@ Section Refinement.
Lemma lateChoice_l Δ Γ x v ρ t :
spec_ctx ρ -∗ x ↦ᵢ v -∗
(x ↦ᵢ #0 -∗ ∀ b : bool, {⊤,⊤;Δ;Γ} ⊨ #b ≤log≤ t : TBool) -∗
{⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ t : TBool.
(x ↦ᵢ #0 -∗ ∀ b : bool, {Δ;Γ} ⊨ #b ≤log≤ t : TBool) -∗
{Δ;Γ} ⊨ lateChoice #x ≤log≤ t : TBool.
Proof.
iIntros "#Hs Hx Hlog".
unfold lateChoice. unlock.
......@@ -103,7 +102,7 @@ Section Refinement.
Lemma prerefinement Δ Γ x x' n ρ :
spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗
{⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool.
{Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool.
Proof.
iIntros "#Hspec Hx Hx'".
iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
......@@ -120,7 +119,7 @@ Section Refinement.
Lemma prerefinement2 Δ Γ x x' n ρ :
spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗
{⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool.
{Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool.
Proof.
iIntros "#Hspec Hx Hx'".
unfold earlyChoice. unlock.
......
theories/examples/lock.v
View file @ ed2a50a1
......@@ -69,11 +69,11 @@ Section lockG_rules.
Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ E K t τ :
Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ K t τ :
R -∗
▷(∀ (lk : loc) γ, is_lock γ #lk R
-∗ ({E;Δ;Γ} ⊨ fill K #lk ≤log≤ t: τ)) -∗
{E;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t: τ.
-∗ ({Δ;Γ} ⊨ fill K #lk ≤log≤ t: τ)) -∗
{Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t: τ.
Proof.
iIntros "HR Hlog".
iApply bin_log_related_wp_l.
......@@ -85,15 +85,14 @@ Section lockG_rules.
iModIntro. iApply "Hlog". iExists l. eauto.
Qed.
Lemma bin_log_related_release_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
↑N ⊆ E →
Lemma bin_log_related_release_l (R : iProp Σ) (lk : loc) γ Δ Γ K t τ :
is_lock γ #lk R -∗
locked γ -∗
R -∗
▷({E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
{E;Δ;Γ} ⊨ fill K (release #lk) ≤log≤ t: τ.
▷({Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
{Δ;Γ} ⊨ fill K (release #lk) ≤log≤ t: τ.
Proof.
iIntros (?) "Hlock Hlocked HR Hlog".
iIntros "Hlock Hlocked HR Hlog".
iDestruct "Hlock" as (l) "[% #?]"; simplify_eq.
unlock release. simpl.
rel_let_l.
......@@ -106,13 +105,12 @@ Section lockG_rules.
iApply "Hlog".
Qed.
Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ E K t τ :
↑N ⊆ E →
Lemma bin_log_related_acquire_l (R : iProp Σ) (lk : loc) γ Δ Γ K t τ :
is_lock γ #lk R -∗
▷(locked γ -∗ R -∗ {E;Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
{E;Δ;Γ} ⊨ fill K (acquire #lk) ≤log≤ t: τ.
▷(locked γ -∗ R -∗ {Δ;Γ} ⊨ fill K #() ≤log≤ t: τ) -∗
{Δ;Γ} ⊨ fill K (acquire #lk) ≤log≤ t: τ.
Proof.
iIntros (?) "#Hlock Hlog".
iIntros "#Hlock Hlog".
iLöb as "IH".
unlock acquire. simpl.
rel_rec_l.
......@@ -139,13 +137,13 @@ End lockG_rules.
Section lock_rules_r.
Context `{logrelG Σ}.
Variable (E1 E2 : coPset).
Variable (E : coPset).
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Lemma bin_log_related_newlock_r Γ K t τ
(Hcl : nclose specN ⊆ E1) :
(∀ l : loc, l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #l : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #()): τ.
(Hcl : nclose specN ⊆ E) :
(∀ l : loc, l ↦ₛ #false -∗ {E;Δ;Γ} ⊨ t ≤log≤ fill K #l : τ) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K (newlock #()): τ.
Proof.
iIntros "Hlog".
unfold newlock. unlock.
......@@ -155,8 +153,8 @@ Section lock_rules_r.
Qed.
Lemma bin_log_related_newlock_l_simp Γ K t τ :
(∀ l : loc, l ↦ᵢ #false -∗ {E1;Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗
{E1;Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ.
(∀ l : loc, l ↦ᵢ #false -∗ {Δ;Γ} ⊨ fill K #l ≤log≤ t : τ) -∗
{Δ;Γ} ⊨ fill K (newlock #()) ≤log≤ t : τ.
Proof.
iIntros "Hlog".
unfold newlock. unlock.
......@@ -170,10 +168,10 @@ Section lock_rules_r.
Transparent acquire.
Lemma bin_log_related_acquire_r Γ K l t τ
(Hcl : nclose specN ⊆ E1) :
(Hcl : nclose specN ⊆ E) :
l ↦ₛ #false -∗
(l ↦ₛ #true -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (acquire #l) : τ.
(l ↦ₛ #true -∗ {E;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K (acquire #l) : τ.
Proof.
iIntros "Hl Hlog".
unfold acquire. unlock.
......@@ -185,8 +183,8 @@ Section lock_rules_r.
Lemma bin_log_related_acquire_suc_l Γ K l t τ :
l ↦ᵢ #false -∗
(l ↦ᵢ #true -∗ {E1;Δ;Γ} ⊨ fill K (#()) ≤log≤ t : τ) -∗
{E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
(l ↦ᵢ #true -∗ {Δ;Γ} ⊨ fill K (#()) ≤log≤ t : τ) -∗
{Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
Proof.
iIntros "Hl Hlog".
unfold acquire. unlock.
......@@ -202,8 +200,8 @@ Section lock_rules_r.
Lemma bin_log_related_acquire_fail_l Γ K l t τ :
l ↦ᵢ #true -∗
(l ↦ᵢ #false -∗ {E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ) -∗
{E1;Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
(l ↦ᵢ #false -∗ {Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ) -∗
{Δ;Γ} ⊨ fill K (acquire #l) ≤log≤ t : τ.
Proof.
iIntros "Hl Hlog".
iLöb as "IH".
......@@ -222,10 +220,10 @@ Section lock_rules_r.
Transparent release.
Lemma bin_log_related_release_r Γ K l t τ (b : bool)
(Hcl : nclose specN ⊆ E1) :
(Hcl : nclose specN ⊆ E) :
l ↦ₛ #b -∗
(l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (release #l) : τ.
(l ↦ₛ #false -∗ {E;Δ;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
{E;Δ;Γ} ⊨ t ≤log≤ fill K (release #l) : τ.
Proof.
iIntros "Hl Hlog".
unfold release. unlock.
......@@ -236,36 +234,4 @@ Section lock_rules_r.
Global Opaque release.
Lemma bin_log_related_with_lock_r Γ K Q e ev ew cl v w l t τ :
(to_val e = Some cl) →
(to_val ev = Some v) →
(to_val ew = Some w) →
(nclose specN ⊆ E1) →
(∀ K, (Q -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗
l ↦ₛ #false -∗
(Q -∗ l ↦ₛ #false -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (with_lock e #l ew) : τ.
Proof.
iIntros (????) "HA Hl Hlog".
rel_bind_r (with_lock e).
unfold with_lock. unlock. (*TODO: unlock here needed *)
iApply (bin_log_related_rec_r); eauto. simpl_subst.
rel_bind_r (App _ (# l)).
iApply (bin_log_related_rec_r); eauto. simpl_subst.
iApply (bin_log_related_rec_r); eauto. simpl_subst.
rel_bind_r (App acquire (# l)).
iApply (bin_log_related_acquire_r Γ (_ :: K) l with "Hl"); auto.
iIntros "Hl". simpl.
iApply (bin_log_related_rec_r); eauto. simpl_subst/=.
rel_bind_r (App e ew).
iApply "HA". iIntros "HQ". simpl.
iApply (bin_log_related_rec_r); eauto. simpl_subst.
rel_bind_r (App release _).
iApply (bin_log_related_release_r with "Hl"); eauto.
iIntros "Hl". simpl.
iApply (bin_log_related_rec_r); eauto. simpl_subst.
iApply ("Hlog" with "HQ Hl").
Qed.
End lock_rules_r.
theories/examples/or.v
View file @ ed2a50a1
......@@ -34,24 +34,22 @@ Hint Resolve or_type : typeable.
Section contents.
Context `{logrelG Σ}.
Lemma bin_log_related_or Δ Γ E e1 e2 e1' e2' :
↑logrelN ⊆ E →
{E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ or e1 e2 ≤log≤ or e1' e2' : TUnit.
Lemma bin_log_related_or Δ Γ e1 e2 e1' e2' :
{Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ or e1 e2 ≤log≤ or e1' e2' : TUnit.
Proof.
iIntros (?) "He1 He2".
iIntros "He1 He2".
iApply (bin_log_related_app with "[He1] He2").
iApply (bin_log_related_app with "[] He1").
iApply binary_fundamental_masked; eauto with typeable.
iApply binary_fundamental; eauto with typeable.
Qed.
Lemma bin_log_or_choice_1_r_val Δ Γ E (v1 v1' v2 : val) :
↑logrelN ⊆ E →
{E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1' v2 : TUnit.
Lemma bin_log_or_choice_1_r_val Δ Γ (v1 v1' v2 : val) :
{Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ v1 #() ≤log≤ or v1' v2 : TUnit.
Proof.
iIntros (?) "Hlog".
iIntros "Hlog".
unlock or. repeat rel_rec_r.
rel_alloc_r as x "Hx".
repeat rel_let_r.
......@@ -61,22 +59,20 @@ Section contents.
iApply bin_log_related_unit.
Qed.
Lemma bin_log_or_choice_1_r_val_typed Δ Γ E (v1 v2 : val) :
↑logrelN ⊆ E →
Lemma bin_log_or_choice_1_r_val_typed Δ Γ (v1 v2 : val) :
Γ ⊢ₜ v1 : TArrow TUnit TUnit →
{E;Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit.
{Δ;Γ} ⊨ v1 #() ≤log≤ or v1 v2 : TUnit.
Proof.
iIntros (??).
iIntros (?).
iApply bin_log_or_choice_1_r_val; eauto.
iApply binary_fundamental_masked; eauto with typeable.
iApply binary_fundamental; eauto with typeable.
Qed.
Lemma bin_log_or_choice_1_r Δ Γ E (e1 e1' : expr) (v2 : val) :
↑logrelN ⊆ E →
{E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ e1 #() ≤log≤ or e1' v2 : TUnit.
Lemma bin_log_or_choice_1_r Δ Γ (e1 e1' : expr) (v2 : val) :
{Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ e1 #() ≤log≤ or e1' v2 : TUnit.
Proof.
iIntros (?) "Hlog".
iIntros "Hlog".
rel_bind_l e1.
rel_bind_r e1'.
iApply (related_bind with "Hlog").
......@@ -86,19 +82,18 @@ Section contents.
iApply interp_ret; eauto using to_of_val.
Qed.
Lemma bin_log_or_choice_1_r_body Δ Γ E (e1 : expr) (v2 : val) :
↑logrelN ⊆ E →
Lemma bin_log_or_choice_1_r_body Δ Γ (e1 : expr) (v2 : val) :
Closed ∅ e1 →
Γ ⊢ₜ e1 : TUnit →
{E;Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit.
{Δ;Γ} ⊨ e1 ≤log≤ or (λ: <>, e1) v2 : TUnit.
Proof.
iIntros (???).
iIntros (??).
unlock or. repeat rel_rec_r.
rel_alloc_r as x "Hx".
repeat rel_let_r.
rel_fork_r as j "Hj". rel_seq_r.
rel_load_r. repeat (rel_pure_r _).
iApply binary_fundamental_masked; eauto with typeable.
iApply binary_fundamental; eauto with typeable.
Qed.
Definition or_inv x : iProp Σ :=
......@@ -115,14 +110,12 @@ Section contents.
(iMod ("Hcl" with "[-]"); first close_shoot); eauto.
Qed.
Lemma bin_log_or_commute Δ Γ E (v1 v1' v2 v2' : val) :
↑orN ⊆ E →
↑logrelN ⊆ E →
{E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1' v2' : TUnit.
Lemma bin_log_or_commute Δ Γ (v1 v1' v2 v2' : val) :
{Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ or v2 v1 ≤log≤ or v1' v2' : TUnit.
Proof.
iIntros (??) "Hv1 Hv2".
iIntros "Hv1 Hv2".
unlock or. repeat rel_rec_r. repeat rel_rec_l.
rel_alloc_l as x "Hx".
rel_alloc_r as y "Hy".
......@@ -153,33 +146,29 @@ Section contents.
iApply bin_log_related_unit.
Qed.
Lemma bin_log_or_idem_r Δ Γ E (v v' : val) :
↑logrelN ⊆ E →
{E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
{E;Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit.
Lemma bin_log_or_idem_r Δ Γ (v v' : val) :
{Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗
{Δ;Γ} ⊨ v #() ≤log≤ or v' v' : TUnit.
Proof.
iIntros (?) "Hlog".
iIntros "Hlog".
by iApply bin_log_or_choice_1_r_val.
Qed.
Lemma bin_log_or_idem_r_body Δ Γ E e :
Lemma bin_log_or_idem_r_body Δ Γ e :
Closed ∅ e →
↑logrelN ⊆ E →
Γ ⊢ₜ e : TUnit →
{E;Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit.
{Δ;Γ} ⊨ e ≤log≤ or (λ: <>, e) (λ: <>, e) : TUnit.
Proof.