F-0: truthful namespace control plane — phase roster, NamespaceCutStage chain, deletion-subject roster, derived wave-wall enrolment

dag/gunbc/fabric/fabric_witness_run.dag

@@ -18,6 +18,7 @@ import product.fabric.work {
   work_for,
 }
 import std.content_hash { ContentHash, content_hash_of_value, serialize_content_hash }
+import gunbc.required_ci_phase_roster { BuildLane, WitnessesLane, required_ci_lane_name }
 import extdeps.git.object_store { GitObjectId, git_object_id_wire_hex, git_object_id_content_hash, git_sha1_object_id }
 import product.fabric.supply {
   SupplierOffer, OfferFungibility, DemandOfferAffordability, GrantDuration, EstimatedGrantDuration,
@@ -547,9 +548,12 @@ fn required_ci_lane_command(lane: String) -> ArgvCommand {
   )
 }
 
-data required_ci_lane_build: String = "build"
+// THE LANE WORDS ARE THE ROSTER'S, NOT THIS MODULE'S. gunbc.required_ci_phase_roster owns lane
+// identity and the phase-to-lane partition; these two datas survive as the join point every
+// existing consumer already names, derived from that single authority rather than restating it.
+data required_ci_lane_build: String = required_ci_lane_name(l: BuildLane)
 
-data required_ci_lane_witnesses: String = "witnesses"
+data required_ci_lane_witnesses: String = required_ci_lane_name(l: WitnessesLane)
 
 // The witnesses lane: the .dag parse sweep and the witness floor fold. Named for its lane
 // rather than for the floor alone, because the parse phase rides here too and a name that

dag/gunbc/namespace/namespace_cut_stage.dag

@@ -0,0 +1,168 @@
+module gunbc.namespace_cut_stage
+
+import std.types { String, NonEmptyStr, Bool, List }
+import gunbc.compiler_frontend_program_interlock {
+  ProgramMilestone,
+  SelfHostRatchetGateEnrolled,
+  NamespaceWaveAdmissionEnrolled,
+  NamespaceBaselineObservationComplete,
+}
+
+// THE NAMESPACE-XL SERIAL CHAIN, AS A CLOSED VARIANT WITH A TOTAL PREREQUISITE FUNCTION.
+// This is the namespace cut's own stage grain -- finer than the interlock's ProgramMilestone rows
+// and NOT a second spelling of them: the interlock braids the namespace program against self-host
+// at milestone grain, while this chain sequences the cut's own execution. The two join where the
+// operator ruled they join (stage_milestone_prerequisites below), and nowhere else.
+//
+// NAMING: these stages are the NAMESPACE-XL chain. An unrelated self-host chain also spells its
+// work items XL-N (gunbc#9669/#9672-#9675); the variants here are namespaced (StageXL5Waves, not
+// XL5) so the two vocabularies cannot collide in one corpus.
+//
+// The same construction rule as milestone_prerequisites applies and is restated because it is the
+// whole point of the carrier: prerequisites are a TOTAL function over a CLOSED variant, so a newly
+// declared stage refuses to compile until its prerequisites are stated -- an unstated-prerequisite
+// stage is unwritable rather than checked. And the standing obligation the interlock records
+// transfers with it: before adding a variant, ask whether it carries two facts that would state
+// different prerequisites if separated; if it does, it is two variants.
+type NamespaceCutStage
+  = StageF0
+  | StageXL0Denominator
+  | StageXL1BaselineCapture
+  | StageXL2RootDeletionRehearsal
+  | StageXL3DeclaringIdentitySpelling
+  | StageXL4ReferenceDerivedGraph
+  | StageAct0ActivationGate
+  | StageXL5Waves
+  | StageXL6AtomicCutover
+  | StageXL7GrammarDeletion
+
+fn namespace_cut_stage_label(s: NamespaceCutStage) -> NonEmptyStr {
+  match s {
+    StageF0 => "F-0: truthful namespace control plane -- stage chain, subject roster, derived wave-wall enrolment" as NonEmptyStr
+    StageXL0Denominator => "XL-0: the denominator -- every authority scheduled to disappear, enumerated at stable identity grain with an executable observation rule" as NonEmptyStr
+    StageXL1BaselineCapture => "XL-1: complete baseline capture -- what the legacy resolver actually selected over one exact base, persisted before anything is deleted" as NonEmptyStr
+    StageXL2RootDeletionRehearsal => "XL-2: root-deletion rehearsal -- the cut executed in a throwaway tree, its failure roster captured as the census" as NonEmptyStr
+    StageXL3DeclaringIdentitySpelling => "XL-3: declaring-identity spelling -- every reference spelled as the fully qualified declaring identity" as NonEmptyStr
+    StageXL4ReferenceDerivedGraph => "XL-4: reference-derived graph -- dependency edges derived from resolved reference targets, never declared" as NonEmptyStr
+    StageAct0ActivationGate => "ACT-0: activation gate -- the manager pins activation base B, re-executes XL-0/XL-1/XL-2/XL-4 on B, and records immutable digests; a manager gate, not an implementation stage" as NonEmptyStr
+    StageXL5Waves => "XL-5: the semantic waves -- subject deletions land under the wave-admission wall, class by class" as NonEmptyStr
+    StageXL6AtomicCutover => "XL-6: atomic cutover -- the authority transition lands in one motion" as NonEmptyStr
+    StageXL7GrammarDeletion => "XL-7: grammar deletion, LAST -- import becomes a typed, located parse error (gunbc.namespace_cut_landing_order namespace_cut_grammar_last_ruling)" as NonEmptyStr
+  }
+}
+
+// DIRECT EDGES ONLY; the closure is derived, never restated. The chain is serial by operator
+// design -- each stage's evidence is an input to the next -- so each row names its predecessor
+// and nothing else. StageXL7GrammarDeletion last realizes the grammar-last ruling structurally:
+// its position in this chain is DERIVED from these edges, and a reordering is an edit to exactly
+// one row rather than a prose migration.
+fn stage_prerequisites(s: NamespaceCutStage) -> List<NamespaceCutStage> {
+  match s {
+    StageF0 => []
+    StageXL0Denominator => [StageF0]
+    StageXL1BaselineCapture => [StageXL0Denominator]
+    StageXL2RootDeletionRehearsal => [StageXL1BaselineCapture]
+    StageXL3DeclaringIdentitySpelling => [StageXL2RootDeletionRehearsal]
+    StageXL4ReferenceDerivedGraph => [StageXL3DeclaringIdentitySpelling]
+    StageAct0ActivationGate => [StageXL4ReferenceDerivedGraph]
+    StageXL5Waves => [StageAct0ActivationGate]
+    StageXL6AtomicCutover => [StageXL5Waves]
+    StageXL7GrammarDeletion => [StageXL6AtomicCutover]
+  }
+}
+
+// WHERE THE CHAIN JOINS THE INTERLOCK, and only there. The operator ruling that shaped ACT-0
+// gates activation on the interlock triple by name; every other stage's cross-program
+// obligations arrive transitively through the chain rather than being restated per stage
+// (direct edges, derived closure -- the same rule as above, applied across the join).
+fn stage_milestone_prerequisites(s: NamespaceCutStage) -> List<ProgramMilestone> {
+  match s {
+    StageF0 => []
+    StageXL0Denominator => []
+    StageXL1BaselineCapture => []
+    StageXL2RootDeletionRehearsal => []
+    StageXL3DeclaringIdentitySpelling => []
+    StageXL4ReferenceDerivedGraph => []
+    StageAct0ActivationGate => [SelfHostRatchetGateEnrolled, NamespaceWaveAdmissionEnrolled, NamespaceBaselineObservationComplete]
+    StageXL5Waves => []
+    StageXL6AtomicCutover => []
+    StageXL7GrammarDeletion => []
+  }
+}
+
+data namespace_cut_stages: List<NamespaceCutStage> = [
+  StageF0,
+  StageXL0Denominator,
+  StageXL1BaselineCapture,
+  StageXL2RootDeletionRehearsal,
+  StageXL3DeclaringIdentitySpelling,
+  StageXL4ReferenceDerivedGraph,
+  StageAct0ActivationGate,
+  StageXL5Waves,
+  StageXL6AtomicCutover,
+  StageXL7GrammarDeletion,
+]
+
+fn namespace_cut_stage_is(a: NamespaceCutStage, b: NamespaceCutStage) -> Bool {
+  (namespace_cut_stage_label(s: a) as String) == (namespace_cut_stage_label(s: b) as String)
+}
+
+// ---------------------------------------------------------------------------------------------
+// ACT-0'S POPULATION: THE RECEIPTS THE GATE MUST HOLD. The activation gate is not a deletion
+// stage and carries no subjects; its standing is derived from whether each required receipt is
+// held against the pinned activation base. The receipt kinds are closed so the gate's
+// denominator is a total fold, and the held-roster below is the SINGLE home a receipt lands in
+// -- reading it empty is an observation of the carrier, not a guess about the world.
+//
+// RE-RUN, NEVER UPDATE: any source-relevant movement of main invalidates a pinned base, so a
+// stale receipt is retired by deleting its row and re-running the producing stage against the
+// new base. A receipt row is immutable once written; there is no arm for amending one.
+// ---------------------------------------------------------------------------------------------
+type ActivationReceiptKind
+  = DenominatorRosterDigest
+  | BaselineCaptureReceipt
+  | RehearsalFailureRosterDigest
+  | ReferenceGraphDigest
+
+fn activation_receipt_kind_label(k: ActivationReceiptKind) -> String {
+  match k {
+    DenominatorRosterDigest => "XL-0 denominator roster digest over the activation base"
+    BaselineCaptureReceipt => "XL-1 baseline capture receipt over the activation base"
+    RehearsalFailureRosterDigest => "XL-2 rehearsal failure-roster digest over the activation base"
+    ReferenceGraphDigest => "XL-4 reference-graph digest over the activation base"
+  }
+}
+
+type ActivationReceipt {
+  kind: ActivationReceiptKind
+  activation_base_commit: NonEmptyStr
+  digest: NonEmptyStr
+}
+
+data required_activation_receipt_kinds: List<ActivationReceiptKind> = [
+  DenominatorRosterDigest,
+  BaselineCaptureReceipt,
+  RehearsalFailureRosterDigest,
+  ReferenceGraphDigest,
+]
+
+// Empty by construction today: no activation base has been pinned. A row lands here only when
+// the manager executes ACT-0.
+data held_activation_receipts: List<ActivationReceipt> = []
+
+// The gate's outstanding population, at receipt-kind identity grain: every required kind not
+// held. Parameterized on the held roster so a witness can author both the complete and the
+// incomplete population (the fixture boundary is the boundary that decides, DESIGN 4b).
+fn activation_receipts_outstanding(held: List<ActivationReceipt>) -> List<String> {
+  required_activation_receipt_kinds
+    |> filter(k => !any(held, r => activation_receipt_kind_label(k: r.kind) == activation_receipt_kind_label(k: k)))
+    |> map(k => activation_receipt_kind_label(k: k))
+}
+
+// One kind's outstanding view, for the stage whose deliverable produces exactly that receipt:
+// XL-2 owns the rehearsal digest and XL-4 the reference-graph digest, so each stage's standing
+// reads its own receipt out of the shared gate carrier rather than minting a parallel one.
+fn activation_receipt_kind_outstanding(kind: ActivationReceiptKind, held: List<ActivationReceipt>) -> List<String> {
+  activation_receipts_outstanding(held: held)
+    |> filter(label => label == activation_receipt_kind_label(k: kind))
+}

dag/gunbc/namespace/namespace_cut_subject_observation.dag

@@ -0,0 +1,179 @@
+module gunbc.namespace_cut_subject_observation
+
+import std.types { String, NonEmptyStr, Bool, List }
+import std.process { ProcessExit, ExitSuccess, exit_failure }
+import extdeps.filesystem.filesystem_io { Filesystem }
+import std.decl_ref { DeclarationRef, decl_ref, decl_field_ref }
+import v2.std.decl_index { DeclFact, decl_facts }
+import v2.lens.module_graph { ModuleDeclarationFact, module_declaration_facts_live }
+import v2.std.decl_ref_resolution {
+  DeclarationRefResolution,
+  DeclarationRefResolved,
+  DeclarationRefModuleAbsent,
+  DeclarationRefDeclarationAbsent,
+  DeclarationRefFieldAbsent,
+  DeclarationRefAmbiguous,
+  resolve_declaration_ref,
+}
+import gunbc.namespace_cut_stage { namespace_cut_stage_label }
+import gunbc.namespace_cut_subject_roster {
+  NamespaceCutSubjectIdentity,
+  NamespaceCutSubjectProbe,
+  DagDeclarationProbe,
+  DagDeclarationFieldProbe,
+  HostRustItemProbe,
+  namespace_cut_subjects,
+  namespace_cut_subject_label,
+  subject_probe_list,
+  subject_deleted_at_stage,
+  probe_render,
+}
+
+// THE LIVE HALF OF THE SUBJECT ROSTER, SPLIT FROM THE PURE HALF ON PURPOSE. The roster module
+// carries only identities and joins, so a consumer (the program-standing report, a witness) can
+// import it without its loader closure reaching live-read code -- the same pure/live split the
+// lens-enforcement gate note names as the repair shape for module_graph. This module is the
+// live-read carrier home (v2.std.live_read live_read_carrier_homes_v0) and holds every
+// observation that touches the tree.
+
+// ---------------------------------------------------------------------------------------------
+// OBSERVATION. Three answers, because two media and a refusal are three states:
+//  - SubjectProbePresent / SubjectProbeAbsent: decided by runtime declaration-ref resolution
+//    over the reflection facts this module reads.
+//  - SubjectProbeUnobservable: the honest arm. Host Rust items have no observation instrument in
+//    this tree, and an ambiguous resolution is a corpus defect this roster must surface rather
+//    than adjudicate. Neither is Present and neither is Absent, and folding either into a
+//    verdict would be the empty-observation narrow. NEXT-RUNG TRIGGER for the host half: a Rust
+//    item observation authority (a modeled host-item census at item-identity grain) reaching
+//    this roster, at which point HostRustItemProbe resolves like its substrate sibling and the
+//    unobservable arm shrinks to the ambiguity case.
+// ---------------------------------------------------------------------------------------------
+type SubjectProbeObservation
+  = SubjectProbePresent { probe: NamespaceCutSubjectProbe }
+  | SubjectProbeAbsent { probe: NamespaceCutSubjectProbe }
+  | SubjectProbeUnobservable { probe: NamespaceCutSubjectProbe, why: String }
+
+fn probe_ref(p: NamespaceCutSubjectProbe) -> DeclarationRef {
+  match p {
+    DagDeclarationProbe { module_path, decl_name } =>
+      decl_ref(module_path: module_path, decl_name: decl_name)
+    DagDeclarationFieldProbe { module_path, decl_name, field_name } =>
+      decl_field_ref(module_path: module_path, decl_name: decl_name, field_name: field_name)
+    HostRustItemProbe { crate_relative_file, item_name } =>
+      decl_ref(module_path: crate_relative_file, decl_name: item_name)
+  }
+}
+
+
+fn observe_probe(
+  p: NamespaceCutSubjectProbe,
+  facts: List<DeclFact>,
+  modules: List<ModuleDeclarationFact>
+) -> SubjectProbeObservation {
+  match p {
+    HostRustItemProbe { crate_relative_file: _, item_name: _ } =>
+      SubjectProbeUnobservable {
+        probe: p,
+        why: "host Rust item: no item-grain observation authority exists in this tree yet; refusing to fabricate Present or Absent",
+      }
+    DagDeclarationProbe { module_path: _, decl_name: _ } =>
+      observation_from_resolution(p: p, r: resolve_declaration_ref(ref: probe_ref(p: p), facts: facts, modules: modules))
+    DagDeclarationFieldProbe { module_path: _, decl_name: _, field_name: _ } =>
+      observation_from_resolution(p: p, r: resolve_declaration_ref(ref: probe_ref(p: p), facts: facts, modules: modules))
+  }
+}
+
+// A MODULE GONE IS THE SUBJECT GONE. DeclarationRefModuleAbsent maps to Absent rather than to a
+// refusal because deleting a whole module is a legitimate terminal state for a deletion subject
+// -- what must NOT map to Absent is ambiguity, which is two declarations answering one identity
+// and is reported under its own name.
+fn observation_from_resolution(
+  p: NamespaceCutSubjectProbe,
+  r: DeclarationRefResolution
+) -> SubjectProbeObservation {
+  match r {
+    DeclarationRefResolved { declaration_identity: _ } => SubjectProbePresent { probe: p }
+    DeclarationRefModuleAbsent { reference: _ } => SubjectProbeAbsent { probe: p }
+    DeclarationRefDeclarationAbsent { reference: _ } => SubjectProbeAbsent { probe: p }
+    DeclarationRefFieldAbsent { reference: _ } => SubjectProbeAbsent { probe: p }
+    DeclarationRefAmbiguous { reference: _, candidates: _ } =>
+      SubjectProbeUnobservable { probe: p, why: "ambiguous: more than one declaration answers this identity" }
+  }
+}
+
+fn observation_render(o: SubjectProbeObservation) -> String {
+  match o {
+    SubjectProbePresent { probe } => concat("PRESENT      ", probe_render(p: probe))
+    SubjectProbeAbsent { probe } => concat("ABSENT       ", probe_render(p: probe))
+    SubjectProbeUnobservable { probe, why } =>
+      concat("UNOBSERVABLE ", concat(probe_render(p: probe), concat(" -- ", why)))
+  }
+}
+
+
+// ---------------------------------------------------------------------------------------------
+// THE RUNNABLE INSTRUMENT. One live acquisition, every probe resolved against it, one written
+// report -- the producer a reader re-runs instead of quoting:
+//
+//   gunbc run --source-root dag --source-root src/v2 \
+//     --entry dag/gunbc/namespace/namespace_cut_subject_observation.dag \
+//     --function subject_roster_report --arg out=/tmp/namespace-cut-subjects.txt
+//
+// This module is a live-read carrier for exactly this entry (decl_facts +
+// module_declaration_facts_live) and is enrolled in v2.std.live_read live_read_carrier_homes_v0.
+// The FACT pool roots (per-root, below) deliberately include src/v1: most deletion subjects
+// live in the seed's .dag corpus, and a walk that omitted it would report the cut complete
+// while the seed still resolves imports -- the false Absent this instrument must not be able to
+// produce. src/v1 is NOT a --source-root of the entry: the seed corpus is a SUBJECT the
+// reflection walk reads, never a module pool this module executes from.
+// ---------------------------------------------------------------------------------------------
+// ONE ACQUISITION PER ROOT, NOT ONE UNION. decl_facts retains a Node per declaration, so a
+// union walk over the seed plus the v2 corpus held both node populations resident at once and
+// was SIGKILLed on a memory-tight host (measured 2026-08-29, remote runner, ~14min then kill).
+// Every dag-grain probe names a module under exactly one root, so the report acquires each
+// root's facts separately and resolves each probe against its own root -- halving the peak and
+// keeping the false-Absent property: a v1 probe is still resolved against a walk that includes
+// src/v1.
+data subject_roster_v1_pool_roots: List<String> = ["src/v1"]
+data subject_roster_v2_pool_roots: List<String> = ["src/v2"]
+
+fn probe_is_v1(p: NamespaceCutSubjectProbe) -> Bool {
+  match p {
+    DagDeclarationProbe { module_path, decl_name: _ } => starts_with(s: module_path, prefix: "v1.")
+    DagDeclarationFieldProbe { module_path, decl_name: _, field_name: _ } => starts_with(s: module_path, prefix: "v1.")
+    HostRustItemProbe { crate_relative_file: _, item_name: _ } => false
+  }
+}
+
+fn subject_report_lines() -> List<String> {
+  let v1_facts = decl_facts(pool_roots: subject_roster_v1_pool_roots)
+  let v1_modules = module_declaration_facts_live(pool_roots: subject_roster_v1_pool_roots)
+  let v2_facts = decl_facts(pool_roots: subject_roster_v2_pool_roots)
+  let v2_modules = module_declaration_facts_live(pool_roots: subject_roster_v2_pool_roots)
+  namespace_cut_subjects
+    |> flat_map(s => concat(
+      [concat("subject: ", concat(namespace_cut_subject_label(s: s) as String, concat(" -- deleted at ", namespace_cut_stage_label(s: subject_deleted_at_stage(s: s)) as String)))],
+      subject_probe_list(s: s)
+        |> map(p => concat("  ",
+          if probe_is_v1(p: p) {
+            observation_render(o: observe_probe(p: p, facts: v1_facts, modules: v1_modules))
+          } else {
+            observation_render(o: observe_probe(p: p, facts: v2_facts, modules: v2_modules))
+          }))
+    ))
+}
+
+fn subject_roster_report(out: String) -> ProcessExit {
+  if out == "" {
+    exit_failure(reason: "subject_roster_report: --arg out=<path> is required -- the roster is written, not printed")
+  } else {
+    let body = fold(subject_report_lines(), init: "namespace cut subject roster -- observed\n\n", f: fn(acc, line) {
+      concat(acc, concat(line, "\n"))
+    })
+    if Filesystem.Write(path: out, content: body).success {
+      ExitSuccess
+    } else {
+      exit_failure(reason: concat("subject_roster_report: derived and could not be written to ", out))
+    }
+  }
+}