| m8 + # lpt0 = # avol1, avol1[m10] = mapped(buf1), avol1[m5] = mapped(buf0), avol1[0] = mapped(buf), m0 = LEB_SIZE, m1 = EB_PAGE_SIZE, sb = mksb(adr1, m4, m11, m12, m13, m14, m15), disk-layout(mksb(adr0, m9, m10, m5, m6, m7, m8), # lpt0), ebm-vol-inv(avol1), is-encoded(lpt0, lebs(avol1, m7, lptlebs(# lpt0, LEB_SIZE))), is-encoded(log0, buf1), is-encoded(mksb(adr0, m9, m10, m5, m6, m7, m8), buf), is-encoded-pad(orphans0, m6, buf0), mapped-full?(avol1, m7, lptlebs(# lpt0, LEB_SIZE)), m8 ≤ # avol1, avol1 ⊆ avol2, ⌊err⌋ , m3 ≠ LEB_SIZE → # buf1 = m3 ⊦ ⟪skip; if err = ESUCCESS then {persistence_io_read_orphans#(sb, avol2; orphans; err); if err ≠ ESUCCESS then debug#("persistence-io: reading orphans failed")}; if err = ESUCCESS then {m := # avol2 - m15; let buf = ? in {persistence_io_read_lebs#(m14, lptlebs(m, m0), m0, avol2; ; buf, err); if err = ESUCCESS then {lpt := mklparray(m); lpt := fill(lpt, mklp(0, 0, LP_FREE, 0)); persistence_io_decode_lpt#(buf; lpt, err)}; if err ≠ ESUCCESS then debug#("persistence-io: reading LPT failed")}}; if err = ESUCCESS then {logoff := m0; adr := adr1; m2 := m4}⟫ ( ( err = ESUCCESS → (∃ lpt1, log1, orphans1. disk-layout(sb, # lpt1) ∧ m15 + # lpt1 = # avol1 ∧ is-encoded(sb, buf) ∧ avol2[m12].mapped? ∧ is-encoded-pad(orphans1, m13, avol2[m12].data) ∧ avol2[m11].mapped? ∧ (logoff ≠ LEB_SIZE → # avol2[m11].data = logoff) ∧ is-encoded(log1, avol2[m11].data) ∧ mapped-full?(avol2, m14, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, m14, lptlebs(# lpt1, LEB_SIZE)))) ∧ m1 = EB_PAGE_SIZE ∧ m0 = LEB_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb = mksb(adr0, m9, m10, m5, m6, m7, m8) ∧ adr = adr0 ∧ m2 = m9 ∧ # lpt = # lpt0 ∧ is-encoded(lpt, lebs(avol2, m7, lptlebs(# lpt, LEB_SIZE))) ∧ lebs(avol2, m7, lptlebs(# lpt, LEB_SIZE)) = lebs(avol1, m7, lptlebs(# lpt, LEB_SIZE)) ∧ log0 = log ∧ orphans0 = orphans)) |
m8 + # lpt0 = # avol1, avol1[0] = mapped(buf), avol1[m5] = mapped(buf0), avol1[m10] = mapped(buf1), m0 = LEB_SIZE, m1 = EB_PAGE_SIZE, sb = mksb(adr1, m4, m11, m12, m13, m14, m15), disk-layout(mksb(adr0, m9, m10, m5, m6, m7, m8), # lpt0), ebm-vol-inv(avol1), is-encoded(mksb(adr0, m9, m10, m5, m6, m7, m8), buf), is-encoded(log0, buf1), is-encoded(lpt0, lebs(avol1, m7, lptlebs(# lpt0, LEB_SIZE))), is-encoded-pad(orphans0, m6, buf0), mapped-full?(avol1, m7, lptlebs(# lpt0, LEB_SIZE)), m8 ≤ # avol1, avol1 ⊆ avol2, ⌊err⌋ , m3 ≠ LEB_SIZE → # buf1 = m3 ⊦ ⟪if err = ESUCCESS then {persistence_io_read_orphans#(sb, avol2; orphans; err); if err ≠ ESUCCESS then debug#("persistence-io: reading orphans failed")}; if err = ESUCCESS then {m := # avol2 - m15; let buf = ? in {persistence_io_read_lebs#(m14, lptlebs(m, m0), m0, avol2; ; buf, err); if err = ESUCCESS then {lpt := mklparray(m); lpt := fill(lpt, mklp(0, 0, LP_FREE, 0)); persistence_io_decode_lpt#(buf; lpt, err)}; if err ≠ ESUCCESS then debug#("persistence-io: reading LPT failed")}}; if err = ESUCCESS then {logoff := m0; adr := adr1; m2 := m4}⟫ ( ( err = ESUCCESS → (∃ lpt1, log1, orphans1. disk-layout(sb, # lpt1) ∧ m15 + # lpt1 = # avol1 ∧ is-encoded(sb, buf) ∧ avol2[m12].mapped? ∧ is-encoded-pad(orphans1, m13, avol2[m12].data) ∧ avol2[m11].mapped? ∧ (logoff ≠ LEB_SIZE → # avol2[m11].data = logoff) ∧ is-encoded(log1, avol2[m11].data) ∧ mapped-full?(avol2, m14, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, m14, lptlebs(# lpt1, LEB_SIZE)))) ∧ m1 = EB_PAGE_SIZE ∧ m0 = LEB_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb = mksb(adr0, m9, m10, m5, m6, m7, m8) ∧ adr = adr0 ∧ m2 = m9 ∧ # lpt = # lpt0 ∧ is-encoded(lpt, lebs(avol2, m7, lptlebs(# lpt, LEB_SIZE))) ∧ lebs(avol2, m7, lptlebs(# lpt, LEB_SIZE)) = lebs(avol1, m7, lptlebs(# lpt, LEB_SIZE)) ∧ log0 = log ∧ orphans0 = orphans))