From f4fed4c24a9edcdf8e9a593bd1397ea74e7117a7 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Wed, 21 Mar 2018 15:18:47 +0100
Subject: [PATCH] Make EqType more realistic
---
.../logrel/F_mu_ref_conc/context_refinement.v | 4 +-
.../logrel/F_mu_ref_conc/examples/counter.v | 2 +-
.../F_mu_ref_conc/examples/stack/FG_stack.v | 81 +++++----
.../F_mu_ref_conc/examples/stack/refinement.v | 32 ++--
.../logrel/F_mu_ref_conc/fundamental_binary.v | 41 ++---
theories/logrel/F_mu_ref_conc/logrel_binary.v | 154 ++++++++++++++++--
.../logrel/F_mu_ref_conc/soundness_binary.v | 9 +-
theories/logrel/F_mu_ref_conc/typing.v | 3 +-
8 files changed, 224 insertions(+), 102 deletions(-)
diff --git a/theories/logrel/F_mu_ref_conc/context_refinement.v b/theories/logrel/F_mu_ref_conc/context_refinement.v
index 7914b5e6..4075952f 100644
--- a/theories/logrel/F_mu_ref_conc/context_refinement.v
+++ b/theories/logrel/F_mu_ref_conc/context_refinement.v
@@ -187,7 +187,9 @@ Proof.
Qed.
Definition ctx_refines (Γ : list type)
- (e e' : expr) (τ : type) := ∀ K thp σ v,
+ (e e' : expr) (Ï„ : type) :=
+ typed Γ e τ ∧ typed Γ e' τ ∧
+ ∀ K thp σ v,
typed_ctx K Γ τ [] TUnit →
rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) →
∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ').
diff --git a/theories/logrel/F_mu_ref_conc/examples/counter.v b/theories/logrel/F_mu_ref_conc/examples/counter.v
index a32818bd..6e70b2a7 100644
--- a/theories/logrel/F_mu_ref_conc/examples/counter.v
+++ b/theories/logrel/F_mu_ref_conc/examples/counter.v
@@ -366,6 +366,6 @@ Theorem counter_ctx_refinement :
Proof.
set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]).
set (HG := soundness_unary.HeapPreIG Σ _ _).
- eapply (binary_soundness Σ _); auto.
+ eapply (binary_soundness Σ _); auto using FG_counter_type, CG_counter_type.
intros. apply FG_CG_counter_refinement.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
index e7e79e79..4463e46d 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
@@ -3,11 +3,14 @@ From iris_examples.logrel.F_mu_ref_conc Require Import typing.
Definition FG_StackType Ï„ :=
TRec (Tref (TSum TUnit (TProd Ï„.[ren (+1)] (TVar 0)))).
+Definition FG_Stack_Ref_Type Ï„ :=
+ Tref (TSum TUnit (TProd Ï„ (FG_StackType Ï„))).
+
Definition FG_push (st : expr) : expr :=
Rec (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
- (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+ (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -19,7 +22,7 @@ Definition FG_pushV (st : expr) : val :=
RecV (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
- (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+ (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -39,8 +42,8 @@ Definition FG_pop (st : expr) : expr :=
If
(CAS
(st.[ren (+7)])
- (Fold (Var 4))
- (Snd (Var 0))
+ (Var 4)
+ (Unfold (Snd (Var 0)))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -52,7 +55,7 @@ Definition FG_pop (st : expr) : expr :=
)
)
)
- (Unfold (Load st.[ren (+ 2)]))
+ (Load st.[ren (+ 2)])
).
Definition FG_popV (st : expr) : val :=
RecV
@@ -67,8 +70,8 @@ Definition FG_popV (st : expr) : val :=
If
(CAS
(st.[ren (+7)])
- (Fold (Var 4))
- (Snd (Var 0))
+ (Var 4)
+ (Unfold (Snd (Var 0)))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -80,7 +83,7 @@ Definition FG_popV (st : expr) : val :=
)
)
)
- (Unfold (Load st.[ren (+ 2)]))
+ (Load st.[ren (+ 2)])
).
Definition FG_iter (f : expr) : expr :=
@@ -100,14 +103,14 @@ Definition FG_iterV (f : expr) : val :=
)
).
Definition FG_read_iter (st : expr) : expr :=
- Rec (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
+ Rec (App (FG_iter (Var 1)) (Fold (Load st.[ren (+2)]))).
Definition FG_stack_body (st : expr) : expr :=
Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
Definition FG_stack : expr :=
TLam (App (Rec (FG_stack_body (Var 1)))
- (Alloc (Fold (Alloc (InjL Unit))))).
+ (Alloc (Alloc (InjL Unit)))).
Section FG_stack.
(* Fine-grained push *)
@@ -116,7 +119,7 @@ Section FG_stack.
Rec (App (Rec
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
- (Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
+ (Alloc (InjR (Pair (Var 3) (Fold (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
@@ -127,20 +130,19 @@ Section FG_stack.
Proof. trivial. Qed.
Section FG_push_type.
- (* The following assumption is simply ** WRONG ** *)
- (* We assume it though to just be able to prove that the
- stack we are implementing is /type-sane/ so to speak! *)
- Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
-
Lemma FG_push_type st Γ τ :
- typed Γ st (Tref (FG_StackType τ)) →
+ typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
typed Γ (FG_push st) (TArrow τ TUnit).
Proof.
- intros H1. repeat (econstructor; eauto using HEQTP).
+ intros HTst.
+ repeat match goal with
+ |- typed _ _ _ => econstructor; eauto
+ end; repeat econstructor; eauto.
- eapply (context_weakening [_; _; _; _]); eauto.
- by asimpl.
- - eapply (context_weakening [_; _]); eauto.
+ - eapply (context_weakening [_; _]); eauto.
Qed.
+
End FG_push_type.
Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st).
@@ -173,8 +175,8 @@ Section FG_stack.
If
(CAS
(st.[ren (+7)])
- (Fold (Var 4))
- (Snd (Var 0))
+ (Var 4)
+ (Unfold (Snd (Var 0)))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
@@ -186,24 +188,28 @@ Section FG_stack.
)
)
)
- (Unfold (Load st.[ren (+ 2)]))
+ (Load st.[ren (+ 2)])
).
Proof. trivial. Qed.
Section FG_pop_type.
- (* The following assumption is simply ** WRONG ** *)
- (* We assume it though to just be able to prove that the
- stack we are implementing is /type-sane/ so to speak! *)
- Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
Lemma FG_pop_type st Γ τ :
- typed Γ st (Tref (FG_StackType τ)) →
+ typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)).
Proof.
- intros H1. repeat (econstructor; eauto using HEQTP).
- - eapply (context_weakening [_; _; _; _; _; _; _]); eauto.
- - asimpl; trivial.
+ replace (FG_Stack_Ref_Type Ï„) with
+ (Tref (TSum TUnit (TProd Ï„.[ren (+1)] (TVar 0)))).[FG_StackType Ï„/];
+ last first.
+ { by asimpl. }
+ intros HTst.
+ repeat match goal with
+ |- typed _ _ _ => econstructor; eauto
+ end; repeat econstructor; eauto; last first.
- eapply (context_weakening [_; _]); eauto.
+ - by asimpl.
+ - eapply (context_weakening [_; _; _; _; _; _; _]); eauto.
+ - econstructor.
Qed.
End FG_pop_type.
@@ -270,13 +276,13 @@ Section FG_stack.
Global Opaque FG_iter.
Lemma FG_read_iter_type st Γ τ :
- typed Γ st (Tref (FG_StackType τ)) →
+ typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
typed Γ (FG_read_iter st)
(TArrow (TArrow Ï„ TUnit) TUnit).
Proof.
intros H1; repeat econstructor.
- eapply FG_iter_type; by constructor.
- - by eapply (context_weakening [_;_]).
+ - by eapply (context_weakening [_;_]); asimpl.
Qed.
Transparent FG_iter.
@@ -296,13 +302,9 @@ Section FG_stack.
Global Opaque FG_iter.
Section FG_stack_body_type.
- (* The following assumption is simply ** WRONG ** *)
- (* We assume it though to just be able to prove that the
- stack we are implementing is /type-sane/ so to speak! *)
- Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
Lemma FG_stack_body_type st Γ τ :
- typed Γ st (Tref (FG_StackType τ)) →
+ typed Γ st (Tref (FG_Stack_Ref_Type τ)) →
typed Γ (FG_stack_body st)
(TProd
(TProd (TArrow Ï„ TUnit) (TArrow TUnit (TSum TUnit Ï„)))
@@ -328,10 +330,6 @@ Section FG_stack.
Qed.
Section FG_stack_type.
- (* The following assumption is simply ** WRONG ** *)
- (* We assume it though to just be able to prove that the
- stack we are implementing is /type-sane/ so to speak! *)
- Context (HEQTP : ∀ τ, EqType (FG_StackType τ)).
Lemma FG_stack_type Γ :
typed Γ FG_stack
@@ -348,7 +346,6 @@ Section FG_stack.
- eapply FG_push_type; try constructor; simpl; eauto.
- eapply FG_pop_type; try constructor; simpl; eauto.
- eapply FG_read_iter_type; constructor; by simpl.
- - asimpl. repeat constructor.
Qed.
End FG_stack_type.
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 711a2307..731802e5 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
@@ -41,7 +41,7 @@ Section Stack_refinement.
simpl.
rewrite CG_locked_push_subst CG_locked_pop_subst
CG_iter_subst CG_snap_subst. simpl. asimpl.
- iApply (wp_bind (fill [FoldCtx; AllocCtx; AppRCtx (RecV _)]));
+ iApply (wp_bind (fill [AllocCtx; AppRCtx (RecV _)]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply wp_alloc; first done. iNext; iIntros (istk) "Histk".
iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -64,7 +64,7 @@ Section Stack_refinement.
iFrame "Hls". iLeft. iSplit; trivial. }
iAssert ((∃ istk v h, (stack_owns h)
∗ stk' ↦ₛ v
- ∗ stk ↦ᵢ (FoldV (LocV istk))
+ ∗ stk ↦ᵢ (LocV istk)
∗ StackLink τi (LocV istk, v)
∗ l ↦ₛ (#â™v false)
)%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
@@ -98,8 +98,8 @@ Section Stack_refinement.
clear v h.
iApply wp_pure_step_later; auto using to_of_val.
iModIntro. iNext. asimpl.
- iApply (wp_bind (fill [FoldCtx;
- CasRCtx (LocV _) (FoldV (LocV _)); IfCtx _ _]));
+
+ iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
iApply wp_alloc; simpl; trivial.
iNext. iIntros (ltmp) "Hltmp".
@@ -140,7 +140,7 @@ Section Stack_refinement.
iApply wp_pure_step_later; auto. iNext.
rewrite -(FG_pop_folding (Loc stk)).
asimpl.
- iApply (wp_bind (fill [UnfoldCtx; AppRCtx (RecV _)]));
+ iApply (wp_bind (fill [AppRCtx (RecV _)]));
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iInv stackN as (istk v h) "[Hoe [Hstk' [Hstk [#HLK Hl]]]]" "Hclose".
iApply (wp_load with "Hstk"). iNext. iIntros "Hstk".
@@ -153,10 +153,7 @@ Section Stack_refinement.
as "[Hj [Hstk' Hl]]"; first solve_ndisj.
iMod ("Hclose" with "[-Hj Hmpt]") as "_".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
- iApply (wp_bind (fill [AppRCtx (RecV _)]));
- iApply wp_wand_l; iSplitR; [iModIntro; iIntros (w) "Hw"; iExact "Hw"|].
- iApply wp_pure_step_later; simpl; auto using to_of_val.
- iModIntro. iNext. iApply wp_value.
+ iModIntro.
iApply wp_pure_step_later; auto. iNext. asimpl.
clear h.
iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -176,10 +173,7 @@ Section Stack_refinement.
* (* The stack is not empty *)
iMod ("Hclose" with "[-Hj Hmpt HLK']") as "_".
{ iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
- iApply (wp_bind (fill [AppRCtx (RecV _)]));
- iApply wp_wand_l; iSplitR; [iModIntro; iIntros (w') "Hw"; iExact "Hw"|].
- iApply wp_pure_step_later; simpl; auto.
- iModIntro. iNext. iApply wp_value. iApply wp_pure_step_later; auto.
+ iModIntro. iApply wp_pure_step_later; auto.
iNext. asimpl.
clear h.
iApply (wp_bind (fill [AppRCtx (RecV _)]));
@@ -195,8 +189,12 @@ Section Stack_refinement.
iModIntro. iNext. asimpl.
iDestruct "HLK'" as (y1 z1 y2 z2) "[% HLK']". subst. simpl.
iApply wp_pure_step_later; [simpl; by rewrite ?to_of_val |].
- iNext.
- iApply (wp_bind (fill [CasRCtx (LocV _) (FoldV (LocV _)); IfCtx _ _]));
+ iNext. asimpl.
+ iApply (wp_bind (fill [UnfoldCtx; CasRCtx (LocV _) (LocV _); IfCtx _ _]));
+ iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
+ asimpl. iApply wp_pure_step_later; auto.
+ simpl. iNext. iApply wp_value.
+ iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _); IfCtx _ _]));
iApply wp_wand_l; iSplitR; [iIntros (w) "Hw"; iExact "Hw"|].
asimpl. iApply wp_pure_step_later; auto.
simpl. iNext. iApply wp_value.
@@ -249,7 +247,7 @@ Section Stack_refinement.
by (by rewrite FG_iter_of_val).
replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
by (by rewrite CG_iter_of_val).
- iApply (wp_bind (fill [AppRCtx _])); iApply wp_wand_l;
+ 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)
@@ -337,6 +335,6 @@ Theorem stack_ctx_refinement :
Proof.
set (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR); GFunctor (authR stackUR)]).
set (HG := soundness_unary.HeapPreIG Σ _ _).
- eapply (binary_soundness Σ); eauto using FG_stack_closed, CG_stack_closed.
+ eapply (binary_soundness Σ); eauto using FG_stack_type, CG_stack_type.
intros; apply FG_CG_counter_refinement.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/fundamental_binary.v b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
index db6088a3..d1ec85e8 100644
--- a/theories/logrel/F_mu_ref_conc/fundamental_binary.v
+++ b/theories/logrel/F_mu_ref_conc/fundamental_binary.v
@@ -356,8 +356,8 @@ Section fundamental.
iApply wp_atomic; eauto.
iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
iModIntro.
- iApply (wp_store with "Hv1"); auto using to_of_val.
- iNext. iIntros "Hw2".
+ iApply (wp_store with "Hv1"); auto using to_of_val.
+ iNext. iIntros "Hw2".
iMod (step_store with "[$Hs Hw Hv2]") as "[Hw Hv2]"; eauto;
[solve_ndisj | by iFrame|].
iMod ("Hclose" with "[Hw2 Hv2]").
@@ -381,30 +381,31 @@ Section fundamental.
('`IHHtyped3 _ _ _ j ((CasRCtx _ _) :: K)).
iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=.
iApply wp_atomic; eauto.
- iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
+ iMod (interp_ref_open' _ _ l l' with "[]") as
+ (v v') "(>Hl & >Hl' & #Hiv & Heq & Hcl)"; eauto.
+ { iExists (_, _); eauto. }
iModIntro.
- iPoseProof ("Hv") as "Hv'".
- rewrite {2}[⟦ τ ⟧ Δ (v, v')]interp_EqType_agree; trivial.
- iMod "Hv'" as %Hv'; subst.
- destruct (decide (v' = w)) as [|Hneq]; subst.
- - iAssert (â–· ⌜w' = wâŒ)%I as ">%".
- { rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
- simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
- iNext. iIntros "Hv1".
+ destruct (decide (v = w)) as [|Hneq]; subst.
+ - iApply (wp_cas_suc with "Hl"); eauto using to_of_val; eauto.
+ iNext. iIntros "Hl".
+ iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
+ iDestruct "Heq" as %[-> _]; last trivial.
iMod (step_cas_suc
- with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
- iFrame. iFrame "Hs".
- iMod ("Hclose" with "[Hv1 Hv2]").
+ with "[Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
+ { iFrame. iFrame "Hs". }
+ iMod ("Hcl" with "[Hl Hl']").
{ iNext; iExists (_, _); by iFrame. }
iExists (#â™v true); iFrame; eauto.
- - iAssert (â–· ⌜v' ≠w'âŒ)%I as ">%".
- { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
- simpl. iApply (wp_cas_fail with "Hv1"); eauto.
- iNext. iIntros "Hv1".
+ - iApply (wp_cas_fail with "Hl"); eauto using to_of_val; eauto.
+ iNext. iIntros "Hl".
+ iMod ("Heq" with "Hl Hl' Hiv Hiw") as "(Hl & Hl' & Heq)".
+ iDestruct "Heq" as %[_ Heq].
+ assert (v' ≠w').
+ { by intros ?; apply Hneq; rewrite Heq. }
iMod (step_cas_fail
- with "[$Hs Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
+ with "[$Hs Hu Hl']") as "[Hw Hl']"; simpl; eauto; first solve_ndisj.
iFrame.
- iMod ("Hclose" with "[Hv1 Hv2]").
+ iMod ("Hcl" with "[Hl Hl']").
{ iNext; iExists (_, _); by iFrame. }
iExists (#â™v false); eauto.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/logrel_binary.v b/theories/logrel/F_mu_ref_conc/logrel_binary.v
index 2c21dbad..f0e2b7cf 100644
--- a/theories/logrel/F_mu_ref_conc/logrel_binary.v
+++ b/theories/logrel/F_mu_ref_conc/logrel_binary.v
@@ -231,25 +231,149 @@ Section logrel.
apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
Qed.
- Lemma interp_EqType_agree τ v v' Δ :
- env_Persistent Δ → EqType Ï„ → interp Ï„ Δ (v, v') ⊢ ⌜v = v'âŒ.
+ Lemma interp_ref_pointsto_neq E Δ τ l w (l1 l2 l3 l4 : loc) :
+ ↑logN.@(l1, l2) ⊆ E →
+ l2 ≠l4 →
+ l ↦ᵢ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
+ |={E ∖ ↑logN.@(l3, l4)}=> l ↦ᵢ w ∗ ⌜l ≠l1âŒ.
Proof.
- intros ? HÏ„; revert v v'; induction HÏ„; iIntros (v v') "#H1 /=".
- - by iDestruct "H1" as "[% %]"; subst.
- - by iDestruct "H1" as (n) "[% %]"; subst.
- - by iDestruct "H1" as (b) "[% %]"; subst.
- - iDestruct "H1" as ([??] [??]) "[% [H1 H2]]"; simplify_eq/=.
- rewrite IHHÏ„1 IHHÏ„2.
- by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
- - iDestruct "H1" as "[H1|H1]".
- + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
- rewrite IHHÏ„1. by iDestruct "H1" as "%"; subst.
- + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
- rewrite IHHÏ„2. by iDestruct "H1" as "%"; subst.
+ intros Hnin Hneq.
+ destruct (decide (l = l1)); subst; last auto.
+ iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
+ iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
+ iDestruct "Hi" as ((v1, v2)) "(Hl3 & Hl2' & ?)".
+ iMod "Hl3".
+ by iDestruct (@mapsto_valid_2 with "Hl1 Hl3") as %?.
Qed.
+
+ Lemma interp_ref_pointsto_neq' E Δ τ l w (l1 l2 l3 l4 : loc) :
+ ↑logN.@(l1, l2) ⊆ E →
+ l1 ≠l3 →
+ l ↦ₛ w -∗ interp (Tref τ) Δ (LocV l1, LocV l2) -∗
+ |={E ∖ ↑logN.@(l3, l4)}=> l ↦ₛ w ∗ ⌜l ≠l2âŒ.
+ Proof.
+ intros Hnin Hneq.
+ destruct (decide (l = l2)); subst; last auto.
+ iIntros "Hl1"; simpl; iDestruct 1 as ((l5, l6)) "[% Hl2]"; simplify_eq.
+ iInv (logN.@(l5, l6)) as "Hi" "Hcl"; simpl.
+ iDestruct "Hi" as ((v1, v2)) "(Hl3 & Hl2' & ?)".
+ iMod "Hl2'"; simpl.
+ unfold heapS_mapsto.
+ iDestruct (@own_valid_2 _ _ _ cfg_name with "Hl1 Hl2'") as %[_ Hvl].
+ exfalso.
+ specialize (Hvl l6); revert Hvl. simpl.
+ rewrite /= gmap.lookup_op !lookup_singleton -Some_op. by intros [? _].
+ Qed.
+
+ Lemma interp_ref_open' Δ τ l l' :
+ env_Persistent Δ → EqType τ →
+ ⟦ Tref τ ⟧ Δ (LocV l, LocV l') -∗
+ |={⊤, ⊤ ∖ ↑logN.@(l, l')}=>
+ ∃ w w', ▷ l ↦ᵢ w ∗ ▷ l' ↦ₛ w' ∗ ▷ ⟦ τ ⟧ Δ (w, w') ∗
+ ▷ (∀ z z' u u' v v',
+ l ↦ᵢ z -∗ l' ↦ₛ z' -∗ ⟦ τ ⟧ Δ (u, u') -∗ ⟦ τ ⟧ Δ (v, v') -∗
+ |={⊤ ∖ ↑logN.@(l, l')}=> l ↦ᵢ z ∗
+ l' ↦ₛ z' ∗ ⌜v = u ↔ v' = u'âŒ)
+ ∗ (▷ (∃ vv : val * val, l ↦ᵢ vv.1 ∗ l' ↦ₛ vv.2 ∗ ⟦ τ ⟧ Δ vv)
+ ={⊤ ∖ ↑logN.@(l, l'), ⊤}=∗ True).
+ Proof.
+ iIntros (HΔ Heqt); simpl.
+ iDestruct 1 as ((l1, l1')) "[% H1]"; simplify_eq.
+ iInv (logN.@(l1, l1')) as "Hi" "$"; simpl. iClear "H1".
+ iDestruct "Hi" as ((v1, v2)) "(Hl1 & Hl1' & Hrl)"; simpl in *.
+ destruct Heqt; simpl in *.
+ - iModIntro; iExists _, _; iFrame.
+ iNext. iIntros (??????) "? ?". iIntros ([??] [??]); subst.
+ by iModIntro; iFrame.
+ - iModIntro; iExists _, _; iFrame.
+ iNext. iIntros (??????) "? ?".
+ iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
+ simplify_eq. by iModIntro; iFrame.
+ - iModIntro; iExists _, _; iFrame.
+ iNext. iIntros (??????) "? ?".
+ iDestruct 1 as (?) "[% %]". iDestruct 1 as (?) "[% %]".
+ simplify_eq. by iModIntro; iFrame.
+ - iModIntro; iExists _, _; iFrame; iFrame "#". iNext.
+ iIntros (z z' u u' v v') "Hl1 Hl1' Huu". iDestruct 1 as ((l2, l2')) "[% #Hl2]";
+ simplify_eq; simpl in *.
+ iDestruct "Huu" as ((l3, l3')) "[% #Hl3]";
+ simplify_eq; simpl in *.
+ destruct (decide ((l1, l1') = (l2, l2'))); simplify_eq.
+ + destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq; first by iFrame.
+ destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
+ * iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ * iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ * iMod (interp_ref_pointsto_neq' with "Hl1' []")
+ as "[Hl1' %]";
+ simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ * iFrame; iModIntro; iPureIntro; split; by inversion 1.
+ + destruct (decide ((l1, l1') = (l3, l3'))); simplify_eq.
+ * destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
+ -- iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ -- iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { iExists (_, _); iSplit; first eauto. iFrame "#". }
+ by iFrame.
+ -- iMod (interp_ref_pointsto_neq' with "Hl1' []")
+ as "[Hl1' %]";
+ simpl; eauto.
+ { iExists (_, _); iSplit; first eauto. iFrame "#". }
+ by iFrame.
+ -- iFrame; iModIntro; iPureIntro; split; by inversion 1.
+ * destruct (decide ((l2, l2') = (l3, l3'))); simplify_eq.
+ -- destruct (decide (l1 = l3)); destruct (decide (l1' = l3')); subst.
+ ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ ++ iMod (interp_ref_pointsto_neq with "Hl1 []")
+ as "[Hl1 %]"; simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ ++ iMod (interp_ref_pointsto_neq' with "Hl1' []")
+ as "[Hl1' %]";
+ simpl; eauto.
+ { by iExists (_, _); iFrame "#". }
+ by iFrame.
+ ++ iFrame; iModIntro; iPureIntro; split; by inversion 1.
+ -- iFrame.
+ { destruct (decide (l2 = l3)); destruct (decide (l2' = l3'));
+ simplify_eq; auto.
+ + iInv (logN.@(l3, l2')) as "Hib1" "Hcl1".
+ iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
+ iDestruct "Hib1" as ((v11, v12)) "(Hlx1' & Hlx2 & Hr1)".
+ iDestruct "Hib2" as ((v11', v12')) "(Hl1'' & Hl2' & Hr2)".
+ simpl.
+ iMod "Hlx1'"; iMod "Hl1''".
+ by iDestruct (@mapsto_valid_2 with "Hlx1' Hl1''") as %?.
+ + iInv (logN.@(l2, l3')) as "Hib1" "Hcl1".
+ iInv (logN.@(l3, l3')) as "Hib2" "Hcl2".
+ iDestruct "Hib1" as ((v11, v12)) "(Hl1 & Hl2' & Hr1)".
+ iDestruct "Hib2" as ((v11', v12')) "(Hl1' & Hl2'' & Hr2)".
+ simpl.
+ iMod "Hl2'"; iMod "Hl2''".
+ unfold heapS_mapsto.
+ iDestruct (@own_valid_2 _ _ _ cfg_name with "Hl2' Hl2''") as %[_ Hvl].
+ exfalso.
+ specialize (Hvl l3'); revert Hvl.
+ rewrite /= gmap.lookup_op !lookup_singleton -Some_op. by intros [? _].
+ + iModIntro; iPureIntro; split; intros; simplify_eq. }
+ Qed.
+
End logrel.
Typeclasses Opaque interp_env.
Notation "⟦ τ ⟧" := (interp τ).
Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)).
-Notation "⟦ Γ ⟧*" := (interp_env Γ).
\ No newline at end of file
+Notation "⟦ Γ ⟧*" := (interp_env Γ).
diff --git a/theories/logrel/F_mu_ref_conc/soundness_binary.v b/theories/logrel/F_mu_ref_conc/soundness_binary.v
index 18e2dffb..471dd8ea 100644
--- a/theories/logrel/F_mu_ref_conc/soundness_binary.v
+++ b/theories/logrel/F_mu_ref_conc/soundness_binary.v
@@ -45,11 +45,12 @@ Qed.
Lemma binary_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
Γ e e' τ :
- (∀ f, e.[upn (length Γ) f] = e) →
- (∀ f, e'.[upn (length Γ) f] = e') →
+ (Γ ⊢ₜ e : τ) → (Γ ⊢ₜ e' : τ) →
(∀ `{heapIG Σ, cfgSG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
Γ ⊨ e ≤ctx≤ e' : τ.
Proof.
- intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
- eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
+ intros He He' Hlog; repeat split; auto.
+ intros K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
+ eapply (bin_log_related_under_typed_ctx _ _ _ _ []);
+ eauto using typed_n_closed.
Qed.
diff --git a/theories/logrel/F_mu_ref_conc/typing.v b/theories/logrel/F_mu_ref_conc/typing.v
index 9c4bfc2c..e17af915 100644
--- a/theories/logrel/F_mu_ref_conc/typing.v
+++ b/theories/logrel/F_mu_ref_conc/typing.v
@@ -27,8 +27,7 @@ Inductive EqType : type → Prop :=
| EqTUnit : EqType TUnit
| EqTNat : EqType TNat
| EqTBool : EqType TBool
- | EqTProd τ τ' : EqType τ → EqType τ' → EqType (TProd τ τ')
- | EqSum τ τ' : EqType τ → EqType τ' → EqType (TSum τ τ').
+ | EQRef Ï„ : EqType (Tref Ï„).
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
--
GitLab