Repository navigation
PrimitiveIdentity join: one identity per primitive across registry, PrimitiveContract rows, algebra templates, interpreter dispatch and emit handlers - #8964
Merged
Conversation
…genuinely two: ask once, keyed on the declaration The fact "this primitive is served by the host" is carried in three forked places -- builtin_function_registry on the typecheck side, the interpreter dispatch tables on the runtime side, X_host_binding rows on the declaration side -- so a resolver collecting call candidates cannot tell two authorities for one concept from one concept with a declared realization. gunbc#8952's wall refused 1215 sites across five names for exactly that reason. This lands the single authority to ask, keyed on std.decl_ref DeclarationRef (the namespace layer's own declaration identity -- no new identity type is minted) and total over every declaration: primitive_projection_for_declaration(declaration) -> PrimitiveProjectionAnswer ProjectionFidelity = HostRealizedSeam | ModeledProjection | DivergentProjection Three fidelities rather than a boolean suppress, because the five names are three classes and a boolean would have had to put map_get somewhere: suppress it and the only real finding in the 1215 is erased, refuse everything and the wall stays unlandable. Each row was established by READING the declaration -- a seam's whole body is a self-call, a modeled projection has a real body the builtin arm intercepts ahead of, and map_get's declared Outcome<Optional<V>> diverges from the primitive's Optional<V>. Also lands the opposite direction, which the projection query is blind to by construction: primitive_runtime_coverage answers whether any runtime-bearing surface row joins a symbol at all -- the class gunbc#8952 found in emit_map_has by probing. It reports a census fact, not an adjudication that no runtime exists, and says so. And replaces the prose open denominator with a counted one: PrimitiveSymbolDisposition at symbol grain, so the distance to the roadmap node's terminal bar is a number the next session re-derives rather than a sentence. Population-wide closure across all five surfaces stays open and stays that node's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016fLASFswmgC58ucKFMqfYc
… both absence arms Two arms of this carrier spelled absence-of-observation while reading as observation-of-absence. Both were requested by gunbc#8952, which consumes this carrier, and both are correct independently of that consumer. THE PROJECTION QUERY. DeclarationProjectsNoPrimitive carried two meanings: "no primitive-bearing surface carries this name, so no builtin co-candidate can exist" and "a surface does carry it and nobody has classified this declaration". Those have opposite repairs -- the first is closed at a call site, the second by disposing a symbol here -- and at a candidate-resolution wall the ignorance arm lands on the REFUSING side. Measured: 13 disposed against 196 undisposed, so the collapsed answer would have manufactured 196 refusals from a join whose entire purpose is to remove them, and it would have looked sound from both ends. DeclarationPrimitiveUndisposed is now a third arm of the same total answer, so the collapse is unrepresentable at the boundary rather than merely agreed between two sessions that will both be archived. The discrimination is DERIVED -- it asks whether the census carries the declaration's name -- so it stays right as the population grows. THE RUNTIME-COVERAGE QUERY, the same split one layer down. NoRuntimeRowOnAny- Surface measured "the rosters do not enumerate this" and read as "nothing runs it". Renamed to RuntimeRowAbsentFromEnumeratedSurfaces, which says what it measures. to_int and with are exactly the symbols where that decides whether someone files a defect against a live method-dispatch path. Carried as a variant rather than a note, because a caveat is read later as hedging and dropped while a variant has to be named to compile. Executed: 37/37 PASS, wall 132s, resolve 1806ms, all witnesses 1073ms. New discriminating pair: list_at_optional (on no surface -> classified NoPrimitive) and to_upper (on the census, no projection row -> Undisposed). A carrier that collapsed absence answers identically for both. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016fLASFswmgC58ucKFMqfYc
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 23, 2026
…uthority The wall refuses 29 sites in the v1 seed: to_string (26, across compile.dag, dag_collect.dag, dag_collect_support.dag) against v1.compiler.emit_core_support.to_string vs the builtin, and map_has (3, in 04_infer.dag) against v1.compiler.resolve.map_has vs the builtin. These are the src/v1 residue that no dag/-rooted witness can reach and that #8964 does not cover -- now measured rather than deferred, because the wall found them. Repaired the way the diagnostic asks and at the grain the defect has: four listed imports, not twenty-nine qualified call sites. Naming the authority once per module is what the wall is asking the author to do, and it preserves behaviour exactly -- the declared function is what these sites resolve to today. The call shape settles intent for to_string rather than my judgement doing it: the sites call to_string(value: x), and is the DECLARED function's parameter name (fn to_string(value: Int) -> String). A labelled call names its callee. map_has is behaviourally identical under either authority and the declared one is what runs today, so naming it changes nothing but the silence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 23, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 23, 2026
…the prose outrunning the mechanism THE JOIN (#8964, on main at 642604b) now decides whether a same-named builtin is a rival authority or the same one seen through a declaration: seam and modeled projections drop the builtin, divergent keeps both and refuses, no-projection keeps both, and UNDISPOSED drops it -- 196 of 209 census symbols sit in that last arm, and treating ignorance as an answer would scale the wall's strictness inversely with how much of the census is done. The builtin is retained only when a declared candidate positively says the two differ. PROSE CORRECTION, the load-bearing half. Level 1a was described as "a listed import names one exact declaration". It does not: authored_import_names is a Map<String, Bool>, so it carries NAME MEMBERSHIP and cannot say WHICH declaration the author meant. What the mechanism does is remove the implicit builtin co-candidate; the remaining DECLARED population still undergoes exact cardinality admission, so one visible name plus several declarations still refuses. Conservative, never silently selects the wrong declared function, and strictly weaker than the sentence I had written. An inflated sentence in a merged PR is what the next lane builds against. A boundary control pins it: a source naming to_string in a listed import AND reaching a second to_string through the closure must still refuse. If anyone later reads 1a as "the imported declaration excludes every transitive homonym", that control goes red -- the stronger rule needs an exact-binding carrier that does not exist. VisibilityUnobservable is documented as a COMPATIBILITY FALLBACK that may never serve as a resolution authority downstream: it reports that this seam cannot see source visibility, not that the author named nothing. Two over-strict assertions replaced with per-class ones. "No blocking diagnostic at all" read false for both GREEN sources, because the census compiles against live witness roots and an unrelated UnresolvedType lands in the count -- a check whose red is produced by something it does not measure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 25, 2026
…efore deciding, and stop erasing the ambiguity arm (#8952) * Callable lookup collects every admissible candidate before deciding, and the ambiguity arm stops being erased `map_get` names two callables — the registered builtin (Optional<V>) and v2.std.collection.map_get (Outcome<Optional<V>>) — and which one a bare call meant was decided by whether the consumer's transitive import closure happened to reach the declaration. One import edge added to extdeps.git moved two unrelated modules' closures and silently re-typechecked three untouched files (gap-analysis row 30; 46 files carry the same bare spelling). The three-state outcome this needs already existed and could not describe the collision, for two independent reasons: (a) The candidate set was never assembled. lookup_func_sig asked the resolved function environment first and consulted the builtin/global path only on the Unresolved arm, so a declared map_get and the builtin map_get were never co-candidates — the declared one won by short-circuit. (b) Where ambiguity was constructed, func_sig_if_resolved mapped it onto the same Absent that means "no such signature", and ten call sites read the seed's inference through it. Both are closed here. Candidates are collected per admissible level and then decided (0/1/many through the existing module_path_owner_binding_decide), with lexical scope applying first: a module's own declaration wins, the import closure and the builtin surface are ONE level where nothing ranks two answers, and the corpus census stays strictly outside both. A lone builtin still answers Unresolved so the call routes to the known-builtin bridge — the builtin is a candidate in the decision, never an answer. func_sig_if_resolved is deleted and replaced by a total projection whose two arms every site now names. Candidates carry identities (module path + declaration name, or the primitive) rather than pasted strings, because a builtin has no qualified name to paste. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the `emit_map_has` registry row: a certified callable with no runtime at any tier An independent repair, landed beside the callable-candidate wall rather than folded into it, because it is gap-analysis row 30 with the two halves swapped. A registry row types a bare call; an interpreter arm runs it. `emit_map_has` had the first and not the second, so the call typechecked clean and answered `NoSuchFunction` when evaluated. Measured by execution rather than by reading the dispatch table: a probe calling it bare through `gunbc run` refused with `NoSuchFunction`, while the same probe's `map_get` and `length` returned 7 and 3. Row 30 is a consumer's import closure CHANGING a name's meaning; this is the closure being the only thing SUPPLYING one. All 21 live call sites reach the declared `v1.compiler.infer_types` `emit_map_has` through their own closure, which is exactly what kept the row invisible: nothing was ever served by it. Deleting it costs no call site and converts a runtime `NoSuchFunction` for any future caller outside that closure into a compile-time unresolved-name refusal. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the emit_map_has deletion note to module scope: an in-body annotation is refused Only module-item grain is modeled (DESIGN 4c), and the src/v1 parse sweep refuses a block inside a declaration body. The note now attaches to builtin_function_registry and names where the row sat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist two more in-body annotations to module scope The src/v1 parse sweep refused ten annotation lines across 04_lookup and 04_infer for the same reason as the emit_map_has note: only module-item grain is modeled. Each block now attaches to the declaration it describes and names the arm inside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the emit_map_has receipt: 20 call sites, not 21 The earlier figure counted the declaration in 04_types.dag as one of its own callers -- the measure-the-name-rather-than-the-binding error this change exists to close, committed inside the receipt for it. The note records the correction rather than applying it silently. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Level 1a: a name the author brought into scope is not a collision with the builtin The row-30 incident is TRANSITIVE: dag/extdeps/git/object_store.dag names v2.std.collection zero times and reached the declaration through somebody else's edge. Collecting the builtin as a co-candidate against every visible declaration therefore refused sixteen modules that name their authority outright -- 02_parse, 03_ingest, 03_resolve, target_model among them. So the level structure gains 1a: names in type_env.source_visible_names (locals, kernel, selective imports, all-module exports) are what the author named, and the builtin surface is not a co-candidate against them. 1b keeps the incident's case, where nothing was named and the closure supplied one. This ranks what-the-author-named against what-a-closure-supplied, never one kind of callable over another: two listed imports of a name are still ambiguous, and an unlisted declaration still does not beat the builtin. source_visible_names is reused rather than a fresh visibility notion minted beside it -- infer_env's closure_independent_bare_free_call_note already gates global-bare resolution on the same map. It is resolve-time only, so an EMPTY map is ignorance rather than an answer and takes the 1a arm; the rung is per path -- refuses on resolve, silent on emit -- with the emit row's trigger being persistence onto TypedModule.type_env. The witness is rebuilt as a triple. Its RED was the listed-import shape, which is the storm rather than the defect: it would have certified refusing the v2 compiler core as correct. The RED is now transitive reach, and the listed import becomes a green control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the stage0 mirrors, and route the eleventh consumer of the erasing projection The brief named ten consumers of func_sig_if_resolved -- nine in v1.compiler.infer, one in v1.compiler.emit. There is an eleventh, in hand-written periphery rather than in emitted code: cli_run.rs imported it, which is why the emitted mirrors compiled as .dag and then failed to build as Rust. All three of its uses are inside tests that PIN the legacy ImportScoped policy and assert its first-hit behaviour -- the one place the collapse is legitimate, since an ambiguity cannot arise under that policy and the other assertion is a genuine miss. They now go through a cfg(test) helper that does the collapse locally and says why, rather than through a production projection that would erase the arm for everyone else. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reapply the eleventh-consumer fix that the mirror copy had reverted The previous commit's message claimed this change and its diff deleted it. The regen candidate tree under target/stage0-regen-candidate/src is a whole crate source tree -- it carries hand-written files like cli_run.rs through unchanged, not only the emitted mirrors -- so 'cp candidate/*.rs' restored the original over the edit. git status then showed six changed files, which is exactly what the six drifted mirrors would show, so the reverted edit was invisible in the count. Read what changed, not how many changed: the two are the same number here and they are not the same fact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the RED fixture, and stop a broken fixture from masquerading as a quiet wall The RED imported PosixUserName, which extdeps.posix.identity does not export. The source failed for an unrelated reason, produced zero AmbiguousReference rows, and the assertion read false -- indistinguishable from 'the wall did not fire'. Executed, that is exactly what it looked like. Corrected to PosixUserId, and joined by two assertions the pair could not make on its own: the RED's only blocking diagnostics are the ambiguity itself, and both GREEN sources carry no blocking diagnostic at all. A fixture that breaks for any other reason now fails loudly on those instead of returning a verdict about the wall it never reached. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The wall could not fire for its own specimen: drop the algebra-template exclusion builtin_callable_candidates excluded every algebra method template name, reasoning that receiver-dispatched names belong to the known-method ExprCall arm. Measured, that guard was redundant for the names it named and fatal for the ones it did not: of ~50 algebra template names only 19 carry a builtin_function_registry row, and filter/any/contains/fold/map are not among them, so infer_builtin_call_type already answered Absent and they were never candidates. What the guard actually excluded was the 19 names that DO have a free-call surface -- map_get first among them, the exact name row 30 is about. Executed evidence of the effect: the RED source produced VariantNotFound and NonExhaustiveMatch -- row 30's ORIGINAL symptom, the declared Outcome-returning map_get winning outright -- and no AmbiguousReference at all. The admission test is now the registry alone, which is precisely the question being asked: a registry row means a bare call to this name types against a primitive. A name without one produces no candidate anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the lookup mirror: the wall now fires on its own specimen Measured through compile_dag_diagnostic_census on the real acceptance path, with the mirrors regenerated and installed so the binary carries the change: RED (imports extdeps.posix.identity, names no authority for map_get) -> AmbiguousReference/BLOCK/map_get and the VariantNotFound/NonExhaustiveMatch that row 30 describes are GONE -- replaced by the refusal, which is the point GREEN1 (import v2.std.collection { map_get }, then a bare call) -> no AmbiguousReference; the named authority resolves GREEN2 (declares its own map_has, no path to the declarer) -> census empty Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Narrow 1a to the listed-import arm: an is_all import names a module, not a declaration source_visible_names folds BOTH import arms into one map -- is_all contributes every name in the imported module's interface AND every name that module acquired through ancestry_str_bindings. So 'import v2.std.collection' would put map_get in it without the author writing the word, and the ancestry half contributes transitively: the closure-supply case row 30 is about, arriving through a set whose name suggests the opposite. Membership there is NECESSARY for 'the author named this declaration' and not SUFFICIENT. The sufficient half cannot be recovered by filtering, because the union already happened at construction. So authored_import_names becomes its own field on TypeEnv, built from the specific_names arm alone, threaded through every literal site. Type parameters are deliberately not in it: authored, but not imports. Measured before cutting: of the modules that bare-call map_get and import v2.std.collection, all six name it in a listed import and none uses is_all, so the narrowed rule still covers the population 1a was introduced for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the 29 production collisions the wall exposes, by naming the authority The wall refuses 29 sites in the v1 seed: to_string (26, across compile.dag, dag_collect.dag, dag_collect_support.dag) against v1.compiler.emit_core_support.to_string vs the builtin, and map_has (3, in 04_infer.dag) against v1.compiler.resolve.map_has vs the builtin. These are the src/v1 residue that no dag/-rooted witness can reach and that #8964 does not cover -- now measured rather than deferred, because the wall found them. Repaired the way the diagnostic asks and at the grain the defect has: four listed imports, not twenty-nine qualified call sites. Naming the authority once per module is what the wall is asking the author to do, and it preserves behaviour exactly -- the declared function is what these sites resolve to today. The call shape settles intent for to_string rather than my judgement doing it: the sites call to_string(value: x), and is the DECLARED function's parameter name (fn to_string(value: Int) -> String). A labelled call names its callee. map_has is behaviourally identical under either authority and the declared one is what runs today, so naming it changes nothing but the silence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Wire suppression through the merged PrimitiveIdentity join, and stop the prose outrunning the mechanism THE JOIN (#8964, on main at 642604b) now decides whether a same-named builtin is a rival authority or the same one seen through a declaration: seam and modeled projections drop the builtin, divergent keeps both and refuses, no-projection keeps both, and UNDISPOSED drops it -- 196 of 209 census symbols sit in that last arm, and treating ignorance as an answer would scale the wall's strictness inversely with how much of the census is done. The builtin is retained only when a declared candidate positively says the two differ. PROSE CORRECTION, the load-bearing half. Level 1a was described as "a listed import names one exact declaration". It does not: authored_import_names is a Map<String, Bool>, so it carries NAME MEMBERSHIP and cannot say WHICH declaration the author meant. What the mechanism does is remove the implicit builtin co-candidate; the remaining DECLARED population still undergoes exact cardinality admission, so one visible name plus several declarations still refuses. Conservative, never silently selects the wrong declared function, and strictly weaker than the sentence I had written. An inflated sentence in a merged PR is what the next lane builds against. A boundary control pins it: a source naming to_string in a listed import AND reaching a second to_string through the closure must still refuse. If anyone later reads 1a as "the imported declaration excludes every transitive homonym", that control goes red -- the stronger rule needs an exact-binding carrier that does not exist. VisibilityUnobservable is documented as a COMPATIBILITY FALLBACK that may never serve as a resolution authority downstream: it reports that this seam cannot see source visibility, not that the author named nothing. Two over-strict assertions replaced with per-class ones. "No blocking diagnostic at all" read false for both GREEN sources, because the census compiles against live witness roots and an unrelated UnresolvedType lands in the count -- a check whose red is produced by something it does not measure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete tmp_census_report.dag: undeclared scaffold, and a parallel authority for the probe corpus A debugging harness I used to read the census while iterating. Right thing to have while iterating; experimental residue the moment the PR is proposed. It has no test fn, no assertion, and nothing that can go red -- and the 'tmp_' in a committed path is a statement that the author knew. The worse half is that it carried red_src / green1_src / green2_src as data rows duplicating the witness file's three sources: two authorities for the probe corpus, in adjacent files, in the PR whose subject is one name having two authorities. Whichever someone edited later, the other would silently disagree, and the scaffold has no assertion to notice. Reading a census as a string is a reasonable capability to want; if it is wanted it is a separate proposal with its own consumer, not a leftover. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rebuild the boundary control on a homonym the census can actually reach Its first version imported v1.compiler.emit_core_support -- a SEED module. compile_dag_diagnostic_census resolves against the witness roots [dag, src/v2], so that import could never resolve, no to_string candidate existed, and the assertion read false for a reason with nothing to do with the boundary. Third fixture broken this way, and this one was inside the control built to prevent a different mistake. Rebuilt on v2.std.spine int_max, whose own closure reaches std.realization_width, which declares int_max too -- so ONE listed import puts both declarations in the closure at once. No builtin is involved, because int_max has no registry row, which is what makes the row ISOLATE its claim rather than restate the RED: the declared population survives a listed import and still undergoes exact cardinality admission. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Revert four seed import repairs superseded by the primitive-identity join The 29 seed collisions these repaired now answer DeclarationPrimitiveUndisposed, so the builtin is not admitted as a rival and the refusals do not fire. The edits' stated reason no longer exists; leaving them would be residue whose justification a later reader could not reconstruct. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Witness: no symbol reaches the primitive surface through the interpreter roster alone The projection query's Undisposed arm is defined over five surfaces, one of which (InterpreterDispatch) is the only one whose authority reaches v2.*. A consumer restricted to the other four answers identically today, but only as an occupancy fact. This checks the equality rather than assuming it, and goes red naming the first interpreter-only symbol anyone adds. Rung: mechanically preventable, not structural -- the two censuses remain capable of diverging and this check is what catches it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Drop the interpreter-only-symbol guard: its precondition is false Measured 31 interpreter-only symbols, so the four-surface substitution the guard was written to license does not hold and there is nothing to guard. Keeping it would either assert something false or be re-pointed at the current count, which is a tree-copied census pin rather than an oracle. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the Undisposed->suppress arm's justification beside the arm It is a consumer-side policy choice, not taxonomy work, and an unexplained arm reads as an oversight. Refusing on an unclassified symbol would refuse 196 symbols corpus-wide: a wall whose strictness rises with how much census work remains undone is not strict, it is broken. Also records why the answer has three arms rather than a boolean -- the argument is about where the decision lives, not what the states mean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair main's broken cargo check: the hand-written probe missed SymbolIndex's new field Inherited, not introduced by the merge: on origin/main SymbolIndex declares five fields including type_head_exposures, and the hand-written peel-fixpoint probe in cli_run.rs initializes four, so cargo check --all-targets and the documented local cargo test --workspace both fail there. Neither the struct nor that probe is touched by this branch. It is the eleventh-consumer class again: the field was added to the emitted mirror, and the hand-written seed periphery that constructs the same struct is a population no .dag census reaches. The Rust suite left CI on 2026-07-11, so nothing observed it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Emitter: a call in a data initializer is a cross-ref, so it stops going to the JSON serializer data_value_has_cross_refs answers one question -- does this initializer reference another declaration -- and ExprVar was already true for exactly the right reason. ExprCall is that same reference with an argument list, and it fell through `_` to false, routing `data d: R = mk(..)` to a serializer that can only render literals. The serializer then refused with "unsupported mock expression", so the failure surfaced one layer below the judgment that caused it. TOTAL AT THE LEVEL EXAMINED, BLIND ONE LEVEL DOWN: exhaustive over expr_data, no arm missing, nothing a reviewer or a wildcard-free lens could catch -- the `_` carried the payload. Wrong by the function's own definition, not incomplete. MEASURED BEFORE EDITING, with two instruments that disagreed: line regex 1259 rows (WRONG -- blind to multi-line and to nested calls) multi-line census 3181 rows across 971 files, corpus-wide emitted mirrors 9 rows refused, all in std_primitive_projection.rs The third decides: only the seed closure is lowered to Rust, and the JSON branch is guarded by record-shaped-type AND no-cross-refs. Every row on that path today emitted successfully, which by construction means it holds no call. So nothing that works today can move. VERIFIED AFTER: JSON-path rows 34 before and 34 after -- zero existing rows changed route. The emitter mirror moved by exactly one line. required-regen reports first_generation_equal=true. Authorized as a scoped one-arm repair; the surrounding emitter is untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist the not-runnable-is-not-zero annotation to module-item grain Fourth instance of this class on this lane, and the reason I missed it is the finding: my local sweep checked src/v1/*.dag, because that is where the previous three appeared. The required-ci parse phase covers dag/ as well, and required-regen -- the only phase I can run locally in a tight loop -- does not run that parse at all. So the local verification loop cannot see this class in dag/, and I scoped the sweep to where the error had last appeared rather than to where the rule applies. Swept every .dag this branch touches, not just the file CI named: all clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
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.
What this lands
One authority that can answer, of a declaration, whether it is the modeled surface of a primitive — keyed on identity rather than on a spelling, and total.
The consumer is the bare-call candidate collector in #8952, whose first corpus run refused 1215 sites across 5 names because a modeled
stdsurface and the primitive it projects are two co-candidates with no relation between them. That is the §3 defect in its plainest form: the fact this primitive is served by the host is carried in three forked places (builtin_function_registryon the typecheck side, the interpreter dispatch tables on the runtime side,X_host_bindingrows on the declaration side, present for two names out of the population), and there is no single authority to ask.Why three fidelities and not a boolean suppress
I read the declarations rather than matching the names. The five collision names are three classes, and a boolean would have had to put
map_getsomewhere — suppress it and the only real finding in the 1215 is erased; refuse everything and the wall stays unlandable. A three-state does not choose, it distinguishes, and the residue falls out of the model instead of out of a threshold.HostRealizedSeamv2.std.decl_indexdecl_facts,export_signature_facts,data_decl_type_facts;v2.std.concept_indexconcept_decl_facts,concept_decl_facts_live;v2.std.collectionempty_map_primitive_delegatedecl_facts(pool_roots: pool_roots))ModeledProjectionv2.std.algebralength;v2.std.collectionmap_insert,empty_mapDivergentProjectionv2.std.collectionmap_getOutcome<Optional<V>>against the primitive'sOptional<V>declaration_and_primitive_are_one_authorityis true for exactly the first two.Why the first two are not one variant
They agree at the resolver — both suppress — so the distinction has to earn its keep elsewhere, and it does. A
HostRealizedSeambody is correct by construction: reaching it recurses to the evaluation-budget refusal, which is what a declared host seam should look like. AModeledProjectionbody is dead code that looks live —v2.std.algebra lengthhas a genuinefold_listbody that no bare call reaches, and someone will eventually edit it believing it runs. Different facts, different futures; averaging them would erase that. tidy-pike had this recorded as an open question in #8952 and will carry the fidelity into the advisory rather than only the boolean. Repairing the dead-code half is not claimed here.The identity key — DFS before minting
No new identity type was minted. The key is
std.decl_refDeclarationRef, which is the namespace layer's own identity for a declaration; §3 makes namespace the declaration-identity authority and its cite-the-symbol rule is literally name the module and the symbol. What I looked at before settling on it:v2.std.qualified_nameQualifiedName(FreeMonoid<Symbol>) is the v2 segment-list form and lives downstream ofdag/std, so astdcarrier keying on it inverts the direction its consumers read;std.decl_refDeclarationRefis already the carrier D0 uses, already carries a field discriminator anddeclaration_ref_eq, and its own header records that two parallel lanes minting duplicate constructors was the collision that redded this witness closure once already. Minting a third module-path-plus-decl-name pair beside it would have repeated, inside the PR whose subject is single authority, exactly the history DESIGN records forModulePath.The shape explicitly refused (operator ruling, relayed): generalizing the
X_host_binding: PrimitiveContractmarker to the ~8 declarations. It is a second representation scattered beside eachfnrather than one authority; it keys on a bare name inside a module scope so two same-named declarations collapse; and it has no room for a fidelity. Module qualification answers the second, one carrier answers the first,ProjectionFidelityanswers the third.The second direction, from #8952's own finding
The projection query is blind by construction to a primitive with no declaration. tidy-pike found one by probing:
emit_map_haswas a registry row with no runtime at any tier, typechecking clean at 21 call sites that all happened to reach a same-named declaration through their own closure. So this PR also lands the opposite question:It reports a census fact — no
InterpreterDispatchand noEmitHandlerrow on the derived five-surface census joins this symbol — not an adjudication that no runtime exists. A dispatch site the interpreter roster does not enumerate is invisible here exactly as it is to every other consumer of that roster, which is the standing limit that roster records for itself.The residue is counted, not described
The open denominator was prose. Prose has no size, so it never ranks for closing. It is now a typed disposition at symbol grain:
primitive_undisposed_surface_symbol_count()is a number the next session re-derives by running it. The witness over it deliberately asserts that the classifier is total over the census, not that the residue has any particular size: a size assertion would be a tree-copied census pin, and it would go red the day the terminal bar is reached — which is the defect the roadmap node already records against an earlier acceptance clause of this same carrier. Measured population for context (five surfaces, distinct authored symbols): registry 122, contract rows 64, algebra 87 rows / 59 names, emit handlers 57, interpreter 188 rows / 164 spellings — 209 distinct symbols over ~518 census rows.The census join now consults the declared population by canonical name after the D0 alias table. That is not a spelling rule: a symbol joins only if a
PrimitiveDefinitionfor that canonical name has been declared, so a surface growing a new symbol nobody declared staysSymbolUndisposedand is counted.What the consumer gets at merge
This carrier's claim is about what the query answers, which is executed here. It is deliberately not a claim about how many call sites a consumer's resolver refuses — that population belongs to #8952, is measured there, and has moved twice while this PR was open.
At head
1b741a705c, asking the exact query that resolver will ask. The evidence column says how each row is established, because they are not all established the same way:v2.std.algebralengthModeledProjectionv2.std.collectionmap_insertModeledProjectionv2.std.decl_indexdecl_factsHostRealizedSeamv2.std.decl_indexdata_decl_type_factsHostRealizedSeamv2.std.collectionmap_getDivergentProjectionv2.std.collectionempty_mapModeledProjectionv2.std.algebrato_upper(no row)DeclarationPrimitiveUndisposedv2.std.collectionlist_at_optionalDeclarationProjectsNoPrimitiveThe
empty_mapcaveat is small and stated anyway:w_seam_and_modeled_projections_are_one_authorityproves it is one authority, which is what the consumer acts on, but no executed assertion distinguishes itsModeledProjectionfromHostRealizedSeam. The value in the table is read from the roster literal in this diff.Every name #8952 identified as a collision is disposed and carries a row, so nothing in their merge is serialised behind further disposition work here.
An earlier revision of this section asserted site counts — "all 1161 sites resolve at merge, 1149 suppressed and the 12
map_getsites correctly refusing". Both halves were wrong and the error is worth naming rather than just deleting. The counts were #8952's, measured before their resolver gained a level-1a arm that resolves any name the author brought into scope; and themap_getsites in particular all namemap_getin an import list, so they resolve at 1a and never reach the divergent verdict at all.DivergentProjectionremains the right verdict for the symbol — what I got wrong was where that verdict gets consulted, which is a fact about the consumer's resolver and not about this carrier.The general shape: I borrowed another lane's measurement to assert a consequence in a graph I had not measured. Both halves checked out on their own; only the arrow between them was invented. This PR now states what it executed and points at #8952 for the population, which is where that authority lives.
Absence is two states, and collapsing them would have inverted this PR's purpose
DeclarationProjectsNoPrimitiveoriginally carried both "no primitive-bearing surface carries this name, so no builtin co-candidate can exist" and "a surface does carry it, and nobody has classified this declaration". Those have opposite repairs — the first is closed by qualifying a reference at a call site, the second by disposing a symbol in this carrier — and at a candidate-resolution wall the ignorance arm lands on the refusing side.The consequence is the part worth stating: the wall's strictness would have scaled inversely with how much of the census is disposed. At 13 of 209, that is 196 manufactured refusals from a join whose entire purpose is to remove refusals — and it would have looked correct from both ends. This side answers truthfully that no projection is declared; the consumer reasons soundly that an undeclared projection means two authorities. Both halves check out; only the arrow between them is invented.
So it is a third arm of the same total answer rather than an agreement between two sessions — both of which will be archived. A consumer cannot silently merge them, and every future one must name all three to compile.
The same split existed one layer down, in the runtime-coverage arm:
NoRuntimeRowOnAnySurfacemeasured the rosters do not enumerate this and read as nothing runs it. It is nowRuntimeRowAbsentFromEnumeratedSurfaces, which says what it measures.to_intandwithare exactly the symbols where that distinction decides whether someone files a defect against a live method-dispatch path. Carried as a variant rather than a note, because a caveat gets read later as hedging and dropped while a variant has to be named to compile.Raised by #8952 in review of the query shape; correct independently of that consumer.
What this does NOT claim
primitive-identity-join. Population-wide closure across all five surfaces stays open and stays that node's; the 209-symbol disposition is roughly 80 host query bridges that are not primitives at all, it is a large volume of individual judgment calls, and none of it is what unblocks CALLABLE-LOOKUP-UNIQUE: collect every admissible callable candidate before deciding, and stop erasing the ambiguity arm #8952. Scoped deliberately, on the operator's ruling, with the distance to the bar now a number instead of a sentence.ModeledProjectiondead-code class. This carrier makes it observable; fixing it is a separate lane.src/v1is touched.Evidence
The carrier is verified by execution. A local probe (uncommitted, deleted after the run) called the carrier's own functions against the live five-surface census on the tree at
d3d173dc7f:PROBE HELDmeans every one of these passed: the three fidelities answer for their named declarations (decl_factsseam,lengthmodeled,map_getdivergent); an unclassified declaration answersDeclarationProjectsNoPrimitive;map_getis not one authority whiledecl_facts/length/map_insert/empty_mapare;lengthagainstprimitive_map_insertis not one authority; the roster carries zero violations, exactly 1 divergent row and exactly 9 one-authority rows. Those two row counts are a controlled fixture — the population and the expectation are both authored in this PR — not a measurement copied from the tree.Two numbers in it were predictions I had made statically and had labelled as unverified, and execution confirmed both: the census derives exactly 209 distinct authored symbols, and
registry_no_runtime=4.registry_no_runtime=4is a CANDIDATE SET, not a defect count, and it should be quoted as one. The four areemit_map_has,Some,to_int,with. What the carrier measured is that noInterpreterDispatchand noEmitHandlerrow on the derived census joins these symbols — it did not establish that they have no runtime. A method-dispatch site the interpreter roster does not enumerate would look identical here, andto_intandwithboth have contract rows and algebra templates, so they are exactly the shape that could be perfectly live.Someis a constructor spelling. Onlyemit_map_hasis an established defect, and it was established by #8952's probe, not by this count — the value of reaching it here is convergence: two instruments of independent construction, one probing the runtime and one reading the census, returning the same specimen. That is a receipt that the mechanism generalizes; it is not a licence to read the other three as findings.disposed=13 / undisposed=196is the counted residue against the terminal bar, and it is the number this PR exists to make readable.All 35 witnesses pass.
claim_batchover both entry groups under one prepared subject — the 19 new witnesses plus the 16 existing D0/D1 witnesses, run as a regression check because this PR rewires the census join:37 = 21 witnesses in the new file + 16 existing D0/D1 witnesses run as a regression check, because this PR rewires the census join. The new discriminating pair for the absence split is
list_at_optional(carried by no surface → classifiedNoPrimitive) againstto_upper(on the census, no projection row →Undisposed); a carrier that collapsed absence answers identically for both, so one of them reds.Per-witness cost is 0–119ms; the most expensive is
w_every_census_symbol_lands_in_exactly_one_disposition_armat 119ms, which derives the whole five-surface census. The run's own cost partition attributes 49.8s of its 51.6s to building the whole-tree bare-reference edge index once (edge_index_tree_census34.4s over 3881 source files) for declarer discovery — a fixed preparation cost unrelated to this change, which the required floor pays once across every witness.A correction, recorded rather than silently edited, because I published this claim wrong twice in opposite directions.
An earlier revision of this section said a standalone
claim_batchrun "takes over an hour per invocation" and blamed the instrument. A later revision retracted the two-minute figure as unreproducible. Both were wrong, and the same mistake produced both. I was readingps -o etimeasHH:MM; it isMM:SSunder an hour. Confirmed against a control: a process slept for a clock-measured 75 seconds reportsetime=01:15,etimes=75. So every "hour-plus" figure I reported was a run of one or two minutes, and the compounding error was that I had no clock on the wall time between my own observations and assumed successive readings were minutes apart when they were seconds apart.The measured facts, by
date +%saround the invocation rather than by readingps: a full run of both entry groups completes in roughly two minutes, of which ~30s is the one-time whole-tree graph-facts build. The compiler's own instrumented spans — 1755–1857ms of entry resolve, ~1s for all witnesses, 0–119ms each — were consistent across every run and were the defensible numbers the whole time. There was never a cost problem in this change, and there was never a cost problem in the tooling. There was a misread format.I am leaving this here at length because the failure shape is the reusable part: three successive conclusions (the run blew its timeout, my census functions were 15x cost, the tooling is inherently slow) were one bad instrument reading wearing three explanations, each moving the cause one layer outward without ever questioning the measurement. When a second explanation is needed to rescue the first, stop explaining and re-measure the baseline with a different instrument.
Two defects found and fixed in this PR's own witnesses
Named here rather than left invisible because they never shipped. Both are the kind that pass review, since a green test reads as evidence.
An inverted red. The residue witness originally asserted
undisposed > 0. That red is not merely unreachable — it is inverted: it goes red on the day the work succeeds, silently converting the roadmap node's terminal bar into a permanent obstacle. It was written into the same carrier whose roadmap node already records that exact defect against an earlier acceptance clause of itself, so this is a class recurring inside the file that documents it. The witness now asserts that the disposition classifier is total over the census and says so in a comment, and no size assertion is made anywhere.A
measure() == measure()partition.divergent_row_countanddisposed_symbol_countwere each computed by subtracting from a total, so the partition witnesses over them restated the definitions of their own operands — the change-detector shape DESIGN's oracle rule names. Both are now independent filter counts, and the one surviving sum assertion tests that the classifier is exhaustive rather than that arithmetic works.Rung
Mechanically preventable for the projection class: the invalid states (a projection naming an undeclared primitive, two projections for one declaration) are detected by executing detectors with discriminating REDs, but both remain writable. Next-rung trigger: deriving the roster from the declarations rather than authoring it beside them, which needs declaration introspection over
.dagbodies — the same triggerprimitive_contract_roster_notealready carries.