diff --git a/dag/gunbc/merge_admission_produce.dag b/dag/gunbc/merge_admission_produce.dag index b75169d2a89..2d15ef9e6a1 100644 --- a/dag/gunbc/merge_admission_produce.dag +++ b/dag/gunbc/merge_admission_produce.dag @@ -107,13 +107,13 @@ fn parse_receipt_wire_v2(text: String) -> MergeAdmissionReceiptV2? { let lines = receipt_wire_lines(text: text) if !((length(lines) == 6) || (length(lines) == 7)) { none - } else if !(lines.first() == merge_admission_receipt_schema_v2) { + } else if match lines.first() { Present { value: schema_line } => !(schema_line == merge_admission_receipt_schema_v2) Absent => true } { none - } else if lines.skip(n: 2).first() == "" { + } else if match lines.skip(n: 2).first() { Present { value: field } => field == "" Absent => true } { none - } else if lines.skip(n: 4).first() == "" { + } else if match lines.skip(n: 4).first() { Present { value: field } => field == "" Absent => true } { none - } else if lines.skip(n: 5).first() == "" { + } else if match lines.skip(n: 5).first() { Present { value: field } => field == "" Absent => true } { none } else { match walk_attempt_id(raw: lines.skip(n: 1).first()) { diff --git a/dag/gunbc/merge_admission_subject.dag b/dag/gunbc/merge_admission_subject.dag index a64561a99e2..60cb2c8acf6 100644 --- a/dag/gunbc/merge_admission_subject.dag +++ b/dag/gunbc/merge_admission_subject.dag @@ -133,9 +133,9 @@ fn render_git_object_id_wire(oid: GitObjectId) -> String { fn parse_git_object_id_wire(raw: String) -> GitObjectId? { if !(length(split(s: raw, delimiter: ":")) == 2) { none - } else if split(s: raw, delimiter: ":").first() == "sha1" { + } else if match split(s: raw, delimiter: ":").first() { Present { value: algorithm } => algorithm == "sha1" Absent => false } { git_sha1_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first()) - } else if split(s: raw, delimiter: ":").first() == "sha256" { + } else if match split(s: raw, delimiter: ":").first() { Present { value: algorithm } => algorithm == "sha256" Absent => false } { git_sha256_object_id(hex: split(s: raw, delimiter: ":").skip(n: 1).first()) } else { none @@ -160,13 +160,13 @@ fn parse_tested_subject_wire(text: String) -> TestedSubject? { let lines = receipt_wire_lines(text: text) if !(length(lines) == 5) { none - } else if !(lines.first() == merge_admission_tested_subject_schema) { + } else if match lines.first() { Present { value: schema_line } => !(schema_line == merge_admission_tested_subject_schema) Absent => true } { none - } else if lines.skip(n: 2).first() == "" { + } else if match lines.skip(n: 2).first() { Present { value: field } => field == "" Absent => true } { none - } else if lines.skip(n: 3).first() == "" { + } else if match lines.skip(n: 3).first() { Present { value: field } => field == "" Absent => true } { none - } else if lines.skip(n: 4).first() == "" { + } else if match lines.skip(n: 4).first() { Present { value: field } => field == "" Absent => true } { none } else { match walk_attempt_id(raw: lines.skip(n: 1).first()) { diff --git a/dag/gunbc/plans/value_null_split.dag b/dag/gunbc/plans/value_null_split.dag index 3fd266a1738..27f14af7f0c 100644 --- a/dag/gunbc/plans/value_null_split.dag +++ b/dag/gunbc/plans/value_null_split.dag @@ -3,12 +3,119 @@ module gunbc.plans.value_null_split import std.dissolution { unbound_dissolution } import gunbc.plan { Plan, PlanRetirement, PlanRetiresWhen, PlanIsAuthorityOnly } import std.markdown { MarkdownBlock, TableBlock, AlignNone } -import gunbc.plans.md_helpers { h2, p, li, ol, cell, row, task, tasks, Unchecked } +import std.types { Bool, Int, List, NonEmptyStr, String } +import gunbc.plans.md_helpers { h2, p, li, ol, ul, cell, row } + +// PHASE STANDING IS NOT A CHECKBOX, and this module used to prove why. Every phase below was +// `task(state: Unchecked)` while Phase A had DEMONSTRABLY LANDED -- its witness module exists, runs +// in the required floor, and one of its claims is enrolled and firing. The document stated the +// right invariant in its own review bar ("every phase ships with a discriminating witness that goes +// RED when the carrier regresses") and then tracked itself by hand anyway, so it went stale by a +// full phase with nothing to notice. A hand-maintained status is the execution-provenance failure +// applied to a plan: it reads identically whether the phase landed or nobody updated the line. +// +// So the status is DERIVED from the witness roster rather than typed. What that buys and what it +// does not, stated so neither is overread: the roster below is HAND-AUTHORED, so a phase whose +// witness is never declared here reads Unwitnessed exactly like a phase with no witness at all. +// This is therefore a CITATION, one step above a checkbox because there is a single authority for +// the answer instead of one per rendering, and one step below evidence. +// +// NEXT RUNG, naming the capability rather than an artifact: reading claim OUTCOMES at claim-identity +// grain from inside `.dag`. The required floor already computes exactly that join -- its +// `required-floor-disposition` output carries one row per claim identity with the outcome that +// claim reached -- but it is an out-of-band run artifact, not something a `.dag` fold can consult, +// so no declaration here can be green-by-execution about a phase. When that capability lands, +// `value_null_phase_standing` reads the outcome instead of the roster and the citation becomes +// evidence. +type ValueNullPhase + = PhaseCarrierWitnesses + | PhaseStopProducingNull + | PhaseDeleteNullBridges + | PhaseNoneLiteralMigration + | PhaseCrossRepresentationEquality + | PhaseArgumentCoercion + | PhasePrimitiveSignatureDenominator + +type ValueNullPhaseWitness { + phase: ValueNullPhase + claim: NonEmptyStr +} + +type ValueNullPhaseStanding + = PhaseWitnessEnrolled { claim: NonEmptyStr } + | PhaseUnwitnessed + +// Equality is DERIVED from one exhaustive projection rather than written as a 7x7 comparison, +// following `std.fermi` `fermi_ordinal`. The first draft of this function matched `a` and then +// matched `b` inside each arm with a `_ => false` wildcard, which the non-fold residue detector +// correctly flagged: a wildcard over a CLOSED coproduct is un-migrated modeling, because adding an +// eighth phase would silently take the `_` arm at seven sites instead of failing to compile. Here +// a new arm makes `value_null_phase_ordinal` non-exhaustive and the compiler refuses. +fn value_null_phase_ordinal(phase: ValueNullPhase) -> Int { + match phase { + PhaseCarrierWitnesses => 0 + PhaseStopProducingNull => 1 + PhaseDeleteNullBridges => 2 + PhaseNoneLiteralMigration => 3 + PhaseCrossRepresentationEquality => 4 + PhaseArgumentCoercion => 5 + PhasePrimitiveSignatureDenominator => 6 + } +} + +fn value_null_phase_eq(a: ValueNullPhase, b: ValueNullPhase) -> Bool { + value_null_phase_ordinal(phase: a) == value_null_phase_ordinal(phase: b) +} + +// One row per phase that has a discriminating witness enrolled today. Phase A's rows are the +// carrier-pinning claims in `v2.test.manual.value_null_split_witness`; Phase B's is the +// construction claim added while Phase B was built (session still-swift-363, PR gunbc#9785, held). +// A phase absent from this list has no enrolled discriminator, which is the honest reading of +// "not started" and is NOT the same statement as "not landed". +data value_null_phase_witnesses: List = [ + ValueNullPhaseWitness { + phase: PhaseCarrierWitnesses, + claim: "v2.test.manual.value_null_split_witness.raw_get_miss_differs_from_optional_absent" as NonEmptyStr, + }, + ValueNullPhaseWitness { + phase: PhaseCarrierWitnesses, + claim: "v2.test.manual.value_null_split_witness.map_get_miss_is_absent_not_present" as NonEmptyStr, + }, + ValueNullPhaseWitness { + phase: PhaseStopProducingNull, + claim: "test.claim.first_optional_construction_witness.first_of_a_list_whose_head_is_an_absent_optional_is_present_of_absent" as NonEmptyStr, + }, +] + +fn value_null_phase_standing(phase: ValueNullPhase) -> ValueNullPhaseStanding { + fold( + value_null_phase_witnesses, + init: PhaseUnwitnessed, + f: fn(acc, w) { + match acc { + PhaseWitnessEnrolled { claim: _ } => acc + PhaseUnwitnessed => + if value_null_phase_eq(a: w.phase, b: phase) { + PhaseWitnessEnrolled { claim: w.claim } + } else { + acc + } + } + } + ) +} + +fn value_null_phase_standing_label(phase: ValueNullPhase) -> String { + match value_null_phase_standing(phase: phase) { + PhaseWitnessEnrolled { claim: c } => concat("discriminator enrolled: `", concat(c as String, "`")) + PhaseUnwitnessed => "no discriminator enrolled" + } +} fn value_null_split_body() -> List { [ - p(text: "**Status:** lane opened (keen-ferret-250) · **Parent:** model↔realization fork §3.2 · **DESIGN.md open thread** · Linked from [model-realization-fork.md](model-realization-fork.md) and [fail-closed-lockdown.md](fail-closed-lockdown.md) §4 tier-1."), - p(text: "**Verified against the live tree 2026-07-26.** Census counts are receipts; re-check before acting."), + p(text: "**Ownership: none.** This plan was opened by a lane whose session no longer exists -- a `--to` addressed to it is refused as `recipient session not found`, and the name appears in no work item. A lane name written inside a document is a CITATION and rots exactly like a `file:line` or a merge-event trigger; absence from the live session graph is decidable, presence in this paragraph is not. Read the plan as an unowned authority to work AGAINST, never as a lane to defer to. **Parent:** model↔realization fork §3.2 · **DESIGN.md open thread** · Linked from [model-realization-fork.md](model-realization-fork.md) and [fail-closed-lockdown.md](fail-closed-lockdown.md) §4 tier-1."), + p(text: "**Census counts are receipts; re-check before acting.** Sections 0-3 were verified against the live tree on 2026-07-26 and have not been re-verified since. Sections 4, 4b and the phase standings were verified 2026-08-31, and the two dates are kept apart deliberately: a single freshness stamp over a document whose halves were measured five weeks apart is the same overclaim as a folded outcome column."), h2(text: "0. Problem — one native carrier, four meanings"), p(text: "`Value::Null` overloads four distinct semantics today: (1) the `None`/`none` literal and `LitNull`, (2) `Optional::Absent` (bridged in `match_pattern` at `v1_interpreter.rs:2830`), (3) `Witness::Violates` on map miss (bridged at `:2808` with a fabricated diagnostic), (4) untyped lookup miss (`raw_map_lookup`, `list_get_at_or_null`, `get` on map/list). A blanket `CrossRepresentationEquality` guard cannot close the Optional/Witness straddle — `present == None → false` is *legitimate* at ~218 corpus sites — so the fix is **splitting**, not grounding onto one sentinel."), h2(text: "1. Target carriers (construction authority)"), @@ -45,12 +152,29 @@ fn value_null_split_body() -> List { li(text: "Existing witnesses: `witness_option_bridge_test.dag` (map_get → Present/Absent at model layer); `cross_representation_equality.dag` roster includes `Optional` × `native_value_null` straddle (target: remove when grounded)."), ]), h2(text: "4. Phased landing (construction-first)"), - tasks(items: [ - task(state: Unchecked, text: "**Phase A (this lane):** plan + discriminating witnesses pinning carrier invariants (`value_null_split_witness_test.dag`); emitter row table above is authority for S2 emit."), - task(state: Unchecked, text: "**Phase B:** stop *producing* `Null` where the return type is `Optional` — route `map_get`/`get`+Optional context through `map_lookup_as_optional` (keep raw `get` returning bare value + `Null` miss for `map_lookup_dual_dispatch` until typed overload lands)."), - task(state: Unchecked, text: "**Phase C:** delete `match_pattern` `Null` bridges (`:2808–2834`) once no producer emits `Null` for Optional/Witness arms."), - task(state: Unchecked, text: "**Phase D:** type-directed `None` literal → `optional_absent()` where inhabiting `Optional<_>`; migrate `== None` sites (~218) to `match Absent` or `optional_is_absent` helper."), - task(state: Unchecked, text: "**Phase E:** cross-representation equality — ground `Optional` so `Absent` variant reconciles with narrowed `Null` *only* at the lookup-miss boundary; remove `Optional`×`native_value_null` from testgen roster; bundle `CrossRepresentationEquality` guard removal with this phase (fenced in model-realization-fork §3.1)."), + p(text: "**Standing is derived, never ticked.** Each row's standing is `value_null_phase_standing`, a fold over the enrolled-witness roster in this module -- see the note above it for exactly how far that goes (a citation, not evidence) and for the capability that would close the gap. An earlier revision of this section was a hand-checked task list in which every phase, INCLUDING the landed Phase A, read unchecked."), + TableBlock { + header: row(cells: [cell(text: "phase"), cell(text: "content"), cell(text: "standing")]), + alignments: [AlignNone, AlignNone, AlignNone], + rows: [ + row(cells: [cell(text: "A"), cell(text: "plan + discriminating witnesses pinning carrier invariants (`value_null_split_witness_test.dag`); the emitter row table in section 2 is authority for S2 emit"), cell(text: value_null_phase_standing_label(phase: PhaseCarrierWitnesses))]), + row(cells: [cell(text: "B"), cell(text: "stop *producing* `Null` where the return type is `Optional` -- route `map_get`/`get`+Optional context through `map_lookup_as_optional`. Extends to `first`/`last`/`lookup`, whose `std.algebra` rows declare `OptionalOf` and whose interpreter arms returned the raw element"), cell(text: value_null_phase_standing_label(phase: PhaseStopProducingNull))]), + row(cells: [cell(text: "C"), cell(text: "delete the `match_pattern` `Null` bridges once no producer emits `Null` for Optional/Witness arms"), cell(text: value_null_phase_standing_label(phase: PhaseDeleteNullBridges))]), + row(cells: [cell(text: "D"), cell(text: "type-directed `None` literal to `optional_absent()` where inhabiting `Optional<_>`; migrate the `== None` sites to `match Absent` or an `optional_is_absent` helper"), cell(text: value_null_phase_standing_label(phase: PhaseNoneLiteralMigration))]), + row(cells: [cell(text: "E"), cell(text: "cross-representation equality -- ground `Optional` so `Absent` reconciles with narrowed `Null` ONLY at the lookup-miss boundary; remove the `Optional`x`native_value_null` testgen straddle; bundle the `CrossRepresentationEquality` guard removal"), cell(text: value_null_phase_standing_label(phase: PhaseCrossRepresentationEquality))]), + row(cells: [cell(text: "F"), cell(text: "**NEW, discovered by building Phase B.** The interpreter gains the optional-into-required-parameter coercion the Rust emitter already has in `rust_call_arg_fail_closed_unwrap` -- unwrap `Present`, refuse typed and located on `Absent`. Phase B without this hands a `Present \{ .. \}` variant to every value-position call site"), cell(text: value_null_phase_standing_label(phase: PhaseArgumentCoercion))]), + row(cells: [cell(text: "G"), cell(text: "**NEW, and it gates F.** Close the language-primitive denominator so `SignatureNotGrounded` means \"not a language primitive\" rather than \"not modelled yet\". A builtin call never reaches the `.dag` call path, and `builtin_function_registry` carries a RETURN TYPE only, so argument cardinality cannot be derived for one"), cell(text: value_null_phase_standing_label(phase: PhasePrimitiveSignatureDenominator))]), + ], + }, + h2(text: "4b. What Phase B costs, measured"), + p(text: "Phase B was built and measured on a held draft (session still-swift-363, gunbc#9785, not landed). The required-witnesses-floor result is the number this plan should carry, because it is the argument against anyone later proposing Phase B is small enough to land alone."), + ul(items: [ + li(text: "`planned=3141 passed=2630 known_red_held=15 failed=442` against a baseline of ~0."), + li(text: "The summary's `failed` FOLDS two states. Read at claim-identity grain from the run's disposition output: **442 runtime-errored-before-verdict**, 6 failed assertions, 1 budget-refused, 47 route-gap, 15 known-red-held. The job log prints only the 6, which reads as a truncated log and is not."), + li(text: "**All 442 are `v2.test.*` and none is a `dag/test/claim` witness.** The cause is self-host coupling: v2 is `.dag` interpreted by the v1 seed, so changing the interpreter changes the v2 COMPILER's behaviour as it executes. Phase B's cost lands on the interpreted v2 compiler, not on corpus witnesses -- which is not what a reader of sections 0-3 would predict."), + li(text: "The 6 assertion failures are this plan's own `raw_get_miss_differs_from_optional_absent`, two `self_host_symbol_identity_binding_witness` claims comparing `== none`, `cargo_build_run_argv`, and two `emit_host_shell_exec_run_equals_eval` claims."), + li(text: "**The Phase A witness predicted its own flip in writing** -- its comment says `raw_get_miss_differs_from_optional_absent` \"flips RED in Phase B when get+Optional routes through `map_lookup_as_optional`\". It did. That is the enrolled signal that Phase B landed, so retiring its expected-red disposition is PART of Phase B and not a repair to it."), + li(text: "The `== none` reds are Phase D arriving early, and they confirm section 0's count from the other direction: `none` EVALUATES to `Value::Null` in the interpreter's variable evaluation, so a raw miss compares equal to `none` because it IS `Null`, while a constructed `Absent` variant does not compare equal at all."), ]), h2(text: "5. Review bar"), p(text: "No absorbing fallback: a miss must not widen to `Null` when the type is `Optional` or `Witness`. No new per-site `if matches!(v, Value::Null)` bridges without a counted dissolution trigger. Every phase ships with a discriminating witness that goes RED when the carrier regresses."), diff --git a/dag/gunbc/recurring_failure_mode.dag b/dag/gunbc/recurring_failure_mode.dag index 1ac1f81384d..cd16d2b8d44 100644 --- a/dag/gunbc/recurring_failure_mode.dag +++ b/dag/gunbc/recurring_failure_mode.dag @@ -228,6 +228,12 @@ data unbacked_execution_claim: RecurringFailureMode = RecurringFailureMode { evidence: [], } +data coarser_parallel_authority: RecurringFailureMode = RecurringFailureMode { + identity: "coarser_parallel_authority" as NonEmptyStr, + authored: "**coarser parallel authority** (two carriers are AUTHORED for one fact and one of them is LOSSIER, so the fork never presents as duplication — it presents as abstraction. §3 already forbids two authorities for one fact; what this row adds is the reason that rule keeps being read past, because the second carrier does not look like a copy. A coarse answer and a fine answer never contradict each other in the way two copies do: the coarse one reads as *less specific*, which a reviewer accepts as a summary, so the disagreement is invisible until an input distinguishes the collapsed cases. RECEIPT (measured on main while censusing the `first` interpreter/emitted divergence, gunbc#9785): `v1.compiler.infer_method` `builtin_function_registry` maps a primitive name to a RETURN TYPE, and `std.algebra` `AlgebraFieldTemplate` carries `param_types` and `return_type` for the same operations. 20 of the registry's names also have algebra rows, and the two already answer differently, because the registry is RECEIVER-BLIND where the algebra rows are receiver-relative: `reverse` is `List` against `ReceiverSelf`, so on a `String` receiver the two carriers name different types; `map_keys` and `map_values` share ONE element type variable where algebra distinguishes `ReceiverKey` from `ReceiverValue`, so for any `Map` with `K` /= `V` the registry cannot be right about both; `concat` is `String` against `ReceiverSelf`, so a list concat types as a String; `get` collapses the List reading and the Map reading the algebra rows keep apart. None of these is a stale copy that drifted — the registry was authored coarse and has been coarse the whole time. **WHAT MAKES THE COARSE CARRIER LOOK LEGITIMATE is that its coarseness is usually true of the QUESTION ITS FIRST CONSUMER ASKED.** A caller that only wants \"is this name a builtin\" is well served by a name-to-return-type map, and the carrier is correct for that consumer on the day it lands. It becomes an authority for a fact it never modelled the moment a second consumer asks a finer question of it, and it answers, because a map is total over its keys. **RECOGNITION RULE: when two carriers answer about one operation and one is coarser, ask whether the coarse answer is DERIVED from the fine one or AUTHORED beside it. A derived projection cannot disagree; an authored one is a fork whose disagreements are silent by construction, since \"less specific\" and \"different\" are indistinguishable at the call site.** The repair is never to reconcile the two rosters — that is a second synchronisation obligation, and §5 calls a check standing where construction was available validation. The repair is RELOCATION: the coarse carrier stops being an authority and becomes a projection of the fine one, or its rows leave for the layer that actually owns them. Here the same relocation dissolves a second class: once the registry is no longer a signature authority for anything `std.algebra` owns, there is no second declaration left to disagree, and the population that remains — primitives with no algebra row — is a closeable gap rather than an open denominator.)", + evidence: [], +} + data recurring_failure_mode_roster: List = [ hollow_alias, state_space_conflation, @@ -259,4 +265,5 @@ data recurring_failure_mode_roster: List = [ executed_conjunct_discriminates_nothing, unbacked_execution_claim, mitigation_injected_where_judgment_declined, + coarser_parallel_authority, ] diff --git a/dag/test/claim/first_optional_construction_witness_test.dag b/dag/test/claim/first_optional_construction_witness_test.dag new file mode 100644 index 00000000000..344c7a6793c --- /dev/null +++ b/dag/test/claim/first_optional_construction_witness_test.dag @@ -0,0 +1,133 @@ +module test.claim.first_optional_construction_witness + +// WHAT THIS PINS. `dag/std/algebra.dag` declares `first`, `last`, `get`, `lookup` and `map_get` +// with `return_type: OptionalOf { inner: ReceiverElement }`. That one row is what makes the Rust +// emit arm produce `Option`; the interpreter used to answer the same question by hand and +// answer it differently -- `first` returned `items.front().cloned().unwrap_or(Null)`, i.e. the RAW +// ELEMENT. Two realizations of one declared signature that disagree are DESIGN.md section 5 silent +// wrongness: `(["x"] |> filter(n => true) |> first) == Present { value: "x" }` typechecked and +// returned FALSE interpreted while returning true emitted, with no diagnostic anywhere. +// +// WHY THE PRE-EXISTING first WITNESSES DID NOT CATCH IT. `branded_list_first_optional_witness` +// eliminates `first` with `match { Present { value: v } => .. Absent => .. }` over a NON-optional +// element type, and the interpreter carried compensating raw-unwrap arms in `match_pattern` that +// made exactly that shape agree. So the whole match-scrutinee population -- the large majority of +// the corpus's terminal `|> first` sites -- was green on a divergence it could not observe. The +// two shapes below are the ones the compensation cannot cover, and they are the discriminating +// RED: each one goes red against the raw-element arm and green against the constructed Optional. +// +// SHAPE 1 -- THE ELEMENT TYPE IS ITSELF AN Optional. `[Absent] |> first` must be +// `Present { value: Absent }`, one head that is an absent optional. Under the raw arm the head +// came back bare, so the outer `Present` pattern saw an `Absent` variant and the whole match took +// the OUTER Absent arm: a one-element list read as an empty one. +// +// SHAPE 2 -- THE RESULT IS COMPARED RATHER THAN MATCHED. `==` against `Present { value: .. }` has +// no pattern for a compensation arm to intercept, so it reads the representation directly. + +fn classify(xs: List>) -> String { + match xs |> first { + Present { value: inner } => + match inner { + Present { value: s } => s + Absent => "OUTER-PRESENT-INNER-ABSENT" + } + Absent => "OUTER-ABSENT" + } +} + +// Positive control: the empty list is the one case the raw arm already got right, so a green here +// with the two reds below is what separates "the Optional is constructed" from "the arm refuses". +test fn first_of_an_empty_list_is_absent() -> Bool { + classify(xs: []) == "OUTER-ABSENT" +} + +// SHAPE 1, discriminating: red against `unwrap_or(Value::Null)`, which reported "OUTER-ABSENT". +test fn first_of_a_list_whose_head_is_an_absent_optional_is_present_of_absent() -> Bool { + classify(xs: [Absent]) == "OUTER-PRESENT-INNER-ABSENT" +} + +// Positive control for the same shape: a present head must still reach its payload, so the fix is +// not "wrap everything and lose the value". +test fn first_of_a_list_whose_head_is_a_present_optional_reaches_the_payload() -> Bool { + classify(xs: [Present { value: "x" }]) == "x" +} + +// SHAPE 2, discriminating: this is the exact comparison the BT-0 lane found returning false +// interpreted and true emitted. +test fn first_result_compares_equal_to_the_optional_the_roster_declares() -> Bool { + (["x"] |> filter(n => true) |> first) == Present { value: "x" } +} + +// SHAPE 2, the other direction. The raw arm made this TRUE -- the bare element compared equal to +// itself -- which is the same divergence read from the side where the interpreter was permissive +// rather than wrong-answered. +test fn first_result_does_not_compare_equal_to_the_bare_element() -> Bool { + ((["x"] |> filter(n => true) |> first) == Present { value: "x" }) + && !(match ["x"] |> filter(n => true) |> first { Present { value: v } => v == "y" Absent => true }) +} + +// `last` carries the identical roster row and had the identical raw arm. +test fn last_of_a_list_whose_tail_is_an_absent_optional_is_present_of_absent() -> Bool { + match [Present { value: "a" }, Absent] |> last { + Present { value: inner } => + match inner { + Present { value: _ } => false + Absent => true + } + Absent => false + } +} + +// `get` carries it too, and its absent case was the same or-Null read. +test fn get_past_the_end_is_absent_and_get_in_bounds_is_present() -> Bool { + (match ["a"] |> get(1) { Present { value: _ } => false Absent => true }) + && (match ["a"] |> get(0) { Present { value: s } => s == "a" Absent => false }) +} + +// THE COERCION THIS REPAIR ADDED MUST NOT FIRE ON A FREE TYPE VARIABLE. Constructing the Optional +// created a second obligation: an argument that is now `Optional` meets a parameter declared +// `T`, so the interpreter grew the coercion the Rust arm already had. Applied to a GENERIC formal +// that rule is wrong in both directions, because `T` declares nothing about cardinality and +// `Optional` is a legitimate instantiation rather than a cardinality escape. Measured on the +// first head that carried the coercion: `Present` was SILENTLY UNWRAPPED into the callee -- the +// caller's `T = Optional` arrived as `Int`, which is the same silent divergence this whole +// module exists to remove, pointed at a new seam -- and `Absent` was REFUSED outright with a +// `CallContractMismatch`, which took down the generated-artifact regen actuator. The predicate now +// reads the fn's own declared type-parameter list, so a free type variable is not a required +// formal. These two are the discriminating REDs for that seam and stay enrolled after the climb. +fn observe_arrival(value: T) -> String { + match value { + Present { value: _ } => "PRESENT" + Absent => "ABSENT" + _ => "UNWRAPPED" + } +} + +// RED against the unwrapping arm, which reported "UNWRAPPED": the callee received the bare element. +test fn a_present_optional_into_a_free_type_variable_arrives_whole() -> Bool { + observe_arrival(value: [7] |> first) == "PRESENT" +} + +// RED against the refusing arm, which raised CallContractMismatch on a legitimate instantiation. +test fn an_absent_optional_into_a_free_type_variable_is_not_refused() -> Bool { + observe_arrival(value: [] |> first) == "ABSENT" +} + +// THE WALL THAT KEEPS THE COMPARISON SEAM FROM ANSWERING QUIETLY, and its positive control. +// Constructing the `Optional` made every consumer that COMPARES a `first()` result to a bare value +// compare across two representations, and `Value::eq` cannot decide those: measured before the +// wall, `["schema-v2", "body"].first() == "schema-v2"` answered FALSE with no diagnostic, and +// `[] |> first == none` answered FALSE too. Nine of the fourteen such sites in the generated-artifact +// gate's import closure are merge-admission receipt schema checks, where a quiet `false` rejects a +// valid receipt. A failure arm that fabricates a plausible answer instead of refusing is what +// DESIGN section 5 forbids outright, so both shapes now raise `CrossRepresentationEquality`. +// +// THE TWO REDS ARE FIXTURE-MEASURED, NOT ENROLLED HERE, AND THAT IS STATED RATHER THAN GLOSSED: a +// `test fn` returns `Bool` and an interpreter refusal aborts evaluation, so this harness cannot +// express "this expression refuses". Enrolling them needs a harness that can catch a refusal and +// assert its REASON, which is this seam's next-rung trigger. What IS enrolled is the control below, +// and it is the one that keeps the wall from being over-broad — a wall that refused every +// comparison would also pass a red-only check. +test fn an_optional_compared_against_an_optional_is_not_a_straddle() -> Bool { + (["a"] |> first) == Present { value: "a" } +} diff --git a/dag/test/claim/merge_admission_attempt_witness_test.dag b/dag/test/claim/merge_admission_attempt_witness_test.dag index 7d3c1a79953..368050d4cdb 100644 --- a/dag/test/claim/merge_admission_attempt_witness_test.dag +++ b/dag/test/claim/merge_admission_attempt_witness_test.dag @@ -577,3 +577,202 @@ test fn schemas_are_distinct_and_pinned_to_their_declared_versions() -> Bool { && (merge_admission_receipt_schema_v2 == "gunbc.merge_admission_receipt.v3") && (merge_admission_tested_subject_schema == "gunbc.merge_admission_tested_subject.v2") } + +// THE GUARD ARMS THIS SUITE NEVER EXERCISED, and the receipt that proves it did not. +// +// parse_receipt_wire_v2 rejects a receipt whose SCHEMA line is wrong or whose required fields are +// BLANK, and parse_tested_subject_wire has the same four guards over its own five-line wire; the +// rows for the SUBJECT parser are further down, added after review of #9912 found that this comment +// claimed both parsers while only the receipt one had rows. Those arms had no case here: the suite reaches +// parse_gate_roster_hash_wire and compose_walk_attempt_id directly and feeds the wire parsers only +// well-formed text, a trailing line and a malformed PR line. Measured, not assumed -- mutating the +// blank-field comparison in gunbc.merge_admission_produce to a string no field can equal left all +// 30 witnesses PASSING. An uncovered guard reads as a covered one, and a rewrite of these arms +// would have been verified by a suite that could not see them. +// +// Each row varies ONE line of a wire that parses, which is the convention the rows above state. + +fn wire_v2_with_lines(schema: String, attempt: String, roster: String, conclusion: String, head: String, base: String) -> String { + join([schema, attempt, roster, conclusion, head, base], "\n") +} + +fn good_v2_lines_conclusion() -> String { + match parse_receipt_wire_v2(text: render_receipt_wire_v2(receipt: receipt_fx(attempt: attempt_a(), head: head_sha_fx))) { + Present { value: _ } => "success" + Absent => "UNPARSEABLE-FIXTURE" + } +} + +fn v2_refuses(text: String) -> Bool { + match parse_receipt_wire_v2(text: text) { Present { value: _ } => false Absent => true } +} + +// Positive control, asserted at CARRIER GRAIN rather than on the verdict. A parser that returns +// `Present` before and after a rewrite while binding a different head SHA, attempt id, base commit +// or roster hash is NOT a no-op, and a `Present { value: _ } => true` row cannot see that. Every +// field the accepted class carries is asserted, so a rewrite that reads the wrong line -- an +// off-by-one in a `skip`, a field crossed with its neighbour -- goes red here rather than passing +// as an unchanged verdict. +test fn wire_v2_built_from_explicit_lines_parses_with_every_field_bound() -> Bool { + match parse_receipt_wire_v2(text: wire_v2_with_lines( + schema: merge_admission_receipt_schema_v2, + attempt: attempt_a_raw, + roster: render_gate_roster_hash_wire(hash: roster_fx()), + conclusion: good_v2_lines_conclusion(), + head: head_sha_fx, + base: base_commit_fx, + )) { + Present { value: parsed } => + ((parsed.attempt_id as String) == attempt_a_raw) + && (parsed.tested_head_sha == head_sha_fx) + && (parsed.tested_base_commit_sha == base_commit_fx) + && (parsed.gate_roster_hash == roster_fx()) + && match parsed.pr_number { Absent => true Present { value: _ } => false } + && match parsed.conclusion { Success => true _ => false } + Absent => false + } +} + +test fn wire_v2_refuses_a_wrong_schema_line() -> Bool { + v2_refuses(text: wire_v2_with_lines( + schema: "gunbc.merge_admission_receipt.v2", + attempt: attempt_a_raw, + roster: render_gate_roster_hash_wire(hash: roster_fx()), + conclusion: good_v2_lines_conclusion(), + head: head_sha_fx, + base: base_commit_fx, + )) +} + +test fn wire_v2_refuses_a_blank_gate_roster_hash_line() -> Bool { + v2_refuses(text: wire_v2_with_lines( + schema: merge_admission_receipt_schema_v2, + attempt: attempt_a_raw, + roster: "", + conclusion: good_v2_lines_conclusion(), + head: head_sha_fx, + base: base_commit_fx, + )) +} + +test fn wire_v2_refuses_a_blank_head_sha_line() -> Bool { + v2_refuses(text: wire_v2_with_lines( + schema: merge_admission_receipt_schema_v2, + attempt: attempt_a_raw, + roster: render_gate_roster_hash_wire(hash: roster_fx()), + conclusion: good_v2_lines_conclusion(), + head: "", + base: base_commit_fx, + )) +} + +test fn wire_v2_refuses_a_blank_base_commit_line() -> Bool { + v2_refuses(text: wire_v2_with_lines( + schema: merge_admission_receipt_schema_v2, + attempt: attempt_a_raw, + roster: render_gate_roster_hash_wire(hash: roster_fx()), + conclusion: good_v2_lines_conclusion(), + head: head_sha_fx, + base: "", + )) +} + +// The object-id wire's algorithm prefix is the other comparison pair, and its else-arm answers none +// for an unrecognised algorithm. BOTH declared prefixes need a VALID wire of their own: a row that +// accepts sha1 and rejects md5 leaves the sha256 comparison free to become always-false, which is +// the exact failure class this change exists to prevent. Caught in review of #9912, which is the +// same defect one parser over from the one the mutation control caught. +test fn object_id_wire_accepts_a_valid_sha1_wire() -> Bool { + match parse_git_object_id_wire(raw: "sha1:abc1234def5678901234567890abcd1234567890") { + Present { value: oid } => git_object_id_wire_hex(oid: oid) == "abc1234def5678901234567890abcd1234567890" + Absent => false + } +} + +test fn object_id_wire_accepts_a_valid_sha256_wire() -> Bool { + match parse_git_object_id_wire(raw: "sha256:abc1234def5678901234567890abcd12abc1234def5678901234567890abcd12") { + Present { value: oid } => git_object_id_wire_hex(oid: oid) == "abc1234def5678901234567890abcd12abc1234def5678901234567890abcd12" + Absent => false + } +} + +test fn object_id_wire_refuses_an_undeclared_algorithm() -> Bool { + match parse_git_object_id_wire(raw: "md5:abc1234def5678901234567890abcd1234567890") { + Present { value: _ } => false + Absent => true + } +} + +// THE SUBJECT PARSER'S FOUR GUARDS, WHICH THE FIRST CUT OF THESE ROWS LEFT UNCOVERED. Review of +// #9912 found that the rows above exercised only `parse_receipt_wire_v2`, while the comment claimed +// both parsers -- five of the ten rewritten comparisons had no discriminating evidence at all. +// `parse_tested_subject_wire` takes exactly five lines: schema, attempt id, base_ref, head_sha, +// base_commit_sha, and rejects a wrong schema line or any of the last three blank. + +fn subject_wire_with_lines(schema: String, attempt: String, base_ref: String, head: String, base_commit: String) -> String { + join([schema, attempt, base_ref, head, base_commit], "\n") +} + +fn subject_refuses(text: String) -> Bool { + match parse_tested_subject_wire(text: text) { Present { value: _ } => false Absent => true } +} + +// Positive control for the builder, at carrier grain for the same reason as the receipt one above: +// `base_ref`, `head_sha` and `base_commit_sha` are three consecutive lines, so a rewrite that reads +// the wrong one keeps the verdict and changes the value. +test fn subject_wire_built_from_explicit_lines_parses_with_every_field_bound() -> Bool { + match parse_tested_subject_wire(text: subject_wire_with_lines( + schema: merge_admission_tested_subject_schema, + attempt: attempt_a_raw, + base_ref: "origin/main", + head: head_sha_fx, + base_commit: base_commit_fx, + )) { + Present { value: parsed } => + ((parsed.attempt_id as String) == attempt_a_raw) + && (parsed.base_ref == "origin/main") + && (parsed.head_sha == head_sha_fx) + && (parsed.base_commit_sha == base_commit_fx) + Absent => false + } +} + +test fn subject_wire_refuses_a_wrong_schema_line() -> Bool { + subject_refuses(text: subject_wire_with_lines( + schema: "gunbc.merge_admission_tested_subject.v1", + attempt: attempt_a_raw, + base_ref: "origin/main", + head: head_sha_fx, + base_commit: base_commit_fx, + )) +} + +test fn subject_wire_refuses_a_blank_base_ref_line() -> Bool { + subject_refuses(text: subject_wire_with_lines( + schema: merge_admission_tested_subject_schema, + attempt: attempt_a_raw, + base_ref: "", + head: head_sha_fx, + base_commit: base_commit_fx, + )) +} + +test fn subject_wire_refuses_a_blank_head_sha_line() -> Bool { + subject_refuses(text: subject_wire_with_lines( + schema: merge_admission_tested_subject_schema, + attempt: attempt_a_raw, + base_ref: "origin/main", + head: "", + base_commit: base_commit_fx, + )) +} + +test fn subject_wire_refuses_a_blank_base_commit_line() -> Bool { + subject_refuses(text: subject_wire_with_lines( + schema: merge_admission_tested_subject_schema, + attempt: attempt_a_raw, + base_ref: "origin/main", + head: head_sha_fx, + base_commit: "", + )) +} diff --git a/docs/plans/builtin-registry-population-partition.md b/docs/plans/builtin-registry-population-partition.md new file mode 100644 index 00000000000..7ee2441b43c --- /dev/null +++ b/docs/plans/builtin-registry-population-partition.md @@ -0,0 +1,211 @@ +# Partitioning `builtin_function_registry`: the denominator closes by relocation + +## Why this document exists + +`v1.compiler.infer_method` `builtin_function_registry` carries 131 names and maps each to a RETURN +TYPE. `std.primitive_identity` `primitive_signature` resolves a full parameter signature for a +primitive by keying into `std.algebra`'s `AlgebraFieldTemplate` rows. 20 of the registry's names +have such a row and resolve; **111 answer `SignatureNotGrounded`.** + +While that 111 is a mixed population, `SignatureNotGrounded` is ambiguous between *"not a language +primitive"* and *"a language primitive nobody has modelled yet"*, and a coercion that fails closed +on it cannot distinguish a legitimate absence from an unmodelled one. Closing that ambiguity is the +precondition for the interpreter gaining the optional-into-required-parameter coercion its emitted +counterpart already has (→ [first-optional divergence census](first-optional-divergence-census.md)). + +**The partition is by RELOCATION, not classification.** §3 holds that interface, realization and +policy are three facts and not one row, and that the dispatch selecting a realization is itself +realization. A lens's or a host transport's parameter shape is a realization fact; it does not +belong in a language-primitive signature authority at all. So the two populations are not two kinds +of one thing awaiting a discriminator — they are two different things sharing one table, and the +partition ends with the second population's rows leaving. + +## Four candidate predicates, measured, and why none of them decides it alone + +Recorded so the next reader does not re-derive them. Each was tested against the actual 111 rather +than reasoned about. + +1. **Join on the interpreter's primitive-surface roster.** Fails by construction: + `gunbc.v1_interpreter_primitive_surface` enumerates an arm for BOTH populations, so it + classifies `doc_graph_orphan_count` and `parse_int` identically. It answers "is there an arm", + which is true of every builtin. +2. **Does the name have a `.dag` `fn` declaration?** This is the `HostRealizedSeam` shape from + `std.primitive_projection`, whose doc comment establishes seams *by reading the declaration, not + by matching the name*. It identifies 8 of the 111 and leaves 103 undecided, and it + false-positives on `string_contains`, which matches a declaration inside a witness test. +3. **Does the interpreter arm touch the host?** Fails in both directions on the real population. + `parse_int`, `string_length`, `code_point` and `is_xid_start` look host-touching because their + arms delegate to `v1_rt` helpers; `decl_facts` and `doc_graph_orphan_count` look pure because + their host call is further down the arm than any fixed reading window. +4. **How many modules reference the name?** The strongest of the four and still not sufficient. It + separates cleanly at the extremes — `string_contains` (451 referencing modules), `string_length` + (94), `parse_int` (41) against `doc_graph_orphan_count` (1, in `src/v2/lens/doc_reachability`) — + but breadth of USE is not ownership of the FACT: `filesystem_read` (63), `compile_dag_rust_emit_check` + (71) and `shell_materialize_operation_argv` (10) are widely-used TRANSPORTS, and + `scan_while` / `scan_to_eol` / `skip_horizontal_ws` are narrow LANGUAGE primitives whose only + callers are inside the tokenizer. + +**What the fourth predicate does supply, and it is the useful part, is the HOME.** Its value is not +the count but the module the references land in: `fallback_arm_census_facts` is +`src/v2/lens/fallback_arm_census`'s fact, `emit_host_run_transport` is `src/v2/compiler/emit_host`'s. +Naming the owning module is the §3 question ("a fact's home is its layer") asked mechanically. The +count is a symptom of the answer, never the criterion, and every row below carries its home. + +## The criterion actually applied + +For each name: **does the operation's meaning come from the LANGUAGE, or from a domain authority +that owns it?** A language primitive is one the substrate itself must be able to talk about +regardless of which lens, workflow or instrument exists — text and code-point manipulation, set +construction, hashing, identifier classification, lexer scanning. Everything else names a fact some +module owns, and its signature belongs at that module's declaration, which in most cases already +declares its parameters. + +Both dispositions are adjudications, not lookups, and the residue is judgement — as it must be, +since all four mechanical predicates were measured to fail. What makes them auditable is that each +row states its home, so a disagreement is about one named module rather than about the rule. + +## `LanguagePrimitive` — 24 names + +Disposition: ground a signature through `std.primitive_identity`. Once the transports below have +left the registry, `SignatureNotGrounded` over this population means unambiguously "a language +primitive whose signature is not yet modelled" — a closeable gap, and the property the coercion +needs in order to fail closed honestly. + +| name | referencing modules | first non-test reference | +|---|---|---| +| `string_contains` | 450 | `dag/extdeps/astronomy/stellar_classification.dag` | +| `string_length` | 93 | `dag/extdeps/auth/jwt.dag` | +| `from_code_point` | 40 | `dag/extdeps/dns/domain_name.dag` | +| `parse_int` | 40 | `dag/extdeps/bmc/capability.dag` | +| `discriminant` | 39 | `dag/extdeps/git/git.dag` | +| `char_at` | 26 | `dag/extdeps/auth/jwt.dag` | +| `set_contains` | 20 | `dag/gunbc/emit_summary_map_consumer_partition.dag` | +| `code_point` | 19 | `dag/extdeps/auth/jwt.dag` | +| `empty_set` | 19 | `dag/gunbc/package_delivery.dag` | +| `set_insert` | 15 | `dag/gunbc/package_delivery.dag` | +| `sorted_map_keys` | 8 | `dag/gunbc/instruments/pr_containment_instrument.dag` | +| `atom_identity_hash` | 3 | `dag/std/content_hash.dag` | +| `chars_to_string` | 3 | `src/v1/00_core.dag` | +| `is_emoji_ident` | 3 | `src/v1/01_tokenize.dag` | +| `map_is_empty` | 3 | `src/v1/04_infer.dag` | +| `set_union` | 3 | `dag/std/authorization_profile.dag` | +| `hash_combine` | 2 | `dag/std/content_hash.dag` | +| `is_xid_continue` | 2 | `src/v1/01_tokenize.dag` | +| `is_xid_start` | 2 | `src/v1/01_tokenize.dag` | +| `record_source_chars_index_lookup` | 1 | `src/v1/01_tokenize.dag` | +| `scan_string_end` | 0 | `(no .dag reference)` | +| `scan_to_eol` | 0 | `(no .dag reference)` | +| `scan_while` | 0 | `(no .dag reference)` | +| `skip_horizontal_ws` | 0 | `(no .dag reference)` | + +## `Transport` — 87 names + +Disposition: the signature belongs with the realization authority named under *home*; the name +leaves the language registry. Where that module already declares the operation as a `.dag` `fn`, +the parameter list exists there and relocation supplies the signature at no authoring cost. + +| name | referencing modules | home | +|---|---|---| +| `non_fold_residue_roster_red_fixture_holds` | 0 | `(no .dag reference)` | +| `non_fold_residue_total_fold_green_fixture_holds` | 0 | `(no .dag reference)` | +| `witness_layer_roots_compile_clean_check` | 0 | `(no .dag reference)` | +| `witness_layer_roots_compile_clean_emit_check` | 0 | `(no .dag reference)` | +| `contiguous_loop_elementwise_float_kernel` | 2 | `dag/extdeps/languages/simd/kernel.dag` | +| `contiguous_loop_elementwise_kernel` | 2 | `dag/extdeps/languages/simd/kernel.dag` | +| `filesystem_read` | 62 | `dag/extdeps/llm/claude_agent_sdk_stream.dag` | +| `emit_host_native_cache_evict` | 1 | `dag/extdeps/realization/emit_on_demand_host.dag` | +| `decl_facts` | 27 | `dag/gunbc/bare_name_fork_lens.dag` | +| `compile_dag_diagnostic_census` | 28 | `dag/gunbc/compile_diagnostic_census.dag` | +| `compile_dag_rust_emit_check` | 71 | `dag/gunbc/compile_diagnostic_census.dag` | +| `shell_materialize_operation_argv` | 10 | `dag/gunbc/host/host_operation_exec.dag` | +| `witness_compile_clean_cli_floor_verdicts_agree` | 1 | `dag/gunbc/instruments/dag_compile_clean_cli_floor_agreement.dag` | +| `module_declaration_facts` | 2 | `dag/gunbc/instruments/dag_compile_clean_shard_roster.dag` | +| `install_or_consume_floor_compile_clean_gate_receipt` | 1 | `dag/gunbc/instruments/dag_compile_clean_transport.dag` | +| `consume_generated_artifact_drift_gate_receipt` | 1 | `dag/gunbc/instruments/generated_artifact_gate.dag` | +| `record_generated_artifact_drift_gate_clean` | 1 | `dag/gunbc/instruments/generated_artifact_gate.dag` | +| `record_generated_artifact_drift_gate_failure_detail` | 1 | `dag/gunbc/instruments/generated_artifact_gate.dag` | +| `compile_dag_multi_module_fixture` | 1 | `dag/gunbc/instruments/multi_module_compile_fixture.dag` | +| `test_migration_behavior_discovery_holds` | 1 | `dag/gunbc/legacy_test_behavior_disposition.dag` | +| `test_migration_legacy_behavior_ids` | 2 | `dag/gunbc/legacy_test_behavior_disposition.dag` | +| `test_migration_witness_behavior_ids` | 1 | `dag/gunbc/legacy_test_behavior_disposition.dag` | +| `data_decl_type_facts` | 3 | `dag/gunbc/lifecycle_survivor_scan.dag` | +| `namespace_structural_observation_admissions` | 2 | `dag/gunbc/namespace/namespace_structural_observations_production.dag` | +| `parse_roadmap_acceptance_event_history_jsonl` | 1 | `dag/gunbc/roadmap/roadmap_acceptance_history_carrier.dag` | +| `project_roadmap_acceptance_event_history_from_authority_text_host` | 1 | `dag/gunbc/roadmap/roadmap_acceptance_history_projection.dag` | +| `parse_stage0_cargo_manifest_bins` | 1 | `dag/gunbc/stage0/stage0_rust_host_observation.dag` | +| `observed_monotonic_nanos` | 2 | `dag/std/realization_measurement.dag` | +| `commit_witness_claim_pair_resolvable` | 1 | `dag/test/claim/commit_witness_claim_roster_witness_test.dag` | +| `doc_graph_admitted_root_count` | 1 | `dag/test/claim/doc_reachability_witness_test.dag` | +| `seed_runner_bool_false_failure_detail` | 1 | `dag/test/claim/long/extdeps_scope_placement_gate_loudness_witness_test.dag` | +| `shell_transport_operation_rows` | 1 | `dag/test/claim/operation_argv_corpus_witness_test.dag` | +| `observed_peak_resident_bytes` | 1 | `dag/test/claim/peak_resident_measured_witness_test.dag` | +| `name_resolution_policy_is_namespace_only` | 3 | `src/v1/04_env.dag` | +| `resolution_silent_pick_is_enabled` | 2 | `src/v1/04_env.dag` | +| `resolution_silent_pick_record_global_bare_lcp_pick` | 1 | `src/v1/04_env.dag` | +| `resolution_silent_pick_record_global_bare_lcp_tie` | 1 | `src/v1/04_env.dag` | +| `rc_ptr_eq` | 1 | `src/v1/04_infer.dag` | +| `rc_vec_ptr_eq` | 1 | `src/v1/04_infer.dag` | +| `type_ref_hit_ne_bind_measure_active` | 1 | `src/v1/04_resolve.dag` | +| `resolution_silent_pick_record_fn_parent_first_hit` | 1 | `src/v1/04_sigs.dag` | +| `trace_mark` | 1 | `src/v1/compile.dag` | +| `emit_host_run_transport` | 1 | `src/v2/compiler/emit_host.dag` | +| `emit_host_run_transport_cached` | 1 | `src/v2/compiler/emit_host.dag` | +| `toolchain_home_interference_probe` | 1 | `src/v2/extdeps/toolchain_interference.dag` | +| `complexity_linearity_syntactic_finding_count` | 1 | `src/v2/lens/complexity_linearity_audit.dag` | +| `complexity_linearity_syntactic_site_fired` | 1 | `src/v2/lens/complexity_linearity_audit.dag` | +| `complexity_linearity_wildcard_facts` | 1 | `src/v2/lens/complexity_linearity_audit.dag` | +| `doc_graph_dangling_link_count` | 2 | `src/v2/lens/doc_reachability.dag` | +| `doc_graph_doc_count` | 2 | `src/v2/lens/doc_reachability.dag` | +| `doc_graph_orphan_count` | 1 | `src/v2/lens/doc_reachability.dag` | +| `extdeps_qualified_name_resolves_in_derived_module_set` | 1 | `src/v2/lens/extdeps_shape_transport_policy.dag` | +| `extdeps_shape_transport_policy_facts_for_qualified_name` | 1 | `src/v2/lens/extdeps_shape_transport_policy.dag` | +| `fact_cardinality_decl_facts` | 1 | `src/v2/lens/fact_cardinality.dag` | +| `fallback_arm_census_class_count` | 1 | `src/v2/lens/fallback_arm_census.dag` | +| `fallback_arm_census_facts` | 1 | `src/v2/lens/fallback_arm_census.dag` | +| `fallback_arm_census_reconciliation_holds` | 2 | `src/v2/lens/fallback_arm_census.dag` | +| `fallback_arm_census_total` | 1 | `src/v2/lens/fallback_arm_census.dag` | +| `concept_decl_facts` | 2 | `src/v2/lens/grounding.dag` | +| `transport_script_position_facts_for_path` | 1 | `src/v2/lens/host_language_transport_script.dag` | +| `inert_carrier_declared_count` | 1 | `src/v2/lens/inert_carrier.dag` | +| `inert_carrier_names_live` | 1 | `src/v2/lens/inert_carrier.dag` | +| `export_signature_facts` | 2 | `src/v2/lens/interface_summary.dag` | +| `languages_consumer_census_data_decl_count` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `languages_consumer_census_external_consumer_count` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `languages_consumer_census_format_row_count` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `languages_consumer_census_has_external_consumer` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `languages_consumer_census_is_composition_only` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `languages_consumer_census_per_language_row_count` | 1 | `src/v2/lens/languages_consumer_census.dag` | +| `extdeps_external_authority_facts_for_qualified_name` | 1 | `src/v2/lens/mandatory_tag/corpus_scan.dag` | +| `extdeps_external_authority_live_clean_tree_holds` | 1 | `src/v2/lens/mandatory_tag/corpus_scan.dag` | +| `extdeps_external_authority_live_roster_module_count` | 1 | `src/v2/lens/mandatory_tag/corpus_scan.dag` | +| `dependency_resolution_facts` | 1 | `src/v2/lens/module_graph.dag` | +| `import_resolution_facts` | 1 | `src/v2/lens/module_graph.dag` | +| `reference_resolution_facts` | 1 | `src/v2/lens/module_graph.dag` | +| `census_corpus_roots_follow_layer_authority` | 1 | `src/v2/lens/non_fold_residue.dag` | +| `non_fold_residue_coproduct_universe_count` | 2 | `src/v2/lens/non_fold_residue.dag` | +| `non_fold_residue_count` | 1 | `src/v2/lens/non_fold_residue.dag` | +| `non_fold_residue_stale_roster_count` | 2 | `src/v2/lens/non_fold_residue.dag` | +| `non_fold_residue_unrostered_count` | 2 | `src/v2/lens/non_fold_residue.dag` | +| `test_migration_debt_module_names` | 1 | `src/v2/lens/test_migration_debt.dag` | +| `layer_import_facts` | 1 | `src/v2/std/layer_import_scan.dag` | +| `non_fold_residue_synthetic_unrostered_red_holds` | 1 | `src/v2/test/lens_non_fold_residue/non_fold_residue_test.dag` | +| `non_fold_residue_wildcard_red_fixture_holds` | 1 | `src/v2/test/lens_non_fold_residue/non_fold_residue_test.dag` | +| `observe_declared_import_closure_symbol_binding` | 1 | `src/v2/workflow/class_b_import_closure_probe.dag` | +| `class_b_import_closure_gate_not_affected_skip` | 1 | `src/v2/workflow/class_b_import_closure_transport.dag` | +| `commit_witness_claim_roster_unresolvable_count` | 1 | `src/v2/workflow/commit_witness_claim_roster.dag` | + +## What this partition dissolves + +Two classes, one relocation. Once the registry is no longer a signature authority for anything +`std.algebra` owns, the 20 overlapping names stop being two declarations of one operation — which +is the `coarser_parallel_authority` row in `gunbc.recurring_failure_mode`, filed from the measured +disagreement between the two carriers (`reverse` typed as `List` against +`ReceiverSelf`; `map_keys` and `map_values` sharing one element variable where the algebra rows +distinguish `ReceiverKey` from `ReceiverValue`; `concat` as `String` against `ReceiverSelf`; `get` +collapsing the List and Map readings). There is no second declaration left to disagree. + +## Sequencing + +This is a substrate program, not a step in a repair, and it is expected to span several PRs. This +document is the disposition census and carries no pipeline edit. Relocation lands per owning module, +so each PR is a readable diff against one authority. diff --git a/docs/plans/first-optional-divergence-census.md b/docs/plans/first-optional-divergence-census.md new file mode 100644 index 00000000000..8932af75ca0 --- /dev/null +++ b/docs/plans/first-optional-divergence-census.md @@ -0,0 +1,541 @@ +# The `first` interpreter/emitted divergence: census, root cause, and why the repair is two-sided + +## The claim under census + +`dag/std/algebra.dag` declares five methods with `return_type: OptionalOf { inner: ReceiverElement }` +— `first`, `last`, `get`, `lookup`, `map_get`. That row is the single authority for their result +type, and the Rust emit arm realizes it: `extdeps/languages/rust/emit.dag`'s method template row for +`first` is `{recv}.first().cloned()`, an `Option`. + +The interpreter arm did not. `v1_interpreter`'s `method_call.first` computed +`items.front().cloned().unwrap_or(Value::Null)` — the RAW ELEMENT, or `Value::Null` when the +collection was empty. `method_call.last` and `method_call.get` and `method_call.lookup` were the +same shape; only `map_get` already constructed the Optional (through `map_lookup_as_optional`, whose +doc comment states the construction-not-validation rule this census re-derives from the other side). + +Two realizations of one declared signature that disagree are not a low rung on the §4b ladder. They +are DESIGN.md §5 silent wrongness — outside it. + +## What is measured, and by what + +Executed, not reasoned. A four-case probe run through `gunbc run` against `dag` + `src/v2` +source roots, on the seed as it stands on `main`: + +| probe | interpreted | what `dag/std/algebra.dag` declares | | +|---|---|---|---| +| `[] \|> first`, outer/inner match | `OUTER-ABSENT` | `OUTER-ABSENT` | agrees | +| `[Absent] \|> first`, outer/inner match | `OUTER-ABSENT` | `OUTER-PRESENT-INNER-ABSENT` | **diverges** | +| `[Present { value: "x" }] \|> first` | `x` | `x` | agrees (positive control) | +| `(["x"] \|> filter(n => true) \|> first) == Present { value: "x" }` | `false` | `true` | **diverges** | +| `(["x"] \|> filter(n => true) \|> first) == "x"` | `true` | not well-typed | **diverges** | + +Those five rows are now enrolled as executing evidence in +`dag/test/claim/first_optional_construction_witness_test.dag`, which is red against the raw-element +arm and green against the constructed Optional. The pre-existing +`dag/test/claim/branded_list_first_optional_witness_test.dag` is the regression control: it was +green BEFORE the repair and must stay green after. + +## Why the pre-existing witnesses were green on a real divergence + +`branded_list_first_optional_witness` eliminates `first` with +`match { Present { value: v } => .. Absent => .. }` over a NON-optional element type. The interpreter +carried compensating raw-unwrap arms in `match_pattern` — a `Present` pattern against a value that is +neither `Null` nor a `Variant` matches and binds the value itself — precisely so that shape would +agree. So the entire match-scrutinee population was green on a divergence it is structurally unable +to observe. **A witness whose RED is not authorable is a decoration**; for this class the +match-scrutinee shape is exactly that, and the two shapes in the table are the ones that are not. + +## SUPERSEDED: this census's population was keyed on a SPELLING, and missed the larger half + +**Read this before citing anything below it.** The census's declared population is "every terminal +`|> first` occurrence in `dag/**.dag` and `src/v2/**.dag`". That is a *syntax*, not the operation. +The corpus writes the same declared operation two ways, and the pipe form is the smaller: **224** +pipe-form occurrences against **661** `.first()`, **19** `.last()`, **41** `.lookup()` and **7** +`.get()` across 183 files. Everything below measured one spelling of an operation whose identity +`dag/std/algebra.dag` already fixes. + +Every consumer that has actually failed in production is in the half this document never looked at +— `parse_int(s: fields.first())`, `matches.first().shape`, `lines.first() == schema`. + +A re-derivation scoped to the 944-module import closure of `tools.generated_artifact_gate` — the +population that actually gates landing — finds **270 consumer sites**, classified by what consumes +the result: 137 match-eliminated, 96 propagated, **14 compared to a bare value**, 11 declared-fn +arguments, **5 field accesses on the result**, **3 builtin arguments**, **1 method call on the +result**. Twenty-three of those are un-migrated and **known** to block the closure from loading. + +**Twenty-three is a LOWER BOUND, never a population, and it must not be cited as one.** The +classification's largest non-`match` bucket is 31 sites where a one-line textual reader *cannot +decide* whether `algorithm: parts.first(),` is a record-field assignment or a function argument, +because the opening brace is on a previous line — so that bucket names its own undecidability rather +than being guessed into whichever class looked likelier. Record-field assignment into a declared +non-optional field is a real consumer class (`tested_head_sha: lines.skip(n: 4).first()` in +`gunbc.merge_admission_produce`), it is somewhere inside those 31, and it cannot be counted from +source text. Add 22 `let` bindings whose consumers are not followed here. What would settle it is not +a better reader — it is the compiler, which knows every declared type. + +### How this document's numbers went wrong twice, and the rule that covers both + +**A catch-all is only visible once something has fallen out of it, so the first census of anything +should be assumed to have one.** This is stated here because it is the rule a reader needs in order +to weigh every number below it, and because this document is its own two receipts. + +*First layer — the population was a spelling.* The census declared itself over "every terminal +`|> first` occurrence". That is a syntax, not the operation, and the method-call form is the larger +by far. Everything that has actually failed in production was in the half never looked at. + +*Second layer — the residue wore a class name.* The re-derivation that fixed the spelling produced a +tidy table with six named classes and a 96-site bucket called `propagated / returned onward, +declared type honest`. That is not a class; it is what was left after five were named, described in +a way that reassures. It had already eaten a real one — record-field assignment into a declared +non-optional field. + +The correction was not judgement or restraint. Three successive classifiers were written; the first +two both produced the tidy table. The bucket that now names its own undecidability appeared only +after a **specimen** — `tested_head_sha: lines.skip(n: 4).first()` in `gunbc.merge_admission_produce` +— fell out of the catch-all and showed what it was hiding. Without that specimen the tidy table +would have shipped a third time. + +So the operative rules, both earned here rather than reasoned: + +- Go looking for the catch-all before someone else finds it. The tell is a bucket defined by what it + is **not**, or one whose description is a reassurance — *honest*, *unaffected*, *fine*. +- Where the instrument genuinely cannot decide a position, name the bucket after the + **undecidability** rather than the likelier class, and say what *would* decide it. Here that is + the compiler, which knows every declared type; a guessed split would have produced a tidier table + no reader could question. +- Report the surviving count as a **lower bound**, and make the completion criterion a + self-verifying property rather than a number. + +**The completion criterion is therefore not "23 sites fixed" — it is THE CLOSURE LOADS.** That is +self-verifying and needs no population known in advance, and each fix lets the closure load further +so the next refusal names the next site: exhaustive by construction, every step verified, and it +terminates exactly when the property we want is true. A claim that the known set is repaired and a +claim that the migration is complete are two different assertions, and anything reporting on this +work must say which one it is making. + +**The class this document never named is the largest and the worst of them.** Fourteen sites compare +a `first()` result to a bare value with `==` / `!=`. None of the dispositions below covers it, and +comparison is the shape with no pattern for a compensation arm to intercept — which this very +document establishes from the other side, in the probe table above, where the comparison case +diverges. Nine of the fourteen are merge-admission receipt parsing. + +**What stays true:** the divergence, the root cause, the two-sided argument, and the probe table are +all unaffected — they are about the mechanism, not the population. **What must not be cited:** the +disposition counts below, as a population or as a completeness claim. A census that names its shapes +gets cited as complete whether or not it says it is. + +## The census — a disposition roster, not a shape tally + +Population: every terminal `|> first` occurrence in `dag/**.dag` and `src/v2/**.dag` on `main`. +186 occurrences resolve to **181 real sites over 81 files**, plus 5 that are not sites at all +(4 inside `//` annotations, 1 inside a string literal that carries a probe program). The parent lane +measured 187 across 82; that reconciles exactly as 186/81 plus PR #9775's own known-red row, which +is not on `main`. **Cite this census as the producer of the roster; the count is not the +deliverable and should not be transcribed.** + +Each site carries a DISPOSITION — whether the divergence actually harms it — not merely a shape. +A shape says where the value goes; only the disposition says whether the two realizations answer +differently on an input the corpus can reach. + +| disposition | sites | what it means | +|---|---|---| +| `AgreesUnderCompensation` | 142 | eliminated by `match`. The interpreter's raw-unwrap arms in `match_pattern` bind a `Present { value: v }` pattern to any value that is neither `Null` nor a `Present`/`Absent` variant, so interpreter and emitted agree for **every element type except `Optional` itself**. | +| `Propagates` | 36 | returned onward as the enclosing function's declared `T?`. The declared type is honest; only its REPRESENTATION differs, so the disposition is the caller's. | +| `HarmedNow` | 3 | the value reaches a position that reads the representation directly. | +| `NotASite` | 5 | annotation or string-literal text. | + +**`AgreesUnderCompensation` is a measured disposition, not an assumption.** Its failure condition is +an element type that is itself `Optional`, and the corpus declares exactly five list-of-optional +carriers in total (`List` / `List>`), all in witness tests, none of them reaching a +`first`. So **zero** of the 142 are harmed today. That is precisely why this class stayed invisible: +the shape that dominates the corpus is the one shape the compensation covers. + +**`Propagates` resolves the same way, one level out.** Following all 36 functions to their call +sites: 72 callers eliminate by `match` (unharmed), 2 tail-propagate into another `T?` +(`mercurial_first_changeset_cycle` / `_file_revision_cycle`), and 4 compare `== none` +(`rust_representation_realization_for` in `self_host_symbol_identity_binding_witness_test`). **Zero +harmed today** — but the reason is not the one an earlier revision of this document gave, and the +correction matters more than the verdict did. + +That revision said the `== none` sites agree "because a miss is `Null` on one side and `Absent` on +the other and both compare equal to `none`". **That mechanism is wrong.** In the interpreter `none` +EVALUATES TO `Value::Null` — `v1_interpreter`'s variable evaluation returns `Value::Null` for the +symbols `none` and `None` before any binding is consulted. So the raw side compares equal because it +*is* `Null`; a constructed `Optional::Absent` variant does not compare equal to it at all. These +sites therefore agree **before** the construction lands and BREAK after it, and two of them are +among the six assertion failures the floor reports on this branch. The verdict "zero harmed today" +was right about the pre-change state and was reached by the wrong route — and the wrong route is +exactly what hid the `none`-literal migration (Phase D below) from this census's first draft. + +`HarmedNow`, in full — this is the whole victim list for the pipeline spelling: + +- `dag/std/cache_interface.dag` · `cache_facts_for_id` — declares `-> CacheInterfaceFacts` and + returns `catalog |> filter(..) |> first()`, an `Optional`. Its three callers + (`cache_reach_candidate_probe`, `cache_layer_cost_justified`, + `cache_layer_ids_respect_locality`) then read `.locality` and pass it to `read_latency_cost`. + Sibling defect in the same module: `cache_layer_plan_primary` / `cache_layer_plan_fallback` both + declare `-> CacheInterfaceId` over `.first()`. +- `dag/test/claim/build_latency_actions_collect_witness_test.dag` · + `witness_population_fold_groups_by_host_and_filters_job_name`, twice — + `measure_count(m: srv1.durations |> skip(n: 0) |> first)` passes an `Optional` into a required + parameter. The two realizations agree while the list is non-empty and diverge on empty, where the + emitted arm's `.expect(..)` stops and the interpreter carries `Value::Null` onward. + +**Three of 181.** Read alone that number argues the class is not worth repairing. It is the wrong +denominator, and the next section is why. + +## The finding that changes the shape of the repair + +The census does not stop at `|> first`. The METHOD-CALL spelling `.first()` / `.last()` is a +separate and much larger population — 646 occurrences across 180 files in the same two trees by this +census's filter, 655 across 178 by the parent lane's independent one. Same magnitude, different +filter boundary; neither number should be transcribed, and the disagreement is itself the reason to +name the producer rather than the figure. Its +dominant idiom is the value position, not the match: + + parse_int(s: fields.first()) + trim(tokens.skip(n: 1).first()) + percent(scalars.first()) + OpenBmcCollectionOne { value: values.first() } + fn cache_facts_for_id(..) -> CacheInterfaceFacts { catalog |> filter(..) |> first() } + +Every one of those passes an `Optional` into a position declared `T`. They work TODAY in both +realizations, for two different reasons: + +- **emitted**: `05_emit_rust`'s `rust_call_arg_fail_closed_unwrap` sees a `CardOptional` argument + meeting a required parameter and emits `.expect("fail-closed: an optional value flowed into + non-optional parameter N of F (empty Optional at runtime)")`. Typed, located, fail-closed. +- **interpreted**: nothing. There is no optional→required coercion in `v1_interpreter`'s argument + binding. It works only because `first` handed back the raw element in the first place. + +So the raw-element arm is not an isolated defect in one handler. **It is the compensation that the +interpreter's MISSING argument coercion has been leaning on**, corpus-wide. Repairing `first` alone +— making the interpreter construct the Optional its roster row declares — removes the compensation +without supplying what it was compensating for, and hundreds of value-position sites begin handing a +`Present { .. }` variant to `parse_int`, `trim`, `percent` and to record fields. That is a larger +silent wrongness than the one being fixed, in the same direction. + +That is measured, not argued. With only the `first`/`last`/`get`/`lookup` construction in place, +`bmc_capability_solve_witness_test`'s `firmware_wire_version_is_parsed_before_track_matching` — an +ordinary corpus witness that names nothing about optionals — flips from PASS to +`FAIL (runtime error [type-error]: type error: parse_int expects a string argument, got Variant)`, +while the same witness is green on the unmodified seed. It reaches +`parse_int(s: fields.first())` in `extdeps/bmc/capability.dag`. + +**The repair is therefore two-sided, and both sides derive from authorities that already exist:** + +1. `v1_interpreter` constructs the `Optional` for every algebra row that declares `OptionalOf`, + decided by call site rather than by value shape (the `RawMapLookup` rule, applied to the ordered + collections). One authority: the `AlgebraFieldTemplate` rows. +2. `v1_interpreter` gains the optional→required argument coercion the Rust emit arm already has, + decided by the callee's declared parameter cardinality — the same fact + `rust_call_arg_fail_closed_unwrap` reads — and refusing, typed and located, where the emitted arm + `.expect`s. One authority: the callee's parameter cardinality. + +Neither half is landable without the other, and that is executed rather than predicted: the +capability-solve witness above is the discriminating control, red on half the repair and green on +both halves and on neither. Landing (1) alone is the absorbing-fallback shape read +backwards: it converts a silent agreement into a silent disagreement across a population the +change does not name. + +## What blocks the second half, and why this lane stopped rather than improvised + +Side (2) is implemented in this branch for `.dag`-declared callees: `call_function_inner` binds an +argument, reads the callee parameter's declared type node, and — where that parameter is a required +value parameter — unwraps `Present` and REFUSES on `Absent`, typed and located, exactly where the +emitted arm `.expect`s. Measured: the new witness is 7/7 green, and +`branded_list_first_optional_witness` (the regression population) stays 8/8 green. + +It does not close the class, and the reason is a missing authority rather than a missing edit. +`parse_int(s: fields.first())` never reaches `call_function_inner`: `parse_int` is a BUILTIN, and +`04_method`'s `builtin_function_registry` maps a builtin name to a RETURN TYPE only — 04_sigs says +so in as many words. There is no declared parameter cardinality for a builtin anywhere the +interpreter (or anything else) can read, so the coercion cannot be DERIVED for a builtin call. The +capability-solve witness above stays red for that reason and no other. + +Deciding it by the argument's value shape instead — "if it looks like an `Optional`, unwrap it" — +is available and is the wrong answer twice: it is validation standing where construction was +available (§5), and it is precisely the value-shape inference `map_lookup_as_optional`'s own doc +comment refuses, because a stored `V = Optional` payload is then indistinguishable from a wrapped +result. So this lane stops here rather than shipping it. + +**The grounding this class is waiting on**: builtin PARAMETER signatures, modelled beside the +return type the registry already carries, so that argument cardinality is a fact the substrate +holds rather than a fact only the Rust emitter's static types happen to know. That is +model-before-implement work in `std/` ahead of any further pipeline edit, and it is a routing +decision, not something to improvise inside this repair. + +## Step 1 re-scoped: the signature carrier already exists, and the gap is its denominator + +The routing decision on this lane was to model builtin parameter signatures in `std/` first. Reading +`std/` before authoring turned that into a different task, and the difference is worth recording +because it is the second time on this class that the obvious repair was the wrong one. + +**`dag/std/primitive_identity.dag` already models it, and already executes.** It carries +`PrimitiveSignatureGrounding`, `PrimitiveSemanticContract`, `PrimitiveSignatureResolution` (whose +`SignatureResolved` arm is `{ parameters: List, result: AlgebraTypeTemplate }`), +`primitive_signature`, and `primitive_arity`, green by execution in +`dag/test/claim/primitive_signature_grounding_witness_test.dag`. Its own doc comment refuses the fork +this lane was about to commit, in as many words: *the contract carries a KEY into the one authority, +never its contents.* It even keys the lookup on `(canonical_name, profile)` rather than name alone, +precisely because `get` is `[ReceiverSelf, NamedTemplate { name: "Int" }]` on the List profile and +`[ReceiverSelf, ReceiverKey]` on the Map-shaped ones. + +So there is no new carrier to mint, and authoring one would have been exactly the §3 nickname. +**What is missing is coverage, and it is measurable**: of `builtin_function_registry`'s 131 names, +20 have an `AlgebraFieldTemplate` row and resolve through `primitive_signature`; the other 111 +answer `SignatureNotGrounded`. `parse_int` — the name that reds the corpus control — is one of the +111. + +**The 111 are two populations, and nothing in the substrate separates them.** Some are language +primitives that should carry a signature (`parse_int`, `char_at`, `code_point`, `chars_to_string`, +`string_length`, `string_contains`, `scan_while`, `scan_to_eol`, `set_insert`, `set_union`, +`sorted_map_keys`, `hash_combine`). Most are host or lens transports whose parameter shape is a +Realization fact and not a language one (`doc_graph_orphan_count`, `fallback_arm_census_facts`, +`emit_host_run_transport`, `non_fold_residue_count`, `witness_layer_roots_compile_clean_check`) — +§3 puts those with their transport, not in the language's primitive surface. + +The obvious discriminator does not discriminate. `gunbc.v1_interpreter_primitive_surface` enumerates +an arm for BOTH populations by construction, so joining on it classifies `doc_graph_orphan_count` +and `parse_int` identically — measured, not assumed. Splitting them on a naming convention instead +would be the smuggled heuristic §5 names, so this lane does not. + +**The step-1 modeling question is therefore not "what shape does a builtin signature have" — that is +answered — but "what closes the language-primitive population", i.e. the denominator over which a +signature is obligatory.** That is a routing decision, and this lane has raised it rather than +picking one. + +## The registry and the algebra rows already disagree + +Independent of the `first` class, and worth its own row wherever primitive-surface debt is tracked: +the 20 overlapping names are two authorities for one operation's type, and they do not agree today. +`builtin_function_registry` is receiver-BLIND, so it collapses distinctions the algebra rows carry: + +- `reverse` — registry `List`; algebra `ReceiverSelf` on both a scalar and a + collection profile. On a `String` receiver the two answer with different types. +- `map_keys` and `map_values` — registry gives both `List`, one type variable + for two different element positions; algebra gives `ContainerOf { .., element: ReceiverKey }` and + `.. ReceiverValue`. For any `Map` with `K /= V` the registry cannot be right about both. +- `concat` — registry `String`; algebra `ReceiverSelf`, so a list concat types as a String. +- `get` — registry one `Optional`; algebra distinguishes the List reading from + the Map reading. + +Every one of these is the same §3 fork as the `first` divergence, one layer up: not two +realizations of one declaration, but two declarations of one operation. + +## Measured blast radius, and the class already has an authored program + +**The floor, enumerated from the artifact rather than the log.** The required-witnesses-floor run on +this branch reports `planned=3141 passed=2630 known_red_held=15 failed=442`. The job log prints only +six per-claim failure lines, which reads as a truncated log and is not: the +`required-floor-disposition` artifact separates the outcomes the summary's `failed` folds together. + +| outcome | count | +|---|---| +| `runtime-errored-before-verdict` | 442 | +| `failed` (assertion) | 6 | +| `budget-refused-before-verdict` | 1 | +| `route-gap-before-verdict` | 47 | +| `known-red-held` | 15 | + +So the 442 **errored before reaching a verdict**; they did not assert and fail. All 442 are +`v2.test.*` — 157 `v2.test.claim`, 132 `v2.test.manual`, 71 `v2.test.emit`, 52 `v2.test.execution` +— and **none** is a `dag/test/claim` witness. That is the self-host coupling: the v2 compiler is +`.dag` interpreted by the v1 seed, so changing the interpreter's projections changes v2's own +behaviour as it runs. The blast radius is the interpreted v2 compiler, not the corpus witnesses. + +**A note on how this document's first draft got its number wrong.** It reported the partial repair +as flipping one witness, `bmc_capability_solve firmware_wire_version_is_parsed_before_track_matching`. +That claim's disposition is `declined_outside_gate_closure` / `not_executed` — the floor does not run +it. The sample was not merely small; it was drawn from outside the population the floor measures. + +**Re-measured post-merge, against a trunk control.** At `79ac1aa` (run 33357314877) the artifact +reports 426 `runtime-errored-before-verdict`, 6 `failed`, 15 `known-red-held`, 2619 `passed`. The +same artifact on main at `b41d5648` (run 33356292996) reports **0 errored, 0 failed, 3065 passed**. +The control is what makes the attribution a measurement: the whole population is caused by this +branch and none of it is inherited. It also refuted an attribution this document would otherwise +have carried — two of the six failures name `self_host_symbol_identity_binding_witness`, which is +#9741 territory merged in from main the same hour, and the clean trunk says they are this branch's. +A recently-merged neighbour is the most available explanation and therefore the one to control for. + +**The floor refuses through `non_verdict_unenrolled`, not through `known_red_now_passing`.** Five of +main's 20 known-reds error under this branch instead of returning their known-red verdict. They do +not appear in `known_red_now_passing`, which stays 0; they appear as +`verdict_incomplete=5 non_verdict_unenrolled=5` in the floor's terminal line, and that is what turns +the lane red. The wall is `v2.workflow.floor_non_verdict`, whose header already names this class and +whose roster is `Empty{}` so any enrolled known-red that starts throwing refuses as unrostered debt. +Recorded because the reading error is available and this lane made it: `known_red_now_passing` alone +does not distinguish a still-discriminating known-red from one that has stopped reaching its +assertion, so it is the wrong field to cite for that property — a citation defect, not a safety gap, +because the adjacent counter gates. + +**The build lane's real cause, and a correction to this document's first account of it.** After +refreshing onto main at `a6d6c68d4d1`, `required-witnesses-build` fails where it passed at +`abee235`. This document first recorded the cause as `NoSuchField { type_name: "Optional", field: +"shape" }` at `extdeps.bmc.types` line 183 (`matches.first().shape`), reproduced by running +`run_generated_artifact_drift_gate_body` locally, and explicitly ruled OUT stale artifacts. **That +was wrong, and the ruled-out hypothesis was half the answer.** The CI log reports: + + generated-artifact rostered=35 adjudicated=32 matches=30 drifted=2 absent=0 unadjudicated=3 + drifted DESIGN.md + drifted docs/design-ledgers.md + UNADJUDICATED .github/workflows/{witnesses,fleet-converge,fleet-desired}.yml + — CallContractMismatch { callee: "outcome_accepted", detail: "an optional value flowed + into non-optional parameter 1 ('value') (empty Optional at runtime)" } + +Two classes, both this branch's: + +- **3 unadjudicated** — this branch's own argument-coercion arm, the same refusal `main_wet` gives. + Those artifacts cannot be generated at all, so the gate reaches no verdict on them. +- **2 drifted** — `DESIGN.md` and `docs/design-ledgers.md`, the deliberate unregenerated projections + recorded below. + +**Why the local reproduction pointed elsewhere.** The local entry evaluates the gate body as one +expression and dies at the first refusal it meets, which is the `bmc.types` field read; CI's build +lane adjudicates PER ARTIFACT PATH and so records a per-path outcome for all 35. Same subject, two +routes, different first failures — and reproducing *a* failure locally is not the same as +reproducing *the* failure. The `NoSuchField` site is real and remains an in-class value-position +victim; it is simply not why the lane is red. + +**What changed to make this blocking: main #9814, "Restore generated-artifact drift to required CI".** +The generated-artifact drift check was a declared rung drop and is now a required check again. So the +drift recorded below stopped being latent debt that dissolves with the repair and became an active +blocker. That does not change the refusal to fabricate the bytes from a stock-interpreter seed — a +green gate over a live divergence is worse than a red one — but it does mean this branch cannot show +a green build lane until the repair completes, for a second independent reason. + +**A measured victim outside the floor: `main_wet`.** The generated-artifact actuator +`tools.generated_artifact_gate main_wet` refuses under this branch's interpreter with +`CallContractMismatch { callee: "outcome_accepted", detail: "an optional value flowed into +non-optional parameter 1 ('value') (empty Optional at runtime)" }` — this branch's own coercion arm, +firing. Evidence about scope rather than an incident: the affected population is wider than the +floor's witness set and reaches the wet actuators. Consequence for this branch: the `DESIGN.md` and +`docs/design-ledgers.md` projections cannot regenerate here, so they sit inconsistent with their +`.dag` authority. That drift is **deliberately left**. It could be cleared by building the seed from +main's Rust and running it over this tree, and that is precisely what must not happen: those bytes +are what the *stock* interpreter computes, while the drift gate here executes *this* interpreter, so +committing them would green the gate across a live divergence — fail-open wearing a green check. The +drift needs no dissolution trigger of its own; it ends when the repair completes. + +**The class is Phase B of an already-open lane.** `gunbc.plans.value_null_split` (lane +keen-ferret-250) models this whole class: `Value::Null` overloads four meanings — the `none`/`None` +literal, `Optional::Absent`, `Witness::Violates` on map miss, and untyped lookup miss — and it lays +out a phase order: + +| phase | content | state | +|---|---|---| +| A | discriminating witnesses pinning the carriers | landed | +| B | stop PRODUCING `Null` where the return type is `Optional` | **what the repair on this branch is** | +| C | delete the `match_pattern` `Null` bridges | the compensating arms this branch leaves in place | +| D | type-directed `none` → `optional_absent`; migrate ~218 `== None` sites over 66 files | not started — the third gate | +| E | cross-representation equality; remove the straddle row | not started | + +**The Phase-A witness predicted this branch's failure by name, in writing.** +`v2.test.manual.value_null_split_witness` carries the comment: *"`raw_get_miss_differs_from_optional_absent` +stays GREEN while raw get miss is untyped and `optional_absent()` is `Optional::Absent`; it flips +RED in Phase B when get+Optional routes through `map_lookup_as_optional`."* It is one of the six +assertion failures. That is not a defect in the repair — it is the enrolled signal that Phase B +landed, and updating its disposition is part of Phase B. + +`value_null_split` §0 also pre-refutes the fix this census would otherwise have reached for: a +blanket cross-representation equality guard **cannot** close the straddle, because `present == None +→ false` is legitimate at those ~218 sites. The remedy is splitting the carriers, not grounding them +onto one sentinel. + +**So the completion has three gates, not one**: the optional-into-required argument coercion (needs +a closed language-primitive denominator → [partition census](builtin-registry-population-partition.md)), +Phase D's `none`-literal migration, and Phase C's bridge deletion. None is optional and none is +this branch's alone. + +## The scheduling hold is not the dissolution trigger + +These are two different objects and this document keeps them apart, because conflating them is how +a trigger rots. + +**The hold is procedural and belongs to this moment.** PR #9775 enrols this divergence as a +known-red with an expected-red roster row, and the floor counts `known_red_now_passing` as its own +outcome, so repairing the primitive while that row still stands breaks BT-0's floor. That is an +ordering constraint on when a repair may land. It is a note to the authors involved, not a claim +about the defect. + +**The trigger is semantic and belongs to any future reader**: *when the interpreted and emitted +realizations of `first` agree on the optional result shape*. A trigger phrased "after PR #9775" +would name a merge event, and merge events rot — a PR is renumbered, superseded, split, or lands +with the row removed, at which point the trigger is either unsatisfiable or vacuously satisfied +while nothing about the defect has changed. Nothing in this document, in +`gunbc.recurring_failure_mode`, or on the witness carries a PR number as a trigger; the one PR +number below is a population reconciliation, not a condition. + +**The transition, in order, when the repair lands** — this is §4b(4) dissolution-on-climb, and the +middle pair is the whole rule: + +1. repair the interpreter's `first` semantics; +2. REMOVE the discriminator from the expected-red roster — the production disposition goes; +3. RETAIN the discriminator as ordinary passing evidence — the evidence stays, and becomes the + permanent regression control proving the two arms still agree; +4. observe `known_red_now_passing = 0`. + +Step 4 is not a formality. That channel exists precisely to catch someone repairing the primitive +and leaving a stale expected-red disposition behind, so a nonzero value there is a defect in the +repairing transaction, never noise. + +## Rung, ceiling, trigger + +- **Class**: `first_optional_representation_divergence` — a collection projection declared + `Optional` realized as a raw element in one arm and as `Option` in the other. +- **Rung found at**: below the ladder (silent wrongness). Both arms typecheck; neither warns. +- **Rung after part (1) + (2)**: mechanically preventable. The interpreter refuses when an algebra + arm's result does not inhabit the optionality its roster row declares, and refuses when an absent + optional reaches a required position. The invalid state stays writable — a hand-written arm in the + seed can still compute the wrong thing — so this is rung 2, not 3. +- **Attainable ceiling**: structurally impossible (rung 4), reached when the arm BODIES stop being + hand-written Rust in the seed and are projected from the same rows the emit arm reads. That is the + §7 self-host frontier for `v1_interpreter`, not a local edit. +- **Next-rung trigger**: the capability that lets an interpreter primitive's body be derived from + its `AlgebraFieldTemplate` row rather than authored beside it — the same `v1_interpreter` pure-eval + dissolution named on the `method_call.map_keys` arm. Not an artifact; the capability. + +## Roster + +`HarmedNow` and `NotASite` are listed in full above. `Propagates` (36 sites) is rostered here at +identity grain; `AgreesUnderCompensation` (142) is the complement and its membership test is +mechanical — the occurrence is a `match` scrutinee, directly or through a `let` bound one line up. + +### Propagates — returned onward as the enclosing function's `T?` + +- `dag/extdeps/filesystem/linux.dag` · `linux_proc_mount_row_for_target` +- `dag/extdeps/git/object_store.dag` · `git_find_stored_object` +- `dag/extdeps/git/object_store.dag` · `git_find_unavailable` +- `dag/extdeps/languages/rust/emit.dag` · `rust_pair_completion_spelling_for` +- `dag/extdeps/languages/rust/representation.dag` · `rust_representation_realization_for` +- `dag/extdeps/llm/codex_auth.dag` · `codex_default_organization` +- `dag/extdeps/mercurial.dag` · `mercurial_first_cycle_node` +- `dag/extdeps/pijul.dag` · `pijul_delivery_dependency_issue` +- `dag/extdeps/pijul.dag` · `pijul_delivery_unavailable_issue` +- `dag/extdeps/pijul.dag` · `pijul_find_channel` +- `dag/extdeps/pijul.dag` · `pijul_missing_channel_member_issue` +- `dag/extdeps/pijul.dag` · `pijul_missing_conflict_change_issue` +- `dag/extdeps/pijul.dag` · `pijul_missing_context_issue` +- `dag/extdeps/pijul.dag` · `pijul_missing_dependency_issue` +- `dag/extdeps/pijul.dag` · `pijul_missing_tree_change_issue` +- `dag/extdeps/pijul.dag` · `pijul_present_change_declared_missing` +- `dag/extdeps/pijul.dag` · `pijul_present_path_declared_missing` +- `dag/extdeps/pijul.dag` · `pijul_present_vertex_declared_missing` +- `dag/extdeps/pijul.dag` · `pijul_self_dependency` +- `dag/extdeps/pijul.dag` · `pijul_state_identity_issue` +- `dag/gunbc/design/interaction.dag` · `detent_named` +- `dag/gunbc/design/material.dag` · `carrier_named` +- `dag/gunbc/design/state_response.dag` · `rest_member` +- `dag/gunbc/host/host_standup.dag` · `assimilation_obligation_for_input` +- `dag/gunbc/instruments/e0599_emitter_decision_census.dag` · `e0599_row_for_operation` +- `dag/gunbc/live_deploy/repository_convergence.dag` · `convergence_ref_at` +- `dag/gunbc/live_deploy/repository_convergence.dag` · `convergence_worktree_at` +- `dag/gunbc/roadmap/roadmap_belt_actuate.dag` · `belt_dispatch_result_for_label` +- `dag/gunbc/roadmap/roadmap_closing_contract_authoring.dag` · `closing_contract_target_node` +- `dag/gunbc/roadmap/roadmap_execution_contract.dag` · `dispatch_host_realization` +- `dag/gunbc/roadmap/roadmap_style.dag` · `swatch_named` +- `dag/gunbc/roadmap/roadmap_validation_oracle.dag` · `validation_oracle_first_incomplete` +- `dag/std/target_representation.dag` · `checkpoint_row_migration_for` +- `dag/std/target_representation.dag` · `representation_spelling_for` +- `dag/test/claim/algebra_carrier_roster_witness_test.dag` · `ascii_least` +- `dag/test/claim/roadmap/roadmap_program_view_witness_test.dag` · `fx_line_view` diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index cbf25b4ab2c..891d479ba2b 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -784,6 +784,160 @@ fn optional_absent(ctx: &InterpContext) -> Value { } } +/// Whether a value already carries the `Optional` contract, i.e. is one of the two constructors +/// `optional_present`/`optional_absent` build. Used only to REFUSE a disagreeing arm — never to +/// decide whether to wrap, which is a call-site fact (see `RawMapLookup`). +fn is_optional_value(v: &Value, ctx: &InterpContext) -> bool { + match v { + Value::Variant { + type_name, + variant_name, + .. + } => { + *type_name == ctx.sym("Optional") + && (*variant_name == ctx.sym("Present") || *variant_name == ctx.sym("Absent")) + } + _ => false, + } +} + +/// ONE AUTHORITY FOR `Optional`-VALUEDNESS: the `AlgebraFieldTemplate` rows projected from +/// `dag/std/algebra.dag`. `first`/`last`/`get`/`lookup`/`map_get` each declare +/// `return_type: OptionalOf { inner: ReceiverElement }` there, and that row is what makes the Rust +/// emit arm produce `Option`. Before this function existed the interpreter arms answered the +/// same question by hand and answered it differently — `first` returned the RAW element (or +/// `Value::Null`), so `xs |> first == Present { value: x }` was false interpreted and true emitted: +/// DESIGN.md §5 silent wrongness, which is outside the ladder rather than low on it. Both arms now +/// read this row, so a single definition cannot disagree with itself. +/// +/// `None` = the roster has no row for this spelling (not an algebra method, or a free-call-only +/// builtin); `Some(false)` = declared non-optional. A spelling whose rows DISAGREE is refused by +/// the caller rather than resolved by majority — a mixed roster is a modelling defect, not an input. +fn algebra_row_returns_optional(method: &str) -> Option> { + let mut optional = false; + let mut plain = false; + for t in crate::std_algebra::all_algebra_field_templates().iter() { + if t.name != method { + continue; + } + if matches!( + *t.return_type, + crate::std_algebra::AlgebraTypeTemplate::OptionalOf { .. } + ) { + optional = true; + } else { + plain = true; + } + } + match (optional, plain) { + (false, false) => None, + (true, true) => Some(Err(())), + (o, _) => Some(Ok(o)), + } +} + +/// What an argument value is, with respect to the `Optional` contract. +enum OptionalArg { + NotOptional(Value), + Present(Value), + Absent, +} + +fn classify_optional_arg(val: Value, ctx: &InterpContext) -> OptionalArg { + match &val { + Value::Variant { + type_name, + variant_name, + fields, + } if *type_name == ctx.sym("Optional") => { + if *variant_name == ctx.sym("Present") { + OptionalArg::Present( + fields_get(fields, ctx.sym("value")) + .cloned() + .unwrap_or(Value::Null), + ) + } else if *variant_name == ctx.sym("Absent") { + OptionalArg::Absent + } else { + OptionalArg::NotOptional(val) + } + } + _ => OptionalArg::NotOptional(val), + } +} + +/// Whether a declared parameter is a VALUE parameter whose type is required (not `T?`, and not an +/// `Optional` carrier spelled without the cardinality flag). The two spellings name one carrier, +/// so the predicate asks both — the same pairing `05_emit_rust`'s +/// `rust_call_arg_fail_closed_unwrap` makes, and for the same reason: unwrapping into +/// `witness_from_optional(opt: Optional)` would strip the very value the callee exists to +/// inspect. +/// +/// A FREE TYPE VARIABLE DECLARES NOTHING ABOUT CARDINALITY, so it is not a required formal. For +/// `fn outcome_accepted(value: T)`, `T` instantiating to `Optional` is a legitimate +/// instantiation and not a cardinality escape; treating it as required both unwrapped `Present` +/// into the callee (a SILENT corruption of the very kind this repair exists to remove — the callee +/// declared `Outcome>` and would have received `Outcome`) and refused `Absent` +/// outright. That is the already-rostered `mitigation_injected_where_judgment_declined` shape, and +/// this predicate is the producer its row names as the trigger: it distinguishes a free type +/// variable from a declared non-optional formal, reading the fn's own declared type-parameter list +/// rather than guessing from the spelling of a name. +fn param_declares_required_value( + param: &Rc, + pname: &str, + type_param_names: &[String], + ctx: &InterpContext, +) -> bool { + match param.children.first() { + Some(type_expr) => { + let type_name = authored_name_at(ctx.si(), type_expr.clone()); + type_name != pname + && type_expr.return_cardinality != Cardinality::CardOptional + && type_name != "Optional" + && !type_param_names.iter().any(|t| t == &type_name) + } + None => false, + } +} + +/// The wall that keeps the two realizations from drifting apart again: whatever an algebra arm +/// computes, the value it hands back must inhabit the return type its roster row declares. An arm +/// that reverts to the raw element refuses here, loudly and located by method name, instead of +/// silently producing a value the emitted mirror would never produce. +fn algebra_result_matches_declared_optionality( + method: &str, + value: Value, + ctx: &InterpContext, +) -> InterpResult { + match algebra_row_returns_optional(method) { + None => Ok(value), + Some(Err(())) => Err(InterpError::TypeError { + msg: format!( + "algebra roster disagrees with itself about `{}`: some rows declare \ + `OptionalOf` and some do not, so the interpreter cannot derive the method's \ + optionality from dag/std/algebra.dag", + method + ), + }), + Some(Ok(false)) => Ok(value), + Some(Ok(true)) => { + if is_optional_value(&value, ctx) { + Ok(value) + } else { + Err(InterpError::TypeError { + msg: format!( + "interpreter arm for `{}` produced {} where dag/std/algebra.dag declares \ + `Optional<..>`; the emitted realization returns an Optional here, so \ + returning the bare value would be a silent semantic divergence", + method, + value.type_label() + ), + }) + } + } + } +} + /// Whether a `raw_map_lookup` result already carries the `Optional` contract (a /// `.dag`-authored `Map.lookup` closure returns `Optional` by construction) or is a bare /// storage read still needing the wrap (native `Value::Map`/field storage, miss = `Value::Null`). @@ -3747,7 +3901,8 @@ pub struct InterpContext { // key for the ctx's lifetime (as PureCallMemo.keepalive_fns / EvalRecomputeTrace.keepalive_fns // / EvalCallMemo.keepalive_fns), and the cache dies with the ctx (as data_cache). // Value = (filtered named-param list, all-param list), matching call_function's two uses. - param_name_cache: std::cell::RefCell, Vec)>>>, + param_name_cache: + std::cell::RefCell, Vec, Vec)>>>, param_name_cache_keepalive: std::cell::RefCell>>, // Same chokepoint, ExprVar arm: eval_var rebuilt the name String from its span // (expr_var_name_at) and re-interned it (ctx.sym) per read. The interned Symbol is memoized @@ -4661,7 +4816,22 @@ fn call_function_inner( }) .map(|(i, _)| all[i].clone()) .collect(); - let c = Rc::new((filtered, all)); + // A `fn f(v: T)` node carries `params = concat(type_params, value_params)` + // (`v1.compiler.parse` `parse_fn_body_from_prefix`), and a TYPE parameter is exactly + // the entry whose declared type is its own name -- the same shape `filtered` uses to + // drop them from the positional list. Naming that set is what lets the coercion below + // tell a declared non-optional formal from a FREE type variable. + let type_params: Vec = fn_node + .params + .iter() + .enumerate() + .filter(|(i, p)| match p.children.first() { + Some(type_expr) => authored_name_at(ctx.si(), type_expr.clone()) == all[*i], + None => true, + }) + .map(|(i, _)| all[i].clone()) + .collect(); + let c = Rc::new((filtered, all, type_params)); ctx.param_name_cache_keepalive .borrow_mut() .push(fn_node.clone()); @@ -4671,6 +4841,7 @@ fn call_function_inner( }; let param_names: &Vec = &cached_params.0; let all_param_names: &Vec = &cached_params.1; + let type_param_names: &Vec = &cached_params.2; let mut bindings = HashMap::new(); if !args.is_empty() { @@ -4764,6 +4935,43 @@ fn call_function_inner( } } + // OPTIONAL INTO A REQUIRED PARAMETER — the interpreted half of a rule the emitted half already + // had. `05_emit_rust`'s `rust_call_arg_fail_closed_unwrap` sees an `Optional` argument meet a + // parameter declared `T` and emits + // `.expect("fail-closed: an optional value flowed into non-optional parameter N of F ..")`. + // The interpreter had NO such coercion, and did not need one only because `first`/`last`/`get` + // handed back the RAW element instead of the `Optional` their `dag/std/algebra.dag` rows + // declare. Constructing that Optional without supplying this is the same silent wrongness + // pointed the other way: `parse_int(s: fields.first())` would receive a `Present { .. }` + // variant. Present unwraps; ABSENT STOPS THE LINE, typed and located, where the emitted arm + // panics. + for (i, param) in fn_node.params.iter().enumerate() { + let pname = &all_param_names[i]; + if !param_declares_required_value(param, pname, type_param_names, ctx) { + continue; + } + let key = ctx.sym(pname); + let Some(val) = bindings.get(&key).cloned() else { + continue; + }; + match classify_optional_arg(val, ctx) { + OptionalArg::NotOptional(_) => {} + OptionalArg::Present(inner) => { + bindings.insert(key, inner); + } + OptionalArg::Absent => { + return Err(InterpError::CallContractMismatch { + callee: fn_node.name.clone(), + detail: format!( + "an optional value flowed into non-optional parameter {} ('{}') \ + (empty Optional at runtime)", + i, pname + ), + }) + } + } + } + let caller_label_matches_param = |param_name: &str, arg_label: &str| { param_name == arg_label || param_name == "_" @@ -5471,6 +5679,9 @@ fn eval_binop(op: &BinOp, left: Value, right: Value, ctx: &InterpContext) -> Int if let Some(detail) = cross_family_content_hash_straddle(&left, &right) { return Err(InterpError::CrossRepresentationEquality { detail }); } + if let Some(detail) = optional_against_bare_straddle(&left, &right, ctx) { + return Err(InterpError::CrossRepresentationEquality { detail }); + } } let result = if matches!(op, BinOp::Eq) { equal @@ -5512,6 +5723,56 @@ fn eval_binop(op: &BinOp, left: Value, right: Value, ctx: &InterpContext) -> Int } } +/// An `Optional` meeting a bare `T` under `==` / `!=`. +/// +/// `Value::eq` cannot decide these — a `Present { value: "x" }` is simply not equal to `"x"` — so +/// the comparison SILENTLY ANSWERS FALSE, which DESIGN §5 forbids outright: a failure arm must +/// refuse, never fabricate a plausible answer. It became reachable when `first`/`last`/`get` +/// started constructing the `Optional` their `dag/std/algebra.dag` rows declare, because every +/// consumer written against the old raw-element answer now compares across representations. +/// Measured before this wall: `["schema-v2", "body"].first() == "schema-v2"` returned `false`, and +/// nine such sites are merge-admission receipt schema checks, where a quiet `false` rejects a valid +/// receipt with no diagnostic. +/// +/// ONE SHAPE IS NOT A STRADDLE: Optional against Optional is an ordinary comparison of one +/// representation with itself. +/// +/// THE `x == none` IDIOM IS A STRADDLE AND REFUSING IT IS THE POINT, which is the opposite of what +/// this function first did. `none` evaluates to the host `Value::Null` carrier, so the carve-out +/// that spared it looked like protecting a working test. It was measured, and it was not working: +/// `[].first() == none` answered FALSE, because a constructed `Absent` variant is not `Value::Null`. +/// Sparing it preserved a silent false — the very class this wall exists to stop — so the spare is +/// deleted and the two-carrier case refuses with its own sentence. +/// +/// It stays NARROW by construction rather than by exception. A declared `T?` field whose absent +/// state IS `Value::Null` still compares `Null == Null` and never reaches here; only a CONSTRUCTED +/// `Optional` meeting the Null carrier fires, which is exactly the un-migrated population. +fn optional_against_bare_straddle(a: &Value, b: &Value, ctx: &InterpContext) -> Option { + let (a_opt, b_opt) = (is_optional_value(a, ctx), is_optional_value(b, ctx)); + if a_opt == b_opt { + return None; + } + if matches!(a, Value::Null) || matches!(b, Value::Null) { + return Some(format!( + "{} vs {} — a constructed `Absent`/`Present` and the host Null carrier are two \ + representations of ABSENCE, so `==` would silently fabricate `false` (DESIGN §5): \ + measured, `[].first() == none` answered false. Eliminate the `Optional` with `match` \ + (`Present {{ value: v }}` / `Absent`) instead of testing it against `none`.", + describe_repr(a), + describe_repr(b), + )); + } + Some(format!( + "{} vs {} — an `Optional` and a bare `T` are two representations of one value, \ + so `==` would silently fabricate `false` (DESIGN §5). `dag/std/algebra.dag` declares \ + `first`/`last`/`get`/`lookup`/`map_get` as returning `Optional<..>`; eliminate it with \ + `match` (`Present {{ value: v }}` / `Absent`) and compare `v`, or compare against an \ + `Optional` on both sides.", + describe_repr(a), + describe_repr(b), + )) +} + fn cross_representation_numeric_straddle(a: &Value, b: &Value) -> Option { match (a, b) { (Value::Int(_) | Value::Float(_), v @ Value::Variant { .. }) @@ -6887,7 +7148,22 @@ fn eval_call(node: &Rc, env: &Rc, ctx: &InterpContext) -> InterpResul v1_native_intercept_arms!(v1_native_intercept_dispatch, func_name, args, env, ctx); - if let Some(result) = eval_builtin(&func_name, &args, ctx)? { + // A BUILTIN'S REFUSAL MUST SAY WHERE IT IS. `eval_builtin` receives a name and values and + // has no span, so an argument-shape refusal read `parse_int expects a string argument, got + // Variant` with no file and no line — typed but UNLOCATED, which DESIGN §5 does not admit: + // every path fails with a typed, LOCATED diagnostic. It became load-bearing when + // constructing the `Optional` for `first`/`last`/`get` started routing Optionals into + // builtins, whose registry declares a return type and no parameter list, so no coercion can + // be derived for them and the refusal is the only signal a reader gets. The call node is in + // scope here and carries the span, so the location is attached at the one seam that knows + // it. NARROW BY CONSTRUCTION: this locates refusals raised by builtin dispatch only, and + // the general interpreter-wide locator is a separate class with its own trigger. + if let Some(result) = eval_builtin(&func_name, &args, ctx).map_err(|e| match e { + InterpError::TypeError { msg } => InterpError::TypeError { + msg: format!("{}:{}: {}", node.span.file, node.span.start, msg), + }, + other => other, + })? { return Ok(result); } } @@ -8053,8 +8329,38 @@ fn eval_field_access( Ok(items) => Ok(items.get(1).cloned().unwrap_or(Value::Null)), Err(_) => extract_field(&base_val, &field_name, env, ctx), }, + // `opt.value` is `FieldAccessStyle::OptionalUnwrap`, decided once in 04_lookup's + // `field_summary_for_type`. The emitted mirror realizes that row as `.unwrap()`, so the + // absent case must STOP in both realizations; returning `Value::Null` here let an absent + // optional flow on as a plausible value with no diagnostic (DESIGN.md §5). The + // `Present { value: .. }` arm is what keeps the 176 emitted unwrap sites reading the + // payload now that `first`/`last`/`get`/`lookup` construct a real Optional. Some(FieldAccessStyle::OptionalUnwrap) => match &base_val { - Value::Null => Ok(Value::Null), + Value::Variant { + type_name, + variant_name, + fields, + } if *type_name == ctx.sym("Optional") && *variant_name == ctx.sym("Present") => { + Ok(fields_get(fields, ctx.sym("value")) + .cloned() + .unwrap_or(Value::Null)) + } + Value::Variant { + type_name, + variant_name, + .. + } if *type_name == ctx.sym("Optional") && *variant_name == ctx.sym("Absent") => { + Err(InterpError::TypeError { + msg: "`.value` projected an absent Optional; there is no value to read \ + (the emitted realization panics on the same read)" + .to_string(), + }) + } + Value::Null => Err(InterpError::TypeError { + msg: "`.value` projected an absent Optional carried in the raw value-or-Null \ + representation; there is no value to read" + .to_string(), + }), _ => Ok(base_val), }, Some(FieldAccessStyle::EnumAccessor) => extract_field(&base_val, &field_name, env, ctx), @@ -8739,7 +9045,8 @@ macro_rules! v1_algebra_method_arms { let key = $args.first().ok_or_else(|| InterpError::TypeError { msg: "lookup requires a key argument".to_string(), })?; - raw_map_lookup(&$receiver, key, $env, $ctx).map(RawMapLookup::into_raw) + let raw = raw_map_lookup(&$receiver, key, $env, $ctx)?; + Ok(map_lookup_as_optional(raw, $ctx)) }, arm "method_call.map" { "map" } => list_method_with_closure("map", $receiver, $args, $env, $ctx, |items, f, $env, $ctx| { @@ -8959,14 +9266,25 @@ macro_rules! v1_algebra_method_arms { }, }, + // `first`/`last` are declared `OptionalOf { inner: ReceiverElement }` in + // dag/std/algebra.dag. The Optional is CONSTRUCTED here, decided by the call site + // (empty vs non-empty), never inferred from the element's shape — a stored + // `Element = Optional` head must come back as `Present { value: Absent }`, which is + // exactly the case the old raw `unwrap_or(Value::Null)` collapsed into `Absent`. arm "method_call.first" { "first" } => { let items = expect_list(&$receiver, "first")?; - Ok(items.front().cloned().unwrap_or(Value::Null)) + Ok(match items.front().cloned() { + Some(v) => optional_present(v, $ctx), + None => optional_absent($ctx), + }) }, arm "method_call.last" { "last" } => { let items = expect_list(&$receiver, "last")?; - Ok(items.last().cloned().unwrap_or(Value::Null)) + Ok(match items.last().cloned() { + Some(v) => optional_present(v, $ctx), + None => optional_absent($ctx), + }) }, arm "method_call.reverse" { "reverse" } => { @@ -9057,20 +9375,21 @@ macro_rules! v1_algebra_method_arms { Ok(map_lookup_as_optional(raw, $ctx)) }, + // Same roster row as `first`/`last` (`get: OptionalOf { inner: ReceiverElement }`), + // so every branch constructs the Optional rather than leaking the raw storage read. arm "method_call.get" { "get" } => { - if matches!(&$receiver, Value::Str(_)) { - let key = $args.first().ok_or_else(|| InterpError::TypeError { - msg: "get requires a key argument".to_string(), - })?; - raw_map_lookup(&$receiver, key, $env, $ctx).map(RawMapLookup::into_raw) - } else if let Ok(items) = expect_list(&$receiver, "get") { + if let Ok(items) = expect_list(&$receiver, "get") { let idx = expect_int($args.first(), "get")?; - Ok(list_get_at_or_null(&items, idx)) + Ok(match list_index_in_bounds(&items, idx) { + Some(v) => optional_present(v, $ctx), + None => optional_absent($ctx), + }) } else { let key = $args.first().ok_or_else(|| InterpError::TypeError { msg: "get requires a key argument".to_string(), })?; - raw_map_lookup(&$receiver, key, $env, $ctx).map(RawMapLookup::into_raw) + let raw = raw_map_lookup(&$receiver, key, $env, $ctx)?; + Ok(map_lookup_as_optional(raw, $ctx)) } }, @@ -9266,7 +9585,9 @@ fn eval_algebra_method_inner( env: &Rc, ctx: &InterpContext, ) -> InterpResult { - v1_algebra_method_arms!(v1_algebra_dispatch, method, receiver, args, env, ctx) + let produced: InterpResult = + v1_algebra_method_arms!(v1_algebra_dispatch, method, receiver, args, env, ctx); + algebra_result_matches_declared_optionality(method, produced?, ctx) } pub fn fixture_now_secs(ctx: &InterpContext) -> Result { @@ -15048,7 +15369,10 @@ macro_rules! v1_builtin_arms { [list_val, idx_val] if free_monoid_to_vec(list_val).is_some() => { let items = expect_list(list_val, "get")?; let idx = expect_int(Some(idx_val), "get")?; - Ok(Some(list_get_at_or_null(&items, idx))) + Ok(Some(match list_index_in_bounds(&items, idx) { + Some(v) => optional_present(v, $ctx), + None => optional_absent($ctx), + })) } _ => Ok(None), }, @@ -17201,8 +17525,14 @@ fn value_to_list_carrier(val: &Value) -> Option<(Rc>, u64)> { } } -fn list_get_at_or_null(items: &RrbVector, idx: i64) -> Value { - items.get(idx as usize).cloned().unwrap_or(Value::Null) +/// In-bounds read, with the ABSENCE left for the caller to construct as an `Optional`. The +/// or-Null form this replaced could not distinguish an out-of-range index from a stored +/// `Value::Null`, which is the same collapse `first` used to make. +fn list_index_in_bounds(items: &RrbVector, idx: i64) -> Option { + if idx < 0 { + return None; + } + items.get(idx as usize).cloned() } fn expect_list(val: &Value, context: &str) -> InterpResult>> { diff --git a/src/v2/workflow/floor_non_verdict.dag b/src/v2/workflow/floor_non_verdict.dag index cf1666e25a3..f5616285770 100644 --- a/src/v2/workflow/floor_non_verdict.dag +++ b/src/v2/workflow/floor_non_verdict.dag @@ -15,6 +15,14 @@ import v2.std.collection { List } // assert anything. A diagnostic can describe evidence truthfully while the gate draws a false // conclusion from it; that happened on every run for a day. // +// WHICH FIELD CARRIES THIS, because a reader arrives here having cited the wrong one. The property +// "my enrolled known-reds are still discriminating" is carried by `non_verdict_unenrolled` in the +// floor's terminal line, NOT by `known_red_now_passing`: a known-red that stops reaching its +// assertion leaves the latter at 0, indistinguishable there from one still correctly red, and is +// refused by the former. Citing `known_red_now_passing` alone for that property is a citation +// defect and not a safety gap -- the adjacent counter gates -- but the two are read together often +// enough that saying so here is cheaper than rediscovering it. +// // THE RUNG, PER SEAM, because the governing rung is the minimum across them and stating only the // strongest is the inflation DESIGN section 4b(1) forbids: routing a thrown claim into its arm is // MITIGATABLE; printing the count is MITIGATABLE; printing `failed=0` without distinguishing