From fce91b05a08f5af6df0c315a849f28eed937d034 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 00:02:27 +0000 Subject: [PATCH 1/5] docs(r3): align S-1 brief Pop A scope with population-coverage-audit (post-merge correction) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary PB Mgr post-merge review at [`gunb-ai/gunbc#1134` comment-4375420840](https://github.com/gunb-ai/gunbc/issues/1134#issuecomment-4375420840) flagged that the merged S-1 brief (PR #1711, sha 126cb1fea) had Pop A property naming drift from `docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A", which is the authoritative scope. The merged version named (incorrectly): - `prop_run_steps_termination` / `prop_run_steps_foo` (run-step termination) - Peano materialization cap - `behavior_round_trip` / `behavior_round_trip_bar` (behavior round-trip) Audit-canonical scope is **four coverage items** on `dsl/std/induction.dag` + `dsl/std/termination.dag`: - **A.1**: `derive_bound` / `master_theorem` fail-closed boundary coverage - **A.2**: `int_pow_bounded` / `ceil_log` boundary coverage - **A.3**: `peano_literal_materialization_cap` + `positive_descent_amount_from_positive_int` / `proportional_divisor_from_int_at_least_two` cap coverage - **A.4**: `meet_sub_value` / `join_sub_value` `ShrinkFactor`-preservation coverage Verified each item against the audit per substrate-line citations (`src/v3/std/induction.dag` :281 / :329 / :767 / :802 / :808 / :823 / :897; `src/v3/std/termination.dag` :140 / :146 / :162). Substrate live for all four; mechanical port from v2. ## Why this matters Pop A dispatch is the immediately-dispatchable worker action upon S-1 brief landing. Wrong property names + wrong target surfaces would have routed the dispatched worker to migrate properties that don't match the v2-test receipts cool-stag's PB inventory tracks — worker either stalls or migrates similarly-named-but-different properties that don't preserve the actual G-2 ratchets. PB Mgr noted: *"PB can still dispatch using the audit as the authoritative scope, but I recommend a docs-only correction PR to align."* This commit lands that correction. ## Discipline-correction surfaced This is the THIRD wrong Pop A property list in the brief. Failure mode timeline: 1. **First wrong list**: cool-stag's earlier read-back had markdown stripped by shell expansion; PM copied stripped property names into brief without grep-verifying against audit. 2. **Second wrong list**: Director sent "clean version" correction; PM applied it on aab4edc2f BUT the correction never made it to main (PR #1711 squash-merge took only the first commit; aab4edc2f stayed on branch only). 3. **Audit-canonical version**: cool-stag's post-merge review identified the actual authoritative source (`docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A") which I cited in cross-refs but never read. Per `feedback_verify_thesis_claims`: when authoring at brief layer + citing an audit, **read the audit**, don't just cross-reference it. The pattern of relying on relayed property names without grep-verifying against the canonical source has now produced wrong content twice. Discipline rule reinforced: every property/file/symbol name in PM-authored briefs must be grep-verified against either (a) live source code, or (b) the authoritative audit referenced in cross-refs. Citation-without-verification is the recurring failure mode across PR #1608 OTP false-citation, PR #1711 wrong Pop A list, and now this post-merge correction. ## R3 Debt Receipt - **Debt paid**: Pop A scope aligned with population-coverage-audit; brief now consumable by PB Mgr's Pop A dispatch without scope-mismatch risk. PB Mgr explicitly named this as scope-label-correction-not-S-1-reversal. - **Debt found + routed (process)**: citation-discipline failure mode catalogued. See "Discipline-correction surfaced" above. Adding to discipline-tracking memory: cross-references aren't verification; read the cited source. - **No new debt**: brief structure unchanged; only Pop A scope narrative corrected. PB Mgr can dispatch Pop A using either this corrected brief or the audit directly. ## What's NOT changed - 6 PM ratifications of PB input packet defaults — unchanged - Dispatch sequence (Pop A → Dispatches 2/3/4 cascade-gated) — unchanged - Cross-program asks routing (Substrate Decision 2 + Decision 5) — unchanged - G-2 prereq chain enumeration — unchanged - Constraints honored — unchanged Pre-merge structural review still valid; this corrects a scope-narrative error that snuck through. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../r3-tv2-retirement-s1-worker-brief.md | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md index 3b390d2f45a..5426a5fc8b0 100644 --- a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md +++ b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md @@ -13,7 +13,7 @@ S-1 unblocks the **G-1 implementation chain** for T-V2-Retirement: - **G-1**: deletion of Cargo.lock v2 dev-deps. Cascade-gated on §3.1 + §3.2 dispositions completing (one of which needs Substrate-side authority migration; the other needs PM choice between replace vs delete). - **G-2 prereq stack**: S-1 + S-2 + S-3 + S-4 + G-1. S-1 brief enumerates the entire chain (per Decision 6 below) so workers don't reconstruct it from the audit. -The narrowest immediately-dispatchable worker action under S-1 is **Pop A v3 property-test migration** (§"Worker dispatch sequence" below) — port four internal v2-test property receipts to live v3 surfaces. S-1-only; no Evaluator/Substrate authority migration prerequisite; prevents G-2 from silently dropping the ratchets. +The narrowest immediately-dispatchable worker action under S-1 is **Pop A v3 property-test migration** (§"Worker dispatch sequence" below) — port the **four audited Pop A coverage items** (per `docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A") onto live v3 `dsl/std/induction.dag` + `dsl/std/termination.dag` surfaces. S-1-only; no Evaluator/Substrate authority migration prerequisite; prevents G-2 from silently dropping the ratchets. ## Consumes (authoritative inputs) @@ -100,25 +100,30 @@ PB Mgr's recommended narrowest first dispatch under S-1 is **Pop A v3 property-t ### Dispatch 1 — Pop A v3 property-test migration (S-1-only; immediately dispatchable) -**Scope**: port four internal v2-test property receipts onto live v3 surfaces: -1. `prop_run_steps_termination` / `prop_run_steps_foo` (run-step termination property) -2. Peano materialization cap (Peano arithmetic materialization upper bound) -3. `behavior_round_trip` / `behavior_round_trip_bar` (behavior round-trip property) +**Scope**: port the **four audited Pop A coverage items** per `docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A" (authoritative source) onto live v3 surfaces: + +1. **A.1 — `derive_bound` / `master_theorem` fail-closed boundary coverage** (from v2 `std_induction`; v3 substrate at `src/v3/std/induction.dag:897` + `:823`). v3-side property test asserts fail-closed semantics: 0 branches → `ErrorBound`; negative branches → `ErrorBound`; invalid work exponents; `master_theorem` boundary cases. + +2. **A.2 — `int_pow_bounded` / `ceil_log` boundary coverage** (from v2 `std_induction`; v3 substrate at `src/v3/std/induction.dag:767` + `:802` + `:808`). v3-side property test re-asserts: negative-exp → `None`; non-negative matches `pow`; overflow at `2^63` → `None`; degenerate-base cap (`0`/`1`/`-1`) doesn't deep-recurse; `ceil_log` semantics. + +3. **A.3 — `peano_literal_materialization_cap` + `positive_descent_amount_from_positive_int` + `proportional_divisor_from_int_at_least_two` cap coverage** (from v2 `std_induction` + `std_termination`; v3 substrate at `src/v3/std/termination.dag:140` (cap=256) + `:146` + `:162`). v3-side property test asserts oversize `Int` inputs → `None`; cap of 256 is single-source v3 declaration. **Bonus**: v3 test cites `peano_literal_materialization_cap()` directly so the cap value is grep-clean across the codebase (replaces magic 256 in v2 test bodies). + +4. **A.4 — `meet_sub_value` / `join_sub_value` `ShrinkFactor`-preservation coverage** (from v2 `std_induction`; v3 substrate at `src/v3/std/induction.dag:281` + `:329`). v3-side property test ports meet/join cases against v3 `SubValueRelation` / `InductiveField` / `RecursionShape` constructors; `ShrinkFactor`-preservation invariant is identical between versions; near-mechanical port. **Why this dispatch is narrowest**: - S-1-only (does NOT need R2-Evaluator/PB-Runtime/Substrate authority migration) - Prevents G-2 from silently dropping the property ratchets - Prerequisite-shaped (preserves test surface for later cleanup) rather than deletion-shaped (which would break G-1) - Single-author work (no cross-program coordination per dispatch) +- Substrate is **LIVE on v3 side for all 4 items** (verified per `r3-pb-tv2-population-coverage-audit.md` §"Population A summary" — no R2-Evaluator / PB-Runtime / Substrate-authority dependency) **Live v3 surfaces** the migration targets: -- Run-step termination: live v3 termination semantics in `dsl/std/termination.dag` + v3 Evaluator -- Peano materialization cap: live v3 numeric carrier work per T-Numeric-Construction lane -- Behavior round-trip: v3 substrate behaviors (Value / Transform / Branch / Loop / Bind) + serialization +- `dsl/std/induction.dag` (A.1, A.2, A.4) +- `dsl/std/termination.dag` (A.3 cap + A.1 master_theorem-recurrence indirectly via `recurrence` form) -**Recommended worker assignment**: silent-boar or witty-tern (per PB Mgr's at-the-time read at `docs/briefs/r3-pb-tv2-g1-readiness-receipt.md` + read-back at [#1134 comment-4375362161](https://github.com/gunb-ai/gunbc/issues/1134#issuecomment-4375362161)). PB Manager picks specific worker per their cadence + readiness. +**Recommended worker assignment**: silent-boar or witty-tern (per PB Mgr's read-back at [#1134 comment-4375362161](https://github.com/gunb-ai/gunbc/issues/1134#issuecomment-4375362161)). PB Manager picks specific worker per their cadence + readiness. -**Closure**: dispatch produces one PR migrating the four property receipts to v3 surfaces; PB Manager confirms the property ratchets are preserved on v3 side; PR merges; ratchet status tracked in PB Manager's inventory. +**Closure**: dispatch produces one PR (or 4 sub-PRs per coverage item) migrating the four audited Pop A coverage items to v3 surfaces; PB Manager confirms property ratchets preserved on v3 side; PR(s) merge; ratchet status tracked in PB Manager's inventory. ### Dispatch 2 — B.1 (peano_arith consumer) — gated on Decision 1 prerequisite From b1bbece38d418fe4abc7f816e5dc9f6aefdbfb8e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 00:06:45 +0000 Subject: [PATCH 2/5] =?UTF-8?q?docs(r3):=20correct=20S-2/S-3=20labels=20to?= =?UTF-8?q?=20audit-canonical=20(T-FixedPoint=20/=20T-LensProducer-Retirem?= =?UTF-8?q?ent)=20=E2=80=94=20fix=20BLOCKING=20P2=20facts-flow-forward=20v?= =?UTF-8?q?iolation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Inline blocking review at PR #1713 line 154 (sha fce91b05a) flagged that my brief's S-2 = `kernel_algebra_profile` authority migration **drops the actual audit S-2 = T-FixedPoint closure**, violating P2 facts-flow-forward from the parent audit. Verified against `docs/audit/t-v2-retirement-audit.md` §1 STOP-condition table: | Label | My brief had | Audit-canonical | |---|---|---| | S-1 | PM-authored T-V2-Retirement worker brief | PM-authored T-V2-Retirement worker brief ✓ | | S-2 | substrate-fact-introduction for `kernel_algebra_profile` | **T-FixedPoint closed** (gate per r3-structure.md Lane 5: `pb_self_compile_fixed_point`) | | S-3 | `verification.dag` convergence design call | **T-LensProducer-Retirement closed** (3 sub-gates) | | S-4 | PB-Runtime trampoline live | PB-Runtime trampoline live ✓ | S-1 + S-4 were correct; S-2 + S-3 were wrong. The kernel_algebra_profile authority migration (my-old-S-2) is actually the §3.2 prerequisite for G-1 (one of the v2-oracle test consumer dissolutions). The verification.dag convergence (my-old-S-3) is a G-2 prerequisite independent of S-1+S-2+S-3+S-4 per audit §"verification.dag convergence" position. ## Fix §"G-2 prerequisite chain" rewritten to match audit S-N definitions: - **S-2 — T-FixedPoint closed** (gate per r3-structure.md Lane 5; PB Mgr lane; R3 in flight). Cited audit §1 directly. - **S-3 — T-LensProducer-Retirement closed** (3 sub-gates: `lens_apply.rs` / `lens_testgen.rs` / `regen_lens.rs`; PB Mgr lane). Cited audit §1 + design-pb-runtime-interpreter.md §5.1. - **S-4 — PB-Runtime trampoline live** (unchanged; was already correct). - Added explicit note that Decision 2 + Decision 5 routings are §3 audit prerequisites within G-1/G-2 implementation work, NOT in the S-N stack — clarifies the distinction between gate-stack labels (S-1/S-2/S-3/S-4) and routing decisions. The rationale paragraph explicitly cites audit §1 framing: *"S-2 (T-FixedPoint) and S-3 (T-LensProducer-Retirement) are explicit prerequisites because their closure is what allows S-4 (PB-Runtime trampoline) to be the live bootstrap; without S-2+S-3, removing src/v2/stage0 from the workspace breaks the build chain even if PB-Runtime is technically present."* ## Discipline-correction surfaced This is the **fourth** wrong content in this brief cycle. Failure pattern: 1. cool-stag's stripped-markdown read-back → wrong Pop A property names (1st) 2. Director's clean-version → orphaned correction (2nd) 3. cool-stag's audit-pointer in post-merge review → audit-canonical Pop A scope (3rd; this PR's main fix) 4. Inline review on S-2/S-3 labels → wrong gate-stack assignments (4th; this commit) All four are the same citation-discipline failure: I cited the audit in cross-refs but didn't verify content against it. The audit was the canonical source for **all four** (Pop A scope + S-N labels) — should have been the FIRST thing I read end-to-end at brief-authoring time. Discipline rule reinforced: **cross-references aren't verification; read the cited authority end-to-end at authoring time, not just when reviewers point at specific sections.** Adding to discipline-tracking memory. ## R3 Debt Receipt - **Debt paid**: BLOCKING P2 facts-flow-forward violation corrected. S-N labels now match audit-canonical definitions. Brief no longer drops S-2 (T-FixedPoint) and S-3 (T-LensProducer-Retirement) from the prerequisite stack. - **Debt found + routed (process)**: citation-discipline failure pattern is now four-instance. Adding hard rule to memory: when authoring a brief that cites an audit, read the audit end-to-end at authoring time. Cross-references aren't verification. - **No new debt**: substantive S-N gate definitions consume audit text directly; no new disposition introduced. PR #1714 base unchanged (Pop A scope-label correction); this commit corrects S-N labeling on the same branch as a follow-on fix in the same review cycle. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../r3-tv2-retirement-s1-worker-brief.md | 35 ++++++++++++++----- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md index 5426a5fc8b0..33e72cc9d7a 100644 --- a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md +++ b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md @@ -153,28 +153,47 @@ PB Mgr's recommended narrowest first dispatch under S-1 is **Pop A v3 property-t ## G-2 prerequisite chain (full retirement of `src/v2/`) -Per audit §1, G-2 prereq stack is `S-1 + S-2 + S-3 + S-4 + G-1`. This brief covers S-1; the rest enumerated for worker dispatch surface: +Per `docs/audit/t-v2-retirement-audit.md` §1 STOP-condition table, G-2 prereq stack is `S-1 + S-2 + S-3 + S-4 + G-1`. This brief covers S-1; the rest enumerated per audit S-N definitions: -### S-2 — substrate-fact-introduction for `kernel_algebra_profile` +### S-2 — T-FixedPoint closed (audit §1 row "S-2") -Per Decision 2 routing, Substrate Manager owns this. v3-side single-authority `kernel_algebra_profile` lands at `dsl/std/algebra.dag` (or successor as v3 substrate inhabitance consolidates). Substrate-introduction procedure per [`INVARIANTS.md`](../../INVARIANTS.md) §P1. +Per audit: *"T-FixedPoint closed"* (gate per `r3-structure.md` Lane 5: `pb_self_compile_fixed_point` — `compiler.dag` compiles to bit-identical stage0 Rust). -### S-3 — `verification.dag` convergence design call +S-2 + S-3 closure is what allows S-4 (PB-Runtime trampoline) to be the live bootstrap — without S-2+S-3, removing `src/v2/stage0` from the workspace breaks the build chain even if PB-Runtime is technically present (audit §1). -Per Decision 5 routing, Substrate Manager owns the design call (or Director arb if Substrate cannot scope). Convergence determines whether v3's `TestPredicate` / `TestSuite` model fully replaces v2's `AssertKind` / `TestClaim` / `TestCase`, or whether some v2 surface continues under a renamed module path. +PB Manager-owned (T-FixedPoint lane). R3 in flight. -### S-4 — PB-Runtime trampoline live as bootstrap path +### S-3 — T-LensProducer-Retirement closed (audit §1 row "S-3") -Per `docs/design-pure-bootstrap-zero.md` §"First-time bootstrap" — PB-Runtime trampoline replaces v2-as-bootstrap-path. PB Manager-owned execution. +Per audit: *"T-LensProducer-Retirement closed (all 3 sub-gates: `lens_apply.rs`, `lens_testgen.rs`, `regen_lens.rs`)"*. + +PB Manager-owned (T-LensProducer-Retirement lane; sub-gates per `r2-pure-bootstrap-manager.md` row T-LensProducer-Retirement + `design-pb-runtime-interpreter.md` §5.1). R3 in flight. + +### S-4 — PB-Runtime trampoline live as bootstrap path (audit §1 row "S-4") + +Per audit: *"PB-Runtime trampoline lands such that bootstrap no longer routes through `src/v2/stage0`"*. Gate per `design-pb-runtime-interpreter.md` §3. + +PB Manager-owned. NOT MET; PB-Runtime interpreter-as-data is the gate. ### G-1 — Cargo.lock v2 dev-deps deletion (covered above; Dispatch 4) +G-1's STOP condition per audit §"G-1 STOP condition" is **S-1 only** (PM worker brief — landed via PR #1711). G-1's *implementation* additionally requires §3.1 + §3.2 dispositions (Dispatches 2-3 above; Decisions 1+2 of this brief). + ### G-2 — `src/v2/` workspace member removal + directory deletion -Final deletion. Cascade-gated on S-1 + S-2 + S-3 + S-4 + G-1 all closing. PB Manager-owned execution. +Final deletion. Cascade-gated on **S-1 + S-2 + S-3 + S-4 + G-1** all closing per audit §"G-2 STOP condition for G-2 work". PB Manager-owned execution. Per `docs/audit/t-v2-g2-deletion-plan-and-guardrails.md` for full deletion plan + guardrails. +### Note on Decision 2 + Decision 5 routings + +Decisions 2 + 5 (per §"PM decisions" above) are routings within G-1 / G-2 implementation work — **not** equivalent to the S-N gates: + +- **Decision 2** (`kernel_algebra_profile` v3-side authority migration) is the §3.2 prerequisite for G-1 (one of the two v2-oracle test consumer dissolutions; lets PB retire the parity test). Substrate-side authority migration; routed to Substrate Manager (jolly-ram-908 #1130). NOT in the S-N chain. +- **Decision 5** (`verification.dag` convergence) is a G-2 prerequisite (independent of S-1 + S-2 + S-3 + S-4) per audit §"verification.dag convergence" position. Substrate Manager design call; routed in parallel. NOT in the S-N chain. + +S-N labels match audit definitions (T-FixedPoint / T-LensProducer-Retirement / PB-Runtime trampoline). Decision 2 + Decision 5 are routing decisions within audit §3 surfaces, not the S-N stack. + ## Cross-program coordination (PM relays in parallel with this brief) Two cross-program asks routed in parallel with this brief landing: From 4cdd59a56471d97a731e7364f724d7dcdafd238d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 00:08:38 +0000 Subject: [PATCH 3/5] =?UTF-8?q?docs(r3):=20remove=20fabricated=20A.1-via-t?= =?UTF-8?q?ermination.dag=20routing=20=E2=80=94=20fix=20BLOCKING=20P2=20si?= =?UTF-8?q?ngle-authority=20violation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Inline blocking review (sha fce91b05a, line 117 on closed PR #1713) flagged that my surface-routing summary implicitly placed A.1 (`derive_bound` / `master_theorem`) in `dsl/std/termination.dag`. Audit (`docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A" A.1) explicitly says: *"v3-side substrate analog LIVE — fn derive_bound(...) declared at src/v3/std/induction.dag:897; fn master_theorem(form: RecurrenceForm) -> CostBound at :823."* Both functions live at `induction.dag`, not `termination.dag`. My "A.1 master_theorem-recurrence indirectly via 'recurrence' form" framing was fabricated — there's no audit support for routing master_theorem through termination.dag. The reviewer correctly flagged this as P2 single-authority/facts-flow-forward — the Pop A worker would have looked at the wrong surface. ## Fix §"Live v3 surfaces" rewritten with explicit per-symbol substrate-line citations directly from audit: **Before** (HEAD pre-fix): ``` - `dsl/std/induction.dag` (A.1, A.2, A.4) - `dsl/std/termination.dag` (A.3 cap + A.1 master_theorem-recurrence indirectly via `recurrence` form) ``` **After** (this commit): ``` - `dsl/std/induction.dag` — A.1 (`derive_bound`:897, `master_theorem`:823), A.2 (`int_pow_bounded`:767, `ceil_log`:802, `ceil_log_iter`:808), A.4 (`meet_sub_value`:281, `join_sub_value`:329) - `dsl/std/termination.dag` — A.3 (`peano_literal_materialization_cap`:140, `positive_descent_amount_from_positive_int`:146, `proportional_divisor_from_int_at_least_two`:162) ``` A.1 + A.2 + A.4 routed exclusively to `induction.dag`. A.3 alone routed to `termination.dag`. Each symbol cited with its substrate-line number per audit. ## Discipline-correction surfaced This is the **fifth** wrong content in this brief cycle. The pattern continues: surface routing summary added a fabricated "indirect via recurrence form" claim that wasn't supported by audit. Citation-without-verification at the summary-line level — even though I cited audit lines correctly in the per-item descriptions (line 105 / A.1 has correct `induction.dag:897 + :823`), the summary §"Live v3 surfaces" introduced a fabricated claim. Failure mode for THIS instance: when summarizing per-item details into a high-level surface-routing list, the summarization step itself can fabricate content without the per-item sources flagging it. Fix shape: summaries must cite the same source as per-item details, with line numbers, so the summary verifies against the audit at every layer. Adding to discipline-tracking memory: when authoring a surface-routing summary in a brief, every per-symbol routing must cite its substrate-line number directly from the audit. No "indirect" / "via" framing without explicit audit support. ## R3 Debt Receipt - **Debt paid**: BLOCKING P2 single-authority violation corrected. Surface routing now lists per-symbol substrate-line citations directly from audit; no fabricated "indirect" routing claims. - **Debt found + routed (process)**: fifth instance of citation-discipline failure pattern. Hard rule reinforced: summaries must cite at every layer; "indirect via X form" framings without audit support are fabrications waiting to be caught. - **No new debt**: per-symbol substrate-line citations consume audit text directly. PR #1714 base unchanged (Pop A scope-label correction); this is the third commit in the same review cycle (Pop A scope at fce91b05a + S-N labels at b1bbece38 + surface routing here). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-tv2-retirement-s1-worker-brief.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md index 33e72cc9d7a..ca1e43892d7 100644 --- a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md +++ b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md @@ -117,9 +117,9 @@ PB Mgr's recommended narrowest first dispatch under S-1 is **Pop A v3 property-t - Single-author work (no cross-program coordination per dispatch) - Substrate is **LIVE on v3 side for all 4 items** (verified per `r3-pb-tv2-population-coverage-audit.md` §"Population A summary" — no R2-Evaluator / PB-Runtime / Substrate-authority dependency) -**Live v3 surfaces** the migration targets: -- `dsl/std/induction.dag` (A.1, A.2, A.4) -- `dsl/std/termination.dag` (A.3 cap + A.1 master_theorem-recurrence indirectly via `recurrence` form) +**Live v3 surfaces** the migration targets (per audit substrate-line citations): +- `dsl/std/induction.dag` — A.1 (`derive_bound`:897, `master_theorem`:823), A.2 (`int_pow_bounded`:767, `ceil_log`:802, `ceil_log_iter`:808), A.4 (`meet_sub_value`:281, `join_sub_value`:329) +- `dsl/std/termination.dag` — A.3 (`peano_literal_materialization_cap`:140, `positive_descent_amount_from_positive_int`:146, `proportional_divisor_from_int_at_least_two`:162) **Recommended worker assignment**: silent-boar or witty-tern (per PB Mgr's read-back at [#1134 comment-4375362161](https://github.com/gunb-ai/gunbc/issues/1134#issuecomment-4375362161)). PB Manager picks specific worker per their cadence + readiness. From 27cc93002b2a7dd67a46259bc2114a77792803c7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 4 May 2026 20:10:54 -0400 Subject: [PATCH 4/5] WIP: Gunbc PM --- docs/briefs/r3-tv2-retirement-s1-worker-brief.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md index ca1e43892d7..86811784d62 100644 --- a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md +++ b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md @@ -13,7 +13,7 @@ S-1 unblocks the **G-1 implementation chain** for T-V2-Retirement: - **G-1**: deletion of Cargo.lock v2 dev-deps. Cascade-gated on §3.1 + §3.2 dispositions completing (one of which needs Substrate-side authority migration; the other needs PM choice between replace vs delete). - **G-2 prereq stack**: S-1 + S-2 + S-3 + S-4 + G-1. S-1 brief enumerates the entire chain (per Decision 6 below) so workers don't reconstruct it from the audit. -The narrowest immediately-dispatchable worker action under S-1 is **Pop A v3 property-test migration** (§"Worker dispatch sequence" below) — port the **four audited Pop A coverage items** (per `docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A") onto live v3 `dsl/std/induction.dag` + `dsl/std/termination.dag` surfaces. S-1-only; no Evaluator/Substrate authority migration prerequisite; prevents G-2 from silently dropping the ratchets. +The narrowest immediately-dispatchable worker action under S-1 is **Pop A v3 property-test migration** (§"Worker dispatch sequence" below) — port the **four audited Pop A coverage items** (per `docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A") onto live v3 `src/v3/std/induction.dag` + `src/v3/std/termination.dag` surfaces (audit-canonical root; v3-staged authority that v3 compiler reads). S-1-only; no Evaluator/Substrate authority migration prerequisite; prevents G-2 from silently dropping the ratchets. ## Consumes (authoritative inputs) From cfc86352b018c9fcbedf21d4f614b9cce3280ceb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 00:11:24 +0000 Subject: [PATCH 5/5] =?UTF-8?q?docs(r3):=20normalize=20Pop=20A=20v3=20surf?= =?UTF-8?q?ace=20root=20to=20src/v3/std/...=20per=20audit-canonical=20?= =?UTF-8?q?=E2=80=94=20fix=20gpt-5-5-pro=20Boundary=20Discipline=20finding?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary gpt-5-5-pro review at sha fce91b05 (manual trigger) flagged Boundary Discipline / single-authority finding (NON-BLOCKING): summary at line 16 + surface-routing list at line 121-122 used `dsl/std/induction.dag` + `dsl/std/termination.dag` while per-item details at lines 105-111 cited `src/v3/std/induction.dag:N` substrate-line anchors. Two different roots for the same v3 surfaces — avoidable ambiguity for a brief whose purpose is audit-aligned worker dispatch. ## Verification Both files exist: - `dsl/std/induction.dag` — older shared v2/v3 mirror (header: "Inductive type structure and structural recursion") - `src/v3/std/induction.dag` — v3-staged mirror (header: "v3-staged inductive structure ... Bootstrap-staged mirror of `dsl/std/induction.dag` for v3") Both contain `fn derive_bound` + `fn master_theorem` (parallel-authority pattern). `src/v3/std/...` is the v3-staged authority that the v3 compiler reads; `dsl/std/...` is the shared/older v2-aligned authority. The audit (`docs/briefs/r3-pb-tv2-population-coverage-audit.md` §"Population A") consistently cites `src/v3/std/...` as the v3-side substrate analog — that's the canonical v3-property-test target. ## Fix Normalized brief to use `src/v3/std/...` consistently: - Line 16 (summary): `dsl/std/induction.dag + dsl/std/termination.dag` → `src/v3/std/induction.dag + src/v3/std/termination.dag` (with rationale: "audit-canonical root; v3-staged authority that v3 compiler reads") - Lines 121-122 (surface routing): `dsl/std/induction.dag` → `src/v3/std/induction.dag`; `dsl/std/termination.dag` → `src/v3/std/termination.dag` (with rationale: "audit-canonical v3-staged authority root") Per-item details at lines 105-111 already used `src/v3/std/...` correctly; no change there. All references in the brief now consistent. ## Discipline-correction surfaced This is the **sixth** wrong-content instance in this brief cycle. New failure mode: parallel-authority confusion at root level — `dsl/std/...` and `src/v3/std/...` both exist, both contain the relevant functions, but only one (`src/v3/std/...`) is the v3-property-test target per audit. Without explicit verification of which root the audit cites, the brief drifted toward `dsl/std/...` in summary lines while details correctly cited `src/v3/std/...`. Pattern noted: when authoring a brief that names parallel-authority surfaces, **explicitly verify which root the audit cites** before composing summary text. The "v3-staged mirror" framing in `src/v3/std/induction.dag`'s file header is the giveaway: `src/v3/std/...` is the v3-canonical authority. Discipline rule (added to memory): for parallel-authority surfaces (e.g., `dsl/std/X.dag` + `src/v3/std/X.dag`), authoring discipline requires verifying which root is canonical for the consumer. The audit citation is the authoritative source; cross-reference against file headers + grep for canonical declarations. ## R3 Debt Receipt - **Debt paid**: NON-BLOCKING Boundary Discipline / single-authority finding corrected. Brief now uses `src/v3/std/...` consistently across summary + per-item details + surface routing. - **Debt found + routed (process)**: parallel-authority root confusion is the sixth instance of citation-discipline failure pattern in this brief cycle. Each instance has a slightly different shape (Pop A property names; S-N labels; surface routing fabrication; root-path normalization). Adding to discipline-tracking memory: cite-then-verify is the pattern; cross-references aren't verification at any layer. - **No new debt**: per-symbol substrate-line citations remain audit-canonical; only the root path normalized. PR #1714 base unchanged (Pop A scope-label correction); this commit normalizes root paths in the same review cycle. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/r3-tv2-retirement-s1-worker-brief.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md index 86811784d62..ba186b589ab 100644 --- a/docs/briefs/r3-tv2-retirement-s1-worker-brief.md +++ b/docs/briefs/r3-tv2-retirement-s1-worker-brief.md @@ -117,9 +117,9 @@ PB Mgr's recommended narrowest first dispatch under S-1 is **Pop A v3 property-t - Single-author work (no cross-program coordination per dispatch) - Substrate is **LIVE on v3 side for all 4 items** (verified per `r3-pb-tv2-population-coverage-audit.md` §"Population A summary" — no R2-Evaluator / PB-Runtime / Substrate-authority dependency) -**Live v3 surfaces** the migration targets (per audit substrate-line citations): -- `dsl/std/induction.dag` — A.1 (`derive_bound`:897, `master_theorem`:823), A.2 (`int_pow_bounded`:767, `ceil_log`:802, `ceil_log_iter`:808), A.4 (`meet_sub_value`:281, `join_sub_value`:329) -- `dsl/std/termination.dag` — A.3 (`peano_literal_materialization_cap`:140, `positive_descent_amount_from_positive_int`:146, `proportional_divisor_from_int_at_least_two`:162) +**Live v3 surfaces** the migration targets (per audit substrate-line citations; `src/v3/std/...` is the audit-canonical v3-staged authority root): +- `src/v3/std/induction.dag` — A.1 (`derive_bound`:897, `master_theorem`:823), A.2 (`int_pow_bounded`:767, `ceil_log`:802, `ceil_log_iter`:808), A.4 (`meet_sub_value`:281, `join_sub_value`:329) +- `src/v3/std/termination.dag` — A.3 (`peano_literal_materialization_cap`:140, `positive_descent_amount_from_positive_int`:146, `proportional_divisor_from_int_at_least_two`:162) **Recommended worker assignment**: silent-boar or witty-tern (per PB Mgr's read-back at [#1134 comment-4375362161](https://github.com/gunb-ai/gunbc/issues/1134#issuecomment-4375362161)). PB Manager picks specific worker per their cadence + readiness.