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

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
  Program Definition sint τ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.
15
  Solve Obligations with solve_proper.
16

17
  Instance sint_persistent τi vv : Persistent (sint τi vv).
18
  Proof. apply _. Qed.
19 20

  Lemma module_refinement Δ Γ :
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
      iAssert (sinv τi stk stk' l) with "[-]" as "Hinv".
      { iExists _,_. iFrame.
        rewrite stack_link_unfold. iExists _; iSplitL; eauto. }
46 47 48
      iMod (inv_alloc (stackN.@(stk,stk')) with "[Hinv]") as "#Hinv".
      { iNext. iExact "Hinv". }
      iModIntro.
49
      iExists l, stk, stk'. eauto.
50 51
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (? ?) "#Hvv /=".
52
      iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
53 54 55 56 57 58 59 60 61 62 63 64 65
      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
66
      iApply bin_log_related_weaken_2.
67 68
      iApply (FG_CG_pop_refinement' (stackN.@(stk,stk')) with "Hinv").
      solve_ndisj.
69 70 71
    - iApply bin_log_related_arrow_val; eauto.
      { unlock FG_push. done. }
      iAlways. iIntros (? ?) "#Hvv /=".
72
      iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
      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)]).
89 90
      iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "Hinv Hτi").
      solve_ndisj.
91
  Qed.
92
End Mod_refinement.
93 94 95 96 97 98 99 100

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.
101
  eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
102 103
  apply module_refinement.
Qed.