diff --git a/dag/test/claim/root4_measure_missing_generics_witness_test.dag b/dag/test/claim/root4_measure_missing_generics_witness_test.dag index 16040dbd392..7f0bd15d75f 100644 --- a/dag/test/claim/root4_measure_missing_generics_witness_test.dag +++ b/dag/test/claim/root4_measure_missing_generics_witness_test.dag @@ -7,7 +7,26 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data root4_measure_missing_generics_witness_note: String = "Root-4 measure_missing_generics family: a function-generic container argument must preserve its applied arguments through render_rust_decl_type overlay resolution. The executable emitter-level fixtures use deliberately synthetic Root4AppliedCarrier, Root4AliasCarrier, and Root4ZeroArityCarrier names, so they exercise the structural shape without re-declaring the canonical std.measure.Measure authority; canonical Measure behavior is covered by the stamped canonical-seven receipt. The decision is structural (__applied_type_args or resolved-type children), never a type-name check. The combined-state fixture proves that an explicitly empty applied-argument property does not suppress non-empty resolved children. RED controls: w_zero_param_alias_use_site_stays_bare pins the closed-alias use site to the bare alias name; w_unrelated_zero_param_leaf_unchanged proves a bare leaf without applied or resolved children does not gain arguments. w_zero_param_alias_use_site_stays_bare previously asserted the OPPOSITE shape -- Rc>>, an alias declared in Rust with no parameters and then applied to three arguments, which rustc refuses as E0107. It was enrolled and green, so the defect had a defender: the emitted declaration pub type ClosedCarrierAlias = Rc>; already carries the substitution, and a use site that re-supplies the definition arguments cannot compile under any reading. The witness now asserts the declaration and the bare use site together, and excludes the applied spelling, so the emitted pair is checked for agreement rather than either half alone.\n\nw_positive_int_refined_alias_rhs_stays_bare_nat REQUIRED SPELLING CHANGED (eager-deer-389, Root B cutover): it required 'pub type PositiveInt = crate::std_nat::Nat' and now requires 'pub type PositiveInt = i64;'. This is a deliberate model change, not a red made to go away, and the reason is recorded here rather than in a commit message because the next reader of this row will ask. Root B deletes the global RustCorpusRepr emission mode and keys Rust primitive realization on the DECLARING MODULE of the type. Under the deleted mode this fixture emitted the std_nat path only because its synthetic single-module closure happened to contain no v1 sources -- the SAME declaration realized differently depending on which other sources shared the closure, which is precisely the defect the cut removes. Under declaration keying, dag/std/nat.dag's Nat realizes natively everywhere, so the refined alias RHS renders as the native spelling. MEASURED, not assumed: emitting this exact source on the post-cut emitter produces 'pub type PositiveInt = i64;' AND emits std_nat.rs containing 'pub type Nat = i64;', so the two spellings denote the SAME Rust type and the old required string would still have compiled -- what changed is which of two equivalent spellings the emitter chooses, not the type. The row's actual subject is unaffected: it exists to prove the refined alias RHS stays BARE rather than gaining phantom type arguments (the E0107 class), and both exclusions -- 'Nat' and 'Nat<' -- are unchanged and still hold, with the native spelling satisfying bareness at least as strongly. If a future cut makes Nat structural again this row flips back, and that flip is a real signal rather than noise." -fn w_applied_generic_carrier_preserves_arguments() -> Bool { +// ONE WITNESS PER SUBJECT, WHERE THERE USED TO BE ONE CONJUNCTION OVER FIVE. +// +// WHY, AND IT IS COST BEFORE IT IS STYLE: four of the five subjects below each run a full +// `compile_dag_rust_emit_check` -- a separate emit compile per snippet -- so the single +// `root4_measure_missing_generics_witness_holds` that conjoined them cost roughly five times a +// one-snippet witness by construction, and was the most expensive row in the corpus. Measured +// from the required floor's own `[over-cost]` lines across five main runs: cpu_ms 3322, 3901, +// 3998, 4252, 5623 against a 1552ms disclosure line and a 5000ms fail-stop. Every one of the +// five is 2.1x-3.6x the line, and the last one crossed the limit and failed the required run. +// The row was over the disclosure line in its BEST run, so this is a cost debt the gate had +// been reporting all along, not a flake. +// +// AND THE SPLIT IS STRICTLY STRONGER THAN THE CONJUNCTION IT REPLACES, which is why this is a +// repair rather than a cost dodge. `a && b && c && d && e` reports ONE verdict for five +// subjects: when it goes red, nothing says which subject regressed, and the four that held are +// indistinguishable from the one that did not. Five witnesses name the failing subject in the +// failure itself. NOTHING IS ASSERTED LESS: the same five predicates run over the same five +// fixtures with the same required and excluded spellings. The `w_` names are unchanged, so the +// RED-control prose in the note above still names its subjects correctly. +test fn w_applied_generic_carrier_preserves_arguments() -> Bool { compile_dag_rust_emit_check( "module root4_applied_carrier\n\ntype ProbeQuantity { value: Int }\ntype ProbeMagnitude { value: Int }\ntype Root4AppliedCarrier { payload: M }\n\nfn witness(items: List>) -> List> {\n items\n}\n", "src/root4_applied_carrier.rs", @@ -16,7 +35,7 @@ fn w_applied_generic_carrier_preserves_arguments() -> Bool { ) } -fn w_empty_applied_property_falls_through_to_resolved_children() -> Bool { +test fn w_empty_applied_property_falls_through_to_resolved_children() -> Bool { rust_decl_type_container_overlay_is_admitted( authored_is_leaf: true, closed_alias: false, @@ -43,7 +62,7 @@ fn w_empty_applied_property_falls_through_to_resolved_children() -> Bool { ) } -fn w_zero_param_alias_use_site_stays_bare() -> Bool { +test fn w_zero_param_alias_use_site_stays_bare() -> Bool { compile_dag_rust_emit_check( "module root4_closed_alias\n\ntype ProbeQuantity\ntype ProbeScale\ntype ProbeMagnitude\ntype Root4AliasCarrier { payload: M }\ntype ClosedCarrierAlias = Root4AliasCarrier\n\nfn witness(items: List) -> List {\n items\n}\n", "src/root4_closed_alias.rs", @@ -52,7 +71,7 @@ fn w_zero_param_alias_use_site_stays_bare() -> Bool { ) } -fn w_unrelated_zero_param_leaf_unchanged() -> Bool { +test fn w_unrelated_zero_param_leaf_unchanged() -> Bool { compile_dag_rust_emit_check( "module root4.unrelated_zero_param\nimport std.nat { Nat }\n\ntype Root4ZeroArityCarrier { count: Nat }\n\nfn witness(items: List) -> Root4ZeroArityCarrier {\n Root4ZeroArityCarrier { count: 0 }\n}\n", "src/root4_unrelated_zero_param.rs", @@ -61,7 +80,7 @@ fn w_unrelated_zero_param_leaf_unchanged() -> Bool { ) } -fn w_positive_int_refined_alias_rhs_stays_bare_nat() -> Bool { +test fn w_positive_int_refined_alias_rhs_stays_bare_nat() -> Bool { compile_dag_rust_emit_check( "module std.integer_positive_int_probe\nimport std.nat { Nat }\ntype PositiveInt = Nat where gt_zero\n", "src/std_integer_positive_int_probe.rs", @@ -69,11 +88,3 @@ fn w_positive_int_refined_alias_rhs_stays_bare_nat() -> Bool { ["Nat", "Nat<"] ) } - -test fn root4_measure_missing_generics_witness_holds() -> Bool { - w_applied_generic_carrier_preserves_arguments() - && w_empty_applied_property_falls_through_to_resolved_children() - && w_zero_param_alias_use_site_stays_bare() - && w_unrelated_zero_param_leaf_unchanged() - && w_positive_int_refined_alias_rhs_stays_bare_nat() -}