[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 88 from proof inv-commit (previous step)

# avol = # avol0, # lpt0 = # lpt, # lebs(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt = # avol0, avol0[0] = mapped(buf2), avol0[3] = mapped(buf0), avol0[1] = mapped(buf1), err = ESUCCESS, sb0 = mksb(adr0, m2, 1, 3, m6, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), 4 < # avol0, 2 < # avol0, ebm-vol-inv(avol2), ebm-vol-inv(avol0[2, mapped(mkbuf(0))]), ebm-vol-inv(avol0), ebm-vol-inv(avol0[2, mapped(mkbuf(0))][4, mapped(buf)]), ebm-vol-inv(avol), is-encoded(lpt, lebs(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded(lpt0, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr0, m2, 1, 3, m6, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf2), is-encoded-pad(orphans0, m6, buf0), is-encoded-pad(orphans, # orphans, buf), mapped-full?(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), range=(avol, 0, avol0[2, mapped(mkbuf(0))][4, mapped(buf)], 0, 5 + lptlebs(# lpt, LEB_SIZE)), range=(avol, 5 + 2 * lptlebs(# lpt, LEB_SIZE), avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lpt), 2 * lptlebs(# lpt, LEB_SIZE) + 5 ≤ # avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, err ≠ ESUCCESS → avol2 = avol, logoff ≠ LEB_SIZE → # buf1 = logoff, err = ESUCCESS → id○(avol2, avol, 0) ∧ is-encoded(mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf3) ∧ avol2[0] = mapped(buf3), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪sb0 := mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)); logoff := 0⟫ ( (∃ lpt1, log, orphans. disk-layout(sb0, # lpt1) ∧ sb0.main + # lpt1 = # avol2 ∧ avol2[0].mapped? ∧ is-encoded(sb0, avol2[0].data) ∧ avol2[sb0.orph].mapped? ∧ is-encoded-pad(orphans, sb0.orphsize, avol2[sb0.orph].data) ∧ avol2[sb0.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol2[sb0.log].data = logoff) ∧ is-encoded(log, avol2[sb0.log].data) ∧ mapped-full?(avol2, sb0.lpt, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, sb0.lpt, lptlebs(# lpt1, LEB_SIZE)))) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb0.indexaddr = adr ∧ sb0.maxino = m3 ∧ avol2[sb0.log].data = mkbuf(0) ∧ is-encoded(lpt, lebs(avol2, sb0.lpt, lptlebs(# avol2 - sb0.main, LEB_SIZE))) ∧ is-encoded-pad(orphans, sb0.orphsize, avol2[sb0.orph].data)) ∧ ( err ≠ ESUCCESS → sb0 = mksb(adr0, m2, 1, 3, m6, 5, sb0.main) ∧ avol2[1] = avol0[1] ∧ avol2[3] = avol0[3] ∧ lebs(avol2, 5, lptlebs(# avol2 - sb0.main, LEB_SIZE)) = lebs(avol0, 5, lptlebs(# avol2 - sb0.main, LEB_SIZE))) ∧ sb0.main = 5 + 2 * lptlebs(# lpt, LEB_SIZE) ∧ # avol2 = # avol0 ∧ subarray(avol2, sb0.main, # avol2 - sb0.main) = subarray(avol0, sb0.main, # avol2 - sb0.main))

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 89:
# lebs(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)) = lptsize(# lpt, LEB_SIZE), # lpt0 = # lpt, # avol = # avol0, (5 + 2 * lptlebs(# lpt, LEB_SIZE)) + # lpt = # avol0, avol0[1] = mapped(buf1), avol0[3] = mapped(buf0), avol0[0] = mapped(buf2), err = ESUCCESS, sb0 = mksb(adr0, m2, 1, 3, m6, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), 2 < # avol0, 4 < # avol0, ebm-vol-inv(avol), ebm-vol-inv(avol0[2, mapped(mkbuf(0))][4, mapped(buf)]), ebm-vol-inv(avol0), ebm-vol-inv(avol0[2, mapped(mkbuf(0))]), ebm-vol-inv(avol2), is-encoded(mksb(adr0, m2, 1, 3, m6, 5, 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf2), is-encoded(lpt0, lebs(avol0, 5, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf1), is-encoded(lpt, lebs(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE))), is-encoded-pad(orphans, # orphans, buf), is-encoded-pad(orphans0, m6, buf0), mapped-full?(avol0, 5, lptlebs(# lpt, LEB_SIZE)), mapped-full?(avol, 5 + lptlebs(# lpt, LEB_SIZE), lptlebs(# lpt, LEB_SIZE)), range=(avol, 5 + 2 * lptlebs(# lpt, LEB_SIZE), avol0, 5 + 2 * lptlebs(# lpt, LEB_SIZE), # lpt), range=(avol, 0, avol0[2, mapped(mkbuf(0))][4, mapped(buf)], 0, 5 + lptlebs(# lpt, LEB_SIZE)), 5 + 2 * lptlebs(# lpt, LEB_SIZE) ≤ # avol0, 2 * lptlebs(# lpt, LEB_SIZE) + 5 ≤ # avol0, err = ESUCCESS → id○(avol2, avol, 0) ∧ is-encoded(mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), buf3) ∧ avol2[0] = mapped(buf3), logoff ≠ LEB_SIZE → # buf1 = logoff, err ≠ ESUCCESS → avol2 = avol, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪logoff := 0⟫ ( (∃ lpt1, log, orphans0. disk-layout(mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), # lpt1) ∧ mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main + # lpt1 = # avol2 ∧ avol2[0].mapped? ∧ is-encoded(mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)), avol2[0].data) ∧ avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).orph].mapped? ∧ is-encoded-pad (orphans0, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).orphsize, avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).orph].data) ∧ avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).log].mapped? ∧ ( logoff ≠ LEB_SIZE → # avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).log].data = logoff) ∧ is-encoded (log, avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).log].data) ∧ mapped-full? (avol2, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).lpt, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded (lpt1, lebs (avol2, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).lpt, lptlebs(# lpt1, LEB_SIZE)))) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).indexaddr = adr ∧ mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).maxino = m3 ∧ avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).log].data = mkbuf(0) ∧ is-encoded (lpt, lebs (avol2, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).lpt, lptlebs (# avol2 - mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main, LEB_SIZE))) ∧ is-encoded-pad (orphans, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).orphsize, avol2[mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).orph].data)) ∧ ( err ≠ ESUCCESS → mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)) = mksb (adr0, m2, 1, 3, m6, 5, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main) ∧ avol2[1] = avol0[1] ∧ avol2[3] = avol0[3] ∧ lebs (avol2, 5, lptlebs (# avol2 - mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main, LEB_SIZE)) = lebs (avol0, 5, lptlebs (# avol2 - mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main, LEB_SIZE))) ∧ mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main = 5 + 2 * lptlebs(# lpt, LEB_SIZE) ∧ # avol2 = # avol0 ∧ subarray (avol2, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main, # avol2 - mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main) = subarray (avol0, mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main, # avol2 - mksb(adr, m3, 2, 4, # orphans, 5 + lptlebs(# lpt, LEB_SIZE), 5 + 2 * lptlebs(# lpt, LEB_SIZE)).main))

Proof step 88 from proof inv-commit (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information