| # lpt2 = # avol0, # lpt0 = # avol0, isbuf ↔ false, lpt2[n0] = mklp(0, m3, LP_FREE, m2), avol = avol0[n0, mapped(mkbuf(0))], keyset(gch) = gc-heap(lpt2, log0), log = log0, lpt = lpt0, m0 = 0, m1 = n0, n0 < # avol0, awbuf-inv(avol0[n0, mapped(mkbuf(0))], bleb), awbuf-inv(avol0, bleb), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb, lpt2, avol0), bufs-log-only(bleb, log0, lpt2), freelist-cons(lpt2, n0 ' + nx0), log-group-block(log0, lpt2), lpt-free-unref(lpt0), lpt-free-unref(lpt2), lpt-leb-size(lpt0), lpt-leb-size(lpt2), lpt-ram-flash(lpt2, lpt0, log0), synced(avol0), bleb ≠ buffered(m1) → (bleb ≠ nobuffer → avol[bleb.leb].mapped? ∧ bleb.leb < # avol ∧ bleb.isbuf?) ∧ ( bleb = nobuffer ∨ is-aligned(# avol[bleb.leb].data, EB_PAGE_SIZE) → m1 < # avol → m1 < # avol ∧ (avol[m1].mapped? → avol[m1].mapped? ∧ m1 < # avol)), bleb = nobuffer ∨ is-aligned(# avol0[n0, mapped(mkbuf(0))][bleb.leb].data, EB_PAGE_SIZE) ⊦ [abort] ( awbuf-inv(avol0[n0, mapped(mkbuf(0))], bleb) → ⟪lpt1 := lpt2[n0, lpt2[n0, mklp(lpt2[n0].ref-size, 0, lpt2[n0].flags, lpt2[n0].gcheapidx)][n0].ref-size:= 0]; freelist := (n0 ' + nx0).tail; if err ≠ ESUCCESS then freelist := n0 ' + freelist else lpt1[n0].flags := LP_INDEX_NODES⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(bleb, log0, lpt1) ∧ # lpt1 = # avol0 ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(false, bleb, lpt1, avol0[n0, mapped(mkbuf(0))]) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0))), bleb = buffered(m1), buffered(n0) = bleb, (bleb = nobuffer ∨ is-aligned(# avol[bleb.leb].data, EB_PAGE_SIZE)) ∧ m1 < # avol ∧ avol[m1].mapped? ∧ m0 = # avol[m1].data |