| adr0 = adr1, m0 = m1, log0 = log1, lpt = lpt0, avol ↓ avol0, ns1 = ns2, abs-istore(avol0, lpt1, istore1), abs-gstore(avol0, lpt1, gstore1, ns3), adr2 = adr1, m2 = m1, log2 = log3, ns3 < # lpt1, ns4 = ns2, flash-lpt-cons(lpt0, istore2, gstore2), isbuf0 → synced(avol0), pstate0 = unbuffered → bleb = nobuffer, pstate0 = readonly ↔ isbuf1, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb = buffered(pstate0.lnum), synced(avol0), inv-journal(log2, gstore1, gstore2, ns3), inv-index(istore1, istore2), inv-state(pstate0, log2, gstore1, istore1, isbuf0), lpt-free-unref(lpt1), lpt-free-unref(lpt0), freelist-cons(lpt1, log4), log3 = log1, bin-heap-inv(gch, lpt1), keyset(gch) = gc-heap(lpt1, log3), bufs-log-only(bleb, log3, lpt1), # lpt1 = # avol0, ¬ dups(log3), log-group-block(log3, lpt1), buf-ro-rw-mode(isbuf1, bleb, lpt1, avol0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log3), m3 = LEB_SIZE, awbuf-inv(avol0, bleb), # lpt0 = # avol0, adr3 = adr4, m4 = m5, log5 = log6, ns5 = ns6 ⊦ ⟪persistence_recover#(; adr3, m4, log5, ns5, log7, lpt2, freelist, gch0, m6, adr0, m0, log0, avol, lpt, ns1, bleb0, isbuf2; err)⟫ ( ( err = ESUCCESS → (∃ adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf. ( adr = adr2 ∧ istore = remove-refsize0(crash(istore1, istore2)) ∧ istore0 = istore2 ∧ ginval = ns3 ∧ gstore = crash(gstore1, gstore2, ns3, log2) ∧ gstore0 = gstore2 ∧ log = log2 ∧ maxino = m2 ∧ ns = ns4) ∧ ⟨apersistence_recover#(; adr4, m5, log6, ns6, adr, log, maxino, ns, istore, istore0, ginval, gstore, gstore0; pstate, isbuf, err0)⟩ ( ( abs-istore(avol, lpt2, istore) ∧ abs-gstore(avol, lpt2, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log7 ∧ ginval < # lpt2 ∧ ns = ns1 ∧ flash-lpt-cons(lpt, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb0 = nobuffer) ∧ (pstate = readonly ↔ isbuf2) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb0 = buffered(pstate.lnum))) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns0, pstate, isbuf. ⟨apersistence_recover# (; adr4, m5, log6, ns6, adr5, log8, maxino0, ns7, istore3, istore4, ginval0, gstore3, gstore4; pstate1, isbuf3, err0)⟩ ( adr = adr5 ∧ istore = istore3 ∧ istore0 = istore4 ∧ ns = ginval0 ∧ gstore = gstore3 ∧ gstore0 = gstore4 ∧ log = log8 ∧ m = maxino0 ∧ ns0 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ err = err0)))) |