| # lpt2 = # avol, # lpt0 = # avol, isbuf ↔ true, lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), gstore[n] = groupblock(gndx, lax, m3), adr = adr0, istore = istore1, istore0 = istore2, keyset(gch0) = gc-heap(lpt2, log1) -- key-index(m3, n), keyset(gch) = gc-heap(lpt2, log1), log = log1, maxino = m, ns = ns0, remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore ∪ ginval, n < # avol, ginval < # avol, abs-gstore(avol, lpt2, gstore, ginval), abs-istore(avol, lpt2, istore2), awbuf-inv(avol, bleb), bin-heap-inv(gch0, lpt), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb, lpt2, avol), bufs-log-only(bleb, log1, lpt2), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt2, freelist), id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt), inv(gstore \ ginval), inv(gstore0), inv(istore2), inv(istore1), log-group-block(log1, lpt2), lpt-free-unref(lpt2), lpt-free-unref(lpt0), lpt-leb-size(lpt2), lpt-leb-size(lpt0), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), n ∈ gstore, n ∈ gstore0, key-index(m3, n) ∈ gc-heap(lpt2, log1), istore1 ⊑ istore2, pstate ≠ unbuffered → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore2 ⊦ ⟨if isbuf ∧ n ∈ gstore ∧ ¬ n ∈ log then {fail_or_success#(; ; err); if err = ESUCCESS then gstore := gstore -- n, ginval := ginval ++ n} else abort⟩ ( abs-gstore(avol[n, unmapped], lpt2[n, mklp(0, 0, LP_FREE, m2)], gstore, ginval) ∧ ginval < # lpt ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered → bleb = buffered(pstate.lnum)) ∧ ESUCCESS = err), # gc-heap(lpt2, log1) = 0, buffered(n) = bleb, gc-heap(lpt2, log1) = ∅, pstate = readonly, dups(log1), n ∈ log1 |
# lpt0 = # avol, # lpt2 = # avol, isbuf ↔ true, gstore[n] = groupblock(gndx, lax, m3), lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), adr = adr0, istore = istore1, istore0 = istore2, keyset(gch) = gc-heap(lpt2, log1), keyset(gch0) = gc-heap(lpt2, log1) -- key-index(m3, n), log = log1, maxino = m, ns = ns0, remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore ∪ ginval, ginval < # avol, n < # avol, abs-gstore(avol, lpt2, gstore, ginval), abs-istore(avol, lpt2, istore2), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt2), bin-heap-inv(gch0, lpt), buf-ro-rw-mode(false, bleb, lpt2, avol), bufs-log-only(bleb, log1, lpt2), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt2, freelist), id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt), inv(istore1), inv(istore2), inv(gstore0), inv(gstore \ ginval), log-group-block(log1, lpt2), lpt-free-unref(lpt0), lpt-free-unref(lpt2), lpt-leb-size(lpt0), lpt-leb-size(lpt2), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), key-index(m3, n) ∈ gc-heap(lpt2, log1), n ∈ gstore0, n ∈ gstore, istore1 ⊑ istore2, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate = unbuffered → bleb = nobuffer, pstate ≠ unbuffered → bleb = buffered(pstate.lnum) ⊦ ⟨fail_or_success#(; ; err); if err = ESUCCESS then gstore := gstore -- n, ginval := ginval ++ n⟩ ( abs-gstore(avol[n, unmapped], lpt2[n, mklp(0, 0, LP_FREE, m2)], gstore, ginval) ∧ ginval < # lpt ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered → bleb = buffered(pstate.lnum)) ∧ ESUCCESS = err), # gc-heap(lpt2, log1) = 0, buffered(n) = bleb, gc-heap(lpt2, log1) = ∅, pstate = readonly, dups(log1), n ∈ log1