Repository navigation
XL-0T-CUTOVER: build Y — one exact declaration binding per TypeOccurrence from the containment authority — and retire #9813's module-wide precedence at the root. AUTHORING AUTHORIZED by ruling, MERGE HELD for root-cut receipts. Local use-line/qualification repairs are DEAD. - #10207
Closed
briansrls wants to merge 10 commits into
Closed
briansrls wants to merge 10 commits into
briansrls wants to merge 10 commits into
Conversation
…per reference std.occurrence_binding_candidates resolve_reference_via_structural_candidates documents that it builds the candidate index exactly once per transport, and it does. Per reference it then called std.occurrence_binding_resolve resolve_reference_occurrence_binding, whose first act is occurrence_transport_validate over the WHOLE transport -- three full folds across every index entry, declaration and reference. So the once-built index was defeated one layer below itself and the path was O(references x population). MEASURED, NOT REASONED, on the same subject in both directions: the census instrument added here resolving dag/std -- 142 files, 9672 type-occurrence references -- ran past a 45-minute wall producing nothing. After the repair the same run over the same subject completes in 8 seconds. THE REPAIR IS FEWER REPRESENTATIONS OF ONE FACT, NOT A CACHE. occurrence_candidate_index_build already validates exactly once and already held the whole ValidatedOccurrenceTransport; it kept entries_by_id and discarded the other four fields, which is precisely what left the resolver unable to hand a validated transport down. OccurrenceCandidateIndex now carries the ValidatedOccurrenceTransport itself -- entries_by_id is reached through it, so there is no second copy to drift -- and the resolver calls the ALREADY-EXISTING resolve_reference_occurrence_binding_validated. This is DESIGN section 2's demand-graph move (carry the value to the shared ancestor), not a memoization, and DESIGN section 6's bare-minimum-cost standing rule settles it independently: a proven cost-shape defect is always fixed regardless of realized n. Here n is every type occurrence in the corpus. BOTH SITES, because one fact with two homes is what lets a repaired path sit beside an unrepaired one answering the same question. std.reference_binding_observation structural_binding_resolution_from_candidates had the identical shape and is repaired with it. THE `transport` PARAMETER IS GONE from both entry points rather than left unused: a second unvalidated OccurrenceTransport beside the validated one is two representations with nothing forcing them to be the same transport, and a caller handing in a different one would resolve silently against whichever arm read it. BEHAVIOUR IS PRESERVED BY THE EXISTING WITNESSES, which is why this carries no new behavioural test. resolve_type_reference_containment_binding and structural_binding_walk keep their signatures, so test.claim.type_reference_containment_binding_witness_test, test.claim.type_reference_binding_context_witness_test and test.claim.occurrence_binding_candidates_witness_test assert the same bindings through the changed code. What changed is cost, and the instrument -- not a transcribed number -- is what re-derives it. WHY IT IS NOT BUNDLED WITH THE XL-0T CUTOVER IT WAS FOUND UNDER: the cut routes every type occurrence in the corpus through this path, so switching type-position consumers to it while it revalidates per occurrence would ship a regression even if every binding answer were right. It is a prerequisite of that cut, and a cost repair and an authority cutover are two subjects. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
…in the corpus was unbindable
MEASURED FIRST, over dag/std (142 files) with the census instrument's --denominator
mode: 9672 TypeOccurrence REFERENCES against type_occurrence_declarations=0.
TypeOccurrence appeared four times in v1.compiler.parse -- the enum member and three
ParsedOccurrenceReference sites -- and ParsedOccurrenceDeclaration was produced with
FieldOccurrence, LexicalValueOccurrence, CallableOccurrence and
NamespaceSegmentOccurrence, never with TypeOccurrence.
std.occurrence_binding_candidates buckets candidates by authored spelling and
std.occurrence_binding_resolve admits a TypeOccurrence reference against a
TypeOccurrence declaration only, so an empty declaration side made EVERY type
reference in the corpus Unbound -- not mis-bound, UNBINDABLE. The containment
authority the namespace cut resolves through was correct, executing, and had never
been fed a production population.
THE DISCRIMINATING CONTROL that located it upstream of visibility: all three
DeclarationExposureGrounding values returned BYTE-IDENTICAL partitions. Exposure
decides visibility and is the variable the census varies; a zero insensitive to it
cannot be a visibility result.
WHY NO FIXTURE COULD HAVE SHOWN THIS.
test.claim.type_reference_containment_binding_witness_test hand-builds its
declarations with `category: TypeOccurrence` -- exactly the shape production never
emitted -- so the suite supplied the missing side itself and stayed green. DESIGN
section 5's specification-without-execution boundary, sitting on the DESTINATION
authority of a migration, where a green suite is not weak evidence but zero
evidence. Those fixtures are untouched here: they test the authority's logic
correctly, they were never SUFFICIENT, and nothing in the tree said so.
THE RULE IS STATED POSITIVELY rather than as "not a function": a module item
declares a type when it has no body, no transport and no type annotation. That
admits the three authored forms -- `type X { .. }` (Conj), `type X = A | B` (Disj),
and the bare alias `type X` -- and excludes by construction the items that are
values or effects: a function has a body, a `data x: T = v` has a body AND an
annotation, a service carries a transport. Imports cannot be caught by it: they live
in the module node's params and are stamped on a different path from its children.
RESULT, same instrument, same subject, dag/std:
type_occurrence_declarations 0 -> 1243
Y bindings 0 -> 3057
partition still closes at 9672, zero unclassifiable
and the five-way census the cut needs has content for the first time: 2786
OldAndNewAgree, 2203 OldBinds_NewUnresolved, 3136 OldKernel_NewUnresolved, 909
OldSynthetic_NewUnresolved, 367 OldUnresolved_NewUnresolved, 250
OldSynthetic_NewBinds, and 21 OldAndNewDisagree -- the first real binding deltas
anyone can adjudicate.
SCOPE IS DECLARED SO THE NEXT INCREMENT IS DRIVEN BY MEASUREMENT. This stamps
MODULE-LEVEL type declarations. Coproduct VARIANTS in type position and TYPE
PARAMETERS are reachable from this walk and are NOT stamped, so references to them
stay Unbound and the census names them rather than passing over them in silence. The
same run also shows MethodOccurrence at 382 references against 0 declarations --
an independent gap in the same collector, not addressed here.
Stage0 mirror regenerated; the emitted drift is exactly v1_compiler_parse.rs.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
…in targets CI red on the merge-blocking `cargo clippy --all-targets -- -D warnings` step: six lints in the census binary added by the parent commit -- one very-complex-type on the three-vector return of `inputs_for_module`, and five `clone()` calls on `OccurrenceId` and `DeclarationExposureGrounding`, both of which are `Copy`. The return triple is now the named `ModuleInputRows`, because a bare tuple of three vectors says nothing about which list is which, and the five clones are dropped. Behaviour is unchanged: cloning a Copy type and copying it are the same value. WHY IT REACHED CI AT ALL, recorded because the tree already warns about exactly this and I walked into it anyway. I verified the new binary with `cargo build`, and DESIGN's Building & checks section states that `cargo clippy --all-targets -- -D warnings` is "the only command that compiles the integration-test and example targets, so a red there is invisible to every other step". A new `[[bin]]` target sits in precisely that blind spot: every check I ran was green and none of them compiled the file under the gate's lint set. The lesson is not "run clippy too" -- it is that a named gate command is the thing to run, and a proxy for it establishes nothing about the gate. Verified by running the gate command itself rather than a proxy: CLIPPY_STATUS=0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
… cannot decide v1.compiler.parse stamped type REFERENCES as TypeOccurrence and never stamped a type DECLARATION as one. Measured over dag/std (142 files) the production transport carried 9672 TypeOccurrence references and ZERO TypeOccurrence declarations, so every type reference in the corpus was UNBINDABLE -- not mis-bound -- because occurrence_binding_resolve admits a TypeOccurrence reference against a TypeOccurrence declaration only. Every existing fixture stayed green through that because each hand-builds its declarations with `category: TypeOccurrence` -- the shape production never emitted -- so the suite supplied the missing side of the join itself. Those fixtures are correct about the authority's logic and nothing here weakens them; they were never SUFFICIENT, and nothing in the tree said so. THE PARSE TREE CARRIES NO POSITIVE TYPE-DECLARATION MARKER. The parser dispatches on the `type`/`fn`/`data`/`service` keyword and then discards which one it saw: Node has no item-kind field, so the kind survives only as which optional fields happen to be absent. A bare predicate over three absent fields fails open by construction at the parser, so the rule is written as an exhaustive ParsedModuleItemKind match whose ModuleItemUnrecognized arm REFUSES with a located diagnostic rather than defaulting into the type bucket (DESIGN section 5: a failure arm refuses, never widens). The terminal fix is a construction, named in the annotation: parse constructors carry the kind they already know, at which point the emit-side shape predicates dissolve into it. Enrolled with a PRODUCTION-FED control -- not another hand-built transport -- whose third conjunct is the state that was red before this change: a subject with type references and an empty declaration side. It executes on no required run (the required floor's source roots are dag and src/v2, and this subject is only reachable through v1.compiler.parse); rung mitigatable, next-rung trigger stated in the file. Scope, so the next increment is driven by measurement: MODULE-LEVEL type declarations only. Coproduct variants and type parameters in type position stay unstamped, and MethodOccurrence stands at 382 references against 0 declarations -- an independent gap in the same collector. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
…p stamping resources as types
THE CENSUS NOW HAS AN OUTER STATE, and building it found a live fail-open in the
change that introduced it.
TypeOccurrenceBindingCensusOutcome = CensusUnavailable { cause:
ProductionTypeDeclarationPopulationUnestablished } | CensusReady {
joined_declarations }. The thirteen classes are constructible inside CensusReady
and nowhere else. Before the stamping landed, Y never RECEIVED a declaration
population, and reporting that as OldBinds_NewUnresolved turns PRODUCER ABSENT
into a SEMANTIC RESOLUTION ANSWER -- a partition that closes over an absent input
closes over nothing.
CensusReady is constructible only after an exact-set join at OCCURRENCE-ID grain,
with uniqueness on both sides and no extra members. Not count equality, which a
compensating pair of errors satisfies. The join is against an INDEPENDENT reader:
v1.compiler.emit_core_support decides "is this item a type declaration" from
CONNECTIVE, PARAMS and CHILDREN, while the stamper decides it from the ABSENCE of
body, transport and type annotation. Different facts about the same item, so
agreement is evidence rather than measure() == measure(). New parse-only mode
`--establish` answers the obligation over the whole corpus at parse cost.
WHAT IT FOUND ON ITS FIRST RUN. Over dag + src/v2 + src/v1, exactly one diverging
module and three items: Filesystem, Clock and Entropy in std.resources. A
`resource` carries no body, no transport and no type annotation, so the
three-negatives rule stamped all three as TYPE DECLARATIONS, silently, at the
parser. The refusal arm could not fire: a resource is not merely unrecognised, it
is INDISTINGUISHABLE from a type under that rule. The parser's own item error
names TEN keywords -- alias, type, fn, func, service, resource, data, extern,
pattern, interface -- so the four-kind premise was wrong and its falsifier was in
the same file. Fixed with a ModuleItemResource arm keyed on the properties the
resource grammar attaches; the corpus-wide join now reports CensusReady.
Recorded in the annotation as a class and not a specimen: a discriminator built
from ABSENCE is only as complete as the enumeration of kinds it was derived from,
and it fails silently toward the DEFAULT BUCKET rather than toward the refusal
arm, so the refusal reads as coverage and is not.
TWO INSTRUMENT DEFECTS CAUGHT BEFORE BEING REPORTED AS PRODUCTION ONES, both
named in the annotation. The join first read the post-typecheck item list, whose
rebuilt copies carry OccurrenceSynthetic (1077 phantom "no minted occurrence"
rows); and it compared per-file parse ids against the whole-program index, two
different id spaces (40 phantom absences).
EXPOSURE DISCRIMINATION, PRODUCTION-FED. New control: one parsed source, the same
occurrences and the same resolver; under ModuleLocalMemberExposure a module-root
declaration is ModuleExposure and a consumer-module reference is UNBOUND, under
CrossFileProviderExportedExposure it is RootExposure and the same reference
BINDS. Three identical grounding columns are the signature of an absent input,
and this is what makes that signature impossible to mistake for agreement.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
Generated mirrors resolved to ours and REGENERATED below rather than hand-merged: the merge driver refuses on generated-artifact paths by design, and taking a side there drops the other side's authority-derived bytes with no conflict. The census bin's add/add is main's earlier copy of the same file (landed by #10159's squash) against this branch's later evolution of it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
… regenerated on the merge
CENSUS OUTER STATE IS NOW THREE, because two conflated two different facts.
"The join agrees on today's tree" and "the classifier is a durable authority" are
not the same claim, so:
CensusUnavailable { DeclarationDomainAbsent | DeclarationDomainDisagrees }
CensusObservedOnCurrentTree { joined_declarations }
CensusAdmissibleForCut { parser_carried_item_kind, joined_declarations }
DeclarationDomainDisagrees CARRIES the missing and extra sets, so a resource
silently stamped as a type reads as a typed, located cause rather than a generic
unavailability. CensusObservedOnCurrentTree is enough to scope work and discover
disagreements. CensusAdmissibleForCut is UNCONSTRUCTIBLE on this tree and is
modeled anyway: the alternative -- leaving the distinction unmodeled -- is exactly
what would let "the join agrees" be read as "the cut is authorized". Its arm
refuses rather than falling through, so nothing quietly starts answering for it.
THE RECOGNITION RULE, carried into the annotation in the words it was ruled in:
A RESIDUAL REFUSAL DOES NOT PROTECT A CLASSIFIER WHOSE ACCEPTED BUCKET IS DEFINED
BY ABSENCE; A NEW KIND CAN SILENTLY RESEMBLE THE DEFAULT. ModuleItemResource
repairs the KNOWN collision and does not turn absence into a positive authority,
which is why the parser-carried item kind is required before anything is cut over
on this classifier rather than being an improvement to schedule later.
SEED MIRRORS REGENERATED ON THE MERGE, not hand-merged. Resolving the generated
conflicts to "ours" dropped main's authority-derived bytes and produced a stage0
crate whose root referenced modules that no longer existed there -- the four build
errors CI reported. The mirrors here are emitted from the merged authority. Two
rounds, as separate invocations with source roots on each: required-regen
first_generation_equal=true (155/155/155, main.rs declared divergent) then
required-regen-fixed-point fixed_point_equal=true. One round can report success
while the old content still stands.
AN OPEN INCOMPLETENESS, REPORTED RATHER THAN SWEPT, and the gate is what surfaced
it: over the merged corpus the join no longer closes. 202 grammar-owned type
declarations across 100 modules -- ArgvCommand, NozzleDiameter, BuildEnvelope and
others, all genuine type names in files main introduced -- are read as type
declarations by the emit-side reader and are NOT stamped. The census therefore
reports CensusUnavailable { DeclarationDomainDisagrees } and refuses to print a
partition, which is the behaviour it was built for. Which reader is right for
these shapes is NOT yet determined and is not guessed at here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
…ass both polarities came from
THE RESOURCE ARM I ADDED TO FIX THE FIRST FAIL-OPEN CREATED THE SECOND ONE. It
keyed on `properties` being non-empty, and `type X sole_constructor { .. }`
carries a property too -- so 202 sole-constructor type declarations across 100
modules classified as RESOURCES and vanished from the declaration population.
Over-stamping resources as types, then under-stamping types as resources: same
classifier, opposite polarity, one root -- an absence-and-presence heuristic
standing where a positive kind belongs.
THE EXCLUSION IS COMPLETE BY ENUMERATION OF MINTING SITES, not by grep. Module
items have exactly two property sources in v1.compiler.parse:
parsed_sole_constructor_properties, which mints one field-init named
sole_constructor and is the only source every type-item constructor passes along
(four call sites); and parse_resource_entries. `nominal_opaque`, the other
authored type modifier, is dropped lexically by drop_leading_type_modifier and
mints nothing. mint_parsed_optional_int_property is confined to nested
where-predicate nodes and never reaches a module item's own properties. So the
modifier set mintable as a property on a type declaration is a CLOSED SET OF ONE.
A one-member set established by construction is worth more than a longer list
found by search -- and the annotation states what breaks it: a second modifier
that MINTS a property reintroduces this silently and in the same direction, which
no longer list can prevent.
MEASURED, corpus-wide over dag + src/v2 + src/v1 with
`type_occurrence_binding_census --establish`: modules_diverging 100 -> 1, absent
declarations 202 -> 2, zero extras, zero duplicates, zero index absences, zero
parse failures. Both remaining absences are in the one diverging module.
THE RESIDUE IS NOT THIS CLASSIFIER'S DEFECT AND IS FILED RATHER THAN REPAIRED.
`resource Network` and `resource AuthContext` declare no capabilities, so with no
children, body, params or connective they satisfy
v1.compiler.emit_core_support is_bare_leaf_item and the INDEPENDENT reader calls
them type declarations. That is the same class in a different authority;
repairing it there is a separate subject and is not smuggled into a parser change.
AND THE COUNTERMEASURE, which is the transferable part. Those two were invisible
while one classifier answered, because both readers AGREED they were types -- the
agreed-wrong pair a disagreement census cannot see by construction. Splitting the
question across two INDEPENDENTLY DERIVED readers converted their agreement into
a disagreement, which is the only form the census can report. Filed as
gunbc.recurring_failure_mode absence_classifier_default_bucket with both
polarities, both specimens, and the rule: WHERE A CENSUS COMPARES TWO READERS, A
THIRD INDEPENDENTLY-DERIVED READER IS THE ONLY THING THAT CAN FALSIFY THEIR
AGREEMENT.
Receipts: required-regen first_generation_equal=true 155/155/155 (main.rs
declared divergent); generated_artifact_gate main_wet for the ledger projection;
clippy --all-targets -D warnings clean; fmt clean.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
…dger conflict exposed RESOLVED BY CONSTRUCTION, NOT BY EDITING MARKERS. The two sides of gunbc.recurring_failure_mode add DISJOINT rows -- this branch adds absence_classifier_default_bucket, main adds instrument_output_read_as_subject_content, non_execution_undifferentiated_by_what_it_silenced and authority_merges_unprotected_while_its_projection_is_guarded -- and no row is edited by both. So main's file was taken WHOLE and this branch's single row re-applied by insertion. Main's 69 rows are byte-identical by construction rather than by inspection, and no conflicted line was ever opened. That matters on this carrier specifically: one row is one line, the longest is 16,792 characters, and hand-composing a markered line of that size loses content no diff view would show. VERIFIED BY IDENTITY, NEVER BY COUNT OR RC. Authority 69 rows -> 70; the main-missing-from-mine set difference is EMPTY. Projection grepped by identity string -- not by heading count, which is silently null on this file since it carries no `###` markers at all -- and all five rows in play are present. docs/design-failure-modes.md was NOT hand-resolved: it is regenerated from the merged authority, which is the only correct move on a driver-bound path. THE NEW ROW: green_reported_over_a_population_the_instrument_does_not_own. `--required-regen` reports first_generation_equal=true 155/155/155 while docs/design-failure-modes.md is STALE, because the ledger projections belong to a different actuator (generated_artifact_gate main_wet). A lane can file a row, run the regen, see green, and stop -- having shipped a row that exists in the authority and nowhere a reader can see it, since DESIGN.md points readers at the projection. Filed with its two neighbours cited and the distinction stated: same denominator shape as incidental_denominator_as_wall with the SIGN REVERSED (theirs a filter that accidentally CREATES safety, so nothing is wrong today and the protection is uncredited; this one accidentally DESTROYS coverage while reporting green, so something IS wrong today and the assurance is credited but absent), and distinct from authority_merges_unprotected_while_its_projection_is_guarded, which is merge-time and repaired by binding the driver to the authority path. IT CARRIES ITS AUTHOR'S OWN INSTANCE OF ITSELF, recorded rather than quietly dropped: within the hour of filing it, this author polled one branch for six minutes, saw no CI run on a merge-conflicted head, and reported that GitHub never creates runs for such a head. Three other DIRTY pull requests were carrying six and seven check-runs each. Recency separated the population; dirtiness did not separate it at all. An instrument's SILENCE read as a fact about a population it never enumerated -- this row's own shape with the sign flipped, and DESIGN §5 names the tell in advance, since "never" is the word that lets a ratchet pass as a wall. Receipts on the merged tree: generated_artifact_gate main_wet exit 0; required-regen first_generation_equal=true 155/155/155 (main.rs declared divergent); required-regen-fixed-point fixed_point_equal=true. .gitattributes byte-identical to main, so the generated-artifact driver bound as intended. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm
Contributor
|
Closing: this PR has nothing to add and resolving its conflict would be actively harmful. This is the auto-opened PR for Verified before closing:
So the correct action is to close, not to rebase-and-push. Following the dashboard's "resolve the conflicts and push" instruction here would have re-proposed other people's work for reversion — the surviving-branch-after-squash-merge hazard. The lane is complete and closed; no further work is intended on this branch. — sent from deep-lark-560 |
Contributor
|
Correcting my own comment above: closing was right, but the mechanism I gave for it was wrong. I wrote that merging this would revert five other lanes. That is false, and the error was the instrument. I used a two-dot Measured properly, with So the merge would delete nothing and revert no one. It is also not quite inert, which is the one thing neither characterisation caught. Because #10166 was squash-merged, the branch re-proposes rows main already has, and the merge result duplicates two ledger rows: with the roster still naming each once. Two multi-kilobyte rows duplicated in the authority, rendered twice in the projection — a §3 single-authority defect, not a destructive one. So the corrected picture: closing is hygiene, not urgency. The genuinely dangerous shape is a branch ahead from a stale base, which carries old content forward over newer; this one is behind and already merged. Same auto-PR symptom, opposite risk — and neither the PR's file count, the two-dot diff, nor the conflict nag distinguishes them. Only the merge-tree result does. — sent from deep-lark-560 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
deep-lark-560.Pushing to
session/deep-lark-560-type-decl-stampadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan