Proof step 8 from proof prepost-add-log-leb (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 9:

  m5 + # lpt = # avol, avol[0] = mapped(buf2), avol[m2] = mapped(buf0), avol[m6] = mapped(buf1), avol0 = avol, buf = mkbuf(m0), m = LEB_SIZE, m0 = EB_PAGE_SIZE, m1 = m8, sb = mksb(adr, m7, m6, m2, m3, m4, m5), disk-layout(mksb(adr, m7, m6, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m7, m6, m2, m3, m4, m5), buf2), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), logoff + m0 ≤ m, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ ⟪encode_ref_node#(m0, rnode(m1); buf; err); if err = ESUCCESS then {ebm_avol_write#(sb.log, logoff, 0, m0, buf; avol; err); if err = ESUCCESS then logoff := logoff + m0 else {logoff := m; debug#("persistence-io: failed to add LEB " + m1.toString + " to log")}}⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, m5, # lpt) = subarray(avol0, m5, # lpt) ∧ ( err = ESUCCESS → m5 + # lpt = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m7, m6, m2, m3, m4, m5), avol[0].data) ∧ avol[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol[m2].data) ∧ avol[m6].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m6].data = logoff) ∧ is-encoded(log + m8 ', avol[m6].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE)))) ∧ ( err ≠ ESUCCESS → m5 + # lpt = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m7, m6, m2, m3, m4, m5), avol[0].data) ∧ avol[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol[m2].data) ∧ avol[m6].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m6].data = logoff) ∧ is-encoded(log, avol[m6].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE)))))

Rule argument

Additional information