counter.v 19.8 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris.algebra Require Import auth.
3
From iris_logrel.F_mu_ref_conc Require Export examples.lock.
4
From iris_logrel.F_mu_ref_conc Require Import tactics soundness_binary relational_properties.
5
From iris.program_logic Require Import adequacy.
6

7
Definition CG_increment (x : expr) : expr :=
8
  Rec (Store x.[ren (+ 2)] (BinOp Add (#n 1) (Load x.[ren (+ 2)]))).
9 10 11 12 13 14

Definition CG_locked_increment (x l : expr) : expr :=
  with_lock (CG_increment x) l.
Definition CG_locked_incrementV (x l : expr) : val :=
  with_lockV (CG_increment x) l.

15 16
Definition counter_read (x : expr) : expr := Rec (Load x.[ren (+2)]).
Definition counter_readV (x : expr) : val := RecV (Load x.[ren (+2)]).
17 18 19 20 21

Definition CG_counter_body (x l : expr) : expr :=
  Pair (CG_locked_increment x l) (counter_read x).
Definition CG_counter : expr :=
  App
22
    (Rec $ App (Rec (CG_counter_body (Var 1) (Var 3)))
23
               (Alloc (#n 0)))
24 25 26
    newlock.

Definition FG_increment (x : expr) : expr :=
27 28
  Rec $ App
    (Rec $
29
      (* try increment *)
30
      If (CAS x.[ren (+4)] (Var 1) (BinOp Add (#n 1) (Var 1)))
31 32 33 34 35 36
          Unit (* increment succeeds we return unit *)
          (App (Var 2) (Var 3)) (* increment fails, we try again *))
    (Load x.[ren (+2)]) (* read the counter *).
Definition FG_counter_body (x : expr) : expr :=
  Pair (FG_increment x) (counter_read x).
Definition FG_counter : expr :=
37
  App (Rec (FG_counter_body (Var 1))) (Alloc (#n 0)).
38

39
Section CG_Counter.
40 41
  Context `{heapIG Σ, cfgSG Σ}.

42
  Notation D := (prodC valC valC -n> iProp Σ).
43
  Implicit Types Δ : listC D.
44 45 46 47 48 49 50

  (* Coarse-grained increment *)
  Lemma CG_increment_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (CG_increment x) (TArrow TUnit TUnit).
  Proof.
    intros H1. repeat econstructor.
51 52
    - eapply (context_weakening [_; _]); eauto.
    - eapply (context_weakening [_; _]); eauto.
53 54 55 56
  Qed.

  Lemma CG_increment_closed (x : expr) :
    ( f, x.[f] = x)   f, (CG_increment x).[f] = CG_increment x.
57
  Proof. intros Hx f. unfold CG_increment. asimpl. rewrite ?Hx; trivial. Qed.
58 59

  Lemma CG_increment_subst (x : expr) f :
60
    (CG_increment x).[f] = CG_increment x.[f].
61 62
  Proof. unfold CG_increment; asimpl; trivial. Qed.

63 64
  Lemma steps_CG_increment E ρ j K x n:
    nclose specN  E 
65 66 67
    spec_ctx ρ - x ↦ₛ (#nv n)
    - j  fill K (App (CG_increment (Loc x)) Unit)
    ={E}= j  fill K (Unit)  x ↦ₛ (#nv (S n)).
68
  Proof.
69
    iIntros (HNE) "#Hspec Hx Hj". unfold CG_increment.
70 71 72 73 74
    tp_rec j.
    tp_load j.
    tp_op j. tp_normalise j.
    tp_store j. tp_normalise j.
    by iFrame.
75 76
  Qed.

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
  (* TODO: those should be accompaied by lemmas; preferably so that 
     [change] does not change too much *)
  Tactic Notation "rel_bind_l" open_constr(efoc) :=
    lazymatch goal with
    | [ |- (_  bin_log_related _ _ _ ?e _ _ ) ] =>
      reshape_expr e ltac:(fun K e' =>
       unify e' efoc; change e with (fill K e'))
    end.
  Tactic Notation "rel_bind_r" open_constr(efoc) :=
    lazymatch goal with
    | [ |- (_  bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
      reshape_expr e ltac:(fun K e' =>
       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
    | [ |- (_  bin_log_related _ _ _ _ ?e _ ) ] =>
      reshape_expr e ltac:(fun K e' =>
       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
    end.
 
  Lemma bin_log_related_CG_increment_r Γ K E1 E2 x n t τ :
    nclose specN  E1 
    x ↦ₛ (#nv n) -
    (x ↦ₛ (#nv (S n)) - {E1,E2;Γ}  t log fill K Unit : τ) -
    {E1,E2;Γ}  t log fill K (App (CG_increment (Loc x)) Unit) : τ.
  Proof.
    iIntros (?) "Hx Hlog".
    unfold CG_increment. simpl.
    iApply bin_log_related_rec_r; auto. simpl.
    (* TODO: rel_bind_r (Load (Loc x)) *)
    change ((Store (Loc x) (BinOp Add (#n 1) (Load (Loc x)))))
    with (fill [StoreRCtx (LocV x);BinOpRCtx Add (#nv 1)] (Load (Loc x))).
    rewrite -fill_app.
    iApply (bin_log_related_load_r with "Hx");auto.
    iIntros "Hx". rewrite ?fill_app /=.
    rel_bind_r (BinOp Add _ _).
    iApply (bin_log_related_binop_r); auto.
    rewrite fill_app /=.
    iApply (bin_log_related_store_r with "Hx"); auto.
  Qed.
  
116 117 118 119
  Global Opaque CG_increment.

  Lemma CG_locked_increment_to_val x l :
    to_val (CG_locked_increment x l) = Some (CG_locked_incrementV x l).
Amin Timany's avatar
Amin Timany committed
120
  Proof. by rewrite with_lock_to_val. Qed.
121 122 123

  Lemma CG_locked_increment_of_val x l :
    of_val (CG_locked_incrementV x l) = CG_locked_increment x l.
Amin Timany's avatar
Amin Timany committed
124
  Proof. by rewrite with_lock_of_val. Qed.
125 126 127 128 129 130 131 132 133

  Global Opaque CG_locked_incrementV.

  Lemma CG_locked_increment_type x l Γ :
    typed Γ x (Tref TNat) 
    typed Γ l LockType 
    typed Γ (CG_locked_increment x l) (TArrow TUnit TUnit).
  Proof.
    intros H1 H2. repeat econstructor.
Amin Timany's avatar
Amin Timany committed
134
    eapply with_lock_type; auto using CG_increment_type.
135 136 137 138 139 140
  Qed.

  Lemma CG_locked_increment_closed (x l : expr) :
    ( f, x.[f] = x)  ( f, l.[f] = l) 
     f, (CG_locked_increment x l).[f] = CG_locked_increment x l.
  Proof.
Amin Timany's avatar
Amin Timany committed
141
    intros H1 H2 f. asimpl. unfold CG_locked_increment.
142 143 144 145 146 147 148 149 150 151
    rewrite with_lock_closed; trivial. apply CG_increment_closed; trivial.
  Qed.

  Lemma CG_locked_increment_subst (x l : expr) f :
  (CG_locked_increment x l).[f] = CG_locked_increment x.[f] l.[f].
  Proof.
    unfold CG_locked_increment. simpl.
    rewrite with_lock_subst CG_increment_subst. asimpl; trivial.
  Qed.

152 153
  Lemma steps_CG_locked_increment E ρ j K x n l :
    nclose specN  E 
154 155
    spec_ctx ρ - x ↦ₛ (#nv n) - l ↦ₛ (#v false)
    - j  fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
156
    ={E}= j  fill K Unit  x ↦ₛ (#nv S n)  l ↦ₛ (#v false).
157
  Proof.
158
    iIntros (HNE) "#Hspec Hx Hl Hj".
Dan Frumin's avatar
Dan Frumin committed
159
    tp_apply j (steps_with_lock _ _ _ K _ _ _ _ UnitV UnitV _) with "Hx Hl"; last by iFrame.
160 161 162
    { iIntros (K') "#Hspec Hx Hj /=".
      iApply (steps_CG_increment E with "Hspec Hx"); auto. }
    Unshelve. all: trivial.
163
  Qed.
164 165 166 167 168 169 170 171 172
  
  Lemma bin_log_related_CG_locked_increment Γ K E1 E2 t τ x n l :
    nclose specN  E1 
    (x ↦ₛ (#nv n) - l ↦ₛ (#v false) -
    (x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
      ({E1,E2;Γ}  t log fill K Unit : τ)) -
    {E1,E2;Γ}  t log fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) : τ)%I.
  Proof. 
    iIntros (?) "Hx Hl Hlog".
173 174 175 176
    unfold CG_locked_increment.  
    iApply (bin_log_related_with_lock_r' Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto. 
    - iIntros (K') "Hlog".
      iApply (bin_log_related_CG_increment_r with "Hx"); auto.
177 178
  Qed.
 
179 180
  Global Opaque CG_locked_increment.

181
  Lemma counter_read_to_val x : to_val (counter_read x) = Some (counter_readV x).
182 183
  Proof. trivial. Qed.

184
  Lemma counter_read_of_val x : of_val (counter_readV x) = counter_read x.
185 186 187 188 189
  Proof. trivial. Qed.

  Global Opaque counter_readV.

  Lemma counter_read_type x Γ :
190
    typed Γ x (Tref TNat)  typed Γ (counter_read x) (TArrow TUnit TNat).
191 192 193 194 195 196
  Proof.
    intros H1. repeat econstructor.
    eapply (context_weakening [_; _]); trivial.
  Qed.

  Lemma counter_read_closed (x : expr) :
197
    ( f, x.[f] = x)   f, (counter_read x).[f] = counter_read x.
198 199 200
  Proof. intros H1 f. asimpl. unfold counter_read. by rewrite ?H1. Qed.

  Lemma counter_read_subst (x: expr) f :
201
    (counter_read x).[f] = counter_read x.[f].
202 203
  Proof. unfold counter_read. by asimpl. Qed.

204 205
  Lemma steps_counter_read E ρ j K x n :
    nclose specN  E 
206 207
    spec_ctx ρ - x ↦ₛ (#nv n)
    - j  fill K (App (counter_read (Loc x)) Unit)
208
    ={E}= j  fill K (#n n)  x ↦ₛ (#nv n).
209
  Proof.
210
    intros HNE. iIntros "#Hspec Hx Hj". unfold counter_read.
211 212 213
    tp_rec j.
    tp_load j. tp_normalise j.
    by iFrame.
214 215 216 217 218 219 220 221
  Qed.

  Opaque counter_read.

  Lemma CG_counter_body_type x l Γ :
    typed Γ x (Tref TNat) 
    typed Γ l LockType 
    typed Γ (CG_counter_body x l)
222
            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
223 224 225 226 227 228
  Proof.
    intros H1 H2; repeat econstructor;
      eauto using CG_locked_increment_type, counter_read_type.
  Qed.

  Lemma CG_counter_body_closed (x l : expr) :
229
    ( f, x.[f] = x)  ( f, l.[f] = l) 
230 231 232 233 234 235 236 237 238 239 240 241 242 243
     f, (CG_counter_body x l).[f] = CG_counter_body x l.
  Proof.
    intros H1 H2 f. asimpl.
    rewrite CG_locked_increment_closed; trivial. by rewrite counter_read_closed.
  Qed.

  Lemma CG_counter_type Γ :
    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
    econstructor; eauto using newlock_type.
    do 2 econstructor; [|do 2 constructor].
    constructor. apply CG_counter_body_type; by constructor.
  Qed.

244
  Lemma CG_counter_closed f : CG_counter.[f] = CG_counter.
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
  Proof.
    asimpl; rewrite CG_locked_increment_subst counter_read_subst; by asimpl.
  Qed.

  (* Fine-grained increment *)
  Lemma FG_increment_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (FG_increment x) (TArrow TUnit TUnit).
  Proof.
    intros H1. do 3 econstructor.
    do 2 econstructor; eauto using EqTNat.
    - eapply (context_weakening [_; _; _; _]); eauto.
    - by constructor.
    - repeat constructor.
    - by constructor.
    - by constructor.
    - eapply (context_weakening [_; _]); eauto.
  Qed.

  Lemma FG_increment_closed (x : expr) :
    ( f, x.[f] = x)   f, (FG_increment x).[f] = FG_increment x.
266
  Proof. intros Hx f. asimpl. unfold FG_increment. rewrite ?Hx; trivial. Qed.
267 268 269 270

  Lemma FG_counter_body_type x Γ :
    typed Γ x (Tref TNat) 
    typed Γ (FG_counter_body x)
271
            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
  Proof.
    intros H1; econstructor.
    - apply FG_increment_type; trivial.
    - apply counter_read_type; trivial.
  Qed.

  Lemma FG_counter_body_closed (x : expr) :
    ( f, x.[f] = x) 
     f, (FG_counter_body x).[f] = FG_counter_body x.
  Proof.
    intros H1 f. asimpl. unfold FG_counter_body, FG_increment.
    rewrite ?H1. by rewrite counter_read_closed.
  Qed.

  Lemma FG_counter_type Γ :
    typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
    econstructor; eauto using newlock_type, typed.
    constructor. apply FG_counter_body_type; by constructor.
  Qed.

293
  Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
294 295
  Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.

296 297
  Definition counterN : namespace := nroot .@ "counter".

298 299 300 301 302 303 304 305 306 307
  Lemma bin_log_related_arrow Γ (e e' : expr) τ τ'
   (Hclosed :  f, e.[upn 2 f] = e)
   (Hclosed' :  f, e'.[upn 2 f] = e') :
    ( Δ vv,  τ  Δ vv -
      []  App (Rec e) (of_val (vv.1)) log App (Rec e') (of_val (vv.2)) : τ') -
    Γ  (Rec e) log (Rec e') : TArrow τ τ'.
  Proof.
    iIntros "#H".
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iModIntro. iApply wp_value; auto.
308
    iExists (RecV e'). 
309 310 311 312 313 314 315 316 317
    rewrite Hclosed Hclosed'. simpl.
    iFrame "Hj". iAlways. iIntros (vv) "Hvv".
    iSpecialize ("H" $! Δ vv with "Hvv").
    iSpecialize ("H" $! Δ with "* Hs []").
    { iAlways. iApply interp_env_nil. }
    rewrite ?fmap_nil. rewrite ?empty_env_subst.
    done.
  Qed.

318 319
  Lemma FG_CG_counter_refinement :
    []  FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
320
  Proof.
321 322 323 324 325 326 327 328
    unfold FG_counter, CG_counter.
    iApply (bin_log_related_alloc_l [] _ _ [AppRCtx (RecV (FG_counter_body (Var 1)))]); auto; simpl. iModIntro.
    iIntros (cnt) "Hcnt".    
    rel_bind_r newlock.
    iApply (bin_log_related_newlock_r); auto; simpl.
    iIntros (l) "Hl".
    iApply (bin_log_related_rec_r [] []); auto. asimpl.
    rewrite CG_locked_increment_subst /=.
329
    rewrite counter_read_subst /=.
330 331 332
    rel_bind_r (Alloc (#n 0)).
    iApply (bin_log_related_alloc_r); auto.
    iIntros (cnt') "Hcnt' /=".
333
    (* establishing the invariant *)
334
    iAssert (( n, l ↦ₛ (#v false)  cnt ↦ᵢ (#nv n)  cnt' ↦ₛ (#nv n) )%I)
335
      with "[Hl Hcnt Hcnt']" as "Hinv".
336
    { iExists _. by iFrame. }
337
    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
338
    { iNext; iExact "Hinv". }
339 340
    iApply (bin_log_related_rec_l [] []); auto.
    iNext. asimpl.
341
    rewrite counter_read_subst /=.
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
    
    iApply (bin_log_related_rec_r [] []); auto. simpl.
    rewrite CG_locked_increment_subst /=.
    rewrite counter_read_subst /=.
    
    iApply (bin_log_related_pair [] with "[]"); last first.
    - Transparent counter_read.
      unfold counter_read.
      iApply (bin_log_related_rec); auto. iAlways. asimpl.
      rel_bind_l (Load (Loc cnt)).
      iApply (bin_log_related_load_l).
        iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
        iModIntro. 
        iExists (#nv n). iFrame "Hcnt". iSplit; eauto.
        iIntros "Hcnt". simpl.
      iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
        { solve_ndisj. } { by compute. }
      iIntros "Hcnt'".
360
      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
361
      { iNext. iExists _. by iFrame. }
362
      simpl. 
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413
      iPoseProof (bin_log_related_nat [TArrow TUnit TNat; TUnit]  n) as "H". iFrame "H". (* TODO: iApply does not work in this case *)
   - Transparent CG_locked_increment.
     unfold CG_locked_increment.
     Transparent with_lock.
     unfold with_lock.
     iApply (bin_log_related_arrow); auto.
     iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
     (* fold this stuff back *)
     change (Rec
             (App
                (Rec
                   (App (Rec (App (Rec (Var 3)) (App release (Loc l))))
                      (App (CG_increment (Loc cnt')).[ren (+4)] (Var 3))))
                (App acquire (Loc l))))
     with (CG_locked_increment (Loc cnt') (Loc l)).
     iLöb as "Hlat".
     iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl.
     rel_bind_l (Load (Loc cnt)).
     iApply (bin_log_related_load_l).
     iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro.
     iExists (#nv n). iSplit; eauto. iFrame "Hcnt".
     iIntros "Hcnt". simpl.
     iMod ("Hclose" with "[Hl Hcnt Hcnt']").
     { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
     iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl.
     rel_bind_l (BinOp Add (#n 1) (#n n)).
     iApply (bin_log_related_binop_l). iNext. simpl.
     rel_bind_l (CAS (Loc cnt) (#n n) (#n (S n))).
     iApply (bin_log_related_cas_l); auto. 
     iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
     iModIntro. 
     iExists (#nv m). iFrame "Hcnt".
     destruct (decide (n = m)).
     + (* CAS succeeds *) subst. iSplitR; eauto.
       { iDestruct 1 as %Hfoo. by exfalso. }
       iIntros "_ Hcnt". simpl.
       iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl");
         auto. solve_ndisj.
       iIntros "Hcnt' Hl". 
       iMod ("Hclose" with "[Hl Hcnt Hcnt']").
       { iNext. iExists (S m). iFrame. }
       iApply (bin_log_related_if_true_l _ []); auto.
       iNext. simpl. iPoseProof (bin_log_related_unit [] ) as "H".
       iExact "H". (* TODO iApply does not work *)
     + (* CAS fails *)
       iSplitL; eauto; last first.
       { iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. }
       iIntros "_ Hcnt". simpl.
       iMod ("Hclose" with "[Hl Hcnt Hcnt']").
       { iNext. iExists m. iFrame. }
       iApply (bin_log_related_if_false_l [] []); auto.
414
  Qed.
415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508

    (* iIntros (Δ [|??] ρ) "#Hspec #HΓ"; iIntros (j K) "Hj"; last first. *)
    (* { iDestruct (interp_env_length with "HΓ") as %[=]. } *)
    (* iClear "HΓ". cbn -[FG_counter CG_counter]. *)
    (* rewrite ?empty_env_subst /CG_counter /FG_counter. *)
    (* iApply fupd_wp. *)
    (* tp_bind j newlock. *)
    (* tp_apply j steps_newlock. *)
    (* iDestruct "Hj" as (l) "[Hj Hl]". *)
    (* tp_rec j. *)
    (* asimpl. rewrite CG_locked_increment_subst /=. *)
    (* rewrite counter_read_subst /=. *)
    (* tp_alloc j as cnt' "Hcnt'". tp_normalise j. *)
    (* tp_rec j. tp_normalise j. *)
    (* asimpl. rewrite CG_locked_increment_subst /=. *)
    (* rewrite counter_read_subst /=. *)
    (* iModIntro. wp_bind (Alloc _). *)
    (* iApply wp_alloc; eauto. iNext. *)
    (* iIntros (cnt) "Hcnt /=". *)
    (* (* establishing the invariant *) *)
    (* iAssert (( n, l ↦ₛ (#v false)  cnt ↦ᵢ (#nv n)  cnt' ↦ₛ (#nv n) )%I) *)
    (*   with "[Hl Hcnt Hcnt']" as "Hinv". *)
    (* { iExists _. by iFrame. } *)
    (* iApply fupd_wp. *)
    (* iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial. *)
    (* { iNext; iExact "Hinv". } *)
    (* (* splitting increment and read *) *)
    (* iApply wp_rec; trivial. iNext. asimpl. *)
    (* rewrite counter_read_subst /=. *)
    (* iApply wp_value; simpl. *)
    (* { by rewrite counter_read_to_val. } *)
    (* iExists (PairV (CG_locked_incrementV _ _) (counter_readV _)); simpl. *)
    (* rewrite CG_locked_increment_of_val counter_read_of_val. *)
    (* iFrame "Hj". *)
    (* iExists (_, _), (_, _); simpl; repeat iSplit; trivial. *)
    (* - (* refinement of increment *) *)
    (*   iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj". *)
    (*   rewrite CG_locked_increment_of_val /=. *)
    (*   destruct v; iDestruct "Heq" as "[% %]"; simplify_eq/=. *)
    (*   iLöb as "Hlat". *)
    (*   iApply wp_rec; trivial. asimpl. iNext. *)
    (*   (* fine-grained reads the counter *) *)
    (*   wp_bind (Load _). *)
    (*   iApply wp_atomic; eauto. *)
    (*   iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose". *)
    (*   iApply (wp_load with "[Hcnt]"); [iNext; by iFrame|].  *)
    (*   iNext. iIntros "Hcnt". *)
    (*   iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
    (*   { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } *)
    (*   iApply wp_rec; trivial. asimpl. iNext. *)
    (*   (* fine-grained performs increment *) *)
    (*   wp_bind (BinOp Add _ _). *)
    (*   iApply wp_nat_binop; simpl. *)
    (*   iNext. iModIntro. *)
    (*   wp_bind (CAS _ _ _). *)
    (*   iApply wp_atomic; eauto. *)
    (*   iInv counterN as (n') ">[Hl [Hcnt Hcnt']]" "Hclose". *)
    (*   (* performing CAS *) *)
    (*   destruct (decide (n = n')) as [|Hneq]; subst. *)
    (*   + (* CAS succeeds *) *)
    (*     (* In this case, we perform increment in the coarse-grained one *) *)
    (*     tp_apply j steps_CG_locked_increment with "Hcnt' Hl" *)
    (*         as "[Hcnt' Hl]".              *)
    (*     iApply (wp_cas_suc with "[Hcnt]"); auto. *)
    (*     iNext. iIntros "Hcnt". *)
    (*     iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
    (*     { iNext. iExists _. iFrame "Hl Hcnt Hcnt'"; trivial. } *)
    (*     simpl.  *)
    (*     iApply wp_if_true. iNext. iApply wp_value; trivial. *)
    (*     iExists UnitV; iFrame; auto. *)
    (*   + (* CAS fails *) *)
    (*     (* In this case, we perform a recursive call *) *)
    (*     iApply (wp_cas_fail _ _ _ (#nv n') with "[Hcnt]"); auto; *)
    (*     [inversion 1; subst; auto | ].  *)
    (*     iNext. iIntros "Hcnt". *)
    (*     iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
    (*     { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". } *)
    (*     iApply wp_if_false. iNext. by iApply "Hlat". *)
    (* - (* refinement of read *) *)
    (*   iAlways. clear j K. iIntros (v) "#Heq". iIntros (j K) "Hj". *)
    (*   rewrite ?counter_read_of_val. *)
    (*   iDestruct "Heq" as "[% %]"; destruct v; simplify_eq/=. *)
    (*   Transparent counter_read. *)
    (*   unfold counter_read at 2. *)
    (*   iApply wp_rec; trivial. simpl. *)
    (*   iNext.  *)
    (*   iApply wp_atomic; eauto. *)
    (*   iInv counterN as (n) ">[Hl [Hcnt Hcnt']]" "Hclose". *)
    (*   tp_apply j steps_counter_read with "Hcnt'" as "Hcnt'". *)
    (*   iApply (wp_load with "[Hcnt]"); eauto.  *)
    (*   iNext. iIntros "Hcnt". *)
    (*   iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
    (*   { iNext. iExists _; iFrame "Hl Hcnt Hcnt'". } *)
    (*   iExists (#nv _); eauto. *)
509 510
End CG_Counter.

511
Theorem counter_ctx_refinement :
512 513
  []  FG_counter ctx CG_counter :
         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
514
Proof.
515
  set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (authR cfgUR) ]).
Dan Frumin's avatar
Dan Frumin committed
516 517 518
  set (HG := soundness_unary.HeapPreIG Σ _ _).
  eapply (binary_soundness Σ _); auto.
  intros. apply FG_CG_counter_refinement.
519
Qed.