Repository navigation
Compiler floor: payload-carrying coproduct arm literals get an excess-field roster (the class is wider than sibling variants) - #9846
Conversation
…gets an excess-field roster
MEASURED, not read: on origin/main a payload-carrying variant literal received NO excess-field
judgment at all. `Circle { radius: 1, nowhere: 2 }` -- a field declared nowhere in the program --
compiled with zero FieldNotFound, and so did a sibling arm's field and an unrelated coproduct's
field. The lane was opened as "admits fields declared on sibling variants"; the nowhere-declared
discrimination control says the class is wider than that, and a repair scoped to sibling arms would
have left it open.
THE ASYMMETRY THAT HID IT, on one literal: against an arm declaring `radius` and `color`,
`Circle { radius: 1 }` reports MissingField == 1 while `Circle { radius: 1, nowhere: 2 }` reports
FieldNotFound == 0. The literal refused an OMITTED field and accepted an INVENTED one, so nothing
downstream ever looked wrong.
MECHANISM. `variant_arm_type_projection` projects an arm out of its owner only when the arm carries
no payload, so `lookup_type_by_name` hands `infer_record_lit_structural` the OWNER coproduct for a
payload arm. `record_lit_construction_field_names` requires Conj, answers `none`, and the
unknown-field arm's `Absent => []` is silence. Presence checking never had this hole because it
reads the arm through `variant_owner_node` -- so the two halves of one judgment were consulting two
different authorities, one of them absent.
THE REPAIR IS THE SAME READ, PROJECTED TO NAMES. `record_lit_variant_arm_field_names` selects the
constructed arm through `variant_owner_node` and expands it exactly as presence checking does, so
excess and missing now answer from ONE roster (DESIGN 3). A nullary arm answers `[]` rather than
`none`, because a zero-field arm's roster is EMPTY and not UNKNOWN: `Red { x: 1 }` was admitted on
main and now refuses, while the bare tag reference `Red` is untouched -- it carries no field inits
for the arm to judge.
`field_in_any_variant_named` is DELETED, not narrowed. It had exactly one definition and one call
site in the .dag authority, and it was unreachable on the arm path it appeared to serve:
`construction_field_names` is Present only for a Conj decl, which an arm name never resolves to.
The selected-arm roster subsumes its only reachable case -- a name that is both a product type and a
coproduct arm -- where the product roster is still consulted first, so what disappears is
specifically sibling-arm acceptance.
EVIDENCE, executed on the regenerated seed. Every probe moved exactly as predicted and all four
positive controls held: sibling / nowhere-declared / unrelated-coproduct fields 0 -> 1, the nullary
arm handed a field 0 -> 1, and valid arm literals, valid product literals, the bare nullary tag and
the pre-existing product wall all unchanged. The missing-field arm still reports MissingField == 1
with FieldNotFound == 0. Enrolled as test.claim.infer_record_lit_variant_field_witness_test, whose
module prefix is inside required_gate_prefixes, with the undeclared-field arm as the discriminating
control and the product arms as regression controls.
Regen reported drift in exactly one file and a second --required-regen returned
first_generation_equal=true, so the seed mirror is a fixed point again.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0168SHaTYM15tXSLQaPPhXfb
…rals it refuses
CORRECTS THE PREVIOUS COMMIT, which the corpus falsified. That commit invented a second roster
(`record_lit_variant_arm_field_names`) reached through a bare-name `lookup_type_by_name`. Run
33448581154 refused a VALID literal with it:
dag/gunbc/host/host_converge.dag:517 field 'host_identity' not found in type 'CodexRuntimeBundle'
`CodexRuntimeBundle` names a local coproduct ARM in gunbc.host_converge and an unrelated PRODUCT
type in gunbc.package_delivery. A name-only lookup answered with the foreign product's fields, so a
literal correct against the arm its own module declares was rejected. A floor change that refuses
valid code is worse than the hole it closes, and no synthetic probe could have caught it -- they are
all single-module and cannot express a cross-module homonym.
THE JOIN, rather than a second lookup beside the first. `presence_fields` already selects the fields
of the type actually being constructed, through a cascade that asks `variant_owner_node` and the
EXPECTED type before any bare-name fallback -- and that cascade has been deciding MissingField over
the whole corpus, so its resolution behavior is the one with evidence behind it. The excess check now
reads it. Both invented functions are deleted, and so is `record_lit_construction_field_names`, which
that join made dead: 91 lines of emitted seed removed against 23 added.
`none` and `[]` stay distinct and the distinction is the wall. `none` is an UNKNOWN roster -- an
unresolved or ambiguous name, or a cascade that bottomed out -- and must stay silent rather than
refuse every field against a roster it does not have. `[]` is a KNOWN EMPTY roster, which is exactly
a nullary arm. The ambiguity guard is shared with MissingField for the reason it exists there: an
ambiguous name has not been resolved to a type, so neither half may judge its fields.
THREE CORPUS LITERALS THIS REFUSES, each a true positive and each behaviour-preserving to repair,
because the excess field was never stored:
fabric_control_plane_charge.dag:8 SingleAuthority { reason: ... } -> Terminal { reason: ... }
type_reference_containment_binding:13 SingleAuthority { bind: ... } -> Scaffold { dissolves_to: SingleAuthority, bind: ... }
annotation_parse_instrument_agreement:30 Terminal { ..., authority: ... } -> field dropped
`SingleAuthority` is a NULLARY arm of ConstructionMechanism and not a Disposition arm at all, so the
first two declared a Disposition by naming something that is not one and attached a field to a tag
that has none. `reason` belongs to Terminal; `authority` is not a field of Terminal. In all three a
paragraph of authored prose was being silently discarded -- DESIGN 4c's misplaced-commentary row,
made visible by the floor rather than by review.
Seed regenerated from the corrected .dag: drift in exactly one file, and a second --required-regen
returned first_generation_equal=true. Mirror digest
0d1a308a806f7a9841840f4195d48872785baf6aa2857a8de202d0d0deefef1e.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0168SHaTYM15tXSLQaPPhXfb
`v2.std.verification` declares `BoolWitnessClaim { witness: BoolWitness }` -- one field. This
literal supplied a `label:` as well, and it was silently discarded. Behaviour-preserving to remove
for the same reason as the other three: the field was never stored, so nothing read it and nothing
changes by deleting it.
Not a missing feature on the type: 30 BoolWitnessClaim literals exist in the corpus and exactly one
carried a label, so this is a one-off rather than a pattern the declaration fails to serve. The
text it carried restates what the module path and the witness function name already say, which is
DESIGN 4c's misplaced-commentary row -- it is not rehomed to an annotation, because an annotation
that restates the declaration is the thing 4c forbids.
Found by the required floor over 2152 resolved modules, the last diagnostic standing after the
build lane went green.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0168SHaTYM15tXSLQaPPhXfb
…he change
gunbc.v1_maintenance_standing carries the rule this follows: an admission is "recorded in the same
PR as the change it admits, because an admission written afterwards is indistinguishable from an
author's own classification." v1 is SemanticsFrozen { maintenance: MaintenanceActive }, and this PR
changes v1 semantics -- programs that compiled now refuse -- so it owes a classification against
the five refused classes, which dominate every admission.
INSTANCE: DefectRepairDiagnosticsMayMove, the class whose own name contemplates diagnostics moving
and which the standing gates on "a specific incorrect behavior the seed exhibits TODAY, evidenced".
That is what separates this from the argv-fabricator proposal the same file REFUSES a few rows
above: an unreachable arm exhibits nothing, while this behavior is measured on a discriminating
pair and cost four corpus literals their authored fields.
NewLanguageBehavior is the hard question and the row answers it rather than omitting it: literally
the accepted language shrinks, and the counter-argument is preserved verbatim for whoever overturns
this -- a strict enough reading refuses every floor repair, which would make DESIGN 4b's
floor-first mandate unimplementable in the seed. Nothing mechanically holds the distinction, and
the row says so.
NO OPERATOR RULING IS CITED, stated plainly rather than dressed up: the two admissions above relay
verbatim operator sentences and this one has none, resting instead on DESIGN 4b naming "fields
exist" in the floor. A reader who wants an operator sentence will not find one.
Filed because the authority requires it, not because a review asked: the dashboard review APPROVED
this PR without any v1 classification. The file's own RcStr row records the precedent -- a first
review approved a change without its classification and a second refused it FOR the omission.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0168SHaTYM15tXSLQaPPhXfb
|
This PR reads Measured just now against current Both sides changed a generated projection since the merge base, so neither side's bytes are the projection of the merged authorities. GitHub does not run this repo's merge driver — its This is not hypothetical: squashing a PR in this state silently reverted two siblings' ledger rows earlier today (#9868), and #9937 exists only to put them back. The loss lands outside any conflict region, so nothing reds. Fix — do not hand-resolve and do not pick a side:
A census of all open PRs found 15 in this state; this is one of the ones GitHub is reporting as clean, which makes it among the more dangerous. |
|
Correcting my own comment above: the remedy I gave is the wrong one for this PR. I wrote the generic recipe — regenerate through This PR's divergence is on The second rebuild-and-verify is not optional: the first pass runs a binary that predates the change it emits, so one pass can self-verify at divergence 0 for the wrong reason. And this case is worse than the doc case, which is why I am correcting rather than leaving it. A bad resolution on a ledger produces a stale document that the next drift gate catches loudly. A bad resolution on Apologies for the noise; better a second comment than a wrong recipe standing. |
Two conflicts, resolved in opposite ways because they are different kinds of fact. dag/gunbc/v1/v1_maintenance_standing.dag -- BOTH ROWS KEPT. Main added the 2026-09-02 authorized-exception row for the adapter-alignment control; this branch adds the excess-field floor admission. They are independent admissions on one carrier, not two versions of one fact, so neither side is a resolution. src/v1/stage0/src/v1_compiler_infer.rs -- REGENERATED, not resolved. The generated-artifact merge driver refused rather than answering, which is what it is for: both sides changed the projection since the merge base, so neither side's bytes are the projection of the merged authorities. The .dag authority (src/v1/04_infer.dag) auto-merged clean, and the bytes were re-derived from it. One wrinkle worth recording, because it inverts the obvious order of operations: this branch's mirror NO LONGER COMPILES against merged main -- main changed elaborate_literal_at to take five arguments and added LiteralUnfolding::UnicodeScalarSequenceUnfold -- so the regen binary could not be built from our own bytes. Main's mirror was installed purely as a BUILD SUBSTRATE to get a working claim_executor, and the merged authority was then re-emitted over it. The result carries both sides by construction: main's new arity and match arm, and this branch's repair, with field_in_any_variant_named and record_lit_construction_field_names absent (grep 0). src/v1/stage0/src/gunbc_rust_source_type_bindings.rs -- INHERITED DRIFT, not this PR's change. Regen rewrote one proof string in it. This branch touches no authority for that file (git diff origin/main...HEAD --name-only matches nothing for it), so the drift arrived from main: an authority row changed there whose mirror was not regenerated. Installing the regenerated bytes is what the gate demands; it is flagged here so it is not read as this change. EVIDENCE, executed. The merged seed builds clean. The second --required-regen was run by a binary REBUILT FROM THE INSTALLED SEED and reports first_generation_equal=true, planned=150 executed=150 adjudicated=150, the single declared_divergent [main.rs] being the standing exception present identically before the merge. --required-regen-fixed-point reports fixed_point_equal=true referenced_first_generation_equal=true. The first pass is not cited as evidence: it ran a binary predating the change it emits, which can self-verify at divergence 0 for the wrong reason. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rnk6hRDoDkLTBmC9p363GM
The class, corrected
A record literal on a payload-carrying coproduct arm received no excess-field judgment at all.
Not "admits sibling variants' fields" — the lane's original title. The discriminating control is the
nowhere-declared field:
Four zeros on sibling-field probes cannot separate "the roster leaks to siblings" from "no roster is
consulted", and it was the second. A repair scoped to sibling arms would have left the class open,
and a §4b(3) row declared against the sibling class would have been retired by a trigger that never
restored the capability.
The asymmetry that hid it, on one literal. Against an arm declaring
radiusandcolor,Circle { radius: 1 }reportsMissingField == 1whileCircle { radius: 1, nowhere: 2 }reportsFieldNotFound == 0. The literal refused an omitted field and accepted an invented one, sonothing downstream ever looked wrong.
Mechanism
variant_arm_type_projectionprojects an arm out of its owner only when the arm carries nopayload, so
lookup_type_by_namehandsinfer_record_lit_structuralthe OWNER coproduct for apayload arm.
record_lit_construction_field_namesrequiredConj, answerednone, and theunknown-field arm's
Absent => []was silence. Presence checking never had the hole because itreads the arm through
variant_owner_node— two halves of one judgment consulting two authorities,one of them absent.
field_in_any_variant_named, which the lane title names, was not the admitting disjunct: it isconsulted only when
construction_field_namesisPresent, which an arm name never produces.The repair: one roster, not a second lookup
The excess check now reads
presence_fields— the same cascadeMissingFielduses, which asksvariant_owner_nodeand the expected type before any bare-name fallback.field_in_any_variant_namedand
record_lit_construction_field_namesare both deleted, not narrowed: 91 lines of emittedseed removed against 23 added.
noneand[]stay distinct and the distinction is the wall.none= roster UNKNOWN (unresolved orambiguous name) → stay silent.
[]= roster KNOWN and EMPTY = a nullary arm →Red { x: 1 }refuseswhile the bare tag
Redis untouched.A first attempt this PR discarded, because the corpus falsified it
The first mutation invented its own roster via a bare-name
lookup_type_by_name. It refused validcode:
CodexRuntimeBundlenames a local coproduct arm ingunbc.host_convergeand an unrelatedproduct type in
gunbc.package_delivery, and the name-only lookup answered with the foreignproduct's fields. Same for
PullRequest { branches, types }inwitness_floor_workflow— decisivelya false refusal, since the emitted
witnesses.ymlvisibly carries those fields. No synthetic probecould catch either: they are all single-module and cannot express a cross-module homonym. The
presence cascade has been deciding
MissingFieldcorpus-wide, so its resolution behavior is the onewith evidence behind it.
Evidence (executed)
MissingField1MissingField1,FieldNotFound0RedAll 11 arms of
test.claim.infer_record_lit_variant_field_witness_testappear in therequired-floor-disposition artifact as
planned_as_changed_witness … passed— executed, not merelyenrolled. Its module prefix is inside
required_gate_prefixes.Corpus population: 3 refusing identities + 1 repaired defect that refuses nothing, all repaired here
The newly-refusing population is three — identities 1, 2 and 4 — every one observed by execution:
gunbc.fabric_control_plane_chargefabric_control_plane_charge_authorityreasonSingleAuthoritygunbc.type_reference_containment_binding..._scaffoldbindSingleAuthorityv2.test.claim.execution.emit_ingest_..._round_trip_testclaim_...labelBoolWitnessClaimIdentity 3 is a REPAIRED DEFECT, not a member of the newly-refusing population, stated separately rather than folded in:
gunbc.annotation_parse_instrument_agreement..._dispositionauthorityTerminalThat module is resolved by no required lane, pinned by three independent facts: its name appears
nowhere in the floor log; the build lane passed with the defect present on a probe branch, so
its closure demonstrably excludes it; and nothing imports it. A scoped
--entrycompile — the lastroute — OOM-killed the runner at 97% of 7.86 GB, because
--entryscopes what is emitted, notwhat is indexed. No available host can compile that module. It is a true defect (
Terminaldeclares only
reason) and it is repaired here, but it is not promoted to "observed", and noreplica fixture is offered in place of the site.
SingleAuthorityis a nullary arm ofConstructionMechanismand not aDispositionarm atall, so the first two declared a
Dispositionby naming something that is not one. Every repair isbehaviour-preserving: the excess field was analysed and then discarded, so nothing read it.
(Initializer analysis measured independently by
smart-moth-158.)§4b(3)
No declared drop is owed. A drop row covers a rung lowered; this raises one and refuses nothing
that was correct. The population is closed and repaired in this PR, so there is no bounded runway or
restoration trigger for a row to carry. Rung: mechanically preventable → structurally guaranteed
for the excess-field class on source→interpretation. Not impossible — the invalid state is still
authorable in source, which is why the RED probes stay enrolled.
Honest ceiling: the roster stays
none(silent) where the cascade cannot resolve the name — anunresolved or ambiguous bare name. Unchanged behaviour, the same guard
MissingFielduses, namedhere so "structurally guaranteed" is not read as covering it.
Seed
Regenerated from the corrected
.dag: drift in exactly one file, second--required-regenreturnedfirst_generation_equal=true. Mirrorv1_compiler_infer.rssha2560d1a308a806f7a9841840f4195d48872785baf6aa2857a8de202d0d0deefef1e.Lane
adhoc-0f99c6bc-193. Intake packet bound to treeec48ae29ba(the merge of09360be7d3binto main
37e705c42e— a PR run compiles the merge ref, not the head), run33455123780.One changed byte in a stage0 seed file that is NOT this change
src/v1/stage0/src/gunbc_rust_source_type_bindings.rsdiffers from main by one line. It isregenerated output, not authorship. Nobody edited it here, and it must not be reverted to main's
bytes to make this PR look tidier — those bytes are a known-false projection.
What it is. The
prooffield of thecheckpoint_row_migration_rowsrow whosedag_nameis"String", dispositionProvenUniqueKernelBinding. The committed proof is 694 bytes and theauthority emits 3422; they agree for 296 characters and then diverge. The new text opens "THE
VERDICT STANDS AND ITS ORIGINAL ARGUMENT WAS EXACTLY INVERTED, corrected here rather than softened
because the inverted form would justify the wrong things if reused" and restates the old
shadowing-is-the-identity-on-one-token argument as the thing being corrected. gunbc#9949 moved that
authority row and did not regenerate its mirror, so main is authority-ahead-of-artifact on one row.
How it got here. The merge's own re-emission wrote it. Resolving the
v1_compiler_infer.rsconflict required rebuilding the emitter from the installed seed and re-emitting the merged
authority; that pass re-derives every projection, including this one. It was not sought and it is
not scoped work.
Why it is worth stating rather than hiding. It is why this PR's
required-witnesses-buildisgreen while gunbc#9977, #9984 and #9985 are red on the same file — the only branch that regenerated
is the only branch whose mirror matches its authority. A natural experiment, not a claim.
It is deliberately not expanded here. The standalone repair is being cut off current main by
lively-koi-693. Whichever lands first makes the other trivial. This PR is a compiler-floor changeand stays one; the retracted phrase
over a fixture module importingis present once on main andzero times here, which is the whole of the difference.