| # gndx3 = # lax0, # lpt = # avol, # lpt0 = # avol, avol[m] = mapped(buf), lpt[m] = mklp(m1, m2, LP_GROUP_NODES, m3), gstore2[m] = groupblock(gndx1, lax, m1), adr = adr0, ax = ax0, gndx = gndx0, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = istore2, keyset(gch) = gc-heap(lpt, log1), log = log1, maxino = m0, ns = ns0, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems log1 ∩ ginval = ∅, dom gstore1 ∪ elems log1 = dom gstore2 ∪ ginval, ginval < # avol, m < # avol, abs-istore(avol, lpt, istore2), abs-leb(mapped(buf), groupblock(gndx1, lax, m1), mklp(m1, m2, LP_GROUP_NODES, m3)), abs-nodes(buf, gndx3, lax0, true), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt), buf-ro-rw-mode(pstate = readonly, bleb, lpt, avol), bufs-log-only(bleb, log1, lpt), flash-lpt-cons(lpt0, istore1, gstore1), freelist-cons(lpt, freelist), inv(gstore2 \ ginval), inv(gstore1), inv(istore2), inv(istore1), inv(groupblock(gndx1, lax, m1)), log-group-block(log1, lpt), lpt-free-unref(lpt), lpt-free-unref(lpt0), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log1), m ∈ gstore2, istore1 ⊑ istore2, err1 = ESUCCESS → ax1 = ax0 + lax0.to-adr(m) ∧ gndx2 = gndx0 + gndx3, isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore2, pstate.index? → pstate.lnum ∈ istore2, pstate = unbuffered → isbuf, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ⟨fail_or_success#(; ; err); if err = ESUCCESS then ax := ax + gstore0[m].ladrlist.to-adr(m), gndx := gndx + gstore0[m].gndlist else ax := ?, gndx := ?⟩ ( (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ ax1 = ax ∧ gndx2 = gndx ∧ err1 = err), dups(log1), m ∈ ginval |
# lpt0 = # avol, # lpt = # avol, # gndx3 = # lax0, gstore2[m] = groupblock(gndx1, lax, m1), lpt[m] = mklp(m1, m2, LP_GROUP_NODES, m3), avol[m] = mapped(buf), keyset(gch) = gc-heap(lpt, log1), remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems log1 ∩ ginval = ∅, dom gstore1 ∪ elems log1 = dom gstore2 ∪ ginval, m < # avol, ginval < # avol, abs-istore(avol, lpt, istore2), abs-leb(mapped(buf), groupblock(gndx1, lax, m1), mklp(m1, m2, LP_GROUP_NODES, m3)), abs-nodes(buf, gndx3, lax0, true), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt), buf-ro-rw-mode(pstate = readonly, bleb, lpt, avol), bufs-log-only(bleb, log1, lpt), flash-lpt-cons(lpt0, istore1, gstore1), freelist-cons(lpt, freelist), inv(groupblock(gndx1, lax, m1)), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval), log-group-block(log1, lpt), lpt-free-unref(lpt0), lpt-free-unref(lpt), lpt-leb-size(lpt0), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log1), m ∈ gstore2, istore1 ⊑ istore2, ¬ dups(log1), ¬ m ∈ ginval, pstate = unbuffered → isbuf, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → log1 ≠ [] ∧ pstate.lnum = log1.last ∧ pstate.lnum ∈ gstore2, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, isbuf → synced(avol), err1 = ESUCCESS → ax1 = ax0 + lax0.to-adr(m) ∧ gndx2 = gndx0 + gndx3, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ⟨fail_or_success#(; ; err); if err = ESUCCESS then ax0 := ax0 + gstore2[m].ladrlist.to-adr(m), gndx0 := gndx0 + gstore2[m].gndlist else ax0 := ?, gndx0 := ?⟩ ( (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ ax1 = ax0 ∧ gndx2 = gndx0 ∧ err1 = err)