Prove each publication from the published parent's proof on collected stores
H(d): incremental publication proofs on collected stores
Collected stores (every local/durable deployment) re-walked a generation's full object closure on every commit, so the harness's per-turn proof cost grew linearly with the volume's history (ProofContext::prove was ~95% of per-turn growth). The incremental proof already existed for uncollected stores. This makes it sound for collected ones, structurally:
- Collection epoch.
Collection::beginbumpsEpochsunder the gate's write lock, before marking.CollectionEpochcan only be made byCollectionEpoch::read; a proof reads it before its first object read. - Typed ticket. A new proof is
Unpublished<CachedProof>(#[must_use]). It becomes reusable only throughpublish(&AppendOutcome)withCommitted/AlreadyCommitted; a failed or conflicted append drops it. There is no API to install an unpublished proof outside loom tests. - Reuse is (epoch, generation) exact.
ProofSlot::currentreads the store's epoch itself and returns the published proof only when it equals the proof's epoch;prove_cachedadditionally requires the new root's parents to be exactly that generation (plus same limits, volume, root file, features). - Admit still sees the live set. The incremental
PublicationScope::Closurelists only objects the parent proof did not list. Those parent objects were admitted to (or marked by) any collection in the same epoch — inductively for earlier reuse — and a new collection invalidates the cache by construction. The get→admit window stays covered by held checkout bases.
Verification
- Loom (
kernel::closure::published::loom_tests, realProofSlot/Unpublished/Epochs+ gate, modelled admit/mark/sweep): commit vs collect, commit vs collect that retires the volume, failed append vs collect; after every interleaving the reusable proof claims exactly the full-walk closure and every claimed object is present. Negative controls: reuse across an epoch, and caching an unpublished generation, both fail the model. 9/9 in 0.56 s atcc585c136, including durable-sequence and cross-epoch retry/delayed-publication interleavings, exact-tie Arc retention, and four negative controls (including unconditional and sequence-only installation). Model build: 9m07s. - Proptest vs the full-walk oracle (
tests/workspace/proof_cache.rs, 48 cases + deterministic): random write/remove transactions over a settled tree, random failed appends; every proof's root/generation/file count/bytes equalprove_generation_closure, listed ⊆ full, reused proof ∪ parent ⊇ full, published listings' union == full walks' union; incremental only after a published parent. - Exact flat pin (
next_proof_work_is_independent_of_prior_turns): proving the next commit after 8 vs 24 turns has==allocations, bytes andWorkCounters; negative control (no published parent, i.e. the old full walk) must grow. (A whole-commit pin is not exact on the memory backend because its persistentOrdMapinsert path depends on store size and key placement, not on proof work.) - Focused native verification at
cc585c136: 3 denied-slot allocation tests (0.01 s), 6 publication properties/negative controls (0.01 s), and 3 full-walk differential/exact proof-cost tests (1.99 s), all passed. The filesystem Windows GNU lib/tests cross-check passed in 1m12s. Native build: 7m21s. Rustfmt and diff checks passed.
Per-turn harness cost (K prior turns, next turn, sample 0)
Scratch profile (not committed): LocalHarness with scripted text turns, acyclic_test_support::measure around one run_headless turn after K turns. Paired command: PROFILE_K=$k PROFILE_S=3 cargo test -p acyclic-harness --lib --features filesystem-local,native-execution,test-support,grpc per_turn_cost_after_k_turns -- --nocapture, baseline = dfe339a21 with the same scratch file.
| OS | K | before allocs / bytes | after allocs / bytes |
|---|---|---|---|
| Linux bb1 | 4 | 128,097 / 50.6 MB | 106,942 / 32.9 MB |
| Linux bb1 | 8 | 151,469 / 68.9 MB | 108,057 / 33.5 MB |
| Linux bb1 | 16 | 198,836 / 105.9 MB | 111,525 / 35.3 MB |
| Linux bb1 | 32 | 291,016 / 179.6 MB | 115,783 / 36.7 MB |
| Windows local | 4 | 128,252 / 50.7 MB | 106,638 / 32.8 MB |
| Windows local | 8 | 151,297 / 68.8 MB | 108,004 / 33.6 MB |
| Windows local | 16 | 198,839 / 106.5 MB | 111,817 / 35.5 MB |
| Windows local | 32 | 291,482 / 180.0 MB | 115,472 / 36.7 MB |
| macOS ivar | 4 | 130,402 / 50,827,917 B | 86,773 / 28,233,519 B |
| macOS ivar | 8 | 153,453 / 69,056,916 B | 88,044 / 28,703,160 B |
| macOS ivar | 16 | 200,979 / 106,059,444 B | 91,951 / 30,177,245 B |
| macOS ivar | 24 | 247,328 / 145,610,785 B | 93,418 / 31,010,191 B |
| macOS ivar | 32 | 293,408 / 180,048,317 B | 95,891 / 32,022,376 B |
Slope per prior turn: ~5,820 allocations and 4.6 MB before → ~316 allocations and 138 KB after (bb1 and Windows agree). The remaining ~316/turn is outside the proof (harness checkout/transaction path resolution, generation mutation and content publication over growing directories/journals); that is the next H(d) site from the same profile, in a follow-up.
Decisions
- Reserve proof-slot custody before constructing its first Arc, so denied admission cannot allocate.
- Route all successful append outcomes through one slot-locked install that compares durable sequence, then collection epoch. Equal-sequence retries refresh invalidated proofs only with a newer epoch; older sequences or epochs cannot regress the slot, and exact ties retain the existing Arc.
- macOS uses a focused integration profile of the same production LocalHarness turn to keep the target at 6.1 GiB. Both independent implementations use the same fixture; it adds three erased future allocations per turn and initializes native services outside measurement. Its figures should be compared as a pair within that OS. The paired command and elapsed times are in the review response.