Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions dag/gunbc/plans/native_obligation_population.dag
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,7 @@ fn native_obligation_population_body() -> List<MarkdownBlock> {
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."),
]),
]
Expand Down
1 change: 1 addition & 0 deletions dag/gunbc/roadmap/roadmap_authority.dag
Original file line number Diff line number Diff line change
Expand Up @@ -936,6 +936,7 @@ fn declared_roadmap_nodes() -> List<RoadmapNode> {
"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."),
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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))
}