Ground primitive arity and parameter types on the semantic contract, by projection

[gunbai-bot]

The mechanism this closes half of

src/v1/04_lookup.dag func_sig_from_global_bare has two arms that return FuncSigUnresolved before doing anything: one when algebra_method_template_name(name) is true, one when infer_builtin_call_type(name) is Present. Every symbol in registry-∪-algebra — 169 distinct names — therefore can never yield a ResolvedFuncSig. No ResolvedFuncSig means no formal/actual application plan, and direct_call_arg_mismatch_diags / direct_call_shape_diags in 04_infer.dag run only over that plan.

So those 169 are not merely unchecked. They are structurally unreachable by the one wall that would check them. #9024 closed the type-application arm of this same hole from the other side; this is the callable-signature arm, and it is shut by construction.

The reason it is shut is that nothing said what a primitive takes. This PR grounds that fact. It does not open the arm — see Rung below.

What landed

std.primitive_identity PrimitiveSemanticContract carried exactly one field, canonical_name. It now carries a signature grounding:

• PrimitiveSignatureGrounding = GroundedInAlgebraTemplate { profile } | SignatureUngrounded { reason }
• PrimitiveSignatureResolution = SignatureResolved { parameters, result } | SignatureAmbiguousOnProfile | SignatureAbsentFromProfile | SignatureNotGrounded
• primitive_signature — total over every contract
• primitive_arity — derived, parameters |> count
• algebra_grounded_semantic_contracts — the population, derived, zero authored rows

std.primitives PrimitiveContract is not touched.

Why not PrimitiveContract, which the work item named

Every one of its five fields is a cost field, and gunbc.roadmap_authority primitive-identity-join rules verbatim: "PrimitiveDefinition (identity + PrimitiveSemanticContract), PrimitiveInvocationSurface, PrimitiveRealization per RealizationTarget, PrimitiveCostFact, and PrimitiveTraversalOrderFact — five separate carriers joined by PrimitiveIdentity, never one mega-row." Grounding the type half on the cost row is that mega-row. PrimitiveSemanticContract already existed, already sat under PrimitiveDefinition, already had PrimitiveCostFact separate beside it, and carried one anemic field. This fills a carrier declared for this and left hollow; it does not author a fifth. (Operator ruling, after two lanes reached the same conclusion independently.)

Projection, not a copy — and the measurement that decided it

The signature half already exists for part of the population, on std.algebra AlgebraFieldTemplate.param_types. A second param_types here would answer "what does map take" from two sets of bytes — the §3 fork this change exists to remove. Two admissible shapes; measured:

	bytes moved	consumer sites touched
Projection (contract keys into algebra)	0	0
Migration (signature half moves here, algebra reads back)	88 authored param_types occurrences	49 — 43 in 04_infer.dag, 4 in 04_types.dag, 2 in 04_lookup.dag

All three migration targets are load-bearing pipeline stages, so it is a stage0 regen on top of a root-cut replacement migration. Projection. The contract carries a key; every parameter fact is read back through primitive_signature.

The finding that shaped the key: name → signature is not a function

A name-keyed projection was considered and refused on measurement. Over the 90 AlgebraFieldTemplate rows (post-merge with main; see Merge below):

• 23 of the 59 distinct names carry more than one template row.
• Several disagree in param_types: join, member, contains, get.
• member disagrees in arity outright — [ReceiverSelf, ReceiverElement] on FinitePowerSet (arity 2), [CallableOf{…}] on PointwisePower (arity 1).
• get takes NamedTemplate{Int} on the List profile and ReceiverKey on two Map-shaped profiles.
• join carries three distinct signatures across three profiles.

These are not duplicates to dedup. They are receiver-polymorphic operations: get on a List takes an index, get on a Map takes a key, and both are correct. A projection keyed on canonical_name alone would have had to pick one silently — the last-import-wins class this compiler already carries as a confirmed structural hole. So the key is (canonical_name, profile), which is not new vocabulary: roadmap_authority already models it as InvocationForm MethodCall { receiver_domain }, and AlgebraProfile is the existing closed enum that names it.

Anyone tempted to "simplify" the key back to a bare name should find this paragraph rather than rediscover it through a wrong answer. Two witnesses go red if they try.

Population: the ruled 59 algebra-known names resolve at their true grain to 90 (name, profile) rows. 87 is what 59 is once a spelling stops standing in for an identity. It is still enumeration by the primary structure with no hand roster — derived by mapping all_algebra_field_templates(), zero rows authored.

Witnesses, and the one I was asked for and did not write

The brief asked for a witness joining the contract's parameters to the algebra templates and refusing on disagreement. Under projection there is one set of bytes, so disagreement has no spelling — such a check would be permanently green by construction, which §4b names as worse than absent because it gets cited as coverage. It is not here. (Operator concurred; the two asks contradicted each other.)

What is here has authorable REDs:

• w_every_algebra_grounded_contract_resolves_a_signature — totality. RED: a grounding naming a (name, profile) pair with no template.
• w_derived_population_is_exactly_the_algebra_template_population — the denominator as a self-denominating identity (derived count == all_algebra_field_templates() |> count), both sides read from the one authority. RED: a derivation that drops a profile.
• w_every_row_of_a_controlled_fixture_resolves_to_its_authored_arity — non-vacuity as a controlled fixture: three hand-authored rows with hand-authored expected arities, plus an absent name. Input and expectation both authored here, neither measured from the tree.
• w_every_declared_grounding_still_resolves_or_says_ungrounded — the hand-authored groundings must resolve or say NotGrounded; Absent/Ambiguous means someone typed a (name, profile) pair upstream no longer honours.
• w_get_takes_an_index_on_a_list_and_a_key_on_a_map, w_member_has_a_different_arity_on_each_profile — the polymorphism regression controls.
• w_a_name_absent_from_its_profile_refuses — the absent arm.
• w_two_templates_of_one_name_on_one_profile_refuse + w_one_template_of_one_name_resolves — the ambiguity arm and its positive control, so a resolver that refused everything would not pass.
• w_an_ungrounded_contract_has_no_arity_not_zero + w_a_nullary_primitive_reports_arity_zero — the discriminating pair. A resolver fabricating 0 for an unresolved signature passes every other claim and fails these two.

On the ambiguity arm, examined rather than assumed

I originally justified its RED as "plant a name-only grounding". That justification was wrong, and the operator was right to press it: GroundedInAlgebraTemplate structurally requires a profile, so a name-only grounding has no constructor and no fixture can author one. The ambiguous collapse by name-keying is therefore structurally impossible, not detected — a higher rung than a wall.

The arm survives because it guards a different class: two rows of one name on one profile. Measured, zero duplicate names within any of the eight profiles today — so it is unoccupied. But the mechanism is live (the template lists are hand-authored, a repeated row is writable) and it is join-reachable (the resolver folds over exactly that list). That is a quiet guard, not a dead one. algebra_signature_from_candidates takes its candidates as a parameter precisely so a fixture can plant the duplicate; that factoring is a correctness requirement, not style.

Arity is derived and has no field anywhere in the module. An unresolved signature has no arity rather than a guessed one: Absent, not zero, because a nullary primitive and an unresolved signature are different facts.

Rung

Nothing here moves the class off mitigatable. The class — a host primitive call binds arguments in no bijection and at no declared type — sits below the floor, because §4b names exact-bijection binding as ordinary floor, and populating a carrier leaves it there. What this PR establishes is that the semantic contract now carries arity and parameter types for a declared population, derived from one authority; nothing consumes them.

Next-rung trigger: func_sig_from_global_bare answering FuncSigResolved for a primitive from this contract, so the 169 reach the existing direct_call_arg_type_mismatch plan rather than a second wall built beside it. That is the next PR and it is the one that actually climbs; it is a load-bearing 04_lookup/04_infer change needing a stage0 regen and is deliberately out of scope here.

Boundary: source → .dag acceptance only. Emission is unmeasured by this change.

The witnesses prove the two surfaces are one authority and that the projection is total and unambiguous. They do not prove any call is checked.

Executed

Measured on BuildBuddy (linux/amd64), release gunbc built from this branch's working tree, 2026-08-24.

Compile — gunbc compile --source-root dag --source-root src/v2, both entries:

entry	rc	result	severity
dag/std/primitive_identity.dag	0	38 files emitted, 38 diagnostics	38 advisory, 0 blocking
dag/test/claim/primitive_signature_grounding_witness_test.dag	0	39 files emitted, 38 diagnostics	38 advisory, 0 blocking

Every diagnostic is the pre-existing where-refinement unenforced … non-literal value at refined position class (std.content_hash, std.decl_ref, and six sites already in primitive_identity). This change adds one more of that same class, at the t.name as NonEmptyStr in the derived population — the established corpus idiom for that cast.

Witnesses — gunbc run … --claim-run, eleven of eleven:

PASS w_every_algebra_grounded_contract_resolves_a_signature
PASS w_derived_population_is_exactly_the_algebra_template_population
PASS w_every_row_of_a_controlled_fixture_resolves_to_its_authored_arity
PASS w_every_declared_grounding_still_resolves_or_says_ungrounded
PASS w_get_takes_an_index_on_a_list_and_a_key_on_a_map
PASS w_member_has_a_different_arity_on_each_profile
PASS w_a_name_absent_from_its_profile_refuses
PASS w_two_templates_of_one_name_on_one_profile_refuse
PASS w_one_template_of_one_name_resolves
PASS w_an_ungrounded_contract_has_no_arity_not_zero
PASS w_a_nullary_primitive_reports_arity_zero

Discriminating REDs, executed:

RED 1  stale hand grounding (revert map_keys/map_values to PartialFunction — the REAL upstream move)
       FAIL w_every_declared_grounding_still_resolves_or_says_ungrounded
RED 2  derivation drops a profile (all_algebra_profiles() |> skip(1))
       FAIL w_derived_population_is_exactly_the_algebra_template_population
RED 3  controlled fixture expectation (arity:2 -> arity:3)
       FAIL w_every_row_of_a_controlled_fixture_resolves_to_its_authored_arity
RESTORED  all three PASS

Also re-run after the merge, because I edited a main-side fixture whose whole purpose is a planted RED — a change that quietly greened it would be worse than a compile error:

PASS determinism_denominator_is_closed_on_declared_primitives
PASS determinism_denominator_predicate_finds_a_planted_hole

One fail-closed receipt from the change itself. signature is a required field, so adding it made every one of the 12 PrimitiveSemanticContract construction sites refuse until each declared a grounding. The deletion-is-the-census property worked in the additive direction: nothing could silently keep a signature-less contract.

What was NOT executed: the witness floor (claim_executor) and emission. Boundary is source → .dag acceptance, as stated above.

Denominator honesty

The population is not closed, and no number here should be read as completeness.

• 64 data *_contract: PrimitiveContract rows; primitive_contract_roster has 64 entries. 64/64 is agreement between a roster and its rows, not a universe.
• Union across the five surfaces the roadmap names: PrimitiveContractRow 64, BuiltinRegistry 130, AlgebraTemplate 59 distinct over 90 rows, InterpreterDispatch 164 distinct spellings over 189 arms, EmitHandler 57 → 218 distinct authored spellings.
• 218 is an UPPER BOUND at spelling grain, not a primitive count: aliases collapse (length/count/size are one interpreter arm with three spellings) and spellings fork (fold vs fold_list are separate surfaces that can disagree).
• 64 of 218 spellings have a contract row; 154 have none; 159 have no arity fact anywhere.
• 12 contract rows name a symbol no other surface names: dedup, filter_map, hash, len, max_by, repeat, replace_section, sort, sum, to_bytes, to_json, zip. That is a finding in its own right, not rounding.

Two observed pre-existing conditions, neither introduced nor fixed here

1. builtin_registry_surface_names is 8 rows behind its primary authority — live, today. std.primitives builtin_registry_surface_names (the hand roster feeding the D0 census) carries 122 spellings; v1.compiler.infer_method builtin_function_registry (the authority it mirrors) carries 130. The set difference runs one way only:

class_b_import_closure_gate_not_affected_skip, compile_dag_diagnostic_census, dependency_resolution_facts, observe_declared_import_closure_symbol_binding, parse_roadmap_acceptance_event_history_jsonl, parse_stage0_cargo_manifest_bins, project_roadmap_acceptance_event_history_from_authority_text_host, type_ref_hit_ne_bind_measure_active

So that surface of primitive_surface_census_derived under-reports by 8 right now. primitive_d0_derived_surface_drift_audit_note predicts this failure in words — mutation control fires when the hand roster is updated, not when builtin_function_registry grows alone. What was not known is that the prediction has already come true and is eight deep, and that two of the eight (compile_dag_diagnostic_census, observe_declared_import_closure_symbol_binding) are rows whose own carrier notes in 04_method.dag promise they inherit the PrimitiveDefinition identity-join dissolution. Rows authored with an explicit promise to be joined are today invisible to the join. A documented gap that has silently become an occupied one is worse than an undocumented one, because the note reads as coverage.

Not fixed here: different subject, different owner (primitive-identity-join), and folding it in would widen this PR's scope. Recorded so the measurement survives.

Note that the surface this PR adds is not of that shape: the population is derived by mapping the primary structure, so there is no second list to drift from.

2. AlgebraFieldTemplate already carries cost_shape beside param_types, so the five-carrier separation is already breached on that surface. Pre-existing, out of scope, named so the next reader does not attribute it to this change.

Merge with main, and the two defects it exposed

Merged origin/main (conflict in dag/std/primitive_identity.dag). Neither side could be taken whole:

• The textual conflict: main's Relocate primitive projection behind the stage0 seed boundary #9060 relocated type PrimitiveIdentity out of this file into std.primitive_projection. My side still declared it. Keeping my side whole would have created two declarers; keeping main's whole would have dropped my carrier work. Resolution keeps my new types and lets main's deletion stand; PrimitiveIdentity now arrives through main's import and still resolves at its use sites.

• A 13th construction site, in a file that did not conflict. Main's Determinism classifies by primitive identity and traversal order, not by a hand roster of symbols #9092 added PrimitiveSemanticContract at src/v2/lens/determinism/reach_witness_test.dag:230. My "all 12 sites refuse until each declares a grounding" census was correct at my base and stale the moment that landed — the merge-interval class, where two individually-correct PRs produce a broken tree. Git flagged only the textual overlap; this one would have surfaced as a floor red in a file neither side touched. It is a deliberately planted primitive that exists to leave the traversal denominator open, so it takes SignatureUngrounded with a typed reason rather than a fabricated signature.

• A stale hand-authored grounding, which nothing would have caught. Main also renamed BooleanAlgebraCollectionProfile → FinitePowerSetProfile, added FinitelySupportedFunctionProfile (8 profiles → 9, 87 rows → 90), and relocated map_keys/map_values off PartialFunctionProfile. My D0 groundings for those two still pointed at the old profile and would have resolved Absent — silently, because the totality fold walks contracts derived from the template rows and so is nearly tautological. The hand-authored groundings are the only ones a human can get wrong, and nothing asserted them. w_every_declared_grounding_still_resolves_or_says_ungrounded is that guard, and RED 1 above is the actual upstream move replayed.

This is also the concrete receipt for the == 87 finding (review 55492, correct and acted on): the authority moved to 90 rows in this same merge, so the snapshot literal would have gone red for reasons having nothing to do with this change — exactly the change-detector failure §5's oracle ruling names. It is replaced by a self-denominating identity plus a controlled fixture, neither of which reads a count out of the current tree.

Provenance

Inventory jointly measured with stern-lynx-526, who independently produced the 57-row EmitHandler figure that corrected mine (my grep had matched nested name: inside rows rather than rows; the union was unaffected because all nine spurious names were already contributed by another surface). Carrier and population ruled by swift-badger-524.

[gunbai-bot]

Not pushing a fix, because the failure is not in this diff. Re-measured just now rather than assuming it was the same failure I diagnosed earlier.

Current state: one failing check, witnesses, run 32766819414 — the same run, not a new one. Cause unchanged: RouteGapFreezeIntersection count=4.

Why it is not mine, proven at tree grain (necessary because main has no completed run carrying the wall — every run since it landed is still queued, so a run comparison cannot answer this):

1. This branch changes exactly three files: dag/std/primitive_identity.dag, dag/test/claim/primitive_signature_grounding_witness_test.dag, src/v2/lens/determinism/reach_witness_test.dag. A diff of origin/main...HEAD restricted to the two authority files the refusal names — src/v2/workflow/floor_route_gap.dag and dag/gunbc/witness_deferral_freeze.dag — is empty.
2. The intersection is a pure function of those two static rosters. Recomputed on origin/main alone with this branch's commits absent, it reproduces: deploy_access_privilege_witness has 2 route-gap identities and its entry is frozen; host_effect_apply_witness has 6 and its entry is frozen.
3. The pre-merge run on head 4eb2e7385 passed the floor (run 32750246049, 49m58s). The only delta is merging main.

The fix exists and is owned elsewhere: #9133, "Retire four stale frozen_path_deferrals rows: the fleet-wide RouteGapFreezeIntersection line-stop" — currently open. Until it merges, main still carries the four rows, so re-running this PR would fail identically. A re-run now is wasted CI, and a commit from me would either duplicate #9133's work or be a no-op push.

The refusal offers two dispositions per identity (retire the freeze row, or drop it from the route-gap roster). Choosing between them requires knowing whether the required floor genuinely consumes each witness — lane knowledge I do not have — and the shrink log is a receipt-bearing authority. Guessing four dispositions to unblock my own PR is the wrong reason to touch it.

This PR otherwise: approved on the current head cc198dff9, no stale providers, no REQUEST_CHANGES, MERGEABLE. The earlier == 87 snapshot-oracle REQUEST_CHANGES is fixed and re-approved. Eleven witnesses pass, three mutations fail, all restore — verified by execution.

When #9133 lands I will merge main and re-run rather than assume, confirming both that the intersection count is actually zero at that head and that the eleven witnesses still route and execute.

— sent from sunny-ant-106