refinement.v 16.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Import auth.
2
From iris.program_logic Require Import adequacy ectxi_language.
3
From iris_logrel.F_mu_ref_conc Require Import lang tactics soundness_binary notation.
4 5
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
From iris_logrel.F_mu_ref_conc.examples.stack Require Import
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  CG_stack FG_stack stack_rules.
7

8 9
Definition stackN : namespace := nroot .@ "stack".

10
Section Stack_refinement.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  Notation D := (prodC valC valC -n> iProp Σ).
13
  Implicit Types Δ : listC D.
14
  Import lang.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
  Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ
    := ( istk v h, (stack_owns h)
         stk' ↦ₛ v
         stk ↦ᵢ (FoldV (#istk))
         StackLink τi (#istk, v)
         l' ↦ₛ (#v false))%I.

  Ltac close_sinv Hcl asn :=
    iMod (Hcl with asn) as "_";
    [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.

  Definition CG_snap_iterV (st l : expr) : val :=
    RecV (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
  Definition FG_read_iterV (st : expr) : val :=
    RecV (App (FG_iter (Var 1)) (Load st.[ren (+2)])).


  Lemma FG_CG_iter_refinement ρ st st' (τi : D) l Δ {τP :  ww, PersistentP (τi ww)} {SH : stackG Σ}:
    spec_ctx ρ - inv stackN (sinv τi st st' l) -
     TArrow (TArrow (TVar 0) TUnit) TUnit  (τi::Δ) (FG_read_iterV (#st)%E, (CG_snap_iterV #st' #l)%E).
  Proof.
    iIntros "#Hs #Hinv". 
    iAlways. iIntros ([f1 f2]) "#Hff /=". 
    iIntros (j K) "Hj /=".
    
    iApply wp_rec; auto using to_of_val.
    iNext. simpl. rewrite FG_iter_subst. simpl.
    replace (FG_iter (of_val f1)) with (of_val (FG_iterV (of_val f1))) by (rewrite FG_iter_of_val; done).    
    wp_bind (Load #st)%E.
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
    iApply (wp_load with "Hst"). iNext. iIntros "Hst".
    tp_rec j; auto using to_of_val.
    tp_normalise j.
    rewrite CG_iter_subst CG_snap_subst. asimpl.
    replace (match @up_close namespace coPset nclose stackN return coPset with
       | @exist _ _ t2 _ =>
           @exist coPset_raw (fun t : coPset_raw => Is_true (coPset_wf t))
             match coPset_opp_raw t2 return coPset_raw with
             | coPLeaf b =>
                 match b return coPset_raw with
                 | true => coPLeaf true
                 | false => coPLeaf false
                 end
             | coPNode b l0 r => coPNode b l0 r
             end
             (coPset_intersection_wf (coPLeaf true) 
                (coPset_opp_raw t2) I (coPset_opp_wf t2))
       end) with (  stackN) by reflexivity.
    replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2))) by (rewrite CG_iter_of_val; done).        
    tp_bind j (App (CG_snap _ _) ())%E.
    iMod (steps_CG_snap with "[$Hs Hst' Hl Hj]") as "(Hj & Hst' & Hl)";  
      first solve_ndisj.
    { iFrame "Hst'". iFrame. }
    tp_normalise j.
    close_sinv "Hclose" "[Hoe Hst' Hst HLK Hl]".

    iLöb as "IH" forall (istk v) "HLK".

    iApply wp_rec; auto. iNext. asimpl.
    wp_bind (Unfold _). iApply wp_fold; auto. iNext.
    iModIntro. wp_bind (Load _).

    clear h.
    iInv stackN as (istk2 v' h) "[Hoe [Hst' [Hst [HLK' Hl]]]]" "Hclose".
    rewrite StackLink_unfold.
    iDestruct "HLK" as (istkl w) "[% [Histk HLK]]". simplify_eq/=.
    iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histkl Hoe]".
    iApply (wp_load with "Histkl"). iNext. iIntros "Histkl".
    iSpecialize ("Hoe" with "Histkl").
    close_sinv "Hclose" "[Hoe Hst Hst' HLK' Hl]".
    iDestruct "HLK" as "[[% %]|HLK]"; subst.
    + (* the stack is empty *)
      iApply wp_case_inl; auto.
      iNext.
      iApply fupd_wp.
      rewrite CG_iter_of_val /=.
      iMod (steps_CG_iter_end with "[$Hs $Hj]") as "Hj"; first solve_ndisj.
      iModIntro.
      iApply wp_value; auto.
      iExists UnitV. iFrame. eauto.
    + iDestruct "HLK" as (y1 z1 y2 z2) "[% [% [Hy Hsl]]]". subst.
      simpl.
      iApply wp_case_inr; first by rewrite /= ?to_of_val /=.
      iNext. asimpl.
      wp_bind (Fst _). iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=).
      iNext. iModIntro.
      wp_bind (App (of_val f1) _).
      rewrite CG_iter_of_val.
      iMod (steps_CG_iter with "[$Hs $Hj]") as "Hj"; first solve_ndisj.
      rewrite CG_iter_subst.
      tp_bind j (App (of_val f2) _).
      iSpecialize ("Hff" $! (y1, y2) with "Hy"). 
      iSpecialize ("Hff" $! j (K ++ _) with "Hj"). simpl.
      iApply (wp_wand with "Hff").
      iIntros (v). iDestruct 1 as (v2) "[Hj [% %]]".
      tp_normalise j. asimpl.
      iApply fupd_wp. tp_rec j; auto using to_of_val.
      asimpl.
      rewrite CG_iter_subst. asimpl.
      replace (CG_iter (of_val f2)) with (of_val (CG_iterV (of_val f2)))
          by (by rewrite CG_iter_of_val).
      tp_snd j; auto using to_of_val.
      tp_normalise j.
      iModIntro.
      iPoseProof "Hsl" as "Hsl'".
      rewrite {2}StackLink_unfold.
      iDestruct "Hsl'" as (zl w') "[% [Hzl Hsl']]". simplify_eq/=.
      iSpecialize ("IH" $! zl z2).
      iPoseProof (persistentP ((StackLink τi) (#zl, z2)) with "Hsl") as "Hsl_box".
      iSpecialize ("IH" with "Hsl_box").
      iSpecialize ("IH" with "Hj").
      iApply wp_rec; auto. iNext. asimpl.      
      wp_bind (Snd _). iApply wp_snd; auto using to_of_val.
  Qed.

  Lemma FG_CG_push_refinement ρ st st' (τi : D) l Δ {τP :  ww, PersistentP (τi ww)} {SH : stackG Σ}:
    spec_ctx ρ - inv stackN (sinv τi st st' l) -
     TArrow (TVar 0) TUnit  (τi::Δ) (FG_pushV (#st)%E, (CG_locked_pushV #st' #l)%E).
  Proof. 
    iIntros "#Hs #Hinv". 
    iAlways. iIntros ([v1 v2]) "#Hvv".
    iIntros (j K) "Hj /=".
    rewrite CG_locked_push_of_val.
    iLöb as "IH".
    iApply wp_rec; eauto using to_of_val. iNext.
    asimpl.
    wp_bind (Load #st)%E. 
    iApply wp_atomic; eauto.
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
    iModIntro. iApply (wp_load _ st 1 (FoldV #istk) with "Hst"). iNext.
    iIntros "Hst".
    close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]".
    iApply wp_rec; eauto using to_of_val. iNext. asimpl.
    wp_bind (ref (InjR _))%E.
    iApply wp_alloc.
    { simpl. rewrite ?to_of_val /=. auto. } iNext. iIntros (istk') "Histk'".    
    wp_bind (CAS _ _ _). clear v h.
    iInv stackN as (istk2 v h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".    (* TODO : why can we remove the later here?*) 
    destruct (decide (istk = istk2)) as [Heq|Hneq]; first subst istk.
    * (* Case CAS succeeds *)
      iMod (steps_CG_locked_push _ _ j K st' v2 with "[$Hj $Hs $Hst' $Hl]") as "[Hj [Hst' Hl]]"; first solve_ndisj.
      iApply (wp_cas_suc with "Hst"); auto.
      iNext. iIntros "Hst".

      iMod (stack_owns_alloc with "[$Hoe $Histk']") as "[Hoe Histk']".
      iMod ("Hclose" with "[HLK Hst Hoe Hl Hst' Histk']").
      { iNext. rewrite /sinv. iExists _,_,_.
        iFrame.
        rewrite (StackLink_unfold _ ((LocV istk'), _)).
        iExists _, _. iSplitR; auto.
        iFrame "Histk'".
        iRight. iExists _, _, _, _. auto.
      }
      iModIntro. iApply wp_if_true. iNext.
      iApply wp_value; eauto. iExists _; iSplitL; auto; simpl.
      done.
    * (* Case CAS fails *)
      iApply (wp_cas_fail with "Hst"); auto.
      congruence. iNext. iIntros "Hst".
      close_sinv "Hclose" "[HLK Hst Hoe Hl Hst' Histk']".
      iApply wp_if_false. iNext.
      iApply "IH". iFrame.
  Qed.

  Lemma FG_CG_pop_refinement ρ st st' (τi : D) l Δ {τP :  ww, PersistentP (τi ww)} {SH : stackG Σ}:
    spec_ctx ρ - inv stackN (sinv τi st st' l) -
     TArrow TUnit (TSum TUnit (TVar 0))  (τi::Δ) (FG_popV (#st)%E, (CG_locked_popV #st' #l)%E).
  Proof. 
    iIntros "#Hs #Hinv". 
    iAlways. iIntros ( [v1 v2] ) "[% %]". subst.
    iIntros (j K) "Hj /="; simplify_eq/=.
    rewrite CG_locked_pop_of_val FG_pop_of_val.
    iLöb as "IH".
    rewrite {2}(FG_pop_folding).
    iApply wp_rec; first by auto using to_of_val. iNext.
    rewrite -(FG_pop_folding #st)%E. asimpl.
    wp_bind (Load _).
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
    iApply (wp_load with "Hst"). iNext. iIntros "Hst".
    iPoseProof "HLK" as "HLK'".
    (* Checking whether the stack is empty *)
    rewrite {2}StackLink_unfold.
    iDestruct "HLK'" as (istk2 w) "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=.
    + iMod (steps_CG_locked_pop_fail with "[$Hs $Hst' $Hl $Hj]")
        as "(Hj & Hstk' & Hl)"; first solve_ndisj.
      close_sinv "Hclose" "[Hoe Hstk' Hst Hl]".
      wp_bind (Unfold _). iApply wp_fold; first by auto using to_of_val.    iNext.
      iModIntro. iApply wp_rec; first auto using to_of_val. iNext. asimpl.
      clear h.
      wp_bind (Load _). iClear "HLK".
      iInv stackN as (istk3 w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
      iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
      iApply (wp_load with "Histk"). iNext. iIntros "Histk".
      iSpecialize ("HLoe"  with "Histk").
      close_sinv "Hclose" "[HLoe Hst' Hst HLK Hl]".
      iApply wp_rec; first by auto. iNext. asimpl.
      iApply wp_case_inl; auto. iNext.
      iApply wp_value; auto. 
      iExists (InjLV ())%V. iFrame "Hj".
      iLeft. iExists (_,_). iSplit; auto.
    + close_sinv "Hclose" "[Hoe Hst' Hst Hl]".
      wp_bind (Unfold _). iApply wp_fold; first auto. iNext.
      iApply wp_rec; first auto. iNext. asimpl.
      wp_bind (Load _).
      clear h.
      iClear "HLK".
      iInv stackN as (istk3 w' h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
      iDestruct (stack_owns_later_open_close with "Hoe Hmpt") as "[Histk HLoe]".
      iApply (wp_load with "Histk"). iNext; iIntros "Histk".
      iSpecialize ("HLoe" with "Histk").
      close_sinv "Hclose" "[HLoe Hl Hst Hst' HLK]".
      iApply wp_rec; first auto using to_of_val. iNext. asimpl.
      iDestruct "HLK'" as (y1 z1 y2 z2) "(% & % & Hτ & HLK2)"; subst.
      simpl.
      iApply wp_case_inr. 
      { by rewrite /= ?to_of_val /=. } iNext.
      asimpl.
      wp_bind (Snd _). 
      iApply wp_snd; try by (rewrite /= to_of_val /=).  iNext.      
      (* now to decide if CAS succeeds or not *)
      iClear "HLK2". clear h. iModIntro.
      wp_bind (CAS _ _ _).
      iInv stackN as (istk w h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
      (* deciding whether CAS will succeed or fail *)
      destruct (decide (istk = istk2)) as [Heq|Hneq]; subst.
      * (* CAS successful *)
        iApply (wp_cas_suc with "Hst"); try by (rewrite /= ?to_of_val /=).
        iNext. iIntros "Hst".
        iPoseProof "HLK" as "HLK'".
        rewrite {2}StackLink_unfold.
        iDestruct "HLK'" as (? ?) "[% [Hmpt' HLK']]"; simplify_eq/=.
        iDestruct (stack_mapstos_agree with "[$Hmpt $Hmpt']") as "%". subst.
        iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
        iDestruct "HLK'" as (yn1 yn2 zn1 zn2)
                                   "[% [% [#Hrel HLK'']]]"; simplify_eq/=.
        (* Now we have proven that specification can also pop. *)
        iMod (steps_CG_locked_pop_suc with "[$Hs $Hst' $Hl $Hj]")
                as "[Hj [Hst' Hl]]"; first solve_ndisj.
        iMod ("Hclose" with "[-Hj]") as "_".
        { iNext. 
          iPoseProof "HLK''" as "HLK2".
          rewrite {2}(StackLink_unfold _ (yn2, zn2)).
          iDestruct "HLK2" as (yn2loc ?) "[% _]"; simplify_eq /=.
          iExists _,_,_. iFrame. iFrame "HLK''". }
        iModIntro.
        iApply wp_if_true. iNext.
        wp_bind (Fst _). 
        iApply wp_fst; try by (auto using to_of_val || rewrite /= ?to_of_val /=). iNext.
        iModIntro.
        iApply wp_value; try by rewrite /= ?to_of_val /=.
        iExists (InjRV zn1). iFrame "Hj".
        iRight. iExists (_,_). simpl. iSplit; auto.
      * (* CAS fails *)
        iApply (wp_cas_fail with "Hst"); try by (rewrite /= ?to_of_val /=).
        congruence.        
        iNext. iIntros "Hst".
        close_sinv "Hclose" "[-Hj]".
        iApply wp_if_false. iNext. 
        by iApply "IH".
  Qed.
    
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
278 279 280 281 282
  Lemma FG_CG_counter_refinement :
    []  FG_stack log CG_stack : TForall (TProd (TProd
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
283 284
  Proof.
    (* executing the preambles *)
Robbert Krebbers's avatar
Robbert Krebbers committed
285
    iIntros (Δ [|??] ρ ?) "#[Hspec HΓ]"; iIntros (j K) "Hj"; last first.
286
    { iDestruct (interp_env_length with "HΓ") as %[=]. } 
287 288
    iClear "HΓ". cbn -[FG_stack CG_stack]. 
    rewrite ?empty_env_subst /CG_stack /FG_stack. 
289
    iApply wp_value; eauto.
290 291 292 293 294 295 296 297 298 299 300 301 302 303
    iExists (Λ: _)%V; iFrame "Hj".
    fold (interp (TProd (TProd
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit))).
    clear j K. iAlways. iIntros (τi) "%". 
    iIntros (j K) "Hj /=".
    iApply fupd_wp.
    tp_tlam j.
    tp_bind j newlock.
    iMod (steps_newlock with "[$Hj]") as (l') "[Hj Hl']"; eauto.
    tp_normalise j.
    tp_rec j.
    tp_alloc j as stk' "Hstk'".
304 305
    rewrite CG_locked_push_subst CG_locked_pop_subst
            CG_iter_subst CG_snap_subst. simpl. asimpl.
306 307 308 309 310 311 312 313 314 315 316
    tp_normalise j.
    tp_rec j.
    tp_normalise j. rewrite ?CG_locked_push_subst ?CG_locked_pop_subst
            ?CG_iter_subst ?CG_snap_subst. simpl. asimpl.
    iApply wp_tlam. iNext.
    wp_bind (ref (InjL _))%E. iApply wp_alloc; eauto. iNext. iIntros (l) "Hl".
    wp_bind (ref _)%E. iApply wp_alloc; eauto. iNext. iIntros (stk) "Hstk".
    iApply wp_rec; eauto. iNext.
    simpl. rewrite FG_push_subst FG_pop_subst FG_iter_subst /=.
    asimpl.

317
    (* establishing the invariant *)
318
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
319 320
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
    change H1 with (@stack_inG _ istkG).
    clearbody istkG. clear γ H1.
323
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
324 325 326
    { rewrite /stack_owns big_sepM_empty. eauto. }
    iMod (stack_owns_alloc with "[$Hoe $Hl]") as "[Hoe Hls]".
    iAssert (StackLink τi (#l, FoldV (InjLV UnitV))) with "[Hls]" as "HLK".
327 328
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
      iFrame "Hls". iLeft. iSplit; trivial. }
330 331 332 333
    iAssert (sinv τi stk stk' l') with "[Hoe Hstk Hstk' HLK Hl']" as "Hinv".
    { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl' HLK". }
    iMod (inv_alloc stackN with "[$Hinv]") as "#Hinv". 
    clear l.
334
    Opaque stack_owns.
335

336
    (* splitting *)
337
    iApply wp_value; first by eauto. 
338
    iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)).
339
    simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".   
340 341 342 343
    iExists (_, _), (_, _); iSplit; eauto.
    iSplit.
    (* refinement of push and pop *)
    - iExists (_, _), (_, _); iSplit; eauto. iSplit.
344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
      + simpl.
        (* TODO: fold (interp (...)) does not work here *)
        replace ( ( vv : prodC valC valC, τi vv
           interp_expr interp_unit (τi :: Δ)
         ((of_val
             ((RecV
                 ((rec: if: CAS #stk (Var 1)
                              (Fold (ref InjR (Var 3, Var 1))) then 
                        () else (Var 2) (Var 3))%E 
                    (! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).1))
            (of_val (vv.1)),
         (of_val
            ((RecV
                ((rec: if: CAS #stk (Var 1)
                             (Fold (ref InjR (Var 3, Var 1))) then 
                       () else (Var 2) (Var 3))%E 
                   (! #stk)%E), CG_locked_pushV (#stk')%E (#l')%E).2))
           (of_val (vv.2)))))%I
        with
        (interp (TArrow (TVar 0) TUnit) (τi :: Δ)
                    ((FG_pushV (#stk)%E)%V,
                      (CG_locked_pushV (#stk')%E (#l')%E))); last first.
        { simpl. unlock. (* TODO: WTF???? *) auto. }
        iApply (FG_CG_push_refinement with "Hspec Hinv").
      + simpl.
        iApply (FG_CG_pop_refinement with "Hspec Hinv").
    - iApply (FG_CG_iter_refinement _ _ _ _ _ Δ with "Hspec Hinv").
   Unshelve. auto. (* TODO why is this goal coming up anyway? *)
372
  Qed.
373 374
End Stack_refinement.

375
Theorem stack_ctx_refinement :
Robbert Krebbers's avatar
Robbert Krebbers committed
376
  []  FG_stack ctx CG_stack : TForall (TProd (TProd
377 378
        (TArrow (TVar 0) TUnit)
        (TArrow TUnit (TSum TUnit (TVar 0))))
Robbert Krebbers's avatar
Robbert Krebbers committed
379
        (TArrow (TArrow (TVar 0) TUnit) TUnit)).
380
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
381 382
  set (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR); GFunctor (authR stackUR)]).
  set (HG := soundness_unary.HeapPreIG Σ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  eapply (binary_soundness Σ); eauto using FG_stack_closed, CG_stack_closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
384
  intros; apply FG_CG_counter_refinement.
385
Qed.