Proof step 19 from proof inv-read-buf (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 20:

  # buf1 = EB_PAGE_SIZE, # lpt = # avol, avol[m3] = mapped(buf2), buf0 = buf, buffered(m3) = bleb, err = ESUCCESS, err = err0, m = (m0 ≤ m5 ⊃ 0;m0 - m5), m1 = (m0 ≤ m5 ⊃ m5 - m0;0), avol[m3].mapped?, m3 < # avol, ebm-vol-inv(avol), m0 ≤ m5 + m4, m5 ≤ m0 + n, m0 + n ≤ LEB_SIZE, n ≤ # buf, 0 + n ≤ # buf0, m0 + n ≤ #(avol[m3].data + mkempbuf(LEB_SIZE - # avol[m3].data)), LEB_SIZE ≥ # avol[m3].data, bleb ≠ nobuffer → bleb.leb < # avol ∧ wbuf-cons(mkwbuf(buf1, m5, m4), avol[bleb.leb], rofs), (m0 ≤ m5 ⊃ true;m0 ≥ m5), (m0 ≤ m5 ⊃ m5 ≥ m0;true), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ( m + min(n - m1, m4 - m) ≤ # buf1 ∧ m1 + min(n - m1, m4 - m) ≤ # copy(avol[m3].data + mkempbuf(LEB_SIZE - # avol[m3].data), m0, buf0, 0, n)) ∧ ( (m0 + n ≤ #(avol[m3].data + mkempbuf(LEB_SIZE - # avol[m3].data)) ∧ 0 + n ≤ # buf0) ∧ (avol[m3].mapped? ∧ m3 < # avol) ∧ LEB_SIZE ≥ # avol[m3].data ∧ avol[m3].mapped? ∧ m3 < # avol) ∧ n ≥ m1 ∧ m4 ≥ m

Rule argument

Additional information