Commit f2cd21a3 authored by Dan Frumin's avatar Dan Frumin

Extend the definition of contextual refinement to cover all EqTypes

parent 6c2be7bd
......@@ -188,8 +188,9 @@ Proof.
Qed.
Definition ctx_refines (Γ : stringmap type)
(e e' : expr) (τ : type) : Prop := K thp σ v,
typed_ctx K Γ τ TUnit
(e e' : expr) (τ : type) : Prop := K thp σ v τ',
ObsType τ'
typed_ctx K Γ τ τ'
rtc step ([fill_ctx K e], ) (of_val v :: thp, σ)
thp' σ', rtc step ([fill_ctx K e'], ) (of_val v :: thp', σ').
Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
......
......@@ -335,6 +335,35 @@ Section logrel.
+ iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
rewrite IHHτ2. by iDestruct "H1" as "%"; subst.
Qed.
(* Observable types are, at the moment, exactly the types which support equality. *)
Definition ObsType : type Prop := EqType.
(* TODO: derive this from [interp_EqType_agree] *)
(* This formulation is more suitable for proving soundness of the logical relation in [soundness_binary.v] *)
Lemma interp_ObsType_agree τ : (v v' : val),
τ [] (v, v') ObsType τ v = v'⌝.
Proof.
induction τ; iIntros (v v') "HI"; simpl; eauto;
try by (iPureIntro; inversion 1).
- iDestruct "HI" as "[% %]"; subst; eauto.
- iDestruct "HI" as (n) "[% %]"; subst; eauto.
- iDestruct "HI" as (b) "[% %]"; subst; eauto.
- iDestruct "HI" as ([v1 v1'] [v2 v2']) "/= [% [H1 H2]]".
simplify_eq/=.
iDestruct (IHτ1 with "H1") as %IH1.
iDestruct (IHτ2 with "H2") as %IH2.
iPureIntro. inversion 1; simplify_eq.
rewrite IH1; auto.
by rewrite IH2.
- iDestruct "HI" as "[HI | HI]";
iDestruct "HI" as ([w w']) "[% HI]"; simplify_eq/=.
+ iDestruct (IHτ1 with "HI") as %IH1. iPureIntro.
inversion 1. by rewrite IH1.
+ iDestruct (IHτ2 with "HI") as %IH2. iPureIntro.
inversion 1. by rewrite IH2.
Qed.
End logrel.
Typeclasses Opaque interp_env.
......
......@@ -9,30 +9,11 @@ Class heapPreIG Σ := HeapPreIG {
heap_preG_heap :> gen_heapPreG loc val Σ
}.
(* In order to obtain the soundness results (typesafety and
refinement) we need to generalize the contextual refinement to
arbitrary types. For types which values we can observe ([obsTy]), it
is the case that two related values are equal. *)
Definition obsTy : type -> Prop := fun ty =>
match ty with
| TUnit | TNat | TBool => True
| _ => False
end.
Lemma interp_obsTy_eq Σ `{heapIG Σ, cfgSG Σ} (v v' : val) τ :
τ [] (v, v') obsTy τ v = v'⌝.
Proof.
induction τ; iIntros "HI"; simpl; eauto.
- iDestruct "HI" as "[% %]"; subst; eauto.
- iDestruct "HI" as (n) "[% %]"; subst; eauto.
- iDestruct "HI" as (b) "[% %]"; subst; eauto.
Qed.
Lemma logrel_adequate Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ σ :
( `{heapIG Σ, cfgSG Σ}, e log e' : τ)
adequate e σ (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h)
(obsTy τ v = v')).
(ObsType τ v = v')).
Proof.
intros Hlog.
eapply (wp_adequacy Σ _); iIntros (Hinv).
......@@ -65,7 +46,7 @@ Proof.
destruct tp as [|? tp']; simplify_eq/=.
iMod ("Hclose" with "[-]") as "_".
{ iExists (_ :: tp'), σ'. eauto. }
iDestruct (interp_obsTy_eq with "Hinterp") as %Hobs.
iDestruct (interp_ObsType_agree with "Hinterp") as %Hobs.
iIntros "!> !%"; eauto.
Qed.
......@@ -76,7 +57,7 @@ Theorem logrel_typesafety Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} e τ e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??.
cut (adequate e σ (λ v, thp' h v', rtc step ([e], ) (of_val v' :: thp', h) (obsTy τ v = v'))); first (intros [_ ?]; eauto).
cut (adequate e σ (λ v, thp' h v', rtc step ([e], ) (of_val v' :: thp', h) (ObsType τ v = v'))); first (intros [_ ?]; eauto).
eapply logrel_adequate; eauto.
Qed.
......@@ -84,10 +65,10 @@ Lemma logrel_simul Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp :
( `{heapIG Σ, cfgSG Σ}, e log e' : τ)
rtc step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp') (obsTy τ v = v')).
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp') (ObsType τ v = v')).
Proof.
intros Hlog Hsteps.
cut (adequate e (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) (obsTy τ v = v'))).
cut (adequate e (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) (ObsType τ v = v'))).
{ destruct 1; naive_solver. }
eapply logrel_adequate; eauto.
Qed.
......@@ -99,8 +80,8 @@ Lemma logrel_ctxequiv Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
( `{heapIG Σ, cfgSG Σ}, Γ e log e' : τ)
Γ e ctx e' : τ.
Proof.
intros He He' Hlog K thp σ v ? Hstep.
cut ( thp' hp' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', hp') (obsTy TUnit v = v')).
intros He He' Hlog K thp σ ? τ' ? ? Hstep.
cut ( thp' hp' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', hp') (ObsType τ' v = v')).
{ naive_solver. }
eapply (logrel_simul Σ _); last by apply Hstep.
intros ??.
......
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