| # lpt0 = # avol, # lpt1 = # avol, # buf0 = gndx.flashsize, # gndx = # lax, isbuf ↔ false, avol[n1] = mapped(buf1), lpt1[n1] = mklp(m4, # buf1, LP_GROUP_NODES, m2), err = err0, keyset(gch) = gc-heap(lpt1, log0), m = buffered(n1).leb, n0 = gndx.flashsize, buffered(n1).isbuf?, avol[m].mapped?, m < # avol, n1 < # avol, n < n0, abs-nodes(buf0, # buf1, gndx, lax, false), awbuf-inv(avol, buffered(n1)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n1), lpt1, avol), bufs-log-only(buffered(n1), log0, lpt1), freelist-cons(lpt1, freelist), is-aligned(# avol[m].data + n, EB_PAGE_SIZE), 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), n1 ∈ log0, 0 + n ≤ # buf0, # buf1 + gndx.flashsize ≤ LEB_SIZE, n ≠ 0 → n < n0 → avol[m].mapped? ∧ m < # avol, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [isbuf := true] ( awbuf-inv(avol[m, mapped(avol[m].data + subarray(buf0, 0, n))], buffered(n1)) ∧ # lpt0 = # avol[m, mapped(avol[m].data + subarray(buf0, 0, n))] → ⟪if err = ESUCCESS then lpt1[buffered(n1).leb] := mklp (lpt1[buffered(n1).leb].ref-size, lpt1[buffered(n1).leb].size + gndx.flashsize, lpt1[buffered(n1).leb].flags, lpt1[buffered(n1).leb].gcheapidx) else {debug#("persistence: adding group node to LEB " + buffered(n1).leb.toString + " failed"); lpt1[buffered(n1).leb] := mklp(lpt1[buffered(n1).leb].ref-size, LEB_SIZE, lpt1[buffered(n1).leb].flags, lpt1[buffered(n1).leb].gcheapidx)}⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(buffered(n1), log0, lpt1) ∧ # lpt1 = # avol[m, mapped(avol[m].data + subarray(buf0, 0, n))] ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf, buffered(n1), lpt1, avol[m, mapped(avol[m].data + subarray(buf0, 0, n))]) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0))), err = ESUCCESS, gndx = [], n = 0, dups(log0) |
# lpt0 = # avol[m, mapped(avol[m].data + subarray(buf0, 0, n))], # gndx = # lax, # buf0 = gndx.flashsize, # lpt1 = # avol, # lpt0 = # avol, isbuf ↔ false, lpt1[n1] = mklp(m4, # buf1, LP_GROUP_NODES, m2), avol[n1] = mapped(buf1), err = err0, keyset(gch) = gc-heap(lpt1, log0), m = buffered(n1).leb, n0 = gndx.flashsize, buffered(n1).isbuf?, avol[m].mapped?, n < n0, n1 < # avol, m < # avol, abs-nodes(buf0, # buf1, gndx, lax, false), awbuf-inv(avol[m, mapped(avol[m].data + subarray(buf0, 0, n))], buffered(n1)), awbuf-inv(avol, buffered(n1)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n1), lpt1, avol), bufs-log-only(buffered(n1), log0, lpt1), freelist-cons(lpt1, freelist), is-aligned(# avol[m].data + n, EB_PAGE_SIZE), 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), n1 ∈ log0, # buf1 + gndx.flashsize ≤ LEB_SIZE, 0 + n ≤ # buf0, n ≠ 0 → n < n0 → avol[m].mapped? ∧ m < # avol, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err = ESUCCESS then lpt1[buffered(n1).leb] := mklp (lpt1[buffered(n1).leb].ref-size, lpt1[buffered(n1).leb].size + gndx.flashsize, lpt1[buffered(n1).leb].flags, lpt1[buffered(n1).leb].gcheapidx) else {debug#("persistence: adding group node to LEB " + buffered(n1).leb.toString + " failed"); lpt1[buffered(n1).leb] := mklp(lpt1[buffered(n1).leb].ref-size, LEB_SIZE, lpt1[buffered(n1).leb].flags, lpt1[buffered(n1).leb].gcheapidx)}⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(buffered(n1), log0, lpt1) ∧ # lpt1 = # avol[m, mapped(avol[m].data + subarray(buf0, 0, n))] ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(true, buffered(n1), lpt1, avol[m, mapped(avol[m].data + subarray(buf0, 0, n))]) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0)), err = ESUCCESS, gndx = [], n = 0, dups(log0)