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

# avol = # lpt0 + m5, avol[0] = mapped(buf), avol[m1] = mapped(buf0), avol[m0] = mapped(buf1), avol0 = subarray(avol, m5, # lpt0), disk-layout(mksb(adr, m, m0, m1, m3, m4, m5), # lpt0), ebm-vol-inv(subarray(avol, m5, # lpt0)), ebm-vol-inv(avol), 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)⟫ ⟨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)

User applied rule insert program lemma

And obtained the following new goals

Proof step 8:
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 9:
# 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))

Rule argument

spec: persistence-io-asm 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, m1, m3, m4, m5), m2, avol, logoff, err, lpt0, plog, 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)%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ 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)