| m6 + # lpt = # avol, avol[m2] = mapped(buf3), avol[m3] = mapped(buf2), avol[0] = mapped(buf1), avol[m6 + m8] = mapped(buf0), m = m7, m0 = m6 + m8, n0 = n, n1 = n2, m8 < # lpt, disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt), ebm-vol-inv(avol), is-aligned(n, EB_PAGE_SIZE), is-aligned(m7, EB_PAGE_SIZE), is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), buf1), is-encoded(lpt, lebs(avol, m5, lptlebs(# lpt, LEB_SIZE))), is-encoded(log, buf3), is-encoded-pad(orphans, m4, buf2), mapped-full?(avol, m5, lptlebs(# lpt, LEB_SIZE)), # buf0 ≤ m7, n2 + n ≤ # buf, m7 + n ≤ LEB_SIZE, logoff ≠ LEB_SIZE → # buf3 = logoff ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then if n0 ≠ 0 then avol[m0] := mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n0)) else choose n with n < n0 ∧ is-aligned(n, EB_PAGE_SIZE) in if n ≠ 0 then avol[m0] := mapped(avol[m0].data + mkempbuf(m - # avol[m0].data) + subarray(buf, n1, n)) ifnone skip] ( ebm-vol-inv(avol) → (∃ lpt0, log, orphans. disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt0) ∧ m6 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), avol[0].data) ∧ avol[m3].mapped? ∧ is-encoded-pad(orphans, m4, avol[m3].data) ∧ avol[m2].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m2].data = logoff) ∧ is-encoded(log, avol[m2].data) ∧ mapped-full?(avol, m5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m5, lptlebs(# lpt0, LEB_SIZE))))) |
m6 + # lpt = # avol, avol[m6 + m8] = mapped(buf0), avol[0] = mapped(buf1), avol[m3] = mapped(buf2), avol[m2] = mapped(buf3), m8 < # lpt, disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt), ebm-vol-inv(avol), is-aligned(m7, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-encoded(log, buf3), is-encoded(lpt, lebs(avol, m5, lptlebs(# lpt, LEB_SIZE))), is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), buf1), is-encoded-pad(orphans, m4, buf2), mapped-full?(avol, m5, lptlebs(# lpt, LEB_SIZE)), m7 + n ≤ LEB_SIZE, n2 + n ≤ # buf, # buf0 ≤ m7, logoff ≠ LEB_SIZE → # buf3 = logoff ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then if n ≠ 0 then avol[m6 + m8] := mapped(avol[m6 + m8].data + mkempbuf(m7 - # avol[m6 + m8].data) + subarray(buf, n2, n)) else {m0 := m6 + m8; choose n1 with n1 < n ∧ is-aligned(n1, EB_PAGE_SIZE) in if n1 ≠ 0 then avol[m0] := mapped(avol[m0].data + mkempbuf(m7 - # avol[m0].data) + subarray(buf, n2, n1)) ifnone skip}] ( ebm-vol-inv(avol) → (∃ lpt0, log, orphans. disk-layout(mksb(adr, m1, m2, m3, m4, m5, m6), # lpt0) ∧ m6 + # lpt0 = # avol ∧ avol[0].mapped? ∧ is-encoded(mksb(adr, m1, m2, m3, m4, m5, m6), avol[0].data) ∧ avol[m3].mapped? ∧ is-encoded-pad(orphans, m4, avol[m3].data) ∧ avol[m2].mapped? ∧ (logoff ≠ LEB_SIZE → # avol[m2].data = logoff) ∧ is-encoded(log, avol[m2].data) ∧ mapped-full?(avol, m5, lptlebs(# lpt0, LEB_SIZE)) ∧ is-encoded(lpt0, lebs(avol, m5, lptlebs(# lpt0, LEB_SIZE)))))