C2: typecheck materialization through the local store

dag/gunbc/commit_workflow.dag

@@ -1553,7 +1553,8 @@ data commit_gate_roster: List<CommitCheckEnrollment> = [
       check_fns: [
         "floor_index_build_share_is_shared_by_reference",
         "floor_index_build_has_plural_readers",
-        "floor_index_build_reds_without_reference_provider"
+        "floor_index_build_reds_without_reference_provider",
+        "floor_typecheck_store_persist_reds_without_any_provider"
       ],
       kind: CorpusWitnessKind,
       span: SpanUndeclared

dag/gunbc/floor/floor_materialization.dag

@@ -154,8 +154,11 @@ data floor_typecheck_store_no_providers: List<CacheProvider> = []
 // processes. The frame is
 // UnboundedSiblingsFrame, not SharedStateFrame: recurring invocations of the fold on a runner host
 // are successive siblings with no shared mutable state to rewire, so there is no LCA process in
-// which the repetition could have been carried, and only a STORE tier can discharge it. No provider
-// does today (see the note above the no-provider verdict below).
+// which the repetition could have been carried, and only a STORE tier can discharge it.
+// floor_typecheck_store_persist_provider is the modeled STORE row; it does not discharge the
+// live ladder while typecheck_materialization_seed_path_note and
+// typecheck_store_family_budget_frontier remain unbound. Live verdicts are
+// floor_typecheck_store_persist_verdicts_without_provider.
 
 fn floor_runner_host_frame() -> std.materialization_ladder.Frame {
   std.materialization_ladder.Frame { name: "runner-host", kind: UnboundedSiblingsFrame }
@@ -194,15 +197,34 @@ fn floor_typecheck_store_cross_process_demands() -> List<FrameDemand> {
 
 data floor_typecheck_store_no_cost_floor_exemptions: List<String> = []
 
-// NO PROVIDER COVERS THESE DEMANDS (2026-10-03). The host-persisted provider that discharged them --
-// shared_typecheck_store PersistentTypedStore, armed by GUNBC_TYPED_STORE_PERSIST -- was DELETED
-// after measurement: armed, a 5-entry claim_batch run exceeded 720 s against ~150 s unarmed and
-// wrote ~7.3 GB in two entries, so its per-entry payload was a closure snapshot rather than one
-// module, and nothing bounded its root or cleaned it. The demands below are unchanged and the
-// ladder therefore REFUSES them; that refusal is the live state, not a fixture. The replacement is a
-// TypecheckModuleRequest store realized through extdeps.realization.materialization_store_local
-// with a per-module encoding, a byte ceiling with oldest-generation eviction and a scoped,
-// self-cleaning root; it re-adds the provider row here with its own green and red controls.
+// Modeled STORE row for TypecheckModuleRequest through
+// extdeps.realization.materialization_store_local. The no-provider ladder is the LIVE RED.
+// persist_verdicts with this provider is the intended discharge fold; it is not claimed as live
+// while typecheck_materialization_seed_path_note and typecheck_store_family_budget_frontier stay
+// unbound.
+
+data floor_typecheck_store_persist_provider_id: String = "materialization_store_local:typed_module"
+
+data floor_typecheck_store_persist_provider: CacheProvider = provider_row(
+  id: floor_typecheck_store_persist_provider_id,
+  scope: [floor_runner_host_frame()],
+  coverage: CoversIdentities { identities: [floor_typecheck_store_identity] },
+  tier: ArtifactTier { keying: ContentKeyed },
+  retention: persistent_retention(capacity: CapacityBounded {
+    limit: ByteCapacity { limit: ExactLimit { value: materialization_store_typed_module_budget_policy } },
+    at_capacity: ReplaceExisting { strategy: LeastRecentlyUsed }
+  })
+)
+
+data floor_typecheck_store_persist_providers: List<CacheProvider> = [floor_typecheck_store_persist_provider]
+
+fn floor_typecheck_store_persist_verdicts() -> List<LadderVerdict> {
+  materialization_ladder(
+    demands: floor_typecheck_store_cross_process_demands(),
+    providers: floor_typecheck_store_persist_providers,
+    cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
+  )
+}
 
 fn floor_typecheck_store_persist_verdicts_without_provider() -> List<LadderVerdict> {
   materialization_ladder(

dag/gunbc/materialization_store_budgets.dag

@@ -2,10 +2,19 @@ module gunbc.materialization_store_budgets
 
 import std.types { List, NonEmptyStr }
 import std.dissolution { DissolutionCondition, unbound_dissolution }
-import std.measure { ByteSize, byte_size }
+import std.measure { ByteSize, byte_size, measure_count }
 import std.cache_identity { typed_module_artifact_kind }
-import extdeps.realization.materialization_store_local { LocalStoreFamilyBudget, local_store_budget_sum, materialization_store_local_facts_at }
+import extdeps.external_authority { CitedFigureStanding, TranscribedUncited }
+import extdeps.realization.materialization_store_local {
+  LocalStoreFamilyBudget,
+  local_store_budget_sum,
+  materialization_store_local_facts_at,
+}
 import extdeps.cache.types { CacheInterfaceCatalogFacts }
+import gunbc.typed_module_cache_capacity {
+  typed_module_bytes_per_entry_estimate,
+  typed_module_cache_entries_ceiling,
+}
 
 // THE DURABLE STORE'S BUDGETS ARE POLICY, AND POLICY IS THIS LAYER'S FACT (DESIGN section 3). The
 // transport (extdeps.realization.materialization_store_local) owns the budget's shape and its
@@ -14,23 +23,44 @@ import extdeps.cache.types { CacheInterfaceCatalogFacts }
 // is structural (std.materialization_store_grant DurableHostVolumeRoot names one path), so the host
 // ceiling is the declared sum of these rows and nothing else.
 
-// POLICY, NAMED AS POLICY: 4 GiB for typed-module results per host. It is not derived from a
-// measurement -- the only measured predecessor stored closure snapshots of ~3.65 GB each, which is not
-// the per-module grain the store holds -- and its REVISION TRIGGER is the TypecheckModuleRequest
-// consumer (PR C2) measuring real per-module entries on the durable root.
-data materialization_store_typed_module_budget_policy: ByteSize = byte_size(count: 4294967296)
+// The product of per-entry unit × residency ceiling remains the family budget shape. The per-entry
+// figure is typed as a TranscribedUncited BET (DESIGN 4d): it reuses typed_module_bytes_per_entry_estimate
+// (TypeEnv-grain in-process denominator) and does not claim to be a measured
+// interface-plus-diagnostics store object. The read_obligation names the instrument that would
+// ground it. typecheck_store_family_budget_frontier stays unbound until that standing is
+// CitedToAuthority.
+
+type TypecheckStoreFamilyEntryBet {
+  bytes: ByteSize
+  standing: CitedFigureStanding
+}
+
+data typecheck_store_family_entry_size_read_obligation: NonEmptyStr = "v1_compiler.cli_run typecheck_store_session observed_largest_entry_bytes after seed_commit_typecheck_hex of TypecheckModuleRequest objects constructed on reconcile_with_typed_cache (interface_text plus diagnostics_text of the module's OWN typecheck_module_items tail, never the import-derived closure), reported on the run receipt line by typecheck_store_session store_receipt_line as largest_entry_bytes. Cite that producer; do not transcribe a count into this module."
+
+data typecheck_store_family_entry_bet: TypecheckStoreFamilyEntryBet = TypecheckStoreFamilyEntryBet {
+  bytes: typed_module_bytes_per_entry_estimate,
+  standing: TranscribedUncited { read_obligation: typecheck_store_family_entry_size_read_obligation }
+}
+
+data typecheck_store_family_budget_frontier: DissolutionCondition = unbound_dissolution(description: "TRIGGER: typecheck_store_family_entry_bet.standing is CitedToAuthority whose authority is the executing observed_largest_entry_bytes instrument on the real typecheck commit path (v1_compiler.cli_run typecheck_store_session). SUFFICIENT FOR: typecheck_module_family_entry_budget_unit is derived from that measurement rather than from this bet. Retired by that standing change and nothing else." as NonEmptyStr)
+
+fn typecheck_module_family_entry_budget_unit() -> ByteSize {
+  typecheck_store_family_entry_bet.bytes
+}
+
+data materialization_store_typed_module_budget_policy: ByteSize = byte_size(
+  count: measure_count(m: typecheck_module_family_entry_budget_unit()) * typed_module_cache_entries_ceiling
+)
 
 data materialization_store_durable_family_budgets: List<LocalStoreFamilyBudget> = [
   LocalStoreFamilyBudget { family: typed_module_artifact_kind, budget: materialization_store_typed_module_budget_policy },
 ]
 
-// The one host-wide figure: the sum of the durable root's declared family budgets.
 data materialization_store_host_ceiling_bytes: ByteSize = local_store_budget_sum(budgets: materialization_store_durable_family_budgets)
 
-// The catalog row for the store as DEPLOYED: the realization's facts at this layer's host ceiling.
 data materialization_store_local_facts: CacheInterfaceCatalogFacts = materialization_store_local_facts_at(ceiling: materialization_store_host_ceiling_bytes)
 
-// THE PRODUCTION CONSUMER IS A DECLARED FRONTIER (DESIGN section 3c): no process opens the durable
-// root in this change; the witnesses pass fixture rows of their own, and the host-ceiling control
-// reads the figure above.
-data materialization_store_durable_budgets_consumer_frontier: DissolutionCondition = unbound_dissolution(description: "TRIGGER: the TypecheckModuleRequest consumer (PR C2) opens DurableHostVolumeRoot through extdeps.realization.materialization_store_local passing materialization_store_durable_family_budgets. SUFFICIENT FOR: these rows bound a production store on every run that consumes it; until then they are read only by the host-ceiling control, and this row is retired by that landing and nothing else." as NonEmptyStr)
+// C2's production consumer is the seed typecheck path (gunbc.typecheck_module_store
+// typecheck_materialization_seed_path_note). Binding this row to a declaration that merely
+// exists would fire before any run opens the durable root.
+data materialization_store_durable_budgets_consumer_frontier: DissolutionCondition = unbound_dissolution(description: "TRIGGER: the TypecheckModuleRequest consumer (PR C2) opens DurableHostVolumeRoot through extdeps.realization.materialization_store_local passing materialization_store_durable_family_budgets from the seed typecheck path (ensure_durable_typecheck_store, lookup_typecheck_module, commit_typecheck_module). SUFFICIENT FOR: these rows bound a production store on every run that consumes it; until then they are read only by the host-ceiling control, and this row is retired by that landing and nothing else." as NonEmptyStr)