diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index ae2ca155828..737903c0af4 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -1,6 +1,6 @@ module gunbc.heal_revalidation -import std.content_hash { Fnv1a64Structural } +import std.content_hash { ContentHash } import std.types { CommitSha, NonEmptyStr } import gunbc.merge_admission { CheckCoverage, @@ -135,8 +135,8 @@ fn classify_workflow_dispatch_preflight( fn classify_heal_revalidation_admission( state: HealRevalidationState, - required_roster: Fnv1a64Structural, - required_gates: List, + required_roster: ContentHash, + required_gates: List, ) -> HealRevalidationAdmissionVerdict { match state { HealRevalidationNotRequired { head } => @@ -166,8 +166,8 @@ fn classify_heal_revalidation_admission( fn heal_revalidation_admits( state: HealRevalidationState, - required_roster: Fnv1a64Structural, - required_gates: List, + required_roster: ContentHash, + required_gates: List, ) -> Bool { match classify_heal_revalidation_admission( state: state, diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag new file mode 100644 index 00000000000..fc7d87256d6 --- /dev/null +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -0,0 +1,139 @@ +module test.claim.declared_type_inhabitance_direct_call_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE-ONLY BY DELIBERATE CHOICE, AND THE SIBLING FILE EXPLAINS WHY IN ITS OWN VOICE. +// test.claim.direct_call_argument_type_witness records that an assertion authored in a +// ReadsLiveTree module is "enrolled and inert -- the specification-without-execution state +// DESIGN 5 names, wearing the costume of a populated probe corpus", because a ReadsLiveTree +// witness is discovered, counted in declined_live, and never folded. These arms are the +// regression control for a discrimination that must not decay, so they are authored where the +// floor actually folds them. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn violation_count(source: String, wanted: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// THE PAIR THIS FILE EXISTS FOR. std.nat and v2.std.nat both declare a type spelled Nat and they +// are NOT the same concept: std.nat.Nat is CommutativeSemiring and realizes natively +// as a kernel integer, while v2.std.nat.Nat is the Peano coproduct Zero | Succ { prev: Nat }. +// v1.compiler.coercion numeric_realization_identity_note names this exact pair as the hazard a +// bare-name rule gets wrong. +// +// declared_type_inhabitance admits a kernel numeric at the FIRST by consulting +// decl_file_realizes_natively, which is keyed on the resolved DECLARING MODULE. If that +// discrimination ever decays to a spelling comparison, the RED arm below admits and goes green, +// which is the whole point of enrolling it: DESIGN 4b(4) keeps the evidence after a climb +// precisely so the higher rung stays real. + +// RED, AND CURRENTLY FAILING -- ENROLLED IN v2.workflow.floor_expected_red rather than fixed. +// A kernel integer at the PEANO Nat. 5 is not Zero and not Succ and no realization row covers +// src/v2/std/nat.dag, so this OUGHT to refuse. It does not, and the control run on 2026-08-23 +// establishes that it never did: gunbc built from origin/main 907f19c2cc7 admits this source +// exactly as the branch does. The refusal was ASSERTED here, not broken by this change. +// The enrolment row carries the full branch-and-main control table and the next-rung trigger. +data peano_nat_arg_source: String = "module probe_inhabit_peano\nimport v2.std.nat { Nat }\nfn takes_peano(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_peano(n: 5) }\n" + +test fn w_kernel_numeric_at_the_peano_nat_is_refused() -> Bool { + violation_count(source: peano_nat_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// GREEN -- the same literal at the NATIVE Nat. Structurally this is a kernel value at an +// algebraic record and reads identically to the arm above; only the declaring module differs. +// It must be admitted, and admitted SILENTLY: the class is decidable, so there is no residue to +// count and nothing here asserts one. +data native_nat_arg_source: String = "module probe_inhabit_native\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: 40) }\n" + +test fn w_kernel_numeric_at_the_natively_realized_nat_is_admitted() -> Bool { + violation_count(source: native_nat_arg_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// THE ADMISSION IS WRITTEN AS A CONJUNCTION -- the declared side must realize natively AND the +// produced value must be a kernel numeric -- and this arm is the control for the second half. +// IT IS CURRENTLY FAILING AND ENROLLED AS A KNOWN RED. A String at the natively-realized Nat is +// admitted, by this branch and by main alike, so the second half of the conjunction is not +// enforced anywhere downstream of declared_type_inhabitance: the consumed predicate +// kernel_value_declared_type_mismatch does not fire for a kernel value at ANY type application. +// Nat is not the specimen that makes this legible -- a String reaching a List parameter is, +// and Map admits one too, so it is not about arity and not about algebra. That is a +// pre-existing gap, older than this branch, and the enrolment row in v2.workflow.floor_expected_red +// carries the five-probe table and names it as this class's next-rung trigger. +data string_at_native_nat_source: String = "module probe_inhabit_native_str\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: \"forty\") }\n" + +test fn w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused() -> Bool { + violation_count(source: string_at_native_nat_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// REACHABILITY, ON A DIFFERENT CLASS THAN THE WALL'S. An undefined name at the same argument +// position must be refused by SOMETHING, or the two accepting arms above cannot distinguish "the +// position is judged and the value was admitted" from "the position is never reached". An +// unresolved value name is refused through inference_error, which constructs +// InternalError { message } -- measured, not assumed. +data undefined_name_arg_source: String = "module probe_inhabit_dc_reach\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: nosuchname_zzz_dc) }\n" + +test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { + violation_count(source: undefined_name_arg_source, wanted: "InternalError") > 0 +} + +// THE LIST-ELEMENT GAP, AUTHORED AS A FIXTURE SO THE PRODUCTION SITE CAN BE REPAIRED. +// dag/gunbc/heal_revalidation.dag passed List into check_coverage_admits's +// required_gates: List -- the same mismatch as the argument beside it, one level +// inside a list -- and this relation did NOT name it. That silence was the only evidence the +// gap existed, which made repairing the production site look like consuming the evidence. +// DESIGN 4b(4) separates those: a climb deletes the redundant PRODUCTION handling and KEEPS the +// discriminating RED as enrolled evidence. So the evidence lives here, where it is reproducible +// on demand, and the live wrong argument in an admission path is repaired. +// +// GREEN, AND THE CLAIM IT WAS BUILT TO DOCUMENT IS WITHDRAWN. A kernel String at a coproduct +// element type inside a list at a direct-call argument IS REFUSED. Measured, run 32667623528. +// +// THIS PAIR WAS AUTHORED TO DOCUMENT A GAP THAT DOES NOT EXIST. The relation descends into a +// list literal's elements at this position and always did; it is kept as a permanent regression +// control over that fact rather than deleted, per DESIGN 4b(4) -- evidence stays enrolled as +// evidence once a wall is shown real. +// +// WHY IT LOOKED LIKE A GAP, and the distinction is the whole correction: the site that started +// this was dag/gunbc/heal_revalidation.dag passing a List VARIABLE into a +// List parameter. That is list-typed-value compatibility, and the relation answers +// Undecidable for a generic carrier BY DESIGN. This probe instead passes a list LITERAL with a +// wrong element, which is a different judgment and one the relation makes. I inferred the second +// from the silence on the first. THE LIST-TYPED-VALUE CASE REMAINS UNMEASURED and no arm here +// claims anything about it. +// +// THE PRODUCED VALUE IS A KERNEL STRING BECAUSE THE FIRST VERSION OF THIS PAIR USED A RECORD +// LITERAL AND ITS CONTROL WENT RED, which is the only reason the mis-design was caught rather +// than enrolled. kernel_value_declared_type_mismatch judges only a KERNEL produced value -- +// is_kernel_type(actual_name) gates its whole body -- so a record literal at a coproduct is not +// judged AT ANY POSITION, list or not. The old pair therefore measured "records are never +// judged" and would have been enrolled as evidence about lists. A String is judged at this +// position by execution (measured: a String at a closed coproduct REFUSES), so the list is now +// the only difference between the two arms. +data record_element_in_list_arg_source: String = "module probe_inhabit_dc_list_elem\nimport std.types { Int, String, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\nfn takes_list(xs: List) -> Int { 1 }\nfn probe() -> Int { takes_list(xs: [\"forty\"]) }\n" + +test fn w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused() -> Bool { + violation_count(source: record_element_in_list_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// THE CONTROL THAT MAKES THAT RED READABLE, and it separates "the relation cannot judge this +// pair" from "the relation cannot see inside a list". SAME two types, SAME direct-call argument +// position, the String passed DIRECTLY rather than wrapped in a list. If this refuses and the +// arm above does not, the list is the whole difference. If this also admits, the probe proves +// nothing about lists and the arm above is measuring the wrong thing -- which is exactly what +// happened to this pair's first version, so this arm is not a formality. +data record_directly_at_coproduct_arg_source: String = "module probe_inhabit_dc_bare_elem\nimport std.types { Int, String, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\nfn takes_one(x: Cop) -> Int { 1 }\nfn probe() -> Int { takes_one(x: \"forty\") }\n" + +test fn w_the_same_wrong_pair_directly_at_the_argument_is_refused() -> Bool { + violation_count(source: record_directly_at_coproduct_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag new file mode 100644 index 00000000000..25b0a6312d1 --- /dev/null +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -0,0 +1,138 @@ +module test.claim.declared_type_inhabitance_list_element_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE-ONLY, AND THE EARLIER ReadsLiveTree DECLARATION MADE EVERY ARM BELOW INERT. A +// ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED -- so these +// arms were enrolled, reviewed, cited as this PR's executable evidence, and executed by nothing. +// That is the specification-without-execution trap DESIGN 5 calls the deepest one, and it is +// worse here than a missing test would have been, because the arms were named as the reason the +// class had climbed. The sibling test.claim.direct_call_argument_type_witness had already made +// this exact move and said why: an assertion in a live-tree module is "enrolled and inert ... +// wearing the costume of a populated probe corpus". This file needs no live read -- every arm +// hands compile_dag_diagnostic_census a source STRING it authors itself -- so nothing is lost by +// declaring what it actually consumes. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that +// declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression +// rather than a missing nicety, and it is not softened to mitigatable anywhere in this file. +// +// WHY ONE CARRIER AND NOT ONE CHECK PER POSITION. The grammar has fourteen type positions; +// twelve can receive a source value. Before the obligation carrier, each position that judged +// anything judged it with its own local chain of predicates -- one rule in N representations, +// where a position added later inherits nothing and a rule repaired at one position stays +// broken at the rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was +// declared and WHAT was produced; declared_type_inhabitance is the single relation that +// decides; the position rides along so the diagnostic can locate the refusal without the +// decision procedure forking. This file is the executing evidence for the FIRST position wired +// through that carrier, and its arms are the shape every later position reuses. +// +// THE RELATION CONSUMES, IT DOES NOT RE-DERIVE. Alias identity is decided once in the tree: +// coproduct_payload_where_parent_required peels transparent aliases through +// transparent_alias_identity_agrees, and the kernel arm defers to +// kernel_value_declared_type_mismatch. A second answer to either question authored here would +// be the nicknaming failure at the level of judgments. +// +// PATH SCOPE, per DESIGN 4b's rung-per-path rule: this asserts source -> .dag acceptance only. +// The refusal sits in inference, so nothing reaches emission with a non-inhabiting list +// element -- but that is a consequence of where the wall sits, not a second measurement, and +// it is not claimed as one. + +fn violation_count(source: String, wanted: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// RED ARM ONE -- the plain kernel at a structured declared type. This is the floor case, and it +// is in this file because the FIRST wiring of the carrier ACCEPTED it: the relation consulted +// only the payload-at-parent predicate, so RefusedKernelAtStructured was a declared verdict +// variant that no code path could produce. A variant nothing constructs is a decoration that +// reads as coverage, which is the rung inflation DESIGN 4b names. This arm exists so that +// deleting the kernel route from the relation goes red rather than quiet. +data kernel_at_structured_source: String = "module probe_inhabit_nega\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [7] }\n" + +test fn w_plain_kernel_at_declared_list_element_is_refused() -> Bool { + violation_count(source: kernel_at_structured_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// RED ARM TWO -- an arm's PAYLOAD type standing where the PARENT coproduct is declared. The +// shape gunbc#8865 recorded, measured here at the list-element position rather than inferred +// from the record-field one: two positions are two paths, and a wall proven at one says +// nothing about the other. +data payload_at_parent_source: String = "module probe_inhabit_negb\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk_inner() -> Inner { Inner { v: 1 } }\nfn probe() -> List { [mk_inner()] }\n" + +test fn w_arm_payload_where_parent_declared_is_refused() -> Bool { + violation_count(source: payload_at_parent_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// GREEN ARM -- the control that stops the wall being a wrecking ball. A genuine member of the +// declared coproduct must still compile and must raise NO inhabitance diagnostic. Without it, +// a relation that refused every list element would score identically on both red arms above, +// and the reds would establish nothing. +data inhabiting_member_source: String = "module probe_inhabit_pos\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [SameRev] }\n" + +test fn w_declared_coproduct_member_is_accepted() -> Bool { + violation_count(source: inhabiting_member_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// REACHABILITY -- an undefined name at the same position must refuse whether or not the +// inhabitance wall exists. This separates "the position is judged and the value was refused" +// from "the position is never reached at all", which the accepting arms above cannot +// distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately: +// keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. +// +// THE ASSERTION MUST BE POSITIVE, AND AN EARLIER REVISION OF IT WAS NOT. This arm shipped +// asserting DeclaredTypeNotInhabited == 0 -- the wall's OWN class, at zero -- while the prose +// above claimed it keyed on a different one. That assertion is satisfied identically by "the +// position is judged and our wall correctly stayed silent" and by "the position is never +// reached by anything", which is precisely the distinction the arm exists to make, so it read +// as coverage while carrying none. It is DESIGN's reachability-read-as-occupancy failure +// turned on a control: a zero is only readable beside a nonzero. Corrected to demand the +// refusal it was named for (review 54993). +// +// WHY InternalError IS THE CLASS: an unresolved value name is refused by v1.compiler.04_infer +// through inference_error, which constructs InternalError { message } -- measured, not assumed +// ("undefined variable 'nosuchname_zzz_probe'" against this exact source). It is coarser than +// the shape deserves, and that coarseness is why the paired green arm below is not optional: +// alone, a positive InternalError count could be produced by any unrelated defect in the +// probe. The pair is what makes the undefined NAME the thing being measured. +data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [nosuchname_zzz_probe] }\n" + +// The same source with the name DEFINED and nothing else changed. It is the discriminator for +// the arm above: if this also reported InternalError, the positive count there would be an +// artifact of the probe rather than evidence about the name. +data defined_name_source: String = "module probe_inhabit_reach_ok\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk() -> Rel { SameRev }\nfn probe() -> List { [mk()] }\n" + +test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { + violation_count(source: undefined_name_source, wanted: "InternalError") > 0 + && violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +test fn w_reachability_control_discriminates_on_the_name() -> Bool { + violation_count(source: defined_name_source, wanted: "InternalError") == 0 + && violation_count(source: defined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the +// declared position is genuinely undecidable at this seam -- optionality lives in +// return_cardinality while the produced value carries the nominal coproduct, so the two are +// not comparable here without peeling a representation this relation does not own. It must +// therefore NOT refuse. This arm is what keeps Undecidable honest: if the relation ever starts +// refusing optionals it goes red, and if a future author repurposes an Undecidable reason to +// mean "unimplemented" this is the arm that notices. +data optional_carrier_source: String = "module probe_inhabit_opt\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn maybe() -> Rel? { none }\nfn probe() -> List { [maybe()] }\n" + +test fn w_optional_carrier_is_undecidable_not_refused() -> Bool { + violation_count(source: optional_carrier_source, wanted: "DeclaredTypeNotInhabited") == 0 +} diff --git a/dag/test/claim/materialization_provider_witness_test.dag b/dag/test/claim/materialization_provider_witness_test.dag index feb4945dd50..97d0fe672a4 100644 --- a/dag/test/claim/materialization_provider_witness_test.dag +++ b/dag/test/claim/materialization_provider_witness_test.dag @@ -6,6 +6,8 @@ import std.content_hash { Fnv1a64, content_hash_atom, as_content_hash_cryptographic, + as_content_hash_structural, + Fnv1a64Structural, sha256_hex_digest, } import std.interface_summary { InterfaceHash, module_key, typed_module_key } @@ -258,26 +260,26 @@ test fn red_sha256_at_fnv1a64_seam_refuses_without_alias() -> Bool { Present { value: sha_b } => { let refused_a = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_a), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) let refused_b = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_b), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) lookup_is_refused_cross_family_content_hash(l: refused_a) @@ -411,7 +413,7 @@ test fn red_admission_wrong_content_is_refused() -> Bool { store: witness_empty_store(budget_count: 1000), req: witness_closure_request(), artifact: witness_complete_closure_artifact(), - observed_digest: content_hash_atom(value: "closure-payload-corrupt") + observed_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-payload-corrupt")) ) admission_is_refused_wrong_content_write(a: a) && (admission_is_admitted(a: a) == false) } @@ -457,7 +459,7 @@ fn witness_size_understated_closure_artifact() -> MaterializedArtifact { } } -fn witness_hash_list_contains(xs: List, wanted: ContentHash) -> Bool { +fn witness_hash_list_contains(xs: List, wanted: Fnv1a64Structural) -> Bool { xs |> fold(init: false, f: (acc, x) => acc || (x == wanted)) } diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index 1c8942b10b6..0fcb5c02332 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -196,6 +196,8 @@ type CompilerDiagnostic span: SourceSpan } | AdmitCallersEntryNotDeclRef { constructor_decl_name: String, span: SourceSpan } + | DeclaredTypeNotInhabited { position: String, expected: String, got: String, span: SourceSpan } + | DeclaredTypeInhabitanceUndecided { position: String, reason: String, span: SourceSpan } | UnlistedImportUse { name: String, span: SourceSpan } | AmbiguousReference { name: String, candidates: List, span: SourceSpan } | AmbiguousAnonymousRecordLiteral { candidates: List, span: SourceSpan } @@ -343,6 +345,8 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan { span: s } => s AdmitCallersEntryNotDeclRef { constructor_decl_name: _, span: s } => s + DeclaredTypeNotInhabited { position: _, expected: _, got: _, span: s } => s + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: s } => s UnlistedImportUse { name: _, span: s } => s AmbiguousReference { name: _, candidates: _, span: s } => s AmbiguousAnonymousRecordLiteral { candidates: _, span: s } => s @@ -419,6 +423,10 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String { ) AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, span: _ } => concat("admit_callers entry on '", cn, "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored") + DeclaredTypeNotInhabited { position: pos, expected: e, got: g, span: _ } => + concat("value does not inhabit its declared type at the ", pos, ": declared '", e, "', produced '", g, "'") + DeclaredTypeInhabitanceUndecided { position: pos, reason: r, span: _ } => + concat("declared-type inhabitance is undecidable at the ", pos, " (", r, "): the modeled facts do not settle whether the produced value inhabits its declared type, so no verdict is asserted in either direction") UnlistedImportUse { name: n, span: _ } => concat("unlisted import use '", n, "' (referenced but not in any import's name list)") AmbiguousReference { name: n, candidates: cs, span: _ } => concat("ambiguous reference '", n, "': ", to_string(value: cs |> count), " candidates: ", join(cs, separator: ", "), " — qualify by containment path, alias, or rename") AmbiguousAnonymousRecordLiteral { candidates: cs, span: _ } => concat("ambiguous anonymous record literal shape matches ", to_string(value: cs |> count), " structs: ", join(cs, separator: ", "), " — add a nominal type") @@ -493,6 +501,7 @@ fn is_interpreter_blocking_diagnostic(d: CompilerDiagnostic) -> Bool { MethodExistenceFrontierAdmitted { method: _, receiver_type: _, trigger: _, span: _ } => false ReceiverTypeUnestablished { method: _, span: _ } => false ServiceConfigReferenceJudgmentDeferred { field: _, referenced_name: _, trigger: _, span: _ } => false + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: _ } => false _ => true } } @@ -503,6 +512,7 @@ fn is_discovery_corpus_advisory_typecheck_diagnostic(d: CompilerDiagnostic) -> B MethodExistenceFrontierAdmitted { method: _, receiver_type: _, trigger: _, span: _ } => true ReceiverTypeUnestablished { method: _, span: _ } => true ServiceConfigReferenceJudgmentDeferred { field: _, referenced_name: _, trigger: _, span: _ } => true + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: _ } => true WhereRefinementUnenforced { predicate: _, formal_type: _, reason: r, span: _ } => is_where_refinement_unenforced_advisory_reason(reason: r) _ => false diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 5e13db023b4..27751211639 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -97,6 +97,7 @@ import v1.compiler.infer_method { builtin_kernel_seed_diagnostics, infer_builtin_call_type, resolve_builtin_call_type } import v1.compiler.infer_cycle { detect_type_cycles_kahn } +import v1.compiler.coercion { decl_file_realizes_natively, type_reference_decl_file } import v1.compiler.infer_env { TypeEnv, TypeBinding, TypeEnvCache, empty_type_env_cache, merge_type_env_cache, merge_type_env_cache_guarded, GuardedTypeEnvCacheMerge, TypeEnvCacheMergeConflict, @@ -2386,6 +2387,238 @@ fn foreign_concrete_coproduct_where_parent_required( // makes "the actual is one of this coproduct's payload types" undecidable from the declaration // alone; refusing there would be a fabricated refusal, which DESIGN section 5 forbids exactly as it // forbids a fabricated success. +// ONE OBLIGATION, ONE AUTHORITY. The grammar has fourteen type positions and twelve of them +// can receive a source value. Before this carrier each position that judged anything judged it +// with its own local chain of else-if predicates, which is one rule in N representations: a +// position added later inherits nothing, and a rule fixed at one position stays broken at the +// rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was declared and WHAT +// was produced; declared_type_inhabitance is the single relation that decides; the position +// travels with the obligation so the diagnostic can locate the refusal without the decision +// procedure forking per position. +// TWO OF THE TWELVE ARE WIRED. THE OTHER TEN ARE DECLARED HERE AND PRODUCE NOTHING YET, AND +// THAT IS STATED AS A COUNT RATHER THAN LEFT TO BE DISCOVERED FROM THE ABSENCE OF CALLERS. +// Measured by construction site, not by reading: PositionDirectCallArgument and +// PositionListElement are the only two members CONSTRUCTED anywhere -- every other member +// occurs solely in declared_type_position_label's match, which renders a name and judges +// nothing. So this coproduct is today an OBLIGATION VOCABULARY, of which two positions have a +// producer. +// +// WHY THAT IS NOT AN UNDECIDABLE ARM AND MUST NEVER BE FILED AS ONE: an unwired position is a +// MISSING OBLIGATION PRODUCER, not a fact the model cannot settle. It is absent from the census +// rather than present with a verdict -- so it produces no diagnostic, blocking or advisory, and +// nothing in the corpus is red on its account. Recording these as expected-red rows would be +// exactly the rung inflation 4b names, since there is no red to expect; and recording them as +// InhabitanceUndecidable would report "we did not look" as "it cannot be decided", which is the +// same inflation aimed at this relation's own self-description. +// +// NEXT-RUNG TRIGGER, one per position and all the same shape: a producer at that grammar seam +// that builds a DeclaredTypeObligation and hands it to declared_type_obligation_diags. The +// decision procedure is already shared and position-agnostic, so wiring one is authoring a +// construction site, never extending this relation -- which is the whole point of the carrier +// and is why the residual ten cost a call each rather than a rule each. +// +// THE TEN AWAITING A PRODUCER: PositionRecordLiteralField, PositionMapValue, +// PositionDataInitializer, PositionDeclaredReturn, PositionLetAnnotation, PositionVariantPayload, +// PositionGenericTypeArgument, PositionCastTarget, PositionParameterDefault, +// PositionCallableReturn. Wiring any of them is a separate change with its own evidence: a +// discriminating RED at that seam plus an accepted positive control, per 4b(1). Until then this +// carrier's honest claim is TWO POSITIONS JUDGED, ten declared -- and any statement that it +// judges "every grammar type position" is false. +type DeclaredTypePosition + = PositionRecordLiteralField + | PositionListElement + | PositionMapValue + | PositionDataInitializer + | PositionDeclaredReturn + | PositionLetAnnotation + | PositionVariantPayload + | PositionGenericTypeArgument + | PositionCastTarget + | PositionParameterDefault + | PositionCallableReturn + | PositionDirectCallArgument + +type DeclaredTypeObligation { + position: DeclaredTypePosition + declared: Node + produced: Node + span: SourceSpan +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. Each reason names something the +// modeled facts genuinely cannot settle at this seam. A position that has not been wired yet is +// NOT undecidable -- it is a missing obligation producer, and it is absent from the census +// rather than present with a verdict. Reading "we did not look" as "it cannot be decided" is +// the rung inflation DESIGN 4b names, applied to this relation's own self-description. +type InhabitanceUndecidableReason + = UndecidableGenericFormal + | UndecidableOptionalCarrier + | UndecidableFormalUnresolved + | UndecidableProducedIdentityErased + +type InhabitanceRefusalReason + = RefusedPayloadAtParent + | RefusedKernelAtStructured + +type InhabitanceVerdict + = Inhabits + | InhabitanceRefused { reason: InhabitanceRefusalReason } + | InhabitanceUndecidable { reason: InhabitanceUndecidableReason } + +fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position { + PositionRecordLiteralField => "record literal field" + PositionListElement => "list element" + PositionMapValue => "map value" + PositionDataInitializer => "data initializer" + PositionDeclaredReturn => "declared return" + PositionLetAnnotation => "let annotation" + PositionVariantPayload => "variant payload" + PositionGenericTypeArgument => "generic type argument" + PositionCastTarget => "cast target" + PositionParameterDefault => "parameter default" + PositionCallableReturn => "callable return" + PositionDirectCallArgument => "direct call argument" + } +} + +// THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating +// them: coproduct_payload_where_parent_required already peels transparent aliases through +// transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the +// tree and this relation inherits it instead of re-deriving a second answer. +fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferScope) -> InhabitanceVerdict { + let declared = obligation.declared + let produced = obligation.produced + let source_indices = scope.type_env.source_indices + let declared_name = authored_name_at(source_indices: source_indices, node: declared) + let produced_name = authored_name_at(source_indices: source_indices, node: produced) + let either_optional = declared.return_cardinality == CardOptional || produced.return_cardinality == CardOptional + let declared_is_generic = (declared.params |> count) > 0 + if either_optional { + InhabitanceUndecidable { reason: UndecidableOptionalCarrier } + } else if declared_is_generic { + InhabitanceUndecidable { reason: UndecidableGenericFormal } + } else if declared_name == "" { + InhabitanceUndecidable { reason: UndecidableFormalUnresolved } + } else if produced_name == "" { + InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if declared_realizes_as_kernel_numeric( + declared: declared, produced: produced, source_indices: source_indices) { + Inhabits + } else if kernel_value_declared_type_mismatch( + formal: declared, actual: produced, + type_env: scope.type_env, source_indices: source_indices) { + InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { + InhabitanceRefused { reason: RefusedPayloadAtParent } + } else { + Inhabits + } +} + +// The obligation carries its own position, so ONE emitter locates every refusal. A per-position +// diagnostic function would be the N-representation problem moved one layer down. +// WHY A KERNEL LITERAL AT AN ALGEBRAICALLY-DECLARED NUMERIC IS ADMITTED, AND WHY THIS IS +// CONSULTING AN AUTHORITY RATHER THAN WIDENING AN ARM. std.nat declares +// `type Nat = CommutativeSemiring` and std.integer declares +// `type Int = AbelianGroup>`: the canonical form of both is an algebraic +// STRUCTURE while their values are authored as kernel integer literals. Read structurally that +// is kernel-at-structured and the relation refused it -- measured, 33 of 50 sites at the +// direct-call seam, every one correct code. +// +// The corpus does not leave this to convention. v1.compiler.coercion +// numeric_realization_declaring_modules records that exactly these declaring modules realize +// natively, and decl_file_realizes_natively answers it. So the class was never undecidable, it +// was UNCONSULTED -- which is why nothing here is counted: a residue would record a deficit +// that does not exist. +// +// THREE PROPERTIES THIS RELIES ON, none of them incidental: +// IDENTITY, NOT SPELLING. The authority is keyed on the resolved declaring module. +// numeric_realization_identity_note names the exact hazard: std.nat.Nat realizes natively +// while v2.std.nat.Nat is the Peano coproduct Zero|Succ and must NOT, so a bare-name rule +// admits the wrong one. The enrolled RED for that pair is the regression control. +// FAIL-CLOSED ON UNKNOWN IDENTITY. decl_file_realizes_natively answers false for the empty +// string, and the empty string is what an unestablished identity yields. No fallback is +// added here, so a site that cannot establish identity keeps refusing. +// A CONJUNCTION, NOT A CARVE-OUT. The produced value must ALSO be a kernel numeric, so a +// String literal at a Nat-declared position stays refused. +// +// SOURCE-LEVEL, NOT EMISSION. decl_file_realizes_natively takes only decl_file; the neighbouring +// lookup_checkpoint takes a RenderTarget and would have made an emission fact answer a +// source-level question, which is why it is deliberately not the surface used here. +// INTERIM, AND THE ROW THAT DISSOLVES IT IS v2.workflow.floor_expected_red chunk_14. +// This decides that a kernel numeral inhabits Nat by asking whether Nat's DECLARING MODULE is +// kernel-backed -- a REALIZATION fact answering a TYPING question. It fails closed on unknown +// identity and is measured behaviour-preserving against main, so it is not unsound; it is +// UNDER-SPECIFIC, and it grants literal syntax module-wide permission to inhabit anything whose +// implementation eventually mentions a numeric carrier. The durable model is an +// expected-type-directed literal introduction judgment -- a type admits a numeral because it +// SUPPLIES one, not because its module realizes natively. Do not build on this predicate. +fn declared_realizes_as_kernel_numeric( + declared: Node, + produced: Node, + source_indices: Map +) -> Bool { + let produced_name = authored_name_at(source_indices: source_indices, node: produced) + let produced_is_kernel_numeric = produced_name == "Int" || produced_name == "Float" + if produced_is_kernel_numeric == false { + false + } else { + decl_file_realizes_natively(decl_file: type_reference_decl_file(n: declared)) + } +} + +// THE UNDECIDABLE ARM IS COUNTED, NOT SILENT, AND NOT A REFUSAL. It used to read +// `InhabitanceUndecidable { reason: _ } => []`, which is total over the verdict and blind one +// level down: the four reasons are declared precisely because they are different facts, and the +// wildcard gave all four the SAME rendering as Inhabits -- an undecidable seam and a decided-good +// seam left the relation as the identical empty list, so nothing downstream could tell a value +// that was judged from one that was never judgeable. That is the fail-open fabrication DESIGN +// section 5 forbids, and its cost is the one section 5 names: the deficit's frequency was zero by +// construction, so no reason could ever rank for the modeling that would settle it. +// +// WHY ADVISORY AND NOT A REFUSAL. Refusing here would fabricate a verdict in the other direction: +// the facts do not settle inhabitance, so asserting non-inhabitance is exactly as invented as +// asserting inhabitance. Undecidable is a property of the facts, never of the wiring, and the +// honest report is that no verdict was reached -- located, per-reason, and countable, so the four +// populations are observable and prioritizable. DeclaredTypeInhabitanceUndecided is registered +// non-blocking in v1.00_core is_interpreter_blocking_diagnostic and advisory in +// is_discovery_corpus_advisory_typecheck_diagnostic, so this makes the residue visible without +// reddening a corpus whose seams were never judged before this carrier existed either. +fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { + match reason { + UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone" + UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" + UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" + UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" + } +} + +fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List { + match declared_type_inhabitance(obligation: obligation, scope: scope) { + Inhabits => [] + InhabitanceUndecidable { reason: r } => + [make_error_node( + diagnostic: DeclaredTypeInhabitanceUndecided { + position: declared_type_position_label(position: obligation.position), + reason: inhabitance_undecidable_reason_label(reason: r), + span: obligation.span + }, + module_name: scope.module_name + )] + InhabitanceRefused { reason: _ } => + [make_error_node( + diagnostic: DeclaredTypeNotInhabited { + position: declared_type_position_label(position: obligation.position), + expected: node_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), + got: node_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), + span: obligation.span + }, + module_name: scope.module_name + )] + } +} + fn coproduct_payload_where_parent_required( formal: Node, actual: Node, @@ -2736,6 +2969,30 @@ fn direct_call_structured_application_mismatch_diags( ) } +fn direct_call_argument_inhabitance_diags( + plan: List, + scope: InferScope +) -> List { + flat_map( + plan, + app => + match app.matched_arg { + Present { value: ta } => + let actual_expr = arg_value(n: ta) + declared_type_obligation_diags( + obligation: DeclaredTypeObligation { + position: PositionDirectCallArgument, + declared: app.formal_subst, + produced: resolved_type(n: actual_expr), + span: actual_expr.span + }, + scope: scope + ) + Absent => [] + } + ) +} + fn container_element_nominal_brand_mismatch( formal: Node, actual: Node, @@ -4305,6 +4562,10 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu plan: call_application_plan, scope: scope ) + let inhabitance_arg_diags = direct_call_argument_inhabitance_diags( + plan: call_application_plan, + scope: scope + ) InferResult { typed: make_named_expr_node( name: func_name, expr_data: ExprCall { call_semantics: Present { value: PlainCallSemantics }, descent_evidence: none }, @@ -4313,7 +4574,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu span: span, name_span: node_name_span(n: texpr) ), - diagnostics: concat(arg_diags, concat(arg_shape_diags, concat(arg_compat_diags, structured_arg_diags))) + diagnostics: concat(arg_diags, concat(arg_shape_diags, concat(arg_compat_diags, concat(structured_arg_diags, inhabitance_arg_diags)))) } } else { let first_arg_type = match typed_args |> first { @@ -4992,7 +5253,22 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu } let elem_results = elements |> map(e => infer_list_literal_element(element: e, expected: elem_expected, scope: scope)) let typed_elements = elem_results |> map(r => r.typed) - let elem_diags = flat_map(elem_results, r => r.diagnostics) + let elem_inhabitance_diags = match elem_expected { + Present { value: declared_elem } => + flat_map(typed_elements, te => + declared_type_obligation_diags( + obligation: DeclaredTypeObligation { + position: PositionListElement, + declared: declared_elem, + produced: resolved_type(n: te), + span: te.span + }, + scope: scope + ) + ) + Absent => [] + } + let elem_diags = concat(flat_map(elem_results, r => r.diagnostics), elem_inhabitance_diags) let elem_type_node = if count(elem_results) > 0 { match first(elem_results) { Present { value: r } => resolved_type(n: r.typed) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 23b01b18d80..347cea2b2f9 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -5049,6 +5049,10 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str "ConstructorCallAdmissionRefused" } CompilerDiagnostic::AdmitCallersEntryNotDeclRef { .. } => "AdmitCallersEntryNotDeclRef", + CompilerDiagnostic::DeclaredTypeNotInhabited { .. } => "DeclaredTypeNotInhabited", + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => { + "DeclaredTypeInhabitanceUndecided" + } CompilerDiagnostic::UnlistedImportUse { .. } => "UnlistedImportUse", CompilerDiagnostic::AmbiguousReference { .. } => "AmbiguousReference", CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { .. } => { @@ -5105,6 +5109,8 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str constructor_decl_name, .. } => constructor_decl_name.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { position, .. } => position.clone(), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { position, .. } => position.clone(), CompilerDiagnostic::UnlistedImportUse { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousReference { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { candidates, .. } => { diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 4e499640948..f189594ed25 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -2,7 +2,11 @@ // Source module: v1.compiler.infer use self::CallArgumentFormalSelection::*; +use self::DeclaredTypePosition::*; use self::DescentSizeExpr::*; +use self::InhabitanceRefusalReason::*; +use self::InhabitanceUndecidableReason::*; +use self::InhabitanceVerdict::*; use self::ServiceConfigFieldJudgment::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, @@ -53,6 +57,7 @@ pub use crate::std_types::{ container_param_name, container_template_algebra, is_kernel_type, kernel_type_set, }; pub use crate::std_types::{NonEmptyStr, SourceSpan}; +pub use crate::v1_compiler_coercion::{decl_file_realizes_natively, type_reference_decl_file}; pub use crate::v1_compiler_infer_access::AccessCheckResultNode; pub use crate::v1_compiler_infer_access::{check_index_access_node, check_slice_access_node}; pub use crate::v1_compiler_infer_cycle::detect_type_cycles_kahn; @@ -3419,6 +3424,212 @@ pub fn foreign_concrete_coproduct_where_parent_required( } } +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum DeclaredTypePosition { + PositionRecordLiteralField, + PositionListElement, + PositionMapValue, + PositionDataInitializer, + PositionDeclaredReturn, + PositionLetAnnotation, + PositionVariantPayload, + PositionGenericTypeArgument, + PositionCastTarget, + PositionParameterDefault, + PositionCallableReturn, + PositionDirectCallArgument, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct DeclaredTypeObligation { + pub position: DeclaredTypePosition, + pub declared: Rc, + pub produced: Rc, + pub span: Rc, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceUndecidableReason { + UndecidableGenericFormal, + UndecidableOptionalCarrier, + UndecidableFormalUnresolved, + UndecidableProducedIdentityErased, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceRefusalReason { + RefusedPayloadAtParent, + RefusedKernelAtStructured, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum InhabitanceVerdict { + Inhabits, + InhabitanceRefused { + reason: InhabitanceRefusalReason, + }, + InhabitanceUndecidable { + reason: InhabitanceUndecidableReason, + }, +} + +pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position.clone() { + DeclaredTypePosition::PositionRecordLiteralField => "record literal field".to_string(), + DeclaredTypePosition::PositionListElement => "list element".to_string(), + DeclaredTypePosition::PositionMapValue => "map value".to_string(), + DeclaredTypePosition::PositionDataInitializer => "data initializer".to_string(), + DeclaredTypePosition::PositionDeclaredReturn => "declared return".to_string(), + DeclaredTypePosition::PositionLetAnnotation => "let annotation".to_string(), + DeclaredTypePosition::PositionVariantPayload => "variant payload".to_string(), + DeclaredTypePosition::PositionGenericTypeArgument => "generic type argument".to_string(), + DeclaredTypePosition::PositionCastTarget => "cast target".to_string(), + DeclaredTypePosition::PositionParameterDefault => "parameter default".to_string(), + DeclaredTypePosition::PositionCallableReturn => "callable return".to_string(), + DeclaredTypePosition::PositionDirectCallArgument => "direct call argument".to_string(), + } +} + +pub fn declared_type_inhabitance( + obligation: Rc, + scope: Rc, +) -> Rc { + { + let declared = obligation.declared.clone(); + let produced = obligation.produced.clone(); + let source_indices = scope.type_env.clone().source_indices.clone(); + let declared_name = authored_name_at(source_indices.clone(), declared.clone()); + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let either_optional = ((declared.return_cardinality.clone() == Cardinality::CardOptional) + || (produced.return_cardinality.clone() == Cardinality::CardOptional)); + let declared_is_generic = ((declared.params.clone().len() as i64) > 0); + if either_optional.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableOptionalCarrier, + }) + } else { + if declared_is_generic.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableGenericFormal, + }) + } else { + if (declared_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableFormalUnresolved, + }) + } else { + if (produced_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, + }) + } else { + if declared_realizes_as_kernel_numeric( + declared.clone(), + produced.clone(), + source_indices.clone(), + ) { + Rc::new(InhabitanceVerdict::Inhabits) + } else { + if kernel_value_declared_type_mismatch( + declared.clone(), + produced.clone(), + scope.type_env.clone(), + source_indices.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + }) + } else { + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + }) + } else { + Rc::new(InhabitanceVerdict::Inhabits) + } + } + } + } + } + } + } + } +} + +pub fn declared_realizes_as_kernel_numeric( + declared: Rc, + produced: Rc, + source_indices: Rc>>, +) -> bool { + { + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let produced_is_kernel_numeric = ((produced_name.clone() == "Int".to_string()) + || (produced_name.clone() == "Float".to_string())); + if (produced_is_kernel_numeric.clone() == false) { + false + } else { + decl_file_realizes_natively(type_reference_decl_file(declared.clone())) + } + } +} + +pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { + match reason.clone() { + InhabitanceUndecidableReason::UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone".to_string(), + InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), + InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), + InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), +} +} + +pub fn declared_type_obligation_diags( + obligation: Rc, + scope: Rc, +) -> Rc>> { + match (*declared_type_inhabitance(obligation.clone(), scope.clone())).clone() { + InhabitanceVerdict::Inhabits => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceUndecidable { reason: r, .. } => { + Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { + position: declared_type_position_label(obligation.position.clone()), + reason: inhabitance_undecidable_reason_label(r.clone()), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]) + } + InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { + position: declared_type_position_label(obligation.position.clone()), + expected: node_type_shape( + obligation.declared.clone(), + scope.type_env.clone().source_indices.clone(), + ), + got: node_type_shape( + obligation.produced.clone(), + scope.type_env.clone().source_indices.clone(), + ), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]), + } +} + pub fn coproduct_payload_where_parent_required( formal: Rc, actual: Rc, @@ -4159,6 +4370,37 @@ pub fn direct_call_structured_application_mismatch_diags( } } +pub fn direct_call_argument_inhabitance_diags( + plan: Rc>>, + scope: Rc, +) -> Rc>> { + Rc::new({ + let mut __result = Vec::new(); + for app in plan.iter().cloned() { + __result.extend( + (*match app.matched_arg.clone() { + Some(ta) => { + let actual_expr = arg_value(ta.clone()); + declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionDirectCallArgument, + declared: app.formal_subst.clone(), + produced: resolved_type(actual_expr.clone()), + span: actual_expr.span.clone(), + }), + scope.clone(), + ) + } + None => Rc::new(vec![]), + }) + .iter() + .cloned(), + ); + } + __result + }) +} + pub fn container_element_nominal_brand_mismatch( formal: Rc, actual: Rc, @@ -7371,6 +7613,11 @@ Rc::new(ArgGenericFoldState { call_application_plan.clone(), scope.clone(), ); + let inhabitance_arg_diags = + direct_call_argument_inhabitance_diags( + call_application_plan.clone(), + scope.clone(), + ); Rc::new(InferResult { typed: make_named_expr_node( func_name.clone(), @@ -7393,7 +7640,10 @@ Rc::new(ArgGenericFoldState { arg_shape_diags.clone(), v1_rt::concat( arg_compat_diags.clone(), - structured_arg_diags.clone(), + v1_rt::concat( + structured_arg_diags.clone(), + inhabitance_arg_diags.clone(), + ), ), ), ), @@ -8804,13 +9054,38 @@ if ((call_ambiguity_cands.clone().len() as i64) > 0) { } __result }); - let elem_diags = Rc::new({ - let mut __result = Vec::new(); - for r in elem_results.iter().cloned() { - __result.extend((*r.diagnostics.clone()).iter().cloned()); - } - __result - }); + let elem_inhabitance_diags = match elem_expected.clone() { + Some(declared_elem) => Rc::new({ + let mut __result = Vec::new(); + for te in typed_elements.iter().cloned() { + __result.extend( + (*declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionListElement, + declared: declared_elem.clone(), + produced: resolved_type(te.clone()), + span: te.span.clone(), + }), + scope.clone(), + )) + .iter() + .cloned(), + ); + } + __result + }), + None => Rc::new(vec![]), + }; + let elem_diags = v1_rt::concat( + Rc::new({ + let mut __result = Vec::new(); + for r in elem_results.iter().cloned() { + __result.extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + elem_inhabitance_diags.clone(), + ); let elem_type_node = if ((elem_results.clone().len() as i64) > 0) { match elem_results.clone().first().cloned() { Some(r) => resolved_type(r.typed.clone()), @@ -22831,3 +23106,40 @@ pub fn reconcile_with_census_extra( }) } } + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionRecordLiteralField; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionListElement; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionMapValue; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDataInitializer; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDeclaredReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionLetAnnotation; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionVariantPayload; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionGenericTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCastTarget; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionParameterDefault; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCallableReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDirectCallArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableGenericFormal; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableOptionalCarrier; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableFormalUnresolved; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableProducedIdentityErased; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedPayloadAtParent; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedKernelAtStructured; diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index 75e740e0287..9a02a12a3c5 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -534,6 +534,17 @@ pub enum CompilerDiagnostic { constructor_decl_name: String, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, + DeclaredTypeInhabitanceUndecided { + position: String, + reason: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -696,6 +707,8 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { span: s, .. } => s.clone(), @@ -748,6 +761,8 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, .. } => v1_rt::concat(v1_rt::concat("admit_callers entry on '".to_string(), cn.clone()), "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { position: pos, reason: r, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("declared-type inhabitance is undecidable at the ".to_string(), pos.clone()), " (".to_string()), r.clone()), "): the modeled facts do not settle whether the produced value inhabits its declared type, so no verdict is asserted in either direction".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous anonymous record literal shape matches ".to_string(), ((cs.clone().len() as i64)).to_string()), " structs: ".to_string()), cs.clone().join(&", ".to_string())), " — add a nominal type".to_string()), @@ -849,6 +864,7 @@ pub fn is_interpreter_blocking_diagnostic(d: Rc) -> bool { CompilerDiagnostic::MethodExistenceFrontierAdmitted { .. } => false, CompilerDiagnostic::ReceiverTypeUnestablished { .. } => false, CompilerDiagnostic::ServiceConfigReferenceJudgmentDeferred { .. } => false, + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => false, _ => true, } } @@ -859,6 +875,7 @@ pub fn is_discovery_corpus_advisory_typecheck_diagnostic(d: Rc true, CompilerDiagnostic::ReceiverTypeUnestablished { .. } => true, CompilerDiagnostic::ServiceConfigReferenceJudgmentDeferred { .. } => true, + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => true, CompilerDiagnostic::WhereRefinementUnenforced { reason: r, .. } => { is_where_refinement_unenforced_advisory_reason(r.clone()) } diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index 964ee6bdf2a..8c93523b661 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -121,6 +121,25 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } +// WHY List AND NOT List, AND WHAT WOULD REPLACE IT. These rows are octet +// values compared against emitted bytes. They were declared List while holding +// integers, which the list-element inhabitance obligation refused: std.bit's Byte is +// `type Byte { bits: List }`, a bit-record, so an Int literal never inhabited it. +// The consumer's signature already carried the right type -- v2.compiler.emit_host +// `emit_host_octets_byte_string(octets: List)` -- so this is the declaration +// agreeing with its single authority, not a carrier weakened to satisfy a wall. +// +// Int is nonetheless weaker than the values deserve: an octet is 0..255 and nothing +// here says so. The correctly shaped type already exists and is grounded -- +// extdeps.network.ipv4 `Octet`, declared as Int refined by range(min: 0, max: 255) -- +// but it is homed in the IPv4 domain, and reaching into a network module for a +// compiler-emission byte would be the layer inversion DESIGN 3 warns about rather +// than a reuse. What is missing is a domain-agnostic octet carrier, not a new +// spelling of one that exists. +// +// So the pointer, deliberately stated as rationale rather than a machine claim: when +// such a carrier lands, these rows and emit_host_octets_byte_string's parameter move +// to it together -- the parameter first, since the declaration follows its consumer. data match_expected_octets: List = [0, 1, 0, 0, 0] data match_alt_expected_octets: List = [0, 2, 0, 0, 0] data loop_expected_octets: List = [0, 1, 0, 0, 0] diff --git a/src/v2/workflow/dag_acceptance.dag b/src/v2/workflow/dag_acceptance.dag index 7ae89c50821..78091a80bf9 100644 --- a/src/v2/workflow/dag_acceptance.dag +++ b/src/v2/workflow/dag_acceptance.dag @@ -970,7 +970,7 @@ fn is_front_end_obligation(obligation: DagStageObligation) -> Bool { } fn post_front_end_obligations(effective: List) -> List { - fold(effective, init: no_rows(), f: fn(acc, o) { + fold(effective, init: no_obligations(), f: fn(acc, o) { if is_front_end_obligation(obligation: o) { acc } else { list_snoc_item(xs: acc, item: o) } }) } diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 735815df85e..7c3ab165419 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -461,10 +461,109 @@ fn floor_expected_red_chunk_13() -> List { Cons { head: "test.claim.method_arg_declared_contract_witness_test.w_method_arg_infers_against_declared_contract_not_element_type_test", tail: Empty {} } } +// TWO ARMS OF THE DIRECT-CALL INHABITANCE WITNESS, ENROLLED BECAUSE THE WALL THEY ASSERT +// DOES NOT EXIST AND NEVER DID -- NOT BECAUSE THIS BRANCH BROKE IT. Both arms assert that a +// value at a direct-call argument is REFUSED. Both are red. The control that settles who +// caused it was run on 2026-08-23: identical probe sources, identical dispatch, gunbc built +// from origin/main 907f19c2cc7 and from the branch head, and main returns the same answer at +// every point. +// +// probe branch main verdict +// kernel 5 at the Peano Nat accepted accepted no change +// "forty" at std.nat.Nat accepted accepted no change +// 40 at std.nat.Nat accepted accepted no change +// +// So the refusals were ASSERTED, not broken. The gap is in the consumed predicate +// v1.compiler.infer kernel_value_declared_type_mismatch, and it is older than this branch and +// WIDER than these two rows. Measured 2026-08-23 by five probes varying only the declared +// type's shape, one String argument at every one: +// +// Int kernel primitive REFUSED +// NatLike = CommutativeSemiring 1-arg application admitted +// OneArg = List 1-arg application admitted +// TwoArg = Map 2-arg application admitted +// Closed = ZzA | ZzB { v: Int } coproduct REFUSED +// +// A KERNEL VALUE IS ADMITTED AT ANY TYPE APPLICATION -- not merely an algebraic one, and not +// as a function of arity: the two-argument Map is admitted exactly as List is. So the +// legible specimen is a String reaching a List parameter unremarked, which is the ordinary +// compiler floor DESIGN requires before any differentiating claim, and Nat is one instance of it. +// The class is "total at the level examined, blind one level down": the judgment is exhaustive +// over primitive / coproduct / application and the application arm never asks what the +// application EXPANDS TO, so there is no missing arm for exhaustiveness checking or review to see. +// Located, with a reproducing input; the admitting branch has NOT been read and no line is named. +// +// NEXT-RUNG TRIGGER, TWO PARTS. The mechanical one: that predicate repaired so a kernel value at +// a type application refuses. The MODEL one, which is what the durable repair looks like and is +// recorded here so the interim is never cited as the design: +// +// declared_realizes_as_kernel_numeric decides that 40 inhabits Nat by consulting +// v1.compiler.coercion decl_file_realizes_natively -- i.e. because Nat's DECLARING MODULE is +// kernel-backed. That is a REALIZATION fact standing in for a TYPING fact, and it amounts to +// peeling the applied type until a scalar appears. It is not unsound: it fails closed on unknown +// identity, and the admit is measured behaviour-preserving-or-narrowing against main. It is +// UNDER-SPECIFIC. It answers "this module's numerics are kernel-backed" where the question is +// "does this type admit this literal", and it therefore grants literal syntax module-wide +// permission to inhabit anything whose implementation eventually mentions a numeric carrier. +// The two answers coincide today for Nat and Int and stop coinciding the moment a module +// declares a numeric type that should NOT take bare literals. +// +// THE DURABLE MODEL IS AN EXPECTED-TYPE-DIRECTED LITERAL INTRODUCTION JUDGMENT: 40 inhabits Nat +// because Nat SUPPLIES A NUMERAL INTRODUCTION, not because its module realizes natively. Lean is +// the worked precedent -- numerals elaborate against the expected type through an OfNat +// obligation, and literal introduction is kept separate from coercion insertion. When that lands, +// declared_realizes_as_kernel_numeric and its consumption of decl_file_realizes_natively dissolve; +// they are the interim, and this row is their dissolution trigger. +// +// TWO CONSTRAINTS ON WHOEVER BUILDS IT, both live in this repository rather than hypothetical. +// A judgment that peels a declared type to its representation defeats abstraction walls that +// already hold: TransparentAlias may be exposed; OpaqueType, SoleConstructorCarrier, Refinement +// and Brand MAY NOT -- sole_constructor is a real, executing construction wall and a peeling +// judgment walks through it silently. And exposure must derive a canonical view ONCE per type +// identity and cache it, with cycle detection and a measured expansion budget: recursive aliases +// can loop, renormalizing at every use site is expensive, and this corpus is already living on a +// per-witness cost line. When it lands, BOTH rows here go green -- and this roster's self-emptying arm +// reds the build and names them for removal, at which point they become permanent regression +// controls under DESIGN 4b(4) rather than being deleted. The flip is EXPECTED and is not a +// regression; it is the dissolution event. fn floor_expected_red_chunk_14() -> List { - Empty {} + Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_refused", tail: Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused", tail: Empty {} } } } +// THE LIST-ELEMENT ARM OF THE DIRECT-CALL INHABITANCE WITNESS. It asserts that a wrong element +// type inside a list at a direct-call argument is refused. It is not. Its PAIRED CONTROL -- +// w_the_same_wrong_pair_directly_at_the_argument_is_refused, deliberately NOT enrolled -- passes +// the identical two types at the identical position without the list, and must stay green: if it +// ever reds, the probe has stopped measuring lists and this enrolment is meaningless. +// +// WHY IT IS ENROLLED RATHER THAN FIXED HERE: the gap was discovered as a live wrong argument in +// dag/gunbc/heal_revalidation.dag (List into required_gates: List), +// and the relation's SILENCE was the only evidence of it. DESIGN 4b(4) puts the evidence in a +// probe and the repair in production, not the reverse, so the evidence lives here where anyone +// can reproduce it. +// +// THE PRODUCTION SITE WAS REPAIRED TWICE AND ONLY THE SECOND WAY WAS RIGHT. Lifting the argument +// through as_content_hash_structural DOUBLE-WRAPPED a value that was already the union -- the +// witness passes Fnv1a64(content_hash_atom(...)) and check_coverage_admits takes ContentHash, so +// heal_revalidation's own two parameters were the ONLY things in the chain declaring the family +// member. Lifting made the comparison Fnv1a64(Fnv1a64(x)) against Fnv1a64(x) and reddened +// heal_revalidation_witness only_exact_healed_head_complete_coverage_admits, a witness that had +// been green. The chain is now ContentHash end to end and the lifts are gone. Reading the CALLEE +// is half the discriminator; the CALLER is the other half, and a declaration sandwiched between +// two that agree with each other is the one that is wrong. +// +// NEXT-RUNG TRIGGER: declared_type_inhabitance descending into a list's element type at a +// direct-call argument. When it lands this row goes green and the roster's self-emptying arm +// names it for removal, at which point it becomes a permanent regression control. +// DELIBERATELY EMPTY, AND PERMANENTLY SO -- THE ROW THAT WAS HERE ASSERTED A GAP THAT DOES NOT +// EXIST. w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused was enrolled while +// its paired control was RED; the control's red proved the pair measured "records are never +// judged" rather than anything about lists. Rebuilt on a kernel String and left UNENROLLED so a +// red would show loudly, it PASSES (run 32667623528, failed=0). The relation descends into a +// list literal's elements at a direct-call argument and always did. +// +// The arm stays in the witness file as a permanent regression control over that fact. Nothing is +// enrolled here because there is nothing red to enrol. fn floor_expected_red_chunk_15() -> List { Empty {} } diff --git a/src/v2/workflow/native_cache_fusion.dag b/src/v2/workflow/native_cache_fusion.dag index 868c3216704..fbe8dcc6cce 100644 --- a/src/v2/workflow/native_cache_fusion.dag +++ b/src/v2/workflow/native_cache_fusion.dag @@ -5,7 +5,7 @@ import std.emit_on_demand { EmitOnDemandCacheReceipt, materialization_for_lookup } import std.content_hash { ContentHash } -import std.content_hash { content_hash_atom } +import std.content_hash { content_hash_atom, as_content_hash_structural } import std.realization { Materialization, Share, Recompute } import v2.std.logic { Bool } import v2.std.text { String } @@ -32,7 +32,7 @@ fn model_lookup_for(o: HostWarmObservation, key: ContentHash) -> EmitOnDemandLoo } fn fusion_agreement_holds_for(o: HostWarmObservation) -> Bool { - let key = content_hash_atom(value: "fusion-law-synthetic-key") + let key = as_content_hash_structural(structural: content_hash_atom(value: "fusion-law-synthetic-key")) let model_share = materialization_for_lookup(lookup: model_lookup_for(o: o, key: key)) == Share host_compile_skipped(o: o) == model_share }