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

m5 + # lpt = # avol, avol[m0] = mapped(buf1), avol[m2] = mapped(buf0), avol[0] = mapped(buf), disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt), ebm-vol-inv(avol), is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), buf), 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)), logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ ⟪persistence_io_add_log_leb#(m1, mksb(adr, m, m0, m2, m3, m4, m5), EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)⟫ ( (∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol[0].data) ∧ avol[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol[m2].data) ∧ avol[m0].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0].data = logoff) ∧ is-encoded(log, avol[m0].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE)))) ∧ ebm-vol-inv(avol))

User applied rule insert program lemma

And obtained the following new goals

Proof step 6:
persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), avol0 = avol ⊦ ⟪persistence_io_add_log_leb#(m, sb, EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, sb.main, # lpt) = subarray(avol0, sb.main, # lpt) ∧ (err = ESUCCESS → persistence-io-inv(sb, logoff, avol, lpt, log + m, orphans)) ∧ (err ≠ ESUCCESS → persistence-io-inv(sb, logoff, avol, lpt, log, orphans)))
Proof step 7:
m5 + # lpt = # avol, avol[0] = mapped(buf), avol[m2] = mapped(buf0), avol[m0] = mapped(buf1), avol = avol, avol1 = avol, log0 = log, lpt0 = lpt, m6 = m1, orphans0 = orphans, sb0 = mksb(adr, m, m0, m2, m3, m4, m5), disk-layout(mksb(adr, m, m0, 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, m, m0, m2, m3, m4, m5), buf), is-encoded-pad(orphans, m3, buf0), mapped-full?(avol, m4, lptlebs(# lpt, LEB_SIZE)), persistence-io-inv(mksb(adr, m, m0, m2, m3, m4, m5), logoff, avol, lpt, log, orphans), logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ [persistence_io_add_log_leb#(m1, mksb(adr, m, m0, m2, m3, m4, m5), EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, sb0.main, # lpt0) = subarray(avol1, sb0.main, # lpt0) ∧ (err = ESUCCESS → persistence-io-inv(sb0, logoff, avol, lpt0, log0 + m6, orphans0)) ∧ (err ≠ ESUCCESS → persistence-io-inv(sb0, logoff, avol, lpt0, log0, orphans0)) → (∃ lpt0, log, orphans. disk-layout(mksb(adr, m, m0, m2, m3, m4, m5), # lpt0) ∧ m5 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m, m0, m2, m3, m4, m5), avol[0].data) ∧ avol[m2].mapped? ∧ is-encoded-pad(orphans, m3, avol[m2].data) ∧ avol[m0].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m0].data = logoff) ∧ is-encoded(log, avol[m0].data) ∧ mapped-full?(avol, m4, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m4, lptlebs(# lpt0, LEB_SIZE)))) ∧ ebm-vol-inv(avol))

Rule argument

spec: <toplevel> name: prepost-add-log-leb seq: persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), avol0 = avol ⊦ ⟪persistence_io_add_log_leb# (m, sb, EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, sb.main, # lpt) = subarray(avol0, sb.main, # lpt) ∧ ( err = ESUCCESS → persistence-io-inv (sb, logoff, avol, lpt, log + m, orphans)) ∧ ( err ≠ ESUCCESS → persistence-io-inv (sb, logoff, avol, lpt, log, orphans))) subst: [sb, m, avol, logoff, err, lpt, log, orphans, avol0] → [mksb(adr, m, m0, m2, m3, m4, m5), m1, avol, logoff, err, lpt, log, orphans, avol] flags: <all paths>

Additional information

Used simplifier rules: ⊦ 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)%m = n ⊦ disk-layout(sb, m) → disk-layout(sb, n); (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main = m4; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orph = m1; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).orphsize = m2; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log = m0; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt = m3; (s)% ⊦ mapped(buf).mapped?; (s)% ⊦ mapped(buf).data = buf; (s)%⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ is-encoded(nx0, buf) → (is-encoded(nx1, buf) ↔ nx0 = nx1); (s)