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

8 9 10 11 12 13 14 15 16 17 18 19 20
Definition CG_increment : val := λ: "x" <>,
  "x" <- BinOp Add (#n 1) (! "x").

Definition CG_locked_increment : val := λ: "x" "l",
  with_lock (λ: "l", CG_increment "x" "l") "l".

Definition counter_read : val := λ: "x" "y", !"x".

Definition CG_counter_body : val := λ: "x" "l",
  (CG_locked_increment "x" "l", counter_read "x").
Definition CG_counter : expr := Let "l" newlock
  ((λ: "x", CG_counter_body "x" "l") (Alloc (#n 0))).

21
Definition FG_increment : val := λ: "v", rec: "inc" <> :=
22 23
  Let "c" (!"v") (If (CAS "v" "c" (BinOp Add (#n 1) "c"))
                     (Unit)
24
                     ("inc" #())).
25 26 27 28 29

Definition FG_counter_body : val := λ: "x",
  (FG_increment "x", counter_read "x").
Definition FG_counter : expr := 
  FG_counter_body (Alloc (#n 0)).
Robbert Krebbers's avatar
Robbert Krebbers committed
30

31
Section CG_Counter.
32 33
  Context `{heapIG Σ, cfgSG Σ}.

Robbert Krebbers's avatar
Robbert Krebbers committed
34
  Notation D := (prodC valC valC -n> iProp Σ).
35
  Implicit Types Δ : listC D.
Dan Frumin's avatar
Dan Frumin committed
36
  
37
  (* Coarse-grained increment *)
38 39 40 41
  Lemma CG_increment_type Γ :
    typed Γ CG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
  Proof.    
    unfold CG_increment. unlock.
Dan Frumin's avatar
Dan Frumin committed
42
    eauto 10 with typeable.    
43 44
  Qed.

Dan Frumin's avatar
Dan Frumin committed
45 46
  Hint Resolve CG_increment_type : typeable.
  
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  Lemma steps_CG_increment E ρ j K x n:
    nclose specN  E 
    spec_ctx ρ - x ↦ₛ (#nv n)
    - j  fill K (CG_increment (Loc x) Unit)
    ={E}= j  fill K (Lit Unit)  x ↦ₛ (#nv (S n)).
  Proof.
    iIntros (HNE) "#Hspec Hx Hj".
    unfold CG_increment. unlock. (*TODO: need an unlock :( *)
    tp_rec j; simpl.
    tp_rec j; simpl.
    tp_load j.
    tp_op j. tp_normalise j.
    tp_store j.
    by iFrame.
  Qed.
62 63 64 65
 
  Lemma bin_log_related_CG_increment_r Γ K E1 E2 x n t τ :
    nclose specN  E1 
    x ↦ₛ (#nv n) -
66
    (x ↦ₛ (#nv (S n)) - {E1,E2;Γ}  t log fill K (Lit Unit) : τ) -
67 68 69
    {E1,E2;Γ}  t log fill K (App (CG_increment (Loc x)) Unit) : τ.
  Proof.
    iIntros (?) "Hx Hlog".
70 71 72
    rel_bind_r (CG_increment (#x))%E.
    unfold CG_increment. unlock. 
    iApply bin_log_related_rec_r; auto. simpl.
73
    iApply bin_log_related_rec_r; auto. simpl.
74
    rel_bind_r (Load (Loc x)).
75
    iApply (bin_log_related_load_r with "Hx");auto.
76
    iIntros "Hx". simpl.
77
    rel_bind_r (BinOp Add _ _).
78
    iApply (bin_log_related_binop_r); auto. simpl.
79 80 81
    iApply (bin_log_related_store_r with "Hx"); auto.
  Qed.
  
82 83
  Global Opaque CG_increment.

84 85
  Lemma CG_locked_increment_type Γ :
    typed Γ CG_locked_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
86
  Proof.
87
    unfold CG_locked_increment. unlock.
Dan Frumin's avatar
Dan Frumin committed
88
    eauto 25 with typeable.
89 90
  Qed.

Dan Frumin's avatar
Dan Frumin committed
91 92
  Hint Resolve CG_locked_increment_type : typeable.

93 94
  Lemma steps_CG_locked_increment E ρ j K x n l :
    nclose specN  E 
95 96
    spec_ctx ρ - x ↦ₛ (#nv n) - l ↦ₛ (#v false)
    - j  fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
97 98
    ={E}= j  fill K (Lit Unit)  x ↦ₛ (#nv S n)  l ↦ₛ (#v false).
  Proof.    
99
    iIntros (HNE) "#Hspec Hx Hl Hj".
100 101 102 103 104 105
    unfold CG_locked_increment. unlock. (* TODO: unlock needed :( *)
    tp_rec j; simpl. rewrite !Closed_subst_id.
    tp_rec j; simpl. rewrite !Closed_subst_id.
    tp_apply j (steps_with_lock _ _ _ K _ _ l _ _ UnitV UnitV) with "Hx Hl";
      last by iFrame.
    { simpl. by rewrite decide_left. }
106
    { iIntros (K') "#Hspec Hx Hj /=".
107 108 109 110
      iApply fupd_trans.
      iApply (steps_CG_increment E with "Hspec Hx"); auto.
      tp_rec j; simpl. by rewrite !Closed_subst_id.
    }
111
  Qed.
112
  
113
  Lemma bin_log_related_CG_locked_increment_r Γ K E1 E2 t τ x n l :
114 115 116
    nclose specN  E1 
    (x ↦ₛ (#nv n) - l ↦ₛ (#v false) -
    (x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
117
      ({E1,E2;Γ}  t log fill K (Lit Unit) : τ)) -
118 119 120
    {E1,E2;Γ}  t log fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) : τ)%I.
  Proof. 
    iIntros (?) "Hx Hl Hlog".
121 122 123 124 125 126 127
    unfold CG_locked_increment. unlock.
    rel_bind_r (App _ (#x))%E.
    iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.
    rel_bind_r (App _ (#l))%E.
    iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.    
    iApply (bin_log_related_with_lock_r Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto. 
    - simpl. by rewrite decide_left.
128
    - iIntros (K') "Hlog".
129
      iApply bin_log_related_rec_r; eauto. simpl. rewrite !Closed_subst_id.
130
      iApply (bin_log_related_CG_increment_r with "Hx"); auto.
131 132
  Qed.
 
133 134
  Global Opaque CG_locked_increment.

135 136
  Lemma counter_read_type Γ :
    typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
137
  Proof.
138
    unfold counter_read. unlock.
Dan Frumin's avatar
Dan Frumin committed
139
    eauto 10 with typeable.
140 141
  Qed.

Dan Frumin's avatar
Dan Frumin committed
142 143
  Hint Resolve counter_read_type : typeable.

144 145
  Lemma steps_counter_read E ρ j K x n :
    nclose specN  E 
146 147
    spec_ctx ρ - x ↦ₛ (#nv n)
    - j  fill K (App (counter_read (Loc x)) Unit)
148
    ={E}= j  fill K (#n n)  x ↦ₛ (#nv n).
149
  Proof.
150 151 152 153
    intros HNE. iIntros "#Hspec Hx Hj". unfold counter_read. unlock.
    tp_rec j. tp_normalise j.
    tp_rec j. tp_normalise j.
    tp_load j.
154
    by iFrame.
155 156 157 158
  Qed.

  Opaque counter_read.

159 160 161 162 163
  Lemma CG_counter_body_type Γ :
    typed Γ CG_counter_body
          (TArrow (Tref TNat)
            (TArrow LockType
              (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)))).
164
  Proof.
165
    unfold CG_counter_body. unlock.
Dan Frumin's avatar
Dan Frumin committed
166
    eauto 15 with typeable.
167 168
  Qed.

Dan Frumin's avatar
Dan Frumin committed
169 170
  Hint Resolve CG_counter_body_type : typeable.

171 172 173
  Lemma CG_counter_type Γ :
    typed Γ CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
174 175
    unfold CG_counter.
    eauto 15 with typeable.
176 177
  Qed.

Dan Frumin's avatar
Dan Frumin committed
178 179
  Hint Resolve CG_counter_type : typeable.

180
  (* Fine-grained increment *)
181 182
  Lemma FG_increment_type Γ :
    typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TUnit)).
183
  Proof.
184
    unfold FG_increment. unlock.
Dan Frumin's avatar
Dan Frumin committed
185
    eauto 20 with typeable.
186 187
  Qed.

Dan Frumin's avatar
Dan Frumin committed
188 189
  Hint Resolve FG_increment_type : typeable.

190 191
  Lemma bin_log_FG_increment_l Γ K E x n t τ :
    x ↦ᵢ (#nv n) -
192 193
    (x ↦ᵢ (#nv (S n)) - {E,E;Γ}  fill K (Lit Unit) log t : τ) -
    {E,E;Γ}  fill K (FG_increment (Loc x) Unit) log t : τ.
194 195 196
  Proof.
    iIntros "Hx Hlog".
    iApply bin_log_related_bind_l.
197 198 199 200 201 202 203 204
    wp_bind (FG_increment #x).
    unfold FG_increment. unlock.
    iApply wp_rec; eauto. 
    solve_closed. (* TODO: why is it not being solved automatically? *)
    iNext. simpl.
    iApply wp_value; eauto. simpl. by rewrite decide_left.
    iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
    iNext. simpl.
205 206
    wp_bind (Load (Loc x)).
    iApply (wp_load with "[Hx]"); auto. iNext.
207 208 209
    iIntros "Hx".
    iApply wp_rec; eauto. solve_closed. (* TODO: same comment here *)
    iNext. simpl.
210 211 212 213 214 215 216
    wp_bind (BinOp _ _ _).
    iApply (wp_nat_binop). iNext. iModIntro. simpl.    
    wp_bind (CAS _ _ _).    
    iApply (wp_cas_suc with "[Hx]"); auto.
    iNext. iIntros "Hx".
    iApply wp_if_true. iNext.
    iApply wp_value; auto.
217
    by iApply "Hlog".
218 219 220 221 222
    (* TODO !!!! 
       Is this actually better than using bin_log_related lemmas?
     *)
  Qed.

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
  (* TODO: this is not really needed.
     This is just an experiment to seeif it is easier to use bin_log_related lemmas *)
  (* Lemma bin_log_FG_increment_l' Γ K E x n t τ : *)
  (*   x ↦ᵢ (#nv n) - *)
  (*   (x ↦ᵢ (#nv (S n)) - {E,E;Γ}  fill K Unit log t : τ) - *)
  (*   {E,E;Γ}  fill K (App (FG_increment (Loc x)) Unit) log t : τ. *)
  (* Proof. *)
  (*   iIntros "Hx Hlog". *)
  (*   iApply (bin_log_related_rec_l Γ E with "[-]"); auto. *)
  (*   iNext. *)
  (*   change (Rec *)
  (*         (App *)
  (*            (Rec *)
  (*               (If *)
  (*                  (CAS (Loc x).[ren (+4)]  *)
  (*                     (Var 1) (BinOp Add (#n 1) (Var 1))) Unit *)
  (*                  (App (Var 2) (Var 3)))) *)
  (*            (Load (Loc x).[ren (+2)]))) with (FG_increment (Loc x)). simpl. *)
  (*   rel_bind_l (Load (Loc x)).  rewrite -fill_app. *)
  (*   iApply (bin_log_related_load_l E E Γ with "[-]"); auto. *)
  (*   iModIntro. iExists (#nv n). iSplit; eauto. iFrame "Hx". *)
  (*   iIntros "Hx". rewrite fill_app /=. *)
  (*   iApply (bin_log_related_rec_l); auto. *)
  (*   iNext. simpl. *)
  (*   rel_bind_l (BinOp Add _ _). rewrite -fill_app. *)
  (*   iApply (bin_log_related_binop_l). rewrite fill_app /=. *)
  (*   iNext. rel_bind_l (CAS _ _ _). rewrite -fill_app. *)
  (*   iApply (bin_log_related_cas_l); auto. *)
  (*   iModIntro. iExists (#nv n). iFrame. *)
  (*   iSplitR. *)
  (*   - iDestruct 1 as %Hfoo. by exfalso. *)
  (*   - iIntros "% Hx". rewrite fill_app /=. *)
  (*     iApply bin_log_related_if_true_l; auto. *)
  (*     iNext. by iApply "Hlog". *)
  (* Qed. *)
258

259 260
  Global Opaque FG_increment.
  
261 262 263 264
  Lemma FG_counter_body_type Γ :
    typed Γ FG_counter_body
          (TArrow (Tref TNat)
            (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat))).
265
  Proof.
266
    unfold FG_counter_body. unlock.
Dan Frumin's avatar
Dan Frumin committed
267
    eauto 15 with typeable.
268 269
  Qed.

Dan Frumin's avatar
Dan Frumin committed
270 271
  Hint Resolve FG_counter_body_type : typeable.
  
272 273 274
  Lemma FG_counter_type Γ :
    typed Γ FG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
275 276
    unfold FG_counter.
    eauto 15 with typeable.
277 278
  Qed.

Dan Frumin's avatar
Dan Frumin committed
279
  Hint Resolve FG_counter_type : typeable.
280

281 282
  Definition counterN : namespace := nroot .@ "counter".

283 284 285 286
  Lemma bin_log_related_arrow Γ (f x f' x' : binder) (e e' : expr) (τ τ' : type)
    (Hclosed  : Closed  (rec: f x := e)%E )
    (Hclosed' : Closed  (rec: f' x' := e')%E) :

287
    ( Δ vv,  τ  Δ vv -
288 289
        App (Rec f x e) (of_val (vv.1)) log App (Rec f' x' e') (of_val (vv.2)) : τ') -
    Γ  (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
290 291
  Proof.
    iIntros "#H".
292 293
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
    cbn-[subst_p]. rewrite /env_subst !Closed_subst_p_id.
294
    iModIntro. iApply wp_value; auto.
295 296
    { simpl. erewrite decide_left. done. }
    iExists (RecV f' x' e'). simpl.
297 298
    iFrame "Hj". iAlways. iIntros (vv) "Hvv".
    iSpecialize ("H" $! Δ vv with "Hvv").
299
    iSpecialize ("H" $! Δ with "Hs []").
300
    { iAlways. iApply interp_env_nil. }
301 302
    rewrite !fmap_empty /env_subst !subst_p_empty. done.
    Unshelve. all: rewrite /Closed /= in Hclosed Hclosed'; eauto.
303 304
  Qed.

305 306 307
  Definition counter_inv l cnt cnt' : iProp Σ :=
    ( n, l ↦ₛ (#v false)  cnt ↦ᵢ (#nv n)  cnt' ↦ₛ (#nv n))%I.

308 309 310 311 312 313 314
  (* A logically atomic specification for
     a fine-grained increment with a baked in frame. *)
  (* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
  Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ  :
     (|={E1,E2}=>  n, x ↦ᵢ (#nv n)  R(n) 
       (( n, x ↦ᵢ (#nv n)  R(n)) ={E2,E1}= True) 
        ( m, x ↦ᵢ (#nv (S m))  R(m) - 
315 316
            {E2,E1;Γ}  fill K (Lit Unit) log t : τ))
    - ({E1,E1;Γ}  fill K (FG_increment (Loc x) Unit) log t : τ).
317 318
  Proof.
    iIntros "#H".
319 320 321 322
    rel_bind_l (FG_increment _).
    Transparent FG_increment. unfold FG_increment. unlock.
    iApply (bin_log_related_rec_l _ E1 (_ ++ K)); auto. iNext. simpl.
    Opaque FG_increment.
323
    iLöb as "IH".   
324 325
    iApply (bin_log_related_rec_l _ E1 K); auto. iNext. simpl.
    rel_bind_l (Load (Loc x)). 
326 327 328 329
    iPoseProof "H" as "H2". (* lolwhat *)    
    Opaque bin_log_related.
    iApply (bin_log_related_load_l).
    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
330
    iExists (#nv n). iFrame. iIntros "Hx".
331 332 333
    rewrite ->uPred.and_elim_l.
    iApply fupd_logrel.
    iMod ("Hrev" with "[HR Hx]").
334 335
    { iExists _. iFrame. } iModIntro. simpl.
    iApply (bin_log_related_rec_l); auto. simpl.
336
    iNext.
337 338 339
    rel_bind_l (BinOp _ _ _).
    iApply (bin_log_related_binop_l). iNext. simpl.
    rel_bind_l (CAS _ _ _).
340
    iApply (bin_log_related_cas_l); auto.
341
    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
342
    destruct (decide (n = n')); subst.
343
    - iExists (#nv n'). iFrame.
344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
      iIntros "_ Hx". simpl.
      rewrite ->uPred.and_elim_r.
      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
      iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.   
    - iExists (#nv n'). iFrame. 
      iSplitL; eauto; last first.
      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
      iIntros "_ Hx". simpl.
      iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.   
      rewrite ->uPred.and_elim_l.
      iMod ("HQ" with "[Hx HR]").
      { iExists _; iFrame. }      
      iApply "IH".
  Qed.    

Dan Frumin's avatar
Dan Frumin committed
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
  (* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
  (*   Closed  (Lam x e)  *)
  (*   to_val (lang.subst x (of_val v) e) = Some ev  *)
  (*   Γ  (App (Lam x e) v) log t : τ *)
  (*    Γ  (lang.subst x (of_val v) e) log t : τ. *)
  (* Proof. *)
  (*   iIntros (??) "Hr". *)
  (*   Transparent bin_log_related. *)
  (*   iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
  (*   cbn-[subst_p].  *)
  (*   (* assert (Closed  (lang.subst x v e)). *) *)
  (*   (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
  (*   rewrite /env_subst !Closed_subst_p_id. *)
  (*   iSpecialize ("Hr" with "Hs []"). *)
  (*   { iAlways. by iFrame. } *)
  (*   rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
  (*   { rewrite /Closed. simpl. *)
  (*     rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
  (*   iMod ("Hr" with "Hj") as "Hr". *)
  (*   iModIntro. simpl. *)
  (*   rewrite {1}wp_unfold /wp_pre /=. *)
  (*   iApply wp_value; eauto. *)
  (*   iApply (wp_bind_inv in "Hr". *)
  (*   Opaque bin_log_related. *)


386
  (* TODO: try to use with_lock rules *)
387 388 389 390 391 392
  Lemma FG_CG_increment_refinement l cnt cnt' Γ :
    inv counterN (counter_inv l cnt cnt') -
    Γ  FG_increment (Loc cnt) log CG_locked_increment (Loc cnt') (Loc l) : (TArrow TUnit TUnit).
  Proof.
    iIntros "#Hinv".
    Transparent CG_locked_increment with_lock.
393
    Transparent FG_increment.
394
    unfold CG_locked_increment. unlock.
395
    unfold FG_increment. unlock.
396

397 398 399
    iApply (bin_log_related_rec_l _  []); auto.
    iNext. simpl.
    rel_bind_r (App _ (#cnt')%E).
400 401
    iApply (bin_log_related_rec_r _ _); auto. simpl. rewrite !Closed_subst_id.
    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl. rewrite !Closed_subst_id.
402 403 404 405 406

    unfold with_lock. unlock.
    rel_bind_r (App _ (λ: "l", _))%E.

    iApply (bin_log_related_rec_r Γ); eauto.
407 408
    { simpl. by rewrite decide_left. }
    simpl. rewrite !Closed_subst_id.
409

410
    iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
411 412 413 414

    iApply bin_log_related_arrow. 
    iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
    (* TODO: cannot use FG_increment_logatomic atm *)
415 416 417 418 419
    (* iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#v false))  cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]"). *)
    (* iAlways. *)
    (* iInv counterN as ">Hcnt" "Hcl". iModIntro. *)
    (* iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". *)
    (* iExists n. iFrame. clear n. *)
420
    (* iSplit. *)
421 422 423 424 425 426 427 428 429 430 431 432
    (* - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]". *)
    (*   iMod ("Hcl" with "[-]"). *)
    (*   { iNext. iExists _. iFrame. } *)
    (*   done. *)
    (* - iIntros (m) "[Hcnt [Hl Hcnt']]". *)
    (*   iApply (bin_log_related_CG_locked_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj.  } *)
    (*   iIntros "Hcnt' Hl". *)
    (*   iMod ("Hcl" with "[-]"). *)
    (*   { iNext. iExists _. iFrame. } *)
    (*   simpl. *)
    (*   iApply bin_log_related_unit. *)
    (*   Opaque CG_locked_increment with_lock. *)
433
    iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457
    iLöb as "IH".
    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
    rel_bind_l (! #cnt)%E.
    iApply (bin_log_related_load_l).
      iInv counterN as ">Hcnt" "Hcl". iModIntro.
      iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
      iExists (#nv n). iFrame. iIntros "Hcnt".
      iMod ("Hcl" with "[-]"); simpl.
      { iNext. iExists _. iFrame. }
    iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
    rel_bind_l (BinOp Add _ _).
    iApply bin_log_related_binop_l. iNext. simpl.
    rel_bind_l (CAS _ _ _).
    iApply (bin_log_related_cas_l); eauto.
    iInv counterN as ">Hcnt" "Hcl". iModIntro.
    iDestruct "Hcnt" as (m) "[Hl [Hcnt Hcnt']]".
    iExists _; iFrame.
    destruct (decide (m = n)) as [|Hmn]; subst.
    - (* CASE [m = n], CAS successful *)
      iSplitR. iIntros "%". by exfalso.
      iIntros "% Hcnt".
      rel_bind_r (acquire #l).
      iApply (bin_log_related_acquire_r with "Hl"); simpl; eauto. solve_ndisj. 
      iIntros "Hl".
458
      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj.
459 460 461 462 463
      rel_bind_r (App _ #())%E.
      iApply (bin_log_related_rec_r _ _); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
      rel_bind_r (CG_increment _ _).
      iApply (bin_log_related_CG_increment_r with "Hcnt'"). solve_ndisj. simpl.
      iIntros "Hcnt'".
464
      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id.
465 466 467 468 469 470
      rel_bind_r (release #l)%E.
      iApply (bin_log_related_release_r with "Hl"). solve_ndisj.
      iIntros "Hl". simpl.
      iMod ("Hcl" with "[-]").
      { iNext. iExists _. by iFrame. }
      iApply (bin_log_related_if_true_l _ _ []). iNext. simpl.
471
      iApply (bin_log_related_rec_r _ _ _ []); simpl; eauto.
472 473 474 475 476 477
      iApply bin_log_related_unit.
    - (* CASE [m  n], CAS fails *)
      iSplitL; last first. iIntros "%". exfalso. apply Hmn. by inversion H1.
      iIntros "% Hcnt". simpl.
      iMod ("Hcl" with "[-]").
      { iNext. iExists _. by iFrame. }
478
      iApply (bin_log_related_if_false_l _ _ []). iNext. simpl.
479 480
      iApply "IH".
  Qed.
481

482
  Lemma FG_CG_counter_refinement :
483
      FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
484
  Proof.
485 486 487 488
    unfold FG_counter, CG_counter.
    rel_bind_r newlock.
    iApply (bin_log_related_newlock_r); auto; simpl.
    iIntros (l) "Hl".
489
    iApply (bin_log_related_rec_r _ _ _ []); auto. rewrite /= !Closed_subst_id /=.
490 491 492 493
    rel_bind_l (Alloc _).
    iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
    iIntros (cnt) "Hcnt".        
    rel_bind_r (Alloc _).
494 495
    iApply (bin_log_related_alloc_r); auto.
    iIntros (cnt') "Hcnt' /=".
496

497
    (* establishing the invariant *)
498
    iAssert (counter_inv l cnt cnt')
499
      with "[Hl Hcnt Hcnt']" as "Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
500
    { iExists _. by iFrame. }
501
    iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
502 503 504 505
    unfold FG_counter_body. unlock.
    iApply (bin_log_related_rec_l _ _ []); auto.
    iNext. rewrite /= !Closed_subst_id /=.

506
    iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
507 508 509 510 511
    rewrite /= !Closed_subst_id /=.
    rel_bind_r (CG_counter_body _).    
    unfold CG_counter_body. unlock.
    iApply (bin_log_related_rec_r _ _); auto. 
    rewrite /= !Closed_subst_id /=.
512
    iApply (bin_log_related_rec_r _ _ _ []); auto. 
513
    rewrite /= !Closed_subst_id /=.
514
    
515
    iApply (bin_log_related_pair _ with "[]"); last first.
516
    - Transparent counter_read.
517
      unfold counter_read. unlock.
518
      iApply (bin_log_related_rec_r _ _ _ []); auto. simpl.
519 520
      iApply (bin_log_related_rec_l _ _ []); auto. simpl. iNext.      
      iApply bin_log_related_rec; simpl. iAlways. cbn.
521 522
      iApply (bin_log_related_load_l _ _ _ []).
      iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
523
        iModIntro. 
524
        iExists (#nv n). iFrame "Hcnt".
525 526
        iIntros "Hcnt". simpl.
      iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
527
        { solve_ndisj. }
528
      iIntros "Hcnt'".
529
      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
530
      { iNext. iExists _. by iFrame. }
531 532 533
      simpl.
      iApply (bin_log_related_val); auto.
      intros. simpl. eauto.
534
   - iApply (FG_CG_increment_refinement with "Hinv").
535
  Qed.
536

537 538
End CG_Counter.

539
Theorem counter_ctx_refinement :
540
    FG_counter ctx CG_counter :
Robbert Krebbers's avatar
Robbert Krebbers committed
541
         TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
542
Proof.
543 544 545 546 547 548 549
  set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR ]).
  set (HG := HeapPreIG Σ _ _).
  eapply (binary_soundness Σ _).
  (* TODO: how to get rid of this bullshit with closed conditions? *)
  rewrite /FG_counter /CG_counter; try solve_closed.
  rewrite /FG_counter /CG_counter; try solve_closed.
  Transparent newlock. unfold newlock. solve_closed.
Dan Frumin's avatar
Dan Frumin committed
550
  intros. apply FG_CG_counter_refinement.
551
Qed.