module_refinement.v 6.66 KB
Newer Older
1 2 3 4 5 6
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
  CG_stack FG_stack stack_rules refinement.

Section Mod_refinement.
7
  Context `{HLR : logrelG Σ}.
8 9 10 11
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types Δ : listC D.
  Import lang.

12 13 14 15
  Program Definition sint {LG : logrelG Σ} {Z : stackPreG Σ} τi : prodC valC valC -n> iProp Σ := λne vv,
    ( γ (l stk stk' : loc), (vv.2) = (#stk', #l)%V  (vv.1) = #stk
       inv (stackN .@ (stk,stk')) (sinv' γ τi stk stk' l))%I.
  Solve Obligations with solve_proper.
16

17
  Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : PersistentP (sint τi vv).
18 19 20 21 22 23 24 25 26 27 28 29 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 57 58 59 60 61 62
  Proof. apply _. Qed.

  Lemma interp_subst_up_2 Δ1 Δ2 τ τi :
     τ  (Δ1 ++ Δ2)   τ.[upn (length Δ1) (ren (+1))]  (Δ1 ++ τi :: Δ2).
  Proof.
    revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto.
    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
    - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
    - unfold interp_expr. intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2.
    - apply fixpoint_proper=> τ' ww /=.
      properness; auto. apply (IHτ (_ :: _)).
    - intros vv; simpl.
      rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness.
      { by rewrite !lookup_app_l. }
      rewrite !lookup_app_r; [|lia ..].
      assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat.
      { lia. }
      rewrite Hwat. simpl. done.
    - unfold interp_expr.
      intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
    - intros vv; simpl; properness; auto. apply (IHτ (_ :: _)).
    - intros vv; simpl; properness; auto. by apply IHτ.
  Qed.
  Lemma interp_subst_2 τ τi Δ :
     τ  Δ   τ.[ren (+1)]  (τi :: Δ).
  Proof. by apply (interp_subst_up_2 []). Qed.

  Lemma bin_log_weaken_2 τi Δ Γ e1 e2 τ :
    {,;Δ;Γ}  e1 log e2 : τ -
    {,;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ}  e1 log e2 : τ.[ren (+1)].
  Proof.
    rewrite bin_log_related_eq /bin_log_related_def.
    iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
    iSpecialize ("Hlog" $! vvs with "Hs [HΓ]").
    { by rewrite interp_env_ren. }
    unfold interp_expr.
    iIntros (j K) "Hj /=".
    iMod ("Hlog" with "Hj") as "Hlog".
    iApply (wp_mono with "Hlog").
    iIntros (v). simpl.
    iDestruct 1 as (v') "[Hj Hτ]".
    iExists v'. iFrame.
    by rewrite -interp_subst_2.
  Qed.
  
63
  Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ :
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
    {,;Δ;Γ}  FG_stack.stackmod log CG_stack.stackmod : TForall $ TExists $ TProd (TProd
                                                 (TArrow TUnit (TVar 0))
                                                 (TArrow (TVar 0) (TSum TUnit (TVar 1))))
                                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
  Proof.
    unlock FG_stack.stackmod CG_stack.stackmod.
    iApply bin_log_related_tlam; auto.
    iIntros (τi Hτi) "!#".
    iApply (bin_log_related_pack _ (sint τi)).
    do 3 rel_tlam_l.
    do 3 rel_tlam_r.
    repeat iApply bin_log_related_pair.
    - iApply bin_log_related_arrow; eauto.
      iAlways. iIntros (? ?) "_".
      rel_seq_l.
      rel_seq_r.
      rel_alloc_l as istk "Histk". simpl.
      rel_alloc_l as stk "Hstk".
82
      rel_alloc_r as stk' "Hstk'".
83 84
      rel_alloc_r as l "Hl".
      rel_vals.
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
      rewrite -persistentP.
      iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
      pose (SG := StackG Σ _ γ).
      iAssert (prestack_owns γ ) with "[Hemp]" as "Hoe".
      { rewrite /prestack_owns big_sepM_empty fmap_empty.
        iFrame "Hemp". }
      iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
      iAssert (preStackLink γ τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
      { rewrite preStackLink_unfold.
        iExists _, _. iSplitR; simpl; trivial.
        iFrame "Histk". iLeft. iSplit; trivial. }
      iAssert (sinv' γ τi stk stk' l) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
      { iExists _, _, _. by iFrame. }
      iMod (inv_alloc (stackN.@(stk,stk')) with "[Hinv]") as "#Hinv".
      { iNext. iExact "Hinv". }
      iModIntro.
      iExists γ, l, stk, stk'. eauto.
102 103
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (? ?) "#Hvv /=".
104
      iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
105 106 107 108 109 110 111 112 113 114 115 116 117 118
      simplify_eq/=.
      rel_let_l.
      rel_let_r.
      Transparent FG_pop CG_locked_pop.
      rel_rec_l.
      rel_proj_r; rel_rec_r.
      unlock CG_locked_pop. simpl_subst/=.
      rel_proj_r.
      rel_let_r.
      replace (#();; acquire # l ;; let: "v" := (CG_pop #stk') #() in release # l ;; "v")%E with ((CG_locked_pop $/ LitV (Loc stk') $/ LitV (Loc l)) #())%E; last first.
      { unlock CG_locked_pop. simpl_subst/=. reflexivity. }
      replace (TSum TUnit (TVar 1))
      with (TSum TUnit (TVar 0)).[ren (+1)] by done.
      iApply bin_log_weaken_2.
119 120 121 122 123
      pose (SG := StackG Σ _ γ).
      change γ with stack_name.
      iApply (FG_CG_pop_refinement' (stackN.@(stk,stk'))).
      { solve_ndisj. }
      by rewrite sinv_unfold.
124 125 126
    - iApply bin_log_related_arrow_val; eauto.
      { unlock FG_push. done. }
      iAlways. iIntros (? ?) "#Hvv /=".
127
      iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
      simplify_eq/=.
      rel_let_r.
      Transparent FG_push.
      rel_rec_l.
      iApply bin_log_related_arrow_val; eauto.
      { unlock FG_push. simpl_subst/=. done. }
      { unlock FG_push. simpl_subst/=. solve_closed. }
      iAlways. iIntros (v v') "#Hτi /=".
      rel_let_r.
      rel_proj_r; rel_rec_r.
      unlock CG_locked_push. simpl_subst/=.
      rel_proj_r; rel_let_r.
      replace (let: "x" := v' in acquire # l ;; (CG_push #stk') "x" ;; release # l)%E
        with ((CG_locked_push $/ LitV stk' $/ LitV l) v')%E; last first.
      { unlock CG_locked_push. simpl_subst/=. done. }
      change TUnit with (TUnit.[ren (+1)]).
144 145 146 147 148 149
      pose (SG := StackG Σ _ γ).
      change γ with stack_name.
      iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "[Hinv] Hτi").
      { solve_ndisj. }
      by rewrite sinv_unfold.
  Qed.
150
End Mod_refinement.
151 152 153 154 155 156 157 158 159 160 161 162

Theorem module_ctx_refinement :
    FG_stack.stackmod ctx CG_stack.stackmod :
    TForall $ TExists $ TProd (TProd
                                 (TArrow TUnit (TVar 0))
                                 (TArrow (TVar 0) (TSum TUnit (TVar 1))))
                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
Proof.
  set (Σ := #[logrelΣ; GFunctor (authR stackUR)]).
  eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ].
  apply module_refinement.
Qed.