diff --git a/dag/gunbc/floor/floor_route_gap_seed_growth.dag b/dag/gunbc/floor/floor_route_gap_seed_growth.dag index e61f79d976b..8ec18ca41a3 100644 --- a/dag/gunbc/floor/floor_route_gap_seed_growth.dag +++ b/dag/gunbc/floor/floor_route_gap_seed_growth.dag @@ -5,16 +5,16 @@ import gunbc.seed_growth { SeedGrowthJustification } import std.decl_ref { DeclarationRef, WholeDeclaration } // FORWARD-FREEZE RECEIPT for the typed route-gap expectation consumed by the required floor. -// The modeled authority is v2.workflow.floor_route_gap FloorRouteGapExpectation; these three +// The modeled authority is v2.workflow.floor_route_gap FloorRouteGapExpectation; these four // declarations are its seed-side realization at the interpreter boundary, not a second policy. data floor_route_gap_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { hand_authored_declarations: [ - DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "FloorRouteGapExpectedGround", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "FloorRouteGapExpectation", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "floor_route_gap_expectation_mismatch", field: WholeDeclaration } - ], - reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed, and v1_compiler.cli_run is the boundary that receives v1_interpreter.HermeticEffectGround after a claim executes. v2.workflow.floor_route_gap owns the expectation vocabulary and population; the Rust realization decodes that authority and refuses when the observed operation or closed ground differs, instead of letting an identity-only enrollment absorb changed evidence. A modeled row without this consumer cannot constrain the host terminal ledger.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The required floor is the instrument guarding that program, and this change strengthens a pre-existing route-gap debt roster from identity-only agreement to operation-and-ground agreement. It adds no language behavior, compatibility route, escape hatch, seed feature, or emitted public surface.\n\nHAND-ITEM DELTA: +3, exactly the closed ground mirror, the decoded expectation record, and the pure mismatch classifier enumerated above. All other Rust edits are inside existing declarations and are ExistingSeedItemModified.\n\nHAND-LOC DELTA AT THIS RECEIPT: src/v1/stage0/src/cli_run.rs +223/-49 and src/v1/stage0/src/bin/claim_executor.rs +5/-5 against origin/main. The latter adds no declaration. The item observation producer is currently absent, so these diff-derived figures remain review evidence rather than a mechanically joined admission.", + DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "ROUTE_GAP_ADMISSION_PARTITION_ENTRY", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_suppressed_rows_value", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_declared_map_value", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "route_gap_admission_decode_and_enforce", field: WholeDeclaration } + ], reason: "WHY RUST IS STILL NEEDED: the required floor executes in the seed, and v1_compiler.cli_run is the boundary that receives v1_interpreter.HermeticEffectGround after a claim executes. v2.workflow.floor_route_gap owns the expectation vocabulary and population; the Rust realization decodes that authority and refuses when the observed operation or closed ground differs, instead of letting an identity-only enrollment absorb changed evidence. A modeled row without this consumer cannot constrain the host terminal ledger.\n\nWHY THE ADMISSION PARTITION IS MODELED, WITH FOUR COUNTED HAND ITEMS: the partition decision — INCLUDING the membership judgment — is modeled on the authority itself: v2.workflow.floor_route_gap.floor_route_gap_admission_partition, the single implementation of the route-gap admission decision, receives the discovery walk's declared-identity index WHOLE AS A KEYED MAP and asks map_contains_key per suppressed row, so refuse-if-undeclared is decided by the .dag relation, not by the marshal. The runner does no membership test: a Rust-side contains_key would BE the judgment made outside the authority, and flattening the index into a list for the .dag to linearly re-scan was the corpus-sized join this shape retires (a per-row linear contains over the required-run census — declared in the tens of thousands, suppressed in the hundreds — is millions of interpreted string comparisons per required run, the cost-shape defect DESIGN.md §6 always fixes; the keyed map keeps the judgment in .dag at one O(1) lookup per suppressed row). An earlier revision carried a Rust classifier (route_gap_suppressed_undeclared) beside the modeled relation; it was DELETED rather than kept beside the .dag call, so the decision — membership and arms both — has one implementation and the seed decision surface shrank by that classifier. What feeds the relation and enforces its answer could not vanish with it: the entry name the run site and the pairing witness share (ROUTE_GAP_ADMISSION_PARTITION_ENTRY), the shared suppressed-row marshal (route_gap_suppressed_rows_value), the shared declared-index marshal (route_gap_declared_map_value, which spells the index's disposition values through required_floor_disposition_label), and the shared production decode+enforce (route_gap_admission_decode_and_enforce, extracted from run_required_floor so the misnamed fixture's refusal flows through the actual production branch) are four new module-scope seed items, counted in the delta below. The row marshal's ground decoding is inlined in that marshal, the arm-for-arm spelling after v2.workflow.floor_route_gap FloorRouteGapSuppressionGround, so a rename on either side breaks the pairing instead of forking the vocabulary.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The required floor is the instrument guarding that program, and this change strengthens a pre-existing route-gap debt roster from identity-only agreement to operation-and-ground agreement, and closes its undeclared-enrollment hole. It adds no language behavior, compatibility route, escape hatch, seed feature, or emitted public surface.\n\nHAND-ITEM DELTA: +4, all in v1_compiler.cli_run.required_floor_runner and all enumerated above: the shared entry name (ROUTE_GAP_ADMISSION_PARTITION_ENTRY), the shared suppressed-row marshal (route_gap_suppressed_rows_value), the shared declared-index marshal (route_gap_declared_map_value), and the shared production decode+enforce (route_gap_admission_decode_and_enforce — the branch run_required_floor executes on the partition's answer, extracted so the pairing test drives the SAME function and the misnamed fixture produces the actual REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared). The arm spelling inside the suppressed-row marshal is inlined (no nested hand declaration). All other Rust edits are inside existing declarations and are ExistingSeedItemModified.\nHAND-LOC CENSUS, BEFORE AND AFTER, AT THIS RECEIPT: against origin/main, `git diff --numstat origin/main..HEAD` over the eight files of this PR re-derives 1164 insertions and 15 deletions; the seed realization's own line count in v1_compiler.cli_run/required_floor_runner.rs moves by +638/-7 (production +256/-7, the #[cfg(test)] pairing witness and its tests +380). The item observation producer is currently absent, so this diff-derived census remains review evidence rather than a mechanically joined admission.\n\nHAND-LOC DELTA AT THIS RECEIPT, all eight files: src/v1/stage0/src/cli_run/required_floor_runner.rs (call-site marshals + modeled-partition call + shared decode+enforce, per-identity measurement record, refusal, pairing witness through run_in_context_with_args, tests), src/v2/workflow/floor_route_gap.dag (contract amendment + the modeled partition), src/v2/workflow/required_floor.dag (one exact-grain authored-module row for test.claim.route_gap_partition_witness), src/v2/test/fixture/route_gap_admission_partition.dag (the shared fixture: four rows, both arms, all three grounds), dag/test/claim/route_gap_partition_witness_test.dag (the floor-side route witness), dag/gunbc/floor/floor_route_gap_seed_growth.dag (this receipt), dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag (the unimported-bare-name divergence row), docs/plans/route-gap-dormant-observation.md (the finding doc). The item observation producer is currently absent, so these diff-derived figures remain review evidence rather than a mechanically joined admission.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, - trigger: "Delete the three seed declarations when the self-emitted claim executor executes the required floor and consumes v2.workflow.floor_route_gap FloorRouteGapExpectation directly; the modeled expectation then remains the sole authority and the hand-written decode/classifier disappears with the v1 floor bridge.", - current_boundary: "v2.workflow.floor_route_gap FloorRouteGapExpectation -> v1_compiler.cli_run FloorRouteGapExpectation -> v1_compiler.cli_run floor_route_gap_expectation_mismatch -> v1_compiler.cli_run run_required_floor" + trigger: "Delete the four seed declarations when the self-emitted claim executor executes the required floor and consumes v2.workflow.floor_route_gap FloorRouteGapExpectation directly; the modeled expectation, the modeled admission partition, and its declared ground coproduct then remain the sole authorities and the hand-written decode/classifier disappears with the v1 floor bridge.", + current_boundary: "v2.workflow.floor_route_gap FloorRouteGapExpectation and floor_route_gap_admission_partition -> v1_compiler.cli_run FloorRouteGapExpectation -> v1_compiler.cli_run.required_floor_runner floor_route_gap_expectation_mismatch and the run-site marshals -> v1_compiler.cli_run run_required_floor" } diff --git a/dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag b/dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag new file mode 100644 index 00000000000..ce0cea0e4c7 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/an_unimported_bare_name_binds_differently_per_realization.dag @@ -0,0 +1,24 @@ +module gunbc.recurring_failure_mode.an_unimported_bare_name_binds_differently_per_realization + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +// AN UNIMPORTED BARE VALUE NAME IS RESOLVED TWICE -- once per realization of the language -- and +// the two resolutions have different fallback rules, so one name can mean two functions. The +// interpreter's search over declaring modules and the emitter's mapping to runtime builtins are +// two realizations of one resolution decision, and nothing forces them to agree: where the +// arities happen to differ the emitted build refuses (loud, costly, caught late), and where they +// happen to match the program compiles and SILENTLY runs the wrong function in one realization. +// The wall is the authored import: an imported name has one binding by construction, while a +// bare name with no import anywhere is a resolution the author never made. +data an_unimported_bare_name_binds_differently_per_realization: RecurringFailureMode = RecurringFailureMode { + identity: "an_unimported_bare_name_binds_differently_per_realization" as NonEmptyStr, + receipts: [ + "SPECIMEN, FOUND 2026-10-05. `v2.workflow.floor_route_gap.floor_route_gap_admission_partition` (PR #13376) called `contains(xs: declared, item: row.identity, eq: floor_route_gap_string_eq)` WITHOUT importing `contains`. The interpreter resolved the bare name to `v2.std.algebra.contains` (the generic list-membership function, src/v2/std/algebra.dag:201) and every .dag-level claim and pairing lib test evaluated green. The emitter resolved the same bare name to `v1_rt::contains` -- the 2-parameter String substring builtin (src/v1_rt.rs:332) -- and lowered the call as `v1_rt::contains(declared.clone(), row.identity.clone(), floor_route_gap_string_eq)`, failing the emitted build with error[E0061] 'this function takes 2 arguments but 3 arguments were supplied' at emitted src/v2_workflow_floor_route_gap.rs:2139:106; the String/Rc> type note was the tell that the bound function was the substring builtin, not list membership.", + "WHY THE LOCAL BATTERY COULD NOT SEE IT: the interpreter's resolution is the only resolution every .dag-level check exercises, so a bare name that binds differently per realization evaluates consistently green on every interpreted lane; emission is the only lane that runs the emitter's fallback, which made CI's emit-build the sole discriminator. A green interpreter run is not evidence that a name means the same thing in the other realization.", + "WHY THE CORPUS DID NOT CATCH IT AT REVIEW: the corpus always imports this name (src/v2/lens/coverage.dag:3, src/v2/workflow/vocab.dag), so the unimported form contradicted the convention but enforced nothing -- a reader who assumed the convention was a rule saw nothing wrong in the module text.", + "REMEDY AT THE SOURCE: author the import so the name has one binding (`import v2.std.algebra { contains }`); in the specimen's final shape the call itself was retired by the keyed-map membership fix (side-chat review 5424676896 / review 76768), which is why the class guard is import discipline plus a resolution-time refusal, not any one call site. The class guard this row asks for, NARROWED TO THE FAILING CLASS: a bare VALUE name that has no local declaration, no import, and no admitted intrinsic -- a name that would otherwise bind through a realization-specific FALLBACK (the interpreter's declaring-module search, the emitter's runtime-builtin mapping, the two rules this specimen caught diverging) -- refuses at resolution time with a typed, located cause ('bare name X is not imported and names no intrinsic'); bare names the language admits as intrinsics in every realization (map, fold, count, the emitter-handled builtins) are legitimate unimported and stay outside the guard, as does any name imported somewhere visible. The existing ambiguity wall (claim_scope_for's AmbiguousBareNameRead) fires only when two declarers are visible, and an unimported non-intrinsic name with one declarer visible per realization is not ambiguous, just different.", + "NEXT-RUNG TRIGGER: the loader's bare-channel decision carried as a substrate fact -- per declined bare name, the declining arm and the declaring module -- is the observation that would make 'resolved by fallback' readable at one authority (the bare_reference_channel_outcome_seed_growth trigger); the resolution-time refusal above is what closes the class." + ], + evidence: [], +} diff --git a/dag/test/claim/route_gap_partition_witness_test.dag b/dag/test/claim/route_gap_partition_witness_test.dag new file mode 100644 index 00000000000..a619136d542 --- /dev/null +++ b/dag/test/claim/route_gap_partition_witness_test.dag @@ -0,0 +1,140 @@ +module test.claim.route_gap_partition_witness + +import std.types { List, Bool, Int } +import v2.std.integer { int_add } +import v2.workflow.floor_route_gap { + FloorRouteGapAdmissionRow, + FloorRouteGapAdmissionMeasuredRow, + FloorRouteGapAdmissionRefusedRow, + FloorRouteGapSuppressionGround, + floor_route_gap_admission_partition, +} +import v2.test.fixture.route_gap_admission_partition { + route_gap_partition_fixture_suppressed, + route_gap_partition_fixture_expected, + partition_fixture_declared, + partition_fixture_decided, +} + +// THE ROUTE WITNESS for the route-gap admission partition (docs/plans/ +// route-gap-dormant-observation.md). The required floor's runner marshals the run's real values +// -- the identities suppression removed with the ground that removed each, and the discovery +// walk's declared-identity index WHOLE AS A KEYED MAP -- into `v2.workflow.floor_route_gap` +// `.floor_route_gap_admission_partition`, the modeled relation on the authority that owns the +// register; the membership judgment (`map_contains_key` per row) happens HERE, in the relation, +// not in the marshal, and the runner-side classifier this relation replaces was deleted, so +// this surface is the run site's only route to the answer. This claim drives that surface over +// the shared fixture (src/v2/test/fixture/route_gap_admission_partition.dag) and asserts both +// arms at identity grain on the floor: a declared suppressed row comes back MEASURED with its +// ground kept (the declared `FloorRouteGapSuppressionGround` arms, not free labels), and a +// misnamed enrollment -- renamed, deleted, or fabricated -- comes back REFUSED, the wall's +// discriminating arm. Substrate inputs only: constructed lists and maps through the modeled +// relation; no host effect, no service, no wet lane. The seed's pairing witness in +// `required_floor_runner` evaluates the same fixture rows through `run_in_context_with_args`, +// the real call path the run site uses. +fn measured_row_holds( + row: FloorRouteGapAdmissionRow, + identity: String, + ground: FloorRouteGapSuppressionGround +) -> Bool { + match row { + FloorRouteGapAdmissionMeasuredRow { identity: i, ground: g } => i == identity && g == ground + FloorRouteGapAdmissionRefusedRow { identity: _ } => false + } +} + +fn refused_row_holds(row: FloorRouteGapAdmissionRow, identity: String) -> Bool { + match row { + FloorRouteGapAdmissionMeasuredRow { identity: _, ground: _ } => false + FloorRouteGapAdmissionRefusedRow { identity: i } => i == identity + } +} + +fn count_measured_holding( + rows: List, + identity: String, + ground: FloorRouteGapSuppressionGround, +) -> Int { + fold(rows, init: 0, f: fn(acc, r) { + if measured_row_holds(row: r, identity: identity, ground: ground) { + int_add(a: acc, b: 1) + } else { + acc + } + }) +} + +fn count_refused_naming(rows: List, identity: String) -> Int { + fold(rows, init: 0, f: fn(acc, r) { + if refused_row_holds(row: r, identity: identity) { + int_add(a: acc, b: 1) + } else { + acc + } + }) +} + +// THE MEASUREMENT ARM, AT IDENTITY GRAIN, ACROSS ALL THREE DECLARED GROUNDS: a declared +// suppressed row keeps its ground and is named, never absorbed into a count. For identities +// whose module the 2026-08-29 gate cut withdrew this record closes nothing -- the gate decision +// owns their dormancy. Membership is judged by the relation against the fixture's keyed +// declared map. +test fn the_partition_measures_a_declared_suppressed_row_with_its_ground_kept() -> Bool { + let decided = floor_route_gap_admission_partition( + suppressed: route_gap_partition_fixture_suppressed, + declared: partition_fixture_declared(), + ) + count(decided) == 4 + && count_measured_holding( + rows: decided, + identity: "test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.a_holds", + ground: OutsideRequiredGate + ) == 1 + && count_measured_holding( + rows: decided, + identity: "test.claim.parse_test.parse_witness_floor_holds", + ground: WithheldCostDebt + ) == 1 + && count_measured_holding( + rows: decided, + identity: "test.claim.wet_lane_probe.wet_lane_declared_holds", + ground: DeclinedNoCiWetLane + ) == 1 +} + +// THE WALL'S DISCRIMINATING ARM: an enrollment the tree does not declare refuses. Suppression +// removes such a row before the reverse join, so no other guard can ever see it; the cheapest +// way to fake a green run -- enrolling an identity that does not exist -- must come back as a +// refusal, never as a count. +test fn the_partition_refuses_an_enrollment_the_tree_does_not_declare() -> Bool { + let decided = floor_route_gap_admission_partition( + suppressed: route_gap_partition_fixture_suppressed, + declared: partition_fixture_declared(), + ) + count(decided) == 4 + && count_refused_naming( + rows: decided, + identity: "test.claim.renamed_away_witness_test.old_witness_name" + ) == 1 +} + +// THE ANSWER MATCHES THE EXPECTED LIST AT IDENTITY GRAIN: the fixture's expected rows are +// consumed by the route the run site takes -- decided rows and expected rows name the same +// identities in the same arms with the same grounds, and the decided list carries nothing +// extra -- so "read by all three sides" is a claim the fixture itself discharges. +test fn the_decided_rows_agree_with_the_expected_rows_at_identity_grain() -> Bool { + let decided = partition_fixture_decided() + count(decided) == count(route_gap_partition_fixture_expected) + && fold( + route_gap_partition_fixture_expected, + init: true, + f: fn(acc, exp) { + acc && match exp { + FloorRouteGapAdmissionMeasuredRow { identity: i, ground: g } => + count_measured_holding(rows: decided, identity: i, ground: g) == 1 + FloorRouteGapAdmissionRefusedRow { identity: i } => + count_refused_naming(rows: decided, identity: i) == 1 + } + } + ) +} diff --git a/docs/plans/route-gap-dormant-observation.md b/docs/plans/route-gap-dormant-observation.md new file mode 100644 index 00000000000..9ce1fe57b84 --- /dev/null +++ b/docs/plans/route-gap-dormant-observation.md @@ -0,0 +1,199 @@ +# Where the route-gap population drops out of the required run — finding, then proposed repair + +Lane: calm-koi-257 (claim-execution-route). Status: finding complete; repair BUILT and under review on +PR #13376 (coordinator ack covered all four conditions; reviews 38602/76419/76431 addressed). + +## The population and the run + +`v2.workflow.floor_route_gap.floor_route_gap_roster` (authority: `src/v2/workflow/floor_route_gap.dag`) +enrolls identities the floor executes and that reach a host effect the hermetic route has no arm for +(`NoMockResponse` 420, `FilesystemRemoval` 10, `UnpublishedMockCase` 8 among the 425 typed rows; 100 more +as bare identity strings in chunks 00–05). 525 distinct identities across 146 modules; every one currently +resolves against the tree (verified per identity: module present, `test fn` tail present — zero stale rows +on current main; an earlier count of 2 stale rows was an artifact of my worktree lagging main and was +withdrawn). + +On required run 37236808750 (merge_group, pr-13305, floor job 111537440982): + + [floor-cost-debt] floor_route_gap: 5 enrolled identity(ies) suppressed (cost-debt roster withholds them) + [floor-required-gate] floor_route_gap: 536 enrolled identity(ies) suppressed (module outside the required gate, never loaded) + [floor-route-gap] roster carries 5 enrolled identity(ies) + [floor-route-gap] 5 enrolled identity(ies) held as route-gapped; 0 unenrolled route gap(s) reported + +Arithmetic: 546 decoded = 541 route-gap-roster rows + 5 gate-inside rows enrolled in the floor's +grandfathered roster (`v2.workflow.floor_grandfathered_roster`). The route-gap source on the run's merge +commit carried 421 typed rows + 120 legacy strings (= 541; current main carries 425 + 120); the 5 carried +rows — `parse_test.parse_witness_floor_holds`, `parse_test.parse_witness_perf_holds`, +`namespace_import_closure_witness.namespace_import_closure_receipt_holds`, +`namespace_structural_root_exposure_generated_witness_test.namespace_structural_root_exposure_generated_witness_holds`, +`v1_dag_parse_witness.v1_dag_parse_witnesses` — are not in the route-gap chunks at all; the floor's +grandfathered roster declares them as gate-inside enrollments, and the runner decodes both sources into +one 546-row roster before the gate split. + +## The chain, and the three drop points + +For an enrolled identity the required run promises (route-gap .dag header): execute → gap → held; or execute +→ pass → stale-row red; or enrolled → did not execute → red. What actually happens for 541 of 546: + +1. **Discovery/import** — preparation ranges over the gate closure. The gate (`required_gate_prefixes`, 11 + prefixes + seed modules, cut 2026-08-29, rung drop "Required gate reduced to the compiler floor") admits + only 5 of the 146 modules carrying enrollments. 536 rows sit in modules never loaded: no plan, no + execution, no receipt. *Declared* — the bankruptcy names the population per run in + `required_floor_disposition.tsv` (`declined_outside_gate_closure=26844`, `declined_outside_required_gate=696` + on this run; summary line `declared=28274 offered=1430 routed=704`). +2. **Selection/admission** — the only mechanism asserting "enrolled ⇒ executed" is the route-gap join + (`required_floor_runner.rs`). `suppress_withheld` removes the 541 from the roster *before* the join, so the + join's universe is the 5 gate-inside rows. The suppressed list is produced **per identity with grounds** — + and then discarded: route-gap publishes only the two aggregate count lines above. Expected-red got the + per-identity treatment on 2026-09-01 (`v1_compiler_expected_red_roster_join.rs`: "THE DENOMINATOR IS THE + ENROLLED ROSTER, NOT THE SURVIVORS", suppressed rows recorded with their ground); route-gap never did. +3. **Decision** — the run greens with "5 held; 0 unenrolled gaps". 541 enrollments are in no ledger the run + publishes: the claim-cost TSV carries only executed identities (704 rows, 5 `host_effect_refused` — the + carried ones: `test.claim.parse_test.parse_witness_floor_holds`, `...parse_witness_perf_holds`, + `test.claim.namespace_import_closure_witness.namespace_import_closure_receipt_holds`, + `test.claim.namespace_structural_root_exposure_generated_witness_test.namespace_structural_root_exposure_generated_witness_holds`, + `test.claim.v1_dag_parse_witness.v1_dag_parse_witnesses`); the measurement receipt carries only + `standing` + `blockers`; the disposition/join TSVs are written by the floor job but **not uploaded**. + +## The (a)/(b)/(c) split (sampled, identity grain) + +- **(a) Deliberately outside the supported guarantee** — the wet/service families: machine intake + (`test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.*`, 44 rows), fabric (31), spark + serving (74), runner (13), codex supervised turn (21), workspace storage — claims whose execution needs + service fabric the hermetic required run does not attach by design. Their route-gap rows were enrolled from + the pre-bankruptcy era; the bankruptcy (declared 2026-08-29) is the standing disposition for the family, + and `DeclinedNoCiWetLane`/`DeclinedOutsideRequiredGate` type the planning-level fact per identity. For + these, a per-identity suppressed record on a required run is **measurement, not closure** — closure for + them is the gate/wet-lane decision already declared in the rung drop. +- **(b) Meant to support, unobserved** — the hermetic-adjacent families whose route gap is exactly the + missing mock arm the register exists to demand: filesystem/store mock arms (`artifact_store_fs_witness`, + `durable_exclusive_hold_file_store`, `materialization_store_local`, `effect_plan_bash`: operations Dir 127, + DirWithTemplate 130, DigestStdin 42, Run 46, Check 26) and the withdrawn `v2.test.execution.emit_on_demand_*` + family (probed 2026-10-01, amendment names the restoration trigger: "the restoration trigger above stands + whole"). The register's demand semantics — "a row leaves when a route is supplied" — require observation; + with no observing run, no arm gets built and the trigger cannot fire. The suppression comment's promise + ("observable again ... in the whole-corpus receipts run") is **a promise with no executor**: no workflow in + `.github/workflows/` (8 files, none scheduled for a corpus pass) runs it, and the rung-drop authority + itself rules the escape hatch out ("a receipt-only run outside the required path does NOT retire the row"). + So for (b) the absence of that run is not merely a gap — it is the defect: the demand register's only + claimed observation point does not exist. +- **(c) Defect (structural, live today at zero count)** — the class "enrollment the tree no longer declares". + The mechanism cannot see it: suppression counts it with the (a)/(b) rows, no arm refuses it, and the + roster header itself warns "an enrollment nothing observes is a row that can never ask to be removed". + Zero live rows today (audited); the class is one rename away, and nothing would notice. Also (c): the + route-gap contract's four-arm sentence still claims whole-roster observability and was never amended when + gate-bounded suppression landed (2026-08-29) — two authorities now disagree silently. + +## Proposed repair (one partition in the existing admission path) + +In `suppress_withheld` + the route-gap join in `required_floor_runner.rs`, partition the roster at identity +grain — the cost-debt partition precedent (gunbc#9684) and the expected-red join-report precedent +(2026-09-01), no new system, no new CI job: + +1. **Declared + gate-inside** → observed today, join as now (held / stale-red). +2. **Declared + outside-gate (or cost-debt withheld)** → typed, located, per-identity suppressed row carried + into the outcome (like the expected-red join report) and named per identity on the existing stderr + channel (pattern: the cost-debt "kept as record" line), each with its ground + (`OutsideRequiredGate` / `CostDebtWithheld`). Label: for (a) this is measurement; for (b) it is the + explicit disposition that replaces the green absence. +3. **Undeclared** (module absent from the discovery roots / identity tail absent) → **typed refusal**, red, + naming identity and roster. Fires on zero rows today; keeps it that way. +4. **Text amendments**: the route-gap header's four-arm sentence and the suppression comment's + "whole-corpus receipts run" promise are amended to state the real standing (dormant until the gate + widens; no receipts run exists and none retires rows). + +Acceptance path: author a fresh claim in an out-of-gate module, enroll it in `floor_route_gap`, and the +required run records it per identity with ground `OutsideRequiredGate` — or, if misnamed, refuses. Heavy +runs remote/CI only. + +## Repair as approved and built (coordinator ack, conditions + single-implementation round) + +The partition decision is now **modeled on the .dag authority** — +`v2.workflow.floor_route_gap.floor_route_gap_admission_partition` is the single implementation of the +route-gap admission decision, membership judgment included; the Rust call site marshals the run's real +values (suppressed identities with their declared ground arms, and the discovery walk's declared-identity +index WHOLE as a keyed map) into it through `run_in_context_with_args`, and the relation performs the +membership judgment itself with `map_contains_key` per row — the runner does no membership test, so +refuse-if-undeclared is decided on the authority. An earlier Rust classifier +(`route_gap_suppressed_undeclared`) was **deleted** rather than kept beside the call — one implementation, +a net reduction of seed decision surface; the seed receipt counts **+4 hand items**, all in the runner: the +shared entry name, the suppressed-row marshal, the declared-index marshal, and the shared production +decode+enforce (`route_gap_admission_decode_and_enforce`) — extracted from `run_required_floor` so the +pairing test drives the same function the run site executes, and the misnamed fixture produces the actual +`REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared`, not just the relation's refusal arm. The declared index arrives as a keyed map so the judgment +stays in .dag at one O(1) lookup per suppressed row: an earlier shape flattened the declared index for +the .dag to linearly re-scan per suppressed row (541 x 28,274 ≈ 15M interpreted string comparisons per +required run) — a cost-shape defect, fixed per DESIGN §6 rather than retired on "n is small here"; a +per-row Boolean read in Rust was the intermediate shape, retired because a Rust-side `contains_key` IS +the refuse-if-undeclared judgment. What would move even the marshal into the .dag is the self-emitted +claim executor owning the discovery walk and feeding the relation directly; deliberately not built. The +judgment could not have been expressed in .dag on its own earlier because the declared universe is +discovery-walk knowledge (the roster decodes in a hermetic frame whose subject is the gate closure); +modeling the RELATION and marshaling the index whole as a keyed map is the resolution of that. + +1. **The wall (closure)**: a refused row names an enrollment the tree does not declare (module or tail + absent from the discovery roots; the disposition index covers every declared witness identity, + gunbc#9684) and the run refuses with `cause=RouteGapEnrollmentUndeclared`, naming the identities and + the modeled entry that decided. +2. **Single authority**: the route-gap .dag header contract states the gate-bounded amendment (the two + further arms) beside the original four; the `suppress_withheld` stderr line no longer promises a + whole-corpus receipts run — it states the true standing; and the membership test has exactly one + implementation, on the authority. +3. **Measurement (labeled)**: every suppressed identity is named with the ground the modeled partition + returned for it, headed MEASUREMENT — for the (a) families this records declared dormancy and closes + nothing. The ground itself is a **declared coproduct** (round 3, per review 76626): `ground` carries + `v2.workflow.floor_route_gap`'s `FloorRouteGapSuppressionGround` (`OutsideRequiredGate | + WithheldCostDebt | DeclinedNoCiWetLane`, spelled arm-for-arm after the floor's suppression enum as + the seed realizes it — `v1.expected_red_roster_join`'s suppression ground, generated into the runner + as a Rust enum) instead of a free label; the marshal decodes the enum into the declared arm and the + run site refuses an arm the enum does not declare, so a fabricated ground can never pass as a label. + The arms cannot be shared by import because the eval universe's discovery roots are `dag` + `src/v2` + (no `src/v1`), so name-alignment is what keeps the two spellings one vocabulary. +4. **Not closed here — class (b)**: unchanged from the section above; the named follow-ups are gate + admission of those modules, or a dispatch instrument row running a probe roster with the join armed. + +**Evidence, pinned on both sides of the boundary:** +- **Floor-side route witness** — `test.claim.route_gap_partition_witness`, gate-admitted at exact module + grain in `required_gate_authored_modules` (the same mechanism and operator ruling as + `test.claim.discovery_census_witness` and `test.claim.seed_growth_admission_witness`): drives the + modeled relation over the shared fixture `src/v2/test/fixture/route_gap_admission_partition.dag` and + asserts both arms on the floor — the route, executed by a required run. Substrate inputs only + (constructed lists; no host effect, no service). +- **Seed-side pairing witness** — `route_gap_admission_partition_tests` in `required_floor_runner.rs` + drives the SAME entry by the SAME constant through `run_in_context_with_args` (the real call path the + run site uses) and asserts both arms at identity grain; a second test pins the marshal shape (identity + and declared ground arm, nothing else). Runs via the required `rust-unit-tests` lane (see the wall's + standing below — `DESIGN.md` "Building & checks"; the lane returned required on 2026-09-30). +- **One implementation**: with the Rust classifier deleted, the run site's route to the answer is the + modeled entry by construction; a run-path refusal names the entry that decided it. + +**The wall's real standing (corrected per review 76431 — an earlier revision of this paragraph claimed a +shipped fixture; the fixture is gone, per review 38602, and this is what actually holds):** + +- **Green by execution on the required path:** the partition IS the run's own admission step — on every + required run it executes over the real roster, names every suppressed enrollment per identity with its + ground (the `[floor-route-gap]` suppressed lines), and the reverse join decides over the observable + remainder. The consumer is the fold itself; nothing about the green arm is test-only. A freshly authored + claim shaped like the dropped population (declared, out-of-gate, enrolled) gets the same typed, located + disposition on that run as the 536 do. +- **Discriminating red: authored at unit grain AND enrolled on a required lane.** The misnamed-enrollment + control runs both ways this PR ships: + - **On the floor (REQUIRED, blocks merge):** the claim-home row in `v2.workflow.required_floor` + `required_gate_authored_modules` gate-admits `test.claim.route_gap_partition_witness`, whose third test + (`dag/test/claim/route_gap_partition_witness_test.dag`) drives the modeled partition over the shared + fixture and asserts the refused arm at identity grain — the wall's red executes on the `witnesses` + lane, which is a required merge gate, with substrate inputs only (constructed rows and the fixture's + keyed declared map; nothing shipped on the production roster, per review 38602's rejection). + - **At unit grain (REQUIRED):** the pairing witness in `route_gap_admission_partition_tests` drives + `run_in_context_with_args` — the real call path the run site takes — over the same fixture rows and + asserts both arms; it runs via `cargo test --release -p v1-compiler --lib`, which per `DESIGN.md` + "Building & checks" runs as the `rust_unit_tests` step of the required `rust-unit-tests` job, so a + unit-test red blocks a merge. (The doc previously cited a stale generated projection, + `docs/onboarding.md` line 175, saying the lane ran on no required step; the authority is `DESIGN.md`, + and `DESIGN.md` records the lane's 2026-09-30 return and the retirement of the + `rust_unit_tests_off_the_merge_path` drop.) + The standing caveat that remains is narrower: a *live roster* misname — a misnamed enrollment shipped + onto main's production roster — is not how the red is authored (rejected by review 38602: it would red + main forever and fabricate a gap the §5 oracle forbids); the red is authored from fixtures the claim + supplies. The (b) follow-up above — a dispatch instrument row that runs a probe roster with the join + armed — remains the path to authoring that red over the real production roster rather than a fixture. diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index 7fb2c6cbf8f..202484ca103 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -269,6 +269,207 @@ pub(crate) fn floor_route_gap_expectation_mismatch( } } +/// THE ROUTE the run site takes to the admission decision. The relation it names is modeled on +/// `v2.workflow.floor_route_gap` — the authority that owns the register — and there is no Rust +/// copy of the membership test: this constant is the single route, and the pairing witness +/// drives the same name through `run_in_context_with_args` so a rename here breaks the witness +/// instead of silently forking the decision. +pub(crate) const ROUTE_GAP_ADMISSION_PARTITION_ENTRY: &str = + "v2.workflow.floor_route_gap.floor_route_gap_admission_partition"; + +/// THE MARSHAL the run site and the pairing witness share: a suppressed row reaches the modeled +/// relation as a `FloorRouteGapSuppressedRow` record carrying its identity and its ground — the +/// runner's suppression enum decoded into the relation's declared coproduct +/// (`v2.workflow.floor_route_gap`'s `FloorRouteGapSuppressionGround`), arm-for-arm — and +/// nothing else. One marshal, so the shape cannot fork between the real roster and the fixture. +pub(crate) fn route_gap_suppressed_rows_value( + ctx: &v1_interpreter::InterpContext, + rows: &[(String, SuppressionGround)], +) -> v1_interpreter::Value { + // The declared arms are spelled arm-for-arm after the runner's suppression enum, so this + // decode is the spelling's only authority: a rename on either side breaks this match or the + // fixture, never forks silently. Inlined — the marshal is one counted seed item with no + // nested hand declaration of its own. + v1_interpreter::list_value( + rows.iter() + .map(|(identity, ground)| v1_interpreter::Value::Record { + type_name: ctx.sym("FloorRouteGapSuppressedRow"), + fields: Rc::new(vec![ + (ctx.sym("identity"), v1_interpreter::str_value(identity)), + ( + ctx.sym("ground"), + v1_interpreter::Value::Variant { + type_name: ctx.sym("FloorRouteGapSuppressionGround"), + variant_name: ctx.sym(match *ground { + SuppressionGround::OutsideRequiredGate => "OutsideRequiredGate", + SuppressionGround::WithheldCostDebt => "WithheldCostDebt", + SuppressionGround::DeclinedNoCiWetLane => "DeclinedNoCiWetLane", + }), + fields: Rc::new(vec![]), + }, + ), + ]), + }) + .collect::>(), + ) +} + +/// THE SECOND MARSHAL the run site and the pairing witness share: the discovery walk's +/// declared-identity index, marshaled WHOLE as a keyed map (identity -> disposition label) — +/// the shape the modeled relation judges membership with. The runner does no membership test: +/// `contains_key` here would BE the refuse-if-undeclared decision made outside +/// `v2.workflow.floor_route_gap`'s `floor_route_gap_admission_partition`, so the judgment +/// travels to the .dag authority and this marshal only moves the data. Keyed, because the +/// alternative — the same universe flattened into a list the relation re-scans per row — is +/// the corpus-sized join the .dag contract retires. +pub(crate) fn route_gap_declared_map_value( + declared: &HashMap, +) -> v1_interpreter::Value { + let mut entries = im::HashMap::new(); + for (identity, disposition) in declared { + let key = v1_interpreter::CanonKey::new(v1_interpreter::str_value(identity)) + .expect("identity is a valid string map key"); + entries = entries.update( + key, + v1_interpreter::str_value(required_floor_disposition_label(disposition)), + ); + } + v1_interpreter::map_value(entries) +} + +/// THE PRODUCTION DECODE + ENFORCE for the modeled admission partition's answer, shared by the +/// run site and the pairing test: every row is decoded by its declared arm (a refused row with +/// no identity, an unknown ground arm, or an unknown arm refuses the whole decode — never +/// widens), a refused row raises REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared, and +/// every measured row is recorded per identity with its ground on the roster's channel as +/// MEASUREMENT (closes nothing). The fixture test drives this function over the misnamed +/// fixture and requires the actual error, so the production branch — not only the relation — +/// is exercised by a discriminating control. +pub(crate) fn route_gap_admission_decode_and_enforce( + ctx: &v1_interpreter::InterpContext, + decided_rows: Vec<&v1_interpreter::Value>, + roster_len: usize, +) -> Result, String> { + let mut route_gap_refused: Vec = Vec::new(); + let mut route_gap_measured: Vec<(String, String)> = Vec::new(); + for row in decided_rows { + let v1_interpreter::Value::Variant { + variant_name, + fields, + .. + } = row + else { + return Err(format!( + "route_gap_admission_partition: malformed admission row, observed {}", + floor_value_shape(Some(row)) + )); + }; + let field_str = |name: &str| -> Option { + let value = ctx.field(fields, name)?; + match value { + v1_interpreter::Value::Str(s) => Some(s.to_string()), + _ => None, + } + }; + let ground_arm = |name: &str| -> Option { + let value = ctx.field(fields, name)?; + match value { + v1_interpreter::Value::Variant { variant_name, .. } => { + Some(ctx.resolve(*variant_name).as_str().to_string()) + } + _ => None, + } + }; + match ctx.resolve(*variant_name).as_str() { + "FloorRouteGapAdmissionRefusedRow" => match field_str("identity") { + Some(identity) => route_gap_refused.push(identity), + None => { + return Err( + "route_gap_admission_partition: a refused row carries no identity" + .to_string(), + ) + } + }, + "FloorRouteGapAdmissionMeasuredRow" => { + match (field_str("identity"), ground_arm("ground")) { + (Some(identity), Some(arm)) => { + // The relation returns the declared arm; decode it back to the runner's + // suppression enum by the same arm-for-arm spelling the marshal used, and + // refuse an arm the enum does not declare — a fabricated ground can never + // pass as a label. + let ground = match arm.as_str() { + "OutsideRequiredGate" => SuppressionGround::OutsideRequiredGate, + "WithheldCostDebt" => SuppressionGround::WithheldCostDebt, + "DeclinedNoCiWetLane" => SuppressionGround::DeclinedNoCiWetLane, + other => { + return Err(format!( + "route_gap_admission_partition: a measured row carries unknown suppression ground arm {other}" + )) + } + }; + route_gap_measured.push(( + identity, + crate::v1_compiler_expected_red_roster_join::suppression_ground_label( + ground, + ), + )); + } + _ => { + return Err( + "route_gap_admission_partition: a measured row carries no identity or ground" + .to_string(), + ) + } + } + } + other => { + return Err(format!( + "route_gap_admission_partition: unknown admission arm {other}" + )) + } + } + } + if !route_gap_refused.is_empty() { + return Err(format!( + "REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared — the route-gap roster \ + enrolls identity(ies) the tree does not declare, refused by the modeled admission \ + partition ({ROUTE_GAP_ADMISSION_PARTITION_ENTRY}). Suppression removes them before \ + the reverse join, so no other guard can ever see them and a row that cannot be \ + observed can never ask to be removed. Delete the enrollment or restore the \ + identity: [{}]", + route_gap_refused.join(", ") + )); + } + // MEASUREMENT, NOT CLOSURE: every suppressed enrollment is named at identity grain with the + // ground the modeled partition returned for it, on the roster's own channel. For identities + // whose module the 2026-08-29 gate cut withdrew, this line records a declared dormancy — + // the gate decision owns it, and this record closes nothing for them. + let mut measured_by_ground: Vec<(String, Vec)> = Vec::new(); + for (identity, ground) in &route_gap_measured { + match measured_by_ground.iter_mut().find(|(g, _)| g == ground) { + Some((_, named)) => named.push(identity.clone()), + None => measured_by_ground.push((ground.clone(), vec![identity.clone()])), + } + } + measured_by_ground.sort(); + for (ground, named) in &measured_by_ground { + eprintln!( + "[floor-route-gap] {} enrolled identity(ies) suppressed, kept as record and NOT \ + held as agreement (dormant, not deleted; MEASUREMENT — the {ground} arm is owned by \ + the gate cut of 2026-08-29 and the cost-debt roster, not by this check): {}", + named.len(), + named.join(", ") + ); + } + eprintln!( + "[floor-route-gap] roster carries {} enrolled identity(ies) after admission; {} \ + suppressed with ground and named above", + roster_len, + route_gap_measured.len() + ); + Ok(route_gap_measured) +} + /// `v2.workflow.required_floor`'s claims execute Hermetic (pure in-process evaluation), so /// CPU is the judged basis. A lane that later admits an execution mode whose purpose is /// external or blocking interaction picks wall instead — but the choice is made here, by @@ -9573,7 +9774,10 @@ pub fn run_required_floor( "[floor-required-gate] {name}: {outside_gate} enrolled identity(ies) suppressed \ because their module is outside the required gate and was never loaded; their \ enrollment is dormant, not deleted, and becomes observable again when the gate \ - roster admits the module or in the whole-corpus receipts run" + roster admits the module. There is no other observation point: no whole-corpus \ + receipts run exists or is scheduled, and the rung-drop authority rules a \ + receipt-only run outside the required path out as a retirement path — so the \ + consuming rosters record these identities per identity, never as a bare count" ); } removed @@ -10397,12 +10601,54 @@ pub fn run_required_floor( out }; let mut route_gap_roster = route_gap_roster; - let _ = suppress_withheld(&mut route_gap_roster, "floor_route_gap"); - let _ = suppress_declined_no_ci_wet_lane(&mut route_gap_roster, "floor_route_gap"); - eprintln!( - "[floor-route-gap] roster carries {} enrolled identity(ies)", - route_gap_roster.len() - ); + // THE ADMISSION PARTITION IS THE MODELED RELATION, and the relation is the single + // implementation. `suppress_withheld` returns exactly which identities it removed and why; + // this was the one call site that dropped the list (`let _ =`), so the reverse join below + // decided only over the identities a gate-bounded run can observe while every other + // enrollment sat in no ledger the run publishes. The runner now marshals the run's real + // values -- the suppressed identities with the ground that removed each, decoded into the + // relation's declared coproduct, and the discovery walk's declared-identity index -- into + // `v2.workflow.floor_route_gap` + // `.floor_route_gap_admission_partition` through the hermetic frame the manifest was folded + // in. There is no Rust copy of the membership test to rot apart from the roster it joins; + // the arms and their meaning live on the authority's contract, and the pairing witness + // (`test.claim.route_gap_partition_witness`, floor-side) drives the same surface over the + // shared fixture. + let mut route_gap_suppressed = suppress_withheld(&mut route_gap_roster, "floor_route_gap"); + route_gap_suppressed.extend(suppress_declined_no_ci_wet_lane( + &mut route_gap_roster, + "floor_route_gap", + )); + route_gap_suppressed.sort(); + // + // THE WALL: a refused row names an enrollment the tree does not declare. The disposition + // index covers EVERY declared witness identity over the discovery roots (gunbc#9684), so + // absence there is absence from the tree — and suppression removed the row BEFORE the + // reverse join, so the stale arm can never fire for it. The cheapest way to fake a green + // run, enrolling an identity that does not exist, costs a refusal, never a count. + let suppressed_rows_value = route_gap_suppressed_rows_value(&hermetic, &route_gap_suppressed); + // THE DECLARED INDEX, MARshaled WHOLE AS A KEYED MAP: the relation does the membership + // judgment (map_contains_key per row) — this site only moves the data, no contains_key + // here, or the refuse-if-undeclared decision would live in Rust beside the .dag authority. + let declared_value = route_gap_declared_map_value(&cost_debt_disposition_index); + let route_gap_decided = v1_interpreter::run_in_context_with_args( + &hermetic, + ROUTE_GAP_ADMISSION_PARTITION_ENTRY, + &[ + (Some("suppressed".to_string()), suppressed_rows_value), + (Some("declared".to_string()), declared_value), + ], + false, + ) + .map_err(|e| format!("route_gap_admission_partition: {e}"))?; + let decided_rows = floor_decode_list(&hermetic, Some(&route_gap_decided)) + .map_err(|e| format!("route_gap_admission_partition: {e}"))?; + // THE DECODE + ENFORCE, SHARED WITH THE FIXTURE TEST: the same function the pairing test + // drives over the misnamed fixture executes here on the run's real values — so the + // production branch (refused rows -> RouteGapEnrollmentUndeclared) is exercised, not just + // the relation. Deleting this call must fail that test, not pass it. + let route_gap_measured = + route_gap_admission_decode_and_enforce(&hermetic, decided_rows, route_gap_roster.len())?; // New enrollments carry the operation and the closed remedy-ground observed at the // interpreter boundary. Their identities are projected into `floor_route_gap_roster` by @@ -17456,6 +17702,391 @@ mod expected_red_roster_join_suppression_tests { } } +#[cfg(test)] +mod route_gap_admission_partition_tests { + use super::*; + + /// THE FIXTURE'S SUPPRESSED ROWS, decoded to (identity, declared-arm) pairs — the shape the + /// shared marshal re-encodes into the relation's coproduct. + fn suppressed_row_pairs( + ctx: &v1_interpreter::InterpContext, + value: &Value, + ) -> Vec<(String, String)> { + let Value::List(items) = value else { + panic!("the fixture suppressed value is not a List"); + }; + items + .iter() + .map(|item| { + let Value::Record { fields, .. } = item else { + panic!("a fixture suppressed row is not a Record"); + }; + let Some(Value::Str(identity)) = ctx.field(fields, "identity") else { + panic!("a fixture suppressed row has no String identity"); + }; + let Some(Value::Variant { variant_name, .. }) = ctx.field(fields, "ground") else { + panic!("a fixture suppressed row has no declared ground arm"); + }; + (identity.to_string(), ctx.resolve(*variant_name).to_string()) + }) + .collect() + } + + /// THE MARSHAL'S INPUT, decoded back to the runner's suppression enum by the arm-for-arm + /// spelling the marshal owns. A fixture arm the enum does not declare panics here instead of + /// passing as a label. + fn ground_arm_enum(arm: &str) -> SuppressionGround { + match arm { + "OutsideRequiredGate" => SuppressionGround::OutsideRequiredGate, + "WithheldCostDebt" => SuppressionGround::WithheldCostDebt, + "DeclinedNoCiWetLane" => SuppressionGround::DeclinedNoCiWetLane, + other => panic!( + "the fixture names a suppression arm the runner's enum does not declare: {other}" + ), + } + } + + /// THE MODELED PARTITION'S RESULT, decoded to (identity, declared-arm, refused) triples — + /// one arm per suppressed row, at identity grain. + fn admission_rows( + ctx: &v1_interpreter::InterpContext, + value: &Value, + ) -> Vec<(String, String, bool)> { + let Value::List(rows) = value else { + panic!("the modeled partition did not return a List"); + }; + rows.iter() + .map(|row| { + let Value::Variant { + variant_name, + fields, + .. + } = row + else { + panic!( + "an admission row is not a Variant, observed {}", + floor_value_shape(Some(row)) + ); + }; + let str_field = |name: &str| -> String { + let Some(Value::Str(s)) = ctx.field(fields, name) else { + panic!("an admission row has no String {name}"); + }; + s.to_string() + }; + let arm_field = |name: &str| -> String { + let Some(Value::Variant { variant_name, .. }) = ctx.field(fields, name) else { + panic!("an admission row has no declared {name} arm"); + }; + ctx.resolve(*variant_name).to_string() + }; + match ctx.resolve(*variant_name).as_str() { + "FloorRouteGapAdmissionMeasuredRow" => { + (str_field("identity"), arm_field("ground"), false) + } + "FloorRouteGapAdmissionRefusedRow" => { + (str_field("identity"), String::new(), true) + } + other => panic!("unknown admission arm {other}"), + } + }) + .collect() + } + + /// THE PAIRING WITNESS, THROUGH THE REAL CALL PATH. The run site marshals the run's real + /// values into `v2.workflow.floor_route_gap.floor_route_gap_admission_partition` via + /// `run_in_context_with_args`; this witness drives the SAME entry, by the SAME constant, + /// over the SHARED fixture (src/v2/test/fixture/route_gap_admission_partition.dag), so a + /// rename of the entry or a fork of the marshal shape breaks here instead of forking the + /// decision. It asserts both arms at identity grain: a declared suppressed row comes back + /// MEASURED with its ground kept, and an enrollment the tree does not declare -- renamed, + /// deleted, or fabricated -- comes back REFUSED, the wall's discriminating arm. The + /// floor-side route witness (`test.claim.route_gap_partition_witness`) asserts the same + /// fixture rows on the floor, so the answer and the route are pinned on both sides. + #[test] + fn the_partition_route_decides_the_shared_fixture_at_identity_grain() { + crate::cli_run::on_live_pool_thread(|| { + let root = process_workspace_root(); + let roots: Vec = ["dag", "src/v2"] + .iter() + .map(|r| root.join(r).to_string_lossy().to_string()) + .collect(); + let entry = root + .join("src/v2/test/fixture/route_gap_admission_partition.dag") + .to_string_lossy() + .to_string(); + let index = crate::cli_run::process_shared_index(&roots); + let (graph, indices) = crate::cli_run::resolve_entry_with_index(&index, &entry) + .expect("the shared fixture resolves"); + let ctx = crate::cli_run::make_eval_context( + &graph, + indices, + v1_interpreter::ExecutionMode::Hermetic, + ); + let read = |name: &str| { + v1_interpreter::with_active_context(&ctx, || { + v1_interpreter::run_in_context( + &ctx, + &format!("v2.test.fixture.route_gap_admission_partition.{name}"), + false, + ) + }) + .unwrap_or_else(|e| panic!("{name} does not evaluate: {e}")) + }; + let suppressed = + suppressed_row_pairs(&ctx, &read("route_gap_partition_fixture_suppressed")); + // THE DECLARED SET AS THE FIXTURE SUPPLIES IT: the modeled keyed map the relation + // judges membership with — the same shape the run site marshals its disposition + // index into. No list is flattened here, and the misnamed fixture identity is + // deliberately absent from it. + let declared = read("partition_fixture_declared"); + assert_eq!( + suppressed.len(), + 4, + "the fixture carries both arms and all three grounds" + ); + let marshal_input = suppressed + .iter() + .map(|(identity, arm)| (identity.clone(), ground_arm_enum(arm))) + .collect::>(); + let args = [ + ( + Some("suppressed".to_string()), + route_gap_suppressed_rows_value(&ctx, marshal_input.as_slice()), + ), + (Some("declared".to_string()), declared), + ]; + let decided = v1_interpreter::with_active_context(&ctx, || { + v1_interpreter::run_in_context_with_args( + &ctx, + ROUTE_GAP_ADMISSION_PARTITION_ENTRY, + &args, + false, + ) + }) + .expect("the modeled admission partition evaluates over the fixture"); + let rows = admission_rows(&ctx, &decided); + assert_eq!( + rows.len(), + 4, + "every suppressed row lands in exactly one arm" + ); + assert_eq!( + rows.iter() + .filter(|(i, g, refused)| !refused + && i == "test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.a_holds" + && g == "OutsideRequiredGate") + .count(), + 1, + "the declared suppressed row is MEASURED with its ground kept" + ); + assert_eq!( + rows.iter() + .filter(|(i, g, refused)| !refused + && i == "test.claim.parse_test.parse_witness_floor_holds" + && g == "WithheldCostDebt") + .count(), + 1, + "the cost-debt withheld declared row is MEASURED with its ground kept" + ); + assert_eq!( + rows.iter() + .filter(|(i, _, refused)| *refused + && i == "test.claim.renamed_away_witness_test.old_witness_name") + .count(), + 1, + "the enrollment the tree does not declare is REFUSED -- the wall's discriminating arm" + ); + }); + } + + /// THE MARSHAL SHAPE the run site owes, pinned beside the fixture: a suppressed row carries + /// its identity and its ground as the declared coproduct arm, and nothing else. + #[test] + fn the_marshal_shape_names_identity_and_ground_only() { + crate::cli_run::on_live_pool_thread(|| { + let root = process_workspace_root(); + let roots: Vec = ["dag", "src/v2"] + .iter() + .map(|r| root.join(r).to_string_lossy().to_string()) + .collect(); + let entry = root + .join("src/v2/test/fixture/route_gap_admission_partition.dag") + .to_string_lossy() + .to_string(); + let index = crate::cli_run::process_shared_index(&roots); + let (graph, indices) = crate::cli_run::resolve_entry_with_index(&index, &entry) + .expect("the shared fixture resolves"); + let ctx = make_eval_context(&graph, indices, v1_interpreter::ExecutionMode::Hermetic); + let value = route_gap_suppressed_rows_value( + &ctx, + &[( + "test.claim.any_witness_test.any_holds".to_string(), + SuppressionGround::OutsideRequiredGate, + )], + ); + let v1_interpreter::Value::List(items) = &value else { + panic!("the marshal produces a List"); + }; + assert_eq!(items.len(), 1); + let v1_interpreter::Value::Record { type_name, fields } = &items[0] else { + panic!("the marshal produces a suppressed-row Record"); + }; + assert_eq!( + ctx.resolve(*type_name).as_str(), + "FloorRouteGapSuppressedRow" + ); + assert_eq!(fields.len(), 2, "identity and ground, nothing else"); + }); + } + + /// THE SECOND MARSHAL'S SHAPE AND ROUTE: the disposition index marshals as a keyed Map, and + /// judged THROUGH THE RELATION it measures a row the index declares and refuses one it does + /// not — the membership judgment exercised on the same call path the run site takes, not a + /// Rust-side contains_key. + #[test] + fn the_declared_index_marshal_judges_membership_through_the_relation() { + crate::cli_run::on_live_pool_thread(|| { + let root = process_workspace_root(); + let roots: Vec = ["dag", "src/v2"] + .iter() + .map(|r| root.join(r).to_string_lossy().to_string()) + .collect(); + let entry = root + .join("src/v2/test/fixture/route_gap_admission_partition.dag") + .to_string_lossy() + .to_string(); + let index = crate::cli_run::process_shared_index(&roots); + let (graph, indices) = crate::cli_run::resolve_entry_with_index(&index, &entry) + .expect("the shared fixture resolves"); + let ctx = make_eval_context(&graph, indices, v1_interpreter::ExecutionMode::Hermetic); + let mut declared: HashMap = HashMap::new(); + declared.insert( + "test.claim.any_witness_test.any_holds".to_string(), + RequiredFloorDisposition::Planned, + ); + let declared_value = route_gap_declared_map_value(&declared); + assert!( + matches!(declared_value, v1_interpreter::Value::Map(_)), + "the declared index marshals as a keyed Map, not a list" + ); + let args = [ + ( + Some("suppressed".to_string()), + route_gap_suppressed_rows_value( + &ctx, + &[ + ( + "test.claim.any_witness_test.any_holds".to_string(), + SuppressionGround::OutsideRequiredGate, + ), + ( + "test.claim.absent_witness_test.gone_holds".to_string(), + SuppressionGround::OutsideRequiredGate, + ), + ], + ), + ), + (Some("declared".to_string()), declared_value), + ]; + let decided = v1_interpreter::with_active_context(&ctx, || { + v1_interpreter::run_in_context_with_args( + &ctx, + ROUTE_GAP_ADMISSION_PARTITION_ENTRY, + &args, + false, + ) + }) + .expect("the modeled partition evaluates over the marshaled index"); + let rows = admission_rows(&ctx, &decided); + assert_eq!(rows.len(), 2, "both suppressed rows land somewhere"); + let declared_row = rows + .iter() + .find(|(i, g, refused)| !refused && i == "test.claim.any_witness_test.any_holds") + .expect("the declared identity is measured"); + assert_eq!( + declared_row.1, "OutsideRequiredGate", + "a measured row keeps its ground" + ); + assert!( + rows.iter() + .any(|(i, _g, refused)| *refused + && i == "test.claim.absent_witness_test.gone_holds"), + "an identity the index does not hold is refused, not counted" + ); + }); + } + + /// THE PRODUCTION BRANCH, DISCRIMINATED: the same decode+enforce function the run site + /// calls — driven over the partition's answer to the misnamed fixture — must return the + /// actual REQUIRED-FLOOR REFUSAL cause=RouteGapEnrollmentUndeclared, so deleting the + /// enforcement in `run_required_floor` cannot leave this control green (the shared function + /// is the enforcement; the call site and this test both own it). + #[test] + fn the_misnamed_fixture_refuses_through_the_production_decode_and_enforce() { + crate::cli_run::on_live_pool_thread(|| { + let root = process_workspace_root(); + let entry = root + .join("src/v2/test/fixture/route_gap_admission_partition.dag") + .to_string_lossy() + .to_string(); + let index = + crate::cli_run::process_shared_index(&["dag".to_string(), "src/v2".to_string()]); + let (graph, indices) = crate::cli_run::resolve_entry_with_index(&index, &entry) + .expect("the shared fixture resolves"); + let ctx = make_eval_context(&graph, indices, v1_interpreter::ExecutionMode::Hermetic); + let read = |name: &str| { + v1_interpreter::with_active_context(&ctx, || { + v1_interpreter::run_in_context( + &ctx, + &format!("v2.test.fixture.route_gap_admission_partition.{name}"), + false, + ) + }) + .unwrap_or_else(|e| panic!("{name} does not evaluate: {e}")) + }; + let suppressed = + suppressed_row_pairs(&ctx, &read("route_gap_partition_fixture_suppressed")); + let marshal_input = suppressed + .iter() + .map(|(identity, arm)| (identity.clone(), ground_arm_enum(arm))) + .collect::>(); + let args = [ + ( + Some("suppressed".to_string()), + route_gap_suppressed_rows_value(&ctx, marshal_input.as_slice()), + ), + ( + Some("declared".to_string()), + read("partition_fixture_declared"), + ), + ]; + let decided = v1_interpreter::with_active_context(&ctx, || { + v1_interpreter::run_in_context_with_args( + &ctx, + ROUTE_GAP_ADMISSION_PARTITION_ENTRY, + &args, + false, + ) + }) + .expect("the modeled partition evaluates over the fixture"); + let decided_rows = + floor_decode_list(&ctx, Some(&decided)).expect("the relation returns a row list"); + let err = route_gap_admission_decode_and_enforce(&ctx, decided_rows, 4).expect_err( + "the misnamed fixture must refuse through the production decode+enforce", + ); + assert!( + err.contains("cause=RouteGapEnrollmentUndeclared"), + "the production branch raises the typed refusal, observed: {err}" + ); + assert!( + err.contains("test.claim.renamed_away_witness_test.old_witness_name"), + "the refusal names the undeclared identity, observed: {err}" + ); + }); + } +} + #[cfg(test)] mod pure_producer_share_refused_carrier_overlap_tests { use super::*; diff --git a/src/v2/test/fixture/route_gap_admission_partition.dag b/src/v2/test/fixture/route_gap_admission_partition.dag new file mode 100644 index 00000000000..789ea472bfa --- /dev/null +++ b/src/v2/test/fixture/route_gap_admission_partition.dag @@ -0,0 +1,67 @@ +module v2.test.fixture.route_gap_admission_partition + +import std.types { List, String } +import v2.std.collection { Map, empty_map, map_insert } +import v2.workflow.floor_route_gap { + FloorRouteGapSuppressedRow, + FloorRouteGapAdmissionRow, + FloorRouteGapAdmissionMeasuredRow, + FloorRouteGapAdmissionRefusedRow, + floor_route_gap_admission_partition, +} + +// ONE FIXTURE, READ BY ALL THREE SIDES. `test.claim.route_gap_partition_witness` asserts the +// modeled partition over these rows on the floor (the route: the same surface the run site +// marshals into). The seed's `required_floor_runner` pairing witness evaluates the same rows +// through `run_in_context_with_args` -- the real call path the run site uses -- and asserts both +// arms at identity grain. The declared set arrives as a keyed Map (`partition_fixture_declared`, +// the shape the run site marshals its keyed disposition index into), so the relation performs +// the membership judgment itself with `map_contains_key` -- never a linear scan of a +// corpus-sized list. The rows span both arms and both grounds the runner produces: a declared +// suppressed row whose module the gate cut withdrew (measured, ground kept), a cost-debt- +// withheld row the tree declares (measured, ground kept), and an enrollment the tree does not +// declare -- renamed, deleted, or fabricated (refused; the wall). Grounds are the declared +// coproduct arms (`v2.workflow.floor_route_gap`'s `FloorRouteGapSuppressionGround`), bound by +// the field's declared type -- the same construction route the runner's marshal takes. +data route_gap_partition_fixture_suppressed: List = [ + FloorRouteGapSuppressedRow { identity: "test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.a_holds", ground: OutsideRequiredGate }, + FloorRouteGapSuppressedRow { identity: "test.claim.parse_test.parse_witness_floor_holds", ground: WithheldCostDebt }, + FloorRouteGapSuppressedRow { identity: "test.claim.wet_lane_probe.wet_lane_declared_holds", ground: DeclinedNoCiWetLane }, + FloorRouteGapSuppressedRow { identity: "test.claim.renamed_away_witness_test.old_witness_name", ground: OutsideRequiredGate } +] + +// THE DECLARED SET AS DATA: a keyed map, identity -> disposition label, holding the three +// identities the tree declares and deliberately NOT the misnamed one -- the wall's +// discriminating input lives in what this map omits. +fn partition_fixture_declared() -> Map { + map_insert( + m: map_insert( + m: map_insert( + m: empty_map(), + key: "test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.a_holds", + value: "declined_outside_gate_closure", + ), + key: "test.claim.parse_test.parse_witness_floor_holds", + value: "withheld_cost_debt", + ), + key: "test.claim.wet_lane_probe.wet_lane_declared_holds", + value: "declined_no_ci_wet_lane", + ) +} + +data route_gap_partition_fixture_expected: List = [ + FloorRouteGapAdmissionMeasuredRow { identity: "test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.a_holds", ground: OutsideRequiredGate }, + FloorRouteGapAdmissionMeasuredRow { identity: "test.claim.parse_test.parse_witness_floor_holds", ground: WithheldCostDebt }, + FloorRouteGapAdmissionMeasuredRow { identity: "test.claim.wet_lane_probe.wet_lane_declared_holds", ground: DeclinedNoCiWetLane }, + FloorRouteGapAdmissionRefusedRow { identity: "test.claim.renamed_away_witness_test.old_witness_name" } +] + +// THE DECIDED LIST IS THE RELATION'S ANSWER OVER THE FIXTURE, and both witnesses check it +// against `route_gap_partition_fixture_expected` at identity grain: measured rows one-for-one +// with the same identity and ground, refused rows one-for-one by identity. +fn partition_fixture_decided() -> List { + floor_route_gap_admission_partition( + suppressed: route_gap_partition_fixture_suppressed, + declared: partition_fixture_declared(), + ) +} diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index 3747d697113..d4b9829a389 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -2,6 +2,7 @@ module v2.workflow.floor_route_gap import std.types { List } import v2.std.algebra { Cons, Empty, list_flat_map } +import v2.std.collection { Map, map_contains_key } // THE EXPECTATION IS TYPED AT THE TWO FACTS THE INTERPRETER OBSERVES. An identity-only row // says merely that some route gap once existed; it cannot object when the witness reaches a @@ -63,6 +64,27 @@ type FloorRouteGapExpectation = { // - Enrolled, and the identity did not execute at all: reds the build. The reverse join is // what keeps a renamed or deleted identity from sitting here forever, unobserved. // +// THE GATE-BOUNDED AMENDMENT (2026-10, declared when the required floor's admission partition +// started recording it per identity; the gate cut itself is 2026-08-29). A gate-bounded fold +// loads only the gate closure, so two further arms exist and the four above decide only over +// the gate-inside remainder: +// +// - Enrolled, and the identity's module is outside the required gate (or the identity is +// withheld by the cost-debt roster, or declined as no-CI-wet-lane): the run cannot observe +// it, and the required floor names it per identity with that ground and holds it as NEITHER +// agreement NOR stale — dormancy is the gate cut's declared decision, and this roster does +// not own it. Observability returns exactly when the gate roster admits the module; there +// is no other observation point (no whole-corpus receipts run exists, and a receipt-only +// run outside the required path does not retire rows). +// - Enrolled, and the tree declares no such identity: REFUSES the required run. Suppression +// removes the row before the reverse join, so the stale arm above can never fire for it; +// an enrollment nothing can observe must refuse rather than count as dormant. +// +// WHAT ADMISSION DOES NOT OWN: an out-of-gate enrollment still demands the route it names. +// The register is the demand list for hermetic route arms, and unobserved demand is what a +// rung drop must name — a module the gate readmits brings its enrollments straight back under +// the four arms above. +// // THE ORACLE THIS ROSTER IS ALLOWED TO BE (DESIGN §5, the 2026-08-01 ruling on numeric // literals). It is a monotone debt contract, and it is legitimate only because all four of that // ruling's conditions hold: the subject universe is INDEPENDENTLY DISCOVERED (the floor's own @@ -2318,3 +2340,63 @@ fn floor_route_gap_expectation_chunk_38() -> List { tail: Empty {} } } + +// THE ADMISSION PARTITION, MODELED ON THE AUTHORITY THAT OWNS THE REGISTER. This is the single +// implementation of the route-gap admission decision, membership test included: the required +// floor's runner marshals the run's real values -- the identities suppression removed, each +// with the ground that removed it, and the discovery walk's declared-identity index AS A KEYED +// MAP -- into this relation through the hermetic frame it already holds. Nothing re-derives the +// membership judgment in Rust: a runner-side contains_key would BE the refuse-if-undeclared +// decision made outside this authority, the shape the changed-selection capability documented +// at v2.workflow.required_floor's dissolve-on note retires. Here the relation asks the map +// itself, per row, whether the tree declares the identity -- and what each arm MEANS is the +// authority's, not the marshal's. +// +// COST, NAMED, AND SHAPE-FIXED: the relation is one call per required run, LINEAR in the +// suppressed population, and it never scans a corpus-sized list. The declared index arrives as +// a keyed Map (the runner's disposition index marshaled whole), so the membership test is a +// keyed lookup per suppressed row -- O(1) amortized per identity in the eval's map substrate -- +// and flattening the universe into a list for a linear contains was the corpus-sized join this +// shape retires: on the required-run census the plan doc cites (declared in the tens of +// thousands, suppressed in the hundreds), a per-row linear scan is millions of interpreted +// comparisons per required run, a proven cost-shape defect that DESIGN.md's §6 says is always +// fixed, not retired on "n is small here". +// +// THE GROUND IS A DECLARED COPRODUCT, NOT A LABEL. Suppression grounds are a closed set -- the +// floor removes a row as outside the required gate, as withheld cost debt, or as declined for +// want of a CI wet lane -- so the field carries that set, and a fabricated ground is a +// construction of a type the runner cannot produce, not a free string. The arms are spelled +// arm-for-arm after the floor's suppression vocabulary as the seed realizes it +// (`v1.expected_red_roster_join`'s suppression ground, generated into the runner as a Rust enum +// whose marshal decodes it here by spelling): the eval universe's discovery roots are `dag` + +// `src/v2`, so the seed-side type cannot be imported here, and name-alignment is what keeps the +// two spellings one vocabulary -- a rename on either side breaks the pairing witness +// (src/v2/test/fixture/route_gap_admission_partition.dag) instead of forking silently. +type FloorRouteGapSuppressionGround = OutsideRequiredGate | WithheldCostDebt | DeclinedNoCiWetLane + +type FloorRouteGapSuppressedRow = { + identity: String, + ground: FloorRouteGapSuppressionGround, +} + +// THE TWO ARMS AT IDENTITY GRAIN. A declared suppressed row is MEASUREMENT: it keeps its ground +// and the run names it, and for identities whose module the 2026-08-29 gate cut withdrew that +// record closes nothing. An undeclared row REFUSES: suppression removed it before the reverse +// join, so no other guard can see it, and an enrollment nothing can observe must never pass as +// a count. +type FloorRouteGapAdmissionRow = + FloorRouteGapAdmissionMeasuredRow { identity: String, ground: FloorRouteGapSuppressionGround } + | FloorRouteGapAdmissionRefusedRow { identity: String } + +fn floor_route_gap_admission_partition( + suppressed: List, + declared: Map, +) -> List { + map( + suppressed, + row => match map_contains_key(m: declared, key: row.identity) { + true => FloorRouteGapAdmissionMeasuredRow { identity: row.identity, ground: row.ground } + false => FloorRouteGapAdmissionRefusedRow { identity: row.identity } + }, + ) +} diff --git a/src/v2/workflow/required_floor.dag b/src/v2/workflow/required_floor.dag index 0b4b54c7118..1285f493d97 100644 --- a/src/v2/workflow/required_floor.dag +++ b/src/v2/workflow/required_floor.dag @@ -907,6 +907,11 @@ fn required_gate_prefixes() -> List { // duplicate-key and well-formed checks and the addition/staleness join; it matched no family prefix, // so those reds executed on no merge lane. Admitted at exact module grain for the same reason as the // test-reference wall: a family prefix would silently widen to any future sibling. +// THE ROUTE-GAP PARTITION WITNESS (same reason, same grain). `test.claim.route_gap_partition_witness` +// carries the route-gap admission partition's discriminating red -- an enrollment the tree does not +// declare refuses -- through the modeled relation on `v2.workflow.floor_route_gap`, over substrate +// inputs only (constructed lists; no host effect, no service). It matched no family prefix, so the +// wall's red would execute on no merge lane without this row. // // THE CALIBRATION SPECIMEN (node adhoc-c9504740-637; sharp-raven-357 ruling with the operator's // go-ahead, 2026-10-05). The enrolment margin is judged in calibrated CPU ms, and the factor comes @@ -933,6 +938,7 @@ fn required_gate_authored_modules() -> List { "v2.test.claim.effect_demand.effect_demand_floor_join_test", "test.claim.test_reference_wall_witness", "test.claim.seed_growth_admission_witness", + "test.claim.route_gap_partition_witness", "test.claim.floor_eval_step_calibration_specimen_test", ] }