Proof step 34 from proof inv-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 35:

  m6 + # lpt = # avol, avol[m6 + m8] = mapped(buf0), avol[0] = mapped(buf1), avol[m3] = mapped(buf2), avol[m2] = mapped(buf3), m0 = m6 + m8, avol[m0].mapped?, m0 < # avol, n1 < n, m8 < # lpt, disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt), ebm-vol-inv(avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))]), ebm-vol-inv(avol), is-aligned(n1, EB_PAGE_SIZE), is-aligned(m7, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-encoded(log, buf3), is-encoded(lpt, lebs(avol, m5, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), buf1), is-encoded-pad(orphans, m4, buf2), mapped-full?(avol, m5, lptlebs(# lpt, LEB_SIZE)), n2 + n1 ≤ # buf, m7 + n ≤ LEB_SIZE, n2 + n ≤ # buf, # buf0 ≤ m7, m7 ≥ # avol[m0].data, logoff ≠ LEB_SIZE → # buf3 = logoff, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err0 = ESUCCESS, n1 = 0, ∃ lpt0, log, orphans. disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt0) ∧ m6 + # lpt0 = # avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))] ∧ avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][0].mapped? ∧ is-encoded (mksb(adr, m1, m2, m3, m4, m5, m6), avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][0].data) ∧ avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][m3].mapped? ∧ is-encoded-pad(orphans, m4, avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][m3].data) ∧ avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][m2].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][m2].data = logoff) ∧ is-encoded(log, avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))][m2].data) ∧ mapped-full?(avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))], m5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded (lpt0, lebs(avol[m0, mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1))], m5, lptlebs(# lpt0, LEB_SIZE)))

Rule argument

Additional information