Proof step 90 from proof inv-recover (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  m8 + # lpt0 = # avol1, avol1[0] = mapped(buf), avol1[m5] = mapped(buf0), avol1[m10] = mapped(buf1), m10 < # avol2, 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 = ESUCCESS → orphans = orphans0, m3 ≠ LEB_SIZE → # buf1 = m3, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪if err ≠ ESUCCESS then debug#("persistence-io: reading orphans failed"); m0 := LEB_SIZE; sb := mksb(adr0, m9, m10, m5, m6, m7, m8); if err = ESUCCESS then {m := # avol2 - sb.main; let buf = ? in {persistence_io_read_lebs#(sb.lpt, 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 := sb.indexaddr; m2 := sb.maxino}⟫ ( ( err = ESUCCESS → (∃ lpt1, log1, orphans1. disk-layout(sb, # lpt1) ∧ sb.main + # lpt1 = # avol1 ∧ is-encoded(sb, buf) ∧ avol2[sb.orph].mapped? ∧ is-encoded-pad(orphans1, sb.orphsize, avol2[sb.orph].data) ∧ avol2[sb.log].mapped? ∧ (logoff ≠ LEB_SIZE → # avol2[sb.log].data = logoff) ∧ is-encoded(log1, avol2[sb.log].data) ∧ mapped-full?(avol2, sb.lpt, lptlebs(# lpt1, LEB_SIZE)) ∧ is-encoded(lpt1, lebs(avol2, sb.lpt, lptlebs(# lpt1, LEB_SIZE)))) ∧ m0 = LEB_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → 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)) ∧ orphans0 = orphans))

Rule argument

Additional information