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

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 28:

  ⟨fail_or_success#(; ; err)⟩ (err = err2), # lpt = # avol, isbuf ↔ isbuf0, avol[m1] = mapped(buf0), avol[m, mapped(avol[m].data + subarray(buf, 0, n0))] = avol1, bleb = buffered(m1), err2 = ESUCCESS, err2 = err1, ¬ isbuf, m = bleb.leb, m0 = m2, n0 = n, bleb.isbuf?, avol[m].mapped?, m1 < # avol, m < # avol, awbuf-inv(avol, buffered(m1)), avol0 ↓ avol1, n0 ≤ # buf, # avol[bleb.leb].data + n0 ≤ LEB_SIZE, n ≤ # buf, # buf0 + n ≤ LEB_SIZE, 0 + n0 ≤ # buf, bleb ≠ nobuffer → avol[bleb.leb].mapped? ∧ bleb.leb < # avol ∧ bleb.isbuf? ⊦ ∃ 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, avol0 ↓ avol

Rule argument

Additional information