Skip to content

M1.c L5a: per-user store policy (XDG cache home, 2 GiB ceiling, UserCacheRoot, one ceiling-typed store construction) - #12596

Closed
briansrls wants to merge 5 commits into
mainfrom
m1c-l5a-store-policy
Closed

briansrls wants to merge 5 commits into
mainfrom
m1c-l5a-store-policy

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

M1.c compiled acquisition bridge, unit L5a: the store policy the local per-user compiler store needs, declared ahead of its consumers.

What lands

  • extdeps.freedesktop.xdg_base_directory (new) is the cited authority for the per-user cache home. It follows the XDG Base Directory Specification 0.8:
    • An absolute XDG_CACHE_HOME wins.
    • A relative or empty one is ignored, and the result names that.
    • The fallback is $HOME/.cache.
    • An unset, empty or relative HOME refuses with its own cause. There is no substitute directory.
    • XdgCacheHome is sole_constructor.
  • gunbc.materialization_store_capacity (new) is the one home of the store byte ceiling. UserCacheRoot gets 2 GiB, measured in apparent file bytes (manifest plus blobs). DurableHostVolumeRoot answers StoreCeilingUndeclared, because no size has been decided for the unattached fleet volume and borrowing 2 GiB would be fabricated policy.
  • std.materialization_store_grant:
    • adds UserCacheRoot { cache_home: XdgCacheHome }, rooted at <cache home>/gunbc/materialization-store;
    • gives WitnessScratchRoot a fixture ceiling;
    • rewrites the module's durability invariant. The §3b divergence (the durability of a root derived from the environment) is stated and executed by durability_is_the_arm_s_not_the_path_s, and rests on object-level preimage verification.
  • std.artifact_store:
    • artifact_store_for_ceiling(StoreCeiling) is the one construction of a store from a ceiling. It never takes a raw ByteSize.
    • store_over_provider_resolved is the provider door: every existing provider check, then that same construction.
    • artifact_store_with_occupancy seeds held rows in recency order, with no per-row replay.
    • The commit order L5b will use: the opened root's ceiling, then artifact_store_for_ceiling, then artifact_store_with_occupancy, then one store_put.

Declared frontier (DESIGN §3c)

Every new declaration has a witness consumer now. Its production consumers land later, and each declaration's leading comment names its trigger:

  • artifact_store_for_ceiling, artifact_store_with_occupancy and materialization_store_byte_ceiling: L5b, which is local_store_commit, the catalog retention and first-use initialization.
  • xdg_cache_home and UserCacheRoot: L8, where the route root opens the store.

The catalog-row witness the_store_catalog_row_admits_exactly_the_ceiling_store lands with the catalog's retention in L5b. Declaring that retention now would claim a ceiling and eviction that nothing applies yet (§4d).

Controls

All runs used claim_batch --hermetic built at this head. Results are recorded on the merged head below.

control result
xdg_base_directory_witness 7/7
materialization_store_capacity_witness 3/3
materialization_store_grant_witness 4/4
artifact_store_witness, in full 31/31
materialization_store_witness 28/29. The one FAIL, a_tampered_part_size_is_an_integrity_refusal, fails identically on clean main
wet materialization_store_local_wet_witness (--wet) 8/8, with no /tmp residue
mutation reds: 25 rounds in total, each with its predicted red set written down before the run every round red on exactly the predicted witnesses and nothing else. Covered: XDG rules; the ceiling value and unit; durability; forking the construction (the door minting its own store); the door skipping each check (release policy, LRU-only, authority, unit); constant sizing; seeding (ordinals, dropped rows, re-sizing, reversal, per-row replay)
entry-route unimported-bare-provider judgment on every touched module and each file whose roster row was retired 0 refusals. Red control: a planted bare filter refuses UnimportedBareProvider Unrostered ...xdg_base_directory.dag#filter

Known limit. A second construction that is identical in value cannot be detected by a value-level witness. Any fork that diverges goes red on the_resolved_door_answers_the_one_ceiling_construction.

Roster retirements

19 rows in src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag move from ActiveDebt to Retired { cause: ImportsFixed }.

  • Cause: the new import std.artifact_store → gunbc.materialization_store_capacity (for StoreCeiling) brings v2.std.algebra into those files' closures through std.effect_grant.
  • Evidence: each retirement is what the entry-route judgment printed.
  • Consequence: a later change that removes that edge must add explicit imports in those 11 files. That includes L1, which drops std.effect_grant's v2.std.algebra import, and L4's std.artifact_store_provider carve. The floor refuses loudly if that is missed.

Receipts

These are carried here rather than in the upstream module (DESIGN §3, External upstream decomposition; §4c):

Stated departures from the spec text

  • materialization_store_byte_ceiling returns StoreCeilingResolution, with StoreCeilingUndeclared for DurableHostVolumeRoot, as above.
  • The unit is carried in the field name StoreCeiling.apparent_file_bytes rather than as a separate unit type, because the v1 seed reads a single-variant coproduct as a type alias.
  • XDG's 0700 creation rule lands with its only consumer, L5b's first-use initialization.
  • The version is held once, as the anchor's literal locator. A locator computed from a version row would project refused on the corpus anchor wall.
  • The spec's artifact_store_from_occupancy(ceiling) became the commit order above. M1.c compiled acquisition bridge: exact seed closure, emitter repairs, scoped exception (pre-merge-review spec, rev 3) #12581 §7.2 and §8 will be updated to match.

Pre-existing reds in this closure, none caused by this change

  • materialization_store_witness a_tampered_part_size_is_an_integrity_refusal.
  • external_model_scope_witness carriers_declare_scope_on_disk and frontier_rosters_are_disjoint, and the scope placement gate's freeze arm. All three come from dag/extdeps/bmc/ipmi_boot_selection.dag being both a scope carrier and a frozen-manifest row.
  • corpus_live_clean_tree_wall_holds, which is already expected-red.

Obligations recorded for later units

  • L5b: a UserCacheRoot with XDG_CACHE_HOME=/var/lib has the same store path as the fleet root, so one directory would carry two ceilings. The fix is either to put the root arm in the store marker, or to refuse a user root that equals or nests the fleet root.
  • After L3: consolidate the four directory-child joins into one, in extdeps.filesystem.
  • L8: confirm that the frozen v1 emitter renders these modules once they are stage0 mirrors.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 5 commits September 29, 2026 02:52
…, UserCacheRoot, occupancy rebuild

Lands the store-policy half of the M1.c compiled acquisition bridge (spec gunbc#12581
revision 3, section 4 "Store path", section 8 row L5a) as a DECLARED FRONTIER: every new
declaration is executed by a hermetic witness now, and its production consumers arrive in
named later landing units.

- extdeps.freedesktop.xdg_base_directory (new, scope carrier): the XDG Base Directory
  Specification 0.8 as the cited authority for the user's cache home. XdgCacheHome is
  sole_constructor, minted only by xdg_cache_home: an absolute non-empty XDG_CACHE_HOME
  wins; an empty or relative one is ignored (and named on the result); the fallback is
  $HOME/.cache; an unset, empty or relative HOME refuses (the one rule the spec is silent
  on, stated as such). Enrolled in gunbc.extdeps_scope_frontier scope_carrier_paths.
- gunbc.materialization_store_capacity (new): the one home of the store's byte ceiling,
  in apparent file bytes (the unit is the field's name). UserCacheRoot 2 GiB (Q11),
  WitnessScratchRoot its fixture field, DurableHostVolumeRoot StoreCeilingUndeclared --
  a stated departure from the spec's `-> StoreCeiling`, because no size is decided for
  the unattached fleet volume and a borrowed number would be fabricated policy.
- std.materialization_store_grant: + UserCacheRoot { cache_home: XdgCacheHome } at
  <cache home>/gunbc/materialization-store, DurableAcrossRuns, Read+Write granted at the
  store root only; WitnessScratchRoot gains `ceiling` (13 sites, 3 files). The module's
  invariant is rewritten and the section 3b divergence stated: an environment-derived
  root answers durable in XDG's sense of the cache home.
- std.artifact_store::artifact_store_from_occupancy (new): observed rows in recency order
  (least recent first) become ordinals 1..N; no per-row replay, so over-ceiling occupancy
  is kept and the commit's ONE store_put evicts it, counted.

Frontier and triggers:
- xdg_cache_home's production reader and UserCacheRoot's constructor: L8's route root
  reads XDG_CACHE_HOME/HOME and opens a UserCacheRoot.
- materialization_store_byte_ceiling and artifact_store_from_occupancy: L5b's
  local_store_commit (census -> ceiling -> occupancy -> one store_put), and L5b's
  catalog retention row naming the ceiling as its RuntimeDerivedLimit authority.
- the spec's 0700 directory-creation rule lands with its only consumer, L5b's first-use
  initialization.

Touches no file #12401 edits.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…reaches eviction only as StoreCeiling

Applies the adversarial review of cf1fd44.

MAJOR -- no caller-supplied ByteSize sizes the occupancy store.
- std.artifact_store: store_over_provider_resolved(provider, resolved: StoreCeiling) is the
  RuntimeDerivedLimit arm of the EXISTING construction path (store_over_provider_with threads an
  optional resolved ceiling through store_from_capacity and store_from_limit), so release policy,
  capacity unit and at_capacity are judged exactly as store_over_provider judges them. It admits
  the ceiling only for a provider whose authority is
  gunbc.materialization_store_capacity materialization_store_byte_ceiling_authority
  (CapacityAuthorityMismatch otherwise) and refuses a resolved ceiling beside an ExactLimit
  (ResolvedCeilingBesideExactLimit).
- artifact_store_from_occupancy(ceiling: ByteSize, ...) is replaced by
  artifact_store_with_occupancy(store, occupancy): it seeds the store a StoreReady carried, keeps
  its budget, and continues its ordinal counter. ArtifactOccupancyRow.artifact_bytes is renamed
  apparent_file_bytes (the Q11 unit).
- artifact_store_witness: the occupancy claims build their store as L5b's commit will (a witness
  root's ceiling from its one home, then the resolved door); 7 new resolution controls and 1 new
  seeding control.

Minors.
- std.materialization_store_grant: the durability divergence now rests on object-level preimage
  verification; the UserCacheRoot / DurableHostVolumeRoot path collision is an L5b obligation with
  both fixes named; the UserCacheRoot frontier sits directly above the root type.
- extdeps.freedesktop.xdg_base_directory: xdg_base_join's comment names the four copies of the
  directory-child join; the absolute-path rule is cited to section "Basics"; the READ and git-grep
  receipts are removed (PR body); the frontier sits above xdg_cache_home. The version is held once,
  in the anchor's literal locator: the version row and the literal-agreement witness are deleted,
  and the scope subject is XdgCacheHome. A stated departure from the review's suggested
  mechanism (derive the locator from the version row): a derived locator projects `refused` on the
  corpus-cadence anchor projection behind corpus_live_clean_tree_wall_holds (observed), the
  constraint extdeps.pin and extdeps.posix.shell_command_language record.
- gunbc.materialization_store_capacity: the transcribed 12.4 MB / ~170 figures are replaced by the
  instrument (the commit's census line); frontiers sit above the declarations they name.

Consequence of the new import (std.artifact_store -> gunbc.materialization_store_capacity):
v2.std.algebra enters its closure through std.effect_grant, so 19 unimported-bare-provider roster
rows in 11 files no longer carry their pair; each is retired ImportsFixed, as the rule directs
(observed by the entry-route judgment; the floor re-derives every ImportsFixed row per run).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…or checks, then answers it

Lane decision (spec gunbc#12581 author) resolving the conflict between the review's routing and
spec sections 2.6 and 9.1 Q11:

- std.artifact_store artifact_store_for_ceiling(ceiling: StoreCeiling) -> ArtifactStore is the
  one construction of a store from a ceiling. It takes the sole_constructor StoreCeiling, never a
  ByteSize, and needs no CacheProvider or ProviderRetention, so L5b's commit can use it with
  artifact_store_with_occupancy without the provider door entering the R-D mirror set.
- store_over_provider_resolved keeps every check it made (scope-released, unit, at_capacity
  LRU-only, authority match) and then answers StoreReady with exactly that construction. The
  store_ready_empty helper is deleted; the pre-existing ExactLimit arm builds from the provider's
  own stated number as it did on the base.
- The leading comment of artifact_store_for_ceiling names the check the commit path relies on:
  test.claim.artifact_store_witness the_store_catalog_row_admits_exactly_the_ceiling_store, which
  runs the constant catalog row through the door. It is a declared frontier that lands in L5b with
  the row's retention: the row declares CapacityUnobserved today, truthfully, because nothing yet
  applies a ceiling to that store or evicts from it.

Witnesses (test.claim.artifact_store_witness): the_ceiling_store_is_empty_and_sized_by_its_ceiling
(the construction), the_resolved_door_answers_the_one_ceiling_construction (the door's answer
equals the construction, compared whole; replaces a_ceiling_derived_provider_is_sized_by_its_resolved_ceiling),
and the six occupancy claims now build their store the way the commit will, with
artifact_store_for_ceiling and no provider.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Sep 29, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-09-29T05:25:52.777950Z 968b4db PR opened
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant