soundness_binary.v 3.53 KB
Newer Older
1
From iris_logrel.F_mu_ref_conc Require Export context_refinement adequacy.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.algebra Require Import auth frac agree.
3
From iris.base_logic Require Import big_op lib.auth.
4
From iris.proofmode Require Import tactics.
5

6 7 8
Class logrelPreG Σ := LogrelPreG {
  logrel_preG_heap :> heapPreG Σ;
  logrel_preG_cfg  :> inG Σ (authR cfgUR)
9
}.
10

11 12 13 14 15
Definition logrelΣ : gFunctors := #[heapΣ; authΣ cfgUR].
Instance subG_heapPreG {Σ} : subG logrelΣ Σ  logrelPreG Σ.
Proof. solve_inG. Qed.

Lemma logrel_adequate Σ `{logrelPreG Σ}
16
    e e' τ σ :
17
  ( `{logrelG Σ},   e log e' : τ) 
18
  adequate e σ (λ v,  thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) 
19
     (ObsType τ  v = v')).
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Proof.
21
  intros Hlog.
22
  eapply (heap_adequacy Σ _); iIntros (Hinv).
23
  iMod (own_alloc ( (to_tpool [e'], )
Dan Frumin's avatar
Dan Frumin committed
24
      ((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
25
  { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
26
  set (Hcfg := LogrelG _ _ _ γc).
27
  iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg".
28 29 30
  { iNext. iExists [e'], . 
    rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
  iApply wp_fupd. iApply wp_wand_r.
Dan Frumin's avatar
Dan Frumin committed
31
  iSplitL.
32
  - iPoseProof (Hlog _) as "Hrel".
33
    rewrite bin_log_related_eq /bin_log_related_def.
34
    iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
35
    { iApply logrel_binary.interp_env_nil. }
36
    rewrite /env_subst !fmap_empty !subst_p_empty. 
37
    iApply fupd_wp.
38 39
    iApply ("Hrel" $! 0 []). simpl.
    rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
40
  - iIntros (v1).
41 42 43 44 45 46 47 48 49
    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. }
50
    iDestruct (interp_ObsType_agree with "Hinterp") as %Hobs.
51 52 53 54
    iIntros "!> !%"; eauto.
Qed.


55 56
Theorem logrel_typesafety Σ `{logrelPreG Σ} e τ e' thp σ σ' :
  ( `{logrelG Σ},   e log e : τ) 
57 58 59 60
  rtc step ([e], σ) (thp, σ')  e'  thp 
  is_Some (to_val e')  reducible e' σ'.
Proof.
  intros Hlog ??.
61
  cut (adequate e σ (λ v,  thp' h v', rtc step ([e], ) (of_val v' :: thp', h)  (ObsType τ  v = v'))); first (intros [_ ?]; eauto).
62 63 64
  eapply logrel_adequate; eauto.
Qed.

65
Lemma logrel_simul Σ `{logrelPreG Σ}
66
    e e' τ v thp hp :
67
  ( `{logrelG Σ},   e log e' : τ) 
68
  rtc step ([e], ) (of_val v :: thp, hp) 
69
  ( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp')  (ObsType τ  v = v')).
70 71
Proof.
  intros Hlog Hsteps.
72
  cut (adequate e  (λ v,  thp' h v', rtc step ([e'], ) (of_val v' :: thp', h)  (ObsType τ  v = v'))).
73 74
  { destruct 1; naive_solver. }
  eapply logrel_adequate; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Qed.
76

77 78 79 80
Lemma logrel_ctxequiv Σ `{logrelPreG Σ} Γ e e' τ :
  Closed (dom _ Γ) e 
  Closed (dom _ Γ) e' 
  ( `{logrelG Σ}, Γ  e log e' : τ) 
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  Γ  e ctx e' : τ.
Proof.
83 84
  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')).
85 86
  { naive_solver. }
  eapply (logrel_simul Σ _); last by apply Hstep.
87
  intros ?.
88
  iApply (bin_log_related_under_typed_ctx _ _ _ _ ); eauto.
89
  iPoseProof (Hlog _) as "Hrel". auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.