From 5fa77cc25faea1adea2ffdffcbb7ed84f4ca434e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 03:25:38 -0400 Subject: [PATCH 01/46] WIP: proud-lynx-311 --- ROADMAP.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index 60979937257..71fbb5339d2 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -369,7 +369,7 @@ Per-row tagging is a scheduled follow-up sweep — **trigger:** post-merge of th ### P0 — real bugs (silent wrong execution) -- **render.dag repeat_string ignores `n`**: `repeat_string` folds over singleton `[0]` so any `n > 0` returns one copy of `s`. Propagates to `indent_text`. Dissolution: fold over a length-`n` list or use a `repeat` combinator. Owner: immediate dispatch. +- **~~render.dag repeat_string ignores `n`~~** — **RETIRED 2026-05-05**. `repeat_string` at `dsl/std/render.dag:178-189` (and the bootstrap mirror `dsl/std/render_repeat_string_bootstrap.dag`) is a recursive `repeat_string_loop(acc, s, remaining)` that descends `remaining` and concats `s` each step — no `fold` over `[0]` remains. Ratcheted by `src/v2/tests/src/render_repeat_test.rs::repeat_string_and_indent_text_semantics_via_interpreter` (asserts `repeat_string("x", 3) == "xxx"` and the indent_text-shaped pad path). - **REST_OPS test table drift — `CreateComment` path wrong**: test authority at `src/v2/tests/src/effects.rs:149-218` lists `POST /repos/{...}/pulls/{pull_number}/comments`; extdep authority at `dsl/extdeps/github/pulls.dag:179-195` says `/repos/{...}/issues/{issue_number}/comments`. Dissolution: test table consumes extdep operation facts directly; delete the parallel table. Owner: immediate dispatch. - **`__BUG_NO_PROFILE_…` fabrication sentinel in `dsl/std/types.dag:115-119`**: `container_param_name_required` returns `concat("__BUG_NO_PROFILE_", kind_name)` on miss; duplicated as fallback in `src/v2/tests/src/compiler-tests.rs:2350-2354`. Violates M5 and C-8 fail-closed. Dissolution: function returns `Option`, caller handles. Owner: immediate dispatch. From 9fae986ce9201f8e68a951c73fa71ff768bb8686 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 13:46:10 -0400 Subject: [PATCH 02/46] WIP: proud-lynx-311 --- ROADMAP.md | 2 +- .../r2-manager-brief-authority-matrix.md | 6 ++--- docs/briefs/r2-release-manager.md | 6 ++--- docs/design-tests-as-data-completeness.md | 24 +++++++++---------- docs/escalation-paths.md | 6 ++--- docs/r3-structure.md | 6 ++--- docs/substrate-reflection-design.md | 8 +++---- docs/thesis-validation-plan.md | 14 +++++------ 8 files changed, 35 insertions(+), 37 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 71fbb5339d2..de1105a391e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -422,7 +422,7 @@ Tracked debt not dispatched with the 2026-04-21 lane wave (Lane 1e P3.0, SG-2c-4 - **`container_template_algebra_rows` string table is duplicate authority**: `dsl/std/types.dag:133-146` declares the renamed map (PR #651 collapsed both consumers onto a single `container_template_algebra` query); rows still duplicate the authoritative type aliases at `:211-213` (`type List = FreeMonoid`, etc.) across Pascal/snake spellings plus algebra self-identities. Dissolution trigger: when `.dag` gains alias reflection, the rows derive from the aliases directly and the hand-maintained table goes away. P2 Boundary Discipline / P1 receipt. Owner: unassigned; small scope. - **Emitter render-helper consolidation (Phase 3.1 candidate after 1e P3.0)**: `named_variant_id` / `render_named_template` / `primitive_type_id_for_port` / `walk_to_disj` / `algebra_field_for_operator` exist 3-5× across `src/v3/compiler/src/emit.rs` + `emit/python_target.rs` + `emit/rust_target.rs` (plus `walk_to_disj_decl` also in `lower.rs` and `infer.rs`). Collapse into one emitter-shared module. Different scope from 1e P3.0 which targets `behavior_result_port` / `port_is_consumed_from`; this is the render-side tranche. P2 Boundary Discipline receipt. Owner: queued behind 1e P3.0 as the natural follow-up. -- **Stale §-style and line-number cross-references to pre-rewrite `INVARIANTS.md` — PARTIAL (T-Receipts W1).** The ledger-named refs in `docs/design-db16-refined-generic-substitution.md`, `docs/perf/clone-elimination.md`, `docs/lane2-compile-time-proofs.md`, `src/v3/M1_DESIGN.md`, `src/v3/SELF_HOSTING.md`, `docs/history/sg-4b-1-fix-declaration-lookup-cleanup.md`, and `docs/briefs/p0-bug-no-profile-sentinel.md` now use stable `INVARIANTS.md#` / principle anchors instead of line-number or pre-rewrite § references. Broader stale INVARIANTS prose outside that named set remains a follow-up sweep; this receipt only closes the listed references. +- **Stale §-style and line-number cross-references to pre-rewrite `INVARIANTS.md` — PARTIAL (T-Receipts W1 + :425 slice 1).** The ledger-named refs in `docs/design-db16-refined-generic-substitution.md`, `docs/perf/clone-elimination.md`, `docs/lane2-compile-time-proofs.md`, `src/v3/M1_DESIGN.md`, `src/v3/SELF_HOSTING.md`, `docs/history/sg-4b-1-fix-declaration-lookup-cleanup.md`, and `docs/briefs/p0-bug-no-profile-sentinel.md` now use stable `INVARIANTS.md#` / principle anchors instead of line-number or pre-rewrite § references. Slice 1 of the residual sweep (proud-lynx-311) extended that to `docs/design-tests-as-data-completeness.md`, `docs/thesis-validation-plan.md`, `docs/substrate-reflection-design.md`, `docs/r3-structure.md`, `docs/escalation-paths.md`, `docs/briefs/r2-manager-brief-authority-matrix.md`, and `docs/briefs/r2-release-manager.md`. Residual narrows to slice 2: `docs/emit-target-spec-gaps.md`, `docs/design-substrate-external-primitives.md`, `docs/design-lens-framework.md`, `docs/thesis/doc-authority.md`, `docs/r2-structure.md`, `docs/design-emission-model.md`, `docs/design-tests-as-data-completeness.md` historical-receipt blocks, `docs/briefs/complexity-v2-v3-comparison-receipt.md`, `docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`, `docs/briefs/r3-pb-t-lensproducer-sub*-retirement.md`, `docs/briefs/r3-pb-runtime-equivalence-corpus-seed-audit.md`, `docs/briefs/r3-pb-t-fixedpoint-worker.md`, `docs/briefs/r2-pb-runtime-evaluator-convergence-matrix.md`, `docs/briefs/r3-pb-binshim-retirement-worker.md`, `docs/briefs/t-ground-languagespec.md`, `docs/briefs/t-ground-tests.md`, `docs/briefs/t-ground-lifetime-analyzer.md`, `docs/briefs/file-preference-bridge-dissolution.md`, `docs/history/lens-wire-in-audit-v2-comparison.md`, `ROADMAP.md` (self-references at :600/:614), and `.github/PULL_REQUEST_TEMPLATE.md`. - **`Strict Forward Progress` subdoc ↔ heading drift**: pre-existing inconsistency between `docs/invariants/strict-forward-progress.md` (bounded-execution content) and the reviewer-usage meaning of the SFP rule name (dissolution-progress). Flagged explicitly in both P4 and P5 of INVARIANTS.md post-#620 as future cleanup. Dissolution: either rename the subdoc to reflect its bounded-execution content (and author a new dissolution-progress subdoc), or split the subdoc into two. Small scope once the design call is made on naming. Owner: unassigned. - **v3 lens capability honesty pass (supersedes the complexity-receipt lane as originally scoped)**: the 2026-04-21 audit (see [docs/v3-lens-capability-register.md](docs/v3-lens-capability-register.md)) found that `src/v3/lenses/complexity.dag` does not subsume v2's `complexity.dag` — v2 produces symbolic `CostExpr` / `SizeExpr` with work/span/certainty/asymptotic-class, v3 produces a single integer depth per port. The same pattern holds for `cost.dag` (PROXY — no named size variables, Dimension wiring deferred), `idempotency.dag` (STUB — Rust oracle), and `parallelism.dag` (STUB — fail-closed placeholder). The originally-claimed "~13× LOC reduction with structurally stronger fail-closed guarantees" was comparing different functions of the program; retracted. **Follow-up work:** (1) the cementing-test discipline generalizes from one lens to every `regen.dag` entry (semantic-equality goldens per lens); (2) `docs/briefs/complexity-v2-v3-comparison-receipt.md` to be rewritten against the register — scope widens from "complexity receipt + registry rename" to "Band C honesty pass" once the register is merged. Substrate dissolution path: port `DescentEvidence` / `CallPattern` / `SubValueRelation` into the v3 substrate, wire per-call producers, and keep the E-M receipt that `MethodSemantics` is structurally subsumed rather than ported. Emit dissolution path: `match` lowering over user-defined sums (currently blocks `.dag` authority for idempotency + parallelism). Both are programs of work, not single lanes. Owner: unassigned; brief rewrite queues for after the 2026-04-21 wave's 5 lanes land and this register is in tree. - **Substrate carrier port program (scopes the "substrate dissolution path" half of the honesty pass above)**: design doc at [docs/design-substrate-carrier-port-program.md](docs/design-substrate-carrier-port-program.md) (2026-04-22). Decomposes the `DescentEvidence` / `CallPattern` / `SubValueRelation` / per-call producer work, with the `MethodSemantics` lane now **closed via M-b structural subsumption**. T/C/I port the carrier *types*; **E-P** has landed the first side-table producer slice (`v3_compiler::dag::per_call_descent_evidence`) for recursive self-call / arithmetic-descent evidence while leaving `TransformNode` unwidened. Full carrier parity still requires cost/complexity consumer wiring and same-source v2/v3 cementing. **E-M receipt:** v3 has no `ExprMethodCall` side slot; v2 `PlainMethodSemantics`, `AlgebraMethodSemantics`, and `ServiceMethodSemantics` map to `TransformTarget::{Callable, FieldProject, Operator}` plus typed declaration/effect metadata, so no ported `MethodSemantics` carrier or Rust mirror is added. Related: per-method metadata surface from `*_templates()` in `dsl/std/algebra.dag` (surfaced by Lane G / PR #654) — **§6a design call is closed** at [`docs/design-substrate-carrier-port-program.md` §6a](docs/design-substrate-carrier-port-program.md) (**Option 3** unified `MethodContract`; live receipt: `src/v3/std/algebra.dag`, `src/v3/lenses/cost.dag`). R2 program ledger: [`docs/r2-structure.md`](docs/r2-structure.md) Goal 5 (pick closed; follow-through per `docs/briefs/r2-release-6a-follow-through-worker.md`). Not part of the core four-carrier port. Closes **method carrier-parity** framing for `cost.dag` + `complexity.dag` at the structural **pick**; full `BEHAVIORALLY COMPLETE` for `cost.dag` additionally requires E-P consumer wiring and the register's separate non-carrier blockers (`Dimension` grammar/data-body wiring, named `SizeVariable` value semantics) that are outside this program, and opens P4 Decidability progress. Does NOT touch the emit-gap half (idempotency / parallelism); that stays in the receipt-closure wave. Owner: unassigned; remaining carrier-program work is E-P consumer/cementing plus the separately tracked non-carrier blockers. diff --git a/docs/briefs/r2-manager-brief-authority-matrix.md b/docs/briefs/r2-manager-brief-authority-matrix.md index 96df339147f..eedfbf56782 100644 --- a/docs/briefs/r2-manager-brief-authority-matrix.md +++ b/docs/briefs/r2-manager-brief-authority-matrix.md @@ -65,7 +65,7 @@ A continuous-state ledger / monitor / aggregated report owned by a manager throu - **Artifact format:** ledger entries / cadence reports inline in manager brief's "Working state" section, OR sibling ledger doc. - **Lifecycle:** activates on spawn → refreshes per cadence (integration-reflection pass / weekly health check / etc.) → dissolves on manager's dissolution. -**Examples:** R2 closure ledger (R2 Release Manager); velocity-tripwire ratio report (R2 Release Manager surfacing to Director per `INVARIANTS.md §P5`); Substrate-Manager bottleneck watch (R2 Release Manager, per `docs/r2-structure.md` §"R2 Release Manager"); R1 Closure Manager's lane status table. +**Examples:** R2 closure ledger (R2 Release Manager); velocity-tripwire ratio report (R2 Release Manager surfacing to Director per `INVARIANTS.md#p5-progress-is-dissolution`); Substrate-Manager bottleneck watch (R2 Release Manager, per `docs/r2-structure.md` §"R2 Release Manager"); R1 Closure Manager's lane status table. ### Category 5: Pre-spawn placeholder @@ -202,7 +202,7 @@ Before authoring a brief that references substrate state, gate condition, existi Cite specific `file:line` / brief filename / `§ref` in the brief's `Read first` section. State the audit receipt before slicing. The 7-reframe pattern on PR #836 (`feedback_verify_thesis_claims` violations: nested-optional gating, unhandled-diagnostic predicate-entailment default, unenumerated-effects 8-req elision, parametric-algebra producer redundancy, cardinality-for-int-lit redundancy, nominal-opaque 7th-connective option, int-lit consumer scope mismatch with `wise-pike-578`) demonstrates the failure mode this invariant prevents. This is the operationalization of `feedback_verify_thesis_claims` for the brief-authoring family. -These do not need new top-level INVARIANTS.md P-rules; `INVARIANTS.md §P2` (single-authority), `§P5` (dispatch-discipline), and the existing `feedback_verify_thesis_claims` discipline already cover them. These are the **local invariants** for the manager-brief family — collected here so brief authoring can cite this matrix as a single review checkpoint. +These do not need new top-level INVARIANTS.md P-rules; `INVARIANTS.md#p2-boundary-discipline` (single-authority), `§P5` (dispatch-discipline), and the existing `feedback_verify_thesis_claims` discipline already cover them. These are the **local invariants** for the manager-brief family — collected here so brief authoring can cite this matrix as a single review checkpoint. ## Refresh discipline @@ -219,5 +219,5 @@ These do not need new top-level INVARIANTS.md P-rules; `INVARIANTS.md §P2` (sin - Cross-manager signal example (Category 3 on PR #847): B7 priority-hint relay. - Standing duties (Category 4) inline in `r2-release-manager.md` Owned deliverables section. - Manager structure authority: [`docs/r2-structure.md` §"Manager structure"](../r2-structure.md). -- Discipline framework: [`INVARIANTS.md §P5` "Dispatch-Discipline Mechanisms"](../../INVARIANTS.md). +- Discipline framework: [`INVARIANTS.md#p5-progress-is-dissolution` "Dispatch-Discipline Mechanisms"](../../INVARIANTS.md). - Escalation discipline: [`docs/escalation-paths.md`](../escalation-paths.md). diff --git a/docs/briefs/r2-release-manager.md b/docs/briefs/r2-release-manager.md index c013be2b865..f6a342f2c84 100644 --- a/docs/briefs/r2-release-manager.md +++ b/docs/briefs/r2-release-manager.md @@ -19,7 +19,7 @@ R2's smallest cross-cutting deliverables + release coordination + demo + discipl | R2 closure demo coordination (Goal 6) | `docs/r2-structure.md` Goal 6 + structural-acceptance-per-lane-close discipline | LIVE on spawn (no separate brief; demo IS the structural acceptance gate per Director directive) | | B-wave Tier 0 through-merge | #810 §5 dispatch ordering | **LANDED** — B1 [#820](https://github.com/gunb-ai/gunbc/pull/820), B2 [#817](https://github.com/gunb-ai/gunbc/pull/817), B3 [#821](https://github.com/gunb-ai/gunbc/pull/821) merged to `main` **2026-04-26 (UTC)** per GitHub merge metadata (fail-closed P3 leak fixes; receipts on those PRs). | | B-wave Tier 2 (B5/B6/B7) | #810 §5 + [`debt-paydown-synthesis-2026-04-25.md` §"Tier 2" items 5–7](debt-paydown-synthesis-2026-04-25.md) | **LANDED in code/docs:** **B5** RESOLVED 2026-04-27 — structural gate `src/v3/compiler/tests/integration/r2_b5_loop_construction_closure_test.rs`; synthesis §5; [`r2-release-b5-loop-construction-closure-audit-worker.md`](r2-release-b5-loop-construction-closure-audit-worker.md) closed as receipt. **B6** RESOLVED 2026-04-26 — checklist + ROADMAP row per synthesis §6. **B7** RESOLVED 2026-04-27 — [#1014](https://github.com/gunb-ai/gunbc/pull/1014) per synthesis §7 (`patch_lower_helpers_*` retirement). Cross-manager brief: [`r2-release-b7-priority-hint-relay-to-pure-bootstrap.md`](r2-release-b7-priority-hint-relay-to-pure-bootstrap.md). | -| Discipline framework central reporting | INVARIANTS.md §P5 "Dispatch-Discipline Mechanisms" (c) + ROADMAP.md "Integration-reflection cadence" velocity-tripwire | LIVE on spawn (mechanism wired via PRs #810 + #812) | +| Discipline framework central reporting | INVARIANTS.md#p5-progress-is-dissolution "Dispatch-Discipline Mechanisms" (c) + ROADMAP.md "Integration-reflection cadence" velocity-tripwire | LIVE on spawn (mechanism wired via PRs #810 + #812) | | Thesis-claim coverage mapping | `docs/r2-structure.md` Open call 1 + `docs/thesis/r2-r3-thesis-mapping.md` (LIVE post-#1078) | LANDED via #1078 — initial mapping complete; refresh as lanes close | | R2 closure ledger | `docs/r2-structure.md` Manager structure section 7 | LIVE on spawn (tracks lane-close green status across all 6 other managers; sub-gate progress for T-LensProducer-Retirement R3 continuation) | | v2 retirement coordination | `docs/r2-structure.md` Transition mechanics v2-retirement note | LIVE on spawn (**post-R3** operational per `docs/r2-structure.md` §"R2 Release Manager" — moved from post-R2 to post-R3 with the R3 structured-program reframe; tracked but not gated) | @@ -41,7 +41,7 @@ R2's smallest cross-cutting deliverables + release coordination + demo + discipl 7. **B1, B2, B3 Tier 0 through-merge** — **complete at HEAD** — #820 / #817 / #821 merged **2026-04-26 (UTC)** per GitHub merge metadata. Standing: surface regressions only; no open Tier-0 coordination queue for this tranche. 8. **R2 demo coordination** — surface "it runs" artifacts at each lane close per **structural-acceptance-per-lane-close discipline** (the demo IS the structural gate; no separate authoring). 9. **Closure ledger** — track lane-close green status across all 6 other managers; surface unblocked work to idle workers; coordinate v2 retirement post-R3 (per `docs/r2-structure.md` §"R2 Release Manager" — v2 retirement moved from post-R2 to post-R3 with the R3 structured-program reframe); track sub-gate progress for T-LensProducer-Retirement R3 continuation per Director directive. **Live artifact: [`docs/r2-closure-ledger.md`](../r2-closure-ledger.md)** — also carries the signal-receiver protocol (cross-manager queue channel; what counts as a receipt; cadence touchpoints with velocity-tripwire reporting). -10. **Velocity-tripwire reporting** — each integration-reflection cadence pass, report introduction:dissolution PR ratio across all manager-authored work; surface ≥3:1 readings to Director per INVARIANTS.md §P5 (c). Manual sweep for dissolution-bearing feature PRs first per calibration caveat. +10. **Velocity-tripwire reporting** — each integration-reflection cadence pass, report introduction:dissolution PR ratio across all manager-authored work; surface ≥3:1 readings to Director per INVARIANTS.md#p5-progress-is-dissolution (c). Manual sweep for dissolution-bearing feature PRs first per calibration caveat. 11. **Substrate Manager bottleneck watch** — per `docs/r2-structure.md` watch condition: if Substrate becomes the new bottleneck (workers idle >7 days waiting for Substrate-authored briefs), surface to Director and recommend B4 split into dedicated B4 Identity-Carrier Manager. ## Cross-program dependencies @@ -140,7 +140,7 @@ Spawn refresh, 2026-04-28 (post-#1078, status-refresh against landed PRs): ## Cross-refs - Parent: `docs/r2-structure.md` §"R2 Release Manager" -- Discipline framework: INVARIANTS.md §P5 "Dispatch-Discipline Mechanisms" (a)/(b)/(c) +- Discipline framework: INVARIANTS.md#p5-progress-is-dissolution "Dispatch-Discipline Mechanisms" (a)/(b)/(c) - Cadence wiring: ROADMAP.md "Integration-reflection cadence" + velocity-tripwire reporting - Structural-acceptance-per-lane-close discipline: `docs/r2-structure.md` (Director-locked 2026-04-28) - §6a source: `docs/design-substrate-carrier-port-program.md §6a` (decision locked Option 3; live receipt landed) diff --git a/docs/design-tests-as-data-completeness.md b/docs/design-tests-as-data-completeness.md index d69520501df..ff49723d401 100644 --- a/docs/design-tests-as-data-completeness.md +++ b/docs/design-tests-as-data-completeness.md @@ -76,7 +76,7 @@ type ProgramShape // a new primitive form. Initial bootstrap: LiteralProgram only. ``` -**Why a single-variant coproduct, not a record**: per `INVARIANTS.md §P1` Step 2 (coproduct-vs-coordinate check), shapes are alternatives — a generated program is *one kind* at a time (a `LiteralProgram` OR, eventually, a `ParameterizedProgram`, OR a `SubstrateDerivedProgram`). The variants are not coordinates. Single-variant-at-bootstrap is structurally honest (it admits future variants without restructuring) and matches `feedback_state_space_vs_behavioral_invariants` (a coproduct is the right shape because illegal combinations like "both LiteralProgram fields and ParameterizedProgram fields populated simultaneously" become unrepresentable). +**Why a single-variant coproduct, not a record**: per `INVARIANTS.md#p1-modeling-faithfulness` Step 2 (coproduct-vs-coordinate check), shapes are alternatives — a generated program is *one kind* at a time (a `LiteralProgram` OR, eventually, a `ParameterizedProgram`, OR a `SubstrateDerivedProgram`). The variants are not coordinates. Single-variant-at-bootstrap is structurally honest (it admits future variants without restructuring) and matches `feedback_state_space_vs_behavioral_invariants` (a coproduct is the right shape because illegal combinations like "both LiteralProgram fields and ParameterizedProgram fields populated simultaneously" become unrepresentable). ### §2.2 `Quantifier` and `QuantifiedTestClaim` @@ -124,7 +124,7 @@ type TestSuite { Existing suite declarations migrate by wrapping each claim in `Enumerated(...)`. The migration is mechanical (one constructor wrap per claim site); the runner consumes both shapes uniformly via match. -**Alternative considered, rejected**: a single `TestSuite { enumerated_claims, quantified_claims }` record. Rejected per `INVARIANTS.md §P1` Step 2 — the order claims appear in the suite is a load-bearing facet (test reporting order, dependency traversal order); a record loses ordering across the two lists. The sum-typed list preserves the ordered sequence. +**Alternative considered, rejected**: a single `TestSuite { enumerated_claims, quantified_claims }` record. Rejected per `INVARIANTS.md#p1-modeling-faithfulness` Step 2 — the order claims appear in the suite is a load-bearing facet (test reporting order, dependency traversal order); a record loses ordering across the two lists. The sum-typed list preserves the ordered sequence. ### §2.4 Generator authoring shape @@ -148,17 +148,17 @@ data parse_smoke_universal: QuantifiedTestClaim = { } ``` -**Bootstrap ergonomics**: at R3 lane open, generators are explicit `List` declarations (no recursion, no induction over a substrate walk). This keeps the bootstrap predicate-runner change small (walk the list, apply predicate per element). Richer generators — programs derived from typed substrate walks (e.g., "every Behavior variant produces a smoke fixture") — attach via the same `ProgramGenerator` carrier without further substrate change: the body returns `List` regardless of how the body computes it. Per `INVARIANTS.md §P4` (decidability) the body must be bounded; that is already the substrate-wide invariant. +**Bootstrap ergonomics**: at R3 lane open, generators are explicit `List` declarations (no recursion, no induction over a substrate walk). This keeps the bootstrap predicate-runner change small (walk the list, apply predicate per element). Richer generators — programs derived from typed substrate walks (e.g., "every Behavior variant produces a smoke fixture") — attach via the same `ProgramGenerator` carrier without further substrate change: the body returns `List` regardless of how the body computes it. Per `INVARIANTS.md#p4-decidability` (decidability) the body must be bounded; that is already the substrate-wide invariant. ### §2.5 Why `ForAll` / `Exists` here, not as `TestPredicate` variants A tempting alternative shape: `TestPredicate::ForAll { generator, predicate }` and `TestPredicate::Exists { generator, predicate }` — fold the quantifier into the predicate coproduct. -**Rejected** per `INVARIANTS.md §P2` (boundary discipline) and `feedback_compositional_not_templating`. Reasons: +**Rejected** per `INVARIANTS.md#p2-boundary-discipline` (boundary discipline) and `feedback_compositional_not_templating`. Reasons: 1. **Predicate vs claim are different scopes.** A `TestPredicate` is "the property checked once given a single program." A quantifier is "how the family relates to the property." Conflating them confuses the reader: every other `TestPredicate` variant takes "the program" as implicit context (the surrounding `TestClaim.source`); `ForAll`/`Exists` would take "a generator" instead, breaking that invariant. 2. **Dispatch is structurally different.** The runner's `TestPredicate` evaluator (`test_runner::evaluate_predicate`) is a per-program function. A `ForAll` predicate is a per-*generator* function. The dispatch shape differs; encoding both through one coproduct buries the distinction in a runtime branch instead of a type-level partition. -3. **Recursion shape.** A `ForAll/Exists`-wrapped predicate could nest (`ForAll { predicate: Exists { ... } }`), implying second-order quantification. That is meaningful in mathematical logic but not in the substrate's bounded-forward-execution premise (per `INVARIANTS.md §P4`). Putting the quantifier on the *claim* makes nesting structurally unexpressible, which is the right answer at this stage of the language. +3. **Recursion shape.** A `ForAll/Exists`-wrapped predicate could nest (`ForAll { predicate: Exists { ... } }`), implying second-order quantification. That is meaningful in mathematical logic but not in the substrate's bounded-forward-execution premise (per `INVARIANTS.md#p4-decidability`). Putting the quantifier on the *claim* makes nesting structurally unexpressible, which is the right answer at this stage of the language. The structural separation (quantifier on `QuantifiedTestClaim`, not in `TestPredicate`) preserves the predicate's "given one program, check property" semantics and isolates the quantification at the claim level where it belongs. @@ -363,7 +363,7 @@ Steps 1–2 are sequential (carrier substrate must land before runner consumes i This lane is **owned by Verification Manager**, with **Substrate Manager assisting on the carrier authoring**: -- **Substrate Manager owns**: the `ProgramGenerator` / `ProgramShape` / `Quantifier` / `QuantifiedTestClaim` / `SuiteClaim` carrier additions in `src/v3/std/verification.dag`. The substrate-fact-introduction procedure (`INVARIANTS.md §P1` Steps 1–3) was applied during this design (see §9). Substrate authoring is a small, focused PR. +- **Substrate Manager owns**: the `ProgramGenerator` / `ProgramShape` / `Quantifier` / `QuantifiedTestClaim` / `SuiteClaim` carrier additions in `src/v3/std/verification.dag`. The substrate-fact-introduction procedure (`INVARIANTS.md#p1-modeling-faithfulness` Steps 1–3) was applied during this design (see §9). Substrate authoring is a small, focused PR. - **Verification Manager owns** (lane primary): the migration audit, every Rust→`.dag` port, the cementing dispatch port, the `m1_5_testgen_test.rs` final port. Owns all closure gates. Owns the migration audit declaration that drives per-PR progress reporting. - **Per-target emission tables (§4)** distribute by emitter: Rust template-contract row authoring is Substrate-adjacent (lives in `rust_method_template_contracts.dag`); same for Python and Go. Verification Manager dispatches the emitter table extensions and owns their behavioral-equivalence tests (Path A vs Path B). @@ -379,7 +379,7 @@ Five design questions surfaced during authoring. Per `feedback_design_before_imp **Question:** When `QuantifiedTestClaim { quantifier: ForAll, generator: G, predicate: P }` evaluates, does the runner walk every program in G's family even after the first failure, or stop at the first failing program? -**Resolved:** stop at the first failing program; emit a typed `Diagnostic` naming (a) the failing program shape, (b) the predicate's specific failure (not just "predicate failed" but the structured failure carrier the predicate already produces). Per `INVARIANTS.md §P3` (fail-closed): failing fast at the first counterexample matches "every detectable problem is a Diagnostic" — exhaustive walk after first failure produces noise without information gain (the user already knows the predicate doesn't hold universally). +**Resolved:** stop at the first failing program; emit a typed `Diagnostic` naming (a) the failing program shape, (b) the predicate's specific failure (not just "predicate failed" but the structured failure carrier the predicate already produces). Per `INVARIANTS.md#p3-fail-closed` (fail-closed): failing fast at the first counterexample matches "every detectable problem is a Diagnostic" — exhaustive walk after first failure produces noise without information gain (the user already knows the predicate doesn't hold universally). **Why not "walk all and report all":** a `ForAll` claim is logically refuted by one counterexample. Reporting more counterexamples is a performance cost without semantic content. A user who wants per-program diagnostics writes per-program enumerated `TestClaim`s (the existing surface); `ForAll` is the universal-quantifier semantic, not a "report all failing fixtures" surface. @@ -389,9 +389,9 @@ Five design questions surfaced during authoring. Per `feedback_design_before_imp **Question:** `ProgramShape` is a sum type. At lane open, which variants ship? Future extensions exist (parameterized programs, substrate-derived programs); naming all of them at lane open would inflate scope. -**Resolved:** **bootstrap with `LiteralProgram { source, file_name }` only**. This single variant matches the existing `TestClaim.source` / `file_name` pair and lets every today's enumerated test become a 1-element generator if rewritten as quantified. The substrate ships with `ProgramShape` as a 1-variant sum (per `INVARIANTS.md §P1` — single-variant sums are structurally honest, admitting future variants without restructuring). +**Resolved:** **bootstrap with `LiteralProgram { source, file_name }` only**. This single variant matches the existing `TestClaim.source` / `file_name` pair and lets every today's enumerated test become a 1-element generator if rewritten as quantified. The substrate ships with `ProgramShape` as a 1-variant sum (per `INVARIANTS.md#p1-modeling-faithfulness` — single-variant sums are structurally honest, admitting future variants without restructuring). -**Dissolution trigger for richer shapes** (per `INVARIANTS.md §P5` scaffold-discipline): when a real lane (e.g., a property-based testing lane in a future release) needs `ParameterizedProgram { template, parameter_bindings: List<...> }` or `SubstrateDerivedProgram { walker_ref: DeclarationRef }`, that lane authors the new variant alongside its first consumer. **The 1-variant bootstrap does not bridge** — the variant is structurally complete for the literal-program use case; future extensions are additive, not migration-required. +**Dissolution trigger for richer shapes** (per `INVARIANTS.md#p5-progress-is-dissolution` scaffold-discipline): when a real lane (e.g., a property-based testing lane in a future release) needs `ParameterizedProgram { template, parameter_bindings: List<...> }` or `SubstrateDerivedProgram { walker_ref: DeclarationRef }`, that lane authors the new variant alongside its first consumer. **The 1-variant bootstrap does not bridge** — the variant is structurally complete for the literal-program use case; future extensions are additive, not migration-required. ### §8.3 How does the cementing dispatch port preserve the register projection? — RESOLVED: cementing dispatch reads the register declaration directly @@ -416,7 +416,7 @@ fn cementing_modules_for_v2_complete_claims(register: List) The markdown table at `docs/v3-lens-capability-register.md` becomes a *rendering* of the structured register (per `feedback_no_metadata_markers` — the source of truth is structural, not textual; the markdown is generated documentation). **Authority shift** is a one-time migration; afterward, every register update is one `.dag` edit. -**Why not "keep markdown, add `.dag` mirror"**: parallel authority (per `INVARIANTS.md §P2`) — markdown and `.dag` would drift. Single-authority requires one source of truth. +**Why not "keep markdown, add `.dag` mirror"**: parallel authority (per `INVARIANTS.md#p2-boundary-discipline`) — markdown and `.dag` would drift. Single-authority requires one source of truth. **Lane scope**: the register migration (markdown → `.dag` declaration) is in scope for this lane (specifically step 5 — cementing dispatch port). The migration is small (one register declaration ~20 rows) and unblocks the cementing dispatch closure gate. @@ -460,9 +460,9 @@ The meta-harness becomes a `QuantifiedTestClaim` whose generator is "every mater **Question:** §4 named "Path B" (emit target-language test code from `TestClaim` declarations). When does Path B fire — always for every claim, or opt-in? -**Resolved:** opt-in via `TestSuite.target_emission: TargetEmission`, default `NativeRunnerOnly`. Per `INVARIANTS.md §P5` (progress is dissolution): emitting target-language test code for every claim by default would inflate the `target/` tree by ~Nx (one test runner per claim per target) without the user opting into the cross-target equivalence proof. Opt-in matches user intent and keeps default workflow lean. +**Resolved:** opt-in via `TestSuite.target_emission: TargetEmission`, default `NativeRunnerOnly`. Per `INVARIANTS.md#p5-progress-is-dissolution` (progress is dissolution): emitting target-language test code for every claim by default would inflate the `target/` tree by ~Nx (one test runner per claim per target) without the user opting into the cross-target equivalence proof. Opt-in matches user intent and keeps default workflow lean. -**Implementation note:** `TargetEmission` is a sum type per §4.3. The default value (`NativeRunnerOnly`) is set at the `TestSuite` declaration level, not per-claim; per-claim override is unnecessary at lane open (a user wanting per-claim variation declares two suites). Per `INVARIANTS.md §P1` Step 2, `TargetEmission` is a true coproduct (`NativeRunnerOnly` and `EmitToTargets(...)` are alternatives, not coordinates). +**Implementation note:** `TargetEmission` is a sum type per §4.3. The default value (`NativeRunnerOnly`) is set at the `TestSuite` declaration level, not per-claim; per-claim override is unnecessary at lane open (a user wanting per-claim variation declares two suites). Per `INVARIANTS.md#p1-modeling-faithfulness` Step 2, `TargetEmission` is a true coproduct (`NativeRunnerOnly` and `EmitToTargets(...)` are alternatives, not coordinates). **Why on `TestSuite`, not `TestClaim`:** test suites are the natural emission unit (per-suite Cargo target; per-suite Python module; per-suite Go test file). Per-claim emission would generate one target test runner per claim, exploding the file count. Per-suite emission generates one runner per suite per target — same shape as today's hand-authored Rust test files (one file per suite). The granularity matches existing target idioms. diff --git a/docs/escalation-paths.md b/docs/escalation-paths.md index 3d10b4bac6e..fded1f2ea2d 100644 --- a/docs/escalation-paths.md +++ b/docs/escalation-paths.md @@ -78,8 +78,8 @@ Locations swept (main HEAD only): | 28 | `docs/design-pure-bootstrap-zero.md` (implicit) | Migration path for a file in 35-file audit reveals path isn't structurally achievable | Escalate to PB-tier redesign | SOFT | | 29 | `docs/r2-structure.md:147` | Manager discovers program needs to expand (e.g., class-of-pattern dissolution under single-item brief) | Director adjudicates whether to expand program or split new lane (decision artifact format — see Fix 2 below) | SOFT | | 30 | `ROADMAP.md` (Grounding lane) | Scope changes to Grounding Manager's program | Route to director; amendments to THESIS.md require director-authored PRs | SOFT | -| 31 | `INVARIANTS.md §P5` | Paired-dispatch or per-PR gate violations / scaffold without named dissolution trigger | Release Manager surfaces violations; per-brief enforcement at authoring manager's point | SOFT | -| 32 | `INVARIANTS.md §P5` | Velocity tripwire fires (≥3:1 ratio scaffolds:deletions in 7-day window across all managers) | Release Manager surfaces to Director; indicates systemic violation pattern | SOFT (interpretation) / GROUNDED (calculation) | +| 31 | `INVARIANTS.md#p5-progress-is-dissolution` | Paired-dispatch or per-PR gate violations / scaffold without named dissolution trigger | Release Manager surfaces violations; per-brief enforcement at authoring manager's point | SOFT | +| 32 | `INVARIANTS.md#p5-progress-is-dissolution` | Velocity tripwire fires (≥3:1 ratio scaffolds:deletions in 7-day window across all managers) | Release Manager surfaces to Director; indicates systemic violation pattern | SOFT (interpretation) / GROUNDED (calculation) | ### Escalation target: Substrate Manager (post-R2-spawn) (1 clause) @@ -165,6 +165,6 @@ The sweep surfaced three clauses where the trigger is grounded but the resolutio - Authority docs swept: `INVARIANTS.md`, `ROADMAP.md`, `THESIS.md`, `docs/r2-structure.md` - Brief locations swept: `docs/briefs/*.md`, `docs/design-*.md`, `docs/thesis/*.md` -- Discipline framework: `INVARIANTS.md §P5` "Dispatch-Discipline Mechanisms" +- Discipline framework: `INVARIANTS.md#p5-progress-is-dissolution` "Dispatch-Discipline Mechanisms" - Cross-manager signal pattern: R1 "Cross-manager notifications queued" brief pattern (per `docs/r2-structure.md`) - Outstanding sweep targets: PR #835 (`pm/r2-manager-briefs`), PR #836 (`session/zesty-bear-812`) diff --git a/docs/r3-structure.md b/docs/r3-structure.md index f4f077c5c31..9faf0d6f2e9 100644 --- a/docs/r3-structure.md +++ b/docs/r3-structure.md @@ -179,16 +179,16 @@ Plus 2 priority corrections folded into existing lanes (Director-ratified 2026-0 **Owned program**: - **ROADMAP debt-row retirement** — every tracked-debt row in ROADMAP `### Post-merge debt (...)` sections gets a named retirement PR or explicit closure receipt before R3 close -- **Velocity-tripwire enforcement** — per `INVARIANTS.md §P5` (Progress Is Dissolution) Dispatch-Discipline Mechanisms (c) Velocity tripwire (introduction:dissolution PR ratio ≥3:1 in any 7-day window); manager surfaces tripwire readings to Director on cadence +- **Velocity-tripwire enforcement** — per `INVARIANTS.md#p5-progress-is-dissolution` (Progress Is Dissolution) Dispatch-Discipline Mechanisms (c) Velocity tripwire (introduction:dissolution PR ratio ≥3:1 in any 7-day window); manager surfaces tripwire readings to Director on cadence - **Per-PR discipline rule** — every R3 PR includes "debt receipt": names debt found in this PR, names debt paid in this PR, OR names a paydown-lane retirement PR for the debt; vague deferrals rejected - **Closure-receipt cadence** — converts Director's reflective-analysis findings into per-PR retirement work; closes the gap between "tracked debt" and "retired debt" -**Closure gate**: `r3_debt_paydown_zero_remaining` — no tracked-debt rows survive R3 close. Every tracked-debt row retires with a PR receipt before R3 close — unconditional. Per user directive 2026-05-02 (*"all 'accidentally deferred to post R3' into R3 now"*): **there is no post-R3 deferral path for tracked debt**. If a row appears unretirable within R3 it surfaces as a substrate gap requiring a named R3 lane (the directive that motivated this manager's creation), not a deferral. Per `INVARIANTS.md §P5` (Progress Is Dissolution): a tracked-debt row deferred past R3 close is the bridge-as-steady-state pattern P5 explicitly forbids; an escape hatch for "rare structurally-justified deferrals" reintroduces that pattern at lower cadence and must not exist. +**Closure gate**: `r3_debt_paydown_zero_remaining` — no tracked-debt rows survive R3 close. Every tracked-debt row retires with a PR receipt before R3 close — unconditional. Per user directive 2026-05-02 (*"all 'accidentally deferred to post R3' into R3 now"*): **there is no post-R3 deferral path for tracked debt**. If a row appears unretirable within R3 it surfaces as a substrate gap requiring a named R3 lane (the directive that motivated this manager's creation), not a deferral. Per `INVARIANTS.md#p5-progress-is-dissolution` (Progress Is Dissolution): a tracked-debt row deferred past R3 close is the bridge-as-steady-state pattern P5 explicitly forbids; an escape hatch for "rare structurally-justified deferrals" reintroduces that pattern at lower cadence and must not exist. **Authority discipline**: Manager authors per-PR rule documentation + standing reporting cadence. Does not author lane-level structural-acceptance gates (those owned by lane-owning managers). Does not adjudicate cross-program scope conflicts (those route to Director). Does enforce: every tracked-debt row gets a retirement PR before R3 close (per closure-gate at line 173 — no post-R3 deferral path; if a row appears unretirable, manager surfaces it as a substrate gap requiring a named R3 lane, not a deferral). **Hybrid mechanism**: -- **(a) Per-PR discipline rule** — every R3 PR includes debt receipt; vague deferrals rejected. Same shape as the per-PR gate from `INVARIANTS.md §P5` Dispatch-Discipline Mechanisms (b). +- **(a) Per-PR discipline rule** — every R3 PR includes debt receipt; vague deferrals rejected. Same shape as the per-PR gate from `INVARIANTS.md#p5-progress-is-dissolution` Dispatch-Discipline Mechanisms (b). - **(b) Standing manager territory** — owns systemic debt that doesn't fit organic per-PR cleanup; spawns workers for retirement work as needed; reports cadence-aligned to Director's autonomous-loop pattern. **Cross-program coordination**: Debt-Paydown Mgr coordinates with all 8 other R3 managers via the standard cross-manager queue + closure-ledger receipts. diff --git a/docs/substrate-reflection-design.md b/docs/substrate-reflection-design.md index e9498706f0b..6b1f6fa4fe4 100644 --- a/docs/substrate-reflection-design.md +++ b/docs/substrate-reflection-design.md @@ -1897,20 +1897,20 @@ This becomes a follow-up PR with a clean scope. still-valuable future lenses; both land as `.dag` programs after reflection. Neither is in this PR. -**`INVARIANTS.md §"Layer opacity"`:** the long-term target +**`INVARIANTS.md#p2-boundary-discipline (Layer Opacity)`:** the long-term target (§"Rust type-level enforcement") still applies. Reflection is the next step toward it, not the endpoint. Layer opacity's ultimate form is a `DisplayName` type that makes the violation impossible at the Rust level; this PR makes lens-based enforcement structurally cheaper, which buys time for the type-level work. -**`INVARIANTS.md §"Scaffold boundaries"`:** the Rust lenses are +**`INVARIANTS.md#p5-progress-is-dissolution (Scaffold Boundaries)`:** the Rust lenses are tracked scaffolds from this PR's perspective. The tracked `kernel_lens_set` count starts at 3 (the remaining Rust lenses after `lens_unused_parameters` migrates) and must monotonically decrease. Each Rust-lens deletion is a ratchet tick. -**`INVARIANTS.md §"Semantic authority after lowering"`:** this +**`INVARIANTS.md#p2-boundary-discipline (Semantic Authority After Lowering)`:** this PR extends the invariant's reach. Lenses currently read substrate state through Rust field access; after reflection, they read through query primitives that go through the same authority path @@ -2621,7 +2621,7 @@ deferred with a note. | Canonical target test requirement | §5 — tests preserved | | Checkpoint dissolution default | (general project doctrine — not specific to this PR) | | Compositional layering (thesis-level) | §7.1 — self-inspection is a new subsection | -| Rename test as regression check | (covered by existing `INVARIANTS.md §"Layer opacity"`) | +| Rename test as regression check | (covered by existing `INVARIANTS.md#p2-boundary-discipline (Layer Opacity)`) | If a recent thread is missing from this table and it belongs in-scope, flag it and this section updates. diff --git a/docs/thesis-validation-plan.md b/docs/thesis-validation-plan.md index f7767e15e1d..7ce5ad49a38 100644 --- a/docs/thesis-validation-plan.md +++ b/docs/thesis-validation-plan.md @@ -444,7 +444,7 @@ invariant and the lens mechanism. ### IL-1: Layer opacity lens -**Invariant ref:** INVARIANTS.md §"Layer opacity". +**Invariant ref:** INVARIANTS.md#p2-boundary-discipline (Layer Opacity). **Testable form:** no below-boundary string literal in consumer code. Rename a std/ identifier → no compile behavior change. **Status:** PARTIALLY TESTABLE. @@ -455,7 +455,7 @@ code. Rename a std/ identifier → no compile behavior change. ### IL-2: Single authority lens -**Invariant ref:** INVARIANTS.md §"No duplicate representations". +**Invariant ref:** INVARIANTS.md#p2-boundary-discipline (No Duplicate Representations). **Testable form:** for each fact, exactly one declaration is authority. No `fn(A) -> B` where A and B are structurally equivalent (parallel representation). @@ -465,8 +465,7 @@ equivalent (parallel representation). ### IL-3: Structural dispatch lens -**Invariant ref:** INVARIANTS.md §"No case enumeration for open -sets". +**Invariant ref:** INVARIANTS.md#p3-fail-closed (No Case Enumeration For Open Sets). **Testable form:** no string-keyed match arm where a structural walk through declarations would suffice. **Status:** DEFERRED. @@ -475,8 +474,7 @@ walk through declarations would suffice. ### IL-4: Cost coverage lens -**Invariant ref:** INVARIANTS.md §"Cost algebra upstream of -primitives". +**Invariant ref:** INVARIANTS.md#p4-decidability (Cost Algebra Is Upstream Of Language Primitives). **Testable form:** every primitive declaration has a corresponding `CostExpr` in the algebra. `∀ primitive p, ∃ cost_class(p)`. **Status:** DEFERRED. @@ -485,7 +483,7 @@ primitives". ### IL-5: Facts flow forward lens -**Invariant ref:** INVARIANTS.md §"Facts Flow Forward". +**Invariant ref:** INVARIANTS.md#p2-boundary-discipline (Facts Flow Forward). **Testable form:** no per-field re-derivation across stages. Every field consumed at stage K traces to a producer at stage N ≤ K. **Status:** DEFERRED. @@ -494,7 +492,7 @@ field consumed at stage K traces to a producer at stage N ≤ K. ### IL-6: No fabrication lens -**Invariant ref:** INVARIANTS.md §"No fallbacks that fabricate". +**Invariant ref:** INVARIANTS.md#p3-fail-closed (No Fallbacks That Fabricate). **Testable form:** no catch-and-default pattern without an explicit error variant in the return type. **Status:** DEFERRED. From 31d31c78e9a8db23ea02ef2c28825b70b8966037 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 14:02:35 -0400 Subject: [PATCH 03/46] WIP: proud-lynx-311 --- .github/PULL_REQUEST_TEMPLATE.md | 6 +++--- ROADMAP.md | 6 +++--- docs/briefs/complexity-v2-v3-comparison-receipt.md | 2 +- docs/briefs/file-preference-bridge-dissolution.md | 2 +- docs/design-emission-model.md | 2 +- docs/design-lens-framework.md | 4 ++-- docs/history/lens-wire-in-audit-v2-comparison.md | 2 +- docs/r2-structure.md | 4 ++-- docs/substrate-reflection-design.md | 8 ++++---- docs/thesis-validation-plan.md | 14 ++++++++------ 10 files changed, 26 insertions(+), 24 deletions(-) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 79f24d0e1b6..aafe96a3370 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -7,7 +7,7 @@ If this PR adds, modifies, or expands a hand-Rust file under `src/v3/` — including Rust tests under `src/v3/compiler/tests/` and any other hand-authored `.rs` in the v3 tree, since they are part of the SG-0 census (T-PB-A non-test subset OR T-PB-B test subset) — fill in the -"Per-PR dissolution gate" section below per INVARIANTS.md §P5 +"Per-PR dissolution gate" section below per INVARIANTS.md#p5-progress-is-dissolution "Dispatch-Discipline Mechanisms" (b). PRs that touch only `.dag` source, generated Rust, docs, non-Rust test fixtures, or hand-Rust outside `src/v3/` may delete the gate @@ -45,7 +45,7 @@ Evaluator brief **(1)** as appropriate; do not duplicate PB-owned implementation ## Per-PR dissolution gate (required for new/expanded hand-Rust under `v3/`)