Prove each publication from the published parent's proof on collected stores

Merged
VA
1d ago
+1076-57

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::begin bumps Epochs under the gate's write lock, before marking. CollectionEpoch can only be made by CollectionEpoch::read; a proof reads it before its first object read.
  • Typed ticket. A new proof is Unpublished<CachedProof> (#[must_use]). It becomes reusable only through publish(&AppendOutcome) with Committed/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::current reads the store's epoch itself and returns the published proof only when it equals the proof's epoch; prove_cached additionally 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::Closure lists 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, real ProofSlot/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 at cc585c136, 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 equal prove_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 and WorkCounters; 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 persistent OrdMap insert 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.

OSKbefore allocs / bytesafter allocs / bytes
Linux bb14128,097 / 50.6 MB106,942 / 32.9 MB
Linux bb18151,469 / 68.9 MB108,057 / 33.5 MB
Linux bb116198,836 / 105.9 MB111,525 / 35.3 MB
Linux bb132291,016 / 179.6 MB115,783 / 36.7 MB
Windows local4128,252 / 50.7 MB106,638 / 32.8 MB
Windows local8151,297 / 68.8 MB108,004 / 33.6 MB
Windows local16198,839 / 106.5 MB111,817 / 35.5 MB
Windows local32291,482 / 180.0 MB115,472 / 36.7 MB
macOS ivar4130,402 / 50,827,917 B86,773 / 28,233,519 B
macOS ivar8153,453 / 69,056,916 B88,044 / 28,703,160 B
macOS ivar16200,979 / 106,059,444 B91,951 / 30,177,245 B
macOS ivar24247,328 / 145,610,785 B93,418 / 31,010,191 B
macOS ivar32293,408 / 180,048,317 B95,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.