Compiler floor — one declared-type inhabitance authority, two grammar positions wired, ten declared

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<Fnv1a64Structural>,
+  required_roster: ContentHash,
+  required_gates: List<ContentHash>,
 ) -> 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<Fnv1a64Structural>,
+  required_roster: ContentHash,
+  required_gates: List<ContentHash>,
 ) -> Bool {
   match classify_heal_revalidation_admission(
     state: state,

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<Magnitude> 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<Int> parameter is,
+// and Map<String, Int> 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<Fnv1a64Structural> into check_coverage_admits's
+// required_gates: List<ContentHash> -- 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<Fnv1a64Structural> VARIABLE into a
+// List<ContentHash> 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<Cop>) -> 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
+}