[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 9 from proof refine-add-log-leb (previous step)

# avol = # lpt0 + m5, avol[m0] = mapped(buf1), avol[m1] = mapped(buf0), avol[0] = mapped(buf), avol = avol, avol0 = subarray(avol, m5, # lpt0), avol1 = avol, log0 = plog, lpt1 = lpt0, m6 = m2, orphans0 = orphans, sb0 = mksb(adr, m, m0, m1, m3, m4, m5), disk-layout(mksb(adr, m, m0, m1, m3, m4, m5), # lpt0), ebm-vol-inv(subarray(avol, m5, # lpt0)), ebm-vol-inv(avol), is-encoded(mksb(adr, m, m0, m1, m3, m4, m5), buf), is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE))), is-encoded(plog, buf1), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)), persistence-io-inv(mksb(adr, m, m0, m1, m3, m4, m5), logoff, avol, lpt0, plog, orphans), m5 ≤ # avol, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ [persistence_io_add_log_leb#(m2, mksb(adr, m, m0, m1, m3, m4, m5), EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, sb0.main, # lpt1) = subarray(avol1, sb0.main, # lpt1) ∧ (err = ESUCCESS → persistence-io-inv(sb0, logoff, avol, lpt1, log0 + m6, orphans0)) ∧ (err ≠ ESUCCESS → persistence-io-inv(sb0, logoff, avol, lpt1, log0, orphans0)) → ⟨apersistence_io_add_log_leb#(m2, adr, m, avol0, lpt0, orphans; plog; err0)⟩ ( # avol = m5 + (# avol - m5) ∧ avol0 = subarray(avol, m5, # avol - m5) ∧ is-encoded(plog, avol[m0].data) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# avol - m5, LEB_SIZE))) ∧ is-encoded-pad(orphans, m3, avol[m1].data) ∧ err = err0))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 10:
# avol = # lpt0 + m5, avol[0] = mapped(buf), avol[m1] = mapped(buf0), avol[m0] = mapped(buf1), avol0 = subarray(avol, m5, # lpt0), avol1 = avol, disk-layout(mksb(adr, m, m0, m1, m3, m4, m5), # lpt0), ebm-vol-inv(avol), ebm-vol-inv(subarray(avol, m5, # lpt0)), is-encoded(plog, buf1), is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE))), is-encoded(mksb(adr, m, m0, m1, m3, m4, m5), buf), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)), m5 ≤ # avol, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ [persistence_io_add_log_leb#(m2, mksb(adr, m, m0, m1, m3, m4, m5), EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, m5, # lpt0) = subarray(avol1, m5, # lpt0) ∧ ( err = ESUCCESS → m5 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m1, m3, m4, m5), avol[0].data) ∧ avol[m1].mapped? ∧ is-encoded-pad(orphans, m3, avol[m1].data) ∧ avol[m0].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0].data = logoff) ∧ is-encoded(plog + m2 ', avol[m0].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE)))) ∧ ( err ≠ ESUCCESS → m5 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m1, m3, m4, m5), avol[0].data) ∧ avol[m1].mapped? ∧ is-encoded-pad(orphans, m3, avol[m1].data) ∧ avol[m0].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0].data = logoff) ∧ is-encoded(plog, avol[m0].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE)))) → ⟨apersistence_io_add_log_leb#(m2, adr, m, avol0, lpt0, orphans; plog; err0)⟩ ( # avol = m5 + (# avol - m5) ∧ avol0 = subarray(avol, m5, # avol - m5) ∧ is-encoded(plog, avol[m0].data) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# avol - m5, LEB_SIZE))) ∧ is-encoded-pad(orphans, m3, avol[m1].data) ∧ err = err0))

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded(nx0, buf) → (is-encoded(nx1, buf) ↔ nx0 = nx1); (s)%⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ mapped(buf).data = buf; (s)% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)% ⊦ nx + n = nx + n '; (s)% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt = m3; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log = m0; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orphsize = m2; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orph = m1; (s)%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main = m4; (s)%m = n ⊦ disk-layout(sb, m) → disk-layout(sb, n); (s)%⊦ persistence-io-inv(sb, logoff, avol, lpt, log, orphans) ↔ (∃ mainareasize. disk-layout(sb, mainareasize) ∧ sb.main + mainareasize = # avol ∧ avol[0].mapped? ∧ is-encoded(sb, avol[0].data) ∧ avol[sb.orph].mapped? ∧ is-encoded-pad(orphans, sb.orphsize, avol[sb.orph].data) ∧ avol[sb.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[sb.log].data = logoff) ∧ is-encoded(log, avol[sb.log].data) ∧ mapped-full?(avol, sb.lpt, lptlebs(mainareasize, LEB_SIZE)) ∧ # lpt = mainareasize ∧ is-encoded (lpt, lebs(avol, sb.lpt, lptlebs(mainareasize, LEB_SIZE)))); (s)