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

# lpt = # lpt2, # avol0 = # lpt2 + m6, avol0[0] = mapped(buf), avol0[m2] = mapped(buf0), avol0[m1] = mapped(buf1), 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(avol0), ebm-vol-inv(subarray(avol0, m6, # lpt2)), is-encoded(plog, buf1), is-encoded(lpt2, lebs(avol0, m5, lptlebs(# lpt2, LEB_SIZE))), is-encoded(mksb(adr0, m0, m1, m2, m4, m5, m6), buf), is-encoded-pad(ns, m4, buf0), mapped-full?(avol0, m5, lptlebs(# lpt2, LEB_SIZE)), m6 ≤ # avol0, logoff ≠ LEB_SIZE → # buf1 = logoff ⊦ ∀ 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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: ⊦ mapped(buf).data = buf; (s)%eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic% ⊦ is-encoded(nx0, buf) → (is-encoded(nx1, buf) ↔ nx0 = nx1); (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%⊦ is-encoded-pad(ns0, n, buf) → (is-encoded-pad(ns1, n, buf) ↔ ns0 = ns1); (s)% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)