module_refinement.v 4.84 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

Dan Frumin committed
17
  Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : Persistent (sint τi vv).
18 19
  Proof. apply _. Qed.
  
20
  Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ :
21
    {Δ;Γ}  FG_stack.stackmod log CG_stack.stackmod : TForall $ TExists $ TProd (TProd
22 23 24 25 26 27
                                                 (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.
28
    iIntros (τi) "!#".
29
    iApply (bin_log_related_pack (sint τi)).
30 31 32 33 34 35 36 37 38
    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".
39
      rel_alloc_r as stk' "Hstk'".
40 41
      rel_alloc_r as l "Hl".
      rel_vals.
Dan Frumin committed
42
      rewrite -persistent.
43 44 45 46 47 48
      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]".
49
      iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK".
50 51 52 53 54 55 56 57 58
      { 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.
59 60
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (? ?) "#Hvv /=".
61
      iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
62 63 64 65 66 67 68 69 70 71 72 73 74
      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.
Dan Frumin committed
75
      iApply bin_log_related_weaken_2.
76 77 78 79 80
      pose (SG := StackG Σ _ γ).
      change γ with stack_name.
      iApply (FG_CG_pop_refinement' (stackN.@(stk,stk'))).
      { solve_ndisj. }
      by rewrite sinv_unfold.
81 82 83
    - iApply bin_log_related_arrow_val; eauto.
      { unlock FG_push. done. }
      iAlways. iIntros (? ?) "#Hvv /=".
84
      iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)".
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
      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)]).
101 102 103 104 105 106
      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.
107
End Mod_refinement.
108 109 110 111 112 113 114 115 116 117 118 119

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.