Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
1f6539e
Feed the repair census envelope into legacy baseline capture and pers…
Sep 12, 2026
9ebb95d
Hold CaptureAvailable until a live repair observation tap exists.
Sep 12, 2026
fcd46fa
Give enrolment outstanding one fold and stop calling XL-1 persisted.
Sep 12, 2026
dab7f65
Refuse a capture whose repair observation is not of the same tree sub…
Sep 12, 2026
6dfcf30
Admit the XL-1 emit-rust repair-row interpreter bridge so v2 can pers…
Sep 12, 2026
36d855d
Widen the XL-1 bridge to PrimaryRoot and execute it.
Sep 12, 2026
a136d01
Name repair-subject disagreement with the existing subject-field copr…
Sep 12, 2026
ca8c008
Keep the PrimaryRoot tap host-private behind the one builtin.
Sep 12, 2026
70c1039
Merge origin/main after freeze release (#10940).
Sep 12, 2026
26ffe1d
Give the repair-row coproduct one dag home and refuse tap failure as …
Sep 12, 2026
4af31e1
Merge origin/main into XL-1 repair-tap.
Sep 13, 2026
42323e5
Give ReferenceDerivedCandidateRow its generated module home.
Sep 13, 2026
fd2e514
Name repair-subject disagreement with the existing subject-field copr…
Sep 12, 2026
2608bc6
Make XL-1 capture capable and enroll a persisted carrier against a pin.
Sep 13, 2026
33d1e1b
Keep the production pre-cut pin unpinned until ACT-0 names the base.
Sep 13, 2026
3123d86
Drop dangling XL-1 persist aliases, dissolution String, and the uninh…
Sep 13, 2026
f90ab07
Roster the XL-1 emit_host host on the seed-growth justification.
Sep 13, 2026
16a92bb
Make the remaining capture-refusal arm a unit variant so it inhabits.
Sep 13, 2026
8ffcf32
Merge session/stern-ram-86 after the 11203 coproduct/RED fix.
Sep 13, 2026
6dc257b
Carry repair-subject divergence as a typed field, not a decoded String.
Sep 13, 2026
ce3b70a
Merge session/stern-ram-86 after typed repair-subject divergence (rev…
Sep 13, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 17 additions & 23 deletions dag/gunbc/compiler_frontend_program_status.dag
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,9 @@ import v2.workflow.legacy_baseline_capture {
legacy_baseline_capture_capability,
capture_blocked_reason,
}
import v2.workflow.legacy_baseline_persisted_observation {
persisted_legacy_baseline_outstanding,
}
import gunbc.required_ci_phase_roster {
RequiredCiPhase,
NamespaceWaveAdmissionPhase,
Expand Down Expand Up @@ -166,7 +169,6 @@ fn observe_outstanding(subject: NonEmptyStr, outstanding: List<String>) -> Miles
// milestone -- stages_awaiting joins it.
type MissingInstrument
= PhaseCargoExecutionFact
| PersistedLegacyBaselineObservation
| DeclaringIdentitySpellingCensus
| RepairInputOriginRosterProducer
| ExactOccurrenceResidualCensus
Expand All @@ -178,7 +180,6 @@ type MissingInstrument
fn missing_instrument_label(i: MissingInstrument) -> String {
match i {
PhaseCargoExecutionFact => "a per-phase cargo-execution fact on gunbc.required_ci_phase_roster"
PersistedLegacyBaselineObservation => "an admitted CompleteLegacyObservation persisted against a named base"
DeclaringIdentitySpellingCensus => "a census of occurrences not spelled at their declaring identity (XL-3's population)"
RepairInputOriginRosterProducer => "a repair-input origin roster producer: source-declaration carriers plus rendered target-vocabulary carriers, separately typed, over one base, before eligibility or repair disposition (XL-0's population)"
ExactOccurrenceResidualCensus => "the exact occurrence and import-declaration residual an XL-2 rehearsal produces (XL-5's population)"
Expand Down Expand Up @@ -254,7 +255,6 @@ type InstrumentObstacle
fn missing_instrument_obstacle(i: MissingInstrument) -> InstrumentObstacle {
match i {
PhaseCargoExecutionFact => NotBuilt
PersistedLegacyBaselineObservation => NotBuilt
DeclaringIdentitySpellingCensus => NotBuilt
RepairInputOriginRosterProducer => NotBuilt
ExactOccurrenceResidualCensus => NotBuilt
Expand Down Expand Up @@ -402,11 +402,10 @@ fn stage_subject_outstanding(stage: NamespaceCutStage) -> List<String> {
// 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.
// work behind the missing-instrument label. The AVAILABLE arm reads the persist outstanding
// fold: v2.workflow.legacy_baseline_persisted_observation holds a capture by its own
// GitObjectId, never a receipts roster. Production pin stays PreCutBaseUnpinned until ACT-0
// names B; the AVAILABLE arm is outstanding until then. That is not ACT-0's BaselineCaptureReceipt.
// 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
Expand Down Expand Up @@ -484,10 +483,12 @@ fn milestone_status(m: ProgramMilestone) -> MilestoneStanding {
)
)
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 -- and the capture module itself rules out a receipts roster as a relabel-unsafe durable form." as NonEmptyStr,
cause: needs(i: PersistedLegacyBaselineObservation)
}
standing_from_evidence(
e: observe_outstanding(
subject: "namespace Step 0.5 / XL-1: baseline capture against the current pre-cut base" as NonEmptyStr,
outstanding: persisted_legacy_baseline_outstanding()
)
)
}
NamespaceFirstSemanticWave =>
NotDerivable {
Expand Down Expand Up @@ -720,7 +721,6 @@ fn join_names(names: List<String>) -> String {
// ---------------------------------------------------------------------------------------------
data all_missing_instruments: List<MissingInstrument> = [
PhaseCargoExecutionFact,
PersistedLegacyBaselineObservation,
DeclaringIdentitySpellingCensus,
RepairInputOriginRosterProducer,
ExactOccurrenceResidualCensus,
Expand All @@ -742,16 +742,10 @@ fn milestone_missing_instruments(m: ProgramMilestone) -> List<MissingInstrument>
}
}

// 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<MissingInstrument> = [
PersistedLegacyBaselineObservation,
]
// Conditional await remains for instruments whose citing arm is not live on every standing.
// PersistedLegacyBaselineObservation retired: the persist producer exists and the baseline
// milestone reads its outstanding fold directly.
data conditionally_awaited_instruments: List<MissingInstrument> = []

fn milestones_awaiting(i: MissingInstrument) -> List<String> {
fold(program_milestones, init: [], f: fn(acc, m) {
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
module gunbc.emit_rust_reference_derived_rows_bridge_seed_growth

import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.types { String }
import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }

data emit_rust_reference_derived_rows_bridge_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef {
module_path: "v1_compiler.cli_run.emit_host",
decl_name: "Xl1PrimaryRootTap",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.cli_run.emit_host",
decl_name: "compile_xl1_primary_root_tap",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.cli_run.emit_host",
decl_name: "ObservedOccurrenceBindingHalves",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.cli_run.emit_host",
decl_name: "observed_occurrence_transport_and_bindings",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_interpreter",
decl_name: "reference_derived_candidate_rows_value",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_interpreter",
decl_name: "reference_derived_candidate_disposition_value",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_interpreter",
decl_name: "occurrence_transport_value",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_interpreter",
decl_name: "xl1_primary_root_tap_value",
field: WholeDeclaration
}
],
reason: "WHY A HOST BRIDGE RATHER THAN A .dag CONSUMER CALLING THE PRODUCER DIRECTLY. The rows are produced by v1.compiler.emit_rust emit_rust_reference_derived_rows over a ResolvedGraph. The required floor and every dag/src/v2 workflow resolve --source-root dag --source-root src/v2 only. Measured: no module under those roots imports a v1 module, so a consumer there cannot name that function. Adding --source-root src/v1 lets the spelling resolve; calling it from the interpreter still needs a ResolvedGraph, and compile_to_resolved over an authored source vector hits the Node.ident wall (no default for an omitted optional field).\n\nWHY PRIMARYROOT, MEASURED. gunbc run / claim_executor compile_to_resolved only the entry's reference-derived closure (resolve_entry_with_index). The one existing path that compile_to_resolved every indexed module under a root is gunbc compile without --entry (CompileSubject::PrimaryRoot). That transaction emits bytes and never called this arm. compile_dag_reference_occurrence_binding_census compiles a caller-supplied (paths, contents) vector and does not encode OccurrenceTransport (no containment, declarations, or index entries), so ValidatedOccurrenceTransport cannot mint from it. This widening keeps ONE arm and ONE encoding: PrimaryRoot(source_roots[0]) with the rest as pool, then encode repair rows AND the seed-observed OccurrenceTransport (per-module sidecars concatenated as stored; never reconstructed on the v2 side). Binding rows over that same transport travel in the same encoding. If occurrence_transport_validate cannot mint, capture refuses LegacyBaselineObservedTransportRefused rather than fabricating containment.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits by PURPOSE (fierce-lark-661, PrimaryRoot widening 2026-09-12). The v1 oracle is the differential referent for the XL-6 qualification sweep. HAND-ITEM DELTA is the identities in hand_authored_declarations: the emit_host host (Xl1PrimaryRootTap, compile_xl1_primary_root_tap) plus the ObservedOccurrenceBindingHalves extraction that compile_dag_reference_occurrence_binding_census now shares, plus the four v1_interpreter encoders. The dispatch arm is ExistingSeedItemModified inside eval_builtin_inner. v1_interpreter_dispatch_generated.rs is generated from gunbc.v1_interpreter_primitive_surface.",
owning_dissolution_lane: "v1-interpreter-delete" as RoadmapNodeId,
trigger: "Delete this arm with v1.compiler.emit_rust and the interpreter. A producer existing is not the dissolve; the arm is listed in that deletion population from the day it lands.",
current_boundary: "src/v1/stage0/src/cli_run/emit_host.rs compile_xl1_primary_root_tap (Xl1PrimaryRootTap, ObservedOccurrenceBindingHalves, observed_occurrence_transport_and_bindings); src/v1/stage0/src/v1_interpreter.rs free_call.emit_rust_reference_derived_rows_bridge arm and its encoders (repair rows, seed-observed OccurrenceTransport, binding rows over that transport); dag/gunbc/v1/v1_interpreter_primitive_surface.dag roster row; src/v1/04_method.dag builtin signature; dag/std/primitives.dag spelling roster; sole consumer v2.workflow.legacy_repair_tap persist_named_base_from_primary_root_tap"
}
2 changes: 1 addition & 1 deletion dag/gunbc/namespace/namespace_cut_stage.dag
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ 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: repair-input origin denominator -- source-declaration carriers plus rendered target-vocabulary carriers, separately typed, over one base, before eligibility or repair disposition" 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
StageXL1BaselineCapture => "XL-1: capture capability -- the capture transaction can mint a joint binding+repair observation over one exact base; persistence against a named base is the baseline milestone, not this stage" 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
Expand Down
22 changes: 22 additions & 0 deletions dag/gunbc/namespace/reference_derived_candidate.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module gunbc.reference_derived_candidate

import std.types { String }

// THE EMIT-RUST REFERENCE-DERIVED CANDIDATE, ONE HOME. v1.compiler.emit_rust produces rows of this
// shape; v2.workflow.legacy_repair_tap consumes the same types through the host bridge. Reachability
// of ResolvedGraph explains the bridge, not a second copy of the coproduct (review 64840).

type ReferenceDerivedCandidateDisposition
= CandidateSurvived { provider_module: String }
| CandidateOwnModule
| CandidateVariantDelegatedToParent { parent_enum: String }
| CandidateVariantParentUnresolved
| CandidateRegistryAbsent
| CandidateLeafAmbiguous
| CandidateExportProofFailed { provider_module: String }

type ReferenceDerivedCandidateRow {
module_name: String
name: String
disposition: ReferenceDerivedCandidateDisposition
}
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ import gunbc.declaration_lookup_index_seed_growth { declaration_lookup_index_see
import gunbc.emitted_closure_compile_seed_growth { emitted_closure_compile_seed_growth_justification }
import gunbc.evaluation_budget_falsifier_seed_growth { evaluation_budget_falsifier_seed_growth_justification }
import gunbc.namespace_structural_observation_bridge_seed_growth { namespace_structural_observation_bridge_seed_growth_justification }
import gunbc.emit_rust_reference_derived_rows_bridge_seed_growth { emit_rust_reference_derived_rows_bridge_seed_growth_justification }
import gunbc.parsed_import_statement_bridge_seed_growth { parsed_import_statement_bridge_seed_growth_justification }
import gunbc.namespace_wave_admission { namespace_wave_admission_seed_growth_justification }
import gunbc.parse_refusal_location_seed_growth { parse_refusal_location_seed_growth_justification }
Expand Down Expand Up @@ -244,6 +245,7 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
emitted_closure_compile_seed_growth_justification,
evaluation_budget_falsifier_seed_growth_justification,
namespace_structural_observation_bridge_seed_growth_justification,
emit_rust_reference_derived_rows_bridge_seed_growth_justification,
parsed_import_statement_bridge_seed_growth_justification,
namespace_wave_admission_seed_growth_justification,
qualified_pipe_callee_seed_growth_justification,
Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/v1/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1195,6 +1195,15 @@ fn v1_interpreter_authored_roster_arms() -> List<InterpreterPrimitiveDispatchArm
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.emit_rust_reference_derived_rows_bridge" },
form: FreeCall,
authored_spelling: "emit_rust_reference_derived_rows_bridge",
realization_module: "v1_interpreter",
dispatch_symbol: "eval_builtin_inner",
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.compile_dag_rust_emit_check" },
form: FreeCall,
Expand Down
1 change: 1 addition & 0 deletions dag/std/primitives.dag
Original file line number Diff line number Diff line change
Expand Up @@ -621,6 +621,7 @@ fn builtin_registry_surface_names() -> List<String> {
"compile_dag_rust_emit_check",
"parsed_import_statements",
"namespace_structural_observation_admissions",
"emit_rust_reference_derived_rows_bridge",
"witness_layer_roots_compile_clean_check",
"witness_layer_roots_compile_clean_emit_check",
"install_or_consume_floor_compile_clean_gate_receipt",
Expand Down
21 changes: 13 additions & 8 deletions dag/test/claim/compiler_frontend_program_status_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,9 @@ import v2.workflow.legacy_baseline_capture {
legacy_baseline_capture_capability,
capture_blocked_reason,
}
import v2.workflow.legacy_baseline_persisted_observation {
persisted_legacy_baseline_outstanding,
}
import v2.compiler.self_host.stage0_crate_layout { emitter_produced_divergent_registrations }
import gunbc.compiler_frontend_program_status {
milestone_missing_instruments,
Expand Down Expand Up @@ -586,9 +589,8 @@ test fn xl0_is_not_derivable_and_awaits_the_repair_input_origin_producer() -> Bo
// THE SAME QUESTION. XL-1 used to delegate to NamespaceBaselineObservationComplete outright, which
// made "the capture transaction can succeed" and "a capture has been taken against THIS base" one
// row. They separate exactly on the CaptureAvailable arm: the stage clears (its deliverable is the
// capability) while the milestone becomes NOT-DERIVABLE (no persisted observation against the
// current base). This arm asserts the contract on whichever arm is live, so it does not red when
// the capability legitimately becomes available -- it reds if the two are re-fused.
// capability) while the milestone reads persisted_legacy_baseline_outstanding (production pin
// unpinned until ACT-0 names a base). This arm asserts the contract on whichever arm is live.
test fn xl1_follows_the_capability_while_the_baseline_milestone_follows_the_base() -> Bool {
match legacy_baseline_capture_capability() {
CaptureBlocked { phase: p, cause: c } =>
Expand All @@ -597,7 +599,9 @@ test fn xl1_follows_the_capability_while_the_baseline_milestone_follows_the_base
expected: capture_blocked_reason(c: CaptureBlocked { phase: p, cause: c }))
CaptureAvailable =>
standing_is(want: ClassClear, s: stage_status(s: StageXL1BaselineCapture))
&& standing_is(want: ClassNotDerivable, s: milestone_status(m: NamespaceBaselineObservationComplete))
&& standing_agrees_with_population(
s: milestone_status(m: NamespaceBaselineObservationComplete),
expected: persisted_legacy_baseline_outstanding())
}
}

Expand Down Expand Up @@ -655,17 +659,18 @@ test fn the_wave_admission_milestone_is_wired_to_the_phase_roster() -> Bool {
}

// 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).
// blocked the milestone must carry exactly the capability fold's reasons; when capture is available
// it must carry the persist outstanding fold.
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))
standing_agrees_with_population(
s: milestone_status(m: NamespaceBaselineObservationComplete),
expected: persisted_legacy_baseline_outstanding())
}
}

Expand Down
Loading