| # lpt0 = # avol, # lpt2 = # avol, gstore[n] = groupblock(gndx, lax, m3), lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), bh1 = gch, keyset(gch) = gc-heap(lpt2, log1), lpt1 = lpt2[n, mklp(0, 0, LP_FREE, m2)], remove-refsize0(istore0) = istore0, 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, istore), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb, lpt2, avol), bufs-log-only(bleb, log1, lpt2), flash-lpt-cons(lpt0, istore0, gstore0), freelist-cons(lpt2, freelist), inv(istore0), inv(istore), 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, istore0 ⊑ istore, pstate.index? → pstate.lnum ∈ istore, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate = unbuffered → bleb = nobuffer, pstate ≠ unbuffered → bleb = buffered(pstate.lnum) ⊦ ∀ gch, lpt1. bin-heap-inv(gch, lpt1) ∧ id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt1) ∧ keyset(gch) = keyset(bh1) -- key-index(m3, n) → ⟪err := ESUCCESS⟫ ⟨apersistence_deallocate_gnd#(n, adr0, istore, istore0, gstore0, log1, m, ns0, pstate, true; ginval, gstore; err0)⟩ ( abs-gstore(avol[n, unmapped], lpt2[n, mklp(0, 0, LP_FREE, m2)], gstore, ginval) ∧ ginval < # lpt1 ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered → bleb = buffered(pstate.lnum)) ∧ err = err0), # gc-heap(lpt2, log1) = 0, buffered(n) = bleb, gc-heap(lpt2, log1) = ∅, pstate = readonly, dups(log1), n ∈ log1 |
# lpt2 = # avol, # lpt0 = # avol, lpt2[n] = mklp(m3, m1, LP_GROUP_NODES, m2), gstore[n] = groupblock(gndx, lax, m3), keyset(gch0) = gc-heap(lpt2, log1) -- key-index(m3, n), keyset(gch) = gc-heap(lpt2, log1), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore0) = istore0, elems log1 ∩ ginval = ∅, dom gstore0 ∪ elems log1 = dom gstore ∪ ginval, # gc-heap(lpt2, log1) ≠ 0, buffered(n) ≠ bleb, gc-heap(lpt2, log1) ≠ ∅, pstate ≠ readonly, n < # avol, ginval < # avol, abs-gstore(avol, lpt2, gstore, ginval), abs-istore(avol, lpt2, istore), 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, istore0, gstore0), freelist-cons(lpt2, freelist), id-idx(lpt2[n, mklp(0, 0, LP_FREE, m2)], lpt), inv(gstore \ ginval), inv(gstore0), inv(istore), inv(istore0), 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), istore0 ⊑ istore, ¬ dups(log1), ¬ n ∈ log1, pstate ≠ unbuffered → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore ⊦ ⟪err := ESUCCESS⟫ ⟨apersistence_deallocate_gnd#(n, adr0, istore, istore0, gstore0, log1, m, ns0, pstate, true; ginval, gstore; err0)⟩ ( 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)) ∧ err = err0)