Repository navigation
The candidate index built once, then revalidated the whole transport per reference - #10159
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
What the instrument found when it was finally able to run, and the control that makes it a diagnosisThis PR is a cost repair and stands on its own. But the reason it was written is worth recording here, because the first thing the repaired instrument measured is a finding about the authority this repair sits inside. Over The discriminating control is that all three exposure groundings returned byte-identical partitions. The cause, confirmed by execution rather than by reading source ( The existing fixtures cannot see this, and that is the class. Those fixtures are not wrong and nothing here weakens them. They test the authority's logic correctly. They were never sufficient, and nothing in the tree said so. This does not change what this PR does. It is recorded here because the repair and the finding came from the same run, and because the instrument added here is what re-derives both. |
…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
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
The defect
std.occurrence_binding_candidatesresolve_reference_via_structural_candidatesdocuments that it builds the candidate index exactly once per transport, and it does. Per reference it then calledstd.occurrence_binding_resolveresolve_reference_occurrence_binding, whose first act isoccurrence_transport_validateover 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 × population).
Measured in both directions, same subject
The census instrument added here, resolving
dag/std— 142 files, 9672 type-occurrence references:Re-derive with the instrument rather than quoting these numbers (DESIGN §6 — name the instrument, never transcribe its output):
Why this is not a cache
occurrence_candidate_index_buildalready validates exactly once and already held the wholeValidatedOccurrenceTransport. It keptentries_by_idand discarded the other four fields — which is precisely what left the resolver unable to hand a validated transport down, so it rebuilt them per reference.OccurrenceCandidateIndexnow carries theValidatedOccurrenceTransportitself.entries_by_idis reached through it, so there is no second copy to drift — this is strictly fewer representations of one fact than before. That is DESIGN §2's demand-graph move (carry the value to the shared ancestor), not a memoization, and DESIGN §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
std.reference_binding_observationstructural_binding_resolution_from_candidateshad the identical shape — build the index (which validates), then call the unvalidated entry. Repaired with it, because one fact with two homes is what lets a repaired path sit beside an unrepaired one answering the same question, and the next author picks whichever they read first.The
transportparameter is removed from both entry points rather than left unused: a second unvalidatedOccurrenceTransportbeside 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.resolve_reference_occurrence_binding(the public single-transport entry) is deliberately unchanged — its existence was never the defect, and witnesses that hand it a raw transport are its correct callers.Evidence
Behaviour is preserved by the existing witnesses, which is why this carries no new behavioural test.
resolve_type_reference_containment_bindingandstructural_binding_walkkeep their signatures, sotest.claim.type_reference_containment_binding_witness_test,test.claim.type_reference_binding_context_witness_testandtest.claim.occurrence_binding_candidates_witness_testassert the same bindings through the changed code. What changed is cost.Stage0 mirror regenerated (
claim_executor --required-regen); the emitted drift is exactly the two affected files and nothing else.Why it is its own PR
Found under the XL-0T cutover, deliberately not bundled with it. 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.
The instrument
type_occurrence_binding_censuscompares, per type occurrence, what the module-wideTypeEnvpath binds against what the containment authority binds. It refuses if its class totals do not sum to its denominator, and it prints its own limits with its numbers: the X column is the post-rewire persisted env (pre-rewire inference answers unmeasured), it is a two-reader comparison and not correctness evidence, and the undecided fraction is part of the denominator.🤖 Generated with Claude Code
https://claude.ai/code/session_01KLXA6u6f3UK8PR5VEJoUwm