Commit b8326b06 authored by Dan Frumin's avatar Dan Frumin

Add a type safety proof from the binary interpretation

parent ba7fbfe9
......@@ -9,58 +9,76 @@ Class heapPreIG Σ := HeapPreIG {
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp :
Lemma logrel_adequate Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ σ :
( `{heapIG Σ, cfgSG Σ}, e log e' : τ)
rtc step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')).
adequate e σ (λ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h)).
Proof.
intros Hlog Hsteps.
cut (adequate e (λ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))).
{ destruct 1; naive_solver. }
eapply (wp_adequacy Σ _); iIntros (Hinv).
iMod (own_alloc ( to_gen_heap )) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ )). }
intros Hlog.
eapply (wp_adequacy Σ _); iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
iMod (own_alloc ( (to_tpool [e'], )
((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
set (Hcfg := CFGSG _ _ γc).
set (Hcfg := CFGSG _ _ γc).
iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg".
{ iNext. iExists [e'], . rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
{ iNext. iExists [e'], .
rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
iApply wp_fupd.
iApply wp_wand_r.
iApply wp_fupd. iApply wp_wand_r.
iSplitL.
iPoseProof (Hlog _ _) as "Hrel".
iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
{ iAlways. iApply logrel_binary.interp_env_nil. }
simpl.
rewrite /env_subst ?fmap_empty ?subst_p_empty.
iSpecialize ("Hrel" $! 0 []).
iAssert (0 e')%I with "[Hcfg2]" as "H0".
{ rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame. }
iApply fupd_wp. iApply "Hrel"; auto.
iModIntro. iIntros (v1).
iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
iMod ("Hclose" with "[-]") as "_"; [iExists (_ :: tp'), σ; auto|].
iIntros "!> !%"; eauto.
- iPoseProof (Hlog _ _) as "Hrel".
iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
{ iAlways. iApply logrel_binary.interp_env_nil. }
rewrite /env_subst !fmap_empty !subst_p_empty.
iApply ("Hrel" $! 0 []). simpl.
rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
- iModIntro. iIntros (v1).
iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
move: Hvalid=> /auth_valid_discrete_2
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
iMod ("Hclose" with "[-]") as "_".
{ iExists (_ :: tp'), σ'. eauto. }
iIntros "!> !%"; eauto.
Qed.
Theorem logrel_typesafety Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} e τ e' thp σ σ' :
( `{heapIG Σ, cfgSG Σ}, e log e : τ)
rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??.
cut (adequate e σ (λ _, thp' h v, rtc step ([e], ) (of_val v :: thp', h))); first (intros [_ ?]; eauto).
eapply logrel_adequate; eauto.
Qed.
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')).
Proof.
intros Hlog Hsteps.
cut (adequate e (λ _, thp' h v, rtc step ([e'], ) (of_val v :: thp', h))).
{ destruct 1; naive_solver. }
eapply logrel_adequate; eauto.
Qed.
Lemma binary_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
Lemma logrel_ctxequiv Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
Γ e e' τ :
(Closed (dom _ Γ) e)
(Closed (dom _ Γ) e')
( `{heapIG Σ, cfgSG Σ}, Γ e log e' : τ)
Γ e ctx e' : τ.
Proof.
intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
intros He He' Hlog K thp σ v ?. eapply (logrel_simul Σ _)=> ??.
iApply (bin_log_related_under_typed_ctx _ _ _ _ ); eauto.
iPoseProof (Hlog _ _) as "Hrel". auto.
Qed.
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