Bound materialization_store_local: per-family ExactLimit budgets, windowed occupancy index, self-clean on open

[gunbai-bot]

PR C1 of the cross-run materialization sequence (royal-moth-86 rulings, 2026-10-03). It makes extdeps.realization.materialization_store_local bounded and self-cleaning for any request family. The typed-module consumer is C2, which waits on gunbc#13078 (PR B, emitter) and on reconciling typed_module_key with std.computation_identity (#13043). It follows #13064 (PR A), which deleted the two unbounded stores. Operator requirement: an earlier on-disk cache with no ceiling or cleanup filled the CI runners' disks, so any cross-run store must bound its own disk use.

The bound inhabits existing homes; no new cache vocabulary

• Budget per family, host ceiling = declared sum (ruling (b)). Each family's store is constructed by std.artifact_store store_over_provider from its own CacheProvider row: CapacityBounded { ByteCapacity { ExactLimit }, ReplaceExisting { LeastRecentlyUsed } } (ruling 1a). Unbounded or unobserved rows refuse at construction. An artifact over its family's budget refuses (StoreCommitDidNotFit) before any eviction. One family never evicts another's entries. An undeclared family refuses (StoreCommitBudgetUndeclared).
• Typed-module budget: 4 GiB, named as POLICY (local_store_typed_module_budget_policy). Its revision trigger is C2 measuring real per-module entries. local_store_host_ceiling_bytes is the one host-wide figure. The catalog row's retention is now CapacityBounded at that ceiling (it was CapacityUnobserved), so retention_growth_is_bounded holds.
• One root per host is structural. DurableHostVolumeRoot is a nullary arm naming /var/lib/gunbc/materialization-store. Only WitnessScratchRoot fixtures carry other (small) budgets. Budgets derive from the root, never from a caller.
• Disk capacity on runners and fleet hosts is not something this session can observe. This PR does not claim the volume holds 4 GiB plus headroom. The producer is gunbc.host.host_disk_observation (df per host). The apply-time refusal is gunbc.runner_lifecycle runner_width_disk_preflight. No consumer writes the durable root until C2.

Occupancy, concurrency, cleanup

• Index: one CAS slot per family in the root (occupancy-<family>), with a canonical versioned encoding (v2): live rows, then doomed rows. A slot that fails to decode refuses as StoreCommitOccupancyUnavailable and never reads as empty. Recovery is to delete the family's slot files; the next open then sweeps every object the empty index no longer names.

• One deletion authority: local_store_is_object_name holds exactly when a name is store_object_name's form: the prefix parses with std.content_hash parse_content_hash and re-serializes to itself, followed by the format suffix. An index row naming anything else, such as ../outside…, makes the index corrupt. The sweep uses the same relation, so a foreign notes.materialization.txt is never a candidate.

• Undeleted bytes stay charged: a reservation's single CAS does three things:

  • it retires the doomed names the host has now confirmed gone;
  • it admits the new row against the budget less the doomed bytes still charged;
  • it moves the rows it evicted into doomed.

  Filesystem.Delete now carries its typed error kind, and filesystem_delete separates a target that is already absent from a refused delete. A write publishes only if every delete it caused was confirmed. Otherwise it refuses as cleanup_outstanding and publishes nothing. Later writes that do not fit the budget less the undeleted bytes refuse the same way, so a host that keeps refusing deletes stops the writes instead of growing the disk.

• One writer per family (the family hold). Every write to a family -- reservation and its cleanup, deleting what it evicted, publication, settlement, recency -- runs inside one std.durable_exclusive_hold per family (gunbc.durable_exclusive_hold_file_store), held by the writing process and released when the write settles. The open-time sweep holds every family. A second writer refuses as busy and never waits; a refused commit costs only a recomputation. Lookups take no hold. This replaces the per-operation CAS handling of interleavings: a row evicted under its publishing writer, and a stale cleaner deleting an object a later writer republished, now have no schedule in which they can occur. So the post-publish re-read, StoreCommitEvictedDuringPublish and the declared in-flight residual are deleted.

• The ceiling, stated exactly: under the hold, the bytes charged (live plus doomed) are at most the family budget at every index write, and the bytes on disk are at most that, because an object is published only after every delete it caused is confirmed. The families' budgets sum to materialization_store_host_ceiling_bytes. There is no in-flight excess left to declare.

• A holder that dies holding a family is freed by observation, never by age. Its owner names its process (boot, pid, start time, pid namespace). The next writer looks it up on this host, and only a holder observed dead is recovered, through file_hold_recovery_assess; the store is added to that function's admit_callers. An unobservable holder stays held: a family that cannot be shown free is not written.

• The hold is required, not advisory. Every family mutation takes the held value and derives its root and family from it: index writes, reservation, deletes, the commit, recency. The sweep's deletes take a sealed LocalStoreAllFamiliesHeld. Both proofs are sole_constructor records minted only by the hold acquisitions, so a mutation without the hold cannot be written. test.claim.materialization_store_local_seal_witness asserts exactly one SoleConstructorViolation for each forged proof.

• The authority boundary, closed by construction.

  • One bracket: local_store_with_family(root, family, run) is the only way a writer's LocalStoreFamilyHeld is minted; it releases whatever the body returned.
  • No separate root: the held value carries the store root and the family, and no mutator takes either separately, so authority for one root or family cannot write another.
  • Sealed helpers: every raw effectful helper (acquire, settled acquire, release, index write, deletes, reserve, the commit and sweep internals, recency) is sealed with exact admit_callers to the bracket's own path.
  • Sealed admission: what a reservation admitted is a sealed LocalStoreAdmission, minted only by local_store_reserve.
  • Revalidation: a held value can still leak out of its bracket, so every mutation first re-observes the hold slot and refuses a stale hold. local_store_commit_under(held, ...) is the public held-taking entry.

• The opened store is one capability. LocalStoreCapability is sealed and binds the root, the store instance the marker names, and the exact family catalog with each family's byte budget. The marker encodes that catalog (families <family>=<bytes>,...), and a reopen with a different catalog refuses. The capability is minted only by local_store_open_decide, sealed to local_store_open plus one named hermetic fixture. Held values carry it, so a hold derives root, store and budgets from it. Lookup, commit, batch, recency and the bracket consume it and take no separate root, store or budgets. The bracket selects the family from a request, and recency takes the served requests.

• Round 10: exact catalog and a capability only after a clean sweep.

  • Marker codec. The catalog is one field of length-prefixed rows, <n>:<family>=<bytes>; (n counted in Unicode scalars), sorted, one row per family. store_marker_decode is a total scan over the whole marker. It requires exactly one catalog field, no leading zeros, no duplicate or unsorted rows, and exactly one instance line after the field; anything else is StoreMarkerMalformed. The magic is now v3, so a v2 marker refuses as unrecognized.
  • Bound from the marker. local_store_open_decide binds the DECODED catalog. It first refuses an offered catalog that names a family twice (LocalStoreCatalogInadmissible), then requires the offered catalog to encode to the identical canonical field. local_store_initialize refuses a duplicate catalog or a multi-line instance label before writing a marker.
  • Pre-open, then capability. Marker verification yields only a sealed LocalStorePreOpen, which no public function takes. LocalStoreCapability is now { binding, sweep: LocalStoreCleanSweep }. It is minted only in local_store_open_swept (sealed to local_store_open), from a sweep that held every family, read every index and had no refused delete. Otherwise the open is LocalStoreSweepIncomplete and nothing is writable. Holds carry the sealed LocalStoreBinding; the in-store lookup goes through the sealed local_store_lookup_bound.

• Lifecycle self-check (DESIGN 6b): each way a state could be reached without the invariant, and how it is closed.

  1. Marker write. A duplicate offered catalog or a multi-line label is refused before any write. Two concurrent initializers with different catalogs race create-new; the loser opens the winner's marker and refuses as a catalog mismatch. A torn marker (crash mid-write) decodes as malformed and the root refuses; this is fail-closed and needs an operator, with no route to a wrong bound.
  2. Decode. Delimiter collision, duplicate rows in either order, two catalog fields, extra or missing instance lines, leading zeros and unsorted rows all refuse (hermetic a_marker_outside_the_canonical_encoding_is_malformed; round trip and collision in the_marker_catalog_round_trips_and_no_two_catalogs_share_an_encoding).
  3. Open. A different offered catalog refuses before sweeping (wet partial-catalog and larger-budget controls). The budgets are the decoded ones (hermetic: an out-of-order offer binds the marker's order).
  4. Sweep. An unavailable sweep (hold, listing or index refused) and a refused orphan delete both mint nothing (wet an_unavailable_sweep_leaves_the_store_unwritable_by_real_execution and a_refused_orphan_delete_leaves_the_store_unwritable_by_real_execution; both red when the capability is minted regardless).
  5. After open. An orphan can appear only from a crash or a foreign writer. Every store write path charges its bytes in the index before creating a file (reserve, then create-new), so a crash leaves charged residue, never uncharged bytes. A process outside the store writing into its root is outside the modeled guarantee: no store bounds bytes it did not write.
  6. Mint. LocalStoreCapability, LocalStoreBinding and LocalStoreCleanSweep are sole_constructor. Spelling any of them outside the module is one SoleConstructorViolation (three probes, including promoting a pre-open's binding). The one hermetic fixture admitted to the decision receives a pre-open, which writes nothing.
  7. Use. Every mutation runs inside the family bracket and re-validates its hold. A leaked hold refuses as stale (existing control). Budgets, root and store come only from the binding.
  8. Release. A failed release leaves the hold recorded. A live owner's hold makes later writes refuse busy, and a dead owner's is recovered by observation (existing control). Writes refuse; nothing widens.
  9. Marker replaced under a live capability. The store never deletes or rewrites its marker, so only a foreign actor could. That is outside the modeled guarantee, as in 5.

• Public surface, audited (every function without admit_callers):

  • Capability mints (the only effectful functions that take a root or budgets): local_store_open(root, budgets) and local_store_initialize(root, instance_label, budgets). Both verify, or create then verify, the marker before any capability exists.
  • Capability consumers (effectful; nothing authority-bearing beside the capability or a held value derived from it): local_store_lookup(capability, req), local_store_commit(capability, req, payloads), local_store_lookup_batch(capability, reqs), local_store_record_recency(capability, served), local_store_with_family(capability, of, run) and local_store_commit_under(held, req, payloads).
  • Pure (no effect; a root, family, key or budget argument here derives a name or a figure and confers no authority): store_path, the marker codec (store_marker_family_row, store_marker_catalog_field, store_marker_head, store_marker_content, store_marker_catalog_admissible, store_marker_label_admissible, store_marker_scan_digit, store_marker_scan_step, store_marker_decode), filesystem_fault, store_read_observation, store_publish_observation, local_store_budget_sum, local_store_family_provider, local_store_family_budget, local_store_object_bytes, local_store_index_key, local_store_hold_key, local_store_object_suffix, local_store_is_object_name, the index codec (local_store_index_row_line, local_store_doomed_row_line, local_store_index_encode, local_store_digits_int, local_store_index_line_decode, local_store_index_decode), local_store_doomed_bytes, local_store_row_key, local_store_artifact_store, local_store_name_by_key, local_store_index_of, local_store_name_set, local_store_index_retention, local_store_stale_generations, the refusal renderers, local_store_hold_owner_process, local_store_authority_root, local_store_delete_split, local_store_object_presence, local_store_presence_converges, the commit-receipt constructors, and materialization_store_local_facts_at.

• One canonical family catalog per store. Initialization writes the family catalog into the identity marker (format v2), and open refuses a different or partial roster before anything is swept. The sweep decides orphans by reading every family's index, so a forgotten family would otherwise lose its objects.

• A windowed slot advances only when settled. Generation reclamation is best effort, so before the occupancy index or a family hold advances, any generation at or below head - k must be gone. The CAS store's cas_reclaim_below is retried once; if stale generations still stand, the write refuses (LocalStoreIndexUnsettled / LocalStoreHoldUnsettled). The slot then stops advancing, and its generation files stay bounded.

• Presence has three typed arms, read through the store's own verifying lookup. Verified present converges with no new bytes. Established absent runs the normal admission path at the current request's size. Unavailable (unreadable or failing verification: bytes may be there) refuses before any index write.

• Mechanical move: the process-holder identity, its owner text and the liveness observer moved from gunbc.machine_intake_mtcollins1_maintenance_hold to gunbc.process_hold_identity when the store became the second holder of that kind. Only the codec's unit_hold_ prefix became process_hold_; the bodies are unchanged, and the maintenance hold imports them.

• The hold slot's windowed operations are the store's alone. gunbc.durable_exclusive_hold_file_store keeps main's observe_file_hold, file_hold_acquire_prepare, file_hold_acquire, file_hold_release_assess and file_hold_recovery_assess unchanged. It adds observe_file_hold_windowed, file_hold_acquire_windowed, file_hold_release_assess_windowed and file_hold_recovery_assess_windowed, each sealed to the store function that calls it. The store's hold slot is windowed (k = 2), like its occupancy index, so a hold taken on every commit does not grow without bound.

• Self-clean on open: list the root first, then read the indexes, then delete only canonical object names that no index holds, live or doomed. The marker, index slots and foreign files are never touched. An unreadable index stops the sweep. The pure local_store_open_decide stays filesystem-free and reports LocalStoreSweepNotRun.

• Recency is advisory (ruling 1a). A lookup never writes. local_store_record_recency does one CAS per family per process. Losing it only makes eviction less precise, and it has no refusal arm.

Leasing domain: opt-in generation windows (DESIGN 3b)

The index changes on every commit, but gunbc.durable_cas_file_store keeps every generation forever. Keep-all and windowed are two contracts with two names, added beside each other; nothing on main changes.

• Unchanged (main's signatures, result types and keep-all semantics): file_compare_and_set(root, publication, verified) -> CasOutcome, observe_cas_slot_state(root, key), and the hold operations above. No caller outside this PR's own modules is touched, so callers landing on main in parallel keep compiling.
• Added, store-private: file_compare_and_set_windowed(root, publication, verified, window: CasGenerationWindow) -> CasFileWrite { outcome, reclamation } and observe_cas_slot_state_windowed(root, key, window). Each admits only extdeps.realization.materialization_store_local's caller and one named witness. k >= 2 is construction: CasGenerationWindow is sole_constructor, reached only through cas_generation_window.
• One implementation beneath both, sealed. file_compare_and_set_retained and observe_cas_slot_state_retained take the internal CasSlotRetention selector and admit only their two wrappers and the in-module hold paths. The raw helpers are sealed to their exact callers: cas_compare_and_set_outcome (to the retained commit), cas_observe_retained_slot and cas_observe_window (to the internal observers), cas_window_generations, and the effectful cas_reclaim_below (to the windowed commit and local_store_settle_slot). A keep-all caller cannot mint a window, commit windowed or delete an audit slot's generations: five admission probes (a_direct_*_call_is_an_admission_refusal) each assert exactly one ConstructorCallAdmissionRefused.
• The settlement gate is on the only windowed write path. The store calls local_store_settle_slot before every windowed commit, and the windowed API admits no other writer, so no caller can advance a window past an unreclaimable generation. Executing red: an_unreclaimable_index_generation_stops_further_writes_and_bounds_the_slot_by_real_execution. It makes generation 1 undeletable; once the window passes it, five further writes refuse before head+1 exists and the slot's file population is unchanged.
• Window reads take the head from a slot-root listing and verify head+1 is absent. On a race they re-read, bounded, and otherwise refuse (ProbedWindowHeadUnsettled); they never guess. Window writes reclaim at or below head-k only after their own commit, and a refused delete is reported in CasFileWrite.reclamation.
• Unsealed effectful scan, both modules: every public effectful function left in durable_cas_file_store and durable_exclusive_hold_file_store is main's, with main's signature (cas_read_generation, cas_probe_gallop, cas_probe_bisect, cas_first_generation_absent, cas_observe_slot, observe_cas_slot_state, cas_commit_at, file_compare_and_set, cas_slot_keys; observe_file_hold, file_hold_acquire_prepare, file_hold_acquire_commit, file_hold_acquire, file_hold_release_assess, file_hold_release_commit). The hold plans carry the retention internally and stay sole_constructor, so a windowed plan exists only from a sealed windowed assess.
• The leasing conformance row (gunbc.design_argument) cites file_compare_and_set_windowed and states the two-contract split; DESIGN.md is regenerated from it. docs/plans/fabric-storage.md names the head-probe bound this also lifts; the fabric heads are not opted in.
• The durable exclusive hold, revisited: an earlier revision of this PR declined the hold because its slots were unbounded CAS slots. The retention parameter above removes that objection. Three review rounds of per-operation interleaving fixes then showed the earliest unjustified boundary was unowned concurrent mutation of one family (DESIGN 6b), so the hold now owns it.

Evidence (BuildBuddy, by real execution)

• materialization_store_local_wet_witness_test:
  • Disk bound: 12 commits overrun a 4096-byte fixture family. After every commit the root's object bytes, measured from the files rather than the index, stay at or below budget. Before the run it is 0; after, it is positive and at or below budget. Evictions occurred.
  • Refusals: over-budget refuses and evicts nothing; an undeclared family refuses; a corrupt index refuses and never reads empty.
  • Cleanup: an orphan is swept on open while the indexed object and the marker are kept. The index slot stays at or below k+1 files after 12 commits.
  • Recency: recorded once, and records nothing for unknown names.
  • One writer per family: while the family is held by a live writer (this process), a commit refuses as busy and writes nothing; after release, the same commit lands. It goes red when a live holder is treated as recoverable.
  • Dead holder: a hold owned by this boot and namespace but a pid with no process is recovered by observation, and the commit lands.
  • Leaked hold: a bracket body returns its held value; committing under it afterwards refuses as stale and writes nothing. Red when the revalidation is disabled.
  • Seals (test.claim.materialization_store_local_seal_witness): a forged LocalStoreAdmission is exactly one SoleConstructorViolation, and direct calls to local_store_write_index and local_store_acquire_settled from outside are exactly one ConstructorCallAdmissionRefused each.
  • Budget bound to the store: a store created with the fixture budgets, reopened with a larger budget for the same family, refuses; the root's bytes stay within the created budget. Red when the catalog carries names only.
  • Forged capability: spelling a LocalStoreCapability is exactly one SoleConstructorViolation. Neither a hand-built store for an uninitialized root nor one store's identity on another root can be written.
  • Partial catalog: a store initialized with two families holds an object of one. Reopening with a roster that omits that family, or with none, refuses, and the object still serves. Red when the catalog check is disabled.
  • Unreclaimable generation: the index's first generation is replaced by a directory. After the window passes it, every later commit refuses, and the slot's file count does not grow. Red when the settle gate is disabled.
  • Presence unavailable: a directory at Y's object path makes Y's presence unestablishable; the commit refuses and the index is unchanged. It goes red when unavailable is treated as absent.
  • Persistently refused delete: X's file is replaced by a directory, so every delete of it is refused. Y's eviction of X is refused, so Y refuses as cleanup_outstanding and is not published. A later Z also refuses, because X stays charged. Once the obstruction is cleared, Z commits and its receipt names X as retired. Disk stays within budget throughout.
  • Names: traversal, suffix-only and prefixed names are not object names. A foreign notes.materialization.txt survives the sweep, and an index row naming ../outside… refuses as corrupt.
  • Reds: with the unconfirmed-delete gate disabled, the refused-delete control fails. Each retry control fails with its fix reverted, and so do the busy and presence controls. All 29 of the store file's claims pass, plus all 15 seal and admission probes (executed in the session container).
  • Hold slot bounded: after 12 commits the family's hold slot holds at most k+1 files, beside the occupancy index slot.
• durable_cas_file_store_wet_witness_test: a window slot keeps at most k+1 files after 10 commits and reads its head back; a KeepAll slot keeps all 10; a racing writer under a window loses, re-reads and lands, so both commits stand; k=1 is not admitted. All 11 claims pass.
• Every other claim file importing a changed module: 39 hermetic files gave 391 PASS / 5 FAIL; wet files gave 110 PASS. All 5 hermetic FAILs and the one remaining wet FAIL (a_listener_behind_a_failed_connect…: the runner has no /proc/net/tcp6) fail identically at base with this diff reversed.
• Four stale #get bare-provider roster rows (pre-existing drift that blocks admission of their wet files) are retired as ImportsFixed. One overlaps Delete both dead cross-run stores; rehome keying to v1_compiler.closure_identity #13064.

Not in this PR

C2: the TypecheckModuleRequest per-module encoding and the seed consumer. Compute-family budgets: bold-dove-431 declares theirs with its own grounding. Cross-host binaries belong on std.fabric_blob.

Do not merge from this session; the operator lands it.

🤖 Generated with Claude Code

[briansrls]

Blocking at exact head 2585470: C1 does not yet establish the hard on-disk capacity bound it claims.

1. A reservation can be evicted before its object is published. Reachable interleaving with family budget B: writer A reserves X of size B, committing index {X}, then pauses. Writer B reads {X}, reserves Y of size B, and store_put evicts X, committing index {Y}; its delete of X is either a no-op or a reported refusal because X is not present yet, and B still publishes Y. A then publishes X and verifies its exact readback. local_store_commit never re-reads the occupancy index after local_store_reserve, so A can return StoreCommitSettled. Disk now holds X+Y (2B) while the index names only Y. This falsifies the module's stated construction that every published object is indexed when it appears; a future open may sweep X, but no future open is required for the CapacityBounded claim.

2. Independently, eviction failure is not fail-closed. local_store_delete_names returns refused names, but local_store_commit proceeds to publish and settle the new object; the refused deletes are only attached to the receipt. Repeated delete refusal therefore permits physical object bytes to grow past the family budget. local_store_open likewise returns LocalStoreOpened when sweeping reports delete_refused/unavailable, and the CAS generation window commits even when reclamation is incomplete. These are useful diagnostics, but they do not bound disk use. Either unremoved bytes must remain accounted against the budget, or new publication/further writes must refuse until cleanup is established.

3. The persisted index is later used as deletion authority without validating its names. local_store_index_row_decode accepts any non-empty token, while store_path simply appends that token to the root; a syntactically valid row such as ../outside can escape the root when evicted. The sweep recognizer is also only contains(".materialization."), despite the authority saying foreign files are never touched. Decode/admission needs the exact canonical store-object filename relation before any row can authorize a delete, and sweep needs the same exact recognizer.

Please add discriminating controls for the reserve/evict/publish interleaving, persistent delete refusal, and malformed/foreign names. The sequential healthy-host witnesses are green, but they do not reach these paths. I found no objection to the per-family budget vocabulary or the KeepAll/KeepGenerationWindow split once these realization gaps are closed.

[briansrls]

One blocking capacity path remains at exact head bb3b97c.

The three prior findings are substantially repaired: deletion authority is now the canonical store-object-name relation; delete refusals stay typed and doomed bytes remain represented; and the post-publish re-read catches the reserve/evict/publish race. But a retry of the SAME request bypasses the new cleanup gate.

Reachable sequence with X occupying the family budget and Y requiring X's eviction:

1. Y's first reservation writes an index with Y live and X doomed.
2. Deleting X is refused, so the commit returns cleanup_outstanding and Y is not published.
3. A normal retry of Y reads the same index. Cleanup of doomed X is refused again, but live_names already contains Y, so local_store_reserve returns LocalStoreReserved { evicted: [], ... } before applying the artifact > budget_total - undeleted cleanup-outstanding check.
4. local_store_publish_reserved therefore has no evicted deletions to gate on, publishes Y, and its post-publish read sees Y live, so the commit settles. X remains doomed and physically present. Disk now holds X + Y past the family budget.

The new persistent-delete control retries a different name Z, so it correctly reds that path but does not discriminate this same-name retry. This is not the declared in-flight publish/re-read residual: it is a completed settled write after an earlier cleanup_outstanding refusal.

There is also a matching authority mismatch in the index claim: when store_put evicts X, next_index keeps the packed live rows (including Y) and appends X to doomed, so live+doomed can exceed the family budget at that CAS. That temporary over-accounting could be an honest reservation state, but rows currently do not distinguish reserved-not-published from live/present, which is what enables the retry above.

Required repair: make an already-indexed name distinguish an existing verified object from an unmaterialized reservation. A retry may converge when the exact object is already present and valid, but if it is absent and doomed bytes leave no room it must remain cleanup_outstanding (or otherwise clear the cleanup debt before publication). Add the direct control: first Y returns cleanup_outstanding, retry Y before clearing X, Y must still not appear and disk must remain bounded.

The canonical-name, typed-refusal, traversal/foreign-name, and original interleaving repairs otherwise look sound. All four exact-head checks are green, but they do not reach this retry path.

[briansrls]

Blocking at exact head af65ffa: review 75099's policy-placement and typed-carrier corrections are sound, but my prior same-request cleanup-debt bypass remains reachable.

In local_store_reserve, after retrying doomed deletions it computes undeleted and live_names, then checks set_contains(live_names, name) before artifact > budget_total - undeleted. So this sequence still succeeds incorrectly:

1. X is committed.
2. First Y attempt reserves Y, moves X to doomed, cannot delete X, returns cleanup_outstanding, and does not publish Y.
3. Retry the same Y while X is still undeletable.
4. Y is already in the live index, so reserve returns LocalStoreReserved immediately, bypassing the cleanup-outstanding test.
5. The publication phase has no newly evicted names to delete, publishes Y, and the post-publish reread sees Y live, so it can settle while physical X remains. Disk exceeds the family budget after the commit returns.

Carrying the reservation's real budget removes the zero-budget fallback but does not close this branch-order defect. The idempotent/live fast path must distinguish a verified existing object from an unfinished reservation whose object is absent, or cleanup debt must gate that path. Add the direct control: X committed -> first Y cleanup_outstanding -> retry Y before clearing X -> retry still refuses, Y remains absent, physical bytes stay within budget. CI can be assessed after that code correction.

[briansrls]

Blocking at exact head 9fe2537: the same-payload retry bypass is closed, but an unfinished live reservation is still bound only to the FIRST attempt's byte count, not to the current prepared object.

The live-row arm reads the object. Present eventually goes through store_commit_settle and can converge without new bytes. Absent calls local_store_reserve_unfinished, which computes live and own from the persisted index row and never receives the current prepared object's bytes. A retry of the same request can offer a different result and a larger encoded object—the store already models divergent outputs for one request key. Reachable case: other live rows remain; the first, smaller Y reservation evicts X and its publication is blocked by X's refused delete; X is later cleared; old-live-bytes + remaining-live-bytes now fit, but a retry of Y carries a larger prepared result such that current-Y-bytes + remaining-live-bytes exceed the family budget. The unfinished arm admits from the stale smaller row, publication creates the larger Y, the post-publish read sees Y's name live, and settlement can succeed while the index undercharges the object and physical bytes exceed the ceiling.

Bind an unfinished reservation to the prepared result (at least its byte size, preferably its offered result/content identity), or re-run/update that live row under CAS using the current object's bytes before publication. A size mismatch may refuse if that is the chosen contract, but it cannot inherit the old row's accounting. Add a wet red with: another live object retained; first small Y attempt cleanup_outstanding; doomed X cleared; same Y retried with a larger payload; the retry must update/repack or refuse and disk must stay within budget.

The requested same-Y/same-bytes control is good, the map provider and debt-roster corrections are correct, and all four exact-head checks are green. I found no other blocker.

[briansrls]

Blocking at exact head 281714d.

The requested stale-size repair is closed. When a live row's object is absent, the retry now falls through the ordinary admission path with the CURRENT prepared object's bytes; store_put replaces the stale row's size and repacks/evicts against that figure. The new wet control retains W, creates a smaller unpublished Y reservation, clears doomed X, retries the same Y larger, requires W to be evicted, and checks physical bytes stay within budget. That is the discriminator I requested.

One adjacent fail-closed gap remains: local_store_object_present maps both FilesystemExactPathUnreadable and FilesystemExactPathKindUnrecognized to false, exactly like established absence. An already-live object can therefore physically exist but be unreadable; a retry then enters the unfinished-reservation path, replaces its indexed byte charge with the offered result's size, may evict other live rows, and only later refuses when publication/readback sees the occupied or unavailable object. The index mutation is not rolled back. Retrying an unreadable large object with a smaller offered result can consequently undercharge the existing bytes and admit later writes beyond the physical family ceiling. This also contradicts the store's own rule that only NotFound is absence and every other read failure is unavailable.

Required repair: make the live-row observation at least three-way—readable present, established absent, unavailable/unrecognized. Only established absent may re-enter current-size admission. Unavailable/unrecognized must refuse before any index CAS or eviction, carrying the typed observation. Add a control with a live row whose object path is unreadable/non-file and another retained live object; retrying must leave the index and the other object unchanged and refuse rather than treating the path as an unfinished reservation.

All four exact-head checks are green; this path is not covered by the current 21 wet controls.

[briansrls]

Follow-up at the same exact head; the existing REQUEST_CHANGES remains in force. The current-size repack and its larger-retry wet control do close the stale-size finding. The detail does not close the current blocker: local_store_object_present still maps FilesystemExactPathUnreadable and FilesystemExactPathKindUnrecognized onto the same false result as established absence, after which the ordinary admission path may rewrite the index before final readback refuses.

Reviewing the stacked byte-part change also exposed a second C1 concurrency gap: doomed cleanup is performed physically after reading an index generation but before winning the CAS that removes the doom. A stale cleaner can read generation I and pause; another cleaner can delete X and CAS-remove the doom; a new writer can reserve, publish, post-read and settle X; then the stale cleaner can resume and delete the new X before losing its CAS against I. The physical delete is not owned by an index state. Cleanup needs a claimed/tombstoned/leased state established before deletion, or an equivalent construction preventing same-name republication until every stale cleaner is unable to delete it. This needs an interleaved control.

[briansrls]

Blocking at exact head 2a4cb50.

The Round-8 opened-store substitution finding is materially closed: LocalStoreCapability is sole-constructor, carries root + portable store identity + budgets, held values carry it, and the public lookup/commit/batch/recency/hold routes no longer accept independent authority-bearing arguments. The forged-capability and larger-budget reopen controls are the right discriminators.

Two gaps remain in that construction.

1. The persisted catalog is not an exact, uniquely decoded catalog yet.

store_marker_catalog_line renders each row as <family>=<bytes>, sorts the rendered strings and comma-joins them. ArtifactKindId is only a branded NonEmptyStr, so the encoding is not injective: [x=1, y=2] and one row whose family is x=1,y and budget is 2 both render x=1,y=2. Duplicate rows are also semantically ambiguous: [F=10, F=20] and its reversal render the same marker, while local_store_family_budget selects the first offered F row, so the effective budget changes after a reopen that the marker accepts. Separately, store_marker_catalog_matches accepts any matching line anywhere in the marker; a marker containing two families ... lines can authorize two different catalogs under the same store-instance bytes.

Required repair: one total canonical marker decoder, exactly one catalog field, unambiguous family encoding (for example length-prefixing), unique family keys, and refusal on duplicates/extras/malformed rows. Prefer populating the capability from the decoded marker catalog rather than retaining the caller's list after a textual membership check. Add controls for duplicate-row reversal, a delimiter collision, and two catalog lines.

2. A writable capability is returned even when open-time cleanup did not establish the physical bound.

local_store_open_decide mints LocalStoreCapability before sweep. local_store_open then always returns LocalStoreOpened { capability, sweep: local_store_sweep(...) }, including LocalStoreSweepUnavailable and LocalStoreSwept with non-empty delete_refused. The write APIs consume only the capability; they do not require a clean-sweep proof.

Reachable red: initialize at budget B; plant a canonical unindexed orphan (the existing sweep control already models this residue); make the reopen sweep unable to acquire the family hold, or make the orphan deletion refuse; retain the returned capability; once the hold clears, commit indexed bytes up to B. The orphan remains uncharged, so physical store bytes exceed B. In stacked #13095 a process crash can natively leave a .copy orphan, so this is not only an externally planted population.

Required repair: marker verification should mint only a pre-open/internal handle. Export the writable LocalStoreCapability only after sweep proves every canonical orphan gone, with no unavailable sweep and no refused deletion; alternatively carry a sealed clean-sweep proof required by every mutation and charge any retained residue. Add the direct failed/refused-sweep-then-write capacity red.

All four exact-head checks are green. I found no remaining objection to the root/store/budget argument consolidation itself. Do not queue this head.

[briansrls]

Approved at exact head 77d6548.

Both Round 9 blockers are closed by construction.

1. The marker catalog now has one canonical, injective encoding and one total decoder. Family names are scalar-length-prefixed, byte capacities are canonical decimal values, rows are sorted and unique, and the decoder consumes the whole marker with exactly one catalog field and one instance line. Duplicates in either order, delimiter-bearing names, noncanonical digits, unsorted rows, extra catalog/instance lines and malformed lengths refuse. The opened binding carries the catalog decoded from the marker, while a caller's offered catalog is only checked for exact canonical equality; it is not the source of the enforced budgets.

2. Marker verification yields only LocalStorePreOpen. The writable LocalStoreCapability contains a sealed LocalStoreCleanSweep and is minted only by local_store_open_swept after every family was held, all indexes were readable, and the sweep had neither an unavailable outcome nor any refused deletion. Refused/unavailable sweep paths return LocalStoreUnavailable and expose no capability. The wet controls prove a later write is impossible and physical bytes remain within B; the capability, binding and clean-sweep proof are independently unforgeable.

The public surface remains authority-complete: effectful store operations consume LocalStoreCapability or a held value derived from its binding; no separate root, portable store identity, catalog, family, slot or store path can be substituted. All four exact-head checks are green. Queue #13081.

[briansrls]

Re-approved at exact head 6942881.

The head is a merge of the previously approved 77d6548 with main at a78d8f0 (#13208). The only compatibility resolution required by C1's CAS API is mechanical and correct in gunbc.roadmap_dogfood_route: KeepAllGenerations is supplied to both observe_cas_slot_state calls and to file_compare_and_set, and the write matches the CasFileWrite.outcome projection. That preserves #13208's keep-every-generation behavior; no windowed-retention policy is accidentally imposed on the dogfood start receipt.

The approved materialization-store implementation is unchanged in the approved-head-to-current-head delta. Exact-head floor, generated, emit-build, and witnesses all completed successfully, and the PR is open, non-draft, and mergeable. Queue #13081 first.

[briansrls]

Blocking at exact head a0d9060.

The additive recut fixes the compatibility failure: file_compare_and_set / observe_cas_slot_state and the non-windowed file_hold_* entry points have their old signatures, result shapes and keep-all behavior; file_compare_and_set_retained, observe_cas_slot_state_retained and the hold retained helpers are sealed to their wrappers/internal commits. The changed-file population no longer includes the parallel keep-all callers, and the exact-head four checks are green.

Two related construction gaps remain against the requested criterion.

1. file_compare_and_set_windowed does not itself preserve the generation-settlement gate. file_compare_and_set_retained first calls cas_compare_and_set_outcome, which can commit head+1, and only after CasCommitted calls cas_reclaim_below. If an old generation <= head-k is undeletable, a direct caller can invoke file_compare_and_set_windowed repeatedly and each call can advance before reporting CasReclamationIncomplete. materialization_store_local's local_store_settle_slot correctly blocks ITS index and hold paths before they advance, but that gate is outside the public windowed contract. The current CAS wet evidence tests successful reclamation, not persistent cleanup refusal followed by another direct windowed write.

2. The keep-all/windowed split is bypassable below the wrappers. cas_compare_and_set_outcome is public, accepts CasSlotRetention directly, and has no admit_callers. cas_reclaim_below is also public and performs the generation deletions with caller-supplied root/key/window/head. cas_observe_retained_slot likewise exposes the retention selector. A module using the ordinary keep-all API can import these helpers, mint a CasGenerationWindow, commit under KeepGenerationWindow and/or delete generations from an audit slot. Thus it is not yet true by construction that only the distinct windowed contract can reach windowed observation/reclamation.

Required repair: either (A) make the windowed API explicitly store-private, sealing file_compare_and_set_windowed, observe_cas_slot_state_windowed and the file_hold_*_windowed family to materialization_store_local plus named witnesses, or (B) make the public windowed contract itself perform the pre-advance settlement gate. In either case, seal cas_compare_and_set_outcome to file_compare_and_set_retained, cas_observe_retained_slot to its exact internal callers, and cas_reclaim_below to the windowed implementation plus local_store_settle_slot. Add admission reds for the raw helper calls and an executing red: leave generation <= head-k undeletable, invoke the public windowed write again, require refusal before head+1 is created and no file-count growth.

The PR body also still describes the superseded breaking API (file_compare_and_set returning CasFileWrite, every old caller passing KeepAllGenerations, and dogfood-route migration). Recut that section to the additive two-contract design before landing.

I found no regression in the previously approved materialization-store authority construction. Do not queue this head.

[gunbai-bot]

Review 76441, both findings fixed in 9419c77:

• StoreMarkerScan is now a declared coproduct, one arm per phase: StoreMarkerReadingCount, StoreMarkerReadingName, StoreMarkerExpectingEquals, StoreMarkerReadingBytes and StoreMarkerPastField, plus StoreMarkerScanRefused. Each arm carries only its own fields, so 'refused with live spans' and an out-of-range phase have no constructor. A numeral in progress is StoreMarkerDigits (StoreMarkerNoDigits | StoreMarkerDigitsRead { value }), which refuses leading zeros and overflow. The scalar position lives in a wrapper, StoreMarkerScanAt.
• StoreMarkerSpan.bytes is ByteSize, parsed straight from the numeral, so the decoded catalog's budgets carry no bare-Int crossing.
  The three hermetic codec controls and the wet open controls (larger budget, partial catalog, commit/read-back) pass on it.

[briansrls]

Approved at exact head 3a8672d.

This implements option A coherently. Main's keep-all contracts retain their exact public signatures and result types. The windowed CAS and hold operations have distinct names and admit only the materialization-store path plus the named executing fixtures. The internal retention selector and raw effectful helpers are sealed to exact caller rosters: cas_compare_and_set_outcome only from file_compare_and_set_retained; cas_observe_retained_slot only from the internal observation/commit paths; cas_observe_window and cas_window_generations only from their named readers; and cas_reclaim_below only from the retained post-commit cleanup and local_store_settle_slot. The compile probes discriminate direct windowed CAS/hold access and direct raw outcome/observe/reclaim access.

The generation-settlement property remains on the store's only production windowed-write route. local_store_write_index gates local_store_write_index_settled through local_store_settle_slot; family acquisition does the corresponding hold-slot gate. The new wet control makes generation 1 undeletable after generation 3 commits, then proves generations 4-8 all refuse before publication and the slot-file population does not grow. That is the requested red for the former unbounded repeated-call route.

The PR body's API section now accurately describes the additive two-contract design rather than the superseded required-argument migration. The effectful-surface scan agrees with the code: the remaining unsealed effectful functions are the pre-existing keep-all API or sealed-plan commits, while every new windowed/raw path is restricted.

All four exact-head checks are green. Queue #13081 first.