From fcd5c1de2275acb01f1d1b68470b1bea6f46cea6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 4 Jun 2019 08:26:54 +0200
Subject: [PATCH] =?UTF-8?q?Get=20rid=20of=20`=CF=81`=20argument=20of=20`sp?=
=?UTF-8?q?ec=5Fctx`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
.../logrel/F_mu_ref_conc/examples/counter.v | 30 ++--
theories/logrel/F_mu_ref_conc/examples/fact.v | 22 +--
theories/logrel/F_mu_ref_conc/examples/lock.v | 30 ++--
.../F_mu_ref_conc/examples/stack/CG_stack.v | 68 ++++-----
.../F_mu_ref_conc/examples/stack/refinement.v | 14 +-
.../logrel/F_mu_ref_conc/fundamental_binary.v | 134 +++++++++---------
theories/logrel/F_mu_ref_conc/rules_binary.v | 107 +++++++-------
.../logrel/F_mu_ref_conc/soundness_binary.v | 6 +-
8 files changed, 208 insertions(+), 203 deletions(-)
diff --git a/theories/logrel/F_mu_ref_conc/examples/counter.v b/theories/logrel/F_mu_ref_conc/examples/counter.v
index 58eb5906..7c4eaa75 100644
--- a/theories/logrel/F_mu_ref_conc/examples/counter.v
+++ b/theories/logrel/F_mu_ref_conc/examples/counter.v
@@ -60,21 +60,21 @@ Section CG_Counter.
Hint Rewrite CG_increment_subst : autosubst.
- Lemma steps_CG_increment E Ï j K x n:
+ Lemma steps_CG_increment E j K x n:
nclose specN ⊆ E →
- spec_ctx Ï âˆ— x ↦ₛ (#nv n) ∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit)
+ spec_ctx ∗ x ↦ₛ (#nv n) ∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (S n)).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
- iMod (step_load _ _ j ((BinOpRCtx _ (#nv _) :: StoreRCtx (LocV _) :: K))
+ iMod (step_load _ j ((BinOpRCtx _ (#nv _) :: StoreRCtx (LocV _) :: K))
_ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
{ iFrame "Hspec Hj"; trivial. }
simpl.
- iMod (do_step_pure _ _ _ ((StoreRCtx (LocV _)) :: K) with "[$Hj]") as "Hj";
+ iMod (do_step_pure _ _ ((StoreRCtx (LocV _)) :: K) with "[$Hj]") as "Hj";
eauto.
simpl.
- iMod (step_store _ _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
+ iMod (step_store _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
iModIntro; iFrame.
Qed.
@@ -108,15 +108,15 @@ Section CG_Counter.
Hint Rewrite CG_locked_increment_subst : autosubst.
- Lemma steps_CG_locked_increment E Ï j K x n l :
+ Lemma steps_CG_locked_increment E j K x n l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— x ↦ₛ (#nv n) ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
={E}=∗ j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
iMod (steps_with_lock
- _ _ j K _ _ _ _ UnitV UnitV with "[$Hj Hx $Hl]") as "Hj"; eauto.
+ _ j K _ _ _ _ UnitV UnitV with "[$Hj Hx $Hl]") as "Hj"; eauto.
- iIntros (K') "[#Hspec Hxj]".
iApply steps_CG_increment; by try iFrame.
- by iFrame.
@@ -151,16 +151,16 @@ Section CG_Counter.
Hint Rewrite counter_read_subst : autosubst.
- Lemma steps_counter_read E Ï j K x n :
+ Lemma steps_counter_read E j K x n :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— x ↦ₛ (#nv n)
+ spec_ctx ∗ x ↦ₛ (#nv n)
∗ j ⤇ fill K (App (counter_read (Loc x)) Unit)
={E}=∗ j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (step_load _ _ j K with "[$Hj Hx]") as "[Hj Hx]"; eauto.
+ iMod (step_load _ j K with "[$Hj Hx]") as "[Hj Hx]"; eauto.
by iFrame.
Qed.
@@ -247,17 +247,17 @@ Section CG_Counter.
Lemma FG_CG_counter_refinement :
[] ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
- iIntros (Δ [|??] Ï ?) "#(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
+ iIntros (Δ [|??] ?) "#(Hspec & HΓ)"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter.
iApply fupd_wp.
- iMod (steps_newlock _ _ j (LetInCtx _ :: K) with "[$Hj]")
+ iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
as (l) "[Hj Hl]"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (step_alloc _ _ j (LetInCtx _ :: K) with "[$Hj]")
+ iMod (step_alloc _ j (LetInCtx _ :: K) with "[$Hj]")
as (cnt') "[Hj Hcnt']"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
@@ -308,7 +308,7 @@ Section CG_Counter.
+ (* CAS succeeds *)
(* In this case, we perform increment in the coarse-grained one *)
iMod (steps_CG_locked_increment
- _ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
+ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply (wp_cas_suc with "[Hcnt]"); auto.
iModIntro. iNext. iIntros "Hcnt".
diff --git a/theories/logrel/F_mu_ref_conc/examples/fact.v b/theories/logrel/F_mu_ref_conc/examples/fact.v
index 5ef328cc..d39e9d8d 100644
--- a/theories/logrel/F_mu_ref_conc/examples/fact.v
+++ b/theories/logrel/F_mu_ref_conc/examples/fact.v
@@ -68,7 +68,7 @@ Section fact_equiv.
Lemma fact_fact_acc_refinement :
[] ⊨ fact ≤log≤ fact_acc : (TArrow TNat TNat).
Proof.
- iIntros (? vs Ï _) "[#HE HΔ]".
+ iIntros (? vs _) "[#HE HΔ]".
iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
iClear "HΔ". simpl.
iIntros (j K) "Hj"; simpl.
@@ -87,7 +87,7 @@ Section fact_equiv.
- iApply wp_pure_step_later; auto.
iNext; simpl; asimpl.
rewrite fact_acc_body_unfold.
- iMod (do_step_pure _ _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
rewrite -fact_acc_body_unfold.
simpl; asimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
@@ -95,7 +95,7 @@ Section fact_equiv.
iApply wp_pure_step_later; auto.
iNext; simpl.
iApply wp_value. simpl.
- iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
simpl.
iApply wp_pure_step_later; auto.
iNext; simpl.
@@ -106,7 +106,7 @@ Section fact_equiv.
- iApply wp_pure_step_later; auto.
iNext; simpl; asimpl.
rewrite fact_acc_body_unfold.
- iMod (do_step_pure _ _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
rewrite -fact_acc_body_unfold.
simpl; asimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
@@ -114,7 +114,7 @@ Section fact_equiv.
iApply wp_pure_step_later; auto.
iNext; simpl.
iApply wp_value. simpl.
- iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
simpl.
iApply wp_pure_step_later; auto.
iNext; simpl.
@@ -124,11 +124,11 @@ Section fact_equiv.
iApply (wp_bind (fill [AppRCtx (RecV _)])).
iApply wp_pure_step_later; auto.
iNext; simpl; iApply wp_value; simpl.
- iMod (do_step_pure _ _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
asimpl.
- iMod (do_step_pure _ _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
asimpl.
@@ -146,7 +146,7 @@ Section fact_equiv.
Lemma fact_acc_fact_refinement :
[] ⊨ fact_acc ≤log≤ fact : (TArrow TNat TNat).
Proof.
- iIntros (? vs Ï _) "[#HE HΔ]".
+ iIntros (? vs _) "[#HE HΔ]".
iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
iClear "HΔ". simpl.
iIntros (j K) "Hj"; simpl.
@@ -173,7 +173,7 @@ Section fact_equiv.
iNext; simpl; asimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
simpl; asimpl.
- iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
iApply (wp_bind (fill [IfCtx _ _])).
iApply wp_pure_step_later; auto.
iNext; simpl.
@@ -198,12 +198,12 @@ Section fact_equiv.
iApply wp_pure_step_later; auto.
iNext; simpl.
iApply wp_value. simpl.
- iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+ iMod (do_step_pure _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
simpl.
iApply wp_pure_step_later; auto.
iNext; simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
- iMod (do_step_pure _ _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
+ iMod (do_step_pure _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
with "[$Hj]") as "Hj"; eauto.
simpl.
iApply (wp_bind (fill [LetInCtx _])).
diff --git a/theories/logrel/F_mu_ref_conc/examples/lock.v b/theories/logrel/F_mu_ref_conc/examples/lock.v
index ba8a8a91..7c3d8ed5 100644
--- a/theories/logrel/F_mu_ref_conc/examples/lock.v
+++ b/theories/logrel/F_mu_ref_conc/examples/lock.v
@@ -84,29 +84,29 @@ Section proof.
Context `{cfgSG Σ}.
Context `{heapIG Σ}.
- Lemma steps_newlock E Ï j K :
+ Lemma steps_newlock E j K :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K newlock
+ spec_ctx ∗ j ⤇ fill K newlock
⊢ |={E}=> ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec Hj]".
- by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
+ by iMod (step_alloc _ j K with "[Hj]") as "Hj"; eauto.
Qed.
Typeclasses Opaque newlock.
Global Opaque newlock.
- Lemma steps_acquire E Ï j K l :
+ Lemma steps_acquire E j K l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— l ↦ₛ (#â™v false) ∗ j ⤇ fill K (App acquire (Loc l))
+ spec_ctx ∗ l ↦ₛ (#â™v false) ∗ j ⤇ fill K (App acquire (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#â™v true).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
- iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
- iMod (step_cas_suc _ _ j ((IfCtx _ _) :: K)
+ iMod (step_rec _ j K with "[Hj]") as "Hj"; eauto. done.
+ iMod (step_cas_suc _ j ((IfCtx _ _) :: K)
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
{ simpl. iFrame "Hspec Hj Hl"; eauto. }
- iMod (step_if_true _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
+ iMod (step_if_true _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
{ by iFrame. }
by iIntros "!> {$Hj $Hl}".
Unshelve. all:trivial.
@@ -115,9 +115,9 @@ Section proof.
Typeclasses Opaque acquire.
Global Opaque acquire.
- Lemma steps_release E Ï j K l b:
+ Lemma steps_release E j K l b:
nclose specN ⊆ E →
- spec_ctx Ï âˆ— l ↦ₛ (#â™v b) ∗ j ⤇ fill K (App release (Loc l))
+ spec_ctx ∗ l ↦ₛ (#â™v b) ∗ j ⤇ fill K (App release (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
@@ -129,26 +129,26 @@ Section proof.
Typeclasses Opaque release.
Global Opaque release.
- Lemma steps_with_lock E Ï j K e l P Q v w:
+ Lemma steps_with_lock E j K e l P Q v w:
nclose specN ⊆ E →
(* (∀ f, e.[f] = e) (* e is a closed term *) → *)
- (∀ K', spec_ctx Ï âˆ— P ∗ j ⤇ fill K' (App e (of_val w))
+ (∀ K', spec_ctx ∗ P ∗ j ⤇ fill K' (App e (of_val w))
⊢ |={E}=> j ⤇ fill K' (of_val v) ∗ Q) →
- spec_ctx Ï âˆ— P ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ P ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE He) "[#Hspec [HP [Hl Hj]]]".
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (steps_acquire _ _ j (SeqCtx _ :: K) with "[$Hj Hl]") as "[Hj Hl]";
+ iMod (steps_acquire _ j (SeqCtx _ :: K) with "[$Hj Hl]") as "[Hj Hl]";
auto. simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iMod (He (LetInCtx _ :: K) with "[$Hj HP]") as "[Hj HQ]"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (steps_release _ _ j (SeqCtx _ :: K) _ _ with "[$Hj $Hl]")
+ iMod (steps_release _ j (SeqCtx _ :: K) _ _ with "[$Hj $Hl]")
as "[Hj Hl]"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
index d6a5b42b..07444d11 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
@@ -81,18 +81,18 @@ Section CG_Stack.
Hint Rewrite CG_push_subst : autosubst.
- Lemma steps_CG_push E Ï j K st v w :
+ Lemma steps_CG_push E j K st v w :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ v ∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w))
+ spec_ctx ∗ st ↦ₛ v ∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (step_load _ _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
+ iMod (step_load _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
simpl.
- iMod (step_store _ _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
+ iMod (step_store _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
{ rewrite /= !to_of_val //. }
iModIntro. by iFrame.
Qed.
@@ -124,14 +124,14 @@ Section CG_Stack.
Hint Rewrite CG_locked_push_subst : autosubst.
- Lemma steps_CG_locked_push E Ï j K st w v l :
+ Lemma steps_CG_locked_push E j K st w v l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ v ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ st ↦ₛ v ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#â™v false).
Proof.
intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
- iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]")
+ iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]")
as "Hj"; auto.
iIntros (K') "[#Hspec Hxj]".
iApply steps_CG_push; first done. by iFrame.
@@ -164,46 +164,46 @@ Section CG_Stack.
Hint Rewrite CG_pop_subst : autosubst.
- Lemma steps_CG_pop_suc E Ï j K st v w :
+ Lemma steps_CG_pop_suc E j K st v w :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ FoldV (InjRV (PairV w v)) ∗
+ spec_ctx ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗
j ⤇ fill K (App (CG_pop (Loc st)) Unit)
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v.
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (step_load _ _ _ (UnfoldCtx :: CaseCtx _ _ :: K) with "[$Hj $Hx]")
+ iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K) with "[$Hj $Hx]")
as "[Hj Hx]"; eauto.
simpl.
- iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (do_step_pure _ _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K)
+ iMod (do_step_pure _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K)
with "[$Hj]") as "Hj"; eauto.
simpl.
- iMod (step_store _ _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]";
+ iMod (step_store _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]";
eauto using to_of_val.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
- iMod (do_step_pure _ _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
by iFrame "Hj Hx".
Qed.
- Lemma steps_CG_pop_fail E Ï j K st :
+ Lemma steps_CG_pop_fail E j K st :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ FoldV (InjLV UnitV) ∗
+ spec_ctx ∗ st ↦ₛ FoldV (InjLV UnitV) ∗
j ⤇ fill K (App (CG_pop (Loc st)) Unit)
⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K)
+ iMod (step_load _ j (UnfoldCtx :: CaseCtx _ _ :: K)
_ _ _ with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
- iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
by iFrame "Hj Hx"; trivial.
@@ -237,28 +237,28 @@ Section CG_Stack.
Hint Rewrite CG_locked_pop_subst : autosubst.
- Lemma steps_CG_locked_pop_suc E Ï j K st v w l :
+ Lemma steps_CG_locked_pop_suc E j K st v w l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
- iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
+ iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
_ (InjRV w) UnitV
with "[$Hj $Hx $Hl]") as "Hj"; eauto.
iIntros (K') "[#Hspec Hxj]".
iApply steps_CG_pop_suc; eauto.
Qed.
- Lemma steps_CG_locked_pop_fail E Ï j K st l :
+ Lemma steps_CG_locked_pop_fail E j K st l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
- iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _
+ iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _
(InjLV UnitV) UnitV
with "[$Hj $Hx $Hl]") as "Hj"; eauto.
iIntros (K') "[#Hspec Hxj] /=".
@@ -293,14 +293,14 @@ Section CG_Stack.
Hint Rewrite CG_snap_subst : autosubst.
- Lemma steps_CG_snap E Ï j K st v l :
+ Lemma steps_CG_snap E j K st v l :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— st ↦ₛ v ∗ l ↦ₛ (#â™v false)
+ spec_ctx ∗ st ↦ₛ v ∗ l ↦ₛ (#â™v false)
∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#â™v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
- iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV
+ iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV
with "[$Hj $Hx $Hl]") as "Hj"; eauto.
iIntros (K') "[#Hspec [Hx Hj]]".
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
@@ -353,9 +353,9 @@ Section CG_Stack.
Hint Rewrite CG_iter_subst : autosubst.
- Lemma steps_CG_iter E Ï j K f v w :
+ Lemma steps_CG_iter E j K f v w :
nclose specN ⊆ E →
- spec_ctx Ï
+ spec_ctx
∗ j ⤇ fill K (App (CG_iter (of_val f))
(Fold (InjR (Pair (of_val w) (of_val v)))))
⊢ |={E}=>
@@ -366,22 +366,22 @@ Section CG_Stack.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
iAsimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iAsimpl.
- iMod (do_step_pure _ _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]")
+ iMod (do_step_pure _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]")
as "Hj"; eauto.
Qed.
- Lemma steps_CG_iter_end E Ï j K f :
+ Lemma steps_CG_iter_end E j K f :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
+ spec_ctx ∗ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
⊢ |={E}=> j ⤇ fill K Unit.
Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
- iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
iAsimpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
index 2c4883bc..998a8e72 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
@@ -20,7 +20,7 @@ Section Stack_refinement.
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
(* executing the preambles *)
- iIntros (Δ [|??] Ï ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first.
+ iIntros (Δ [|??] ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
@@ -29,11 +29,11 @@ Section Stack_refinement.
clear j K. iAlways. iIntros (Ï„i) "%". iIntros (j K) "Hj /=".
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
iApply wp_pure_step_later; auto. iNext.
- iMod (steps_newlock _ _ j (LetInCtx _ :: K) with "[$Hj]")
+ iMod (steps_newlock _ j (LetInCtx _ :: K) with "[$Hj]")
as (l) "[Hj Hl]"; eauto.
- iMod (do_step_pure _ _ j K with "[$Hj]") as "Hj"; eauto.
+ iMod (do_step_pure _ j K with "[$Hj]") as "Hj"; eauto.
simpl. iAsimpl.
- iMod (step_alloc _ _ j (LetInCtx _ :: K) with "[$Hj]")
+ iMod (step_alloc _ j (LetInCtx _ :: K) with "[$Hj]")
as (stk') "[Hj Hstk']"; eauto.
simpl.
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
@@ -110,7 +110,7 @@ Section Stack_refinement.
* (* CAS succeeds *)
(* In this case, the specification pushes *)
iMod "Hstk'". iMod "Hl".
- iMod (steps_CG_locked_push _ _ j K with "[Hj Hl Hstk']")
+ iMod (steps_CG_locked_push _ j K with "[Hj Hl Hstk']")
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
{ rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
iApply (wp_cas_suc with "Hstk"); auto.
@@ -250,7 +250,7 @@ Section Stack_refinement.
iApply (wp_bind (fill [FoldCtx; AppRCtx _])); iApply wp_wand_l;
iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iInv stackN as (istk3 w h) "[Hoe [>Hstk' [>Hstk [#HLK >Hl]]]]" "Hclose".
- iMod (steps_CG_snap _ _ _ (AppRCtx _ :: K)
+ iMod (steps_CG_snap _ _ (AppRCtx _ :: K)
with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]"; first solve_ndisj.
{ rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". }
iApply (wp_load with "[$Hstk]"). iNext. iIntros "Hstk".
@@ -308,7 +308,7 @@ Section Stack_refinement.
iAsimpl.
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val).
- iMod (step_snd _ _ _ (AppRCtx _ :: K) with "[$Hspec Hj]") as "Hj";
+ iMod (step_snd _ _ (AppRCtx _ :: K) with "[$Hspec Hj]") as "Hj";
[| | |simpl; by iFrame "Hj"|]; rewrite ?to_of_val; auto.
iApply wp_pure_step_later; trivial.
iNext. simpl.
diff --git a/theories/logrel/F_mu_ref_conc/fundamental_binary.v b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
index cb8a0fd8..b683aa59 100644
--- a/theories/logrel/F_mu_ref_conc/fundamental_binary.v
+++ b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
@@ -8,9 +8,9 @@ Section bin_log_def.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
- Definition bin_log_related (Γ : list type) (e e' : expr) (Ï„ : type) := ∀ Δ vvs Ï,
+ Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) := ∀ Δ vvs,
env_Persistent Δ →
- spec_ctx Ï âˆ§
+ spec_ctx ∧
⟦ Γ ⟧* Δ vvs ⊢ ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)]).
End bin_log_def.
@@ -32,13 +32,13 @@ Section fundamental.
iIntros (v); iDestruct 1 as (w) Hv; simpl.
(* Put all quantifiers at the outer level *)
- Lemma bin_log_related_alt {Γ e e' Ï„} : Γ ⊨ e ≤log≤ e' : Ï„ → ∀ Δ vvs Ï j K,
+ Lemma bin_log_related_alt {Γ e e' τ} : Γ ⊨ e ≤log≤ e' : τ → ∀ Δ vvs j K,
env_Persistent Δ →
- spec_ctx Ï âˆ— ⟦ Γ ⟧* Δ vvs ∗ j ⤇ fill K (e'.[env_subst (vvs.*2)])
+ spec_ctx ∗ ⟦ Γ ⟧* Δ vvs ∗ j ⤇ fill K (e'.[env_subst (vvs.*2)])
⊢ WP e.[env_subst (vvs.*1)] {{ v, ∃ v',
j ⤇ fill K (of_val v') ∗ interp τ Δ (v, v') }}.
Proof.
- iIntros (Hlog Δ vvs Ï j K ?) "(#Hs & HΓ & Hj)".
+ iIntros (Hlog Δ vvs j K ?) "(#Hs & HΓ & Hj)".
iApply (Hlog with "[HΓ]"); iFrame; eauto.
Qed.
@@ -47,7 +47,7 @@ Section fundamental.
Lemma bin_log_related_var Γ x τ :
Γ !! x = Some τ → Γ ⊨ Var x ≤log≤ Var x : τ.
Proof.
- iIntros (? Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (? Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Heq ?]"; first done.
iDestruct "Heq" as %Heq.
erewrite !env_subst_lookup; rewrite ?list_lookup_fmap ?Heq; eauto.
@@ -56,19 +56,19 @@ Section fundamental.
Lemma bin_log_related_unit Γ : Γ ⊨ Unit ≤log≤ Unit : TUnit.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists UnitV; eauto.
Qed.
Lemma bin_log_related_nat Γ n : Γ ⊨ #n n ≤log≤ #n n : TNat.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists (#nv _); eauto.
Qed.
Lemma bin_log_related_bool Γ b : Γ ⊨ #♠b ≤log≤ #♠b : TBool.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists (#â™v _); eauto.
Qed.
@@ -77,11 +77,11 @@ Section fundamental.
(IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) :
Γ ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (PairLCtx e2.[env_subst _]) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((PairLCtx e2'.[env_subst _]) :: K)).
+ ('`IHHtyped1 _ _ j ((PairLCtx e2'.[env_subst _]) :: K)).
smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]"
- ('`IHHtyped2 _ _ _ j ((PairRCtx v') :: K)).
+ ('`IHHtyped2 _ _ j ((PairRCtx v') :: K)).
iApply wp_value. iExists (PairV v' w'); iFrame "Hw".
iExists (v, v'), (w, w'); simpl; repeat iSplit; trivial.
Qed.
@@ -90,8 +90,8 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) :
Γ ⊨ Fst e ≤log≤ Fst e' : τ1.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
- smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (FstCtx :: K)); cbn.
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ j (FstCtx :: K)); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_pure_step_later; eauto. iNext.
iMod (step_fst with "[Hs Hv]") as "Hw"; eauto.
@@ -102,8 +102,8 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) :
Γ ⊨ Snd e ≤log≤ Snd e' : τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
- smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (SndCtx :: K)); cbn.
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ j (SndCtx :: K)); cbn.
iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq.
iApply wp_pure_step_later; eauto. iNext.
iMod (step_snd with "[Hs Hv]") as "Hw"; eauto.
@@ -114,9 +114,9 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : τ1) :
Γ ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2).
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
- ('`IHHtyped _ _ _ j (InjLCtx :: K)); cbn.
+ ('`IHHtyped _ _ j (InjLCtx :: K)); cbn.
iApply wp_value. iExists (InjLV v'); iFrame "Hv".
iLeft; iExists (_,_); eauto 10.
Qed.
@@ -125,9 +125,9 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : τ2) :
Γ ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
- ('`IHHtyped _ _ _ j (InjRCtx :: K)); cbn.
+ ('`IHHtyped _ _ j (InjRCtx :: K)); cbn.
iApply wp_value. iExists (InjRV v'); iFrame "Hv".
iRight; iExists (_,_); eauto 10.
Qed.
@@ -142,10 +142,10 @@ Section fundamental.
(IHHtyped3 : τ2 :: Γ ⊨ e2 ≤log≤ e2' : τ3) :
Γ ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iDestruct (interp_env_length with "HΓ") as %?.
smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((CaseCtx _ _) :: K)); cbn.
+ ('`IHHtyped1 _ _ j ((CaseCtx _ _) :: K)); cbn.
iDestruct "Hiv" as "[Hiv|Hiv]";
iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq.
- iApply fupd_wp.
@@ -168,14 +168,14 @@ Section fundamental.
(IHHtyped3 : Γ ⊨ e2 ≤log≤ e2' : τ) :
Γ ⊨ If e0 e1 e2 ≤log≤ If e0' e1' e2' : τ.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((IfCtx _ _) :: K)); cbn.
+ ('`IHHtyped1 _ _ j ((IfCtx _ _) :: K)); cbn.
iDestruct "Hiv" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
- - iMod (step_if_true _ _ j K with "[-]") as "Hz"; eauto.
+ - iMod (step_if_true _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. iModIntro. iNext.
iApply '`IHHtyped2; eauto.
- - iMod (step_if_false _ _ j K with "[-]") as "Hz"; eauto.
+ - iMod (step_if_false _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto.
iModIntro. iNext. iApply '`IHHtyped3; eauto.
Qed.
@@ -185,15 +185,15 @@ Section fundamental.
(IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : TNat) :
Γ ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (BinOpLCtx _ _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((BinOpLCtx _ _) :: K)); cbn.
+ ('`IHHtyped1 _ _ j ((BinOpLCtx _ _) :: K)); cbn.
smart_wp_bind (BinOpRCtx _ _) w w' "[Hw #Hiw]"
- ('`IHHtyped2 _ _ _ j ((BinOpRCtx _ _) :: K)); cbn.
+ ('`IHHtyped2 _ _ j ((BinOpRCtx _ _) :: K)); cbn.
iDestruct "Hiv" as (n) "[% %]"; simplify_eq/=.
iDestruct "Hiw" as (n') "[% %]"; simplify_eq/=.
iApply fupd_wp.
- iMod (step_nat_binop _ _ j K with "[-]") as "Hz"; eauto.
+ iMod (step_nat_binop _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. iModIntro. iNext.
iApply wp_value. iExists _; iSplitL; eauto.
destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
@@ -206,13 +206,13 @@ Section fundamental.
(IHHtyped : TArrow τ1 τ2 :: τ1 :: Γ ⊨ e ≤log≤ e' : τ2) :
Γ ⊨ Rec e ≤log≤ Rec e' : TArrow τ1 τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists (RecV _). iIntros "{$Hj} !#".
iLöb as "IH". iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
iApply fupd_wp.
- iMod (step_rec _ _ j' K' _ (of_val v') v' with "[-]") as "Hz"; eauto.
+ iMod (step_rec _ j' K' _ (of_val v') v' with "[-]") as "Hz"; eauto.
asimpl. change (Rec ?e) with (of_val (RecV e)).
iApply ('`IHHtyped _ ((_,_) :: (v,v') :: vvs)); repeat iSplit; eauto.
iModIntro.
@@ -225,13 +225,13 @@ Section fundamental.
(IHHtyped : τ1 :: Γ ⊨ e ≤log≤ e' : τ2) :
Γ ⊨ Lam e ≤log≤ Lam e' : TArrow τ1 τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists (LamV _). iIntros "{$Hj} !#".
iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
iDestruct (interp_env_length with "HΓ") as %?.
iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
iApply fupd_wp.
- iMod (step_lam _ _ j' K' _ (of_val v') v' with "[-]") as "Hz"; eauto.
+ iMod (step_lam _ j' K' _ (of_val v') v' with "[-]") as "Hz"; eauto.
asimpl. iFrame "#". change (Lam ?e) with (of_val (LamV e)).
iApply ('`IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto.
iModIntro.
@@ -245,11 +245,11 @@ Section fundamental.
(IHHtyped2 : τ1 :: Γ ⊨ e2 ≤log≤ e2' : τ2) :
Γ ⊨ LetIn e1 e2 ≤log≤ LetIn e1' e2': τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iDestruct (interp_env_length with "HΓ") as %?.
smart_wp_bind (LetInCtx _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((LetInCtx _) :: K)); cbn.
- iMod (step_letin _ _ j K with "[-]") as "Hz"; eauto.
+ ('`IHHtyped1 _ _ j ((LetInCtx _) :: K)); cbn.
+ iMod (step_letin _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. iModIntro.
asimpl.
iApply ('`IHHtyped2 _ ((v, v') :: vvs)); repeat iSplit; eauto.
@@ -261,11 +261,11 @@ Section fundamental.
(IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) :
Γ ⊨ Seq e1 e2 ≤log≤ Seq e1' e2': τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iDestruct (interp_env_length with "HΓ") as %?.
smart_wp_bind (SeqCtx _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((SeqCtx _) :: K)); cbn.
- iMod (step_seq _ _ j K with "[-]") as "Hz"; eauto.
+ ('`IHHtyped1 _ _ j ((SeqCtx _) :: K)); cbn.
+ iMod (step_seq _ j K with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto. iModIntro.
asimpl.
iApply '`IHHtyped2; repeat iSplit; eauto.
@@ -276,11 +276,11 @@ Section fundamental.
(IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ1) :
Γ ⊨ App e1 e2 ≤log≤ App e1' e2' : τ2.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j (((AppLCtx (e2'.[env_subst (vvs.*2)]))) :: K)); cbn.
+ ('`IHHtyped1 _ _ j (((AppLCtx (e2'.[env_subst (vvs.*2)]))) :: K)); cbn.
smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
- ('`IHHtyped2 _ _ _ j ((AppRCtx v') :: K)); cbn.
+ ('`IHHtyped2 _ _ j ((AppRCtx v') :: K)); cbn.
iApply ("Hiv" $! (w, w') with "Hiw"); simpl; eauto.
Qed.
@@ -288,12 +288,12 @@ Section fundamental.
(IHHtyped : (subst (ren (+1)) <$> Γ) ⊨ e ≤log≤ e' : τ) :
Γ ⊨ TLam e ≤log≤ TLam e' : TForall τ.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply wp_value. iExists (TLamV _).
iIntros "{$Hj} /= !#"; iIntros (Ï„i ? j' K') "Hv /=".
iApply wp_pure_step_later; auto. iNext.
iApply fupd_wp.
- iMod (step_tlam _ _ j' K' (e'.[env_subst (vvs.*2)]) with "[-]") as "Hz"; eauto.
+ iMod (step_tlam _ j' K' (e'.[env_subst (vvs.*2)]) with "[-]") as "Hz"; eauto.
iApply '`IHHtyped; repeat iSplit; eauto. iModIntro. rewrite interp_env_ren; auto.
Qed.
@@ -301,9 +301,9 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : TForall τ) :
Γ ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/].
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (TAppCtx) v v' "[Hj #Hv]"
- ('`IHHtyped _ _ _ j (TAppCtx :: K)); cbn.
+ ('`IHHtyped _ _ j (TAppCtx :: K)); cbn.
iApply wp_wand_r; iSplitL.
{ iSpecialize ("Hv" $! (interp τ' Δ) with "[#]"); [iPureIntro; apply _|].
iApply "Hv"; eauto. }
@@ -315,9 +315,9 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : τ.[(TRec τ)/]) :
Γ ⊨ Fold e ≤log≤ Fold e' : TRec τ.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply (wp_bind (fill [FoldCtx])); iApply wp_wand_l; iSplitR;
- [|iApply ('`IHHtyped _ _ _ j (FoldCtx :: K));
+ [|iApply ('`IHHtyped _ _ j (FoldCtx :: K));
simpl; repeat iSplitR; trivial].
iIntros (v); iDestruct 1 as (w) "[Hv #Hiv]".
iApply wp_value. iExists (FoldV w); iFrame "Hv".
@@ -329,16 +329,16 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : TRec τ) :
Γ ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/].
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply (wp_bind (fill [UnfoldCtx])); iApply wp_wand_l; iSplitR;
- [|iApply ('`IHHtyped _ _ _ j (UnfoldCtx :: K));
+ [|iApply ('`IHHtyped _ _ j (UnfoldCtx :: K));
simpl; repeat iSplitR; trivial].
iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]".
rewrite /= fixpoint_interp_rec1_eq /=.
change (fixpoint _) with (interp (TRec τ) Δ).
iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=.
iApply fupd_wp.
- iMod (step_Fold _ _ j K (of_val w') w' with "[-]") as "Hz"; eauto.
+ iMod (step_Fold _ j K (of_val w') w' with "[-]") as "Hz"; eauto.
iApply wp_pure_step_later; auto.
iModIntro. iApply wp_value. iNext; iExists _; iFrame "Hz".
by rewrite -interp_subst.
@@ -348,22 +348,22 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : TUnit) :
Γ ⊨ Fork e ≤log≤ Fork e' : TUnit.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
iApply fupd_wp.
- iMod (step_fork _ _ j K with "[-]") as (j') "[Hj Hj']"; eauto.
+ iMod (step_fork _ j K with "[-]") as (j') "[Hj Hj']"; eauto.
iApply wp_fork; iModIntro. rewrite -bi.later_sep. iNext; iSplitL "Hj".
- iExists UnitV; eauto.
- - iApply wp_wand_l; iSplitR; [|iApply ('`IHHtyped _ _ _ _ [])]; eauto.
+ - iApply wp_wand_l; iSplitR; [|iApply ('`IHHtyped _ _ _ [])]; eauto.
Qed.
Lemma bin_log_related_alloc Γ e e' τ
(IHHtyped : Γ ⊨ e ≤log≤ e' : τ) :
Γ ⊨ Alloc e ≤log≤ Alloc e' : Tref τ.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
- smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (AllocCtx :: K)).
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ j (AllocCtx :: K)).
iApply fupd_wp.
- iMod (step_alloc _ _ j K (of_val v') v' with "[-]") as (l') "[Hj Hl]"; eauto.
+ iMod (step_alloc _ j K (of_val v') v' with "[-]") as (l') "[Hj Hl]"; eauto.
iApply wp_atomic; eauto.
iApply wp_alloc; eauto. do 2 iModIntro. iNext.
iIntros (l) "Hl'".
@@ -377,8 +377,8 @@ Section fundamental.
(IHHtyped : Γ ⊨ e ≤log≤ e' : (Tref τ)) :
Γ ⊨ Load e ≤log≤ Load e' : τ.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
- smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ _ j (LoadCtx :: K)).
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]" ('`IHHtyped _ _ j (LoadCtx :: K)).
iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
iApply wp_atomic; eauto.
iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
@@ -398,11 +398,11 @@ Section fundamental.
(IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ) :
Γ ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((StoreLCtx _) :: K)).
+ ('`IHHtyped1 _ _ j ((StoreLCtx _) :: K)).
smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]"
- ('`IHHtyped2 _ _ _ j ((StoreRCtx _) :: K)).
+ ('`IHHtyped2 _ _ j ((StoreRCtx _) :: K)).
iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
iApply wp_atomic; eauto.
iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
@@ -423,13 +423,13 @@ Section fundamental.
(IHHtyped3 : Γ ⊨ e3 ≤log≤ e3' : τ) :
Γ ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool.
Proof.
- iIntros (Δ vvs Ï ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+ iIntros (Δ vvs ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
- ('`IHHtyped1 _ _ _ j ((CasLCtx _ _) :: K)).
+ ('`IHHtyped1 _ _ j ((CasLCtx _ _) :: K)).
smart_wp_bind (CasMCtx _ _) w w' "[Hw #Hiw]"
- ('`IHHtyped2 _ _ _ j ((CasMCtx _ _) :: K)).
+ ('`IHHtyped2 _ _ j ((CasMCtx _ _) :: K)).
smart_wp_bind (CasRCtx _ _) u u' "[Hu #Hiu]"
- ('`IHHtyped3 _ _ _ j ((CasRCtx _ _) :: K)).
+ ('`IHHtyped3 _ _ j ((CasRCtx _ _) :: K)).
iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
iApply wp_atomic; eauto.
iMod (interp_ref_open' _ _ l l' with "[]") as
diff --git a/theories/logrel/F_mu_ref_conc/rules_binary.v b/theories/logrel/F_mu_ref_conc/rules_binary.v
index 1e939ff1..7c2449c0 100644
--- a/theories/logrel/F_mu_ref_conc/rules_binary.v
+++ b/theories/logrel/F_mu_ref_conc/rules_binary.v
@@ -33,12 +33,12 @@ Section definitionsS.
Definition spec_inv (Ï : cfg F_mu_ref_conc_lang) : iProp Σ :=
(∃ tp σ, own cfg_name (◠(to_tpool tp, to_gen_heap σ))
∗ ⌜rtc erased_step Ï (tp,σ)âŒ)%I.
- Definition spec_ctx (Ï : cfg F_mu_ref_conc_lang) : iProp Σ :=
- inv specN (spec_inv Ï).
+ Definition spec_ctx : iProp Σ :=
+ (∃ Ï, inv specN (spec_inv Ï))%I.
Global Instance heapS_mapsto_timeless l q v : Timeless (heapS_mapsto l q v).
Proof. apply _. Qed.
- Global Instance spec_ctx_persistent Ï : Persistent (spec_ctx Ï).
+ Global Instance spec_ctx_persistent : Persistent spec_ctx.
Proof. apply _. Qed.
End definitionsS.
Typeclasses Opaque heapS_mapsto tpool_mapsto.
@@ -164,13 +164,14 @@ Section cfg.
exists z; split; eauto using nsteps_l.
Qed.
- Lemma step_pure' E Ï j K e e' (P : Prop) n :
+ Lemma step_pure' E j K e e' (P : Prop) n :
P →
PureExec P n e e' →
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
+ spec_ctx ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
Proof.
- iIntros (HP Hex ?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+ iIntros (HP Hex ?) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hspec".
+ rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
iDestruct "Hrtc" as %Hrtc.
iDestruct (own_valid_2 with "Hown Hj")
@@ -208,16 +209,17 @@ Section cfg.
Qed.
- Lemma do_step_pure E Ï j K e e' `{!PureExec True 1 e e'}:
+ Lemma do_step_pure E j K e e' `{!PureExec True 1 e e'}:
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
+ spec_ctx ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
Proof. by eapply step_pure'; last eauto. Qed.
- Lemma step_alloc E Ï j K e v:
+ Lemma step_alloc E j K e v:
to_val e = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
+ spec_ctx ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
Proof.
- iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
+ iIntros (??) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hinv".
+ rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
iDestruct (own_valid_2 with "Hown Hj")
@@ -235,12 +237,12 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
- Lemma step_load E Ï j K l q v:
+ Lemma step_load E j K l q v:
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v
+ spec_ctx ∗ j ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v
={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
Proof.
- iIntros (?) "(#Hinv & Hj & Hl)".
+ iIntros (?) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
@@ -256,12 +258,12 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
- Lemma step_store E Ï j K l v' e v:
+ Lemma step_store E j K l v' e v:
to_val e = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v'
+ spec_ctx ∗ j ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v'
={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ v.
Proof.
- iIntros (??) "(#Hinv & Hj & Hl)".
+ iIntros (??) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
@@ -281,12 +283,12 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
- Lemma step_cas_fail E Ï j K l q v' e1 v1 e2 v2:
+ Lemma step_cas_fail E j K l q v' e1 v1 e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → v' ≠v1 →
- spec_ctx Ï âˆ— j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ{q} v'
+ spec_ctx ∗ j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ{q} v'
={E}=∗ j ⤇ fill K (#♠false) ∗ l ↦ₛ{q} v'.
Proof.
- iIntros (????) "(#Hinv & Hj & Hl)".
+ iIntros (????) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (Ï) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
@@ -302,12 +304,12 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
- Lemma step_cas_suc E Ï j K l e1 v1 v1' e2 v2:
+ Lemma step_cas_suc E j K l e1 v1 v1' e2 v2:
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → v1 = v1' →
- spec_ctx Ï âˆ— j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ v1'
+ spec_ctx ∗ j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ v1'
={E}=∗ j ⤇ fill K (#♠true) ∗ l ↦ₛ v2.
Proof.
- iIntros (????) "(#Hinv & Hj & Hl)"; subst.
+ iIntros (????) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (Ï) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
@@ -327,83 +329,84 @@ Section cfg.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
- Lemma step_rec E Ï j K e1 e2 v :
+ Lemma step_rec E j K e1 e2 v :
to_val e2 = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (App (Rec e1) e2)
+ spec_ctx ∗ j ⤇ fill K (App (Rec e1) e2)
={E}=∗ j ⤇ fill K (e1.[Rec e1,e2/]).
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_lam E Ï j K e1 e2 v :
+ Lemma step_lam E j K e1 e2 v :
to_val e2 = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (App (Lam e1) e2)
+ spec_ctx ∗ j ⤇ fill K (App (Lam e1) e2)
={E}=∗ j ⤇ fill K (e1.[e2/]).
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_letin E Ï j K e1 e2 v :
+ Lemma step_letin E j K e1 e2 v :
to_val e1 = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (LetIn e1 e2)
+ spec_ctx ∗ j ⤇ fill K (LetIn e1 e2)
={E}=∗ j ⤇ fill K (e2.[e1/]).
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_seq E Ï j K e1 e2 v :
+ Lemma step_seq E j K e1 e2 v :
to_val e1 = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Seq e1 e2)
+ spec_ctx ∗ j ⤇ fill K (Seq e1 e2)
={E}=∗ j ⤇ fill K e2.
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_tlam E Ï j K e :
+ Lemma step_tlam E j K e :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (TApp (TLam e)) ={E}=∗ j ⤇ fill K e.
+ spec_ctx ∗ j ⤇ fill K (TApp (TLam e)) ={E}=∗ j ⤇ fill K e.
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_Fold E Ï j K e v :
+ Lemma step_Fold E j K e v :
to_val e = Some v → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Unfold (Fold e)) ={E}=∗ j ⤇ fill K e.
+ spec_ctx ∗ j ⤇ fill K (Unfold (Fold e)) ={E}=∗ j ⤇ fill K e.
Proof. by intros ?; apply: do_step_pure. Qed.
- Lemma step_fst E Ï j K e1 v1 e2 v2 :
+ Lemma step_fst E j K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ j ⤇ fill K e1.
+ spec_ctx ∗ j ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ j ⤇ fill K e1.
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_snd E Ï j K e1 v1 e2 v2 :
+ Lemma step_snd E j K e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ j ⤇ fill K e2.
+ spec_ctx ∗ j ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ j ⤇ fill K e2.
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_case_inl E Ï j K e0 v0 e1 e2 :
+ Lemma step_case_inl E j K e0 v0 e1 e2 :
to_val e0 = Some v0 → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Case (InjL e0) e1 e2)
+ spec_ctx ∗ j ⤇ fill K (Case (InjL e0) e1 e2)
={E}=∗ j ⤇ fill K (e1.[e0/]).
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_case_inr E Ï j K e0 v0 e1 e2 :
+ Lemma step_case_inr E j K e0 v0 e1 e2 :
to_val e0 = Some v0 → nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Case (InjR e0) e1 e2)
+ spec_ctx ∗ j ⤇ fill K (Case (InjR e0) e1 e2)
={E}=∗ j ⤇ fill K (e2.[e0/]).
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_if_false E Ï j K e1 e2 :
+ Lemma step_if_false E j K e1 e2 :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (If (#â™ false) e1 e2) ={E}=∗ j ⤇ fill K e2.
+ spec_ctx ∗ j ⤇ fill K (If (#♠false) e1 e2) ={E}=∗ j ⤇ fill K e2.
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_if_true E Ï j K e1 e2 :
+ Lemma step_if_true E j K e1 e2 :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (If (#â™ true) e1 e2) ={E}=∗ j ⤇ fill K e1.
+ spec_ctx ∗ j ⤇ fill K (If (#♠true) e1 e2) ={E}=∗ j ⤇ fill K e1.
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_nat_binop E Ï j K op a b :
+ Lemma step_nat_binop E j K op a b :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (BinOp op (#n a) (#n b))
+ spec_ctx ∗ j ⤇ fill K (BinOp op (#n a) (#n b))
={E}=∗ j ⤇ fill K (of_val (binop_eval op a b)).
Proof. by intros; apply: do_step_pure. Qed.
- Lemma step_fork E Ï j K e :
+ Lemma step_fork E j K e :
nclose specN ⊆ E →
- spec_ctx Ï âˆ— j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e.
+ spec_ctx ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e.
Proof.
- iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+ iIntros (?) "[#Hinv Hj]". iDestruct "Hinv" as (Ï) "Hinv".
+ rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
iDestruct (own_valid_2 with "Hown Hj")
as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index 79cab342..2ce4327f 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -26,8 +26,10 @@ Proof.
iExists (λ σ _, own γ (◠to_gen_heap σ)); iFrame.
iApply wp_fupd. iApply wp_wand_r.
iSplitL.
- iPoseProof ((Hlog _ _ [] [] ([e'], ∅)) with "[$Hcfg]") as "Hrel".
- { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
+ iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
+ { iSplit.
+ - by iExists ([e'], ∅).
+ - by iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
simpl.
replace e with e.[env_subst[]] at 2 by by asimpl.
iApply ("Hrel" $! 0 []).
--
GitLab