[Imprint][Data Privacy Statement][E-Mail]



View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

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

# buf3 = EB_PAGE_SIZE, m5 + # lpt = # avol, avol[m2] = mapped(buf0), avol[0] = mapped(buf2), avol[m6] = mapped(buf1), avol0 = avol, err = err0, err = ESUCCESS, logoff = # buf1, avol[m6].mapped?, m6 < # avol, disk-layout(mksb(adr, m7, m6, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))]), ebm-vol-inv(avol), is-encoded(rnode(m8), buf3), is-encoded(mksb(adr, m7, m6, m2, m3, m4, m5), buf2), is-encoded(lpt, lebs(avol, m4, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), 0 + EB_PAGE_SIZE ≤ # buf3, # buf1 + EB_PAGE_SIZE ≤ LEB_SIZE, # buf1 ≥ # avol[m6].data, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪logoff := logoff + EB_PAGE_SIZE⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ subarray(avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m5, # lpt) = subarray(avol0, m5, # lpt) ∧ ( err = ESUCCESS → m5 + # lpt = # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))] ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].mapped? ∧ is-encoded (mksb(adr, m7, m6, m2, m3, m4, m5), avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].mapped? ∧ is-encoded-pad (orphans, m3, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].mapped? ∧ ( logoff ≠ LEB_SIZE → # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data = logoff) ∧ is-encoded (log + m8 ', avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data) ∧ mapped-full? (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded (lpt, lebs (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)))) ∧ ( err ≠ ESUCCESS → m5 + # lpt = # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))] ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].mapped? ∧ is-encoded (mksb(adr, m7, m6, m2, m3, m4, m5), avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][0].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].mapped? ∧ is-encoded-pad (orphans, m3, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m2].data) ∧ avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].mapped? ∧ ( logoff ≠ LEB_SIZE → # avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data = logoff) ∧ is-encoded(log, avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))][m6].data) ∧ mapped-full? (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE)) ∧ is-encoded (lpt, lebs (avol[m6, mapped(avol[m6].data + mkempbuf(# buf1 - # avol[m6].data) + subarray(buf3, 0, EB_PAGE_SIZE))], m4, lptlebs(# lpt, LEB_SIZE))))), # buf1 = LEB_SIZE

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information