| # lpt1 = # avol, # lpt0 = # avol, lpt1[m] = mklp(m1, m2, LP_GROUP_NODES, m3), gstore[m] = groupblock(gndx, lax, m1), bh1 = gch, keyset(gch) = gc-heap(lpt1, log0), lpt = lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], remove-refsize0(gstore0) = gstore0, remove-refsize0(istore0) = istore0, elems log0 ∩ ginval = ∅, dom gstore0 ∪ elems log0 = dom gstore ∪ ginval, # gc-heap(lpt1, log0) ≠ 0, gc-heap(lpt1, log0) ≠ ∅, m < # avol, ginval < # avol, abs-gstore(avol, lpt1, gstore, ginval), abs-istore(avol, lpt1, istore), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(pstate = readonly, bleb, lpt1, avol), bufs-log-only(bleb, log0, lpt1), flash-lpt-cons(lpt0, istore0, gstore0), freelist-cons(lpt1, freelist), inv(gstore \ ginval), inv(gstore0), inv(istore), inv(istore0), log-group-block(log0, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log0), m ∈ gstore0, m ∈ gstore, key-index(m1, m) ∈ gc-heap(lpt1, log0), istore0 ⊑ istore, ¬ dups(log0), ¬ m ∈ log0, isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), pstate.journal? → log0 ≠ [] ∧ pstate.lnum = log0.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore, pstate = unbuffered → isbuf ⊦ [gc_heap_update#(lpt[m].gcheapidx, n; gch, lpt)] ( bin-heap-inv(gch, lpt) ∧ id-idx(lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], lpt) ∧ keyset(gch) = (keyset(bh1) -- key-index(m1, m)) ++ key-index(n, m) → ⟨apersistence_set_gblock_refsize#(m, n, adr0, istore, istore0, ginval, gstore0, log0, m0, ns0, pstate, isbuf; gstore)⟩ ( abs-gstore(avol, lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], gstore, ginval) ∧ ginval < # lpt ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)))) |
# lpt0 = # avol, # lpt1 = # avol, gstore[m] = groupblock(gndx, lax, m1), lpt1[m] = mklp(m1, m2, LP_GROUP_NODES, m3), bh1 = gch, keyset(gch) = gc-heap(lpt1, log0), lpt = lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], remove-refsize0(istore0) = istore0, remove-refsize0(gstore0) = gstore0, elems log0 ∩ ginval = ∅, dom gstore0 ∪ elems log0 = dom gstore ∪ ginval, ginval < # avol, m < # avol, abs-gstore(avol, lpt1, gstore, ginval), abs-istore(avol, lpt1, istore), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(pstate = readonly, bleb, lpt1, avol), bufs-log-only(bleb, log0, lpt1), flash-lpt-cons(lpt0, istore0, gstore0), freelist-cons(lpt1, freelist), inv(istore0), inv(istore), inv(gstore0), inv(gstore \ ginval), log-group-block(log0, lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, log0), key-index(m1, m) ∈ gc-heap(lpt1, log0), m ∈ gstore, m ∈ gstore0, istore0 ⊑ istore, pstate = unbuffered → isbuf, pstate.index? → pstate.lnum ∈ istore, pstate.journal? → log0 ≠ [] ∧ pstate.lnum = log0.last ∧ pstate.lnum ∈ gstore, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, isbuf → synced(avol) ⊦ ∀ gch, lpt. bin-heap-inv(gch, lpt) ∧ id-idx(lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], lpt) ∧ keyset(gch) = (keyset(bh1) -- key-index(m1, m)) ++ key-index(n, m) → ⟨apersistence_set_gblock_refsize#(m, n, adr0, istore, istore0, ginval, gstore0, log0, m0, ns0, pstate, isbuf; gstore)⟩ ( abs-gstore(avol, lpt1[m, mklp(n, m2, LP_GROUP_NODES, m3)], gstore, ginval) ∧ ginval < # lpt ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))), # gc-heap(lpt1, log0) = 0, gc-heap(lpt1, log0) = ∅, dups(log0), m ∈ log0