Commit 0770367b authored by Robbert Krebbers's avatar Robbert Krebbers

Improve notations for binary logrel.

parent 42b71ff1
......@@ -199,9 +199,9 @@ Section bin_log_related_under_typed_ctx.
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
typed_ctx K Γ τ Γ' τ'
( Δ (HΔ : ctx_PersistentP Δ), @bin_log_related _ _ _ Δ Γ e e' τ)
( Δ (HΔ : ctx_PersistentP Δ), Δ Γ e log e' : τ)
Δ (HΔ : ctx_PersistentP Δ),
@bin_log_related _ _ _ Δ Γ' (fill_ctx K e) (fill_ctx K e') τ'.
Δ Γ' fill_ctx K e log fill_ctx K e' : τ'.
Proof.
revert Γ τ Γ' τ' e e'.
induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl.
......
......@@ -254,8 +254,7 @@ Section CG_Counter.
Definition counterN : namespace := nroot .@ "counter".
Lemma FG_CG_counter_refinement Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Δ [] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
(* executing the preambles *)
intros [|v vs] ρ j K [=].
......
......@@ -13,15 +13,10 @@ Section Stack_refinement.
Implicit Types Δ : listC D.
Lemma FG_CG_counter_refinement Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ Δ [] FG_stack CG_stack
(TForall
(TProd
(TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0)))
)
(TArrow (TArrow (TVar 0) TUnit) TUnit)
)).
Δ [] FG_stack log CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
(* executing the preambles *)
iIntros { [|??] ρ j K [=] } "[#Hheap [#Hspec [_ Hj]]]".
......@@ -376,16 +371,10 @@ End Stack_refinement.
Definition Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR].
Theorem stack_ctx_refinement :
ctx_refines [] FG_stack CG_stack
(TForall
(TProd
(TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0)))
)
(TArrow (TArrow (TVar 0) TUnit) TUnit)
)
).
ctx_refines [] FG_stack CG_stack (TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit))).
Proof.
eapply (@binary_soundness Σ);
eauto using FG_stack_closed, CG_stack_closed.
......
......@@ -3,6 +3,22 @@ From iris.proofmode Require Import tactics pviewshifts invariants.
From iris_logrel.F_mu_ref_par Require Import rules_binary.
From iris.algebra Require Export upred_big_op.
Section bin_log_def.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Definition bin_log_related (Δ : listC D) (Γ : list type)
(e e' : expr) (τ : type) : Prop := vvs ρ j K,
length Γ = length vvs
heapI_ctx spec_ctx ρ [] zip_with (λ τ, interp τ Δ) Γ vvs
j fill K (e'.[env_subst (vvs.*2)])
WP e.[env_subst (vvs.*1)] {{ v, v',
j fill K (# v') interp τ Δ (v, v') }}.
End bin_log_def.
Notation "Δ ∥ Γ ⊨ e '≤log≤' e' : τ" :=
(bin_log_related Δ Γ e e' τ) (at level 74, Γ, e, e', τ at next level).
Section typed_interp.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
......@@ -21,23 +37,12 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Definition bin_log_related (Δ : listC D) (Γ : list type)
(e e' : expr) (τ : type) : Prop := vvs ρ j K,
length Γ = length vvs
heapI_ctx spec_ctx ρ [] zip_with (λ τ, interp τ Δ) Γ vvs
j fill K (e'.[env_subst (vvs.*2)])
WP e.[env_subst (vvs.*1)] {{ v, v',
j fill K (# v') interp τ Δ (v, v') }}.
Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
(at level 20).
Notation "✓✓ Δ" := (ctx_PersistentP Δ) (at level 20).
Lemma typed_binary_interp_Pair Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e1 log e1' τ1)
(IHHtyped2 : Δ Γ e2 log e2' τ2) :
Δ Γ Pair e1 e2 log Pair e1' e2' TProd τ1 τ2.
(IHHtyped1 : Δ Γ e1 log e1' : τ1)
(IHHtyped2 : Δ Γ e2 log e2' : τ2) :
Δ Γ Pair e1 e2 log Pair e1' e2' : TProd τ1 τ2.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (PairLCtx e2.[env_subst _]) v v' "[Hv #Hiv]"
......@@ -49,8 +54,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Fst Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' TProd τ1 τ2) :
Δ Γ Fst e log Fst e' τ1.
(IHHtyped : Δ Γ e log e' : TProd τ1 τ2) :
Δ Γ Fst e log Fst e' : τ1.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" (IHHtyped _ _ j (K ++ [FstCtx])); cbn.
......@@ -60,8 +65,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Snd Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' TProd τ1 τ2) :
Δ Γ Snd e log Snd e' τ2.
(IHHtyped : Δ Γ e log e' : TProd τ1 τ2) :
Δ Γ Snd e log Snd e' : τ2.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" (IHHtyped _ _ j (K ++ [SndCtx])); cbn.
......@@ -71,8 +76,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_InjL Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' τ1) :
Δ Γ InjL e log InjL e' (TSum τ1 τ2).
(IHHtyped : Δ Γ e log e' : τ1) :
Δ Γ InjL e log InjL e' : (TSum τ1 τ2).
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
......@@ -82,8 +87,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_InjR Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' τ2) :
Δ Γ InjR e log InjR e' TSum τ1 τ2.
(IHHtyped : Δ Γ e log e' : τ2) :
Δ Γ InjR e log InjR e' : TSum τ1 τ2.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
......@@ -97,10 +102,10 @@ Section typed_interp.
(Hclosed3 : f, e2.[iter (S (length Γ)) up f] = e2)
(Hclosed2' : f, e1'.[iter (S (length Γ)) up f] = e1')
(Hclosed3' : f, e2'.[iter (S (length Γ)) up f] = e2')
(IHHtyped1 : Δ Γ e0 log e0' TSum τ1 τ2)
(IHHtyped2 : Δ τ1 :: Γ e1 log e1' τ3)
(IHHtyped3 : Δ τ2 :: Γ e2 log e2' τ3) :
Δ Γ Case e0 e1 e2 log Case e0' e1' e2' τ3.
(IHHtyped1 : Δ Γ e0 log e0' : TSum τ1 τ2)
(IHHtyped2 : Δ τ1 :: Γ e1 log e1' : τ3)
(IHHtyped3 : Δ τ2 :: Γ e2 log e2' : τ3) :
Δ Γ Case e0 e1 e2 log Case e0' e1' e2' : τ3.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
......@@ -123,10 +128,10 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_If Δ Γ e0 e1 e2 e0' e1' e2' τ {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e0 log e0' TBool)
(IHHtyped2 : Δ Γ e1 log e1' τ)
(IHHtyped3 : Δ Γ e2 log e2' τ) :
Δ Γ If e0 e1 e2 log If e0' e1' e2' τ.
(IHHtyped1 : Δ Γ e0 log e0' : TBool)
(IHHtyped2 : Δ Γ e1 log e1' : τ)
(IHHtyped3 : Δ Γ e2 log e2' : τ) :
Δ Γ If e0 e1 e2 log If e0' e1' e2' : τ.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
......@@ -139,9 +144,9 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_nat_bin_op Δ Γ op e1 e2 e1' e2' {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e1 log e1' TNat)
(IHHtyped2 : Δ Γ e2 log e2' TNat) :
Δ Γ BinOp op e1 e2 log BinOp op e1' e2' binop_res_type op.
(IHHtyped1 : Δ Γ e1 log e1' : TNat)
(IHHtyped2 : Δ Γ e2 log e2' : TNat) :
Δ Γ BinOp op e1 e2 log BinOp op e1' e2' : binop_res_type op.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (BinOpLCtx _ _) v v' "[Hv #Hiv]"
......@@ -159,8 +164,8 @@ Section typed_interp.
Lemma typed_binary_interp_Lam Δ Γ (e e' : expr) τ1 τ2 {HΔ : ✓✓ Δ}
(Hclosed : f, e.[iter (S (S (length Γ))) up f] = e)
(Hclosed' : f, e'.[iter (S (S (length Γ))) up f] = e')
(IHHtyped : Δ TArrow τ1 τ2 :: τ1 :: Γ e log e' τ2) :
Δ Γ Lam e log Lam e' TArrow τ1 τ2.
(IHHtyped : Δ TArrow τ1 τ2 :: τ1 :: Γ e log e' : τ2) :
Δ Γ Lam e log Lam e' : TArrow τ1 τ2.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
value_case. iExists (LamV _). iIntros "{$Hj} !".
......@@ -176,9 +181,9 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_App Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e1 log e1' TArrow τ1 τ2)
(IHHtyped2 : Δ Γ e2 log e2' τ1) :
Δ Γ App e1 e2 log App e1' e2' τ2.
(IHHtyped1 : Δ Γ e1 log e1' : TArrow τ1 τ2)
(IHHtyped2 : Δ Γ e2 log e2' : τ1) :
Δ Γ App e1 e2 log App e1' e2' : τ2.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]"
......@@ -190,8 +195,8 @@ Section typed_interp.
Lemma typed_binary_interp_TLam Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : (τi : D), ( vw, PersistentP (τi vw))
(τi :: Δ) (subst (ren (+1)) <$> Γ) e log e' τ) :
Δ Γ TLam e log TLam e' TForall τ.
(τi :: Δ) (subst (ren (+1)) <$> Γ) e log e' : τ) :
Δ Γ TLam e log TLam e' : TForall τ.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
value_case. iExists (TLamV _).
......@@ -204,8 +209,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_TApp Δ Γ e e' τ τ' {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' TForall τ) :
Δ Γ TApp e log TApp e' τ.[τ'/].
(IHHtyped : Δ Γ e log e' : TForall τ) :
Δ Γ TApp e log TApp e' : τ.[τ'/].
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (TAppCtx) v v' "[Hj #Hv]"
......@@ -217,8 +222,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Fold Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' τ.[(TRec τ)/]) :
Δ Γ Fold e log Fold e' TRec τ.
(IHHtyped : Δ Γ e log e' : τ.[(TRec τ)/]) :
Δ Γ Fold e log Fold e' : TRec τ.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
iApply (@wp_bind _ _ _ [FoldCtx]);
......@@ -232,8 +237,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Unfold Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' TRec τ) :
Δ Γ Unfold e log Unfold e' τ.[(TRec τ)/].
(IHHtyped : Δ Γ e log e' : TRec τ) :
Δ Γ Unfold e log Unfold e' : τ.[(TRec τ)/].
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
iApply (@wp_bind _ _ _ [UnfoldCtx]);
......@@ -250,8 +255,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Fork Δ Γ e e' {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' TUnit) :
Δ Γ Fork e log Fork e' TUnit.
(IHHtyped : Δ Γ e log e' : TUnit) :
Δ Γ Fork e log Fork e' : TUnit.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
iPvs (step_fork _ _ j K with "* [-]") as {j'} "[Hj Hj']"; eauto.
......@@ -261,8 +266,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Alloc Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' τ) :
Δ Γ Alloc e log Alloc e' Tref τ.
(IHHtyped : Δ Γ e log e' : τ) :
Δ Γ Alloc e log Alloc e' : Tref τ.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" (IHHtyped _ _ j (K ++ [AllocCtx])).
......@@ -276,8 +281,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Load Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' (Tref τ)) :
Δ Γ Load e log Load e' τ.
(IHHtyped : Δ Γ e log e' : (Tref τ)) :
Δ Γ Load e log Load e' : τ.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]" (IHHtyped _ _ j (K ++ [LoadCtx])).
......@@ -293,9 +298,9 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Store Δ Γ e1 e2 e1' e2' τ {HΔ : ✓✓ Δ}
(IHHtyped1 : Δ Γ e1 log e1' (Tref τ))
(IHHtyped2 : Δ Γ e2 log e2' τ) :
Δ Γ Store e1 e2 log Store e1' e2' TUnit.
(IHHtyped1 : Δ Γ e1 log e1' : (Tref τ))
(IHHtyped2 : Δ Γ e2 log e2' : τ) :
Δ Γ Store e1 e2 log Store e1' e2' : TUnit.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]"
......@@ -316,10 +321,10 @@ Section typed_interp.
Lemma typed_binary_interp_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ {HΔ : ✓✓ Δ}
(HEqτ : EqType τ)
(IHHtyped1 : Δ Γ e1 log e1' Tref τ)
(IHHtyped2 : Δ Γ e2 log e2' τ)
(IHHtyped3 : Δ Γ e3 log e3' τ) :
Δ Γ CAS e1 e2 e3 log CAS e1' e2' e3' TBool.
(IHHtyped1 : Δ Γ e1 log e1' : Tref τ)
(IHHtyped2 : Δ Γ e2 log e2' : τ)
(IHHtyped3 : Δ Γ e3 log e3' : τ) :
Δ Γ CAS e1 e2 e3 log CAS e1' e2' e3' : TBool.
Proof.
iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
......@@ -352,7 +357,7 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp Δ Γ e τ {HΔ : ctx_PersistentP Δ} :
Γ ⊢ₜ e : τ Δ Γ e log e τ.
Γ ⊢ₜ e : τ Δ Γ e log e : τ.
Proof.
intros Htyped; revert Δ HΔ; induction Htyped; intros Δ HΔ.
- iIntros {vvs ρ j K Hlen} "(#Hh & #Hs & #HΓ & Hj) /=".
......@@ -392,6 +397,3 @@ Section typed_interp.
- eapply typed_binary_interp_CAS; eauto.
Qed.
End typed_interp.
Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" :=
(bin_log_related Δ Γ e e' τ) (at level 20).
......@@ -12,8 +12,7 @@ Section soundness.
Local Opaque to_heap.
Lemma wp_basic_soundness e e' τ :
( H H' Δ (HΔ : ctx_PersistentP Δ),
@bin_log_related Σ H H' Δ [] e e' τ)
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : ctx_PersistentP Δ), Δ [] e log e' : τ)
ownP (Σ:=globalF Σ)
WP e {{ _, thp' h v, rtc step ([e'], ) (# v :: thp', h) }}.
Proof.
......@@ -63,7 +62,7 @@ Section soundness.
Qed.
Lemma basic_soundness e e' τ v thp hp :
( H H' Δ (HΔ : ctx_PersistentP Δ), @bin_log_related Σ H H' Δ [] e e' τ)
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : ctx_PersistentP Δ), Δ [] e log e' : τ)
rtc step ([e], ) (# v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (# v' :: thp', hp')).
Proof.
......@@ -81,7 +80,7 @@ Section soundness.
Lemma binary_soundness Γ e e' τ :
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
( H H' Δ (HΔ : ctx_PersistentP Δ), @bin_log_related Σ H H' Δ Γ e e' τ)
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : ctx_PersistentP Δ), Δ Γ e log e' : τ)
ctx_refines Γ e e' τ.
Proof.
intros H1 K HK htp hp v Hstp Hc Hc'.
......
Markdown is supported
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