Proof step 83 from proof synced-write-buf (previous step)

Heuristic symbolic execution applied rule choose left

And obtained the following new goals

• Proof step 84:

  ⟨avol[m] := mapped(avol[m].data + subarray(buf, 0, n)); isbuf := true⟩ (avol = avol1 ∧ (isbuf ↔ isbuf0) ∧ err2 = err1), ⟨fail_or_success#(; ; err)⟩ (err = err2), # lpt = # avol, avol[m1] = mapped(buf0), bleb = buffered(m1), ¬ isbuf, m = bleb.leb, m0 = m2, n0 = n2, bleb.isbuf?, m1 < # avol, n < n0, awbuf-inv(avol, buffered(m1)), is-aligned(# avol[m].data + n, EB_PAGE_SIZE), avol0 ↓ avol1, # buf0 + n2 ≤ LEB_SIZE, n2 ≤ # buf, # avol[bleb.leb].data + n0 ≤ LEB_SIZE, n0 ≤ # buf, bleb ≠ nobuffer → avol[bleb.leb].mapped? ∧ bleb.leb < # avol ∧ bleb.isbuf?, n ≠ 0 → n < n0 → avol[m].mapped? ∧ m < # avol ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; let m = buffered(m1).leb in if err = ESUCCESS then avol[m] := mapped(avol[m].data + subarray(buf, 0, n2)) else { choose n1 with n1 ≠ 0 ∧ n1 < n2 ∧ is-aligned(# avol[m].data + n1, EB_PAGE_SIZE) in avol[m] := mapped(avol[m].data + subarray(buf, 0, n1)) ifnone skip or skip; isbuf := true}⟩ (synced(avol) ∧ avol0 ↓ avol), bleb = nobuffer, err2 = ESUCCESS, n = 0, avol0 ↓ avol

• Proof step 121:

  ⟨skip; isbuf := true⟩ (avol = avol1 ∧ (isbuf ↔ isbuf0) ∧ err2 = err1), ⟨fail_or_success#(; ; err)⟩ (err = err2), # lpt = # avol, avol[m1] = mapped(buf0), bleb = buffered(m1), ¬ isbuf, m = bleb.leb, m0 = m2, n0 = n, bleb.isbuf?, m1 < # avol, awbuf-inv(avol, buffered(m1)), avol0 ↓ avol1, # buf0 + n ≤ LEB_SIZE, n ≤ # buf, # avol[bleb.leb].data + n0 ≤ LEB_SIZE, n0 ≤ # buf, bleb ≠ nobuffer → avol[bleb.leb].mapped? ∧ bleb.leb < # avol ∧ bleb.isbuf?, ∀ n. (n ≠ 0 → n < n0 → avol[m].mapped? ∧ m < # avol) ∧ ¬(n ≠ 0 ∧ n < n0 ∧ is-aligned(# avol[m].data + n, EB_PAGE_SIZE)) ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; let m = buffered(m1).leb in if err = ESUCCESS then avol[m] := mapped(avol[m].data + subarray(buf, 0, n)) else { choose n1 with n1 ≠ 0 ∧ n1 < n ∧ is-aligned(# avol[m].data + n1, EB_PAGE_SIZE) in avol[m] := mapped(avol[m].data + subarray(buf, 0, n1)) ifnone skip or skip; isbuf := true}⟩ (synced(avol) ∧ avol0 ↓ avol), bleb = nobuffer, err2 = ESUCCESS, avol0 ↓ avol

Rule argument

Additional information