soundness_binary.v 2.47 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref 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 Require Import soundness.
Amin Timany's avatar
Amin Timany committed
6 7 8 9

Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
    e e' τ v thp hp :
  ( `{heapG Σ, 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 16
  { destruct 1; naive_solver. }
  eapply (wp_adequacy Σ); first by apply _.
Ralf Jung's avatar
Ralf Jung committed
17
  iIntros (Hinv ?).
Amin Timany's avatar
Amin Timany committed
18 19 20 21 22 23 24 25 26 27 28
  iMod (own_alloc ( to_gen_heap )) as (γ) "Hh".
  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ )). }
  iMod (own_alloc ( (Excl' e', )
      ((Excl' e', ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
  { apply auth_valid_discrete_2. split=>//. }
  set (Hcfg := CFGSG _ _ γc).
  iMod (inv_alloc specN _ (spec_ctx ([e'], )) with "[Hcfg1]") as "#Hcfg".
  { iNext. iExists e', . iSplit; eauto.
    rewrite /to_gen_heap fin_maps.map_fmap_empty.
    iFrame. }
  set (HeapΣ := HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ)).
Ralf Jung's avatar
Ralf Jung committed
29
  iExists (λ σ _, own γ ( to_gen_heap σ)); iFrame.
Amin Timany's avatar
Amin Timany committed
30 31 32
  iApply wp_fupd. iApply (wp_wand with "[-]").
  - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
    { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
Amin Timany's avatar
Amin Timany committed
33 34 35
    replace e with e.[env_subst[]] at 2 by by asimpl.
    iApply ("Hrel" $! []).
    rewrite /tpool_mapsto. asimpl. iFrame.
Amin Timany's avatar
Amin Timany committed
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
  - iModIntro. iIntros (v'). iDestruct 1 as (v2) "[Hj #Hinterp]".
    iInv specN as ">Hinv" "Hclose".
    iDestruct "Hinv" as (e'' σ) "[Hown %]".
    rewrite /tpool_mapsto /=.
    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
    move: Hvalid=> /auth_valid_discrete_2
      [/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
    iMod ("Hclose" with "[-]") as "_".
    + iExists (#v2), σ. auto.
    + iIntros "!> !%". eauto.
Qed.

Lemma binary_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
    Γ e e' τ :
  ( f, e.[upn (length Γ) f] = e) 
  ( f, e'.[upn (length Γ) f] = e') 
  ( `{heapG Σ, cfgSG Σ}, Γ  e log e' : τ) 
  Γ  e ctx e' : τ.
Proof.
  intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ??.
  eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
Qed.