diff --git a/dag/gunbc/plans/native_obligation_population.dag b/dag/gunbc/plans/native_obligation_population.dag index 0c488b5d3ce..d1d98e12868 100644 --- a/dag/gunbc/plans/native_obligation_population.dag +++ b/dag/gunbc/plans/native_obligation_population.dag @@ -110,6 +110,7 @@ fn native_obligation_population_body() -> List { ol(items: [ li(text: "Ruled 2026-10-09: the frontier is observed from a run, never reasoned from source."), li(text: "Ruled 2026-10-10 (operator, relayed by smart-gull-336): the denominator is the derived universe -- green identities, exactly one observed frontier and typed exclusions/refusals -- and the green set alone is never a production-admission denominator; the first frontier's subject is a stable qualified identity or a derived single-member target with a cardinality assertion, never \"the smallest member\"."), + li(text: "Runtime task, declared: typed refusal reasons for the population predicates (`native_member_is_eligible`, `native_member_is_a_subject_row`). They return Bool today, admitted for the first fold with an empty green set; the trigger is the first non-empty green set."), li(text: "Deferred: widening the universe from one identity to all of `v2.test.*`; trigger is M1 landed with a terminal that the driver can pass."), ]), ] diff --git a/dag/gunbc/roadmap/roadmap_authority.dag b/dag/gunbc/roadmap/roadmap_authority.dag index b9c99d6074b..5fb060274d4 100644 --- a/dag/gunbc/roadmap/roadmap_authority.dag +++ b/dag/gunbc/roadmap/roadmap_authority.dag @@ -936,6 +936,7 @@ fn declared_roadmap_nodes() -> List { "a_host_judged_member_is_ineligible" as NonEmptyStr, "the_population_is_disjoint_from_the_emitted_subject_rows" as NonEmptyStr, "the_denominator_is_the_derived_universe_not_the_green_set" as NonEmptyStr, + "the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route" as NonEmptyStr, ], )), parent: in_project(project: "native-route-to-live", contribution: "This is the shape the native route takes on the required path: the drop v2_native_route_off_the_merge_path retires only when this population is judged on a landing, and D10 admission reads its green set as the subject denominator."), diff --git a/dag/test/claim/native/native_obligation_population_witness_test.dag b/dag/test/claim/native/native_obligation_population_witness_test.dag index ecdd48e5d04..11f52761aa3 100644 --- a/dag/test/claim/native/native_obligation_population_witness_test.dag +++ b/dag/test/claim/native/native_obligation_population_witness_test.dag @@ -1,9 +1,11 @@ module test.claim.native.native_obligation_population_witness_test -import std.types { Bool, String, List } +import std.types { Bool, String, List, list_length } +import v2.std.algebra { any } +import gunbc.emitted_subject_build_gate { emitted_subject_build_rows, emitted_subject_build_label_text } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import gunbc.plans.native_obligation_population { - native_denominator_is_the_universe, native_member_is_eligible, native_member_is_a_subject_row, + native_denominator_is_the_universe, native_population_green_set, native_member_is_eligible, native_member_is_a_subject_row, } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -31,3 +33,20 @@ test fn the_denominator_is_the_derived_universe_not_the_green_set() -> Bool { && !native_denominator_is_the_universe(universe: ["a", "b", "c"], green: ["a"], frontier: ["b", "c"], exclusions: []) && !native_denominator_is_the_universe(universe: ["a", "b"], green: ["a"], frontier: ["b"], exclusions: ["z"]) } + +// INHABITANCE: the real route, and it can go red today. The real emitted_subject_build_rows derive exactly +// the two labels the disjointness control above supplies (the two compiler products, operator ruling +// 2026-10-09: emitted_subject_build_rows stays the two products), and each of them refuses as a population +// member through the real predicate -- so deleting the label fold, changing the subject roster, or breaking +// native_member_is_a_subject_row reds this claim. The last two conjuncts run the same predicates over the real +// native_population_green_set; that row is empty until the first native adjudication lands (the plan's declared +// trigger), so they are the real path's last execution for the green set and carry no weight of their own yet. +test fn the_real_subject_rows_derive_the_supplied_labels_and_each_refuses_as_a_member_the_real_route() -> Bool { + let labels = emitted_subject_build_rows() |> map(r => emitted_subject_build_label_text(row: r)) + list_length(labels) == 2 + && any(labels, l => l == "//gunbc/instruments:self-host") + && any(labels, l => l == "//gunbc/instruments:v2-native-cli") + && !any(labels, l => !native_member_is_a_subject_row(member: l, subject_labels: labels)) + && !any(native_population_green_set, m => !native_member_is_eligible(member: m)) + && !any(native_population_green_set, m => native_member_is_a_subject_row(member: m, subject_labels: labels)) +}