Commit ac24a813 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for ctx_refines.

parent 0770367b
......@@ -189,6 +189,8 @@ Definition ctx_refines (Γ : list type)
typed_ctx K Γ τ [] TUnit
rtc step ([fill_ctx K e], ) (# v :: thp, σ)
thp' σ' v', rtc step ([fill_ctx K e'], ) (# v' :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
(ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ}.
......@@ -357,12 +357,11 @@ Section CG_Counter.
End CG_Counter.
Definition Σ := #[auth.authGF heapUR; auth.authGF cfgUR].
Theorem counter_ctx_refinement :
ctx_refines [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
[] FG_counter ctx CG_counter :
TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
set (Σ := #[auth.authGF heapUR; auth.authGF cfgUR]).
eapply (@binary_soundness Σ);
auto using FG_counter_closed, CG_counter_closed, FG_CG_counter_refinement.
all: typeclasses eauto.
......@@ -368,14 +368,13 @@ Section Stack_refinement.
End Stack_refinement.
Definition Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR].
Theorem stack_ctx_refinement :
ctx_refines [] FG_stack CG_stack (TForall (TProd (TProd
[] FG_stack ctx CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit))).
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
set (Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR]).
eapply (@binary_soundness Σ);
eauto using FG_stack_closed, CG_stack_closed.
all: try typeclasses eauto.
......@@ -81,7 +81,7 @@ Section soundness.
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : ctx_PersistentP Δ), Δ Γ e log e' : τ)
ctx_refines Γ e e' τ.
Γ e ctx e' : τ.
intros H1 K HK htp hp v Hstp Hc Hc'.
eapply basic_soundness; eauto.
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