[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 12 from proof recovery (previous step)

# lpt0 = # avol2, # avol0 = sb.main + # avol2, adr0 = sb.indexaddr, adr1 = adr2, avol1 = avol1, avol2 = subarray(avol0, sb.main, # avol0 - sb.main), avol4 = avol1, avol5 = avol0, log1 = log2, lpt1 = lpt2, m0 = sb.maxino, m10 = m2, m11 = m3, m2 = EB_PAGE_SIZE, m3 = LEB_SIZE, m4 = m5, m9 = m1, orphans = ns1, sb1 = sb, ebm-vol-inv(avol2), ebm-vol-inv(avol0), is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol2, LEB_SIZE))), is-encoded(log0, avol0[sb.log].data), is-encoded-pad(ns0, sb.orphsize, avol0[sb.orph].data), avol0 ⊆ avol1, ∃ lpt1, log1, orphans. persistence-io-inv(sb, m1, avol0, lpt1, log1, orphans), ∃ lpt, log, orphans. persistence-io-inv(sb, m1, avol0, lpt, log, orphans) ⊦ [persistence_io_recover#(; adr1, m4, orphans, log1, lpt1, sb0, logoff, m6, m7, avol1; err)] ( ( err = ESUCCESS → (∃ lpt, log, orphans. persistence-io-inv(sb0, logoff, avol1, lpt, log, orphans)) ∧ m6 = EB_PAGE_SIZE ∧ m7 = LEB_SIZE ∧ ebm-vol-inv(avol1)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb0 = sb1 ∧ # avol1 = # avol5 ∧ adr1 = sb0.indexaddr ∧ m4 = sb0.maxino ∧ # lpt1 = # avol1 - sb0.main ∧ is-encoded(lpt1, lebs(avol1, sb0.lpt, lptlebs(# avol1 - sb0.main, LEB_SIZE))) ∧ lebs(avol1, sb0.lpt, lptlebs(# avol1 - sb0.main, LEB_SIZE)) = lebs(avol5, sb0.lpt, lptlebs(# avol1 - sb0.main, LEB_SIZE)) ∧ is-encoded(log1, avol1[sb0.log].data) ∧ is-encoded-pad(orphans, sb0.orphsize, avol1[sb0.orph].data) ∧ avol1[sb0.orph] = avol5[sb0.orph] ∧ avol1[sb0.log] = avol5[sb0.log]) → (err = ESUCCESS → avol4 = avol1) → ( err = ESUCCESS → (∃ adr, m, plog, avol, lpt, ns. (adr = adr0 ∧ m = m0 ∧ plog = log0 ∧ lpt = lpt0 ∧ avol2 ⊆ avol ∧ ns = ns0) ∧ ⟨apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr, m, plog, lpt, ns, avol; err0)⟩ ( ( m = sb0.maxino ∧ adr = sb0.indexaddr ∧ # avol1 = sb0.main + # avol ∧ avol = subarray(avol1, sb0.main, # avol1 - sb0.main) ∧ is-encoded(plog, avol1[sb0.log].data) ∧ is-encoded(lpt, lebs(avol1, sb0.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb0.orphsize, avol1[sb0.orph].data)) ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, log, avol, lpt, ns. ⟨apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr3, m8, plog0, lpt3, ns2, avol3; err0)⟩ ( adr = adr3 ∧ m = m8 ∧ log = plog0 ∧ avol = avol3 ∧ lpt = lpt3 ∧ ns = ns2 ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ err = err0))))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 13:
# lpt0 = # avol0 - sb.main, sb.main + # lpt4 = # avol0, avol0[sb.log] = mapped(buf1), avol0[sb.orph] = mapped(buf0), avol0[0] = mapped(buf), adr1 = adr2, avol4 = avol1, log1 = log2, lpt1 = lpt2, m4 = m5, orphans = ns1, disk-layout(sb, # lpt4), ebm-vol-inv(subarray(avol0, sb.main, # lpt0)), ebm-vol-inv(avol0), is-encoded(sb, buf), is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# lpt0, LEB_SIZE))), is-encoded(log0, buf1), is-encoded(lpt4, lebs(avol0, sb.lpt, lptlebs(# lpt4, LEB_SIZE))), is-encoded-pad(ns0, sb.orphsize, buf0), mapped-full?(avol0, sb.lpt, lptlebs(# lpt4, LEB_SIZE)), avol0 ⊆ avol1, m1 ≠ LEB_SIZE → # buf1 = m1 ⊦ [persistence_io_recover#(; adr1, m4, orphans, log1, lpt1, sb0, logoff, m6, m7, avol1; err)] ( ( err = ESUCCESS → (∃ lpt5, log4, orphans2. disk-layout(sb0, # lpt5) ∧ sb0.main + # lpt5 = # avol1 ∧ avol1[0].mapped? ∧ is-encoded(sb0, avol1[0].data) ∧ avol1[sb0.orph].mapped? ∧ is-encoded-pad(orphans2, sb0.orphsize, avol1[sb0.orph].data) ∧ avol1[sb0.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol1[sb0.log].data = logoff) ∧ is-encoded(log4, avol1[sb0.log].data) ∧ mapped-full?(avol1, sb0.lpt, lptlebs(# lpt5, LEB_SIZE)) ∧ is-encoded(lpt5, lebs(avol1, sb0.lpt, lptlebs(# lpt5, LEB_SIZE)))) ∧ m6 = EB_PAGE_SIZE ∧ m7 = LEB_SIZE ∧ ebm-vol-inv(avol1)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb0 = sb ∧ # avol1 = # avol0 ∧ adr1 = sb.indexaddr ∧ m4 = sb.maxino ∧ # lpt1 = # avol1 - sb.main ∧ is-encoded(lpt1, lebs(avol1, sb.lpt, lptlebs(# avol1 - sb.main, LEB_SIZE))) ∧ lebs(avol1, sb.lpt, lptlebs(# avol1 - sb.main, LEB_SIZE)) = lebs(avol0, sb.lpt, lptlebs(# avol1 - sb.main, LEB_SIZE)) ∧ is-encoded(log1, avol1[sb.log].data) ∧ is-encoded-pad(orphans, sb.orphsize, avol1[sb.orph].data) ∧ avol1[sb.orph] = avol0[sb.orph] ∧ avol1[sb.log] = avol0[sb.log]) → (err = ESUCCESS → avol4 = avol1) → ( err = ESUCCESS → (∃ avol. subarray(avol0, sb.main, # avol0 - sb.main) ⊆ avol ∧ ⟨adr := sb.indexaddr, m := sb.maxino; apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr, m, log0, lpt0, ns0, avol; err0)⟩ ( m = sb0.maxino ∧ adr = sb0.indexaddr ∧ # avol1 = sb0.main + (# avol1 - sb0.main) ∧ avol = subarray(avol1, sb0.main, # avol1 - sb0.main) ∧ is-encoded(log0, avol1[sb0.log].data) ∧ is-encoded(lpt0, lebs(avol1, sb0.lpt, lptlebs(# avol1 - sb0.main, LEB_SIZE))) ∧ is-encoded-pad(ns0, sb0.orphsize, avol1[sb0.orph].data) ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ ESUCCESS = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, log, avol, lpt, ns. ⟨apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr3, m8, plog0, lpt3, ns2, avol3; err0)⟩ ( adr = adr3 ∧ m = m8 ∧ log = plog0 ∧ avol = avol3 ∧ lpt = lpt3 ∧ ns = ns2 ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ err = err0))))

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded(lpt0, buf) ∧ # lpt0 = # lpt1 → (is-encoded(lpt1, buf) ↔ lpt0 = lpt1); (s)% ⊦ mapped(buf).data = buf; (s)%m = n ⊦ disk-layout(sb, m) → disk-layout(sb, n); (s)%n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s)% ⊦ m + m0 < n → ¬ n + n0 < m; (s)% ⊦ m < n → n ≠ 0; (s)%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%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% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)% ⊦ 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)%⊦ 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 ↔ ¬ n < m; (ss)% ⊦ # subarray(avol, m, n) = n; (s)