module_refinement.v 5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 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 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
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.
  Context `{logrelG Σ, stackG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types Δ : listC D.
  Import lang.

  Program Definition sint `{logrelG Σ, stackG Σ} τi : prodC valC valC -n> iProp Σ := λne vv,
    ( (l stk stk' : loc), (vv.2) = (# stk', # l)%V  (vv.1) = #stk
       inv stackN (sinv τi stk stk' l))%I.
  Next Obligation. solve_proper. Qed.

  Instance sint_persistent τi vv : PersistentP (sint τi vv).
  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.
  
  Lemma module_refinmenet Δ Γ :
    {,;Δ;Γ}  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".
      rel_alloc_r as stl' "Hstk'".
      rel_alloc_r as l "Hl".
      rel_vals.
      admit.
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (? ?) "#Hvv /=".
      iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
      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.
      by iApply FG_CG_pop_refinement'.
    - iApply bin_log_related_arrow_val; eauto.
      { unlock FG_push. done. }
      iAlways. iIntros (? ?) "#Hvv /=".
      iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)".
      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)]).
      iApply (FG_CG_push_refinement with "Hinv Hτi").
  Admitted.

End Mod_refinement.