Proof step 48 from proof prepost-write-lebs (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 49:

  # avol0 = # avol1, # buf = (n2 + n4) * LEB_SIZE, # avol1 = n3 + n5 + n2 + n4, avol = avol0[n5 + n4, mapped(mkbuf(0))], err = err0, lebs(avol0, n5, n4) = subarray(buf, 0, n4 * LEB_SIZE), m = 0, m0 = n5 + n4, n0 = LEB_SIZE, n1 = n4 * LEB_SIZE, avol[m0].mapped?, m0 < # avol, n < n0, n5 + n4 < # avol1, n5 + n4 < # avol0, ebm-vol-inv(avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))]), ebm-vol-inv(avol0[n5 + n4, mapped(mkbuf(0))]), ebm-vol-inv(avol1), ebm-vol-inv(avol0), is-aligned(n, EB_PAGE_SIZE), is-aligned(LEB_SIZE, EB_PAGE_SIZE), mapped-full?(avol0, n5, n4), range=(avol0, n5 + n2 + n4, avol1, n5 + n2 + n4, n3), range=(avol0, 0, avol1, 0, n5), n1 + n ≤ # buf, n4 * LEB_SIZE + LEB_SIZE ≤ # buf, n5 + n2 + n4 ≤ # avol1, m ≥ # avol[m0].data, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪n6 := n4 + 1⟫ ( n6 ≤ n2 + n4 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))] = # avol1 ∧ range=(avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))], 0, avol1, 0, n5) ∧ range=(avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))], n5 + n2 + n4, avol1, n5 + n2 + n4, n3) ∧ ( err = ESUCCESS → lebs(avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))], n5, n6) = subarray(buf, 0, n6 * LEB_SIZE) ∧ mapped-full?(avol[m0, mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n))], n5, n6)) ∧ n4 < n6), n3 + n2 = 0, err = ESUCCESS, n = 0, n2 = 0

Rule argument

Additional information