From 2d29ea4cd4264c9c309ba4204cd80c3ab2288c29 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 10:53:34 +0000 Subject: [PATCH 1/7] required_floor: admit test.claim.seed_growth_admission_witness to the authored-module roster Operator ruling (escalation msg_341a9785, approved 2026-10-03). Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/workflow/required_floor.dag | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/v2/workflow/required_floor.dag b/src/v2/workflow/required_floor.dag index f0553316ecf..2393d2dcb19 100644 --- a/src/v2/workflow/required_floor.dag +++ b/src/v2/workflow/required_floor.dag @@ -899,6 +899,11 @@ fn required_gate_prefixes() -> List { // 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 { [ "test.claim.runner_capacity_plan_witness", @@ -916,6 +921,7 @@ fn required_gate_authored_modules() -> List { "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", ] } From 42e19c78e6ae867c9fc18fe50d28b03b9107b553 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 11:28:13 +0000 Subject: [PATCH 2/7] seed_growth_admission_witness: split the join conjunction; warm the shared roster producer The join claim measured 81,515 eval steps against the ~72,300-step new-witness ceiling (silent-stag-886, claim_batch --hermetic). Its two answers are independent, so they become two claims; the nullary roster producer every claim of the module reads is enrolled warm rather than rebuilt per frame. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../seed_growth_admission_witness_test.dag | 24 ++++++++++++------- src/v2/workflow/floor_pure_producer_share.dag | 9 +++++++ 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/dag/test/claim/seed_growth_admission_witness_test.dag b/dag/test/claim/seed_growth_admission_witness_test.dag index 86570df8057..97c93a5822b 100644 --- a/dag/test/claim/seed_growth_admission_witness_test.dag +++ b/dag/test/claim/seed_growth_admission_witness_test.dag @@ -22,19 +22,27 @@ 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 +} + +test fn an_unknown_live_population_reports_every_roster_row_stale() -> Bool { + length(xs: seed_growth_stale_justifications(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 diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 76d80a4b24a..e3895b7fbc4 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -805,7 +805,16 @@ import v2.std.collection { List } // PreparedGrammar is one nullary producer, and the refusal-arm counts over the live grammar are // another. A PreparedGrammar is the value dag_prepared_grammar already serves; the census is a record // of two Ints. Both WARM: one grammar preparation is more than one claim's budget. +// THE SEED-GROWTH ROSTER IS ONE NULLARY PRODUCER READ BY EVERY CLAIM OF ITS WITNESS. +// test.claim.seed_growth_admission_witness (admitted to the required gate by operator ruling +// msg_341a9785, 2026-10-03) reads gunbc.seed_growth_admission seed_growth_roster_all_declarations +// in its mechanical-checks, well-formed, staleness and addition claims, and each claim frame +// rebuilt the ~400-row fold. claim_batch --hermetic over that entry (silent-stag-886's receipt for +// gunbc#13101) put the staleness claim near the 100ms new-witness ceiling with the fold paid inline. +// The value is a list of DeclarationRef records, small and portable. Re-derive from this run's +// [floor-shared-fill] ledger: the fill lands at preparation, Stored, and the claims serve hits. data floor_cross_claim_pure_producers_warm: List = [ + "gunbc.seed_growth_admission.seed_growth_roster_all_declarations", "v2.test.claim.parameter_reference.pr_program_parameter_paths", "v2.test.claim.parameter_reference.pr_program_grounding", "v2.test.claim.parameter_reference.pr_program_lexical_reads", From eba4914e7bfc595024833f4b8443b299138e16fc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 12:20:31 +0000 Subject: [PATCH 3/7] seed_growth roster: one row per declaration; staleness witness supplies its roster Admission surfaced reds already on main: eval_match and match_pattern were justified by both the kernel-grounding row (#12846) and the match-guard / value-depth rows (#12903), so the duplicate-key check failed. The later row drops them. The staleness claim (74,485 steps vs ~72,300 ceiling) now exercises seed_growth_stale_over on a supplied roster; the real-roster path stays executed by a_live_roster_declaration_is_not_reported_stale. The warm row is withdrawn: it did not move the cost. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../kernel_grounding_interpreter_seed_growth.dag | 7 +++++-- dag/gunbc/seed_growth_admission.dag | 9 ++++++++- .../claim/seed_growth_admission_witness_test.dag | 13 +++++++++++-- src/v2/workflow/floor_pure_producer_share.dag | 9 --------- 4 files changed, 24 insertions(+), 14 deletions(-) diff --git a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag index 7fdffad1a97..f7e5c750316 100644 --- a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag +++ b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag @@ -12,11 +12,14 @@ import gunbc.seed_growth { SeedGrowthJustification } // constructors out of the tree before the interpreter sees it. What is ADDED is the residue that // keeps the deletion fail-closed and keeps a structural Peano type structural. data kernel_grounding_interpreter_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + // ONE ROW PER DECLARATION. eval_match and match_pattern are already carried by the + // match-guard and value-depth rows (gunbc.interpreter_eval_correctness_seed_growth, #12903); + // naming them here too made the roster's duplicate-key check red, unseen until the witness + // was admitted to the required gate (gunbc#13101). This row's reason and trigger still + // describe the eval_match refusal and match_pattern deletion it made. hand_authored_declarations: [ DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_expr_inner", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_match", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_record_lit", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "match_pattern", field: WholeDeclaration }, ], reason: "The subject is the seed interpreter's own evaluation of three tree forms, which no .dag program can reach: eval_record_lit and match_pattern LOSE their spelling-keyed Zero/Succ arms (a deletion); eval_expr_inner evaluates a Peano-unfolded elaborated literal as its constructor image instead of as the kernel literal, because a Peano unfolding's destination is structural on every route now that a kernel-realized carrier never reaches that arm; and eval_match refuses, located, a constructor pattern matched against a host integer, because with the grounding arms gone such a match could only fall through to a later wildcard silently. The fold that replaces the deleted arms is .dag (v1.compiler.infer ground_kernel_views), so the only hand Rust this adds is the refusal and the image evaluation.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 598ead0bca2..dbb31b08fb8 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -468,9 +468,16 @@ fn seed_growth_live_lookup(live: Map, key: String) -> Bool? { } fn seed_growth_stale_justifications(live_items: List) -> List { + seed_growth_stale_over(roster: seed_growth_roster_all_declarations(), live_items: live_items) +} + +// THE STALENESS RELATION OVER A SUPPLIED ROSTER. The public function above binds it to the real +// roster; a witness of the relation's shape supplies a small roster instead of paying the +// whole-roster key map per claim (DESIGN section 3, a witness discriminates at one interface). +fn seed_growth_stale_over(roster: List, live_items: List) -> List { 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)) diff --git a/dag/test/claim/seed_growth_admission_witness_test.dag b/dag/test/claim/seed_growth_admission_witness_test.dag index 97c93a5822b..a076ad2b53f 100644 --- a/dag/test/claim/seed_growth_admission_witness_test.dag +++ b/dag/test/claim/seed_growth_admission_witness_test.dag @@ -6,6 +6,7 @@ import gunbc.seed_growth_admission { seed_growth_forward_freeze_policy_note, seed_growth_unjustified_additions, seed_growth_stale_justifications, + seed_growth_stale_over, seed_growth_roster_all_declarations, seed_growth_roster_mechanical_checks_holds, seed_growth_roster_well_formed_gate_holds @@ -40,9 +41,17 @@ 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. Over the whole roster this claim cost ~74.5k eval +// steps against the ~72.3k new-witness ceiling (gunbc#13101 floor), all of it the key map the +// assertion does not inspect. The real-roster path is still executed by +// a_live_roster_declaration_is_not_reported_stale below, which is the pairing obligation. test fn an_unknown_live_population_reports_every_roster_row_stale() -> Bool { - length(xs: seed_growth_stale_justifications(live_items: [seed_growth_rogue_declaration()])) - == length(xs: seed_growth_roster_all_declarations()) + 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 } // A ROSTER ROW THAT STILL NAMES A LIVE ITEM IS NOT STALE. Without this control the staleness diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index e3895b7fbc4..76d80a4b24a 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -805,16 +805,7 @@ import v2.std.collection { List } // PreparedGrammar is one nullary producer, and the refusal-arm counts over the live grammar are // another. A PreparedGrammar is the value dag_prepared_grammar already serves; the census is a record // of two Ints. Both WARM: one grammar preparation is more than one claim's budget. -// THE SEED-GROWTH ROSTER IS ONE NULLARY PRODUCER READ BY EVERY CLAIM OF ITS WITNESS. -// test.claim.seed_growth_admission_witness (admitted to the required gate by operator ruling -// msg_341a9785, 2026-10-03) reads gunbc.seed_growth_admission seed_growth_roster_all_declarations -// in its mechanical-checks, well-formed, staleness and addition claims, and each claim frame -// rebuilt the ~400-row fold. claim_batch --hermetic over that entry (silent-stag-886's receipt for -// gunbc#13101) put the staleness claim near the 100ms new-witness ceiling with the fold paid inline. -// The value is a list of DeclarationRef records, small and portable. Re-derive from this run's -// [floor-shared-fill] ledger: the fill lands at preparation, Stored, and the claims serve hits. data floor_cross_claim_pure_producers_warm: List = [ - "gunbc.seed_growth_admission.seed_growth_roster_all_declarations", "v2.test.claim.parameter_reference.pr_program_parameter_paths", "v2.test.claim.parameter_reference.pr_program_grounding", "v2.test.claim.parameter_reference.pr_program_lexical_reads", From 6fc8e23d574817114530cd3bce38f769fea09516 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 12:22:30 +0000 Subject: [PATCH 4/7] seed_growth witness: name the instrument rather than transcribe its figures (review 74732) Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/test/claim/seed_growth_admission_witness_test.dag | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dag/test/claim/seed_growth_admission_witness_test.dag b/dag/test/claim/seed_growth_admission_witness_test.dag index a076ad2b53f..46101bdb6ff 100644 --- a/dag/test/claim/seed_growth_admission_witness_test.dag +++ b/dag/test/claim/seed_growth_admission_witness_test.dag @@ -41,9 +41,9 @@ 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. Over the whole roster this claim cost ~74.5k eval -// steps against the ~72.3k new-witness ceiling (gunbc#13101 floor), all of it the key map the -// assertion does not inspect. The real-roster path is still executed by +// THE ROSTER IS SUPPLIED, THE RELATION IS REAL. Over the whole roster this claim completed over +// the new-witness cost requirement (re-derive: claim_executor --required-floor, its +// COMPLETED-OVER-COST-REQUIREMENT line), all of it the key map the assertion does not inspect. The real-roster path is still executed by // a_live_roster_declaration_is_not_reported_stale below, which is the pairing obligation. test fn an_unknown_live_population_reports_every_roster_row_stale() -> Bool { let roster = [ From 8c85f1a2aaf30d6b758f5fc53720e41da88319af Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 12:34:26 +0000 Subject: [PATCH 5/7] kernel_grounding seed-growth: move the one-row-per-declaration note to module-item grain Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/kernel_grounding_interpreter_seed_growth.dag | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag index f7e5c750316..4d41b3a7ca5 100644 --- a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag +++ b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag @@ -11,12 +11,12 @@ import gunbc.seed_growth { SeedGrowthJustification } // removed, because v1.compiler.infer ground_kernel_views now folds a kernel-grounded carrier's // constructors out of the tree before the interpreter sees it. What is ADDED is the residue that // keeps the deletion fail-closed and keeps a structural Peano type structural. +// ONE ROW PER DECLARATION. eval_match and match_pattern are already carried by the +// match-guard and value-depth rows (gunbc.interpreter_eval_correctness_seed_growth, #12903); +// naming them here too made the roster's duplicate-key check red, unseen until the witness +// was admitted to the required gate (gunbc#13101). This row's reason and trigger still +// describe the eval_match refusal and match_pattern deletion it made. data kernel_grounding_interpreter_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { - // ONE ROW PER DECLARATION. eval_match and match_pattern are already carried by the - // match-guard and value-depth rows (gunbc.interpreter_eval_correctness_seed_growth, #12903); - // naming them here too made the roster's duplicate-key check red, unseen until the witness - // was admitted to the required gate (gunbc#13101). This row's reason and trigger still - // describe the eval_match refusal and match_pattern deletion it made. hand_authored_declarations: [ DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_expr_inner", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_record_lit", field: WholeDeclaration }, From 4ba76d1149123de9f005624bf2341de4e959c550 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 14:12:58 +0000 Subject: [PATCH 6/7] drop the duplicate-key repair in favour of #13100's --- dag/gunbc/kernel_grounding_interpreter_seed_growth.dag | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag index 4d41b3a7ca5..49db2264ca6 100644 --- a/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag +++ b/dag/gunbc/kernel_grounding_interpreter_seed_growth.dag @@ -11,17 +11,12 @@ import gunbc.seed_growth { SeedGrowthJustification } // removed, because v1.compiler.infer ground_kernel_views now folds a kernel-grounded carrier's // constructors out of the tree before the interpreter sees it. What is ADDED is the residue that // keeps the deletion fail-closed and keeps a structural Peano type structural. -// ONE ROW PER DECLARATION. eval_match and match_pattern are already carried by the -// match-guard and value-depth rows (gunbc.interpreter_eval_correctness_seed_growth, #12903); -// naming them here too made the roster's duplicate-key check red, unseen until the witness -// was admitted to the required gate (gunbc#13101). This row's reason and trigger still -// describe the eval_match refusal and match_pattern deletion it made. data kernel_grounding_interpreter_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { hand_authored_declarations: [ DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_expr_inner", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_record_lit", field: WholeDeclaration }, ], - reason: "The subject is the seed interpreter's own evaluation of three tree forms, which no .dag program can reach: eval_record_lit and match_pattern LOSE their spelling-keyed Zero/Succ arms (a deletion); eval_expr_inner evaluates a Peano-unfolded elaborated literal as its constructor image instead of as the kernel literal, because a Peano unfolding's destination is structural on every route now that a kernel-realized carrier never reaches that arm; and eval_match refuses, located, a constructor pattern matched against a host integer, because with the grounding arms gone such a match could only fall through to a later wildcard silently. The fold that replaces the deleted arms is .dag (v1.compiler.infer ground_kernel_views), so the only hand Rust this adds is the refusal and the image evaluation.", + reason: "The subject is the seed interpreter's own evaluation of three tree forms, which no .dag program can reach: eval_record_lit and match_pattern LOSE their spelling-keyed Zero/Succ arms (a deletion); eval_expr_inner evaluates a Peano-unfolded elaborated literal as its constructor image instead of as the kernel literal, because a Peano unfolding's destination is structural on every route now that a kernel-realized carrier never reaches that arm; and eval_match refuses, located, a constructor pattern matched against a host integer, because with the grounding arms gone such a match could only fall through to a later wildcard silently. The fold that replaces the deleted arms is .dag (v1.compiler.infer ground_kernel_views), so the only hand Rust this adds is the refusal and the image evaluation. ALREADY JUSTIFIED BY THEIR OWN ROWS, and so not repeated here because the roster cites each declaration once: eval_match (gunbc.interpreter_eval_correctness_seed_growth match_arm_guard_seed_growth_justification) and match_pattern (gunbc.interpreter_eval_correctness_seed_growth value_depth_seed_growth_justification) -- each also carries this change's edit described above, and this row's trigger still governs that edit.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, trigger: "Delete the eval_match refusal and the eval_expr_inner image arm when match and literal evaluation are realized by the self-emitted interpreter, which reads the same folded tree and has no constructor-versus-integer case to refuse. Equivalently, when the seed interpreter's pattern matcher returns a typed refusal instead of an Optional, so an unfolded constructor pattern over an integer is refused where it is matched rather than by a pre-check in eval_match. Rewording the refusal or widening its exempt constructor list does not dissolve this row. The exemption (kernel_raw_payload_constructor) is keyed on the pattern's parent carrier spelling, Optional or Witness, because the seed's MatchPattern carries no DeclarationRef (review 73985); a DeclarationRef on the pattern is the next rung for that key.", current_boundary: "src/v1/stage0/src/v1_interpreter.rs eval_expr_inner, eval_match, eval_record_lit, match_pattern; src/v1/04_infer.dag ground_kernel_views; dag/gunbc/kernel_grounding_interpreter_seed_growth.dag", From d4f0cdb46df245f8280474f64e60f0a908cf3549 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 15:18:06 +0000 Subject: [PATCH 7/7] seed_growth staleness: hold the real binding to the complete roster Side-chat REQUEST_CHANGES (royal-moth-86): after the split nothing reddened an empty or partial roster binding. The roster binding is now its own step (seed_growth_stale_declarations) under the key render, and a new claim requires every roster row stale against a population naming none of them. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/seed_growth_admission.dag | 17 ++++++++++++----- .../seed_growth_admission_witness_test.dag | 19 +++++++++++++++---- 2 files changed, 27 insertions(+), 9 deletions(-) diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 6aed20c3915..2287fc24314 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -460,19 +460,26 @@ fn seed_growth_live_lookup(live: Map, key: String) -> Bool? { } fn seed_growth_stale_justifications(live_items: List) -> List { + 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) -> List { seed_growth_stale_over(roster: seed_growth_roster_all_declarations(), live_items: live_items) } -// THE STALENESS RELATION OVER A SUPPLIED ROSTER. The public function above binds it to the real -// roster; a witness of the relation's shape supplies a small roster instead of paying the -// whole-roster key map per claim (DESIGN section 3, a witness discriminates at one interface). -fn seed_growth_stale_over(roster: List, live_items: List) -> List { +// 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, live_items: List) -> List { let live = seed_growth_live_set(live_items: live_items) filter( 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) -> List { diff --git a/dag/test/claim/seed_growth_admission_witness_test.dag b/dag/test/claim/seed_growth_admission_witness_test.dag index 46101bdb6ff..cfaf45ce815 100644 --- a/dag/test/claim/seed_growth_admission_witness_test.dag +++ b/dag/test/claim/seed_growth_admission_witness_test.dag @@ -6,6 +6,7 @@ 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, @@ -41,10 +42,11 @@ 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. Over the whole roster this claim completed over -// the new-witness cost requirement (re-derive: claim_executor --required-floor, its -// COMPLETED-OVER-COST-REQUIREMENT line), all of it the key map the assertion does not inspect. The real-roster path is still executed by -// a_live_roster_declaration_is_not_reported_stale below, which is the pairing obligation. +// 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 }, @@ -54,6 +56,15 @@ test fn an_unknown_live_population_reports_every_roster_row_stale() -> Bool { && 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 // function above is satisfied by one that reports everything stale, which reports nothing. test fn a_live_roster_declaration_is_not_reported_stale() -> Bool {