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 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  iApply wp_fupd. iApply (wp_wand with "[-]").
  - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
    { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
    rewrite (empty_env_subst e). iApply ("Hrel" $! []).
    rewrite /tpool_mapsto (empty_env_subst e'). asimpl. iFrame.
  - 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.