soundness_binary.v 2.57 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref_conc Require Export context_refinement.
Amin Timany's avatar
Amin Timany committed
2 3 4
From iris.algebra Require Import auth frac agree.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Amin Timany's avatar
Amin Timany committed
5
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_unary.
Amin Timany's avatar
Amin Timany committed
6 7 8 9

Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
    e e' τ v thp hp :
  ( `{heapIG Σ, cfgSG Σ}, []  e log e' : τ) 
Ralf Jung's avatar
Ralf Jung committed
10 11
  rtc erased_step ([e], ) (of_val v :: thp, hp) 
  ( thp' hp' v', rtc erased_step ([e'], ) (of_val v' :: thp', hp')).
Amin Timany's avatar
Amin Timany committed
12 13
Proof.
  intros Hlog Hsteps.
Ralf Jung's avatar
Ralf Jung committed
14
  cut (adequate NotStuck e  (λ _ _,  thp' h v, rtc erased_step ([e'], ) (of_val v :: thp', h))).
Amin Timany's avatar
Amin Timany committed
15
  { destruct 1; naive_solver. }
Ralf Jung's avatar
Ralf Jung committed
16
  eapply (wp_adequacy Σ _); iIntros (Hinv ?).
Amin Timany's avatar
Amin Timany committed
17
  iMod (own_alloc ( to_gen_heap )) as (γ) "Hh".
Hai Dang's avatar
Hai Dang committed
18
  { by apply auth_auth_valid, to_gen_heap_valid. }
Amin Timany's avatar
Amin Timany committed
19 20
  iMod (own_alloc ( (to_tpool [e'], )
      ((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
Hai Dang's avatar
Hai Dang committed
21
  { apply auth_both_valid. split=>//. split=>//. apply to_tpool_valid. }
Amin Timany's avatar
Amin Timany committed
22 23 24 25
  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. }
  set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
Ralf Jung's avatar
Ralf Jung committed
26
  iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
Amin Timany's avatar
Amin Timany committed
27 28
  iApply wp_fupd. iApply wp_wand_r.
  iSplitL.
29 30 31 32
  iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
  { iSplit.
    - by iExists ([e'], ).
    - by iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
Amin Timany's avatar
Amin Timany committed
33
  simpl.
Amin Timany's avatar
Amin Timany committed
34 35 36
  replace e with e.[env_subst[]] at 2 by by asimpl.
  iApply ("Hrel" $! 0 []).
  { rewrite /tpool_mapsto. asimpl. by iFrame. }
Amin Timany's avatar
Amin Timany committed
37 38 39 40
  iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
  iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
  rewrite /tpool_mapsto /=.
  iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
Hai Dang's avatar
Hai Dang committed
41
  move: Hvalid=> /auth_both_valid
Amin Timany's avatar
Amin Timany committed
42 43 44 45 46 47 48 49
    [/prod_included [/tpool_singleton_included Hv2 _] _].
  destruct tp as [|? tp']; simplify_eq/=.
  iMod ("Hclose" with "[-]") as "_"; [iExists (_ :: tp'), σ; auto|].
  iIntros "!> !%"; eauto.
Qed.

Lemma binary_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
    Γ e e' τ :
Amin Timany's avatar
Amin Timany committed
50
  (Γ  e : τ)  (Γ  e' : τ) 
Amin Timany's avatar
Amin Timany committed
51 52 53
  ( `{heapIG Σ, cfgSG Σ}, Γ  e log e' : τ) 
  Γ  e ctx e' : τ.
Proof.
Amin Timany's avatar
Amin Timany committed
54 55 56 57
  intros He He' Hlog; repeat split; auto.
  intros K thp σ v ?. eapply (basic_soundness Σ _)=> ??.
  eapply (bin_log_related_under_typed_ctx _ _ _ _ []);
    eauto using typed_n_closed.
Amin Timany's avatar
Amin Timany committed
58
Qed.