Skip to content
18 changes: 16 additions & 2 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -460,12 +460,26 @@ fn seed_growth_live_lookup(live: Map<String, Bool>, key: String) -> Bool? {
}

fn seed_growth_stale_justifications(live_items: List<DeclarationRef>) -> List<String> {
seed_growth_stale_declarations(live_items: live_items)
|> map(r => declaration_ref_display_key(ref: r))
}

// THE ROSTER BINDING IS ONE STEP AND THE KEY RENDERING ANOTHER. The real-roster binding is its own
// function so a witness can hold it to the COMPLETE roster (every row reported stale against a live
// population that names none of them) without paying the display-key render of every row, which is
// the expense and which no completeness assertion inspects.
fn seed_growth_stale_declarations(live_items: List<DeclarationRef>) -> List<DeclarationRef> {
seed_growth_stale_over(roster: seed_growth_roster_all_declarations(), live_items: live_items)
}

// THE STALENESS RELATION OVER A SUPPLIED ROSTER. A witness of the relation's shape supplies a
// small roster (DESIGN section 3, a witness discriminates at one interface).
fn seed_growth_stale_over(roster: List<DeclarationRef>, live_items: List<DeclarationRef>) -> List<DeclarationRef> {
let live = seed_growth_live_set(live_items: live_items)
filter(
xs: seed_growth_roster_all_declarations(),
xs: roster,
predicate: fn(r) { !seed_growth_live_has(live: live, r: r) }
)
|> map(r => declaration_ref_display_key(ref: r))
}

fn seed_growth_unjustified_additions(added: List<DeclarationRef>) -> List<String> {
Expand Down
44 changes: 36 additions & 8 deletions dag/test/claim/seed_growth_admission_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ import gunbc.seed_growth_admission {
seed_growth_forward_freeze_policy_note,
seed_growth_unjustified_additions,
seed_growth_stale_justifications,
seed_growth_stale_declarations,
seed_growth_stale_over,
seed_growth_roster_all_declarations,
seed_growth_roster_mechanical_checks_holds,
seed_growth_roster_well_formed_gate_holds
Expand All @@ -22,19 +24,45 @@ test fn seed_growth_roster_mechanical_checks_hold() -> Bool {

// THE JOIN IS SPLIT AND THE SPLIT IS THE ASSERTION. Under the single-candidate-set form these two
// calls were one, so the population that found an unjustified addition was the same one that
// declared every untouched roster row stale. Here the SAME candidate list goes to both functions
// and they must answer differently: the rogue is an unjustified addition, and passing it as the live
// declared every untouched roster row stale. Here the SAME candidate goes to both functions and
// they must answer differently: the rogue is an unjustified addition, and passing it as the live
// population makes every real roster row stale rather than none. A reimplementation that collapsed
// them again reds on the second conjunct.
test fn seed_growth_join_refuses_unknown_declaration() -> Bool {
let rogue = DeclarationRef {
// them again reds on the second claim. The two answers are independent, so they are two claims
// rather than one conjunction paying both under one budget (DESIGN section 3, a witness
// discriminates at one interface).
fn seed_growth_rogue_declaration() -> DeclarationRef {
DeclarationRef {
module_path: "v1_compiler.cli_run",
decl_name: "totally_unjustified_hand_rust_symbol",
field: WholeDeclaration
}
length(xs: seed_growth_unjustified_additions(added: [rogue])) == 1
&& length(xs: seed_growth_stale_justifications(live_items: [rogue]))
== length(xs: seed_growth_roster_all_declarations())
}

test fn seed_growth_join_refuses_unknown_declaration() -> Bool {
length(xs: seed_growth_unjustified_additions(added: [seed_growth_rogue_declaration()])) == 1
}

// THE ROSTER IS SUPPLIED, THE RELATION IS REAL. Rendering every roster row's display key put the
// whole-roster form of this claim over the new-witness cost requirement (re-derive:
// claim_executor --required-floor, its COMPLETED-OVER-COST-REQUIREMENT line), and the assertion
// inspects none of the keys. The generic relation is discriminated here on a supplied roster; the
// next claim holds the real binding to the complete roster.
test fn an_unknown_live_population_reports_every_roster_row_stale() -> Bool {
let roster = [
DeclarationRef { module_path: "v1_compiler.a", decl_name: "first", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.b", decl_name: "second", field: WholeDeclaration }
]
length(xs: seed_growth_stale_over(roster: roster, live_items: [seed_growth_rogue_declaration()])) == 2
&& length(xs: seed_growth_stale_over(roster: roster, live_items: roster)) == 0
}

// THE REAL BINDING RANGES OVER THE COMPLETE ROSTER. Against a live population that names no roster
// row, every row is stale -- so a staleness function bound to an empty roster or any strict subset
// reds here, which a_live_roster_declaration_is_not_reported_stale cannot detect (an empty binding
// also reports nothing stale). seed_growth_stale_justifications is this list rendered to keys.
test fn the_real_staleness_binding_covers_every_roster_row() -> Bool {
length(xs: seed_growth_stale_declarations(live_items: [seed_growth_rogue_declaration()]))
== length(xs: seed_growth_roster_all_declarations())
}

// A ROSTER ROW THAT STILL NAMES A LIVE ITEM IS NOT STALE. Without this control the staleness
Expand Down
6 changes: 6 additions & 0 deletions src/v2/workflow/required_floor.dag
Original file line number Diff line number Diff line change
Expand Up @@ -899,6 +899,11 @@ fn required_gate_prefixes() -> List<String> {
// in today but would silently widen if a sibling is ever planted. Its claims run through the census
// probe over planted fixture sources (no live-tree read, SubstrateInputsOnly in spirit -- the
// fixture sources are supplied strings), priced at NewWitnessTier.
// THE SEED-GROWTH ADMISSION WITNESS (operator ruling, escalation msg_341a9785, approved
// 2026-10-03). `test.claim.seed_growth_admission_witness` carries the seed-growth roster's
// duplicate-key and well-formed checks and the addition/staleness join; it matched no family prefix,
// so those reds executed on no merge lane. Admitted at exact module grain for the same reason as the
// test-reference wall: a family prefix would silently widen to any future sibling.
fn required_gate_authored_modules() -> List<String> {
[
"test.claim.runner_capacity_plan_witness",
Expand All @@ -916,6 +921,7 @@ fn required_gate_authored_modules() -> List<String> {
"test.claim.discovery_census_witness",
"v2.test.claim.effect_demand.effect_demand_floor_join_test",
"test.claim.test_reference_wall_witness",
"test.claim.seed_growth_admission_witness",
]
}

Expand Down