diff --git a/dag/gunbc/plans/dag_v2_defork_audit.dag b/dag/gunbc/plans/dag_v2_defork_audit.dag index f6f2573fbb4..829a5c70ccb 100644 --- a/dag/gunbc/plans/dag_v2_defork_audit.dag +++ b/dag/gunbc/plans/dag_v2_defork_audit.dag @@ -78,7 +78,7 @@ fn dag_v2_defork_audit_body() -> List { h3(text: "2B. 2026-09-22 executed correction to the `coercion` row — shared-symbol-count 0 was the wrong discriminator"), p(text: "**This audit classified `coercion` as a genuine not-a-fork on a shared *symbol* count of 0. Measured by execution, that count answers the wrong question.** The two modules share no symbol and denote no different concept: they answer ONE question — may this value cross from one model to another — and they answer it with **two admission authorities keyed on different identity relations**. `std.coercion` `dag_can_cast` folds over `dag_cast_rules` + `grounded_primitive_coproduct_identities`, keyed on type-name **STRINGS**, and it EXECUTES (`v1.compiler.infer` consults it at three decision points -- `kernel_value_declared_type_mismatch_bounded`, `application_type_names_compatible` and `validate_cast` (explicit `as`)). `v2.std.coercion` `coercion_fold` asks `v2.std.find_witness` `find_witness` for a structure-preserving witness, keyed on node **IDENTITY**, and has **no established executing consumer**. A shared-symbol count cannot see this, because the two sides cannot share a symbol: they cannot share a KEY."), p(text: "**The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity)."), - p(text: "**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either."), + p(text: "**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Int→Nat` — and `Bool→Int` at #12055, until #12227 withdrew its row (a `Bool` is not an `Int`), after which both sides refuse it and the fixture keeps it as the control that the withdrawal holds. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That cell is a property of the RAW HELPER roster, not a production refusal: every live composition in `v1.compiler.infer` admits name identity before it consults `dag_cast_rules`. Both sides matched their OWN declared contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either."), p(text: "**NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all."), p(text: "**Instrument:** `gunbc test`-reachable claims in `v2.test.claim.coercion.two_algebra_fork` — `name_keyed_coercion_matches_the_declared_cast_rosters_holds`, `homomorphism_coercion_matches_the_structural_preservation_contract_holds`, `homomorphism_coercion_admits_only_identity_quality_holds`. Each pins ONE algebra to its OWN independently specified contract, so a move in either side's admission set — consolidation included — reds the claim that owns it and the author must restate the row. **There is deliberately no fourth claim comparing the two algebras to each other** (review 70065): with both sides pinned to independent expectations, such a comparison is ENTAILED and its RED is not independently authorable, which DESIGN §4b rules out before the check is written. The agreement relation is DERIVED from the two expectation columns a row carries side by side. Two mutation arms establish discrimination rather than change detection: adding a `Bool→Float` row to `dag_cast_rules` reds ONLY the roster claim, and weakening the structural-preservation predicate reds ONLY the two homomorphism claims."), ThematicBreak, diff --git a/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag b/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag index 43079880b12..7ffac65ef7f 100644 --- a/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag +++ b/dag/gunbc/recurring_failure_mode/two_admission_authorities_keyed_on_different_relations.dag @@ -13,7 +13,7 @@ data two_admission_authorities_keyed_on_different_relations: RecurringFailureMod "DISTINGUISHING FACTS, and the first is the recognition rule: A FIXTURE THAT WANTS TO ASK BOTH AUTHORITIES ABOUT ONE SUBJECT MUST AUTHOR THE SUBJECT TWICE. That is not fixture awkwardness -- it IS the measurement, and it is available before any execution. Further tells: the two admission sets differ in BOTH directions, so neither authority is merely the stricter one and the comfortable reading is unavailable; and one side's key is a SPELLING while the other's is a resolved structural identity.", - "SPECIMEN 1 (gunbc, 2026-09-22, v2.test.claim.coercion.two_algebra_fork). std.coercion dag_can_cast folds over dag_cast_rules and grounded_primitive_coproduct_identities, keyed on TYPE-NAME STRINGS, and it executes: v1.compiler.infer consults it at three decision points -- kernel_value_declared_type_mismatch_bounded, application_type_names_compatible and validate_cast (explicit `as`). v2.std.coercion coercion_fold asks v2.std.find_witness find_witness for a structure-preserving witness, keyed on NODE IDENTITY, and it has no established executing consumer. Measured over seven supplied pairs, the admission sets differ in both directions: Int->Float, Bool->Int and Int->Nat are admitted name-only, while String->String -- an IDENTITY crossing -- is admitted homomorphism-only, because dag_cast_rules carries no identity row for it. That last cell is a property of the RAW HELPER roster, not of production: every live composition in v1.compiler.infer (kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast) admits name identity before consulting dag_can_cast, so the compiler does not refuse an identity crossing. What the specimen establishes is two admission contracts on disjoint keys, not a production refusal.", + "SPECIMEN 1 (gunbc, 2026-09-22, v2.test.claim.coercion.two_algebra_fork). std.coercion dag_can_cast folds over dag_cast_rules and grounded_primitive_coproduct_identities, keyed on TYPE-NAME STRINGS, and it executes: v1.compiler.infer consults it at three decision points -- kernel_value_declared_type_mismatch_bounded, application_type_names_compatible and validate_cast (explicit `as`). v2.std.coercion coercion_fold asks v2.std.find_witness find_witness for a structure-preserving witness, keyed on NODE IDENTITY, and it has no established executing consumer. Measured over seven supplied pairs, the admission sets differ in both directions: Int->Float, Bool->Int and Int->Nat were admitted name-only (Bool->Int left the name-keyed roster in #12227), while String->String -- an IDENTITY crossing -- is admitted homomorphism-only, because dag_cast_rules carries no identity row for it. That last cell is a property of the RAW HELPER roster, not of production: every live composition in v1.compiler.infer (kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast) admits name identity before consulting dag_can_cast, so the compiler does not refuse an identity crossing. What the specimen establishes is two admission contracts on disjoint keys, not a production refusal.", "SPECIMEN 2 (gunbc, 2026-09-22, smart-tern-891, a different surface and an independent sighting). One resource appeared under two labels, Network and std.resources.Network, because a diagnostic field carried the caller's IMPORT SPELLING while the wall itself compared through the resolved declaration identity. Correct by identity in one place, keyed by spelling in another, and only the second was load-bearing for the new consumer. Two independent sightings on one day is what makes this a class rather than a fact about coercion.", diff --git a/dag/gunbc/representation_boundary.dag b/dag/gunbc/representation_boundary.dag index bf8969557e8..144dc4466db 100644 --- a/dag/gunbc/representation_boundary.dag +++ b/dag/gunbc/representation_boundary.dag @@ -311,7 +311,7 @@ data coercions_boundary: RepresentationBoundary = RepresentationBoundary { crossing_evidence: InterpretedOnly { what_goes_red: "the identity-keyed half is a real climb with a receipt: passing the empty string once meant identity-unknown, and eight reference sites doing so rendered dag/std/integer.dag aliases as crate::std_nat::Nat instead of i64. There is now no empty string to pass -- an absent identity is DeclarationIdentityAbsent, and the degraded answer is stamped GroundedByUnidentifiedBareRow so it stays countable rather than silent." as NonEmptyStr, blocked_on_a_two_route_oracle: "THE FORK ITSELF. No execution joins the cast table to the homomorphism fold, so if they disagreed today nothing would go red. That is the finding, and it is why this row is not recorded as DEFERRED: a fork whose disposition reads as adjudicated is worse than an unrecorded one, and this fork stayed invisible precisely because the census that holds it asked whether the two modules SHARE TYPE NAMES -- see the scope note on gunbc.plans.dag_v2_defork_audit, whose coercion row answers a resolver-collision question and not this one." as NonEmptyStr, - unbuilt_but_testable_now: "BUILT (#12055, v2.test.claim.coercion.two_algebra_fork), and it measures the two HELPER CONTRACTS, not the production judgments. Seven supplied pairs reach dag_can_cast and coercion_fold directly, each held to an expectation transcribed from ITS OWN declaration: Int to Float, Bool to Int and Int to Nat are admitted name-only, String to String homomorphism-only. WHAT IT DOES NOT ESTABLISH, TWO THINGS. First, no independent semantic oracle: each column restates its own side, so the agree-and-both-wrong arm is still unreportable. Second, no production refusal: every live composition -- kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast -- admits name identity BEFORE consulting dag_can_cast, so the String to String cell is a property of the raw helper roster and not an identity crossing the compiler refuses. What remains unbuilt and climbable is the context matrix named on the trigger." as String + unbuilt_but_testable_now: "BUILT (#12055, v2.test.claim.coercion.two_algebra_fork), and it measures the two HELPER CONTRACTS, not the production judgments. Seven supplied pairs reach dag_can_cast and coercion_fold directly, each held to an expectation transcribed from ITS OWN declaration: Int to Float and Int to Nat are admitted name-only (Bool to Int was too, until #12227 withdrew the row), String to String homomorphism-only. WHAT IT DOES NOT ESTABLISH, TWO THINGS. First, no independent semantic oracle: each column restates its own side, so the agree-and-both-wrong arm is still unreportable. Second, no production refusal: every live composition -- kernel_value_declared_type_mismatch, application_type_names_compatible, validate_cast -- admits name identity BEFORE consulting dag_can_cast, so the String to String cell is a property of the raw helper roster and not an identity crossing the compiler refuses. What remains unbuilt and climbable is the context matrix named on the trigger." as String }, next_trigger: climbs_when(capability: "every consumer of the shared name-pair cast rosters asks ITS OWN judgment through that judgment's one authority, SUFFICIENT FOR dag_can_cast, dag_cast_rules and is_dag_cast_domain_type to have no remaining decision-making caller and be deleted or derived, and for the per-target CastSyntax cast_rules to be consumed by target realization rather than re-deciding legality. THE ROSTER IS NOT ONE QUESTION WITH ONE REPLACEMENT HOME: it is consulted inside declared-type compatibility (v1.compiler.infer kernel_value_declared_type_mismatch and application_type_names_compatible) and inside explicit `as` validation (validate_cast), while v1.compiler.coercion can_cast and the emitter's cast arm read a SEPARATE per-target roster. Literal introduction at a structural destination is already owned by std.literal_elaboration, and Int to Nat is already split between that literal homomorphism and a proof-requiring refinement cast (refinement_cast_rules); neither is a widening. So the homes are expected to be several -- declared-type inhabitance, literal elaboration, an explicit-conversion judgment, target realization -- and naming one fold here, v2.std.coercion coercion_fold or v2.std.inhabitance alike, would be an over-broad home that repointing callers could satisfy while a question stayed forked. The prerequisite is a consumer-by-judgment partition with context-discriminating probes (literal, arbitrary value at a formal, explicit cast, emitted) per admitted pair; if it shows several questions, this row is split per judgment rather than retired whole. Deleting the v1 seed does not fire this: four extdeps language types modules author per-target cast rows and survive v1.") } diff --git a/docs/plans/dag-v2-defork-audit.md b/docs/plans/dag-v2-defork-audit.md index 3377e4c6c86..c9e70ad131f 100644 --- a/docs/plans/dag-v2-defork-audit.md +++ b/docs/plans/dag-v2-defork-audit.md @@ -110,7 +110,7 @@ Three tiers. **Mirror** = v2's used symbols ⊆ dag → mechanical delete + repo **The recognition rule, available before any execution: a fixture that wants to ask both authorities about one subject must author the subject TWICE.** No conversion between a type-name spelling and a node identity exists anywhere in the corpus, so `v2.test.claim.coercion.two_algebra_fork` carries `source_type`/`target_type` (strings) beside `source_name`/`target_name` (symbols) on every row. That duplication is not fixture awkwardness — it **is** the measurement. This is a keys/hashing conformance subject (DESIGN §3b names structural node identity as a home there), not a coercion subject, and the finding generalizes: the class is filed as `gunbc.recurring_failure_mode` `two_admission_authorities_keyed_on_different_relations`, with an independent same-day specimen in a different surface (one resource under `Network` and `std.resources.Network`, a diagnostic field carrying the caller's import spelling while the wall compared resolved declaration identity). -**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Bool→Int`, `Int→Nat`. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That last is the sharpest single fact, because an identity coercion is the one case a reader assumes is free. Both sides matched their OWN independently specified contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either. +**EXECUTED RESULT over seven supplied source/target pairs — the admission sets differ in BOTH directions, so neither side is merely the stricter one.** `coercion_fold`'s only realized preservation rule is `preservation_rule_exact_structural_equality_zip_fold`, whose predicate holds exactly when the candidate is structurally equal to the source, so the homomorphism side cannot SPELL a non-identity crossing at all. **Admitted name-only:** `Int→Float`, `Int→Nat` — and `Bool→Int` at #12055, until #12227 withdrew its row (a `Bool` is not an `Int`), after which both sides refuse it and the fixture keeps it as the control that the withdrawal holds. **Admitted homomorphism-only:** `String→String` — an IDENTITY crossing, which `dag_cast_rules` carries no row for. That cell is a property of the RAW HELPER roster, not a production refusal: every live composition in `v1.compiler.infer` admits name identity before it consults `dag_cast_rules`. Both sides matched their OWN declared contract on all seven pairs (the declared rosters for one, the structural-preservation predicate for the other), so this is a fork between two correct-by-their-own-lights authorities and not a defect in either. **NOT REPAIRED, by ruling (snappy-deer-443, 2026-09-22).** The repair is a replacement migration (DESIGN §3, replacement migrations cut over at the root) — one key wins, the other algebra is cut at its root — with its own blast radius, and it is a separate lane that should start from these executed values rather than from the derivation that found them. The DEFERRED verdict in the table above is therefore **superseded as to its reasoning, not its timing**: the deferral was priced as a module-BASENAME rename held for v1-shrink, and the actual subject is an admission-key consolidation whose cost is not a rename at all. diff --git a/src/v2/test/claim/coercion/two_algebra_fork_test.dag b/src/v2/test/claim/coercion/two_algebra_fork_test.dag index b5de61488e8..cca5d57de12 100644 --- a/src/v2/test/claim/coercion/two_algebra_fork_test.dag +++ b/src/v2/test/claim/coercion/two_algebra_fork_test.dag @@ -38,8 +38,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // crossing exactly when source and target are the SAME model, and admits it at quality // Identity. Nothing in that side spells a non-identity crossing at all. // -// A row can therefore report BOTH AGREE AND BOTH ARE WRONG, or either algebra deviating from its -// own declared contract, rather than only "the two folds match". +// A row can therefore report either algebra deviating from its OWN declared contract, rather than +// only "the two folds match". It CANNOT report that both agree and are both semantically wrong: +// each expectation column is transcribed from its own algebra's declaration, so there is no +// independent semantic oracle here (gunbc.representation_boundary coercions_boundary records the +// same limit). type CoercionAdmission = CrossingAdmitted @@ -67,9 +70,11 @@ type CoercionForkFixture { // // both admit -- int_to_int, float_to_float: a declared row whose source and target are one // model, the only shape on which the two algebras can coincide. -// both refuse -- bool_to_float: no declared row and no structural equality. -// name-only -- int_to_float (a declared widening), bool_to_int (a declared crossing with -// no structural relation at all), int_to_nat (a GROUNDED identity that the +// both refuse -- bool_to_float and bool_to_int: no declared row and no structural +// equality. bool_to_int was name-only until #12227 withdrew its row -- a +// Bool is not an Int (the 2026-09-26 coercion ruling, DESIGN section 4) -- +// so it now pins that the withdrawal holds. +// name-only -- int_to_float (a declared widening), int_to_nat (a GROUNDED identity that the // name-keyed side carries in its own second roster). Each is a crossing the // executing algebra permits and the specified algebra cannot spell. // homomorphism-only -- string_to_string: an IDENTITY crossing, which the name-keyed roster does @@ -111,7 +116,7 @@ data coercion_fork_fixtures: List = [ target_type: "Int", source_name: ^Bool, target_name: ^Int, - expected_name_keyed: CrossingAdmitted, + expected_name_keyed: CrossingRefused, expected_homomorphism: CrossingRefused }, { @@ -235,7 +240,7 @@ fn coercion_admission_equal(left: CoercionAdmission, right: CoercionAdmission) - // // THE MEASUREMENT SURVIVES WITHOUT IT, and this is the point rather than a concession. The // agreement relation is DERIVED from the two expectation columns, which sit side by side on every -// row: four of the seven rows carry expectations that differ, in both directions, and that is the +// row: three of the seven rows carry expectations that differ, in both directions, and that is the // fork stated where a reader meets the population. If either algebra's admission set moves -- in // either direction, consolidation included -- the claim that owns that side reds and the author // must restate the row. Nothing was lost by deleting the comparison except a second spelling of a