test(network): prove block-sync retained-memory accounting

[p0mvn]

Motivation

PR #217 makes block-sync retained-memory accounting exact. Its coverage bounds sampled trace peaks and asserts a final retained total of zero. Both are useful, but neither states the accounting laws:

• the wire-budget final value comes from a sampled trace and permits one request of slack;
• ByteBudget::audit() is one-sided (actual >= expected), so excess charges pass;
• the plateau tests allow a max_body_bytes × 128 arrival margin — a hand-chosen heuristic, unlike the sibling window_slack term, which is derived from MIN_BS_CHECKPOINT_SUBMITTED_BLOCK_APPLIES;
• final_retained_memory_bytes == 0 is exact and valuable, but end-state only.

Together these infer correct accounting from the absence of a visible plateau breach. A charge that is transferred incorrectly, released twice, or briefly stranded can still pass every one of them.

Solution

Three layers that state the laws directly. All test-only; no production logic changes.

Tracker property tests (retained_memory.rs). A contender spinning try_charge at a saturated limit witnesses any headroom the tracker publishes — every byte it wins is headroom that really existed, so "growth exposed nothing" is provable rather than sampled. Also pins racing resizes applying growth exactly once, clones sharing one charge, and all-or-none reservations never oversubscribing.

Accounting probe (accounting_probe.rs, new). Reads the live ledgers via the same RoutineWiring handles the production path threads to each peer routine. It owns its handles, so it outlives teardown — the state in which a zero-slack assertion is meaningful. The fuzz harness now asserts every ledger drains to exactly zero, with no slack. It supersedes retained_memory_probe, which is removed.

Model-based transition test (work_queue_model.rs, new). Generated operation sequences over WorkQueue + RetainedBodyMemoryTracker, asserting conservation after every operation, including the unmatched-body claim path and its RAII rollback.

The model exists because teardown assertions are structurally blind to a transient leak: a reservation stranded by reset_above is swept by a later advance_floor, so the end state is clean. The model fails at the transition that stranded it — see Testing.

The model tracks accounting, not scheduling. Which heights take_in_range_budgeted selects is driven from the call's own result rather than re-derived; its contiguity and byte-cap rules already have unit tests, and reimplementing them in the model would only test the copy.

Testing

• cargo test -p zakura-network --lib block_sync — 260 passed
• cargo test -p zakura-network --lib blocksync_fuzz — 21 passed
• cargo clippy -p zakura-network --all-targets — 0 warnings
• cargo clippy -p zakura-network --lib --all-features — 0 warnings (see the bench commit)
• cargo fmt --all -- --check

Every assertion was validated by mutation testing rather than trusted because it was green. Each mutation is caught, each by a different assertion:

Mutation	Caught by
reconcile_exact as release-then-recharge	contender at the limit
reset_above strands a memory reservation	reservations vs model
claim_received strands a memory reservation	reservations vs model
reconcile_exact ignores the exact size	conservation law
mark_issued over-counts reserved bytes	maintained-vs-scanned drift
uncommitted claim never rolls back	claim grant vs model

The reset_above case is the load-bearing one: it passes the zero-slack teardown assertion, because advance_floor sweeps the stranded reservation before teardown. The model catches it at step 2 and shrinks to a 3-step counterexample. End-state and per-transition assertions cover genuinely different classes of leak.

Two tests were discarded or rewritten because mutation showed they passed under the exact bug they targeted:

• an identity check using Arc pointer equality was ABA-unsafe (the allocator reuses the freed address, so release-then-recharge passed) — deleted, since the contender covers it soundly;
• the conservation law initially read live_bodies back out of the implementation under test, making it circular — the model now tracks the expected size independently.

No accounting bugs were found in #217. Every mutation above is artificial. The accounting held under all of them, which is the intended result: this PR converts "we believe it is correct" into "these properties are proven".

Derived the retained-memory bound. The plateau tests used a hand-chosen max_body × 128 arrival margin. Deriving it from the admission gate instead:

peak_retained <= L                                  # tracker limit, enforced atomically
              +  MIN_BS_CHECKPOINT_SUBMITTED_BLOCK_APPLIES × max_body   # commit-window exemption
              +  max_inflight_bodies × max_body                          # reconciliation growth

L is max_reorder_lookahead_bytes. Above-window requests reserve against it with an atomic try_reserve_many, so the gated lane alone can never exceed it. Exactly two paths charge without consulting the limit: commit-window bodies (exempt, no reservation at issue, charge unconditionally at receipt) and reconciliation growth (an above-window reservation resizes from estimate to exact retained size without re-consulting the limit).

The old margin turns out to be the second term: Σ peers(max_inflight_requests) × max_blocks_per_response = 2 × 64 × 1 = exactly 128 for the single-block scenarios. The derived ceiling reproduces the previous bound identically for two of the three tests, which is a good sign the derivation matches the original reasoning. For the multi-block scenario the same quantity is 2048, so its margin was 16× too small and passed only because reconciliation growth stays far below worst case.

The headline finding is what the measurement showed, not the margin. Peaks against the derived terms:

Scenario	look-ahead budget L	measured peak	commit-window term
fuzz_commit_stall	2 MiB	181.7 MB	227.8 MB
..._resident_plateau	8 MiB	227.7 MB	227.8 MB

The peak tracks the commit-window term to within 0.02% and is unrelated to L. max_reorder_lookahead_bytes is not what sizes block-sync resident memory in these scenarios — the commit-window exemption is, and it is not configurable. Nothing amplifies L here: the exempt bodies never take a reservation against it, so lowering L cannot lower the peak.

Two independent multipliers produce that 227.8 MB, and only the first is structural:

• 401 bodies co-resident, bypassing the gate (MIN_BS_CHECKPOINT_SUBMITTED_BLOCK_APPLIES).
• 16.3× decoded expansion per body — but this is an artefact of the synthetic corpus, not a property of Zcash. The corpus packs 242 transactions of ~135 B into each 32 KiB block, and attributed_memory_size_bytes charges a fixed inline_size_bytes::<Transaction>() per transaction, so tiny transactions make that overhead dominate. Measured against real mainnet vectors, where transactions are ~1.2–1.7 kB:

Block	wire	txs	bytes/tx	decoded ratio
MAINNET_1	1,617	1	1,617	2.31×
MAINNET_982681	5,244	3	1,748	2.22×
MAINNET_434873	13,935	12	1,161	3.12×
synthetic (32 KiB)	32,706	242	135	16.35×

So the plateau tests run ~5–7× pessimistic on decoded expansion. That is the safe direction for a ceiling, but the absolute MB figures in these tests should not be read as representative of mainnet.

Specifications & References

Stacked on feat/exact-block-sync-retained-memory (#217); please merge that first.

AI disclosure: authored with Claude Code.

Follow-up Work

• The commit-window exemption, not the configured cap, sizes resident memory. The bound is now derived, and the measurement above shows the exempt span dominating while L is irrelevant to it. BS_CHECKPOINT_RANGE_BYTE_FLOOR already encodes the wire half of this (401 × 2 MB = ~802 MB), so the floor is known and intentional — checkpoint ranges must be co-resident to commit. What the tests add is that it is the dominant term, and that lowering max_reorder_lookahead_bytes cannot bring resident memory below it. Sizing it with the measured real-block expansion (~2.3–3.1×) rather than the synthetic 16×, a worst-case 2 MB-block range costs roughly 401 × ~8 MB ≈ 3 GB, on top of the 1.5 GiB default L. Typical mainnet blocks (a few kB) make the same term ~20 MB and irrelevant. So the exposure is real but confined to sustained large-block stretches. Worth a design conversation for the OOM work; not a test gap.
• The fuzz corpus is not shape-representative. 242 × 135 B transactions per block, against a real ~1–12 × ~1.2 kB. Since retained memory is charged per transaction, this systematically inflates decoded expansion ~5–7×. Pessimistic (so bounds stay safe), but it means memory figures from these scenarios do not transfer to mainnet, and it is worth knowing before anyone tunes a real limit against them.
• Conservation is not boundedness. The accounting tests prove every byte is charged once, transferred correctly, and released exactly once. That is orthogonal to whether the total stays under a ceiling — conservation holds perfectly while the total climbs. The derived bound above is the first half of the boundedness story; the reconciliation-growth term is a worst case no scenario currently provokes.
• Extend the model across the sequencer stages (prepare_submit clones the charge, retain_for_driver_in_place resizes it, detach/unsubmit/resubmit move it). That is the largest remaining transient-leak surface.
• The model is single-threaded; the fuzz tests are concurrent but assert only peaks and teardown. Loom on the tracker would close the gap, though the contender tests already cover the sharpest race.
• fuzz_reorg remains ignored: a faithful mid-sync reset needs the high-fidelity Committer<MockVerifier> tier.

[v12-auditor]

Note

Complete: Audit complete. V12 did not find any issues that need review.

Open the full results here.

Analyzed 10 files, diff 256253d...fd76b89.