| # lpt4 = # avol0, # lpt1 = # avol0, keyset(gch1) = gc-heap(lpt1, log3), remove-refsize0(gstore2) = gstore2, remove-refsize0(istore2) = istore2, str0 = "persistence: wbuf recover failed", elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(gstore1 \ ns3), inv(gstore2), inv(istore1), inv(istore2), log-group-block(log3, lpt1), lpt-free-unref(lpt4), lpt-free-unref(lpt1), lpt-leb-size(lpt4), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol1 ↓ avol0, istore2 ⊑ istore1, ⌊err0⌋ , pstate0 = unbuffered → bleb1 = nobuffer, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0.index? → pstate0.lnum ∈ istore1, pstate0 = unbuffered → isbuf0 ⊦ ∀ . true → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns1, pstate, isbuf. ⟨apersistence_recover# (; adr4, m5, log6, ns6, adr5, log8, maxino0, ns7, istore3, istore4, ginval0, gstore3, gstore4; pstate1, isbuf3, err1)⟩ ( adr = adr5 ∧ istore = istore3 ∧ istore0 = istore4 ∧ ns = ginval0 ∧ gstore = gstore3 ∧ gstore0 = gstore4 ∧ log = log8 ∧ m = maxino0 ∧ ns1 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ err0 = err1)), dups(log3) |
# lpt1 = # avol0, # lpt4 = # avol0, keyset(gch1) = gc-heap(lpt1, log3), remove-refsize0(istore2) = istore2, remove-refsize0(gstore2) = gstore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(istore2), inv(istore1), inv(gstore2), inv(gstore1 \ ns3), log-group-block(log3, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt4), lpt-leb-size(lpt1), lpt-leb-size(lpt4), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol1 ↓ avol0, istore2 ⊑ istore1, ⌊err0⌋ , ¬ dups(log3), pstate0 = unbuffered → isbuf0, pstate0.index? → pstate0.lnum ∈ istore1, pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0 = unbuffered → bleb1 = nobuffer ⊦ ⟨apersistence_recover#(; adr4, m5, log6, ns6, adr5, log8, maxino0, ns7, istore3, istore4, ginval0, gstore3, gstore4; pstate1, isbuf3, err1)⟩ ( adr = adr5 ∧ istore0 = istore3 ∧ istore = istore4 ∧ ns1 = ginval0 ∧ gstore0 = gstore3 ∧ gstore = gstore4 ∧ log = log8 ∧ m = maxino0 ∧ ns = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ err0 = err1)