| # lpt2 = # avol, # lpt0 = # avol, keyset(gch) = gc-heap(lpt2, log1), lpt3 = lpt2, awbuf-inv(avol, nobuffer), awbuf-inv(avol, bleb0), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb0, lpt2, avol), bufs-log-only(bleb0, log1, lpt2), freelist-cons(lpt2, freelist), log-group-block(log1, lpt2), lpt-free-unref(lpt2), lpt-free-unref(lpt0), lpt-leb-size(lpt2), lpt-leb-size(lpt0), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), ∀ n. n ∈ log1 → n < # avol ∧ lpt2[n].flags = LP_GROUP_NODES ⊦ ∀ log1, lpt2, gch. log1 = [] ∧ bin-heap-inv(gch, lpt2) ∧ keyset(gch) = gc-heap(lpt3, []) ∧ id-idx(lpt3, lpt2) → ⟪persistence_cleanup_lpt#(adr0, m0, [], lpt3, ns0, nobuffer, false; lpt2, freelist, gch, avol)⟫ ( lpt-free-unref(lpt2) ∧ lpt-free-unref(lpt3) ∧ freelist-cons(lpt2, freelist) ∧ bin-heap-inv(gch, lpt2) ∧ keyset(gch) = gc-heap(lpt2, []) ∧ # lpt2 = # avol ∧ lpt-leb-size(lpt2) ∧ lpt-leb-size(lpt3) ∧ lpt-ram-flash(lpt2, lpt3, []) ∧ awbuf-inv(avol, nobuffer) ∧ # lpt3 = # avol), dups(log1) |
# lpt0 = # avol, # lpt2 = # avol, keyset(gch0) = gc-heap(lpt2, []), keyset(gch) = gc-heap(lpt2, log1), awbuf-inv(avol, bleb0), awbuf-inv(avol, nobuffer), bin-heap-inv(gch0, lpt), bin-heap-inv(gch, lpt2), buf-ro-rw-mode(false, bleb0, lpt2, avol), bufs-log-only(bleb0, log1, lpt2), freelist-cons(lpt2, freelist), id-idx(lpt2, lpt), log-group-block(log1, lpt2), lpt-free-unref(lpt0), lpt-free-unref(lpt2), lpt-leb-size(lpt0), lpt-leb-size(lpt2), lpt-ram-flash(lpt2, lpt0, log1), synced(avol), ¬ dups(log1), ∀ n. n ∈ log1 → n < # avol ∧ lpt2[n].flags = LP_GROUP_NODES ⊦ ⟪persistence_cleanup_lpt#(adr0, m0, [], lpt2, ns0, nobuffer, false; lpt, freelist, gch0, avol)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch0, lpt) ∧ keyset(gch0) = gc-heap(lpt, []) ∧ # lpt = # avol ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt2, []) ∧ awbuf-inv(avol, nobuffer) ∧ # lpt2 = # avol)