From 8750e96429b9e0391c746b50c5b4d501e57b2c72 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 1 Aug 2026 13:34:50 +0000 Subject: [PATCH] Primitive identity join D0: five-surface census and join refusals Land std.primitive_identity carriers, derived four-surface census, refusal coproducts, canonical alias lookup, and 15 executing witnesses. Rebases onto main through c9dc667b0 (#7580 publication gate). Co-authored-by: Cursor --- ROADMAP.md | 8 +- dag/gunbc/publication_grant.dag | 2 + dag/gunbc/roadmap_authority.dag | 46 +- dag/std/algebra.dag | 29 +- dag/std/primitive_identity.dag | 760 ++++++++++++++++++ dag/std/primitives.dag | 198 +++++ .../primitive_identity_join_witness_test.dag | 204 +++++ src/v1/stage0/src/std_algebra.rs | 56 +- 8 files changed, 1274 insertions(+), 29 deletions(-) create mode 100644 dag/std/primitive_identity.dag create mode 100644 dag/test/claim/primitive_identity_join_witness_test.dag diff --git a/ROADMAP.md b/ROADMAP.md index a292244daa6..4a4a8598d9f 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -86,8 +86,10 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ - [ ] **InferredTree carries only derived facts: the all-derived carrier lands** — Separate source and inferred carriers so candidate-equals-source is not even well-typed as a grounding proof: every fact on the inferred carrier traces to a derivation or the node refuses. Branch/Match/Loop (the three real inference paths) migrate first; the validate_then_compile door and its lens roster stay. A well-formed node with no derived facts cannot inhabit the carrier. Why: InferredTree becomes a trustworthy proof boundary; every lens consuming it stops reading facts that were never derived; the self-host frontier stops reading greener than it is. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - [ ] **Every node kind derives or refuses: the generic acceptance arm deletes** — The remaining derivation rules beyond Branch/Match/Loop: each v2 node kind either derives into the inferred carrier or its acceptance is a typed compile refusal — the generic accept-anything arm deletes. Coverage is counted per kind, so the frontier shrinks to zero or to named FrontierAccepted rows each carrying a trigger. Why: The last self-certification residue: any kind without a rule is currently accepted on well-formedness alone, which is the recovered defect class in its most general form. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - [ ] **Realization per target: an operation cannot compile for T without exactly one realization** — The realized carrier adds target realization: every executable operation in a program accepted for target T has exactly one compatible realization row for T, refused target-relatively otherwise. gunbc#7485 explicitly leaves this open; it consumes the primitive-identity join (realization rows are its per-target facts) and the derivation-coverage node (a realized tree is derived-then-realized, never source-then-realized). Why: The gunbc#7479 shape at its root: a costed-but-unrealized primitive currently compiles and fails at dispatch; the gate moves that to a located target-relative refusal. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: v2-node-kind-derivation-coverage, primitive-identity-join -- [ ] **Write the closing check for: One primitive identity: definition, per-target realization, and cost as three facts on one key** — One executable check states when this is done, transcribed from the node's own bar: A costed-but-unrealized primitive refuses target-relatively; a realized-but-undefined name cannot be keyed; existing corpus calls all still resolve. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - - [ ] **One primitive identity: definition, per-target realization, and cost as three facts on one key** — PrimitiveDefinition (invocation forms, receiver domain, parameters, result), PrimitiveRealization per target, PrimitiveCostModel — joined by one identity so a call cannot compile for target T without exactly one compatible definition and realization, and interpreter/emitter dispatch derive from realization rows instead of five independently-writable name sets (registry map, PrimitiveContract rows, algebra templates, interpreter arms, per-target templates). Why: Closes the gunbc#7479 CLASS rather than the specimen: filter_map had a cost contract, no seed method, and a green compile. Unlocks the method ambiguity wall (sameness becomes decidable) and un-narrows the method-existence wall — the measured length/count/size dispatch fork on gunbc#7484 is why per-receiver checking stalls at kernel receivers today. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - - [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: primitive-identity-join, method-zero-resolution-general-wall +- [ ] **Write the closing check for: Interpreter primitive roster: the fifth surface becomes readable from .dag** — One executable check states when this is done, transcribed from the node's own bar: A new dispatch arm without a roster row refuses; a roster row without a matching arm refuses; fold_list via eval_call intercept and lookup dual-realization join through derived census. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) + - [ ] **Interpreter primitive roster: the fifth surface becomes readable from .dag** — Land interpreter-primitive-roster across all six v1_interpreter dispatch sites (eval_builtin_inner, eval_algebra_method_inner, eval_call, try_v2_std_collection_map_primitive_grounding, try_parse_table_memo_dispatch, eval_method_call lookup short-circuit — 158 arms / 169 spellings). clever-crab-111 macro authority: eval_builtin_inner arms expand from interpreter_free_call_arm_spellings with construction wall (arm without roster entry unwritable). primitive_surface_census_derived absorbs InterpreterDispatch instead of primitive_interpreter_dispatch_measurement_rows. Prerequisite for primitive-identity-join terminal acceptance. Why: Closes the fifth blind spot in D1 mutation control across all six dispatch sites. Dissolves MeasurementOnly specimen rows into derived surfaces. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) + - [ ] **One primitive identity: definition, per-target realization, and cost as three facts on one key** — PrimitiveDefinition (identity + PrimitiveSemanticContract), PrimitiveInvocationSurface, PrimitiveRealization per RealizationTarget, PrimitiveCostFact, and PrimitiveTraversalOrderFact — five separate carriers joined by PrimitiveIdentity, never one mega-row. TERMINAL acceptance: every primitive-bearing surface across all five authorities (registry, PrimitiveContract rows, algebra templates, interpreter dispatch, emit handlers) joins exactly one identity; population-wide join and realization refusals are the closing contract. D0 is a first slice only — not the closing contract. Namespace supplies declaration identity; this node supplies semantic primitive identity across invocation and realization. Why: Proves the determinism denominator is open (#7532 honest rung) and begins closing it: four surfaces feed primitive_surface_census_derived at runtime; mutation control is CLOSED on AlgebraTemplate and EmitHandler, PARTIAL on BuiltinRegistry and PrimitiveContractRow (parallel hand rosters — primitive_d0_derived_surface_drift_audit_note), NOT DISCOVERED on InterpreterDispatch. fold_list spelling fork and index_by registry+algebra dual absence are named specimens proving the denominator is not closed. Unlocks method ambiguity wall and D1 determinism consumption through PrimitiveIdentity rather than raw symbol. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) + - [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: primitive-identity-join, method-zero-resolution-general-wall + - [ ] **Determinism denominator closure: every primitive carries one traversal-order classification** — v2.std.determinism and v2.lens.determinism consume std.primitive_identity: every PrimitiveDefinition carries exactly one PrimitiveTraversalOrderFact, unclassified refuses, HostUnspecifiedOrder derives a determinism root, aliases resolve through PrimitiveIdentity not raw symbol. Adding a new invokable primitive realization without a traversal-order fact reds before any caller uses it. Why: Dissolves the interim two-root registry (#7532) into a closed denominator — the gate can tell an alias from a distinct operation, and keys/values false-positive class is eliminated by identity not spelling. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - [ ] **Write the closing check for: The capability audit: sole_constructor completeness, then seal the proof-carriers** — One executable check states when this is done, transcribed from the node's own bar: Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) - [ ] **The capability audit: sole_constructor completeness, then seal the proof-carriers** — The language ALREADY has a construction wall: sole_constructor rejects cross-module construction with SoleConstructorViolation and carries a sealed-record specimen (post-merge review of gunbc#7486 refuted this node's earlier premise that no private/sealed/opaque capability exists). What is UNVERIFIED is its completeness: generic carriers (does type Refined sole_constructor hold across instantiation?), every construction form (literals, casts like as TransportScript, coproduct variants, default values), and behavior under module_skips_direct_call_arg_check. Audit by falsification first; extend sole_constructor or ground the reference-grant algebra (the parked visibility-grants design) only where the audit reds. Why: Every capability-kind ceiling resolves together — either sole_constructor suffices (cheap: seal Refined, delete the stub-pack forge arm) or its named gaps price the visibility-grants work honestly instead of by assumption. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) diff --git a/dag/gunbc/publication_grant.dag b/dag/gunbc/publication_grant.dag index 0617a3559e0..9edbdf2598c 100644 --- a/dag/gunbc/publication_grant.dag +++ b/dag/gunbc/publication_grant.dag @@ -76,11 +76,13 @@ data public_file_publish_grants: List = [ public_file_publish_grant(path: "dag/gunbc/publication_grant.dag"), public_file_publish_grant(path: "dag/gunbc/roadmap_presentation.dag"), public_file_publish_grant(path: "dag/gunbc/source_integration_proof_kernel.dag"), + public_file_publish_grant(path: "dag/std/primitive_identity.dag"), public_file_publish_grant(path: "dag/test/claim/acquisition_mechanism_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/advertising_interface_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/crm_stage_vocabulary_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/heal_revalidation_integration_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/heal_revalidation_witness_test.dag"), + public_file_publish_grant(path: "dag/test/claim/primitive_identity_join_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/roadmap_presentation_witness_test.dag"), public_file_publish_grant(path: "dag/test/claim/source_integration_proof_kernel_acceptance_test.dag"), public_file_publish_grant(path: "dag/test/claim/source_integration_proof_kernel_model_witness_test.dag"), diff --git a/dag/gunbc/roadmap_authority.dag b/dag/gunbc/roadmap_authority.dag index ac2f5c513a4..b24f5ba14e2 100644 --- a/dag/gunbc/roadmap_authority.dag +++ b/dag/gunbc/roadmap_authority.dag @@ -229,7 +229,7 @@ fn observation_raw_print_retirement_execution_contract() -> WorkItemExecutionCon ) } -data scm_p1_proof_kernel_contract_note: String = "THE SCM P1 CLOSING DISCRIMINATOR, authored only after the first P1 carrier made the node's whole completion condition executable. The validation is deliberately RED: its closed capability population is the roadmap node's own bar, and this first slice supplies only the bounded candidate-generation model check. Missing behavior is derived set difference, never a hand-maintained progress count; duplicate passing rows cannot erase it, and a false row remains missing. The contract therefore cannot green on zero progress and cannot confuse a modeled carrier with an executed proof kernel. It is enrolled QuarantineProbeExpectRed in gunbc.ci_layer_roots. Each later P1 slice adds an executing scenario check without weakening the aggregate. When the final capability greens, that same change removes the expect-red enrollment and promotes the witness to the ordinary discovery ratchet." +data scm_p1_proof_kernel_contract_note: String = "THE SCM P1 CLOSING DISCRIMINATOR, authored only after the first P1 carrier made the node's whole completion condition executable. The validation is deliberately RED: its closed capability population is the roadmap node's own bar, and this first slice supplies only the bounded candidate-generation model check. Missing behavior is derived set difference, never a hand-maintained progress count; duplicate passing rows cannot erase it, and a false row remains missing. The contract therefore cannot green on zero progress and cannot confuse a modeled carrier with an executed proof kernel. It is enrolled QuarantineProbeExpectRed in gunbc.ci_layer_roots. Each later P1 slice adds an executing scenario check without weakening the aggregate. When the final capability greens, that same change removes the expect-red enrollment and promotes the witness to ordinary discovery ratchet." fn scm_p1_proof_kernel_execution_contract() -> WorkItemExecutionContract { gunbc_claim_execution_contract( @@ -2482,12 +2482,42 @@ fn guarantee_ladder_nodes() -> List { volume: VolumeMedium, t: fields( headline: "One primitive identity: definition, per-target realization, and cost as three facts on one key", - boundary: "PrimitiveDefinition (invocation forms, receiver domain, parameters, result), PrimitiveRealization per target, PrimitiveCostModel — joined by one identity so a call cannot compile for target T without exactly one compatible definition and realization, and interpreter/emitter dispatch derive from realization rows instead of five independently-writable name sets (registry map, PrimitiveContract rows, algebra templates, interpreter arms, per-target templates).", - displaced_cost: "Closes the gunbc#7479 CLASS rather than the specimen: filter_map had a cost contract, no seed method, and a green compile. Unlocks the method ambiguity wall (sameness becomes decidable) and un-narrows the method-existence wall — the measured length/count/size dispatch fork on gunbc#7484 is why per-receiver checking stalls at kernel receivers today.", - first_slice: "The identity type plus the join for the collection-algebra family (map/filter/fold/flat_map/filter_map), with the registry and contract rows re-keyed onto it.", - red_control: "A costed-but-unrealized primitive refuses target-relatively; a realized-but-undefined name cannot be keyed; existing corpus calls all still resolve.", - out_of_scope: "Deleting the seed dispatch (climbs by self-host deletion); new primitives.", - handback: "The three carrier types, the joined family roster, the derived-dispatch receipt." + boundary: "PrimitiveDefinition (identity + PrimitiveSemanticContract), PrimitiveInvocationSurface, PrimitiveRealization per RealizationTarget, PrimitiveCostFact, and PrimitiveTraversalOrderFact — five separate carriers joined by PrimitiveIdentity, never one mega-row. TERMINAL acceptance: every primitive-bearing surface across all five authorities (registry, PrimitiveContract rows, algebra templates, interpreter dispatch, emit handlers) joins exactly one identity; population-wide join and realization refusals are the closing contract. D0 is a first slice only — not the closing contract. Namespace supplies declaration identity; this node supplies semantic primitive identity across invocation and realization.", + displaced_cost: "Proves the determinism denominator is open (#7532 honest rung) and begins closing it: four surfaces feed primitive_surface_census_derived at runtime; mutation control is CLOSED on AlgebraTemplate and EmitHandler, PARTIAL on BuiltinRegistry and PrimitiveContractRow (parallel hand rosters — primitive_d0_derived_surface_drift_audit_note), NOT DISCOVERED on InterpreterDispatch. fold_list spelling fork and index_by registry+algebra dual absence are named specimens proving the denominator is not closed. Unlocks method ambiguity wall and D1 determinism consumption through PrimitiveIdentity rather than raw symbol.", + first_slice: "D0 first slice (NOT closing contract): std.primitive_identity carriers; primitive_surface_census_derived from four authorities; primitive_interpreter_dispatch_measurement_rows (MeasurementOnly) for specimens; refusal predicate machinery; slice witness receipt. Denominator NOT closed — interpreter blind until interpreter-primitive-roster lands.", + red_control: "TERMINAL (population-wide): every derived census row joins exactly one PrimitiveIdentity; surfaces joining two identities refuse; realizations naming unknown primitives refuse; duplicate semantic definitions refuse. D0 SLICE ONLY: derived census exceeds specimen count; four named specimen findings (map_keys five-surface join, fold_list spelling fork, fold_list registry gap, index_by registry+algebra gap); planted missing-identity and unknown-realization RED controls — these witnesses do not substitute for terminal acceptance.", + out_of_scope: "D1 determinism gate consumption (child determinism-denominator-closure); deleting v1 seed dispatch tables; namespace declaration identity.", + handback: "D0: std.primitive_identity carriers, primitive_surface_census_derived, measurement specimen rows, refusal predicates, slice witness receipt. TERMINAL (after interpreter-primitive-roster): population-wide join closure across all five surfaces." + ) + ), + active_sized(identity: "rn_DETERMINISM_DENOMINATOR_CLOSURE", id: "determinism-denominator-closure", + owner: "compiler-guarantee", + path: "docs/plans/compiler-guarantee-recovery-gap-analysis.md", + intricacy: IntricacyHigh, + volume: VolumeMedium, + t: fields( + headline: "Determinism denominator closure: every primitive carries one traversal-order classification", + boundary: "v2.std.determinism and v2.lens.determinism consume std.primitive_identity: every PrimitiveDefinition carries exactly one PrimitiveTraversalOrderFact, unclassified refuses, HostUnspecifiedOrder derives a determinism root, aliases resolve through PrimitiveIdentity not raw symbol. Adding a new invokable primitive realization without a traversal-order fact reds before any caller uses it.", + displaced_cost: "Dissolves the interim two-root registry (#7532) into a closed denominator — the gate can tell an alias from a distinct operation, and keys/values false-positive class is eliminated by identity not spelling.", + first_slice: "Wire determinism_compile_gate to PrimitiveTraversalOrderFact over the primitive_identity census rather than determinism_root_registry symbol matching.", + red_control: "A new primitive realization without traversal-order fact refuses at gate enrollment before corpus reach; map_keys and map_values classify HostUnspecifiedOrder through identity; generic keys/values symbols do not false-positive unrelated functions.", + out_of_scope: "D0 census and join carriers (parent primitive-identity-join); deleting v1 seed dispatch.", + handback: "Identity-keyed determinism classification, closed denominator receipt, deleted interim symbol registry." + ) + ), + active_sized(identity: "rn_INTERPRETER_PRIMITIVE_ROSTER", id: "interpreter-primitive-roster", + owner: "compiler-guarantee", + path: "docs/plans/compiler-guarantee-recovery-gap-analysis.md", + intricacy: IntricacyHigh, + volume: VolumeMedium, + t: fields( + headline: "Interpreter primitive roster: the fifth surface becomes readable from .dag", + boundary: "Land interpreter-primitive-roster across all six v1_interpreter dispatch sites (eval_builtin_inner, eval_algebra_method_inner, eval_call, try_v2_std_collection_map_primitive_grounding, try_parse_table_memo_dispatch, eval_method_call lookup short-circuit — 158 arms / 169 spellings). clever-crab-111 macro authority: eval_builtin_inner arms expand from interpreter_free_call_arm_spellings with construction wall (arm without roster entry unwritable). primitive_surface_census_derived absorbs InterpreterDispatch instead of primitive_interpreter_dispatch_measurement_rows. Prerequisite for primitive-identity-join terminal acceptance.", + displaced_cost: "Closes the fifth blind spot in D1 mutation control across all six dispatch sites. Dissolves MeasurementOnly specimen rows into derived surfaces.", + first_slice: "Roster authority for six sites; eval_builtin_inner via interpreter_free_call_arm_spellings macro; primitive_surface_census_derived absorbs interpreter dispatch; measurement rows deleted.", + red_control: "A new dispatch arm without a roster row refuses; a roster row without a matching arm refuses; fold_list via eval_call intercept and lookup dual-realization join through derived census.", + out_of_scope: "D0 slice carriers and four-surface derivation (parent primitive-identity-join first slice); deleting seed dispatch implementation.", + handback: "Modeled interpreter roster authority, derived fifth surface on primitive_surface_census_derived, deleted measurement scaffold." ) ), active_sized(identity: "rn_JPU4RUV5DNELDCZI4JUQGWHICM", id: "compiler-source-exemption-removal", @@ -2584,6 +2614,8 @@ fn guarantee_ladder_edges() -> List { edge(child: "v2-node-kind-derivation-coverage", parent: "v2-inferred-tree-completeness"), edge(child: "v2-target-realization-gate", parent: "v2-node-kind-derivation-coverage"), edge(child: "v2-target-realization-gate", parent: "primitive-identity-join"), + edge(child: "determinism-denominator-closure", parent: "primitive-identity-join"), + edge(child: "primitive-identity-join", parent: "interpreter-primitive-roster"), edge(child: "accepted-obligation-door-mechanism", parent: "ladder-claims-carrier"), edge(child: "accepted-floor-obligation-closure", parent: "accepted-obligation-door-mechanism"), edge(child: "accepted-floor-obligation-closure", parent: "call-missing-and-duplicate-wall"), diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 306c3c4524d..53febc45502 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -336,11 +336,8 @@ fn partial_function_templates() -> List { } fn algebra_method_template_name(name: String) -> Bool { - [ - OrderedRingProfile, ApproximateFieldProfile, BooleanAlgebraProfile, - BooleanAlgebraCollectionProfile, PointwisePowerCollectionProfile, FreeMonoidScalarProfile, - FreeMonoidCollectionProfile, PartialFunctionProfile - ] |> any(p => algebra_templates_for_profile(profile: p) |> any(t => t.name == name)) + all_algebra_profiles() + |> any(profile => algebra_templates_for_profile(profile: profile) |> any(t => t.name == name)) } fn algebra_templates_for_profile(profile: AlgebraProfile) -> List { @@ -368,3 +365,25 @@ fn algebra_type_param_names(profile: AlgebraProfile) -> List { PartialFunctionProfile => ["K", "V"] } } + +fn all_algebra_profiles() -> List { + [ + OrderedRingProfile, + ApproximateFieldProfile, + BooleanAlgebraProfile, + BooleanAlgebraCollectionProfile, + PointwisePowerCollectionProfile, + FreeMonoidScalarProfile, + FreeMonoidCollectionProfile, + PartialFunctionProfile, + ] +} + +fn all_algebra_field_templates() -> List { + all_algebra_profiles() + |> flat_map(profile => algebra_templates_for_profile(profile: profile)) +} + +fn all_algebra_template_names() -> List { + all_algebra_field_templates() |> map(template => template.name) +} diff --git a/dag/std/primitive_identity.dag b/dag/std/primitive_identity.dag new file mode 100644 index 00000000000..6e09aa24500 --- /dev/null +++ b/dag/std/primitive_identity.dag @@ -0,0 +1,760 @@ +module std.primitive_identity + +import std.algebra { + CostShape, + ShapeIterateBody, + ShapeLinearScan, + all_algebra_field_templates, + all_algebra_template_names, +} +import std.decl_ref { DeclarationRef, DeclField, WholeDeclaration, NamedField } +import std.primitives { primitive_contract_roster, builtin_registry_surface_names } +import std.types { Bool, Int, List, NonEmptyStr, String } +import extdeps.languages.rust.emit { rt_function_registry } + +data primitive_identity_d0_scope_note: String = "D0 is NOT terminal acceptance and does NOT close the subject universe. Landed and executing: join mechanism across five carriers, five refusal variants typed, three refusal detectors executing with witnesses (see primitive_d0_refusal_execution_note), derived census across four surfaces. OPEN at fifth surface (InterpreterDispatch): closure fires when interpreter-primitive-roster lands (primitive_interpreter_dispatch_derivation_next_trigger). Four-of-five derived is honest interim state, not completion." + +data primitive_d0_refusal_execution_note: String = "Five PrimitiveJoinViolation variants typed at D0. Three detectors execute with RED witnesses: primitive_surface_missing_identity_violation, primitive_realization_unknown_primitive_violation, primitive_duplicate_semantic_definition_violation. Two scaffold detectors execute on planted inputs only (terminal join expands population-wide detection): primitive_surface_joins_two_identities_violation, primitive_incompatible_invocation_assignment_violation." + +data primitive_identity_d0_note: String = "D0 (primitive-identity-join first slice): semantic primitive identity is ONE join key across five independently-writable surfaces. See primitive_identity_d0_scope_note — NOT the closing contract. primitive_surface_census_derived reads four live authorities. primitive_interpreter_dispatch_measurement_rows is an interim measurement scaffold, NOT an authority (see primitive_interpreter_dispatch_measurement_scaffold_note). Open denominator receipt: primitive_d0_open_denominator_receipt. Dissolve-on: feature:primitive-realization-single-authority." + +data primitive_interpreter_dispatch_measurement_scaffold_note: String = "SCAFFOLD — interim measurement, NOT an authority: primitive_interpreter_dispatch_measurement_rows carries four join specimens with provenance MeasurementOnly. Dissolution trigger: interpreter-primitive-roster lands on clever-crab-111 v1 lane (interpreter_free_call_arm_spellings macro + six-site roster); primitive_surface_census_derived absorbs InterpreterDispatch; delete primitive_interpreter_dispatch_measurement_rows and this note." + +data primitive_d0_derived_surface_drift_audit_note: String = "Derived-surface drift audit (review 45947 class): AlgebraTemplate — CLOSED, all_algebra_field_templates flat_maps all_algebra_profiles (2c9c01351). EmitHandler — single authority, rt_function_registry with derived rt_functions/rt_ref_map_functions projections (no parallel roster). BuiltinRegistry — OPEN parallel enumeration: builtin_registry_surface_names hand list beside builtin_function_registry Map (witness cannot map_keys Node at runtime; builtin_registry_surface_names_note). PrimitiveContractRow — OPEN parallel enumeration: primitive_contract_roster hand list beside *_contract data rows (primitive_contract_roster_note). D0 mutation control on those two surfaces discovers drift only when the hand list is updated, not when the primary authority grows alone." + +data primitive_d0_open_denominator_receipt_note: String = "Typed located counted open denominator (rung-honesty receipt): derived_surface_authority_count=4 (BuiltinRegistry, PrimitiveContractRow, AlgebraTemplate, EmitHandler); open_surface_authority_count=1 (InterpreterDispatch at primitive_interpreter_dispatch_derivation_next_trigger); interpreter_dispatch_arm_count=158; interpreter_dispatch_spelling_count=169 across six v1_interpreter sites; interpreter_measurement_specimen_count=4 (NOT 158). derived_census_rows_missing_identity_count is measured live by primitive_d0_derived_rows_missing_identity_count — ranks join work remaining on derived surfaces. See primitive_d0_derived_surface_drift_audit_note for per-surface drift status." + +data primitive_d0_derived_surface_authority_count: Int = 4 + +data primitive_d0_open_surface_authority_count: Int = 1 + +data primitive_interpreter_dispatch_arm_count: Int = 158 + +data primitive_interpreter_dispatch_spelling_count: Int = 169 + +data primitive_d0_parallel_roster_surface_authority_count: Int = 2 + +data primitive_d0_mutation_control_coverage_note: String = "Exact D1 mutation-control coverage after D0: DISCOVERED on AlgebraTemplate and EmitHandler — new template or emit-handler row without identity join appears on primitive_surface_census_derived and can refuse. PARTIAL on BuiltinRegistry and PrimitiveContractRow (parallel_roster_surface_authority_count=2) — mutation control fires when the hand roster (builtin_registry_surface_names, primitive_contract_roster) is updated, NOT when builtin_function_registry or a *_contract data row grows alone; see primitive_d0_derived_surface_drift_audit_note. NOT DISCOVERED on InterpreterDispatch — new arm on any of the six v1_interpreter dispatch sites is blind until primitive_interpreter_dispatch_derivation_next_trigger lands. Counted: open_surface_authority_count=1. Derived does not mean complete; parallel roster does not mean single-authority." + +data primitive_interpreter_dispatch_six_sites_note: String = "Interpreter dispatch is SIX sites in v1_interpreter (clever-crab-111 census, parent-verified): eval_builtin_inner 112 arms/115 spellings free calls; eval_algebra_method_inner 39 arms/46 spellings methods; eval_call 2 arms fold_list and fold_list_right native intercept BEFORE eval_builtin_inner; try_v2_std_collection_map_primitive_grounding 2 arms; try_parse_table_memo_dispatch 2 arms; eval_method_call 1 arm lookup short-circuit. Total 158 arms / 169 spellings. D0 primitive_interpreter_dispatch_measurement_rows covers four join specimens only — NOT this six-site population. A census reading only eval_builtin_inner sees about two thirds." + +data primitive_interpreter_dispatch_derivation_next_trigger: String = "Next rung trigger: land interpreter-primitive-roster — modeled roster authority for all six v1_interpreter dispatch sites. clever-crab-111 macro authority makes eval_builtin_inner arms and interpreter_free_call_arm_spellings roster unwritable-by-construction (arm without roster entry and roster entry without arm both refuse); other five sites are hand-declared rows with the macro as dissolution trigger. Coordinate roster shape with clever-crab before building join consumption. No roster row carries identity — arms that join to nothing stay representable for SurfaceMissingPrimitiveIdentity." + +data primitive_interpreter_surface_unenumerable_finding_note: String = "Finding (inherits to v1 exit lane): the interpreter primitive surface was six hand-written Rust dispatch sites in v1_interpreter, not one. v1_interpreter eval_builtin_inner is the main free-call site. v2.compiler.eval v2_eval_call_primitive (carrier src/v2/compiler/05_eval.dag) is a separate v2 witness hook — real symbol, NOT v1 dispatch (§3 cite-the-symbol: never attribute it to v1_interpreter.rs). eval_call native intercept for fold_list fires before eval_builtin_inner — explains registry absence. clever-crab-111 macro authority may make eval_builtin_inner derivable sooner; five other sites remain hand-declared until macro dissolves them." + +data primitive_fold_list_spelling_fork_note: String = "Named finding — SPELLING FORK, not alias: contract/algebra carry fold while interpreter/emit carry fold_list. Distinct from alias groups (length/count/size are one eval_builtin_inner arm with three spellings — aliases sharing an arm cannot disagree). fold and fold_list are separate surfaces that CAN disagree; fold_list additionally lives on eval_call intercept before eval_builtin_inner, so it never reaches builtin_function_registry." + +data primitive_lookup_dual_realization_note: String = "Named finding — first two-realizations-one-name specimen: lookup has eval_method_call short-circuit AND an algebra template arm; the short-circuit shadows the algebra arm. Better join specimen than index_by for SurfaceJoinsTwoIdentities / realization reconciliation. keys and values DO have algebra template arms — determinism undetectability is about the lens view of unqualified symbols, not absence of algebra arms." + +data primitive_interpreter_dispatch_derivation_blocked_note: String = "Interpreter dispatch derivation blocked pending primitive_interpreter_dispatch_derivation_next_trigger. Measurement rows use provenance MeasurementOnly and cover four join specimens only; see primitive_interpreter_dispatch_six_sites_note." + +type PrimitiveIdentity { + slug: NonEmptyStr +} + +type PrimitiveSemanticContract { + canonical_name: NonEmptyStr +} + +type PrimitiveDefinition { + identity: PrimitiveIdentity + semantic_contract: PrimitiveSemanticContract +} + +type InvocationForm + = FreeCall + | MethodCall { receiver_domain: NonEmptyStr } + | OperatorCall + +type PrimitiveInvocationSurface { + primitive: PrimitiveIdentity + form: InvocationForm + authored_symbol: NonEmptyStr +} + +type RealizationTarget + = InterpreterHost + | EmitRust + | EmitTypeScript + +type PrimitiveRealization { + primitive: PrimitiveIdentity + target: RealizationTarget + handler: DeclarationRef +} + +type PrimitiveCostFact { + primitive: PrimitiveIdentity + cost: CostShape +} + +type TraversalOrder + = HostUnspecifiedOrder + | CanonicalOrder + | SourcePreservingOrder + | TraversalOrderUnclassified + +type PrimitiveTraversalOrderFact { + primitive: PrimitiveIdentity + order: TraversalOrder +} + +type PrimitiveSurfaceAuthority + = BuiltinRegistry + | PrimitiveContractRow + | AlgebraTemplate + | InterpreterDispatch + | EmitHandler + +type PrimitiveSurfaceCensusProvenance + = DerivedFromAuthority + | MeasurementOnly + +type PrimitiveSurfaceRow { + authority: PrimitiveSurfaceAuthority + authored_symbol: NonEmptyStr + authority_ref: DeclarationRef + primitive: PrimitiveIdentity? + provenance: PrimitiveSurfaceCensusProvenance +} + +type PrimitiveJoinViolation + = SurfaceMissingPrimitiveIdentity { + authority: PrimitiveSurfaceAuthority + authored_symbol: NonEmptyStr + } + | SurfaceJoinsTwoIdentities { + authority: PrimitiveSurfaceAuthority + authored_symbol: NonEmptyStr + first: PrimitiveIdentity + second: PrimitiveIdentity + } + | IncompatibleInvocationAssignment { + authored_symbol: NonEmptyStr + first: PrimitiveIdentity + second: PrimitiveIdentity + } + | RealizationNamesUnknownPrimitive { + target: RealizationTarget + handler: DeclarationRef + } + | DuplicateSemanticDefinition { identity: PrimitiveIdentity } + +fn primitive_identity_slug(name: String) -> PrimitiveIdentity { + PrimitiveIdentity { slug: concat("primitive.", name) as NonEmptyStr } +} + +fn primitive_identity_eq(left: PrimitiveIdentity, right: PrimitiveIdentity) -> Bool { + left.slug == right.slug +} + +fn decl_ref(module_path: String, decl_name: String) -> DeclarationRef { + DeclarationRef { + module_path: module_path as NonEmptyStr, + decl_name: decl_name as NonEmptyStr, + field: WholeDeclaration, + } +} + +fn decl_field_ref(module_path: String, decl_name: String, field_name: String) -> DeclarationRef { + DeclarationRef { + module_path: module_path as NonEmptyStr, + decl_name: decl_name as NonEmptyStr, + field: NamedField { field_name: field_name as NonEmptyStr }, + } +} + +data primitive_map_keys: PrimitiveIdentity = primitive_identity_slug(name: "map_keys") +data primitive_map_values: PrimitiveIdentity = primitive_identity_slug(name: "map_values") +data primitive_fold_list: PrimitiveIdentity = primitive_identity_slug(name: "fold_list") +data primitive_index_by: PrimitiveIdentity = primitive_identity_slug(name: "index_by") + +data primitive_map_keys_definition: PrimitiveDefinition = PrimitiveDefinition { + identity: primitive_map_keys, + semantic_contract: PrimitiveSemanticContract { canonical_name: "map_keys" as NonEmptyStr }, +} + +data primitive_map_values_definition: PrimitiveDefinition = PrimitiveDefinition { + identity: primitive_map_values, + semantic_contract: PrimitiveSemanticContract { canonical_name: "map_values" as NonEmptyStr }, +} + +data primitive_fold_list_definition: PrimitiveDefinition = PrimitiveDefinition { + identity: primitive_fold_list, + semantic_contract: PrimitiveSemanticContract { canonical_name: "fold_list" as NonEmptyStr }, +} + +data primitive_index_by_definition: PrimitiveDefinition = PrimitiveDefinition { + identity: primitive_index_by, + semantic_contract: PrimitiveSemanticContract { canonical_name: "index_by" as NonEmptyStr }, +} + +data primitive_d0_definitions: List = [ + primitive_map_keys_definition, + primitive_map_values_definition, + primitive_fold_list_definition, + primitive_index_by_definition, +] + +fn surface_row( + authority: PrimitiveSurfaceAuthority, + authored_symbol: String, + authority_ref: DeclarationRef, + primitive: PrimitiveIdentity?, + provenance: PrimitiveSurfaceCensusProvenance +) -> PrimitiveSurfaceRow { + PrimitiveSurfaceRow { + authority: authority, + authored_symbol: authored_symbol as NonEmptyStr, + authority_ref: authority_ref, + primitive: primitive, + provenance: provenance, + } +} + +type PrimitiveSurfaceAliasBinding { + authority: PrimitiveSurfaceAuthority + authored_symbol: NonEmptyStr + identity: PrimitiveIdentity +} + +data primitive_d0_surface_alias_bindings_note: String = "D0 specimen alias table — single (authority × authored_symbol) → PrimitiveIdentity authority consumed by primitive_identity_lookup and all census row builders. Dissolve-on: population-wide join replaces this hand table at terminal acceptance." + +data primitive_d0_surface_alias_bindings: List = [ + PrimitiveSurfaceAliasBinding { + authority: BuiltinRegistry, + authored_symbol: "map_keys" as NonEmptyStr, + identity: primitive_map_keys, + }, + PrimitiveSurfaceAliasBinding { + authority: BuiltinRegistry, + authored_symbol: "map_values" as NonEmptyStr, + identity: primitive_map_values, + }, + PrimitiveSurfaceAliasBinding { + authority: PrimitiveContractRow, + authored_symbol: "map_keys" as NonEmptyStr, + identity: primitive_map_keys, + }, + PrimitiveSurfaceAliasBinding { + authority: PrimitiveContractRow, + authored_symbol: "map_values" as NonEmptyStr, + identity: primitive_map_values, + }, + PrimitiveSurfaceAliasBinding { + authority: PrimitiveContractRow, + authored_symbol: "fold" as NonEmptyStr, + identity: primitive_fold_list, + }, + PrimitiveSurfaceAliasBinding { + authority: PrimitiveContractRow, + authored_symbol: "index_by" as NonEmptyStr, + identity: primitive_index_by, + }, + PrimitiveSurfaceAliasBinding { + authority: AlgebraTemplate, + authored_symbol: "map_keys" as NonEmptyStr, + identity: primitive_map_keys, + }, + PrimitiveSurfaceAliasBinding { + authority: AlgebraTemplate, + authored_symbol: "map_values" as NonEmptyStr, + identity: primitive_map_values, + }, + PrimitiveSurfaceAliasBinding { + authority: AlgebraTemplate, + authored_symbol: "fold" as NonEmptyStr, + identity: primitive_fold_list, + }, + PrimitiveSurfaceAliasBinding { + authority: EmitHandler, + authored_symbol: "map_keys" as NonEmptyStr, + identity: primitive_map_keys, + }, + PrimitiveSurfaceAliasBinding { + authority: EmitHandler, + authored_symbol: "map_values" as NonEmptyStr, + identity: primitive_map_values, + }, + PrimitiveSurfaceAliasBinding { + authority: EmitHandler, + authored_symbol: "index_by" as NonEmptyStr, + identity: primitive_index_by, + }, + PrimitiveSurfaceAliasBinding { + authority: InterpreterDispatch, + authored_symbol: "map_keys" as NonEmptyStr, + identity: primitive_map_keys, + }, + PrimitiveSurfaceAliasBinding { + authority: InterpreterDispatch, + authored_symbol: "map_values" as NonEmptyStr, + identity: primitive_map_values, + }, + PrimitiveSurfaceAliasBinding { + authority: InterpreterDispatch, + authored_symbol: "fold_list" as NonEmptyStr, + identity: primitive_fold_list, + }, + PrimitiveSurfaceAliasBinding { + authority: InterpreterDispatch, + authored_symbol: "index_by" as NonEmptyStr, + identity: primitive_index_by, + }, +] + +fn primitive_identity_lookup( + authority: PrimitiveSurfaceAuthority, + authored_symbol: String, +) -> PrimitiveIdentity? { + primitive_d0_surface_alias_bindings + |> fold(init: none, f: fn(acc, binding) { + match acc { + Present { value: _ } => acc + Absent => + if binding.authority == authority + && (binding.authored_symbol as String) == authored_symbol { + Present { value: binding.identity } + } else { + none + } + } + }) +} + +fn registry_contains_symbol(sym: String) -> Bool { + builtin_registry_surface_names() |> any(name => name == sym) +} + +fn algebra_contains_template_name(name: String) -> Bool { + all_algebra_template_names() |> any(template_name => template_name == name) +} + +fn emit_contains_symbol(sym: String) -> Bool { + rt_function_registry |> any(entry => entry.name == sym) +} + +fn contract_contains_name(name: String) -> Bool { + primitive_contract_roster() |> any(contract => contract.name == name) +} + +fn primitive_registry_surface_rows() -> List { + builtin_registry_surface_names() + |> map(sym => + surface_row( + authority: BuiltinRegistry, + authored_symbol: sym, + authority_ref: decl_ref(module_path: "std.primitives", decl_name: "builtin_registry_surface_names"), + primitive: primitive_identity_lookup(authority: BuiltinRegistry, authored_symbol: sym), + provenance: DerivedFromAuthority, + ) + ) +} + +fn primitive_contract_surface_rows() -> List { + primitive_contract_roster() + |> map(contract => + surface_row( + authority: PrimitiveContractRow, + authored_symbol: contract.name, + authority_ref: decl_field_ref( + module_path: "std.primitives", + decl_name: concat(contract.name, "_contract"), + field_name: "name", + ), + primitive: primitive_identity_lookup( + authority: PrimitiveContractRow, + authored_symbol: contract.name, + ), + provenance: DerivedFromAuthority, + ) + ) +} + +fn primitive_algebra_surface_rows() -> List { + all_algebra_field_templates() + |> map(template => + surface_row( + authority: AlgebraTemplate, + authored_symbol: template.name, + authority_ref: decl_ref(module_path: "std.algebra", decl_name: "all_algebra_field_templates"), + primitive: primitive_identity_lookup(authority: AlgebraTemplate, authored_symbol: template.name), + provenance: DerivedFromAuthority, + ) + ) +} + +fn primitive_emit_surface_rows() -> List { + rt_function_registry + |> map(entry => + surface_row( + authority: EmitHandler, + authored_symbol: entry.name, + authority_ref: decl_ref(module_path: "extdeps.languages.rust.emit", decl_name: "rt_function_registry"), + primitive: primitive_identity_lookup(authority: EmitHandler, authored_symbol: entry.name), + provenance: DerivedFromAuthority, + ) + ) +} + +fn primitive_interpreter_dispatch_measurement_rows() -> List { + [ + surface_row( + authority: InterpreterDispatch, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "v1_interpreter", decl_name: "eval_builtin_inner"), + primitive: primitive_identity_lookup(authority: InterpreterDispatch, authored_symbol: "map_keys"), + provenance: MeasurementOnly, + ), + surface_row( + authority: InterpreterDispatch, + authored_symbol: "map_values", + authority_ref: decl_ref(module_path: "v1_interpreter", decl_name: "eval_builtin_inner"), + primitive: primitive_identity_lookup(authority: InterpreterDispatch, authored_symbol: "map_values"), + provenance: MeasurementOnly, + ), + surface_row( + authority: InterpreterDispatch, + authored_symbol: "fold_list", + authority_ref: decl_ref(module_path: "v1_interpreter", decl_name: "eval_call"), + primitive: primitive_identity_lookup(authority: InterpreterDispatch, authored_symbol: "fold_list"), + provenance: MeasurementOnly, + ), + surface_row( + authority: InterpreterDispatch, + authored_symbol: "index_by", + authority_ref: decl_ref(module_path: "v1_interpreter", decl_name: "eval_algebra_method_inner"), + primitive: primitive_identity_lookup(authority: InterpreterDispatch, authored_symbol: "index_by"), + provenance: MeasurementOnly, + ), + ] +} + +fn primitive_surface_census_derived() -> List { + concat( + concat( + concat(primitive_registry_surface_rows(), primitive_contract_surface_rows()), + primitive_algebra_surface_rows() + ), + primitive_emit_surface_rows() + ) +} + +fn primitive_d0_surface_census() -> List { + concat( + primitive_surface_census_derived(), + primitive_interpreter_dispatch_measurement_rows() + ) +} + +data primitive_map_keys_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { + primitive: primitive_map_keys, + order: HostUnspecifiedOrder, +} + +data primitive_map_values_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { + primitive: primitive_map_values, + order: HostUnspecifiedOrder, +} + +data primitive_fold_list_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { + primitive: primitive_fold_list, + order: SourcePreservingOrder, +} + +data primitive_index_by_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { + primitive: primitive_index_by, + order: TraversalOrderUnclassified, +} + +data primitive_d0_traversal_facts: List = [ + primitive_map_keys_traversal, + primitive_map_values_traversal, + primitive_fold_list_traversal, + primitive_index_by_traversal, +] + +data primitive_map_keys_cost: PrimitiveCostFact = PrimitiveCostFact { + primitive: primitive_map_keys, + cost: ShapeLinearScan, +} + +data primitive_map_values_cost: PrimitiveCostFact = PrimitiveCostFact { + primitive: primitive_map_values, + cost: ShapeLinearScan, +} + +data primitive_fold_list_cost: PrimitiveCostFact = PrimitiveCostFact { + primitive: primitive_fold_list, + cost: ShapeIterateBody, +} + +data primitive_index_by_cost: PrimitiveCostFact = PrimitiveCostFact { + primitive: primitive_index_by, + cost: ShapeIterateBody, +} + +fn primitive_surface_missing_identity_violation(row: PrimitiveSurfaceRow) -> PrimitiveJoinViolation? { + match row.primitive { + Present { value: _ } => none + Absent => + Present { + value: SurfaceMissingPrimitiveIdentity { + authority: row.authority, + authored_symbol: row.authored_symbol, + }, + } + } +} + +fn primitive_surface_row_identity_violation( + row: PrimitiveSurfaceRow, + expected: PrimitiveIdentity, +) -> PrimitiveJoinViolation? { + match row.primitive { + Present { value: id } => + if primitive_identity_eq(left: id, right: expected) { + none + } else { + Present { + value: IncompatibleInvocationAssignment { + authored_symbol: row.authored_symbol, + first: id, + second: expected, + }, + } + } + Absent => + Present { + value: SurfaceMissingPrimitiveIdentity { + authority: row.authority, + authored_symbol: row.authored_symbol, + }, + } + } +} + +fn primitive_surface_joins_two_identities_violation( + left: PrimitiveSurfaceRow, + right: PrimitiveSurfaceRow, +) -> PrimitiveJoinViolation? { + if (left.authored_symbol as String) != (right.authored_symbol as String) { + none + } else { + match left.primitive { + Present { value: first } => + match right.primitive { + Present { value: second } => + if primitive_identity_eq(left: first, right: second) { + none + } else if left.authority == right.authority { + Present { + value: SurfaceJoinsTwoIdentities { + authority: left.authority, + authored_symbol: left.authored_symbol, + first: first, + second: second, + }, + } + } else { + Present { + value: IncompatibleInvocationAssignment { + authored_symbol: left.authored_symbol, + first: first, + second: second, + }, + } + } + Absent => none + } + Absent => none + } + } +} + +fn primitive_incompatible_invocation_assignment_violation( + authored_symbol: String, + first: PrimitiveIdentity, + second: PrimitiveIdentity, +) -> PrimitiveJoinViolation? { + if primitive_identity_eq(left: first, right: second) { + none + } else { + Present { + value: IncompatibleInvocationAssignment { + authored_symbol: authored_symbol as NonEmptyStr, + first: first, + second: second, + }, + } + } +} + +fn primitive_surface_rows_missing_identity_violations( + rows: List +) -> List { + rows |> fold(init: [], f: fn(acc, row) { + match primitive_surface_missing_identity_violation(row: row) { + Present { value: violation } => concat([violation], acc) + Absent => acc + } + }) +} + +fn primitive_definition_identity(definition: PrimitiveDefinition) -> PrimitiveIdentity { + definition.identity +} + +fn primitive_duplicate_semantic_definition_violation( + definitions: List, + target: PrimitiveIdentity +) -> PrimitiveJoinViolation? { + if count( + definitions |> filter(fn(d) { primitive_identity_eq(left: d.identity, right: target) }) + ) > 1 { + Present { value: DuplicateSemanticDefinition { identity: target } } + } else { + none + } +} + +fn primitive_realization_unknown_primitive_violation( + realization: PrimitiveRealization, + definitions: List +) -> PrimitiveJoinViolation? { + let known = definitions + |> any(fn(d) { primitive_identity_eq(left: d.identity, right: realization.primitive) }) + if known { + none + } else { + Present { + value: RealizationNamesUnknownPrimitive { + target: realization.target, + handler: realization.handler, + }, + } + } +} + +fn primitive_d0_derived_rows_missing_identity_count() -> Int { + count(primitive_surface_rows_missing_identity_violations(rows: primitive_surface_census_derived())) +} + +fn primitive_d0_interpreter_measurement_row_count() -> Int { + count(primitive_interpreter_dispatch_measurement_rows()) +} + +fn primitive_d0_open_denominator_receipt_holds() -> Bool { + primitive_d0_derived_surface_authority_count == 4 + && primitive_d0_open_surface_authority_count == 1 + && primitive_interpreter_dispatch_arm_count == 158 + && primitive_interpreter_dispatch_spelling_count == 169 + && primitive_d0_interpreter_measurement_row_count() == 4 + && primitive_d0_derived_rows_missing_identity_count() > 0 +} + +fn primitive_d0_surface_census_row_count() -> Int { + count(primitive_d0_surface_census()) +} + +fn primitive_d0_surface_census_derived_row_count() -> Int { + count(primitive_surface_census_derived()) +} + +fn primitive_d0_surface_census_missing_identity_count() -> Int { + count(primitive_surface_rows_missing_identity_violations(rows: primitive_d0_surface_census())) +} + +fn primitive_d0_surface_census_rows_for( + authority: PrimitiveSurfaceAuthority, + authored_symbol: String, +) -> List { + primitive_d0_surface_census() + |> filter(fn(row) { + row.authority == authority && (row.authored_symbol as String) == authored_symbol + }) +} + +fn primitive_d0_surface_census_row_identity_coherent( + authority: PrimitiveSurfaceAuthority, + authored_symbol: String, + expected: PrimitiveIdentity, +) -> Bool { + let rows = primitive_d0_surface_census_rows_for( + authority: authority, + authored_symbol: authored_symbol, + ) + count(rows) == 1 + && match rows |> first { + Present { value: row } => + match primitive_surface_row_identity_violation(row: row, expected: expected) { + Absent => true + Present { value: _ } => false + } + Absent => false + } +} + +fn primitive_d0_fold_list_spelling_fork_holds() -> Bool { + primitive_d0_surface_census_row_identity_coherent( + authority: PrimitiveContractRow, + authored_symbol: "fold", + expected: primitive_fold_list, + ) + && primitive_d0_surface_census_row_identity_coherent( + authority: InterpreterDispatch, + authored_symbol: "fold_list", + expected: primitive_fold_list, + ) + && !registry_contains_symbol(sym: "fold_list") +} + +fn primitive_d0_index_by_registry_algebra_gap_holds() -> Bool { + !registry_contains_symbol(sym: "index_by") + && !algebra_contains_template_name(name: "index_by") + && contract_contains_name(name: "index_by") + && emit_contains_symbol(sym: "index_by") +} + +fn primitive_d0_fold_list_registry_gap_holds() -> Bool { + !registry_contains_symbol(sym: "fold_list") + && primitive_d0_surface_census_row_identity_coherent( + authority: InterpreterDispatch, + authored_symbol: "fold_list", + expected: primitive_fold_list, + ) +} + +fn primitive_d0_map_keys_five_surface_join_holds() -> Bool { + let rows = primitive_d0_surface_census() + |> filter(fn(row) { (row.authored_symbol as String) == "map_keys" }) + count(rows) == 5 + && rows |> all(fn(row) { + match primitive_surface_row_identity_violation(row: row, expected: primitive_map_keys) { + Absent => true + Present { value: _ } => false + } + }) +} + +fn primitive_d0_interpreter_rows_are_measurement_only() -> Bool { + primitive_interpreter_dispatch_measurement_rows() + |> all(fn(row) { row.provenance == MeasurementOnly }) +} + +fn primitive_d0_derived_rows_are_from_authority() -> Bool { + primitive_surface_census_derived() + |> all(fn(row) { row.provenance == DerivedFromAuthority }) +} + +fn primitive_d0_host_unspecified_traversal_classified() -> Bool { + primitive_d0_traversal_facts + |> all(fn(fact) { + if primitive_identity_eq(left: fact.primitive, right: primitive_map_keys) + || primitive_identity_eq(left: fact.primitive, right: primitive_map_values) { + fact.order == HostUnspecifiedOrder + } else { + true + } + }) +} diff --git a/dag/std/primitives.dag b/dag/std/primitives.dag index 7c731eacbca..8fb746bb8e1 100644 --- a/dag/std/primitives.dag +++ b/dag/std/primitives.dag @@ -517,3 +517,201 @@ data contiguous_loop_elementwise_float_kernel_contract: PrimitiveContract = { certainty: Proven, carrier_cost: CarrierInsensitive } + +data builtin_registry_surface_names_note: String = "Enumerable registry surface names parallel to builtin_function_registry keys. Witness-time census cannot call map_keys on Map because Node is not a runtime Value. Relocated from v1.compiler.infer_method for dag/ compile scope (review 46064) — same parallel-enumeration debt, not a new fork. Dissolve-on: fold builtin_function_registry construction from this list as the single authority." + +fn builtin_registry_surface_names() -> List { + [ + "count", + "string_length", + "code_point", + "to_int", + "scan_while", + "scan_string_end", + "scan_to_eol", + "skip_horizontal_ws", + "parse_int", + "char_at", + "substring", + "from_code_point", + "chars_to_string", + "record_source_chars_index_lookup", + "resolution_silent_pick_is_enabled", + "name_resolution_policy_is_namespace_only", + "resolution_silent_pick_record_global_bare_lcp_pick", + "resolution_silent_pick_record_global_bare_lcp_tie", + "resolution_silent_pick_record_fn_parent_first_hit", + "to_string", + "discriminant", + "concat", + "map_insert", + "map_merge", + "with", + "empty_set", + "set_insert", + "set_union", + "map_contains_key", + "map_has", + "map_is_empty", + "rc_ptr_eq", + "rc_vec_ptr_eq", + "emit_map_has", + "set_contains", + "lookup", + "map_get", + "Some", + "map_keys", + "sorted_map_keys", + "map_values", + "get", + "reverse", + "list_push", + "hash_combine", + "atom_identity_hash", + "trace_mark", + "observed_peak_resident_bytes", + "string_contains", + "length", + "starts_with", + "replace", + "filesystem_read", + "emit_host_run_transport", + "emit_host_run_transport_cached", + "emit_host_native_cache_evict", + "contiguous_loop_elementwise_kernel", + "contiguous_loop_elementwise_float_kernel", + "shell_materialize_operation_argv", + "shell_transport_operation_rows", + "extdeps_shape_transport_policy_facts_for_qualified_name", + "extdeps_qualified_name_resolves_in_derived_module_set", + "extdeps_external_authority_facts_for_qualified_name", + "extdeps_external_authority_live_clean_tree_holds", + "extdeps_external_authority_live_roster_module_count", + "doc_graph_orphan_count", + "doc_graph_admitted_root_count", + "doc_graph_dangling_link_count", + "doc_graph_doc_count", + "compile_dag_rust_emit_check", + "witness_layer_roots_compile_clean_check", + "witness_layer_roots_compile_clean_emit_check", + "consume_floor_compile_clean_gate_verdict", + "witness_compile_clean_cli_floor_verdicts_agree", + "test_migration_debt_module_count", + "test_migration_debt_total_loc", + "test_migration_debt_total_test_fns", + "test_migration_debt_module_names", + "test_migration_debt_known_covered_module_is_not_debt", + "test_migration_delete_guard_holds", + "test_migration_delete_guard_uncovered_deletes", + "inert_carrier_names_live", + "inert_carrier_declared_count", + "inert_lens_unreached_module_count", + "inert_lens_top_level_module_count", + "non_fold_residue_count", + "non_fold_residue_unrostered_count", + "non_fold_residue_stale_roster_count", + "non_fold_residue_coproduct_universe_count", + "commit_witness_claim_roster_unresolvable_count", + "commit_witness_claim_pair_resolvable", + "non_fold_residue_wildcard_red_fixture_holds", + "non_fold_residue_total_fold_green_fixture_holds", + "non_fold_residue_roster_red_fixture_holds", + "non_fold_residue_synthetic_unrostered_red_holds", + "complexity_linearity_syntactic_finding_count", + "complexity_linearity_wildcard_facts", + "complexity_linearity_syntactic_site_fired", + "fallback_arm_census_facts", + "fallback_arm_census_class_count", + "fallback_arm_census_total", + "fallback_arm_census_reconciliation_holds", + "census_corpus_roots_follow_layer_authority", + "transport_script_position_facts_for_path", + "layer_import_facts", + "import_resolution_facts", + "reference_resolution_facts", + "module_declaration_facts", + "concept_decl_facts", + "decl_facts", + "export_signature_facts", + "fact_cardinality_decl_facts", + "languages_consumer_census_data_decl_count", + "languages_consumer_census_per_language_row_count", + "languages_consumer_census_format_row_count", + "languages_consumer_census_external_consumer_count", + "languages_consumer_census_is_composition_only", + "languages_consumer_census_has_external_consumer", + "is_xid_start", + "is_xid_continue", + "is_emoji_ident", + ] +} + +data primitive_contract_roster_note: String = "Hand-maintained parallel enumeration of every *_contract data declaration in this module. A new foo_contract row silently under-reports on primitive_surface_census_derived until this roster is updated — the open-denominator class D0 is designed to expose. Dissolve-on: derive the roster by enumerating *_contract declarations once declaration introspection lands, so contract surfaces read the module rather than a second list." + +fn primitive_contract_roster() -> List { + [ + char_at_contract, + string_length_contract, + substring_contract, + string_contains_contract, + starts_with_contract, + ends_with_contract, + concat_contract, + split_contract, + repeat_contract, + chars_contract, + to_string_contract, + parse_int_contract, + str_eq_contract, + replace_section_contract, + code_point_contract, + from_code_point_contract, + scan_while_contract, + skip_horizontal_ws_contract, + scan_to_eol_contract, + scan_string_end_contract, + map_contract, + filter_contract, + filter_map_contract, + flat_map_contract, + fold_contract, + any_contract, + all_contract, + contains_contract, + join_contract, + sort_contract, + sort_by_contract, + dedup_contract, + len_contract, + count_contract, + sum_contract, + first_contract, + last_contract, + get_contract, + max_by_contract, + reverse_contract, + list_push_contract, + append_contract, + skip_contract, + zip_contract, + enumerate_contract, + empty_map_contract, + map_insert_contract, + map_get_contract, + map_contains_key_contract, + lookup_contract, + map_merge_contract, + map_keys_contract, + map_values_contract, + index_by_contract, + with_contract, + filesystem_read_contract, + to_bytes_contract, + to_json_contract, + hash_contract, + hash_combine_contract, + atom_identity_hash_contract, + contiguous_loop_elementwise_kernel_contract, + contiguous_loop_elementwise_float_kernel_contract, + ] +} diff --git a/dag/test/claim/primitive_identity_join_witness_test.dag b/dag/test/claim/primitive_identity_join_witness_test.dag new file mode 100644 index 00000000000..122d2d71781 --- /dev/null +++ b/dag/test/claim/primitive_identity_join_witness_test.dag @@ -0,0 +1,204 @@ +module test.claim.primitive_identity_join_witness_test + +import std.primitive_identity { + BuiltinRegistry, + DuplicateSemanticDefinition, + InterpreterDispatch, + IncompatibleInvocationAssignment, + PrimitiveContractRow, + RealizationNamesUnknownPrimitive, + SurfaceJoinsTwoIdentities, + SurfaceMissingPrimitiveIdentity, + decl_ref, + primitive_d0_definitions, + primitive_d0_derived_rows_missing_identity_count, + primitive_d0_derived_surface_authority_count, + primitive_d0_fold_list_registry_gap_holds, + primitive_d0_fold_list_spelling_fork_holds, + primitive_d0_derived_rows_are_from_authority, + primitive_d0_host_unspecified_traversal_classified, + primitive_d0_index_by_registry_algebra_gap_holds, + primitive_d0_interpreter_measurement_row_count, + primitive_d0_interpreter_rows_are_measurement_only, + primitive_d0_map_keys_five_surface_join_holds, + primitive_d0_open_denominator_receipt_holds, + primitive_d0_open_surface_authority_count, + primitive_d0_parallel_roster_surface_authority_count, + primitive_d0_surface_census, + primitive_d0_surface_census_derived_row_count, + primitive_d0_traversal_facts, + primitive_fold_list, + primitive_duplicate_semantic_definition_violation, + primitive_identity_eq, + primitive_incompatible_invocation_assignment_violation, + primitive_interpreter_dispatch_arm_count, + primitive_map_keys, + primitive_map_keys_definition, + primitive_map_values, + primitive_realization_unknown_primitive_violation, + primitive_surface_joins_two_identities_violation, + primitive_surface_missing_identity_violation, + PrimitiveRealization, + EmitRust, + MeasurementOnly, + surface_row, +} +import std.primitives { builtin_registry_surface_names } +import std.types { Bool, List, String } + +data primitive_identity_join_witness_note: String = "D0 first slice (NOT closing contract): join mechanism + five refusal variants typed, three detectors executing on census plus two scaffold detectors on planted RED inputs (primitive_d0_refusal_execution_note); subject universe derived across four surfaces, OPEN at fifth (InterpreterDispatch). primitive_interpreter_dispatch_measurement_rows is interim measurement scaffold with dissolution trigger interpreter-primitive-roster — NOT an authority. Open denominator counted by primitive_d0_open_denominator_receipt_holds and primitive_d0_derived_rows_missing_identity_count." + +test fn w_open_denominator_counted_receipt() -> Bool { + primitive_d0_open_denominator_receipt_holds() + && primitive_d0_derived_surface_authority_count == 4 + && primitive_d0_parallel_roster_surface_authority_count == 2 + && primitive_d0_open_surface_authority_count == 1 + && primitive_interpreter_dispatch_arm_count == 158 + && primitive_d0_interpreter_measurement_row_count() == 4 + && primitive_d0_derived_rows_missing_identity_count() > 0 +} + +test fn w_derived_surface_census_population() -> Bool { + let registry_rows = count(builtin_registry_surface_names()) + let derived_rows = primitive_d0_surface_census_derived_row_count() + derived_rows > registry_rows && derived_rows > 100 +} + +test fn w_interpreter_measurement_rows_marked_measurement_only() -> Bool { + primitive_d0_interpreter_rows_are_measurement_only() +} + +test fn w_derived_rows_marked_derived_from_authority() -> Bool { + primitive_d0_derived_rows_are_from_authority() +} + +test fn w_map_keys_joins_all_five_surfaces() -> Bool { + primitive_d0_map_keys_five_surface_join_holds() +} + +test fn w_fold_list_spelling_fork_named_finding() -> Bool { + primitive_d0_fold_list_spelling_fork_holds() +} + +test fn w_fold_list_registry_gap_proves_open_denominator() -> Bool { + primitive_d0_fold_list_registry_gap_holds() +} + +test fn w_index_by_registry_algebra_gap_named_finding() -> Bool { + primitive_d0_index_by_registry_algebra_gap_holds() +} + +test fn w_unknown_realization_refuses() -> Bool { + match primitive_realization_unknown_primitive_violation( + realization: PrimitiveRealization { + primitive: primitive_map_keys, + target: EmitRust, + handler: decl_ref(module_path: "std.primitive_identity", decl_name: "missing_handler"), + }, + definitions: [], + ) { + Present { value: RealizationNamesUnknownPrimitive { target: _, handler: _ } } => true + Absent => false + } +} + +test fn w_duplicate_semantic_definition_refuses() -> Bool { + match primitive_duplicate_semantic_definition_violation( + definitions: primitive_d0_definitions, + target: primitive_map_keys, + ) { + Present { value: _ } => false + Absent => true + } + && match primitive_duplicate_semantic_definition_violation( + definitions: [primitive_map_keys_definition, primitive_map_keys_definition], + target: primitive_map_keys, + ) { + Present { value: DuplicateSemanticDefinition { identity } } => + primitive_identity_eq(left: identity, right: primitive_map_keys) + Absent => false + } +} + +test fn w_host_unspecified_traversal_classified_for_map_projections() -> Bool { + primitive_d0_host_unspecified_traversal_classified() + && count(primitive_d0_traversal_facts) == 4 +} + +test fn w_red_missing_identity_on_joined_surface() -> Bool { + let planted = surface_row( + authority: InterpreterDispatch, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "v1_interpreter", decl_name: "eval_builtin_inner"), + primitive: Absent, + provenance: MeasurementOnly, + ) + match primitive_surface_missing_identity_violation(row: planted) { + Present { value: SurfaceMissingPrimitiveIdentity { authority, authored_symbol } } => + authority == InterpreterDispatch && (authored_symbol as String) == "map_keys" + Absent => false + } +} + +test fn w_red_surface_joins_two_identities() -> Bool { + let left = surface_row( + authority: BuiltinRegistry, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "std.primitives", decl_name: "builtin_registry_surface_names"), + primitive: Present { value: primitive_map_keys }, + provenance: MeasurementOnly, + ) + let right = surface_row( + authority: BuiltinRegistry, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "std.primitives", decl_name: "builtin_registry_surface_names"), + primitive: Present { value: primitive_map_values }, + provenance: MeasurementOnly, + ) + match primitive_surface_joins_two_identities_violation(left: left, right: right) { + Present { value: SurfaceJoinsTwoIdentities { authority, authored_symbol, first, second } } => + authority == BuiltinRegistry + && (authored_symbol as String) == "map_keys" + && primitive_identity_eq(left: first, right: primitive_map_keys) + && primitive_identity_eq(left: second, right: primitive_map_values) + Absent => false + } +} + +test fn w_red_cross_authority_identity_fork() -> Bool { + let registry_row = surface_row( + authority: BuiltinRegistry, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "std.primitives", decl_name: "builtin_registry_surface_names"), + primitive: Present { value: primitive_map_keys }, + provenance: MeasurementOnly, + ) + let contract_row = surface_row( + authority: PrimitiveContractRow, + authored_symbol: "map_keys", + authority_ref: decl_ref(module_path: "std.primitives", decl_name: "map_keys_contract"), + primitive: Present { value: primitive_map_values }, + provenance: MeasurementOnly, + ) + match primitive_surface_joins_two_identities_violation(left: registry_row, right: contract_row) { + Present { value: IncompatibleInvocationAssignment { authored_symbol, first, second } } => + (authored_symbol as String) == "map_keys" + && primitive_identity_eq(left: first, right: primitive_map_keys) + && primitive_identity_eq(left: second, right: primitive_map_values) + Absent => false + } +} + +test fn w_red_incompatible_invocation_assignment() -> Bool { + match primitive_incompatible_invocation_assignment_violation( + authored_symbol: "keys", + first: primitive_map_keys, + second: primitive_map_values, + ) { + Present { value: IncompatibleInvocationAssignment { authored_symbol, first, second } } => + (authored_symbol as String) == "keys" + && primitive_identity_eq(left: first, right: primitive_map_keys) + && primitive_identity_eq(left: second, right: primitive_map_values) + Absent => false + } +} diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index aa5e31a04e6..867a4b1baa8 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -1558,22 +1558,13 @@ pub fn partial_function_templates() -> Rc>> { pub fn algebra_method_template_name(name: String) -> bool { { let mut __found = false; - for p in Rc::new(vec![ - AlgebraProfile::OrderedRingProfile, - AlgebraProfile::ApproximateFieldProfile, - AlgebraProfile::BooleanAlgebraProfile, - AlgebraProfile::BooleanAlgebraCollectionProfile, - AlgebraProfile::PointwisePowerCollectionProfile, - AlgebraProfile::FreeMonoidScalarProfile, - AlgebraProfile::FreeMonoidCollectionProfile, - AlgebraProfile::PartialFunctionProfile, - ]) - .iter() - .cloned() - { + for profile in all_algebra_profiles().iter().cloned() { if { let mut __found = false; - for t in algebra_templates_for_profile(p.clone()).iter().cloned() { + for t in algebra_templates_for_profile(profile.clone()) + .iter() + .cloned() + { if (t.name.clone() == name.clone()) { __found = true; break; @@ -1615,6 +1606,43 @@ pub fn algebra_type_param_names(profile: AlgebraProfile) -> Rc> { } } +pub fn all_algebra_profiles() -> Rc> { + Rc::new(vec![ + AlgebraProfile::OrderedRingProfile, + AlgebraProfile::ApproximateFieldProfile, + AlgebraProfile::BooleanAlgebraProfile, + AlgebraProfile::BooleanAlgebraCollectionProfile, + AlgebraProfile::PointwisePowerCollectionProfile, + AlgebraProfile::FreeMonoidScalarProfile, + AlgebraProfile::FreeMonoidCollectionProfile, + AlgebraProfile::PartialFunctionProfile, + ]) +} + +pub fn all_algebra_field_templates() -> Rc>> { + Rc::new({ + let mut __result = Vec::new(); + for profile in all_algebra_profiles().iter().cloned() { + __result.extend( + (*algebra_templates_for_profile(profile.clone())) + .iter() + .cloned(), + ); + } + __result + }) +} + +pub fn all_algebra_template_names() -> Rc> { + Rc::new({ + let mut __result = Vec::new(); + for template in all_algebra_field_templates().iter().cloned() { + __result.push(template.name.clone()); + } + __result + }) +} + #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct Less; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]