| abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_is_log_empty#(log0; ; empty?)⟫ ⟨apersistence_is_log_empty#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; isbuf1)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ (empty? ↔ isbuf1)) |