various.v 21.6 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6
(* Some refinement from the paper
   "The effects of higher-order state and control on local relational reasoning"
   D. Dreyer, G. Neis, L. Birkedal
*)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import csum agree excl.
7
From iris_logrel Require Export logrel examples.lock examples.counter examples.bot.
Dan Frumin's avatar
Dan Frumin committed
8 9 10 11 12

Section refinement.
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).

13 14 15 16 17 18 19 20 21 22 23 24 25 26
  Lemma refinement1' Γ :
    Γ 
      let: "x" := ref #1 in
      (λ: "f", "f" #();; !"x")
    log
      (λ: "f", "f" #();; #1)
    : ((Unit  Unit)  TNat)%F.
  Proof.
  iIntros (Δ).
  rel_alloc_l as x "Hx".
  rel_let_l.
  iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
  iApply bin_log_related_rec; auto.
  iAlways. cbn.
Dan Frumin's avatar
Dan Frumin committed
27
  iApply (bin_log_related_seq'); auto.
28 29 30 31 32 33 34 35 36 37 38
  - iApply bin_log_related_app; last by iApply bin_log_related_unit.
    iApply bin_log_related_var.
    apply lookup_insert.
  - rel_load_l_atomic.
    iInv (nroot.@"xinv") as "Hx" "Hcl".
    iModIntro. iExists _; iFrame "Hx"; simpl.
    iNext. iIntros "Hx".
    iMod ("Hcl" with "Hx") as "_".
    iApply bin_log_related_nat.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
39 40 41 42 43 44
  Lemma refinement1 Γ :
    Γ 
      let: "x" := ref #1 in
      (λ: "f", "f" #();; !"x")
    log
      (λ: "f", "f" #();; #1)
45
    : ((Unit  Unit)  TNat).
Dan Frumin's avatar
Dan Frumin committed
46 47 48 49 50 51 52 53
  Proof.
  iIntros (Δ).
  rel_alloc_l as x "Hx".
  iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
  rel_let_l.
  iApply bin_log_related_arrow; auto.
  iIntros "!#" (f1 f2) "Hf".
  rel_let_l. rel_let_r.
Dan Frumin's avatar
Dan Frumin committed
54
  iApply (bin_log_related_seq' with "[Hf]"); auto.
Dan Frumin's avatar
Dan Frumin committed
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
  - iApply (bin_log_related_app with "Hf").
    by rel_vals.
  - rel_load_l_atomic.
    iInv (nroot.@"xinv") as "Hx" "Hcl".
    iModIntro. iExists _; iFrame "Hx".
    iNext. iIntros "Hx".
    iMod ("Hcl" with "Hx").
    rel_vals; eauto.
  Qed.

  Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ  oneshotG Σ.
  Proof. solve_inG. Qed.

  Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
  Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
  Lemma new_pending `{oneshotG Σ} : (|==>  γ, pending γ)%I.
  Proof. by apply own_alloc. Qed.
  Lemma shoot γ `{oneshotG Σ} : pending γ == shot γ.
  Proof.
    apply own_update.
    intros n [f |]; simpl; eauto.
    destruct f; simpl; try by inversion 1.
  Qed.
  Definition shootN := nroot .@ "shootN".
  Lemma shot_not_pending γ `{oneshotG Σ} :
    shot γ - pending γ - False.
  Proof.
    iIntros "Hs Hp".
    iPoseProof (own_valid_2 with "Hs Hp") as "H".
    iDestruct "H" as %[].
  Qed.

  Lemma refinement2 `{oneshotG Σ} Γ :
    Γ 
      let: "x" := ref #0 in
      (λ: "f", "x" <- #1;; "f" #();; !"x")
    log
      (let: "x" := ref #1 in
       λ: "f", "f" #();; !"x")
97
    : ((Unit  Unit)  TNat).
Dan Frumin's avatar
Dan Frumin committed
98 99 100 101 102
  Proof.
    iIntros (Δ).
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    rel_let_l; rel_let_r.
103
    iMod new_pending as (γ) "Ht".
Dan Frumin's avatar
Dan Frumin committed
104 105 106
    iMod (inv_alloc shootN _ ((x ↦ᵢ #0  pending γ  x ↦ᵢ #1  shot γ)  y ↦ₛ #1)%I with "[Hx Ht $Hy]") as "#Hinv".
    { iNext. iLeft. iFrame. }
    iApply bin_log_related_arrow; auto.
107
    iIntros "!#" (f1 f2) "#Hf".
Dan Frumin's avatar
Dan Frumin committed
108 109 110 111
    rel_let_l. rel_let_r.
    rel_store_l_atomic.
    iInv shootN as "[[[Hx Hp] | [Hx #Hs]] Hy]" "Hcl";
      iModIntro; iExists _; iFrame "Hx"; iNext; iIntros "Hx"; rel_rec_l.
112
    - iMod (shoot γ with "Hp") as "#Hs".
Dan Frumin's avatar
Dan Frumin committed
113 114
      iMod ("Hcl" with "[$Hy Hx]") as "_".
      { iNext. iRight. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
115
      iApply (bin_log_related_seq' with "[Hf]"); auto.
Dan Frumin's avatar
Dan Frumin committed
116 117 118 119 120
      + iApply (bin_log_related_app with "Hf").
        by rel_vals.
      + rel_load_l_atomic.
        iInv shootN as "[[[Hx >Hp] | [Hx Hs']] Hy]" "Hcl".
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
121
        iModIntro. iExists _; iFrame. iNext. simpl.
Dan Frumin's avatar
Dan Frumin committed
122 123
        iIntros "Hx".
        rel_load_r.
124
        iMod ("Hcl" with "[-]") as "_".
Dan Frumin's avatar
Dan Frumin committed
125
        { iNext. iFrame. iRight; by iFrame. }
126
        iApply bin_log_related_nat.
Dan Frumin's avatar
Dan Frumin committed
127 128
    - iMod ("Hcl" with "[$Hy Hx]") as "_".
      { iNext. iRight. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
129
      iApply (bin_log_related_seq' with "[Hf]"); auto.
Dan Frumin's avatar
Dan Frumin committed
130 131 132 133 134 135 136 137 138 139 140 141 142
      + iApply (bin_log_related_app with "Hf").
        by rel_vals.
      + rel_load_l_atomic.
        iInv shootN as "[[[Hx >Hp] | [Hx Hs']] Hy]" "Hcl".
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
        iModIntro. iExists _; iFrame. iNext.
        iIntros "Hx".
        rel_load_r.
        iMod ("Hcl" with "[-]").
        { iNext. iFrame. iRight; by iFrame. }
        rel_vals; eauto.
  Qed.

143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165

  Lemma refinement25 `{oneshotG Σ} Γ :
    Γ 
      (λ: "f", "f" #();; #1)
    log
      (let: "x" := ref #0 in
       (λ: "f", "x" <- #1;; "f" #();; !"x"))
    : ((Unit  Unit)  TNat).
  Proof.
    iIntros (Δ).
    rel_alloc_r as x "Hx".
    rel_let_r.
    iMod new_pending as (γ) "Ht".
    iMod (inv_alloc shootN _ ((x ↦ₛ #0  pending γ  x ↦ₛ #1  shot γ))%I with "[Hx Ht]") as "#Hinv".
    { iNext. iLeft. iFrame. }
    iApply bin_log_related_arrow; auto.
    iIntros "!#" (f1 f2) "#Hf".
    rel_let_l. rel_let_r.
    iInv shootN as ">[[Hx Hp] | [Hx #Hs]]" "Hcl";
      rel_store_r; rel_seq_r.
    - iMod (shoot γ with "Hp") as "#Hs".
      iMod ("Hcl" with "[Hx]") as "_".
      { iNext. iRight. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
166
      iApply (bin_log_related_seq' with "[Hf]"); auto.
167 168 169 170 171 172 173 174 175 176
      + iApply (bin_log_related_app with "Hf").
        rel_finish.
      + iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
          rel_load_r.
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
        iMod ("Hcl" with "[Hx]") as "_".
        { iNext. iRight. by iFrame. }
        rel_finish.
    - iMod ("Hcl" with "[Hx]") as "_".
      { iNext. iRight. by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
177
      iApply (bin_log_related_seq' with "[Hf]"); auto.
178 179 180 181 182 183 184 185 186 187
      + iApply (bin_log_related_app with "Hf").
        rel_finish.
      + iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
          rel_load_r.
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
        iMod ("Hcl" with "[Hx]") as "_".
        { iNext. iRight. by iFrame. }
        rel_finish.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
188
  (* Also known as "callback with lock" *)
189 190 191 192
  Definition i3 (x x' b b' : loc) : iProp Σ :=
    ( (n:nat), x ↦ᵢ{1/2} #n  x' ↦ₛ{1/2} #n 
    ((b ↦ᵢ #true  b' ↦ₛ #true  x ↦ᵢ{1/2} #n  x' ↦ₛ{1/2} #n)
     (b ↦ᵢ #false  b' ↦ₛ #false)))%I.
193
  Definition i3n := nroot .@ "i3".
194
  Lemma refinement3 Γ :
195 196 197 198 199
    Γ 
      let: "b" := ref #true in
      let: "x" := ref #0 in
      (λ: "f", if: CAS "b" #true #false
               then "f" #();; "x" <- !"x" + #1 ;; "b" <- #true
200 201
               else #(),
       λ: <>, !"x")
202 203 204 205 206 207
    log
      (let: "b" := ref #true in
      let: "x" := ref #0 in
      (λ: "f", if: CAS "b" #true #false
               then let: "n" := !"x" in
                    "f" #();; "x" <- "n" + #1 ;; "b" <- #true
208 209 210
               else #(),
       λ: <>, !"x"))
    : ((Unit  Unit)  Unit) × (Unit  TNat).
211 212 213 214 215 216 217 218 219 220 221
  Proof.
    iIntros (Δ).
    rel_alloc_l as b "Hb".
    rel_let_l.
    rel_alloc_l as x "Hx".
    rel_let_l.
    rel_alloc_r as b' "Hb'".
    rel_let_r.
    rel_alloc_r as x' "Hx'".
    rel_let_r.
    iMod (inv_alloc i3n _ (i3 x x' b b') with "[-]") as "#Hinv".
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 278 279 280 281 282 283 284 285 286 287 288 289
    { iNext. unfold i3. iExists 0.
      iDestruct "Hx" as "[$ Hx]".
      iDestruct "Hx'" as "[$ Hx']".
      iLeft. iFrame. }
    iApply bin_log_related_pair.
    - iApply bin_log_related_arrow; eauto.
      iAlways. iIntros (f f') "Hf".
      rel_let_l.
      rel_let_r.
      rel_cas_l_atomic.
      iInv i3n as (n) "(Hx & Hx' & >Hbb)" "Hcl".
      iDestruct "Hbb" as "[(Hb & Hb' & Hx1 & Hx'1) | (Hb & Hb')]"; last first.
      { iModIntro; iExists _; iFrame.
        iSplitL; last by iIntros (?); congruence.
        iIntros (?); iNext; iIntros "Hb".
        rel_cas_fail_r; rel_if_r; rel_if_l.
        iMod ("Hcl" with "[-]").
        { iNext. iExists n. iFrame. iRight. iFrame. }
        rel_vals; eauto.
      }
      { iModIntro. iExists _; iFrame.
        iSplitR; first by iIntros (?); congruence.
        iIntros (?); iNext; iIntros "Hb".
        rel_cas_suc_r; rel_if_r; rel_if_l.
        rel_load_r. rel_let_r.
        iMod ("Hcl" with "[Hb Hb' Hx Hx']") as "_".
        { iNext. iExists _; iFrame. iRight. iFrame. }
        iApply (bin_log_related_seq' with "[Hf]"); auto.
        { iApply (bin_log_related_app with "Hf").
          iApply bin_log_related_unit. }
        rel_load_l.
        rel_op_l. rel_op_r.
        rel_store_l_atomic.
        iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
        iDestruct (mapsto_agree with "Hx Hx1") as %->.
        iCombine "Hx Hx1" as "Hx".
        iModIntro. iExists _; iFrame. iNext.
        iIntros "Hx".
        iCombine "Hx' Hx'1" as "Hx'".
        rel_store_r.
        iDestruct "Hx" as "[Hx Hx1]".
        iDestruct "Hx'" as "[Hx' Hx'1]".
        iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
        { iCombine "Hx Hx1" as "Hx".
          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
          compute in Hfoo. eauto. }
        iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
        { iNext. iExists _. iFrame. }
        rel_seq_l. rel_seq_r.
        rel_store_l_atomic. clear n'.
        iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
        iDestruct (mapsto_agree with "Hx Hx1") as %->.
        iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
        { iCombine "Hx Hx1" as "Hx".
          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
          compute in Hfoo. eauto. }
        iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
        rel_store_r.
        iMod ("Hcl" with "[-]") as "_".
        { iNext. iExists _. iFrame. iLeft. iFrame. }
        rel_vals; eauto. }
    - iApply bin_log_related_arrow; eauto.
      iAlways. iIntros (u u') "_".
      rel_let_l. rel_let_r.
      rel_load_l_atomic.
      iInv i3n as (n) "(>Hx & Hx' & >Hbb)" "Hcl".
      iModIntro. iExists _; iFrame; iNext. iIntros "Hx".
      rel_load_r.
290
      iMod ("Hcl" with "[-]") as "_".
291 292
      { iNext. iExists _. iFrame. }
      iApply bin_log_related_nat.
293 294
  Qed.

295 296 297 298
  (* /Sort of/ a well-bracketedness example.
     Without locking in the first expression, the callback can reenter
     the body in a forked thread to change the value of x
  *)
299
  Lemma refinement4 Γ `{!lockG Σ}:
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
    Γ 
      (let: "x" := ref #1 in
       let: "l" := newlock #() in
       λ: "f", acquire "l";;
               "x" <- #0;; "f" #();;
               "x" <- #1;; "f" #();;
               let: "v" := !"x" in
               release "l";; "v")
    log
      (let: "x" := ref #0 in
       λ: "f", "f" #();; "x" <- #1;; "f" #();; !"x")
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
    iIntros (Δ).
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    rel_let_l; rel_let_r.
    pose (N:=logrelN.@"lock").
    rel_apply_l (bin_log_related_newlock_l N ( (n m : nat), x ↦ᵢ #n  y ↦ₛ #m)%I with "[Hx Hy]").
    { iExists _, _. iFrame. }
    iIntros (l γ) "#Hl".
    rel_let_l.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f1 f2) "#Hf".
    rel_let_l. rel_let_r.
    rel_apply_l (bin_log_related_acquire_l N _ l with "Hl"); auto.
    iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
    rel_seq_l.
    rel_store_l. rel_seq_l.
329 330
    iApply (bin_log_related_seq' _ _ _ _ _ _ TUnit with "[Hf]"); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ TUnit TUnit with "[Hf]").
Dan Frumin's avatar
Dan Frumin committed
331
      iApply bin_log_related_val; eauto using to_of_val.
332 333 334
      iApply bin_log_related_unit. }
    rel_store_l. rel_seq_l.
    rel_store_r. rel_seq_r.
335 336
    iApply (bin_log_related_seq' _ _ _ _ _ _ TUnit with "[Hf]"); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ TUnit TUnit with "[Hf]").
Dan Frumin's avatar
Dan Frumin committed
337
      iApply bin_log_related_val; eauto using to_of_val.
338 339 340 341 342 343 344 345 346 347
      iApply bin_log_related_unit. }
    rel_load_l.
    rel_let_l.
    rel_load_r.
    rel_apply_l (bin_log_related_release_l N _ l γ with "Hl Hlocked [Hx Hy]"); eauto.
    { iExists _,_. iFrame. }
    rel_seq_l.
    rel_vals; eauto.
  Qed.

348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
  (* "Single return" example *)
  Lemma refinement5 Γ :
    Γ 
      (λ: "f", let: "x" := ref #0 in
               let: "y" := ref #0 in
               "f" #();;
               "x" <- !"y";;
               "y" <- #1;;
               !"x")
    log
      (λ: "f", let: "x" := ref #0 in
               let: "y" := ref #0 in
               "f" #();;
               "x" <- !"y";;
               "y" <- #2;;
               !"x")
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
    iIntros (Δ).
    iApply bin_log_related_arrow; eauto.
    iAlways.
    iIntros (f1 f2) "Hf".
    rel_let_l. rel_let_r.
    rel_alloc_l as x "Hx". rel_let_l.
    rel_alloc_l as y "Hy". rel_let_l.
    rel_alloc_r as x' "Hx'". rel_let_r.
    rel_alloc_r as y' "Hy'". rel_let_r.
Dan Frumin's avatar
Dan Frumin committed
375
    iApply (bin_log_related_seq' with "[Hf]"); eauto.
376 377 378 379 380 381 382 383 384 385
    { iApply (bin_log_related_app with "Hf").
      iApply bin_log_related_unit. }
    rel_load_l. rel_load_r.
    rel_store_l. rel_store_r.
    rel_let_l. rel_let_r.
    rel_store_l. rel_store_r.
    rel_let_l. rel_let_r.
    rel_load_l. rel_load_r.
    iApply bin_log_related_nat.
  Qed.
386 387 388 389 390

  (** Higher-order profiling *)
  Definition τg := TArrow TUnit TUnit.
  Definition τf := TArrow τg TUnit.
  Definition p : val := λ: "g", let: "c" := ref #0 in
Dan Frumin's avatar
Dan Frumin committed
391
                                (λ: <>, FG_increment "c";; "g" #(), λ: <>, !"c").
392 393 394 395 396 397 398 399 400 401 402
  (** The idea for the invariant is that we have to states:
       a) c1 = n, c2 = n
       b) c1 = n+1, c2 = n
      We start in state (a) and can only transition to the state (b) by giving away an exclusive token.
      But once we have transitioned to (b), we remain there forever.
      To that extent we use to resources algebras two model two of those conditions, and we tie it all together in the invariant.
  *)
  Definition i6 `{oneshotG Σ} `{inG Σ (exclR unitR)} (c1 c2 : loc) γ γ' :=
    ( (n : nat),
     (c1 ↦ᵢ #n  c2 ↦ₛ #n  pending γ)
    (c1 ↦ᵢ #(S n)  c2 ↦ₛ #n  shot γ  own γ' (Excl ())))%I.
Dan Frumin's avatar
Dan Frumin committed
403 404

  Program Definition TRV : D := λne _, True%I.
405 406 407
  Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
    inv shootN (i6 c1 c2 γ γ') -
     τg  Δ (g1, g2) -
408
    {Δ;Γ} 
Dan Frumin's avatar
Dan Frumin committed
409
      (FG_increment #c1;; g1 #())
410
    log
Dan Frumin's avatar
Dan Frumin committed
411
      (FG_increment #c2;; g2 #()) : TUnit.
412 413
  Proof.
    iIntros "#Hinv #Hg".
414 415
    iApply (bin_log_related_seq TRV _ _ _ _ _ _ (TVar 0)); auto; last first.
    { iApply (bin_log_related_app _ _ _ _ _ _ TUnit).
Dan Frumin's avatar
Dan Frumin committed
416
      iApply bin_log_related_val; eauto using to_of_val.
417 418
      iApply bin_log_related_unit. }
    rel_apply_l (bin_log_FG_increment_logatomic _
419
      (fun (n : nat) => (c2 ↦ₛ #n  pending γ)  (c2 ↦ₛ #(n-1)  shot γ  own γ' (Excl ())  1  n))%I True%I); first done.
420 421 422 423 424 425
    iAlways.
    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl";
      iModIntro; iExists _; iFrame.
    - iSplitL "Hc2 Ht".
      { iLeft. iFrame. }
      iSplit.
426
      { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
427
        iApply ("Hcl" with "[-]"); iNext.
428 429
        + iExists n. iLeft. iFrame.
        + iExists (n-1). iRight.
430 431
          rewrite minus_Sn_m // /= -minus_n_O.
          iFrame. }
432
      { iIntros "[Hc1 Hc] _".
Dan Frumin's avatar
Dan Frumin committed
433 434 435 436
        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
          (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
          iIntros "Hc2".
        - iMod ("Hcl" with "[-]") as "_".
437
          { iNext. iExists (S n). iFrame. iLeft; iFrame. }
Dan Frumin's avatar
Dan Frumin committed
438 439
          rel_finish.
        - iMod ("Hcl" with "[-]") as "_".
440
          { iNext. iExists n.
441 442
            rewrite minus_Sn_m // /= -minus_n_O.
            iFrame. iRight; iFrame. }
Dan Frumin's avatar
Dan Frumin committed
443
          rel_finish. }
444 445 446 447 448
    - iSplitL "Hc2 Ht".
      { rewrite /= -minus_n_O. iRight. iFrame.
        iDestruct "Ht" as "[$ $]".
        iPureIntro. omega. }
      iSplit.
449
      { iIntros "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
450
        iApply ("Hcl" with "[-]"); iNext.
451 452 453 454
        + iExists (S n). iLeft. iFrame.
        + iExists n. iRight. iFrame.
          assert (S n - 1 = n) as -> by omega. done. }
      { iIntros "[Hc1 Hc] _".
Dan Frumin's avatar
Dan Frumin committed
455 456 457 458
        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
          (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
          iIntros "Hc2".
        - iMod ("Hcl" with "[-]") as "_".
459
          { iNext. iExists (S (S n)). iFrame. iLeft; iFrame. }
Dan Frumin's avatar
Dan Frumin committed
460 461
          rel_finish.
        - iMod ("Hcl" with "[-]") as "_".
462 463
          { iNext. iExists (S n). iRight. iFrame.
            by rewrite -minus_n_O. }
Dan Frumin's avatar
Dan Frumin committed
464
          rel_finish. }
465 466 467 468 469
  Qed.

  Lemma profiled_g' `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
    inv shootN (i6 c1 c2 γ γ') -
     τg  Δ (g1, g2) -
470
    {Δ;Γ} 
Dan Frumin's avatar
Dan Frumin committed
471
      (λ: <>, FG_increment #c1;; g1 #())
472
    log
Dan Frumin's avatar
Dan Frumin committed
473
      (λ: <>, FG_increment #c2;; g2 #()) : τg.
474 475 476 477 478 479 480 481
  Proof.
    iIntros "#Hinv #Hg".
    iApply bin_log_related_arrow_val; auto.
    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
    rel_seq_l. rel_seq_r.
    iApply profiled_g; eauto.
  Qed.

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
  Lemma close_i6 c1 c2 γ γ' `{oneshotG Σ} `{inG Σ (exclR unitR)} :
    (( n : nat, c1 ↦ᵢ #n
      (c2 ↦ₛ #n  pending γ
        c2 ↦ₛ #(n - 1)  shot γ  own γ' (Excl ())  1  n))
     - i6 c1 c2 γ γ')%I.
  Proof.
    iDestruct 1 as (m) "[Hc1 Hc2]".
    iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
      [iExists m; iLeft | iExists (m - 1); iRight]; iFrame.
    rewrite minus_Sn_m // /= -minus_n_O; done.
  Qed.

  Lemma refinement6_helper Δ Γ f'1 f'2 g1 g2 c1 c2 γ γ' m `{oneshotG Σ} `{inG Σ (exclR unitR)} :
    inv shootN (i6 c1 c2 γ γ') -
     τg  Δ (g1, g2) -
     τf  Δ (f'1, f'2) -
    ( i6 c1 c2 γ γ' ={  shootN,}= True) -
    c1 ↦ᵢ #(S m) -
    (c2 ↦ₛ #m  pending γ
       c2 ↦ₛ #(m - 1)  shot γ  own γ' (Excl ())  1  m) -
    own γ' (Excl ()) -
503
    {  shootN;Δ;Γ} 
Dan Frumin's avatar
Dan Frumin committed
504
      (g1 #() ;; f'1 (λ: <>, (FG_increment #c1);; g1 #()) ;; #() ;; ! #c1)
505 506
    log
      (g2 #() ;;
Dan Frumin's avatar
Dan Frumin committed
507
       f'2 (λ: <>, (FG_increment #c2);; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
508 509 510 511 512 513 514 515
  Proof.
    iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht".
    iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
    { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo.
      inversion Hfoo. }
    iMod (shoot γ with "Hp") as "#Hs".
    iMod ("Hcl" with "[-]") as "_".
    { iNext. iExists m. iRight. iFrame. done. }
516 517
    iApply (bin_log_related_seq' _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ TUnit TUnit with "[Hg]").
Dan Frumin's avatar
Dan Frumin committed
518
      iApply bin_log_related_val; eauto using to_of_val.
519
      iApply bin_log_related_unit. }
520 521
    iApply (bin_log_related_seq' _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ τg TUnit with "[Hf]").
Dan Frumin's avatar
Dan Frumin committed
522 523
      iApply bin_log_related_val; eauto using to_of_val.
      by iApply profiled_g'. }
524 525 526 527 528 529 530 531 532 533 534 535 536
    rel_seq_l. rel_seq_r.
    rel_load_l_atomic. clear m.
    iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
      iModIntro; iExists _; iFrame.
    { iExFalso. by iApply shot_not_pending. }
    iNext. iIntros "Hc1".
    rel_load_r. rel_op_r.
    iMod ("Hcl" with "[-]") as "_".
    { iNext. iExists m. iRight. iFrame. }
    rewrite Nat.add_1_r.
    iApply bin_log_related_nat.
  Qed.

537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
  Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} Γ :
    Γ 
      (λ: "f" "g" "f'",
       let: "pg" := p "g" in
       let: "g'" := Fst "pg" in
       let: "g''" := Snd "pg" in
       "f" "g'";; "g'" #();; "f'" "g'";; "g''" #())
    log
      (λ: "f" "g" "f'",
       let: "pg" := p "g" in
       let: "g'" := Fst "pg" in
       let: "g''" := Snd "pg" in
       "f" "g'";; "g" #();; "f'" "g'";; "g''" #() + #1)
    : TArrow τf (TArrow τg (TArrow τf TNat)).
  Proof.
    iIntros (Δ).
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f1 f2) "#Hf". fold interp.
    rel_let_l. rel_let_r.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (g1 g2)"#Hg". fold interp.
    rel_let_l. rel_let_r.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f'1 f'2) "#Hf'". fold interp.
    rel_let_l. rel_let_r.
    unlock p. simpl.
    rel_let_l. rel_let_r.
    rel_alloc_l as c1 "Hc1".
    rel_alloc_r as c2 "Hc2".
566
    iMod new_pending as (γ) "Ht".
567 568 569 570 571 572 573 574 575
    iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done.
    iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv".
    { iNext. iExists 0. iLeft. iFrame. }
    rel_let_l. rel_let_r.
    rel_let_l. rel_let_r.
    rel_proj_l. rel_proj_r.
    rel_let_l. rel_let_r.
    rel_proj_l. rel_proj_r.
    rel_let_l. rel_let_r.
576 577
    iApply (bin_log_related_seq' _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ τg TUnit with "[Hf]").
Dan Frumin's avatar
Dan Frumin committed
578 579
      iApply bin_log_related_val; eauto using to_of_val.
      by iApply profiled_g'. }
580
    rel_seq_l.
581 582 583
    rel_apply_l (bin_log_FG_increment_logatomic _
      (fun (n : nat) => (c2 ↦ₛ #n  pending γ)  (c2 ↦ₛ #(n-1)  shot γ  own γ' (Excl ())  1  n))%I with "Ht'").
    iAlways.
584 585
    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
      iModIntro; iExists _; iFrame; last first.
586 587 588
    { iSplitL "Hc2 Ht Ht'2".
      { iRight. simpl. rewrite -minus_n_O. iFrame. iPureIntro. omega. }
      iSplit.
589 590 591
      - iIntros. iApply "Hcl". iApply close_i6.
        iNext. iExists _; iFrame.
      - iIntros "[Hc1 Hc2] Ht".
592 593 594 595 596 597
        rel_seq_l.
        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
    }
    { iSplitL "Hc2 Ht".
      { iLeft. by iFrame. }
      iSplit.
598 599 600
      - iIntros. iApply "Hcl". iApply close_i6.
        iNext. iExists _; iFrame.
      - iIntros  "[Hc1 Hc2] Ht".
601 602 603
        rel_seq_l.
        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
    }
604 605
  Qed.

Dan Frumin's avatar
Dan Frumin committed
606
End refinement.