| # lpt1 = # avol, # lpt0 = # avol, # buf0 = gndx0.flashsize, # gndx0 = # lax0, (elems nx ∪ dom gstore0) ++ n = dom gstore ∪ ginval, lpt1[n] = mklp(m, # buf1, LP_GROUP_NODES, m3), gstore[n] = groupblock(gndx1, lax1, m), avol[n] = mapped(buf1), keyset(gch) = gc-heap(lpt1, nx + n '), pstate = journal(n), remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, ginval ∩ elems nx = ∅, ginval < # avol, n < # avol, abs-gstore(avol, lpt1, gstore, ginval), abs-istore(avol, lpt1, istore2), abs-nodes(buf0, # buf1, gndx0, lax0, false), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only(buffered(n), nx + n ', lpt1), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt1, freelist), inv(groupblock(gndx1, lax1, m)), inv(istore1), inv(istore2), inv(gstore0), inv(gstore \ ginval), log-group-block(nx + n ', lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, nx + n '), n ∈ gstore, # buf1 + gndx0.flashsize ≤ LEB_SIZE, istore1 ⊑ istore2, ⌊err1⌋ , isbuf1 → synced(avol), ∀ n0. n0 = 0 ∨ ¬ n0 < gndx0.flashsize ∨ ¬ is-aligned(# buf1 + n0, EB_PAGE_SIZE) ⊦ ∃ lax, err. (⌊err⌋ ∨ err = ESUCCESS) ∧ ¬ dups(lax1 + lax) ∧ # lax ≤ # lax0 ∧ inv-flashsize(prefixn(# lax, gndx0), lax) ∧ (err = ESUCCESS ↔ # lax = # lax0) ∧ ⟨ax := lax.to-adr(pstate.lnum), err0 := err; gstore[pstate.lnum].gndlist := gstore[pstate.lnum].gndlist + prefixn(# lax, gndx0); gstore[pstate.lnum].ladrlist := gstore[pstate.lnum].ladrlist + lax; if err0 ≠ ESUCCESS then ax := ?, pstate := readonly; isbuf1 := ?⟩ ( abs-gstore(avol, lpt1[n, mklp(m, LEB_SIZE, LP_GROUP_NODES, m3)], gstore, ginval) ∧ (isbuf1 → synced(avol)) ∧ pstate = readonly ∧ lax0.to-adr(n) = ax ∧ err1 = err0), gndx0 = [], dups(nx), n ∈ nx, n ∈ ginval |
# gndx0 = # lax0, # buf0 = gndx0.flashsize, # lpt0 = # avol, # lpt1 = # avol, (elems nx ∪ dom gstore0) ++ n = dom gstore ∪ ginval, avol[n] = mapped(buf1), gstore[n] = groupblock(gndx1, lax1, m), lpt1[n] = mklp(m, # buf1, LP_GROUP_NODES, m3), keyset(gch) = gc-heap(lpt1, nx + n '), pstate = journal(n), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, ginval ∩ elems nx = ∅, gndx0 ≠ [], n < # avol, ginval < # avol, abs-gstore(avol, lpt1, gstore, ginval), abs-istore(avol, lpt1, istore2), abs-nodes(buf0, # buf1, gndx0, lax0, false), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only(buffered(n), nx + n ', lpt1), flash-lpt-cons(lpt0, istore1, gstore0), freelist-cons(lpt1, freelist), inv(gstore \ ginval), inv(gstore0), inv(istore2), inv(istore1), inv(groupblock(gndx1, lax1, m)), log-group-block(nx + n ', lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, nx + n '), n ∈ gstore, # buf1 + gndx0.flashsize ≤ LEB_SIZE, istore1 ⊑ istore2, ⌊err1⌋ , ¬ dups(nx), ¬ n ∈ ginval, ¬ n ∈ nx, isbuf1 → synced(avol), ∀ n0. n0 = 0 ∨ ¬ n0 < gndx0.flashsize ∨ ¬ is-aligned(# buf1 + n0, EB_PAGE_SIZE) ⊦ ∃ lax, err. (⌊err⌋ ∨ err = ESUCCESS) ∧ ¬ dups(lax1 + lax) ∧ # lax ≤ # lax0 ∧ inv-flashsize(prefixn(# lax, gndx0), lax) ∧ (err = ESUCCESS ↔ # lax = # lax0) ∧ ⟨ax := lax.to-adr(pstate.lnum), err0 := err; gstore[pstate.lnum].gndlist := gstore[pstate.lnum].gndlist + prefixn(# lax, gndx0); gstore[pstate.lnum].ladrlist := gstore[pstate.lnum].ladrlist + lax; if err0 ≠ ESUCCESS then ax := ?, pstate := readonly; isbuf1 := ?⟩ ( abs-gstore(avol, lpt1[n, mklp(m, LEB_SIZE, LP_GROUP_NODES, m3)], gstore, ginval) ∧ (isbuf1 → synced(avol)) ∧ pstate = readonly ∧ lax0.to-adr(n) = ax ∧ err1 = err0)