diff --git a/dag/gunbc/compiler_frontend_program_status.dag b/dag/gunbc/compiler_frontend_program_status.dag index 9b7e612f706..588013aff91 100644 --- a/dag/gunbc/compiler_frontend_program_status.dag +++ b/dag/gunbc/compiler_frontend_program_status.dag @@ -34,6 +34,42 @@ import v2.workflow.legacy_baseline_capture { CaptureAvailable, CaptureBlocked, legacy_baseline_capture_capability, + capture_blocked_reason, +} +import gunbc.required_ci_phase_roster { + RequiredCiPhase, + NamespaceWaveAdmissionPhase, + required_ci_phases, + required_ci_phase_enrolled, +} +import gunbc.namespace_cut_stage { + NamespaceCutStage, + StageF0, + StageXL0Denominator, + StageXL1BaselineCapture, + StageXL2RootDeletionRehearsal, + StageXL3DeclaringIdentitySpelling, + StageXL4ReferenceDerivedGraph, + StageAct0ActivationGate, + StageXL5Waves, + StageXL6AtomicCutover, + StageXL7GrammarDeletion, + namespace_cut_stages, + namespace_cut_stage_label, + stage_prerequisites, + stage_milestone_prerequisites, + ActivationReceiptKind, + RehearsalFailureRosterDigest, + ReferenceGraphDigest, + activation_receipt_kind_outstanding, + activation_receipts_outstanding, + held_activation_receipts, +} +import gunbc.namespace_cut_subject_roster { + subjects_deleted_at, + subject_probe_list, + probe_render, + unobservable_probe_renders, } // WHY THIS IS A SEPARATE MODULE FROM THE INTERLOCK IT READS. The interlock carries a RELATION -- @@ -109,24 +145,32 @@ fn observe_outstanding(subject: NonEmptyStr, outstanding: List) -> Miles // module computes even now that it keeps them. // That distinction is invisible on a ledger, which renders every such row as "pending" and invites // a reader to hear "in progress". +// THREE ROWS RETIRED BY DELIVERY, ONE SPLIT, ONE ADDED (F-0, 2026-08-29). RequiredCiPhaseRoster, +// NamespaceWaveAdmissionWall and NamespaceStepSubjectRoster are DELETED because the instruments +// now exist -- gunbc.required_ci_phase_roster, the wave-admission phase it enrols (landed #9365 +// and until now still reported here as unbuilt: this carrier's own stale reading was the rung +// inflation in the opposite direction, a built wall reported absent), and +// gunbc.namespace_cut_subject_roster. Their awaiting milestones are now DERIVED from those +// carriers below. What SelfHostCargoPhaseEnrolled still awaits is narrower than the roster and +// gets its own row: the roster carries phase identity and lane, not whether a phase executes +// cargo. DeclaringIdentitySpellingCensus is awaited by the stage chain (XL-3), not by any +// milestone -- stages_awaiting joins it. type MissingInstrument = WholeCorpusEmissionBoard - | RequiredCiPhaseRoster + | PhaseCargoExecutionFact | RatchetGateEnrolmentFact - | NamespaceWaveAdmissionWall | PersistedLegacyBaselineObservation - | NamespaceStepSubjectRoster + | DeclaringIdentitySpellingCensus | PersistedBehavioralReceipt | PersistedPromotionOutcome fn missing_instrument_label(i: MissingInstrument) -> String { match i { WholeCorpusEmissionBoard => "a persisted whole-corpus emission measurement at identity grain" - RequiredCiPhaseRoster => "the --required-ci phase roster as a substrate carrier" + PhaseCargoExecutionFact => "a per-phase cargo-execution fact on gunbc.required_ci_phase_roster" RatchetGateEnrolmentFact => "the ratchet's merge-blocking enrolment as a fact distinct from its cadence" - NamespaceWaveAdmissionWall => "the wave-admission wall, classifying deltas" PersistedLegacyBaselineObservation => "an admitted CompleteLegacyObservation persisted against a named base" - NamespaceStepSubjectRoster => "the namespace cut's remaining per-step subjects as rows" + DeclaringIdentitySpellingCensus => "a census of occurrences not spelled at their declaring identity (XL-3's population)" PersistedBehavioralReceipt => "a persisted behavioral receipt over a discriminating corpus" PersistedPromotionOutcome => "a persisted PromotionOutcome over a named candidate" } @@ -204,11 +248,10 @@ fn missing_instrument_obstacle(i: MissingInstrument) -> InstrumentObstacle { ), falsified_by: "THE REFUSAL THIS ARM USED TO CARRY HAS BEEN FALSIFIED BY EXECUTION, on exactly the terms it demanded. It said the predicate is a function of the HOST, that it had refused on the hosts its receipts were taken on, that it had NOT been attempted on one whose budget it admits, and that the falsification must record EXIT STATUS AND PEAK RESIDENT SET TOGETHER because a SIGKILL and a clean empty population are the same bytes.\n\nAttempted 2026-08-28 on srv1 (502 GiB total, ~334 GiB available, aarch64 -- a host the predicate admits by three orders of magnitude), three whole-corpus runs under /usr/bin/time -v with the exit status captured beside the peak: --target dag EXIT=1 peak 13008052 kB wall 25:04; --target rust EXIT=1 peak 13005964 kB wall 27:44; --target rust with the parameter-default gate cleared EXIT=1 peak 12986524 kB wall 25:05. NONE was SIGKILLed and NONE was refused by admission -- each ran frontend, normalize and reconcile and reached emit, then refused on DIAGNOSTICS. So the compile is not memory-refused on an admitting host, and the sentence three milestones were waiting on is answered.\n\nWHAT IS STILL MISSING IS THE BOARD, AND THAT IS WHY THIS IS STILL A NOT-BUILT. No completing whole-corpus run has been obtained on the rust route: clearing the three parameter-default sites revealed EIGHT anonymous-record refusals behind them, reproducing the three-then-eight prefix gunbc.emit_stage_blocking_population_census already records, so the blocking population is still unbounded. And no typed measurement is persisted anywhere a consumer can read, which is the condition milestone_status states in its own words. The remedy is now to WRITE THE INSTRUMENT AND ITS CARRIER -- two constructions, not one -- rather than to find a bigger machine.\n\nWHY THE OLD REFUSAL TEXT IS DELETED RATHER THAN KEPT BESIDE THIS. It argued that the instrument is not unbuilt and that the remedy is not to write a tool. Both halves are now false, and a superseded explanation retained next to its refutation is two accounts of one fact (DESIGN section 3). Its two corrections -- the routing story and the wall-clock authority substitution -- are preserved in this type's header, because those were lessons about how the row went wrong rather than claims about the compile." as NonEmptyStr } - RequiredCiPhaseRoster => NotBuilt + PhaseCargoExecutionFact => NotBuilt RatchetGateEnrolmentFact => NotBuilt - NamespaceWaveAdmissionWall => NotBuilt PersistedLegacyBaselineObservation => NotBuilt - NamespaceStepSubjectRoster => NotBuilt + DeclaringIdentitySpellingCensus => NotBuilt PersistedBehavioralReceipt => NotBuilt PersistedPromotionOutcome => NotBuilt } @@ -323,6 +366,54 @@ fn ratchet_observation_outstanding(cadence: WitnessConsumerCadence) -> List) -> List { + if required_ci_phase_enrolled(p: NamespaceWaveAdmissionPhase, phases: phases) { + [] + } else { + ["gunbc.required_ci_phase_roster required_ci_phases does not enrol the namespace-wave-admission phase"] + } +} + +// The declared deletion subjects of one stage, at probe-identity grain. +fn stage_subject_outstanding(stage: NamespaceCutStage) -> List { + subjects_deleted_at(stage: stage) + |> flat_map(s => subject_probe_list(s: s)) + |> map(p => probe_render(p: p)) +} + +// DEFINITIONAL SINCE F-0, AND THE PREVIOUS ARM WAS THIS CARRIER'S OWN STALE READING: the wall +// landed as the required namespace-wave-admission phase in #9365 (2026-08-26) and this arm +// kept reporting it unbuilt -- rung DEFLATION, which is the same defect as inflation because a +// manager planning against it dispatches work that is already done. The population is +// membership of the phase in gunbc.required_ci_phase_roster required_ci_phases -- the roster +// the workflow emission consumes -- and the reading cannot silently outrun the executor, +// because every --required-ci run joins the host phase enum against that declaration's +// variant set in both directions and refuses on any divergence. Enrolment truth survives a +// lane divergence by construction: both lanes run in every required CI, so lane ownership can +// move a phase between jobs but cannot un-enrol it. +// THE BLOCKED ARM IS OUTSTANDING, NOT NOT-DERIVABLE, since F-0: the capability fold IS the +// milestone's readable population while a capture cannot complete -- each blocked reason is a +// named, observed piece of outstanding work, and reporting it unanswerable hid real known +// work behind the missing-instrument label. The AVAILABLE arm stays NotDerivable on purpose: +// v2.workflow.legacy_baseline_capture rules out a receipts roster in its own words (a plain +// row is not a relabel-safe durable form, and the question is re-asked per base), so once a +// capture CAN complete, whether one HAS completed against the CURRENT base has no population +// here until the persisted-observation instrument exists. +// THE THREE DELETION MILESTONES, DERIVED FROM THE SUBJECT ROSTER SINCE F-0 -- at DECLARED-ROW +// grain, stated at exactly that strength. gunbc.namespace_cut_subject_roster carries every +// authority scheduled to disappear as string-identity probes (not authored citations, which +// would refuse at ingestion the moment a wave deletes a target -- the old absence-is-not-a- +// population limit, solved by moving resolution to run time). The outstanding population is +// the probe identities of the subjects each stage deletes; a wave retires a row WITH ITS +// TYPED DISPOSITION as it deletes the subject, so Clear is reached by row retirement. What +// this fold does NOT verify is that a retired row's declarations are really gone -- that +// verification is the roster's own live observation instrument +// (gunbc.namespace_cut_subject_observation subject_roster_report), which resolves every probe +// against the tree and reports PRESENT/ABSENT/UNOBSERVABLE per identity. Rung: mechanically +// preventable at best, and only while that instrument executes; a row pruned without its +// subject dying is invisible to this fold alone. fn milestone_status(m: ProgramMilestone) -> MilestoneStanding { match m { SelfHostWholeCorpusPopulationDerived => @@ -332,8 +423,8 @@ fn milestone_status(m: ProgramMilestone) -> MilestoneStanding { } SelfHostCargoPhaseEnrolled => NotDerivable { - why: "the --required-ci phase roster lives in host Rust (RequiredCiPhase) and gunbc.witness_floor_workflow models LANES, not phases, so no .dag authority states which phases a lane owns. Derivable once the phase roster is a substrate carrier the workflow emission reads." as NonEmptyStr, - cause: needs(i: RequiredCiPhaseRoster) + why: "gunbc.required_ci_phase_roster now carries phase identity and lane ownership, but WHETHER A PHASE EXECUTES CARGO is a fact about its host body that the roster does not model, and deriving this milestone from mere phase existence would let any phase's enrolment read as the cargo phase's. Derivable once the roster carries a per-phase cargo-execution fact." as NonEmptyStr, + cause: needs(i: PhaseCargoExecutionFact) } SelfHostRatchetObservationEnrolled => standing_from_evidence( @@ -348,38 +439,48 @@ fn milestone_status(m: ProgramMilestone) -> MilestoneStanding { cause: MissingInstruments { first: WholeCorpusEmissionBoard, rest: [RatchetGateEnrolmentFact] } } NamespaceWaveAdmissionEnrolled => - NotDerivable { - why: "the wave-admission wall does not exist yet, so there is nothing to cite. gunbc.compiler_frontend_program_interlock records the admission partition as prose precisely because a partition with no consumer is a guess. Derivable once the wall exists and classifies deltas, at which point its unadjudicated-delta population is this milestone's own." as NonEmptyStr, - cause: needs(i: NamespaceWaveAdmissionWall) - } + standing_from_evidence( + e: observe_outstanding( + subject: "namespace: the wave-admission wall enrolled as a required-ci phase" as NonEmptyStr, + outstanding: wave_admission_enrolment_outstanding(phases: required_ci_phases) + ) + ) NamespaceBaselineObservationComplete => match legacy_baseline_capture_capability() { - CaptureBlocked { phase: _, cause: _ } => - NotDerivable { - why: "v2.workflow.legacy_baseline_capture can PROVE a binding observation was taken during the materialization of a named commit -- head, worktree and subject are checked in order and refuse before promotion -- but its accepted arm is unreachable while R_X(B) has no admission envelope. A complete BINDING observation must not stand in for a complete REPAIR observation. Derivable once the repair census carries an independent denominator and a capture can complete." as NonEmptyStr, - cause: needs(i: PersistedLegacyBaselineObservation) - } + CaptureBlocked { phase: p, cause: c } => + standing_from_evidence( + e: observe_outstanding( + subject: "namespace Step 0.5 / XL-1: baseline capture against the current pre-cut base" as NonEmptyStr, + outstanding: capture_blocked_reason(c: CaptureBlocked { phase: p, cause: c }) + ) + ) CaptureAvailable => NotDerivable { - why: "a capture can now complete, but no capture has been taken against the current pre-cut base. Any movement of that base invalidates a prior enrolment, so this is asked per base rather than accumulated." as NonEmptyStr, + why: "a capture can now complete, but no capture has been taken against the current pre-cut base. Any movement of that base invalidates a prior enrolment, so this is asked per base rather than accumulated -- and the capture module itself rules out a receipts roster as a relabel-unsafe durable form." as NonEmptyStr, cause: needs(i: PersistedLegacyBaselineObservation) } } NamespaceFirstSemanticWave => - NotDerivable { - why: "the milestone is the DELETION of the import-name universe, and absence of a symbol is not a population this module can read -- a citation to a deleted declaration refuses at ingestion rather than answering false. Derivable once gunbc.namespace_cut_landing_order carries the remaining per-step subject population as rows." as NonEmptyStr, - cause: needs(i: NamespaceStepSubjectRoster) - } + standing_from_evidence( + e: observe_outstanding( + subject: "namespace: first semantic wave -- the import-name universe subjects, deleted under the wall" as NonEmptyStr, + outstanding: stage_subject_outstanding(stage: StageXL5Waves) + ) + ) NamespaceFixForwardComplete => - NotDerivable { - why: "same shape as the first wave: Steps 2-4 are fix-forward over a class-grain population that no carrier enumerates. Derivable once the unrepaired classes are rows rather than a description." as NonEmptyStr, - cause: needs(i: NamespaceStepSubjectRoster) - } + standing_from_evidence( + e: observe_outstanding( + subject: "namespace: host/emit machinery, repoints and fix-forward subjects" as NonEmptyStr, + outstanding: stage_subject_outstanding(stage: StageXL6AtomicCutover) + ) + ) NamespaceGrammarRetired => - NotDerivable { - why: "the milestone is a grammar and parse deletion, and the same absence-is-not-a-population limit applies. Derivable once the grammar productions scheduled for deletion are an enumerated roster whose members refuse when they stop being reachable." as NonEmptyStr, - cause: needs(i: NamespaceStepSubjectRoster) - } + standing_from_evidence( + e: observe_outstanding( + subject: "namespace: grammar and parse deletion subjects, LAST" as NonEmptyStr, + outstanding: stage_subject_outstanding(stage: StageXL7GrammarDeletion) + ) + ) SelfHostCorpusEmitsCleanly => NotDerivable { why: "this is S2's population driven to zero, and S2 has no producer. Any figure quoted for the current rustc population today is unsourced -- the 2026-08-24 measurement bankruptcy deleted the boards and the instrument was restored without one. Derivable exactly when S2 is." as NonEmptyStr, @@ -575,11 +676,10 @@ fn join_names(names: List) -> String { // --------------------------------------------------------------------------------------------- data all_missing_instruments: List = [ WholeCorpusEmissionBoard, - RequiredCiPhaseRoster, + PhaseCargoExecutionFact, RatchetGateEnrolmentFact, - NamespaceWaveAdmissionWall, PersistedLegacyBaselineObservation, - NamespaceStepSubjectRoster, + DeclaringIdentitySpellingCensus, PersistedBehavioralReceipt, PersistedPromotionOutcome, ] @@ -596,6 +696,17 @@ fn milestone_missing_instruments(m: ProgramMilestone) -> List } } +// AN INSTRUMENT CAN BE AWAITED CONDITIONALLY: PersistedLegacyBaselineObservation is the +// CaptureAvailable arm's contract on NamespaceBaselineObservationComplete, and while capture is +// BLOCKED that arm is not live, so the awaited-by join over live standings counts it zero. Zero +// here is not death -- deleting the row would delete the very contract the capability's +// transition lands on -- so the conditional citation is declared once, and the liveness witness +// admits exactly this roster's members beside the live join. A row in this list whose citing +// arm is deleted outright IS dead, and pruning it means editing both the arm and this row. +data conditionally_awaited_instruments: List = [ + PersistedLegacyBaselineObservation, +] + fn milestones_awaiting(i: MissingInstrument) -> List { fold(program_milestones, init: [], f: fn(acc, m) { if any(milestone_missing_instruments(m: m), other => missing_instrument_eq(a: other, b: i)) { @@ -653,6 +764,135 @@ fn milestone_report_line(m: ProgramMilestone) -> String { concat("\n ", startability_label(s: milestone_startability(m: m))))))))) } +// --------------------------------------------------------------------------------------------- +// THE NAMESPACE-XL STAGE CHAIN, RENDERED WITH THE SAME VOCABULARY AS THE MILESTONES. The chain +// itself (variants, labels, serial prerequisites, the ACT-0 receipt gate) is +// gunbc.namespace_cut_stage's; this section derives a STANDING per stage from the same +// populations the milestone arms read, and where a stage IS a milestone's own question the arm +// DELEGATES to milestone_status rather than spelling the derivation twice (DESIGN section 3). +// +// The derivations, stated so a reader knows which population moves each row: +// F-0 -- the wave-admission enrolment fold (Clear when the phase roster enrols the wall). +// XL-0 -- the unrealized-observation-rule population: the denominator stage stays +// outstanding while some subject's pulse cannot be taken (today: every host Rust +// probe, which awaits a host-item observation authority). +// XL-1 -- delegation to NamespaceBaselineObservationComplete. +// XL-2 -- the rehearsal digest read out of ACT-0's receipt carrier. +// XL-3 -- NotDerivable: no carrier censuses occurrences not spelled at their declaring +// identity, and fabricating a population would be worse than naming the gap. +// XL-4 -- the reference-graph digest read out of ACT-0's receipt carrier. +// ACT-0 -- the full required-receipt set (all four kinds outstanding today). +// XL-5/6/7 -- delegation to the three deletion milestones. +// --------------------------------------------------------------------------------------------- +fn stage_status(s: NamespaceCutStage) -> MilestoneStanding { + match s { + StageF0 => + standing_from_evidence( + e: observe_outstanding( + subject: "F-0: the control plane's own deliverable -- wall enrolment derived from the phase roster" as NonEmptyStr, + outstanding: wave_admission_enrolment_outstanding(phases: required_ci_phases) + ) + ) + StageXL0Denominator => + standing_from_evidence( + e: observe_outstanding( + subject: "XL-0: every deletion subject's observation rule realized" as NonEmptyStr, + outstanding: unobservable_probe_renders() + ) + ) + StageXL1BaselineCapture => milestone_status(m: NamespaceBaselineObservationComplete) + StageXL2RootDeletionRehearsal => + standing_from_evidence( + e: observe_outstanding( + subject: "XL-2: the rehearsal executed and its failure roster digested" as NonEmptyStr, + outstanding: activation_receipt_kind_outstanding(kind: RehearsalFailureRosterDigest, held: held_activation_receipts) + ) + ) + StageXL3DeclaringIdentitySpelling => + NotDerivable { + why: "no carrier censuses occurrences not yet spelled at their declaring identity. The wave wall's binding channel keys on leaf segments, deliberately invariant under requalification, so it cannot answer this either. Derivable once the spelling census exists." as NonEmptyStr, + cause: needs(i: DeclaringIdentitySpellingCensus) + } + StageXL4ReferenceDerivedGraph => + standing_from_evidence( + e: observe_outstanding( + subject: "XL-4: the reference-derived dependency graph measured and digested" as NonEmptyStr, + outstanding: activation_receipt_kind_outstanding(kind: ReferenceGraphDigest, held: held_activation_receipts) + ) + ) + StageAct0ActivationGate => + standing_from_evidence( + e: observe_outstanding( + subject: "ACT-0: every required activation receipt held against a pinned base" as NonEmptyStr, + outstanding: activation_receipts_outstanding(held: held_activation_receipts) + ) + ) + StageXL5Waves => milestone_status(m: NamespaceFirstSemanticWave) + StageXL6AtomicCutover => milestone_status(m: NamespaceFixForwardComplete) + StageXL7GrammarDeletion => milestone_status(m: NamespaceGrammarRetired) + } +} + +fn stage_missing_instruments(s: NamespaceCutStage) -> List { + match stage_status(s: s) { + Clear { evidence: _ } => [] + Outstanding { evidence: _ } => [] + NotDerivable { why: _, cause } => underivability_instruments(u: cause) + } +} + +// The stage half of the shared-demand join, so an instrument awaited only by a stage (XL-3's +// spelling census) is visible in the instrument report rather than reading as dead. +fn stages_awaiting(i: MissingInstrument) -> List { + fold(namespace_cut_stages, init: [], f: fn(acc, s) { + if any(stage_missing_instruments(s: s), other => missing_instrument_eq(a: other, b: i)) { + concat(acc, [namespace_cut_stage_label(s: s) as String]) + } else { + acc + } + }) +} + +// Startability over BOTH edge kinds a stage carries: its chain predecessor and, where the +// operator ruled one, its interlock milestone prerequisites. Same fail-closed law as the +// milestone classifier, through the same startability_from_populations. +fn stage_prerequisite_names_by_class(s: NamespaceCutStage, want: MilestoneStandingClass) -> List { + concat( + fold(stage_prerequisites(s: s), init: [], f: fn(acc, p) { + if standing_class_label(c: standing_class(s: stage_status(s: p))) + == standing_class_label(c: want) { + concat(acc, [namespace_cut_stage_label(s: p) as String]) + } else { + acc + } + }), + fold(stage_milestone_prerequisites(s: s), init: [], f: fn(acc, m) { + if standing_class_label(c: standing_class(s: milestone_status(m: m))) + == standing_class_label(c: want) { + concat(acc, [milestone_label(m: m) as String]) + } else { + acc + } + }) + ) +} + +fn stage_startability(s: NamespaceCutStage) -> Startability { + startability_from_populations( + unanswerable: stage_prerequisite_names_by_class(s: s, want: ClassNotDerivable), + blocking: stage_prerequisite_names_by_class(s: s, want: ClassOutstanding)) +} + +fn stage_report_line(s: NamespaceCutStage) -> String { + let st = stage_status(s: s) + concat("- [", + concat(standing_class_label(c: standing_class(s: st)), + concat("] ", + concat(namespace_cut_stage_label(s: s) as String, + concat("\n ", concat(standing_detail(s: st), + concat("\n ", startability_label(s: stage_startability(s: s))))))))) +} + // --------------------------------------------------------------------------------------------- // THE REPORT DENOMINATES ITSELF, AND THIS EXISTS BECAUSE ITS ABSENCE COST SOMETHING MEASURABLE. // @@ -744,7 +984,7 @@ fn census_line(c: StandingCensus) -> String { } fn instrument_report_line(i: MissingInstrument) -> String { - let waiting = milestones_awaiting(i: i) + let waiting = concat(milestones_awaiting(i: i), stages_awaiting(i: i)) let obstacle = missing_instrument_obstacle(i: i) concat("- (", concat(to_string(n: count(waiting)), @@ -763,11 +1003,16 @@ fn report() -> String { fold(program_milestones, init: "", f: fn(acc, m) { concat(acc, concat(milestone_report_line(m: m), "\n")) }), - concat("\nmissing instruments, by how many milestones AWAIT each\n\n", + concat("\nnamespace cut stages (gunbc.namespace_cut_stage, serial; standings derived)\n\n", + concat( + fold(namespace_cut_stages, init: "", f: fn(acc, s) { + concat(acc, concat(stage_report_line(s: s), "\n")) + }), + concat("\nmissing instruments, by how many milestones and stages AWAIT each\n\n", fold(all_missing_instruments, init: "", f: fn(acc, i) { concat(acc, concat(instrument_report_line(i: i), "\n")) }) - )))) + )))))) } fn where_are_we(out: String) -> ProcessExit { diff --git a/dag/gunbc/fabric/fabric_witness_run.dag b/dag/gunbc/fabric/fabric_witness_run.dag index 601b0ad0008..d24ebe39711 100644 --- a/dag/gunbc/fabric/fabric_witness_run.dag +++ b/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 diff --git a/dag/gunbc/namespace/namespace_cut_stage.dag b/dag/gunbc/namespace/namespace_cut_stage.dag new file mode 100644 index 00000000000..eb797a19f28 --- /dev/null +++ b/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 { + 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 { + match s { + StageF0 => [] + StageXL0Denominator => [] + StageXL1BaselineCapture => [] + StageXL2RootDeletionRehearsal => [] + StageXL3DeclaringIdentitySpelling => [] + StageXL4ReferenceDerivedGraph => [] + StageAct0ActivationGate => [SelfHostRatchetGateEnrolled, NamespaceWaveAdmissionEnrolled, NamespaceBaselineObservationComplete] + StageXL5Waves => [] + StageXL6AtomicCutover => [] + StageXL7GrammarDeletion => [] + } +} + +data namespace_cut_stages: List = [ + 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 = [ + 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 = [] + +// 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) -> List { + 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) -> List { + activation_receipts_outstanding(held: held) + |> filter(label => label == activation_receipt_kind_label(k: kind)) +} diff --git a/dag/gunbc/namespace/namespace_cut_subject_observation.dag b/dag/gunbc/namespace/namespace_cut_subject_observation.dag new file mode 100644 index 00000000000..27574b809b4 --- /dev/null +++ b/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, + modules: List +) -> 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 = ["src/v1"] +data subject_roster_v2_pool_roots: List = ["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 { + 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= 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)) + } + } +} diff --git a/dag/gunbc/namespace/namespace_cut_subject_roster.dag b/dag/gunbc/namespace/namespace_cut_subject_roster.dag new file mode 100644 index 00000000000..51c7d0089aa --- /dev/null +++ b/dag/gunbc/namespace/namespace_cut_subject_roster.dag @@ -0,0 +1,224 @@ +module gunbc.namespace_cut_subject_roster + +import std.types { String, NonEmptyStr, Bool, List } +import gunbc.namespace_cut_stage { + NamespaceCutStage, + StageXL5Waves, + StageXL6AtomicCutover, + StageXL7GrammarDeletion, + namespace_cut_stage_label, + namespace_cut_stage_is, +} + +// THE NAMESPACE CUT'S DELETION DENOMINATOR: every authority scheduled to disappear, one closed +// variant per subject family, at stable identity grain. This is the carrier +// gunbc.compiler_frontend_program_status has named as its missing NamespaceStepSubjectRoster +// instrument since 2026-08-26 -- "the namespace cut's remaining per-step subjects as rows". +// +// WHY THE PROBES ARE STRINGS AND NOT AUTHORED DeclarationRef LITERALS, which looks like the +// weaker spelling and is the only workable one. The ingestion-time citation wall +// (v1_compiler.declaration_index, cited-symbol arm) resolves every decl_ref literal on every +// required run and REFUSES when the target is gone. Every declaration this roster names is +// SCHEDULED TO BE DELETED: the moment a wave deletes one, an authored citation to it would red +// the whole corpus -- the roster would refuse the very transition it exists to census. So a row +// carries its identity as data strings, the DeclarationRef is CONSTRUCTED at observation time +// from non-literal arguments (which the wall deliberately does not capture -- its own fail-open +// arm), and resolution happens at runtime through v2.std.decl_ref_resolution -- in the live +// sibling module gunbc.namespace_cut_subject_observation, split off so importing THIS module +// never pulls live-read code into a consumer's closure -- where ABSENT is an answer rather than +// a refusal. Absence-as-answer is the whole requirement: after the cut, SubjectProbeAbsent is +// this roster's success state. +// +// IDENTITIES DECIDE, COUNTS SUMMARIZE. Every judgment below is a fold over probe identities; +// no arm compares a count to a count. +type NamespaceCutSubjectIdentity + = ImportGrammarProductions + | ImportParseSurfaceV1 + | ImportAstCarriers + | ResolverImportNameUniverse + | ImportScopeOverlays + | ImportDerivedModuleAdjacency + | HostImportClosureAssembly + | HostTextImportScanners + | ImportDerivedUseLineInputs + | LegacyImportRepairApparatus + | LayerImportFactsConsumers + +fn namespace_cut_subject_label(s: NamespaceCutSubjectIdentity) -> NonEmptyStr { + match s { + ImportGrammarProductions => "the v2 import grammar: lex rule, formal rows, productions, emit rows" as NonEmptyStr + ImportParseSurfaceV1 => "the v1 import parse surface" as NonEmptyStr + ImportAstCarriers => "the import AST carriers on both frontends" as NonEmptyStr + ResolverImportNameUniverse => "the resolver import-name universe: source_visible_names and the import admission folds" as NonEmptyStr + ImportScopeOverlays => "the import scope overlays in v1 inference" as NonEmptyStr + ImportDerivedModuleAdjacency => "import-derived module adjacency and the build ordering it feeds" as NonEmptyStr + HostImportClosureAssembly => "host import-closure assembly in the stage0 CLI" as NonEmptyStr + HostTextImportScanners => "host raw-text import and module-path scanners" as NonEmptyStr + ImportDerivedUseLineInputs => "import-derived inputs to Rust use-line emission" as NonEmptyStr + LegacyImportRepairApparatus => "the unlisted-import repair and census apparatus" as NonEmptyStr + LayerImportFactsConsumers => "the layer_import_facts family and its interpreter arm" as NonEmptyStr + } +} + +// A probe names ONE declaration-grain identity. Two probe kinds because the corpus has two +// realization media on the deletion path: substrate declarations, observable today through the +// declaration-fact reflection the observation sibling executes, and HOST RUST ITEMS, whose +// observation instrument does not exist in this tree yet. A host probe is therefore honest about +// its own standing: it names the item and refuses to claim Present or Absent (see the sibling's +// observe_probe). +type NamespaceCutSubjectProbe + = DagDeclarationProbe { module_path: String, decl_name: String } + | DagDeclarationFieldProbe { module_path: String, decl_name: String, field_name: String } + | HostRustItemProbe { crate_relative_file: String, item_name: String } + +// EVERY SUBJECT HAS AT LEAST ONE PROBE BY CONSTRUCTION: the shape is first + rest, so an +// empty-probed subject has no spelling, and the match is exhaustive, so a subject added without +// probes refuses to compile. The probe lists are the identity grain the exit criterion demands; +// they are not exhaustive over every declaration a wave will touch -- each is the subject's +// ROOT identities, the ones whose absence is the subject being gone (the plan documents carry +// the full per-step sweeps; a sweep is a wave's worklist, a probe is a subject's pulse). +type NamespaceCutSubjectProbes { + first: NamespaceCutSubjectProbe + rest: List +} + +fn subject_probes(s: NamespaceCutSubjectIdentity) -> NamespaceCutSubjectProbes { + match s { + ImportGrammarProductions => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v2.extdeps.languages.dag", decl_name: "dag_grammar_import_decl_expr" }, + rest: [ + DagDeclarationProbe { module_path: "v2.extdeps.languages.dag", decl_name: "dag_grammar_import_block_expr" }, + ], + } + ImportParseSurfaceV1 => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v1.compiler.parse", decl_name: "parse_import" }, + rest: [ + DagDeclarationProbe { module_path: "v1.compiler.parse", decl_name: "parse_imports" }, + ], + } + ImportAstCarriers => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v1.std.core", decl_name: "import_node" }, + rest: [ + DagDeclarationProbe { module_path: "v1.std.core", decl_name: "module_imports" }, + DagDeclarationProbe { module_path: "v2.compiler.name_resolve", decl_name: "Import" }, + ], + } + ResolverImportNameUniverse => NamespaceCutSubjectProbes { + first: DagDeclarationFieldProbe { module_path: "v1.compiler.infer_env", decl_name: "TypeEnv", field_name: "source_visible_names" }, + rest: [ + DagDeclarationProbe { module_path: "v1.compiler.resolve", decl_name: "resolve_module_imports" }, + DagDeclarationProbe { module_path: "v2.compiler.name_resolve", decl_name: "admit_imports" }, + ], + } + ImportScopeOverlays => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v1.compiler.infer", decl_name: "merge_scope_from_imports" }, + rest: [ + DagDeclarationProbe { module_path: "v1.compiler.infer", decl_name: "overlay_direct_import_exports" }, + ], + } + ImportDerivedModuleAdjacency => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v1.compiler.resolve", decl_name: "topological_sort" }, + rest: [ + HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "build_import_adjacency" }, + ], + } + HostImportClosureAssembly => NamespaceCutSubjectProbes { + first: HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "import_closure_from_adjacency" }, + rest: [ + HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "compile_entry_on_declared_import_closure_only" }, + ], + } + HostTextImportScanners => NamespaceCutSubjectProbes { + first: HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "extract_import_paths" }, + rest: [ + HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "referenced_module_paths_in_text" }, + ], + } + ImportDerivedUseLineInputs => NamespaceCutSubjectProbes { + first: DagDeclarationProbe { module_path: "v1.compiler.emit_rust", decl_name: "emit_imports" }, + rest: [ + DagDeclarationProbe { module_path: "v1.compiler.emit_rust", decl_name: "emit_extract_import_paths_fn" }, + ], + } + LegacyImportRepairApparatus => NamespaceCutSubjectProbes { + first: HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "classify_unlisted_import_binding_source" }, + rest: [ + DagDeclarationProbe { module_path: "v1.compiler.infer_env", decl_name: "listed_import_required_bare_call_blocked" }, + ], + } + LayerImportFactsConsumers => NamespaceCutSubjectProbes { + first: HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "layer_import_facts" }, + rest: [], + } + } +} + +fn subject_probe_list(s: NamespaceCutSubjectIdentity) -> List { + let probes = subject_probes(s: s) + concat([probes.first], probes.rest) +} + +// WHICH STAGE DELETES EACH SUBJECT -- the join the stage standings fold over. Total, so a new +// subject refuses to compile until its deleting stage is stated. The partition follows the +// grammar-last ruling structurally: only the grammar and parse surfaces die at XL-7; everything +// semantic dies in the waves; the adjacency/closure repoint lands with the cutover. +fn subject_deleted_at_stage(s: NamespaceCutSubjectIdentity) -> NamespaceCutStage { + match s { + ImportGrammarProductions => StageXL7GrammarDeletion + ImportParseSurfaceV1 => StageXL7GrammarDeletion + ImportAstCarriers => StageXL7GrammarDeletion + ResolverImportNameUniverse => StageXL5Waves + ImportScopeOverlays => StageXL5Waves + ImportDerivedModuleAdjacency => StageXL6AtomicCutover + HostImportClosureAssembly => StageXL6AtomicCutover + HostTextImportScanners => StageXL5Waves + ImportDerivedUseLineInputs => StageXL5Waves + LegacyImportRepairApparatus => StageXL5Waves + LayerImportFactsConsumers => StageXL6AtomicCutover + } +} + +data namespace_cut_subjects: List = [ + ImportGrammarProductions, + ImportParseSurfaceV1, + ImportAstCarriers, + ResolverImportNameUniverse, + ImportScopeOverlays, + ImportDerivedModuleAdjacency, + HostImportClosureAssembly, + HostTextImportScanners, + ImportDerivedUseLineInputs, + LegacyImportRepairApparatus, + LayerImportFactsConsumers, +] + +fn subjects_deleted_at(stage: NamespaceCutStage) -> List { + namespace_cut_subjects + |> filter(s => namespace_cut_stage_is(a: subject_deleted_at_stage(s: s), b: stage)) +} + +fn probe_render(p: NamespaceCutSubjectProbe) -> String { + match p { + DagDeclarationProbe { module_path, decl_name } => + concat(module_path, concat(" ", decl_name)) + DagDeclarationFieldProbe { module_path, decl_name, field_name } => + concat(module_path, concat(" ", concat(decl_name, concat(".", field_name)))) + HostRustItemProbe { crate_relative_file, item_name } => + concat(crate_relative_file, concat(" ", item_name)) + } +} + +// The pure denominator of unrealized observation rules: the probes whose observation cannot +// currently answer, derived from probe kind alone (no live read). This is XL-0's outstanding +// population in the stage standings -- the denominator stage is outstanding exactly while some +// subject's pulse cannot be taken. +fn unobservable_probe_renders() -> List { + namespace_cut_subjects + |> flat_map(s => subject_probe_list(s: s)) + |> filter(p => match p { + HostRustItemProbe { crate_relative_file: _, item_name: _ } => true + DagDeclarationProbe { module_path: _, decl_name: _ } => false + DagDeclarationFieldProbe { module_path: _, decl_name: _, field_name: _ } => false + }) + |> map(p => probe_render(p: p)) +} diff --git a/dag/gunbc/plans/import_namespace_program.dag b/dag/gunbc/plans/import_namespace_program.dag index 90a2235f47d..ad2366c728a 100644 --- a/dag/gunbc/plans/import_namespace_program.dag +++ b/dag/gunbc/plans/import_namespace_program.dag @@ -130,7 +130,7 @@ fn section_9() -> List { [ h2(text: "9. What this plan does NOT claim"), ul(items: [ - li(text: "**No CI mechanism enforces any of this** — no ratchet, no phase, no gate over the import population. **As of the 2026-08-26 ruling this is a BLOCKER rather than a disclosure**: it now gates Step 1 by name. A plan that reads as governed when it is not is worse than one that reads as unguarded, and this gap has since been given an executable consequence rather than left as candour."), + li(text: "**The CI-mechanism gap is CLOSED and this bullet is its record, not its claim.** Earlier revisions said no phase or gate covered the import population, then ruled that gap a Step-1 blocker. The wave-admission wall has since landed as the required `namespace-wave-admission` phase (gunbc#9365), phase enrolment is a substrate fact (`gunbc.required_ci_phase_roster`, joined against the executor's realization on every required run), and the milestone reads it derived: run `gunbc.compiler_frontend_program_status` `where_are_we` rather than trusting any sentence here. The remaining governance gaps are the ones that report names as NOT-DERIVABLE, each with its missing instrument."), li(text: "**No population figure here is live.** Section 5 says why."), li(text: "**Step ownership is not carried by any authority.** Section 4 says which half is assumed."), li(text: "**The ordering relation to self-host is RULED and is no longer a gap** — section 7 projects `gunbc.compiler_frontend_program_interlock`. It is listed here only so a reader of an older revision does not go looking for the open question."), @@ -152,6 +152,9 @@ data import_namespace_program_bindings: List = [ decl_ref(module_path: "gunbc.compiler_frontend_program_interlock", decl_name: "NamespaceChangeClass"), decl_ref(module_path: "gunbc.compiler_frontend_program_interlock", decl_name: "NamespaceDeltaDisposition"), decl_ref(module_path: "gunbc.namespace_cut_landing_order", decl_name: "namespace_cut_grammar_last_ruling"), + decl_ref(module_path: "gunbc.required_ci_phase_roster", decl_name: "required_ci_phases"), + decl_ref(module_path: "gunbc.namespace_cut_stage", decl_name: "stage_prerequisites"), + decl_ref(module_path: "gunbc.namespace_cut_subject_roster", decl_name: "namespace_cut_subjects"), ] fn import_namespace_program_body() -> List { diff --git a/dag/gunbc/required_ci_host_verdict_census.dag b/dag/gunbc/required_ci_host_verdict_census.dag index 42bd3c0966c..0c6b4574893 100644 --- a/dag/gunbc/required_ci_host_verdict_census.dag +++ b/dag/gunbc/required_ci_host_verdict_census.dag @@ -3,6 +3,7 @@ module gunbc.required_ci_host_verdict_census import std.types { List, String, Bool } import std.decl_ref { DeclarationRef, decl_ref } import std.dissolution { DissolutionCondition, unbound_dissolution } +import gunbc.required_ci_phase_roster { RequiredCiLane, BuildLane, WitnessesLane } // Census of the phases selected by claim_executor's RequiredCiPhase roster -- one row each, so the // roster IS the count and no number is transcribed here. IT READ "the seven phases" AND THE ROWS @@ -30,13 +31,15 @@ import std.dissolution { DissolutionCondition, unbound_dissolution } // cut. RealizesCarrier is retained as the negative population so "host Rust exists" cannot be // mistaken for the defect being counted. // -// CEILING. Phase existence and lane ownership are themselves host facts: RequiredCiPhase, its -// exhaustive lane match, and REQUIRED_CI_PHASES have no substrate authority. Therefore this is an -// authored census inside a host-owned frame, not a completeness proof. A newly added Rust phase -// does not appear here by construction. The next-rung trigger at the bottom cuts that root; a -// count pinned to today's list would merely turn this limitation into measure() == measure(). - -type RequiredCiLane = BuildLane | WitnessesLane +// CEILING, PARTIALLY LIFTED. When this census was authored, phase existence and lane ownership +// were host facts with no substrate authority. gunbc.required_ci_phase_roster now carries both, +// the workflow emission consumes its lane vocabulary, and every --required-ci run joins the host +// enum's variant set against that declaration in both directions -- so a newly added phase that +// exists on only one side refuses at run time rather than appearing nowhere. What has NOT fired +// is the atomic-deletion half of the trigger at the bottom: the host enum, lane match and +// REQUIRED_CI_PHASES still exist, so this remains an authored census inside a host-realized +// frame, and the trigger below stands until the host side deletes. A count pinned to today's +// list would still merely turn this limitation into measure() == measure(). type HostVerdictRelation = ReDecidesCarrier { diff --git a/dag/gunbc/required_ci_phase_roster.dag b/dag/gunbc/required_ci_phase_roster.dag new file mode 100644 index 00000000000..fe7d2ce3966 --- /dev/null +++ b/dag/gunbc/required_ci_phase_roster.dag @@ -0,0 +1,97 @@ +module gunbc.required_ci_phase_roster + +import std.types { String, Bool, List } + +// THE SUBSTRATE AUTHORITY FOR WHICH PHASES REQUIRED CI RUNS, AND WHICH LANE OWNS EACH. +// gunbc.required_ci_host_verdict_census recorded the gap this module closes, in its own words: +// "Phase existence and lane ownership are themselves host facts: RequiredCiPhase, its exhaustive +// lane match, and REQUIRED_CI_PHASES have no substrate authority" -- and named this exact carrier +// as its next rung (required_ci_phase_roster_next_rung). This module is that carrier: phase +// identity and lane ownership as one roster, consumed by the workflow emission +// (gunbc.fabric_witness_run takes its lane vocabulary from required_ci_lane_name) and by the +// program-standing derivation (gunbc.compiler_frontend_program_status derives +// NamespaceWaveAdmissionEnrolled from membership in required_ci_phases, never from a status row). +// +// THE HOST REALIZATION IS A DECLARED PARALLEL REPRESENTATION WITH AN EXECUTING JOIN, NOT A TWIN +// LEFT TO DRIFT. claim_executor's RequiredCiPhase enum realizes this coproduct, and every +// --required-ci run joins the two BEFORE running any phase: set equality over this declaration's +// variant names, in both directions, so "declared here and not realized" and "realized and not +// declared" are separate refusals that stop the line (the same join shape +// v1_compiler.namespace_wave_admission vocabulary_findings executes against its disposition +// authority). What the join deliberately does NOT cover is lane ownership -- the host lane match +// is not readable from the declaration index -- and that residue is honest rather than dangerous +// for enrolment truth: both lanes execute in every required run, so a lane divergence can move a +// phase between two jobs that both run; it cannot un-enrol one. The terminal state is the one the +// census's dissolution row already names: the workflow emission consumes this roster whole and +// the host enum, lane match and REQUIRED_CI_PHASES list delete atomically. Until that fires, the +// parallel representation is this module's declared debt and the per-run join is its wall. +type RequiredCiLane + = BuildLane + | WitnessesLane + +fn required_ci_lane_name(l: RequiredCiLane) -> String { + match l { + BuildLane => "build" + WitnessesLane => "witnesses" + } +} + +// THE PHASE IDENTITIES ARE A CLOSED VOCABULARY. Adding a phase means adding a variant, at which +// point required_ci_phase_name and required_ci_phase_lane refuse to compile until the new phase +// states its CLI word and its lane -- construction, not a list a phase can be omitted from. +// The four phases are the post-bankruptcy roster (gunbc.rung_drop required_gate_bankruptcy, +// 2026-08-29): parse, namespace-wave-admission, regen, floor. +type RequiredCiPhase + = ParsePhase + | NamespaceWaveAdmissionPhase + | RegenPhase + | FloorPhase + +fn required_ci_phase_name(p: RequiredCiPhase) -> String { + match p { + ParsePhase => "parse" + NamespaceWaveAdmissionPhase => "namespace-wave-admission" + RegenPhase => "regen" + FloorPhase => "floor" + } +} + +// Lane ownership, total. Parse and the wave wall share the witnesses lane because the wall +// consumes the index the parse phase builds -- one acquisition, two consumers. +fn required_ci_phase_lane(p: RequiredCiPhase) -> RequiredCiLane { + match p { + ParsePhase => WitnessesLane + NamespaceWaveAdmissionPhase => WitnessesLane + RegenPhase => BuildLane + FloorPhase => WitnessesLane + } +} + +// THE ROSTER IS THE DENOMINATOR every enrolment question folds over. A variant absent from this +// list is declared and not enrolled -- a representable state on purpose, because that is exactly +// what a deliberate un-enrolment (a bankruptcy) looks like, and it must be a visible row edit +// here rather than a silent host edit. The per-run host join keeps the two from diverging +// silently in either direction. +data required_ci_phases: List = [ + ParsePhase, + NamespaceWaveAdmissionPhase, + RegenPhase, + FloorPhase, +] + +fn required_ci_phase_is(a: RequiredCiPhase, b: RequiredCiPhase) -> Bool { + required_ci_phase_name(p: a) == required_ci_phase_name(p: b) +} + +// Membership at identity grain. Parameterized on the roster rather than closing over +// required_ci_phases so a witness can author both the enrolled and the un-enrolled population -- +// the RED is authorable at the fixture boundary, which is the boundary that decides (DESIGN 4b). +fn required_ci_phase_enrolled(p: RequiredCiPhase, phases: List) -> Bool { + any(phases, x => required_ci_phase_is(a: x, b: p)) +} + +fn lane_phase_names(lane: RequiredCiLane, phases: List) -> List { + phases + |> filter(p => required_ci_lane_name(l: required_ci_phase_lane(p: p)) == required_ci_lane_name(l: lane)) + |> map(p => required_ci_phase_name(p: p)) +} diff --git a/dag/test/claim/compiler_frontend_program_status_witness_test.dag b/dag/test/claim/compiler_frontend_program_status_witness_test.dag index 7056996867f..490b2ee6d37 100644 --- a/dag/test/claim/compiler_frontend_program_status_witness_test.dag +++ b/dag/test/claim/compiler_frontend_program_status_witness_test.dag @@ -12,12 +12,47 @@ import gunbc.compiler_frontend_program_interlock { SelfHostEmitterProducesEveryRetainedArtifact, SelfHostRatchetGateEnrolled, SelfHostCorpusEmitsCleanly, + SelfHostCargoPhaseEnrolled, + NamespaceWaveAdmissionEnrolled, + NamespaceBaselineObservationComplete, NamespaceFixForwardComplete, NamespaceGrammarRetired, NamespaceFirstSemanticWave, milestone_label, } +import gunbc.required_ci_phase_roster { + RequiredCiPhase, + ParsePhase, + NamespaceWaveAdmissionPhase, + required_ci_phases, +} +import gunbc.namespace_cut_stage { + NamespaceCutStage, + StageXL5Waves, + StageXL6AtomicCutover, + StageXL7GrammarDeletion, + namespace_cut_stages, + namespace_cut_stage_label, + ActivationReceipt, + ActivationReceiptKind, + RehearsalFailureRosterDigest, + activation_receipts_outstanding, + activation_receipt_kind_outstanding, + activation_receipt_kind_label, + required_activation_receipt_kinds, +} +import gunbc.namespace_cut_subject_roster { + subjects_deleted_at, + subject_probe_list, + probe_render, +} import gunbc.emit_subject_clean_frontier { emit_ratchet_runner_cadence } +import v2.workflow.legacy_baseline_capture { + CaptureAvailable, + CaptureBlocked, + legacy_baseline_capture_capability, + capture_blocked_reason, +} import v2.compiler.self_host.stage0_crate_layout { emitter_produced_divergent_registrations } import gunbc.cli_dispatch_surface { gunbc_cli_emitter_gap } import gunbc.compiler_frontend_program_status { @@ -27,9 +62,16 @@ import gunbc.compiler_frontend_program_status { NotDerivable, MissingInstrument, WholeCorpusEmissionBoard, - NamespaceStepSubjectRoster, - RequiredCiPhaseRoster, + PhaseCargoExecutionFact, + DeclaringIdentitySpellingCensus, all_missing_instruments, + conditionally_awaited_instruments, + stages_awaiting, + stage_status, + stage_startability, + stage_prerequisite_names_by_class, + wave_admission_enrolment_outstanding, + stage_subject_outstanding, InstrumentObstacle, NotBuilt, RefusedByAuthority, @@ -410,25 +452,110 @@ test fn the_whole_corpus_board_is_awaited_by_exactly_these_three() -> Bool { && any(waiting, l => l == milestone_label(m: SelfHostCorpusEmitsCleanly)) } -// THE SUBSTITUTION CONTROL. The two three-milestone instruments have DISJOINT memberships, so an -// exchange between them preserves both counts and both cardinalities while making both sets wrong. -// Asserting each set's exact identities plus this disjointness is what a count -- or a count plus a -// single anchor identity, which is what this arm checked in its first cut -- cannot see. -test fn the_two_three_milestone_instruments_do_not_share_a_milestone() -> Bool { - let board = milestones_awaiting(i: WholeCorpusEmissionBoard) - let roster = milestones_awaiting(i: NamespaceStepSubjectRoster) - count(roster) == 3 - && any(roster, l => l == milestone_label(m: NamespaceFirstSemanticWave)) - && any(roster, l => l == milestone_label(m: NamespaceFixForwardComplete)) - && any(roster, l => l == milestone_label(m: NamespaceGrammarRetired)) - && all(board, l => count(roster |> filter(other => other == l)) == 0) +// THE THREE DELETION MILESTONES ARE WIRED TO THE SUBJECT ROSTER -- the same wiring relation as +// the S4a arm: the milestone's members equal its stage's declared-subject fold, re-derived here +// from the roster's own sources (subjects_deleted_at + subject_probe_list) rather than obtained +// from the carrier's stage_subject_outstanding, so a fold that adds or drops a member is visible +// instead of cancelling on both sides. Moves on both sides as waves retire rows; cannot red on +// progress. +fn expected_stage_subjects(stage: NamespaceCutStage) -> List { + subjects_deleted_at(stage: stage) + |> flat_map(s => subject_probe_list(s: s)) + |> map(p => probe_render(p: p)) +} + +test fn the_deletion_milestones_are_wired_to_their_stage_subjects() -> Bool { + standing_agrees_with_population( + s: milestone_status(m: NamespaceFirstSemanticWave), + expected: expected_stage_subjects(stage: StageXL5Waves)) + && standing_agrees_with_population( + s: milestone_status(m: NamespaceFixForwardComplete), + expected: expected_stage_subjects(stage: StageXL6AtomicCutover)) + && standing_agrees_with_population( + s: milestone_status(m: NamespaceGrammarRetired), + expected: expected_stage_subjects(stage: StageXL7GrammarDeletion)) +} + +// THE WAVE-ADMISSION ENROLMENT FOLD ANSWERS BOTH WAYS AT FIXTURE GRAIN -- the RED the live +// roster cannot author (the phase is enrolled) is authored here as a roster without it. +test fn the_wave_admission_enrolment_fold_answers_both_ways() -> Bool { + count(wave_admission_enrolment_outstanding(phases: [ParsePhase])) == 1 + && count(wave_admission_enrolment_outstanding(phases: [ParsePhase, NamespaceWaveAdmissionPhase])) == 0 +} + +// AND THE MILESTONE IS WIRED TO THAT FOLD OVER THE LIVE ROSTER -- the same self-comparison-as- +// wiring-claim shape as the S4a arm: rewiring the milestone off the phase roster reds this. +test fn the_wave_admission_milestone_is_wired_to_the_phase_roster() -> Bool { + standing_agrees_with_population( + s: milestone_status(m: NamespaceWaveAdmissionEnrolled), + expected: wave_admission_enrolment_outstanding(phases: required_ci_phases)) +} + +// THE BASELINE MILESTONE'S TWO ARMS, CHECKED WITHOUT PINNING TODAY'S CAPABILITY. While capture is +// blocked the milestone must carry exactly the capability fold's reasons; when capture becomes +// available the contract is the NotDerivable arm, and this witness accepts it rather than redding +// on that legitimate transition (the backward contract this file has been corrected for twice). +test fn the_baseline_milestone_follows_the_capture_capability() -> Bool { + match legacy_baseline_capture_capability() { + CaptureBlocked { phase: p, cause: c } => + standing_agrees_with_population( + s: milestone_status(m: NamespaceBaselineObservationComplete), + expected: capture_blocked_reason(c: CaptureBlocked { phase: p, cause: c })) + CaptureAvailable => + standing_is(want: ClassNotDerivable, s: milestone_status(m: NamespaceBaselineObservationComplete)) + } +} + +// THE ACTIVATION RECEIPT GATE, AT FIXTURE GRAIN IN BOTH DIRECTIONS: an empty held-roster leaves +// every required kind outstanding by identity, and holding exactly the rehearsal receipt removes +// exactly that kind -- so the fold is keyed on identity, not on count. +test fn the_activation_receipt_fold_is_keyed_on_receipt_identity() -> Bool { + let empty_outstanding = activation_receipts_outstanding(held: []) + let rehearsal_held = activation_receipts_outstanding(held: [ + ActivationReceipt { + kind: RehearsalFailureRosterDigest, + activation_base_commit: "fixture-base" as NonEmptyStr, + digest: "fixture-digest" as NonEmptyStr, + } + ]) + count(empty_outstanding) == count(required_activation_receipt_kinds) + && all(required_activation_receipt_kinds, + k => any(empty_outstanding, o => o == activation_receipt_kind_label(k: k))) + && count(rehearsal_held) + 1 == count(required_activation_receipt_kinds) + && !any(rehearsal_held, o => o == activation_receipt_kind_label(k: RehearsalFailureRosterDigest)) + && count(activation_receipt_kind_outstanding(kind: RehearsalFailureRosterDigest, held: [])) == 1 +} + +// STAGE STARTABILITY AGREES WITH ITS PREREQUISITE STANDINGS, over the whole chain, re-derived +// through the carrier's own per-class partition -- the same law the milestone arm asserts, so +// the stage classifier cannot silently stop consulting either edge kind. +test fn every_stage_startability_agrees_with_its_prerequisite_standings() -> Bool { + all(namespace_cut_stages, s => + startability_matches( + a: stage_startability(s: s), + b: startability_from_populations( + unanswerable: stage_prerequisite_names_by_class(s: s, want: ClassNotDerivable), + blocking: stage_prerequisite_names_by_class(s: s, want: ClassOutstanding)))) +} + +// THE CHAIN'S STAGE LABELS ARE DISTINCT -- the same counted-second-representation guard as the +// milestone roster: a duplicated stage entry would silently double a report row. +test fn the_stage_roster_entries_are_distinct() -> Bool { + let labels = namespace_cut_stages |> map(s => namespace_cut_stage_label(s: s) as String) + all(labels, l => count(labels |> filter(other => other == l)) == 1) } -// THE DISCRIMINATING ARM FOR THE SAME JOIN: an instrument that answers ONE milestone must not -// report three, which is what a fold accidentally ignoring its predicate would produce. -test fn a_single_milestone_instrument_reports_one() -> Bool { - count(milestones_awaiting(i: RequiredCiPhaseRoster)) == 1 - && count(milestones_awaiting(i: NamespaceStepSubjectRoster)) == 3 +// THE SHARED-DEMAND JOIN'S SINGLETON ARMS, at identity grain: the cargo-execution fact is awaited +// by exactly the cargo milestone, and the spelling census by exactly the XL-3 stage -- the row +// that would read as dead if the instrument report only joined milestones. +test fn the_two_new_instruments_are_awaited_at_the_right_grain() -> Bool { + let cargo = milestones_awaiting(i: PhaseCargoExecutionFact) + let spelling_m = milestones_awaiting(i: DeclaringIdentitySpellingCensus) + let spelling_s = stages_awaiting(i: DeclaringIdentitySpellingCensus) + count(cargo) == 1 + && any(cargo, l => l == milestone_label(m: SelfHostCargoPhaseEnrolled)) + && count(spelling_m) == 0 + && count(spelling_s) == 1 } // THE INSTRUMENT ROSTER IS THE SAME COUNTED SECOND REPRESENTATION THE MILESTONE ROSTER IS, for the @@ -438,7 +565,9 @@ test fn a_single_milestone_instrument_reports_one() -> Bool { test fn every_declared_instrument_is_distinct_and_awaited() -> Bool { let labels = all_missing_instruments |> map(i => missing_instrument_label(i: i)) all(labels, l => count(labels |> filter(other => other == l)) == 1) - && all(all_missing_instruments, i => count(milestones_awaiting(i: i)) > 0) + && all(all_missing_instruments, + i => count(milestones_awaiting(i: i)) + count(stages_awaiting(i: i)) > 0 + || any(conditionally_awaited_instruments, c => missing_instrument_label(i: c) == missing_instrument_label(i: i))) } // UNBUILT AND REFUSED ARE DIFFERENT STATES WITH DIFFERENT REMEDIES, and this arm now exhibits that diff --git a/dag/test/claim/namespace_cut_subject_observation_witness_test.dag b/dag/test/claim/namespace_cut_subject_observation_witness_test.dag new file mode 100644 index 00000000000..197108e9b08 --- /dev/null +++ b/dag/test/claim/namespace_cut_subject_observation_witness_test.dag @@ -0,0 +1,87 @@ +module test.claim.namespace_cut_subject_observation_witness + +import std.decl_ref { decl_ref } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import v2.std.decl_index { FnItem } +import v2.std.decl_ref_resolution { + DeclarationIdentity, + DeclarationRefResolved, + DeclarationRefModuleAbsent, + DeclarationRefDeclarationAbsent, + DeclarationRefAmbiguous, +} +import gunbc.namespace_cut_subject_roster { + NamespaceCutSubjectProbe, + DagDeclarationProbe, + HostRustItemProbe, + namespace_cut_subjects, + subject_probe_list, + probe_render, +} +import gunbc.namespace_cut_subject_observation { + SubjectProbeObservation, + SubjectProbePresent, + SubjectProbeAbsent, + SubjectProbeUnobservable, + observation_from_resolution, + observe_probe, + probe_is_v1, +} + +// ReadsLiveTree by G1 carrier-closure honesty, exactly as v2.test.lens_enforcement.gate_test +// records for itself: every arm below feeds AUTHORED values, but the loader closure imports the +// observation module, which is a declared live-read carrier home, so a SubstrateInputsOnly stamp +// would be a lying stamp. The LIVE execution evidence for this instrument is its own runnable +// report (subject_roster_report), exercised by the manager rather than by the floor. +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +fn fixture_probe() -> NamespaceCutSubjectProbe { + DagDeclarationProbe { module_path: "v1.compiler.parse", decl_name: "parse_import" } +} + +// The resolvable citation is carried because a DeclarationRef naming nothing is refused at +// ingestion; the mapping under test never resolves it. +fn observation_kind(o: SubjectProbeObservation) -> String { + match o { + SubjectProbePresent { probe: _ } => "present" + SubjectProbeAbsent { probe: _ } => "absent" + SubjectProbeUnobservable { probe: _, why: _ } => "unobservable" + } +} + +// The mapping's four decided rows: resolved is the only Present, both absence arms are Absent, +// and ambiguity refuses to answer -- the arm whose collapse into Absent would fabricate a +// completed deletion out of a corpus defect. +test fn resolution_maps_to_observation_without_collapsing_ambiguity() -> Bool { + let r = decl_ref(module_path: "gunbc.required_ci_phase_roster", decl_name: "required_ci_phases") + let ident = DeclarationIdentity { qualified_name: "fixture.q", name: "fixture", rel_path: "fixture.dag", kind: FnItem } + observation_kind(o: observation_from_resolution(p: fixture_probe(), r: DeclarationRefResolved { declaration_identity: ident })) == "present" + && observation_kind(o: observation_from_resolution(p: fixture_probe(), r: DeclarationRefModuleAbsent { reference: r })) == "absent" + && observation_kind(o: observation_from_resolution(p: fixture_probe(), r: DeclarationRefDeclarationAbsent { reference: r })) == "absent" + && observation_kind(o: observation_from_resolution(p: fixture_probe(), r: DeclarationRefAmbiguous { reference: r, candidates: [DeclarationIdentity { qualified_name: "fixture.a", name: "a", rel_path: "fixture.dag", kind: FnItem }, DeclarationIdentity { qualified_name: "fixture.b", name: "b", rel_path: "fixture.dag", kind: FnItem }] })) == "unobservable" +} + +// A host probe refuses on EMPTY facts rather than answering Absent -- handed a fact population +// that contains nothing, it must not fabricate a deletion. +test fn a_host_probe_refuses_rather_than_answering_from_no_instrument() -> Bool { + let p = HostRustItemProbe { crate_relative_file: "src/v1/stage0/src/cli_run.rs", item_name: "extract_import_paths" } + observation_kind(o: observe_probe(p: p, facts: [], modules: [])) == "unobservable" +} + +// A dag probe over EMPTY module facts answers Absent by the module-absent route -- authored +// facts, so the arm is exercised without any tree state moving it. Beside it, the pool split: +// a v1 probe and a v2 probe classify to different acquisitions, both ways. +test fn a_dag_probe_over_authored_empty_facts_is_absent_and_pools_split_both_ways() -> Bool { + observation_kind(o: observe_probe(p: fixture_probe(), facts: [], modules: [])) == "absent" + && probe_is_v1(p: fixture_probe()) + && !probe_is_v1(p: DagDeclarationProbe { module_path: "v2.compiler.name_resolve", decl_name: "admit_imports" }) +} + +// Every subject's probes render distinctly -- a duplicated probe row would double a report line +// and a deletion milestone's outstanding member. +test fn every_probe_render_is_distinct_across_the_roster() -> Bool { + let renders = namespace_cut_subjects + |> flat_map(s => subject_probe_list(s: s)) + |> map(p => probe_render(p: p)) + all(renders, r => count(renders |> filter(other => other == r)) == 1) +} diff --git a/docs/plans/namespace-cut-replacement-plan.md b/docs/plans/namespace-cut-replacement-plan.md index d8889811eff..5e70162f9f7 100644 --- a/docs/plans/namespace-cut-replacement-plan.md +++ b/docs/plans/namespace-cut-replacement-plan.md @@ -39,6 +39,17 @@ > plan quarries but whose *terminal shapes* it keeps as evidence — is reopened > there as an operator decision. +> **CURRENT-STATE AUTHORITY (2026-08-29): this document carries REASONING and HISTORY, never +> live standing.** Enrolment, standing and sequencing facts are typed carriers, cited by symbol: +> the required-CI phase roster (and with it the wave-admission wall's enrolment) is +> `gunbc.required_ci_phase_roster` `required_ci_phases`; the NAMESPACE-XL stage chain and its +> prerequisites are `gunbc.namespace_cut_stage` `stage_prerequisites`; the deletion-subject +> denominator is `gunbc.namespace_cut_subject_roster` `namespace_cut_subjects`, observed by +> `gunbc.namespace_cut_subject_observation` `subject_roster_report`; and the derived standing +> report is `gunbc.compiler_frontend_program_status` `where_are_we`. Where a sentence below +> disagrees with those carriers, the carrier is correct and the sentence is a dated record — +> in particular, sentences predating #9365 that say no wall or CI mechanism exists. + Doctrine: DESIGN §3 *replacement migrations cut over at the root* (delete-first; the deletion is the census — bounded by the three silent populations measured across the five parallel cuts, recorded once in [floor-cut-replacement-plan.md](floor-cut-replacement-plan.md) under *What the census does not do*; they apply to this cut identically). Vehicle: integration branch `integration/namespace-cut`, forked from main `64ebefa74`; standing cutover PR gunbc#8282 (draft — the one merge main receives). Executing session: crisp-crab-430; doctrine/coordination: tidy-pike-117. Operator ruling (2026-08-15): delete all the grammar/import up front, then solve each problem as it is revealed — expecting the deletion to also reveal problems import was standing up (the concealment census). **SUPERSEDED ON ORDER 2026-08-25 — `gunbc.namespace_cut_landing_order` `namespace_cut_grammar_last_ruling`: grammar deletion is last.** The concealment-census expectation survives unchanged — what moved is when the grammar is cut, not what cutting it reveals. **Step gating:** each major step closes only when the operator is satisfied with its performance — the executing session stops at the boundary and presents, never rolls into the next step on its own judgment; within a step, the fix-forward loop runs continuously. **Existing designs** covering this region (namespace-resolution-design, the layering repoint design, and kin) are quarry — terminal shapes and mechanisms are evidence; their sequencing never defers the deletion (operator ruling, 2026-08-15; the 2026-08-25 reordering above is the same authority moving the grammar step, not a quarried design deferring it — the distinction this clause exists to enforce). ## The cut, stated in .dag terms diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index c7fe811ee44..4c1926f1580 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -462,6 +462,23 @@ fn run() -> Result { phase_failures .push(format!("declarations ({} finding(s))", findings.len())); } + // THE PHASE ROSTER JOIN RIDES THE SAME INGESTION. The substrate authority + // for phase identity is `gunbc.required_ci_phase_roster` `RequiredCiPhase`; + // this enum is its declared parallel realization, and the two are joined by + // variant-set equality in both directions on every required run — the same + // shape as the wave wall's vocabulary join, for the same DESIGN §3 reason. + // A phase declared and not realized, or realized and not declared, stops + // the line here rather than diverging silently. + let roster_findings = phase_roster_findings(&sweep.index); + for finding in &roster_findings { + eprintln!("required-ci: phase-roster FAIL {finding}"); + } + if !roster_findings.is_empty() { + phase_failures.push(format!( + "phase-roster ({} finding(s))", + roster_findings.len() + )); + } } Err(errors) => { for e in &errors { @@ -1070,6 +1087,69 @@ const REQUIRED_CI_PHASES: [RequiredCiPhase; 4] = [ RequiredCiPhase::Floor, ]; +/// The `.dag` coproduct this enum realizes, and the declaration whose variants it must equal. +/// `gunbc.required_ci_phase_roster` is the substrate authority for phase identity and lane +/// ownership; this enum, its `lane` match and `REQUIRED_CI_PHASES` are its declared parallel +/// realization, scheduled to delete atomically when the workflow emission consumes the roster +/// whole (`gunbc.required_ci_host_verdict_census` `required_ci_phase_roster_next_rung`). +const PHASE_ROSTER_AUTHORITY_MODULE: &str = "gunbc.required_ci_phase_roster"; +const PHASE_ROSTER_AUTHORITY_DECL: &str = "RequiredCiPhase"; + +/// Every phase this binary realizes, in the authority's own variant spelling. +const PHASE_ROSTER_VARIANT_LABELS: [&str; 4] = [ + "ParsePhase", + "NamespaceWaveAdmissionPhase", + "RegenPhase", + "FloorPhase", +]; + +/// Refuse if the host phase enum and the `.dag` phase roster disagree — the same both-directions +/// variant-set join `namespace_wave_admission::vocabulary_findings` executes against its own +/// authority, for the same reason: a second representation diverges on the first amendment, and +/// nothing else joins these two. An absent authority module refuses too — that is the state in +/// which nothing is checking the roster, not permission to proceed. +/// +/// WHAT THIS JOIN DELIBERATELY DOES NOT COVER: lane ownership. The host `lane` match is not +/// readable from the declaration index, and a lane divergence cannot un-enrol a phase — both +/// lanes execute in every required run — so the residue is bounded to which job carries a phase, +/// and its terminal is the atomic deletion the roster's census row names. +fn phase_roster_findings( + index: &v1_compiler::cli_run::declaration_index::DeclarationIndex, +) -> Vec { + use std::collections::BTreeSet; + let Some(record) = + v1_compiler::cli_run::declaration_index::index_get(index, PHASE_ROSTER_AUTHORITY_MODULE) + else { + return vec![format!( + "the phase-roster authority `{PHASE_ROSTER_AUTHORITY_MODULE}` is absent from the \ + index, so nothing joins this host phase enum to the roster it realizes" + )]; + }; + let Some(authored) = record.decl_fields.get(PHASE_ROSTER_AUTHORITY_DECL) else { + return vec![format!( + "`{PHASE_ROSTER_AUTHORITY_MODULE}` declares no `{PHASE_ROSTER_AUTHORITY_DECL}`" + )]; + }; + let here: BTreeSet = PHASE_ROSTER_VARIANT_LABELS + .iter() + .map(|l| l.to_string()) + .collect(); + let mut findings = Vec::new(); + for missing in authored.difference(&here) { + findings.push(format!( + "`{PHASE_ROSTER_AUTHORITY_DECL}` declares `{missing}` and this host enum does not \ + realize it — a phase enrolled with no executor" + )); + } + for extra in here.difference(authored) { + findings.push(format!( + "this host enum realizes `{extra}` and `{PHASE_ROSTER_AUTHORITY_DECL}` does not \ + declare it — a phase running with no authority" + )); + } + findings +} + /// EVERY PHASE IS ACCOUNTED FOR IN EVERY RUN, whether or not this lane owns it. /// /// A lane that simply omitted the other lane's phases would produce a ledger in which "this diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index a656d1ec5a4..71e27b15b99 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -5040,7 +5040,7 @@ fn entry_file_touched_via_import_closure( } /// Receipted Rust mirror of the single authority `v2.std.live_read.live_read_carrier_homes_v0` -/// (`src/v2/std/live_read.dag`) — the module names of the 8 declared live-read carrier homes. +/// (`src/v2/std/live_read.dag`) — the module names of the declared live-read carrier homes. /// Kept in lockstep with that `.dag` roster by hand; a drift here under-approximates axis (iv) /// fail-closed-safe direction only if this list is a SUPERSET of the `.dag` roster, so any /// addition to the `.dag` roster must be mirrored here — the drift gate below @@ -5063,6 +5063,7 @@ const LIVE_READ_CARRIER_HOME_MODULES_V0: &[&str] = &[ "v2.lens.module_graph", "tools.dag_compile_clean_shard_roster", "tools.dag_compile_clean_scope", + "gunbc.namespace_cut_subject_observation", ]; fn runtime_data_dependency_touched_via_carrier_closure( diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index 841e4f733fd..3278139ea7d 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -408,58 +408,35 @@ pub struct TransitionAdmission { /// module, enclosing declaration and leaf, blast radius 0 on every one. DISSOLVE-ON: #9675 /// merging -- base and head then both carry the relocation, the rows report stale, and they are /// removed by that trigger exactly as the four shrinks above were. +/// FIFTH SHRINK, SAME RULE (2026-08-30). #9675 merged (e1905850789), so on every pull_request +/// build from here the merge base and head both carry the relocation, no run can produce the +/// deltas the six rows above named, and they report stale -- refusing every PR. Removed by +/// the trigger they were authored with, in the first merge of main that carried the +/// relocation on both sides. +/// SIXTH POPULATION, SAME RULE (2026-08-29, #9698). Two rows for the `RequiredCiLane` move: +/// `BuildLane` and `WitnessesLane` moved (not duplicated) from +/// `gunbc.required_ci_host_verdict_census` to the new `gunbc.required_ci_phase_roster` -- +/// which the census itself named as its next rung -- so the census's +/// `required_ci_host_verdict_rows` now binds those spellings through the roster. +/// `TargetChanged` firing on a deliberate declaration move is the wall working; these rows +/// adjudicate exactly those two subjects and nothing else. They go STALE the moment #9698 +/// merges and MUST be removed then, exactly as the shrinks above were. pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ TransitionAdmission { - label: "rust-source-prefix-relocation-01", + label: "required-ci lane vocabulary moved to its declared next-rung authority (#9698)", subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_product_reachability", - in_declaration: "path_is_test_harness", - spelling: "rust_source_prefix_stage0_test", + module: "gunbc.required_ci_host_verdict_census", + in_declaration: "required_ci_host_verdict_rows", + spelling: "BuildLane", }, disposition: NamespaceDeltaDisposition::TargetChanged, }, TransitionAdmission { - label: "rust-source-prefix-relocation-02", + label: "required-ci lane vocabulary moved to its declared next-rung authority (#9698)", subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_product_reachability", - in_declaration: "path_is_test_harness", - spelling: "rust_source_prefix_test_harness", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: "rust-source-prefix-relocation-03", - subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_source_lifecycle_scaffold", - in_declaration: "rust_source_discovery_prefix_hints", - spelling: "rust_source_prefix_stage0_example", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: "rust-source-prefix-relocation-04", - subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_source_lifecycle_scaffold", - in_declaration: "rust_source_discovery_prefix_hints", - spelling: "rust_source_prefix_stage0_test", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: "rust-source-prefix-relocation-05", - subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_source_lifecycle_scaffold", - in_declaration: "rust_source_discovery_prefix_hints", - spelling: "rust_source_prefix_test_harness", - }, - disposition: NamespaceDeltaDisposition::TargetChanged, - }, - TransitionAdmission { - label: "rust-source-prefix-relocation-06", - subject: AdmissionSubject::Binding { - module: "gunbc.stage0_rust_source_lifecycle_scaffold", - in_declaration: "rust_source_discovery_prefix_hints", - spelling: "rust_source_prefix_tooling", + module: "gunbc.required_ci_host_verdict_census", + in_declaration: "required_ci_host_verdict_rows", + spelling: "WitnessesLane", }, disposition: NamespaceDeltaDisposition::TargetChanged, }, diff --git a/src/v2/std/live_read.dag b/src/v2/std/live_read.dag index 2ed4539017e..27024412708 100644 --- a/src/v2/std/live_read.dag +++ b/src/v2/std/live_read.dag @@ -52,7 +52,8 @@ data live_read_carrier_homes_v0: List = [ LiveReadCarrierHome { module: "v2.std.decl_index", kind: DeclFactsReflectionCarrier }, LiveReadCarrierHome { module: "v2.lens.module_graph", kind: ModuleDeclarationFactsCarrier }, LiveReadCarrierHome { module: "tools.dag_compile_clean_shard_roster", kind: ModuleDeclarationFactsCarrier }, - LiveReadCarrierHome { module: "tools.dag_compile_clean_scope", kind: ModuleDeclarationFactsCarrier } + LiveReadCarrierHome { module: "tools.dag_compile_clean_scope", kind: ModuleDeclarationFactsCarrier }, + LiveReadCarrierHome { module: "gunbc.namespace_cut_subject_observation", kind: DeclFactsReflectionCarrier } ] data live_read_carrier_callee_symbols_v0: List = [