Checker refuses a non-Bool match guard (PositionMatchGuard); Int guards counted as expected red

dag/extdeps/languages/rust/emit.dag

@@ -329,6 +329,7 @@ data rt_function_registry: List<RuntimeFunction> = [
   { name: "atom_identity_hash", bridge_name: "atom_identity_hash", passes_by_ref: false, wraps_result: false },
   { name: "hash_combine",       bridge_name: "hash_combine",     passes_by_ref: false, wraps_result: false },
   { name: "trace_mark",         bridge_name: "trace_mark",       passes_by_ref: false, wraps_result: false },
+  { name: "observed_monotonic_nanos", bridge_name: "observed_monotonic_nanos", passes_by_ref: false, wraps_result: false },
 
   { name: "rc_ptr_eq",          bridge_name: "rc_ptr_eq",        passes_by_ref: false, wraps_result: false },
   { name: "rc_vec_ptr_eq",      bridge_name: "rc_vec_ptr_eq",    passes_by_ref: false, wraps_result: false },

dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag

@@ -14,7 +14,7 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode {
     "RUNG FOUND AT: mitigated on the operator route; below the floor on the value route (the cast's type was dropped, so `x as Q` was Accepted with `Q` declared nowhere). CEILING: structurally guaranteed -- a cast lowers to a value carrying its operand and its target type, or refuses.",
     "RUNG NOW: mitigated on EVERY route. `v2.compiler.body_lowering_fold` `body_lower_postfix_expr` refuses a postfix chain carrying an as-suffix with `body_lowering_reason_type_annotation_not_carried` located at the authored target type -- the one reason for a type the lowering cannot carry, shared with the let annotation -- and `body_lower_arm_operand_resolved_optional` declines a cast so a let value or an arm reaches that refusal instead of answering the operand. A declared target refuses too: nothing is carried, so nothing is accepted. As an operator operand the cast now refuses with the same reason, because the postfix is folded before the operator reader sees it. CENSUS: the v2-route identity census over the 321-path population (`v2.compiler.reference_conservation_census` `reference_conservation_stratified_sample_paths` plus six) re-derived by `reference_conservation_census_for_paths` over each arm (pair 620ecb0a50f / 4c9f8d326d3): the modules that newly refuse are data rows casting a literal to a refinement and fn bodies casting to String, each refusing whole, and each returns when the trigger below lands.",
     "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY (the one the refusal above was retired by): a TYPED CAST NODE -- `e as T` lowers to Transform[coerce, e] with `v2.std.type_binder` `<cast-target>` -> T beside its positional children, and that node is SUFFICIENT FOR: resolve binding T in type role through the shared type-role frame (an undeclared T refusing at T); infer admitting the crossing through `v2.std.coercion` (not `std.coercion` `dag_cast_rules`, which is v1's side of `coercion_two_algebras_answer_one_question_stall`) or refusing typed; and translate and eval realizing it or refusing typed -- on every route, for every cast the refusal now stops.",
-    "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's <T> over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its carrier (`x as Int` from `x: Pos`) REFUSES, loud and typed at the operand, until `v2.std.coercion` admits a refinement-to-declared-carrier crossing as Widened from the type declaration (its existing widening fold needs per-domain integer value sets); it previously admitted only because an unscoped parameter walk bound x to an unrelated `fn positive(x: Int)`. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.",
+    "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's <T> over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its DECLARED carrier (`x as Int` from `x: Pos`, `type Pos = Int where positive`) is ADMITTED as Widened: `v2.compiler.infer` `refinement_declaration` reads the carrier from the declaration the reference's path reaches, and `v2.std.coercion` `coercion_cast_crossing` composes that carrier edge with the same exact-structural find_witness -- no preservation rule is added and no predicate is evaluated. Only the DECLARED carrier widens, one step: `x as Bool` from x: Pos and `x as Neg` between two refinements of Int REFUSE at the operand; for a refinement of a refinement (`type Pos2 = Pos where ..`) `x as Pos` is Widened and `x as Int` REFUSES (the carrier edge is not walked). The declaration is read through `v2.std.symbol_index` `symbol_index_lookup` on `v2.compiler.resolve` `ResolvedTree` `resolved_declarations` (gunbc#12629: declarations with resolved bodies, so a carrier is the identity resolve bound), and a lookup miss refuses (`bcn_a_refinement_lookup_miss_refuses`). Residue on that arm: the lowered cast's operator names `CoercionCrossing` by the exact rule (`v2.std.compilers.target_model` `canonical_operation_op_coerce`), fixed at lowering, so a Widened crossing is realized under that identity; both are representation-preserving (`OperandUnchanged`), so no emitted program differs. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.",
   ],
 
   evidence: [
@@ -36,7 +36,11 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode {
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_loop_passes_the_resolver_gate", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_foreign_label_on_a_transform_refuses", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_into_a_refinement_refuses_at_infer", field: WholeDeclaration },
-    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_refuses_until_carrier_widening", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_between_sibling_refinements_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_refinement_lookup_miss_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_refinement_of_a_refinement_widens_one_step", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_identity_cast_into_a_refinement_admits", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_as_cast_operand_resolves", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "a_parenthesised_call_operand_resolves", field: WholeDeclaration },

dag/gunbc/recurring_failure_mode/interpreter_ignores_match_arm_guards.dag

@@ -19,9 +19,15 @@ data interpreter_ignores_match_arm_guards: RecurringFailureMode = RecurringFailu
 
     "RECOGNITION RULE: when one node carrier feeds several consumers (checker, emitter, interpreter), each consumer must read every field the carrier's grammar admits, or refuse it. A consumer that reads a subset answers a narrower question than the source asks -- the same shape as `special_cased_lowering_answers_a_narrower_question_than_its_arms_ask`, on the interpretation path instead of the emission path.",
 
-    "ADJACENT GAP FOUND BY THE SAME PROBE, NOT REPAIRED HERE: the checker ACCEPTS a guard that is not Bool. `match n { x if 5 => 1  _ => 2 }` resolved and type-checked clean under `claim_batch`, and only the interpreter's `MatchGuardNotBool` refused it at run time (`match guard at <file>:<offset> evaluated to 5 (Int), not a Bool`, cause token type-error). So a non-Bool guard is refused on the interpretation path at rung 1 and is not refused at acceptance at all; the emitted `if 5` would be a rustc refusal. Its next-rung trigger is the checker requiring a guard to inhabit Bool, which makes the interpreter arm unreachable from an Accepted program.",
+    "ADJACENT GAP FOUND BY THE SAME PROBE: the checker ACCEPTED a guard that is not Bool. `match n { x if 5 => 1  _ => 2 }` resolved and type-checked clean, and only the interpreter's `MatchGuardNotBool` refused it at run time (`match guard at <file>:<offset> evaluated to 5 (Int), not a Bool`, cause token type-error). The guard was inferred with no expected type and judged by nothing.",
 
-    "RUNG FOUND AT: outside the ladder (silent). RUNG NOW: 2, mechanically preventable -- `test.claim.interpreter_match_guard_witness_test` pairs each rejecting guard (the discriminating red, measured red before the repair) with an admitting control.",
+    "ACCEPTANCE WALL, FOLLOW-UP: `v1.compiler.infer` now judges every guard as a `PositionMatchGuard` obligation of the one inhabitance relation, declared Bool (`match_guard_obligation_diags`, called from both arm-inference passes of the ExprMatch arm). Measured under `claim_batch --wet` with the regenerated seed: a String guard refuses `DeclaredTypeNotInhabited` at position `match guard` (zero such rows before), and a Bool guard admits. `test.claim.match_guard_bool_inhabitance_witness_test` carries both. The interpreter refusal stays as the runtime catch.",
+
+    "RESIDUE, NOT A DECLARED DROP (the rung was never higher): an Int guard, literal or value, is still ADMITTED, and the cause is the shared relation rather than this position. `declared_realizes_as_kernel_numeric` admits an Int or Float produced value at ANY declared type whose provenance realizes natively, and `provenance_realizes_natively` answers true for every KernelMinted type, Bool and String included -- so the same admission reaches every wired position, not only guards. Its two rows, `an_int_literal_guard_is_refused_at_acceptance` and `an_int_valued_guard_is_refused_at_acceptance`, are enrolled in `v2.workflow.floor_expected_red` `floor_expected_red_chunk_int_guard_admitted_by_the_relation`. NEXT-RUNG TRIGGER, named as the capability: the inhabitance relation admits a kernel numeric only at a declared type that realizes AS A NUMERIC, not at any natively realized one -- routed to the typing lane as its own corpus-wide item with its own census. When it lands both rows pass, leave the roster, and stay as regression controls.",
+
+    "A PARSE FACT FOUND ON THE WAY, recorded so the next fixture author does not rediscover it: a guard spelled as a bare identifier (`x if s =>`) never reaches the checker. The parser reads `s => 1` as a lambda and refuses `expected FatArrow, found Newline`, so a guard over one binding must be parenthesised (`x if (s) =>`).",
+
+    "RUNG FOUND AT: outside the ladder (silent). RUNG NOW, by path (DESIGN 4b(1), the minimum across in-scope paths): the guard-IGNORED class is at 2, mechanically preventable on the interpretation path -- `test.claim.interpreter_match_guard_witness_test` pairs each rejecting guard (measured red before the repair) with an admitting control. The non-Bool-guard class is at 3, structurally guaranteed, for non-numeric guard types (a String guard has no Accepted program), and at 1, mitigated by the interpreter's typed refusal, for Int and Float guards until the relation trigger above lands -- so its reported rung is 1.",
 
     "ATTAINABLE CEILING: 3, structurally guaranteed. NEXT-RUNG TRIGGER, named as the capability: an executed interpreter-versus-emitted-binary differential over the same source and inputs, reporting disagreement as a located refusal -- the same capability `special_cased_lowering_answers_a_narrower_question_than_its_arms_ask` names, which would have caught this class without anyone knowing to look for guards."
   ],

dag/std/cache_identity.dag

@@ -36,4 +36,10 @@ data native_test_universe_artifact_kind: ArtifactKindId = "native_test_universe"
 
 data native_module_verdict_bundle_artifact_kind: ArtifactKindId = "native_module_verdict_bundle"
 
+data native_module_resolve_artifact_kind: ArtifactKindId = "native_module_resolve"
+
+data native_module_infer_artifact_kind: ArtifactKindId = "native_module_infer"
+
+data native_test_identity_artifact_kind: ArtifactKindId = "native_test_identity"
+
 data cache_interface_product_dissolve_on: DissolutionCondition = unbound_dissolution(description: "dissolve-on: std.cache_identity.CacheInterfaceProduct — deleted closed enum fork; sole cache-backend identity authority is CacheInterfaceId (extdeps/cache/*.dag cited rows keyed by id).")

dag/std/compiler_entry.dag

@@ -241,6 +241,24 @@ type CompilerEntryDriver
 // collection directly rather than going through the constructor. That residual is the same one
 // v1.compiler.emit_rust records for its own two-role split, and its next-rung trigger is the same
 // language capability -- a module-private function boundary -- not anything this change can build.
+// THE SCHEDULER'S OWN WORK IS A ROW, because it is work and the partition is exhaustive.
+// ExclusiveDemandScheduling measures what the demand engine spends deciding WHAT RUNS NEXT --
+// building the plan, selecting from the ready queue, looking up bindings, settling a transition,
+// recomputing readiness and collecting rows -- as distinct from what the demands themselves spend,
+// which ExclusivePrepare and ExclusiveEval already carry.
+//
+// IT EXISTS BECAUSE LEAVING IT OUT WAS A CORRECTNESS DEFECT AND NOT A REPORTING GAP. Review of
+// gunbc#12401 found the driver closing its scheduling span BEFORE calling the engine, so all of the
+// above fell into the parent residual. The partition's tolerance arm is a fixed 50ms, so a large
+// enough selected universe makes an otherwise VALID adjudication exit
+// NativeDriverCostRemainderExceedsTolerance -- a fail-closed refusal fired by correct input, which
+// is the wrong direction of wrong. The row is what makes the scheduler's cost attributable instead
+// of unattributed.
+//
+// IT IS NOT PREPARE. Adding this time to ExclusivePrepare would have been the cheaper edit and it
+// would double-count: the engine already reports its own prepare nanos, and the driver already adds
+// those. The overhead is the scheduling span MINUS what the engine attributed to demands, which is
+// why it needs a key of its own rather than a larger existing one.
 type NativeDriverExclusiveRowKey
   = ExclusiveLoad
   | ExclusiveUniverseDerivation
@@ -251,6 +269,7 @@ type NativeDriverExclusiveRowKey
   | ExclusiveRowSerialization
   | ExclusiveModuleRelease
   | ExclusiveRelayEmit
+  | ExclusiveDemandScheduling
 
 // THE ROSTER IS THE ONE PLACE A ROW IS ADDED, and it is the residual this reshape does not close.
 // A key absent here is absent from every constructed collection, from the sum and from the
@@ -268,6 +287,7 @@ fn native_driver_exclusive_row_keys() -> List<NativeDriverExclusiveRowKey> {
     ExclusiveRowSerialization,
     ExclusiveModuleRelease,
     ExclusiveRelayEmit,
+    ExclusiveDemandScheduling,
   ]
 }
 
@@ -285,6 +305,7 @@ fn native_driver_exclusive_row_name(key: NativeDriverExclusiveRowKey) -> String
     ExclusiveRowSerialization => "row_serialization"
     ExclusiveModuleRelease => "module_release"
     ExclusiveRelayEmit => "relay_emit"
+    ExclusiveDemandScheduling => "demand_scheduling"
   }
 }