| avol0 ⊆ avol1, m0 = sb.maxino, adr0 = sb.indexaddr, # avol0 = sb.main + # avol2, avol2 = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(log0, avol0[sb.log].data), is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol2, LEB_SIZE))), is-encoded-pad(ns0, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol2), # lpt0 = # avol2, ∃ lpt1, log1, orphans. persistence-io-inv(sb, m1, avol0, lpt1, log1, orphans), m2 = EB_PAGE_SIZE, m3 = LEB_SIZE, ebm-vol-inv(avol0), adr1 = adr2, m4 = m5, orphans = ns1, log1 = log2, lpt1 = lpt2 ⊦ ⟪persistence_io_recover#(; adr1, m4, orphans, log1, lpt1, sb0, logoff, m6, m7, avol1; err)⟫ ( ( 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)))) |