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

# avol0 = # lpt1 + m6, # lpt = # lpt1, # lpt + sb.main = # avol0, EB_PAGE_SIZE = EB_PAGE_SIZE, LEB_SIZE = LEB_SIZE, avol0[m1] = mapped(buf1), avol0[m2] = mapped(buf0), avol0[0] = mapped(buf), adr2 = adr1, avol = subarray(avol0, m6, # lpt1), avol0 = avol0, avol1 = avol0, lpt0 = lpt, m7 = EB_PAGE_SIZE, m8 = LEB_SIZE, m9 = m3, ns1 = orphans, orphans = ns0, orphans = orphans, sb = mksb(adr0, m0, m1, m2, m4, m5, m6), sb = sb, sb1 = sb, disk-layout(mksb(adr0, m0, m1, m2, m4, m5, m6), # lpt1), ebm-vol-inv(subarray(avol0, m6, # lpt1)), ebm-vol-inv(avol0), is-encoded(mksb(adr0, m0, m1, m2, m4, m5, m6), buf), is-encoded(lpt1, lebs(avol0, m5, lptlebs(# lpt1, LEB_SIZE))), is-encoded(plog, buf1), is-encoded-pad(ns, m4, buf0), mapped-full?(avol0, m5, lptlebs(# lpt1, LEB_SIZE)), m6 ≤ # avol0, logoff ≠ LEB_SIZE → # buf1 = logoff, ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt, log, orphans) ⊦ [persistence_io_commit#(lpt, adr1, m3, EB_PAGE_SIZE, LEB_SIZE; orphans, sb, avol0, logoff; err)] ( (∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt, log, orphans)) ∧ ebm-vol-inv(avol0) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb.indexaddr = adr2 ∧ sb.maxino = m9 ∧ is-encoded([], avol0[sb.log].data) ∧ is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ is-encoded-pad(ns1, sb.orphsize, avol0[sb.orph].data)) ∧ ( err ≠ ESUCCESS → sb = sb1 ∧ avol0[sb.log] = avol1[sb.log] ∧ avol0[sb.orph] = avol1[sb.orph] ∧ lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE)) = lebs(avol1, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ sb.main = sb1.main ∧ # avol0 = # avol1 ∧ subarray(avol0, sb.main, # avol0 - sb.main) = subarray(avol1, sb.main, # avol0 - sb.main) → ⟨apersistence_io_commit#(lpt, adr1, m3, avol; ns0, adr0, m0, plog, lpt1, ns; err0)⟩ ( m0 = sb.maxino ∧ adr0 = sb.indexaddr ∧ # avol0 = sb.main + (# avol0 - sb.main) ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt1, lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data) ∧ orphans = ns0 ∧ err = err0))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 12:
# avol0 = # lpt2 + m6, # lpt = # lpt2, avol0[m1] = mapped(buf1), avol0[m2] = mapped(buf0), avol0[0] = mapped(buf), avol = subarray(avol0, m6, # lpt2), avol1 = avol0, orphans = ns0, sb = mksb(adr0, m0, m1, m2, m4, m5, m6), disk-layout(mksb(adr0, m0, m1, m2, m4, m5, m6), # lpt2), ebm-vol-inv(subarray(avol0, m6, # lpt2)), ebm-vol-inv(avol0), is-encoded(mksb(adr0, m0, m1, m2, m4, m5, m6), buf), is-encoded(lpt2, lebs(avol0, m5, lptlebs(# lpt2, LEB_SIZE))), is-encoded(plog, buf1), is-encoded-pad(ns, m4, buf0), mapped-full?(avol0, m5, lptlebs(# lpt2, LEB_SIZE)), m6 ≤ # avol0, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ [persistence_io_commit#(lpt, adr1, m3, EB_PAGE_SIZE, LEB_SIZE; orphans, sb, avol0, logoff; err)] ( (∃ lpt0, log, orphans0. disk-layout(sb, # lpt0) ∧ sb.main + # lpt0 = # avol0 ∧ avol0[0].mapped? ∧ is-encoded(sb, avol0[0].data) ∧ avol0[sb.orph].mapped? ∧ is-encoded-pad(orphans0, sb.orphsize, avol0[sb.orph].data) ∧ avol0[sb.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol0[sb.log].data = logoff) ∧ is-encoded(log, avol0[sb.log].data) ∧ mapped-full?(avol0, sb.lpt, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# lpt0, LEB_SIZE)))) ∧ ebm-vol-inv(avol0) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb.indexaddr = adr1 ∧ sb.maxino = m3 ∧ avol0[sb.log].data = mkbuf(0) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ is-encoded-pad(ns0, sb.orphsize, avol0[sb.orph].data)) ∧ ( err ≠ ESUCCESS → sb = mksb(adr0, m0, m1, m2, m4, m5, sb.main) ∧ avol0[m1] = avol1[m1] ∧ avol0[m2] = avol1[m2] ∧ lebs(avol0, m5, lptlebs(# avol0 - sb.main, LEB_SIZE)) = lebs(avol1, m5, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ sb.main = m6 ∧ # avol0 = # avol1 ∧ subarray(avol0, sb.main, # avol0 - sb.main) = subarray(avol1, sb.main, # avol0 - sb.main) → ⟨apersistence_io_commit#(lpt, adr1, m3, avol; ns0, adr0, m0, plog, lpt2, ns; err0)⟩ ( m0 = sb.maxino ∧ adr0 = sb.indexaddr ∧ # avol0 = sb.main + (# avol0 - sb.main) ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt2, lebs(avol0, sb.lpt, lptlebs(# avol0 - sb.main, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data) ∧ orphans = ns0 ∧ err = err0))

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded(lpt0, buf) ∧ # lpt0 = # lpt1 → (is-encoded(lpt1, buf) ↔ lpt0 = lpt1); (s)% ⊦ 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)% ⊦ is-encoded([], buf) ↔ buf = mkbuf(0); (s)%m = n ⊦ disk-layout(sb, m) → disk-layout(sb, n); (s)%eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; 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)% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).log = m0; (s)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).lpt = m3; (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)% ⊦ mksb(adr, m, m0, m1, m2, m3, m4).main = m4; (s)