diff --git a/docs/briefs/b4-2-structural-fold-shape-carrier-worker.md b/docs/briefs/b4-2-structural-fold-shape-carrier-worker.md new file mode 100644 index 00000000000..22a41166ecd --- /dev/null +++ b/docs/briefs/b4-2-structural-fold-shape-carrier-worker.md @@ -0,0 +1,116 @@ +# B4.2 β€” Structural fold-eligibility predicate `(M; B4 Phase 1 #2 of 4 β€” REVISED 2026-04-26 per royal-badger-32 audit)` + +> **Worker brief.** Reports through Substrate Manager (post-R2 spin-up) / +> Director (pre-spin-up). Sub-brief of the +> [B4 Identity-Carrier Substrate Pass program](b4-identity-carrier-substrate-pass.md) +> (merged via #814). +> +> **πŸ”„ REVISED 2026-04-26 by Director.** Original framing +> (`fold_step_formal: Option` carrier on `Instantiation`) +> was misdiagnosed: that carrier memoizes a fact already +> structural at `lens_apply.rs:114` +> (`find_fold_step_bind_via_instantiation`) β€” borderline +> parallel-representation. The Β§0.4 line-38 bridge actually skips +> on **accumulator/element type eligibility for R1's bounded +> interpreter**, NOT on step-formal binding. The two carriers +> address different questions; landing the original carrier would +> NOT close Β§0.4. PR #834 closed as misframed; this brief is +> re-authored against the correct dissolution shape. + +## Read first + +- **[`docs/briefs/b4-identity-carrier-substrate-pass.md`](b4-identity-carrier-substrate-pass.md)** β€” parent program brief. +- **[`src/v3/compiler/src/lens_apply.rs:14`](../../src/v3/compiler/src/lens_apply.rs)** β€” `is_fold_instantiation` already structurally identifies fold instantiations via `dag.std_list_fold_decl() == Some(*template)`. +- **[`src/v3/compiler/src/lens_apply.rs:22-39`](../../src/v3/compiler/src/lens_apply.rs)** β€” `fold_site_skips_d1_monomorph_list_fold_path` doc comment. **The line-38 bridge exists because algebra.dag folds use `List` accumulators while R1's bounded interpreter only certifies `Int` accumulator + `Behavior` elements.** This is the actual Β§0.4 dissolution target. +- **[`src/v3/compiler/src/lens_apply.rs:114`](../../src/v3/compiler/src/lens_apply.rs)** β€” `find_fold_step_bind_via_instantiation`: already-structural step-Bind recovery via `fold_template_callable_formals(dag, *template)` walked against `arguments`. **Do not duplicate this with a memoization carrier** (per `feedback_parallel_representation_debt`). +- **[`src/v3/compiler/src/lens_apply.rs:38, :372-383`](../../src/v3/compiler/src/lens_apply.rs)** β€” the Β§0.4 sites. Line 38 is the load-bearing bridge (accumulator-type skip); :372-383 is the same skip applied to a sibling fold path. +- **[Helper's own dissolution-trigger doc](../../src/v3/compiler/src/lens_apply.rs)** β€” at the line-38 site, the inline comment names: *"R1-certified step shape, or third Transform operand for the step so arity matches eval_std_fold."* Either is the dissolution target β€” neither is `fold_step_formal`. +- **[`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag)** β€” substrate authority. +- **`feedback_parallel_representation_debt`** β€” do not memoize already-structural facts as new substrate fields. +- **`feedback_audit_adjacent_authority_first`** β€” grep + read call sites before designing carriers. +- **`feedback_design_before_implement`** β€” pre-flight audit prevents 1382-site propagation of a contested shape. + +## Frame (revised) + +Per the audit at `lens_apply.rs:22-39`: the `span.file.ends_with("std/algebra.dag")` check at line 38 exists because the bounded R1 interpreter at `eval_std_fold` only certifies certain accumulator/element type shapes. `algebra.dag` folds use `List` accumulators that the interpreter cannot evaluate. The skip prevents the bounded interpreter from running on incompatible shapes; it falls back to a different path. + +The **actual Β§0.4 dissolution** is a structural eligibility predicate: given a fold `Instantiation`, can the bounded R1 interpreter certify its accumulator + element types? If yes, run; if no, skip via the fallback. The predicate is a **structural query against the resolved type arguments**, NOT a new substrate field. + +**The right shape is likely no new substrate.** Possible paths: + +1. **Pure structural query (preferred).** A helper `interpreter_eligible_fold(dag, instantiation) -> bool` that resolves the accumulator + element type arguments and matches against the bounded interpreter's supported set. No substrate change. The line-38 bridge becomes a structural call. +2. **Structural witness carrier (fallback if pure-query has surprising structural holes).** Optional eligibility tag on the fold's `Instantiation` populated at lowering when the type args resolve to interpreter-supported shapes. Only justified if the pure-query path doesn't compose cleanly with existing dispatch. + +Per `feedback_audit_adjacent_authority_first`: **start with the audit. The audit may show option 1 closes Β§0.4 with zero new substrate.** + +## Pre-author authority audit (mandatory) + +Before designing any new substrate, grep for and read carefully: + +1. **`is_fold_instantiation` (`lens_apply.rs:14`)** β€” already-structural; reuse don't duplicate. +2. **`fold_template_callable_formals` + `find_fold_step_bind_via_instantiation` (`lens_apply.rs:114`)** β€” already-structural step-Bind recovery; **do NOT add a memoization carrier**. +3. **`eval_std_fold` and the bounded interpreter** β€” what types does it actually certify? What's the supported set? The audit must produce a precise list of the eligible accumulator+element type shapes. +4. **Line-38 + line-372-383 skip paths** β€” what's the fallback? Is the fallback the right path for ineligible folds, or does the bridge mask a different bug? +5. **Existing structural query helpers** in `lens_apply.rs` and `infer.rs` that resolve type arguments β€” reuse rather than re-implement. + +**If audit shows the eligibility predicate is fully derivable from existing structure**, the implementation lands as a helper function migration with NO substrate change. Surface that finding. + +**If audit shows an irreducible structural hole**, a minimal carrier may be justified β€” but the carrier must be JUSTIFIED INDEPENDENTLY (per `feedback_design_before_implement`), not added speculatively. + +## Slice (audit-conditional) + +Per audit findings: + +1. **Pure-query path (most likely):** + - Author `interpreter_eligible_fold(dag, instantiation)` (or worker-equivalent name) as a helper that resolves the accumulator + element type args structurally and matches against the bounded interpreter's supported set. Per `feedback_lenses_not_passes`: structural fact, zero heuristics. + - Replace `span.file.ends_with("std/algebra.dag")` at `lens_apply.rs:38` and `:372-383` with calls to the new structural helper. + - Regression test: a user-authored fold over an interpreter-eligible accumulator type (e.g., `Int`) outside `std/algebra.dag` runs through the bounded path; a user-authored fold over a `List`-style accumulator is correctly skipped via the structural predicate. + +2. **Carrier path (only if audit justifies):** + - Surface the audit finding that explains why a pure structural query doesn't work. + - Land minimal carrier; populate at lowering; same-PR consumer migration. + +Either way: **single PR; same-PR consumer migration**, per `feedback_parallel_representation_debt`. + +## Acceptance + +- [ ] Audit receipt recorded in PR body: `eval_std_fold`'s supported type set; existing structural helpers consulted; pure-query feasibility verdict. +- [ ] Β§0.4 sites at `lens_apply.rs:38, :372-383` removed; replaced with structural eligibility query. +- [ ] Regression test: structural-only fold dispatch (eligible fold runs through bounded path; ineligible fold correctly skips). +- [ ] **NO new substrate carrier** unless audit produces explicit justification + PR body documents the structural hole. +- [ ] DB-8 fixed-point converges bit-identically. +- [ ] No replacement sentinel string introduced (per `feedback_no_textual_enforcement_bridges`). +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note. + +## STOP-AND-ESCALATE + +- **Audit reveals the bounded interpreter's supported set is not structurally enumerable** (e.g., it dispatches via runtime hooks not visible at type-check time) β€” STOP. Surface to Substrate Manager; the Β§0.4 dissolution may need substrate-deeper work. +- **Pure-query path requires more than reading existing structural helpers** (e.g., needs lowering-time computation that doesn't compose) β€” STOP and surface the hole; carrier path may then be justified. +- **Audit reveals additional `span.file`-based dispatch in the lens evaluation chain** that wasn't named in #810's Β§0.4 β€” surface as separate Phase 2 site (route to B4 Phase 2 queue). +- **DB-8 drifts on a fold path that was previously routing through the file-suffix bridge** β€” surface; may indicate the bridge masked a real eligibility bug. Do NOT silently change semantics. +- **Worker concludes the bridge is structurally undissolvable** β€” STOP. The brief reframes as substrate-deeper work; cross-program escalation to Substrate Manager. + +## Non-goals + +- **NOT adding `fold_step_formal` carrier on `Instantiation`** (that was the misframing of the original brief β€” borderline parallel-rep with `find_fold_step_bind_via_instantiation`). +- **NOT extending `eval_std_fold`'s supported type set** in this lane (that's substrate-deeper work; out of scope). +- Not extending `std.list.fold` semantics or template parameters. +- Not touching B3's lens fold ambiguous fallback (already merged via #821). +- Not addressing other Β§0 sites (those are B4.1/B4.3/B4.4). + +## Cross-program note + +- **Producer:** Substrate Manager (T-Substrate / B4 Phase 1 #2) β€” but likely no new substrate; this lane may close as helper-migration-only. +- **Consumer:** lens-apply runtime β€” same-PR migration. +- **No cross-program consumer signal** β€” lens-apply only. + +## Pre-flight audit credit + +Original brief framing was caught by `royal-badger-32` at PR #834 pre-flight audit; #834 closed as misframed. This brief is re-authored against the correct dissolution target. The pre-flight audit discipline royal-badger-32 demonstrated (audit carrier shape against helper's own doc + actual call sites BEFORE propagating) is the right `feedback_design_before_implement` shape β€” saved as a feedback memory. + +## Reporting + +Single PR. Title: `feat(v3): B4.2 structural fold-eligibility β€” replace span.file.ends_with("std/algebra.dag") with structural type-arg query`. Body cites this brief + B4 program brief + audit receipt + decision (pure-query vs carrier path) + DB-8 disposition. + +On merge: signal Substrate Manager / Director; B4 Phase 1 carrier #2 of 4 closes (with note that #2 may have landed without new substrate, per audit). diff --git a/docs/briefs/b4-3-structural-emit-helper-carrier-worker.md b/docs/briefs/b4-3-structural-emit-helper-carrier-worker.md new file mode 100644 index 00000000000..2b72b4313fe --- /dev/null +++ b/docs/briefs/b4-3-structural-emit-helper-carrier-worker.md @@ -0,0 +1,90 @@ +# B4.3 β€” Structural emit-helper carrier `(M; B4 Phase 1 #3 of 4)` + +> **Worker brief.** Reports through Substrate Manager (post-R2 spin-up) / +> Director (pre-spin-up). Sub-brief of the +> [B4 Identity-Carrier Substrate Pass program](b4-identity-carrier-substrate-pass.md) +> (merged via #814). Replaces Β§0.6 β€” `bind.span.file == "named_alias_emit_helper.v3"` / +> `branch.span.file == "match_emit_helper.v3"` checks β€” with a typed role marker +> on `Bind` / `Branch` nodes, attached at lowering time. + +## Read first + +- **[`docs/briefs/b4-identity-carrier-substrate-pass.md`](b4-identity-carrier-substrate-pass.md)** β€” parent program brief. +- **[`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag)** β€” live substrate authority for `BindNode` / `BranchNode` shape. +- **[`src/v3/compiler/src/emit.rs:3181, :3206`](../../src/v3/compiler/src/emit.rs)** β€” the Β§0.6 cited sites. Note: line numbers per synthesis #810; verify against current `main` at PR-author time. +- **[`src/v3/compiler/src/emit.rs::primitive_type_id_for_port_shared`](../../src/v3/compiler/src/emit.rs)** + **[`src/v3/compiler/src/emit.rs::walk_to_disj`](../../src/v3/compiler/src/emit.rs)** β€” production functions that may consult the helper-role markers. +- **`feedback_audit_adjacent_authority_first`** β€” grep before designing. +- **`feedback_no_metadata_markers`** β€” no `__is_X` string markers; model concepts structurally. +- **`feedback_no_textual_enforcement_bridges`** β€” no replacement sentinel strings. +- **`feedback_coproduct_dissolution`** β€” receipt for any new variant. + +## Frame + +`emit.rs:3181, :3206` dispatches via `bind.span.file == "named_alias_emit_helper.v3"` / `branch.span.file == "match_emit_helper.v3"` β€” file-equality string check, not structural. The Β§0.6 site from the B4 program. Substrate gap: emit helpers (named-alias emission, match emission) need a typed role marker on the `Bind` / `Branch` node attached at lowering time, not inferred from `span.file`. + +The fix is a typed role enum field on `BindNode` / `BranchNode` β€” populated structurally by the lowering pass when it constructs the node for a helper role. Emission consumers ask "does this Bind/Branch carry a `UserCallable` / `UserMatch` role?" instead of "is the source file the magic helper file?". + +## Pre-author authority audit (mandatory) + +Before designing the new carrier, **grep `src/v3/std/` + `src/v3/spec/`** for any existing emit-role marker, lens-helper marker, or `EmitRole`-shaped carrier on `Bind`/`Branch` nodes. Search terms: + +- `EmitRole`, `EmitParticipation`, `BindRole`, `BranchRole` +- existing optional fields on `BindNode` / `BranchNode` declaration in `src/v3/std/substrate.dag` +- existing emit-helper authority in `src/v3/std/emit_model.dag` or sibling files + +**If audit reveals existing authority, reframe as consumer migration.** + +## Slice (assume audit shows substrate gap) + +1. **Land typed role enum carriers in `src/v3/std/substrate.dag`:** + - `type BranchEmitParticipation = UserMatch` (extensible coproduct; document expected future variants in coproduct receipt) + - `type BindEmitParticipation = UserCallable` (same) + - Add optional `emit_participation: BranchEmitParticipation?` field to `BranchNode` declaration. + - Add optional `emit_participation: BindEmitParticipation?` field to `BindNode` declaration. +2. **Mirror in Rust** (`src/v3/compiler/src/dag.rs`) β€” substrate.dag is canonical, Rust mirrors. Builder defaults to `None`. +3. **Lower the role markers** at every helper-role site: + - User `match` Branch nodes get `Some(UserMatch)` at lowering time, not refinement / Bool-`if` Branches. + - User `fn` / lambda Arrow body Bind nodes get `Some(UserCallable)`, not refinement-predicate / `let` / synthetic Binds. +4. **Replace the file-equality checks** at `emit.rs:3181, :3206` (and any sibling `span.file ==` checks for these helper roles) with structural queries against `bind.emit_participation == Some(UserCallable)` / `branch.emit_participation == Some(UserMatch)`. +5. **Audit `emit.rs::primitive_type_id_for_port_shared` + `walk_to_disj`** β€” confirm production code consumes the new markers correctly. If a sibling production site reaches for `span.file` for the same role, migrate it in this PR. +6. **Coproduct dissolution receipt** for the two new variants (`UserMatch`, `UserCallable`) per `feedback_coproduct_dissolution`. Receipt frame: "current taxonomy reflects the two production helper roles known at lower-time; open for extension when new helper roles arrive." +7. **Test migration** β€” rename test fixtures from magic strings (`named_alias_emit_helper.v3`, `match_emit_helper.v3`) to ordinary names; dispatch via the structural marker. Spoofing test: an ordinary fixture filename that matches the old magic string but lacks the role marker is NOT treated as a helper role. Existing tests in `emit.rs:3120+` `#[cfg(test)] mod tests` are precedent. + +## Acceptance + +- [ ] Β§0.6 `bind.span.file == "named_alias_emit_helper.v3"` and `branch.span.file == "match_emit_helper.v3"` sites in `emit.rs:3181, :3206` (and any siblings) removed. +- [ ] Substrate carriers `BranchEmitParticipation { UserMatch }` / `BindEmitParticipation { UserCallable }` land in `src/v3/std/substrate.dag` with Rust mirror parity. +- [ ] Lowering populates `Some(...)` at every user `match` / `fn` / lambda site; `None` for refinement / `let` / synthetic. +- [ ] Authority audit receipt recorded in PR body. +- [ ] Coproduct dissolution receipt for the two new variants. +- [ ] Test migration renames magic-filename fixtures and dispatches via structural marker. +- [ ] Spoofing regression test: ordinary fixture with magic-string filename does NOT receive helper-role treatment without the marker. +- [ ] Production consumer audit: confirm `primitive_type_id_for_port_shared` / `walk_to_disj` and any sibling site uses the structural marker, not `span.file`. +- [ ] DB-8 fixed-point converges bit-identically. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note in PR body. + +## STOP-AND-ESCALATE + +- **Audit reveals helper roles have additional structural dependencies** (e.g., `match_emit_helper` requires more than just role-tagging β€” needs context the lowering doesn't yet thread) β€” surface for substrate-scope call. +- **More than two helper roles surface during the production audit** β€” expand the coproduct or surface for design call (the receipt should remain honest). +- **DB-8 drifts** β€” STOP immediately. +- **A production consumer reaches for `span.file` for a role NOT cited in the synthesis** β€” surface; that's an undiscovered Β§0.X site. + +## Non-goals + +- Not extending the helper-role taxonomy beyond what production code currently dispatches on. +- Not replacing `span.file` checks for legitimate non-role purposes (e.g., diagnostic source-mapping). +- Not addressing other Β§0 sites (those are B4.1/B4.2/B4.4). + +## Cross-program note + +- **Producer:** Substrate Manager (T-Substrate / B4 Phase 1 #3). +- **Consumer:** emit.rs runtime β€” same-PR consumer migration. +- **No cross-program consumer signal** β€” emit-side only. + +## Reporting + +Single PR. Title: `feat(v3): B4.3 structural emit-helper carrier β€” replace span.file equality with typed BindEmitParticipation/BranchEmitParticipation roles`. Body cites this brief + B4 program brief + records the authority audit + coproduct receipt + production consumer audit findings. + +On merge: signal Substrate Manager / Director; B4 Phase 1 carrier #3 of 4 lands. diff --git a/docs/briefs/b4-4-structural-extdeps-fixture-set-carrier-worker.md b/docs/briefs/b4-4-structural-extdeps-fixture-set-carrier-worker.md new file mode 100644 index 00000000000..3fdcef69019 --- /dev/null +++ b/docs/briefs/b4-4-structural-extdeps-fixture-set-carrier-worker.md @@ -0,0 +1,80 @@ +# B4.4 β€” Structural extdeps-fixture-set carrier `(S/M; B4 Phase 1 #4 of 4)` + +> **Worker brief.** Reports through Substrate Manager (post-R2 spin-up) / +> Director (pre-spin-up). Sub-brief of the +> [B4 Identity-Carrier Substrate Pass program](b4-identity-carrier-substrate-pass.md) +> (merged via #814). Replaces Β§0.8 β€” `EXTDEPS_BOOTSTRAP_FIXTURES` hardcoded Rust list β€” +> with a typed declaration in `src/v3/std/`. + +## Read first + +- **[`docs/briefs/b4-identity-carrier-substrate-pass.md`](b4-identity-carrier-substrate-pass.md)** β€” parent program brief. +- **[`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag)** β€” live substrate authority. +- **[`src/v3/spec/v3_l1.dag:69`](../../src/v3/spec/v3_l1.dag)** β€” `DeclarationRef` (consumed by B4.1; likely shape for fixture entries). +- **[`src/v3/compiler/src/bootstrap.rs::std_fixtures`](../../src/v3/compiler/src/bootstrap.rs)** β€” production consumer that today reads `EXTDEPS_BOOTSTRAP_FIXTURES` constant. +- **[`src/v3/compiler/src/bootstrap_regen_fresh.rs`](../../src/v3/compiler/src/bootstrap_regen_fresh.rs)** β€” regen host; runs **before** the bootstrap Dag is loadable. Material constraint: the regen host can't read a substrate authority that requires a loaded Dag. This is the **pre-promotion constraint** worth surfacing explicitly. +- **`feedback_audit_adjacent_authority_first`** β€” grep before designing. +- **`feedback_parallel_representation_debt`** β€” DO NOT keep parallel Rust-const + substrate-authority unless the regen-host pre-promotion constraint genuinely forces it; surface as tracked debt with named ROADMAP dissolution trigger if so. +- **`feedback_construction_over_ratchets`** β€” parity-by-runtime-assertion is a ratchet, not dissolution; only acceptable if the dissolution trigger is named in ROADMAP. + +## Frame + +`bootstrap.rs::std_fixtures()` consumes a hardcoded Rust list `EXTDEPS_BOOTSTRAP_FIXTURES`. The Β§0.8 site. Substrate gap: the extdeps fixture set should be a typed declaration in `src/v3/std/` (or `src/v3/spec/`), not a Rust constant. + +## Pre-author authority audit (mandatory) + +Before designing the new carrier, **grep `src/v3/std/` + `src/v3/spec/`** for any existing fixture-set / bootstrap-set carrier. Search terms: + +- `BootstrapFixture`, `FixtureSet`, `bootstrap_fixture_authority`, `extdeps_bootstrap` +- existing typed fixture declarations consumed by bootstrap + +The fixtures have `DeclarationId`s once loaded β€” the question is whether a typed `List` (or equivalent) declaration already exists or needs to be authored. + +**If audit reveals existing authority, reframe as consumer migration.** + +## Slice (assume audit shows substrate gap) + +1. **Land typed `extdeps_bootstrap_fixture_authority` (or worker-equivalent) declaration in `src/v3/std/extdeps_bootstrap_fixtures.dag`** (or appended to existing `src/v3/std/substrate.dag` β€” worker picks; surface choice). Element shape: typed entries naming each fixture's virtual path (e.g., `virtual_path: String` per row), with the path resolving to a `DeclarationRef` post-load. Coproduct dissolution receipt if any new variant lands. +2. **Migrate `bootstrap.rs::std_fixtures()` to read from the typed declaration** instead of the hardcoded Rust list β€” at the latest possible point in the bootstrap sequence, so the substrate authority is loaded before its consumer fires. +3. **Pre-promotion constraint disposition.** Shape (a) is the only autonomous worker path; shape (b) is a cross-manager design escalation, NOT a worker call: + - **(a) Single authority (autonomous worker path)**: regen host reads the substrate authority directly via a minimal sub-loader that loads only the fixture-set declaration before the full bootstrap. **Worker authors this without further escalation if feasible.** + - **(b) Authority + tracked debt** β€” **NOT autonomous**: if the audit shows shape (a) is genuinely infeasible (e.g., circular dependency, build-time computation requirement), **STOP-AND-ESCALATE to Substrate Manager** for a regen-host-loader sub-lane decision. Per `feedback_construction_over_ratchets` + `feedback_parallel_representation_debt`, the parallel-Rust-const + substrate-authority shape is **only acceptable** with explicit Substrate Manager approval AND a named ROADMAP dissolution trigger. **Do not author shape (b) without that approval citation in the PR body.** +4. **Replace `EXTDEPS_BOOTSTRAP_FIXTURES` Rust constant** β€” delete (shape a) or narrow to regen-host-only (shape b, only if Substrate Manager approval citation present). Surface the disposition in PR body. +5. **Regression test:** bootstrap output is bit-identical (DB-8 must converge); SG-0 census deltas covered if any. + +## Acceptance + +- [ ] `EXTDEPS_BOOTSTRAP_FIXTURES` Rust constant deleted (shape a) **OR** narrowed to regen-host-only with **explicit Substrate Manager approval citation + named ROADMAP debt row** in PR body (shape b). +- [ ] Typed `extdeps_bootstrap_fixture_authority` (or equivalent) declaration lives in `src/v3/std/`. +- [ ] `bootstrap.rs::std_fixtures()` reads the typed authority. +- [ ] Authority audit receipt recorded in PR body. +- [ ] Pre-promotion constraint disposition recorded explicitly. Shape (a) is the autonomous default; shape (b) requires the Substrate Manager approval citation per Slice Β§3. +- [ ] DB-8 fixed-point converges bit-identically. +- [ ] SG-0 census deltas covered. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note. + +## STOP-AND-ESCALATE + +- **The fixtures are non-trivially ordered, conditional, or require build-time computation** that doesn't lower cleanly β€” surface for design call. +- **Shape (a) is genuinely infeasible** (circular dependency, build-time computation required, etc.) β€” STOP and escalate to Substrate Manager for a regen-host-loader sub-lane decision. **Do not author shape (b) without explicit Substrate Manager approval.** Per PM tightening on #836: shape (b) cannot be a worker autonomous-path call. +- **Shape (b) approved by Substrate Manager but ROADMAP debt row would need to track an indefinite dissolution** β€” re-escalate; permanent parallel-representation is not acceptable even with manager approval. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- Not redesigning the bootstrap sequence beyond what's needed for B4.4 disposition. +- Not migrating other Rust constants in `bootstrap.rs` (those are separate program work, possibly Pure Bootstrap Manager territory). +- Not addressing other Β§0 sites. + +## Cross-program note + +- **Producer:** Substrate Manager (T-Substrate / B4 Phase 1 #4). +- **Consumer:** bootstrap loader (same-PR migration). +- **Cross-program coordination:** if shape (b) lands a ROADMAP debt row for full dissolution, the long-term consumer is **Pure Bootstrap Manager** (post-promotion full-substrate-load lane). Heads-up to PB Manager at landing. + +## Reporting + +Single PR. Title: `feat(v3): B4.4 structural extdeps-fixture-set carrier β€” typed authority replaces EXTDEPS_BOOTSTRAP_FIXTURES Rust constant`. Body cites this brief + B4 program brief + records authority audit + pre-promotion-constraint disposition (a or b) + ROADMAP debt row reference if shape (b). + +On merge: signal Substrate Manager / Director; B4 Phase 1 carrier #4 of 4 lands. **All four Phase 1 carriers complete; Phase 2 mechanical site dissolutions become dispatchable.** diff --git a/docs/briefs/b4-phase-2-site-dissolution-queue.md b/docs/briefs/b4-phase-2-site-dissolution-queue.md new file mode 100644 index 00000000000..f921ee8af00 --- /dev/null +++ b/docs/briefs/b4-phase-2-site-dissolution-queue.md @@ -0,0 +1,81 @@ +# B4 Phase 2 β€” Site dissolution queue (skeletons, dispatch-as-Phase-1-lands) + +> **Tracking doc, not a worker brief.** Reports through Substrate Manager +> (post-R2 spin-up). Names the Phase 2 mechanical site-dissolution work +> deferred from the +> [B4 Identity-Carrier Substrate Pass program](b4-identity-carrier-substrate-pass.md) +> (merged via #814). +> +> Phase 2 dispatches **as each Phase 1 carrier lands**; site dissolutions +> are mechanical follow-up PRs once substrate is in place. Worker briefs +> are skeleton-only here; full content authored by Substrate Manager +> (or Director pre-spin-up) at dispatch time per the carrier readiness +> signal. + +## Phase 2 dispatch matrix + +The B4 program identified **8 surface dissolution sites** (Β§0.1 through Β§0.8). +Each Phase 1 carrier subsumes its primary consumer site in the same-PR +migration; Phase 2 covers **secondary consumers** of the same carrier +that didn't land in the carrier PR. + +| # | Β§0 site | File:line | Phase 1 carrier | Phase 2 dispatch trigger | +|---|---------|-----------|-----------------|--------------------------| +| B4.5 | Β§0.5 | `lower.rs:836` β€” `span.file == "dsl/std/types.dag"` type-alias bridge | B4.1 (`DeclarationRef` migration) | After B4.1 first-consumer (#823) merged + B4.1b residual (#826 + Slice 4-5) closes; this site is **not in B4.1's known scope**, dispatch as separate Phase 2 consumer-migration PR. | +| B4.6 | Β§0.7 | `dag.rs:2735-2764` + `lower.rs:1451-1452, 1546-1547` β€” `declaration_name_preference_rank(&span.file)` | B4.1 (`DeclarationRef` migration) | After B4.1 carrier landing fully covers DeclarationRef paths; this site cross-cuts file-preference logic and may share substrate territory with PB-Tier1-Sweep. **Cross-program coordination with Pure Bootstrap Manager.** | +| B4.7 | Β§0.4 secondary | `lens_apply.rs` siblings (if any) of `:38, :372-383` | B4.2 (fold-shape carrier) | After B4.2 lands; audit for any sibling fold-skip consultation of `span.file` not covered in B4.2's same-PR migration. | +| B4.8 | Β§0.6 secondary | `emit.rs` siblings (if any) of `:3181, :3206` | B4.3 (emit-helper carrier) | After B4.3 lands; production-consumer audit on `primitive_type_id_for_port_shared` / `walk_to_disj` / siblings. | +| B4.9 | Β§0.8 secondary | `bootstrap_regen_fresh.rs` regen-host filter | B4.4 (extdeps-fixture-set carrier) | If B4.4 lands shape (b) (authority + tracked debt), full dissolution of regen-host filter is a Phase 2 follow-up tracked via ROADMAP debt row. **Cross-program coordination with Pure Bootstrap Manager.** | +| B4.10 | (Phase 3) | n/a | n/a | **Phase 3 reviewer-discipline ratchet** (per program brief): no new `span.file ==` / `span.file.ends_with` / sentinel-string sites in `src/v3/compiler/src/`. Lands as PR-template-line addition + reviewer-discipline note. Authored by R2 Release Manager (per #827 dispatch-discipline framework enforcement). | +| B4.11 | reserved | n/a | n/a | Reserved for surfaces that emerge during Phase 1 audits (e.g., a fifth carrier surfaces during B4.2 / B4.3 / B4.4 work). | +| B4.12 | reserved | n/a | n/a | Reserved for downstream emit/lens consumers that surface during integration testing. | + +## Skeleton brief shape (each Phase 2 worker brief) + +When Substrate Manager dispatches a Phase 2 worker brief, the shape is: + +```markdown +# B4. β€” consumer migration `(S; B4 Phase 2)` + +> **Worker brief.** Reports through Substrate Manager. Phase 2 site +> dissolution following B4. merger. + +## Read first +- B4 program brief (`docs/briefs/b4-identity-carrier-substrate-pass.md`) +- Phase 1 carrier brief (`docs/briefs/b4--...-worker.md`) β€” merged +- Cited file:line site + +## Frame +The B4. carrier landed in ; this brief migrates the +secondary consumer at from `span.file ...` to structural query. + +## Slice +1. Replace `span.file == "..."` (or equivalent) with structural query against the carrier. +2. Regression test: site dispatches structurally without the file-name marker. +3. DB-8 fixed-point converges. + +## Acceptance +- Site cited in Β§0 dissolves via structural query. +- No replacement sentinel string introduced. +- Regression test added. +- DB-8 converges. +``` + +## Phase 2 cross-program coordination + +- **Pure Bootstrap Manager:** B4.6 (file-preference rank) and B4.9 (regen-host filter) cross-cut PB territory. Coordinate at dispatch time per #827's cross-program handoff pattern. +- **R2 Release Manager:** B4.10 Phase 3 reviewer-discipline ratchet is owned by Release Manager per the #810 dispatch-discipline framework. +- **Modeling Manager / Impossible-Bugs Manager:** no Phase 2 cross-program dependencies known at authoring time. + +## Status (at brief authoring, 2026-04-26) + +- B4.1 first-consumer landed (#823); residual via #826 (open, regen drift on `r1_gates.dag`); Slice 4-5 (full LensOutputEquals + DifferentialEquals migration) implied as B4.1b β€” not yet authored as separate worker brief. +- B4.2 brief authored (`b4-2-structural-fold-shape-carrier-worker.md`); no PR yet. +- B4.3 PR open (#824); CI failing; worker iterating. +- B4.4 PR open (#825); CI failing; worker iterating; flagged parallel-rep concern. + +## Reporting + +This is a tracking doc, not a single PR. Each Phase 2 worker brief lands +as its dispatch trigger fires (per the matrix above). Substrate Manager +maintains the matrix; Director (pre-spin-up) maintains via this file. diff --git a/docs/briefs/brief-authoring-checklist.md b/docs/briefs/brief-authoring-checklist.md new file mode 100644 index 00000000000..44882444633 --- /dev/null +++ b/docs/briefs/brief-authoring-checklist.md @@ -0,0 +1,103 @@ +# Brief-authoring authority-audit checklist + +> **Mandatory pre-author discipline** for any Director / manager +> brief that proposes substrate carriers, claims an existing +> design-doc recommendation, cites file:line authority, or scopes +> a consumer against a producer brief. Captures the discipline +> derived from #836's review cycle (8 substantive reframes, all +> from the same `feedback_audit_adjacent_authority_first` / +> `feedback_verify_thesis_claims` failure mode). + +## When to apply + +**Apply this checklist BEFORE drafting Slice / Acceptance / STOP-AND-ESCALATE for:** + +- Substrate-producer worker briefs (lands new substrate carrier). +- Consumer-migration worker briefs (consumes producer's signal). +- Implementation worker briefs that cite a design-doc recommendation. +- Per-class sub-lane briefs that depend on prior brief decisions. +- Any brief that includes file:line citations as authority. + +**Skip when:** the brief is a tracking doc, a status-only report, a closed-as-redundant routing doc (where the audit receipt itself IS the deliverable), or a fresh-from-scratch design proposal with no prior authority claims. + +## The five-question audit (mandatory) + +Before authoring any of the brief sections above, answer **all five** in writing. The answers go in the PR body that lands the brief; if they reveal the brief's premise is wrong, the brief reframes accordingly **before** authoring. + +### 1. Does the substrate this brief assumes exist already? + +**Grep:** +- `src/v3/std/` + `src/v3/spec/` for the proposed carrier shape (field names, type names, variants). +- `src/v3/compiler/src/dag.rs` and `infer.rs` for the proposed Rust mirror. + +**If found:** the brief is consumer-migration, not producer landing. Reframe before authoring Slice. Cite the existing authority's file:line. + +**Examples from #836's reframes:** +- Parametric-algebra-for-Dimensions: `Declaration.phantom_params` already at `dag.rs:186`; `phantom_unit_mismatch` already at `infer.rs:1057`. Closed as no-op. + +### 2. Does an existing brief already cover this scope? + +**Grep `docs/briefs/`** for similar scope (cardinality, fold, etc.). + +**If found:** route to existing brief; this one becomes a closed-as-redundant routing doc, not a second authority. Per `INVARIANTS.md` P2 (single authority). + +**Examples from #836:** +- cardinality-for-int-lit subset: `t-substrate-cardinality-int-lit-worker.md` already exists with re-scoped post-`wise-pike-578` decisions. Closed as redundant. + +### 3. Does the design-doc Β§Director-actionable recommendation match the brief's premise? + +**For any worker brief that consumes a design-doc:** read the design-doc's Β§Director-actionable / Β§Q-recommendation / Β§"Path forward" section **in full**. Do NOT assume the recommendation matches your initial framing. + +**If the recommendation differs:** reframe Slice + STOP-AND-ESCALATE to match. Surface the design-doc's specific reqs as numbered Slice items. + +**Examples from #836:** +- Nested-optional: design-doc verifies v3 substrate is past the cardinality bridge; recommendation is ungated constructor invariant, not gated implementation. Brief was reframed. +- Unhandled-diagnostic: design-doc Β§4 explicitly recommends totality-by-omission; predicate-entailment is M+ scope reopening DB-11. Brief was reframed. +- Unenumerated-effects: design-doc Β§Q6 enumerates 8 specific reqs; brief had elided 3. Brief was reframed. + +### 4. Are the file:line citations live at HEAD? + +**For every `file.rs:N` citation:** grep the file at HEAD; verify N still names the cited construct. + +**If line numbers drift:** update before authoring. Cite by symbol grep when feasible (e.g., search-anchor) instead of fragile line ranges. + +**Examples from #836:** +- `dag.rs:395-398` (Cardinality) β†’ `:408-411` (variant moved; Arrow now occupies prior range). +- `src/v3/std/types.dag` β†’ `dsl/std/types.dag` (5 briefs had wrong path). + +### 5. Does the carrier shape actually dissolve the cited bridge? + +**For substrate-producer briefs:** read the call-site code that consumes the bridge being dissolved. Confirm the proposed carrier answers the right question. + +**Specifically for span-suffix / file-equality bridges:** read the inline doc comment + the helper function the bridge gates. The bridge often skips on a different fact than the brief assumes. + +**Examples from #836:** +- B4.2 fold_step_formal: brief assumed bridge skips on step-formal binding. Worker pre-flight audit revealed bridge actually skips on accumulator/element type eligibility. Carrier addressed wrong question. Brief reframed. + +## Audit receipt format + +The PR body that lands the brief must include a short audit receipt: + +```markdown +## Authority audit receipt (brief-authoring-checklist.md compliance) + +1. **Substrate exists?** [grep result + answer] +2. **Existing brief?** [grep result + answer] +3. **Design-doc recommendation matches?** [Β§reference + verdict] +4. **Citations live?** [verified at sha XXX] +5. **Carrier dissolves the bridge?** [call-site + helper-doc cite + verdict] +``` + +If any answer reveals a mismatch, the brief reframes; the receipt records the reframe path. + +## Cross-references + +- `feedback_audit_adjacent_authority_first` β€” the parent discipline. +- `feedback_verify_thesis_claims` β€” the failure mode this checklist prevents. +- `feedback_design_before_implement` β€” pre-flight audit prevents propagation of contested shapes. +- `feedback_parallel_representation_debt` β€” what the audit prevents. +- `INVARIANTS.md` P2 (single authority) + P5 (paired dispatch). + +## Provenance + +This checklist captures the discipline lesson from #836's review cycle (8 substantive reframes across the R2 spin-up Wave 1-4 brief authoring), per openai-pro meta-verdict 2026-04-26 SHIP_WITH_DEBT recommendation. The 8 reframes β€” nested-optional gating, unhandled-diagnostic path-default, unenumerated-effects elision, parametric-algebra producer, cardinality-for-int-lit producer, nominal-opaque 7th-connective, int-lit consumer scope mismatch, B4.2 carrier-shape misdiagnosis β€” were all caught reactively by reviewers (7) or worker pre-flight (1). This checklist makes the discipline mechanical and pre-flight rather than reactive. diff --git a/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md b/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md new file mode 100644 index 00000000000..e59ed0eabc3 --- /dev/null +++ b/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md @@ -0,0 +1,95 @@ +# T-ImpossibleBugs β€” Nested-optional flatten implementation worker brief `(M; ungated β€” substrate-constructor invariant per design doc)` + +> **Worker brief.** Reports through Impossible-Bugs Manager (post-R2 +> spin-up) / Director (pre-spin-up). T-ImpossibleBugs Goal 4 class 1 +> of 3. +> +> **NOT GATED on substrate.** Per +> [`docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md`](t-impossiblebugs-nested-optional-flatten-design.md) +> Β§Q2: v3 substrate is past the cardinality bridge β€” +> `TypeConnective::Cardinality { element, bound }` is first-class +> (`src/v3/compiler/src/dag.rs:408-411`); `CardinalityBound::AtMostOne` +> is the carrier for `Option`. The dissolution is a substrate-constructor +> invariant, not new substrate work. Dispatch immediately. + +## Read first + +- **[`docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md`](t-impossiblebugs-nested-optional-flatten-design.md)** β€” design doc with full Q1-Q4 audit, construction-site enumeration, and canonical implementation sketch. **Read in full before slicing.** +- **[`THESIS.md` lines 342-344](../../THESIS.md)** β€” class definition. +- **[`src/v3/compiler/src/dag.rs:408-411`](../../src/v3/compiler/src/dag.rs)** β€” `TypeConnective::Cardinality { element, bound }` first-class. +- **[`src/v3/compiler/src/dag_scalar_generated.rs:21-25`](../../src/v3/compiler/src/dag_scalar_generated.rs)** β€” `CardinalityBound::AtMostOne` (the carrier for `Option`). +- **[`src/v3/compiler/src/lower.rs:1949-1968, :2044-2047`](../../src/v3/compiler/src/lower.rs)** β€” `SurfaceType::Optional` lowering arms (call sites). +- **[`src/v3/compiler/src/infer.rs:2902-2916`](../../src/v3/compiler/src/infer.rs)** β€” `concretize_decl_with_subst` (the **killer construction site** per design doc β€” substitution path that bypasses `lower.rs`). +- **[`docs/modeling-discipline.md`](../modeling-discipline.md)** practice 6 β€” API-level enforcement over convention. +- **`feedback_state_space_vs_behavioral_invariants`** β€” illegal states unrepresentable, not validated. + +## Frame + +Per design doc Β§Q3: the algebraic property is `AtMostOne ∧ AtMostOne = AtMostOne` β€” `Option>` is observationally equivalent to `Option` because `AtMostOne` cardinality is idempotent under self-composition. + +The implementation **closes the constructor API** so that `Cardinality { element: , bound: AtMostOne }` literally **cannot be constructed**. Per `feedback_state_space_vs_behavioral_invariants` + INVARIANTS.md P2: the dissolution is structural, not API-convention. + +**No new substrate.** The work is: +1. One predicate (`cardinality_idempotent_target`) that owns the rule. +2. One allocator (`alloc_cardinality_decl`) β€” the **single substrate-constructor authority**. +3. API closure on `TypeConnective::Cardinality`'s payload so the variant cannot be constructed via struct-init outside the allocator. +4. All call sites route through the allocator (3 hand-Rust + ~22 codegen sites per design doc audit). + +## Slice (per design doc Β§Q3 canonical sketch) + +1. **Author the predicate** `cardinality_idempotent_target(dag, element, bound) -> Option` in `src/v3/compiler/src/dag/builder.rs` (or adjacent). Returns `Some(inner_decl)` when the rule fires; else `None`. **Single rule authority.** +2. **Author the allocator** `alloc_cardinality_decl(dag, element, bound, span) -> DeclarationId`. If the rule fires, returns the inner decl; else allocates fresh `Cardinality { element, bound }`. +3. **Close the constructor API** β€” refactor `TypeConnective::Cardinality`'s payload so the variant cannot be struct-init'd outside `alloc_cardinality_decl`'s body. Per design doc canonical sketch + `docs/modeling-discipline.md` practice 6. +4. **Migrate the 3 hand-Rust call sites:** + - `lower.rs:1949` (`type_to_declaration_id` Optional arm) + - `lower.rs:2044` (`type_to_connective` Optional arm) + - `infer.rs:2902` (`concretize_decl_with_subst` β€” the killer case for generic instantiation) +5. **Migrate the codegen path** β€” `regen_bootstrap_emit.rs` emits `alloc_cardinality_decl` calls instead of literal `TypeConnective::Cardinality { ... }` struct-init in regen output. Affects ~22 sites in `bootstrap_std_generated.rs`. +6. **Regression tests:** + - `Option>` accessor patterns lower to `Option` accessor patterns (constructive β€” try to allocate the nested form, observe it returns the inner). + - `T??` source surface produces `Option` after lowering (not `Option>`). + - Generic instantiation: `fn foo(x: T?) -> T?` instantiated with `T = Int?` produces `Option`, not `Option>`. + - Spoofing test: a non-`AtMostOne` Cardinality (e.g., `Exact(2)`) is unaffected by the idempotent rule. +7. **DB-8 fixed-point bit-identical** β€” existing programs with `T?` continue to compile to identical DAGs; `T??` programs that previously produced nested-cardinality now produce flat (this is the dissolution; record the existence of any). +8. **Surface-syntax `T??` decision** β€” per design doc Β§Q1: tokenizer admits `?` `?` sequence at parse time. Decision: should the parser emit a diagnostic ("nested optional is structurally flattened β€” write `T?` directly") OR silently normalize? Worker picks; surface in PR. Director-lean: silent normalize (the dissolution makes it identical; user-facing diagnostic adds noise). + +## Acceptance + +- [ ] Predicate `cardinality_idempotent_target` authored as single rule authority. +- [ ] Allocator `alloc_cardinality_decl` is the single substrate-constructor authority for `Cardinality` declarations. +- [ ] `TypeConnective::Cardinality`'s payload mechanically closed so struct-init outside the allocator is impossible (per design doc + modeling-discipline practice 6). +- [ ] All 3 hand-Rust call sites migrated. +- [ ] Codegen path (`regen_bootstrap_emit.rs`) emits allocator calls; ~22 codegen sites covered. +- [ ] Regression tests: `T??` flatten / generic-instantiation / spoofing. +- [ ] DB-8 fixed-point bit-identical. +- [ ] Surface-syntax `T??` decision documented in PR body. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note. + +## STOP-AND-ESCALATE + +- **Audit reveals additional construction sites not enumerated in the design doc** β€” surface; the API closure may need extension. Don't migrate ad-hoc. +- **`TypeConnective::Cardinality`'s payload closure breaks more than the construction sites** β€” e.g., pattern-match destructuring elsewhere. Surface; may need a separate accessor pattern (read-side struct-match remains open; only write-side construction is closed). +- **Generic instantiation case (`infer.rs:2902`) reveals a deeper substitution pattern** that needs substrate work β€” surface; the design doc's Q4 may need extension. +- **DB-8 drifts on a program that wasn't expected to flatten** β€” surface; may indicate a legitimate distinction the dissolution shouldn't erase. +- **Codegen migration is too large for one PR** β€” surface; consider splitting hand-Rust + codegen as B4-style stacked PRs (substrate-constructor first, then codegen migration). + +## Non-goals + +- Not extending `OptionalOf` algebra-template semantics (per design doc Β§Q2 note: `OptionalOf` is a parallel construct in `algebra.dag`, not user-surface β€” out of scope). +- Not adding new substrate (v3 already has first-class Cardinality). +- Not authoring full DB-11 alias-`where` closure (adjacent, not subsumed). +- Not addressing other T-ImpossibleBugs classes. + +## Cross-program note + +- **No producer prerequisite** β€” substrate is past the cardinality bridge. +- **Producer:** this brief produces the constructor invariant. +- **Consumer:** existing v3 type-checker / lens consumers (no migration needed; they already walk Cardinality recursively, just stop seeing the nested form). +- **Downstream signal:** lane close β†’ Impossible-Bugs Manager β†’ R2 Release Manager (Goal 4 nested-optional class). + +## Reporting + +Single PR. Title: `feat(v3): T-ImpossibleBugs nested-optional flatten β€” substrate-constructor invariant for AtMostOne idempotence`. Body cites this brief + design doc + construction-site audit receipt + surface-syntax `T??` decision + DB-8 disposition. + +On merge: signal R2 Release Manager + close THESIS R2+ nested-optional bullet. diff --git a/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md b/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md new file mode 100644 index 00000000000..cba2fbd5f84 --- /dev/null +++ b/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md @@ -0,0 +1,93 @@ +# T-ImpossibleBugs β€” Unenumerated effects implementation worker brief `(M; closed-system structural derivation)` + +> **Worker brief.** Reports through Impossible-Bugs Manager (post-R2 +> spin-up) / Director (pre-spin-up). T-ImpossibleBugs Goal 4 class 3 +> of 3. +> +> **No substrate gate.** Per closed-system effects framing in +> [`docs/briefs/t-impossiblebugs-unenumerated-effects-design.md`](t-impossiblebugs-unenumerated-effects-design.md) +> (merged via #808), this is **dissolved by construction** β€” effects +> derive structurally from typed primitive composition; there is no +> annotation surface, no declared-vs-inferred lens, no parallel taxonomy. +> The implementation work is **audit-as-existence-check** + lens +> validation, not substrate carrier landing. + +## Read first + +- **[`docs/briefs/t-impossiblebugs-unenumerated-effects-design.md`](t-impossiblebugs-unenumerated-effects-design.md)** β€” design doc (merged #808). The 5-behavior compositional-fold mechanism + worked examples + Q5.5 OperationEffect retain-vs-retire framing. Read in full. +- **[`THESIS.md`](../../THESIS.md)** R2+ unenumerated-effects bullet β€” Tier 1 commitment ("dissolved by construction"); type-signature shape IS the effect. +- **Closed-system effects discipline** β€” 5-behavior compositional-fold table; the lens IS the same shape complexity/idempotency/termination lenses already use. The discipline is captured in the design doc (`t-impossiblebugs-unenumerated-effects-design.md`) Β§Q1-Q3; consult that as canonical authority. +- **[`src/v3/std/effects.dag`](../../src/v3/std/effects.dag)** β€” `OperationEffect` enum; live-state authority for the Q5.5 retain-vs-retire decision. +- **[`docs/briefs/t-impossiblebugs-effects-lens-implementation-audit.md`](t-impossiblebugs-effects-lens-implementation-audit.md)** (if authored per #810 SHIP_WITH_DEBT recommendation) β€” implementation/audit follow-up brief; if not authored, this brief subsumes its scope. + +## Frame + +Per design doc Q1-Q3: effects compose from the 5 behaviors (`Value | Transform | Branch | Loop | Bind`) the same way complexity, idempotency, termination do. A function is "effectful" iff its body composes operations with write-shaped type signatures (returns modified resource). + +Per Q5.5: the existing `OperationEffect` taxonomy (`Read | Upsert | Create | Append | Delete`) may be retired entirely (path ii β€” preferred default) or retained as a normalized derived view (path i). The audit decides: +- All effectful primitives in `dsl/std/` + `dsl/extdeps/` have type signatures that structurally derive the right effect classification β†’ **path (i)** retain as normalized view. +- At least one effectful primitive requires a hand-declared tag β†’ **path (ii)** retire (the existence-proof shows the taxonomy is parallel-representation). + +Per design doc default: retire (path ii). + +## Slice (per design doc Q6 β€” 8 reqs) + +1. **Effects lens at `src/v3/lenses/effect_enumeration.dag`** β€” parallel to `cost.dag`. Walks the 5-behavior structure (Value / Transform / Branch / Loop / Bind); **anchors on operation type-signature shape**, not on hand-declared OperationEffect tags; composes effect classification per the design doc Q2 table; surfaces structural-fact output (no annotation comparison, no parallel-taxonomy lookup). +2. **Audit-as-existence-check** β€” verify every effectful primitive in `dsl/std/` + `dsl/extdeps/` has a type signature that structurally derives the right effect classification (returned-modified-resource β†’ write-shaped; returns-derived-value-only β†’ read-shaped). **NOT "tag every primitive."** Per design doc Q5.5: any primitive requiring a hand-declared `OperationEffect` tag because its signature doesn't structurally reveal the effect IS the existence-proof for path (ii) β€” taxonomy retirement. +3. **Resource-threading discipline applied to existing primitives** β€” primitives that violate the discipline today (e.g., logging that returns Unit instead of `log.info(msg, log: LogFile) β†’ LogFile'`) get reshaped per the audit's findings. Foundation step toward signature-shape coverage. +4. **Redundancy lens** β€” referential-transparency proof for repeated identical reads with no intervening write. Emits compile-time `RedundantReadError` (Tier 1, not Tier 3). Per design doc Director's aggressive reading. +5. **`reread(key)` primitive in std/** β€” for legitimate re-read cases. Structurally tagged. Single authority for re-read intent (per design doc + #808 closing comment: extend `reread` rather than adding parallel primitives if cache-invalidation / transactional-refresh ever need similar affordance). +6. **Transactional-pattern lens** β€” derived structural fact from Bind composition + typed transaction primitives (`Transaction β†’ Transaction'`). The lens walks the Bind chain and recognizes the begin-modify-commit shape. +7. **Asymmetric-tightening worked example** in PR body β€” concrete demonstration that caller-side constraint via structural type matching rejects a callee whose body composes write-shaped operations beyond the caller's pinned set. Per design doc + claude review observation: the one place declaration-shaped surface re-enters deserves a worked example. +8. **Smoke + integration tests:** + - Function with multiple typed-effect operations produces correct effect-set structural fact (derived from signature shape, not from tag lookup). + - Function with redundant read of same key without intervening write β†’ compile error. + - Function with `reread()` on the same key β†’ compiles cleanly (legitimate re-read structurally tagged). + - Transactional-pattern function compiles + lens recognizes begin-modify-commit shape. + - Caller pinning effect-set βŠ† {read-shaped} rejects callee composing write-shaped operations. + +**Path (i) vs (ii) decision** β€” falls out of Slice Β§2 audit; surface receipt in PR body. **Default per design doc: path (ii) retire.** If audit produces existence-proof for path (i) (every primitive's signature derives cleanly), surface for Director re-decision per design doc Q5.5 STOP. + +## Acceptance + +- [ ] Effects lens at `src/v3/lenses/effect_enumeration.dag` (req 1); lens output observable via standard lens-output infrastructure. +- [ ] Audit-as-existence-check (req 2) completed; receipt recorded in PR body (which primitives audited; path (i) or (ii) verdict with structural justification). +- [ ] Resource-threading discipline (req 3) applied to existing primitives where audit found violations. +- [ ] Redundancy lens (req 4) emits compile-time `RedundantReadError` for same-key re-read without intervening write. +- [ ] `reread(key)` primitive (req 5) authored in std/. +- [ ] Transactional-pattern lens (req 6) recognizes begin-modify-commit shape via Bind composition. +- [ ] Asymmetric-tightening worked example (req 7) in PR body. +- [ ] Smoke + integration tests (req 8) cover read / write / redundancy compile-error / `reread()` / transactional / asymmetric-tightening rejection. +- [ ] Lens reports structural-coverage-gap diagnostics on Q4.5 P1 bypass surfaces (gap becomes visible, not silent). +- [ ] DB-8 fixed-point converges bit-identically. +- [ ] Cross-program signal: Impossible-Bugs Manager β†’ R2 Release Manager (Goal 4 unenumerated-effects class). +- [ ] `cargo test` / clippy / fmt clean. + +## STOP-AND-ESCALATE (per design doc Q6 STOPs) + +- **OperationEffect retirement decision (path (i) vs (ii))** β€” if Slice Β§2 audit produces the existence-proof for path (ii) (any primitive whose signature doesn't structurally reveal its effect after resource-threading migration), STOP and surface retirement scope to Director. Substrate retirement (`OperationEffect` enum + `derive_op_effect` + `idempotency.dag` re-anchor) is its own dedicated sub-lane; this lane should not absorb it. If audit confirms path (i) (all primitives derive cleanly from signature shape), surface that finding for re-decision. +- **Redundancy proof needs a `pure: Bool` carrier** β€” if the lens can't distinguish pure from impure Transforms inline, STOP. May need a sibling carrier on Transform targets. (Note: the deeper closed-system framing is that "pure" should also be derivable from signature shape β€” pure functions don't return modified resources β€” so this STOP may itself dissolve under further design.) +- **Asymmetric-tightening structural gap** β€” if caller can't actually pin effect-set constraints structurally today (i.e., the type system doesn't yet express "I require callee body's signature-shape composition βŠ† {read-shaped}"), STOP β€” that's its own substrate sub-lane. +- **Q4.5 P1 (extdeps typed-primitive bypass) β€” surfaced via lens findings**: lens reports structural-coverage-gap on `dsl/extdeps/llm/openai.dag:92-110`, `anthropic.dag:104-124`, `github/auth.dag:13-24` (and any others the audit finds). **NOT a STOP**; this is the lens delivering its closed-system-foundation-gap-visibility value. Director routes P1 closure to a dedicated extdeps-typed-primitive-consumption lane. Surface findings in PR body. +- **`reread()` ergonomics surface real legitimate-re-read patterns it doesn't cover cleanly** β€” per #808 closing comment, extend the primitive (or add a structurally-tagged sibling) rather than soften the compile-error stance. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- Not extending the 5-behavior set (substrate territory; out of scope for this lens). +- Not authoring `OperationEffect` extensions (path ii retires; path i keeps as derived view, no extensions). +- Not addressing other T-ImpossibleBugs classes. +- Not extending lens infrastructure beyond what this lens needs. + +## Cross-program note + +- **No substrate prerequisite** β€” the closed-system framing is the substrate (already landed via 5-behavior Behavior enum + typed substrate carriers). +- **Producer:** this brief produces the lens. +- **Consumer:** R2 Release Manager (Goal 4 close); future tooling that wants to query effect composition. +- **Adjacent:** Substrate Manager (B4 Identity-Carrier work) β€” Substrate's resource-threading discipline (e.g., `LogFile` carriers) may need landing if path (ii) audit surfaces it. Cross-program coordination at audit time. + +## Reporting + +Single PR. Title: `feat(v3): T-ImpossibleBugs unenumerated effects β€” closed-system lens + audit-as-existence-check + redundancy fail-closed`. Body cites this brief + design doc (#808) + audit receipt + path (i/ii) decision + DB-8 disposition. + +On merge: signal R2 Release Manager + close THESIS R2+ unenumerated-effects bullet. diff --git a/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md b/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md new file mode 100644 index 00000000000..40d5ed26021 --- /dev/null +++ b/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md @@ -0,0 +1,102 @@ +# T-ImpossibleBugs β€” Unhandled diagnostic paths via totality-by-omission `(M; per design doc Director-recommendation)` + +> **Worker brief.** Reports through Impossible-Bugs Manager (post-R2 +> spin-up) / Director (pre-spin-up). T-ImpossibleBugs Goal 4 class 2 +> of 3. +> +> **Path: totality-by-omission per partial-op class** β€” the +> Director-actionable recommendation in +> [`docs/briefs/t-impossiblebugs-unhandled-diagnostic-paths-design.md`](t-impossiblebugs-unhandled-diagnostic-paths-design.md) +> Β§4. NOT predicate-entailment substrate (that's M+, reopens DB-11 +> explicitly-closed design). The work is per-class algebra retype + +> per-target realization migration, not new substrate. + +## Read first + +- **[`docs/briefs/t-impossiblebugs-unhandled-diagnostic-paths-design.md`](t-impossiblebugs-unhandled-diagnostic-paths-design.md)** β€” design doc; **read Β§4 Director-actionable recommendation in full** before slicing. Key facts: + - gunbc already uses totality-by-omission for `force_unwrap` β€” convention precedent. + - Predicate-entailment (the "section 2" substrate path) is M+ scope and reopens DB-11's explicitly-closed asymmetric-strip design. **Not the recommended path.** + - For `/` specifically: closure cost has dropped since original framing β€” `OrderedRing.div: fn(T, T) -> T` at `dsl/std/algebra.dag:182` is consumed via algebra-Conj dispatch (`infer.rs:3975-3977`); closure is **algebra retype + per-target realization migration**. +- **[`THESIS.md` lines 175, 348-350, 391](../../THESIS.md)** β€” class definition + the "made total" branch the design doc closes against. +- **[`dsl/std/algebra.dag:182`](../../dsl/std/algebra.dag)** β€” `OrderedRing.div: fn(T, T) -> T` (the line to retype to total form). +- **[`src/v3/compiler/src/infer.rs:3975-3977`](../../src/v3/compiler/src/infer.rs)** β€” algebra-Conj dispatch site for `Int / Int`. +- **[`src/v3/spec/rust.dag:816`](../../src/v3/spec/rust.dag)** β€” `rust_int_div` realization (renders bare `{lhs} / {rhs}`). +- **[`src/v3/spec/go.dag:742`](../../src/v3/spec/go.dag)** β€” `go_int_div` realization (same shape). +- **[`src/v3/spec/python.dag:486`](../../src/v3/spec/python.dag)** β€” `python_int_div` realization (renders via `__v3_idiv` helper at `python_target.rs:680`; pinned by `m1_4_emit_python_test.rs:108-109`). +- **[`dsl/std/algebra.dag:477-478`](../../dsl/std/algebra.dag)** β€” `OrderedRing.quotient` / `OrderedRing.remainder` (separate per-class sub-lane candidates per design doc audit). +- **`feedback_totality_by_omission`** β€” discipline anchor: partial-op classes close by removing the partial form; coexistence-with-paired-total is the trap. + +## Frame + +Per design doc Β§4: the bug class closes by **removing the partial form**. For `/`, this means changing `OrderedRing.div`'s return type from `T` to a typed-split `Result` carrier where `DivError = DivideByZero | Overflow` preserves the two distinct failure modes (per Slice Β§2 below). All per-target realizations migrate to construct the typed-split return shape idiomatically. + +**Why not pair total + partial?** Coexistence is the **theatre trap** the design doc warns against. Adding `divide_safe` as a separate function alongside an unchanged `div: fn(T,T) -> T` leaves the partial form reachable; closure requires removal. + +**Why not predicate-entailment substrate?** Per design doc: M+ scope, reopens DB-11's asymmetric-strip design. Discarded. + +**Why not park?** The closure is now small (algebra retype + 3 realizations) and satisfies `feedback_totality_by_omission` directly. + +## Slice (per design doc Β§4 follow-on brief shape) + +1. **Audit** every partial operator/function currently reachable from user code: + - `Int / Int` β€” primary target (this PR). + - `[i]` indexing β€” separate sub-lane row. + - `force_unwrap` β€” already total; verify and confirm no regression. + - `OrderedRing.quotient` / `OrderedRing.remainder` at `dsl/std/algebra.dag:477-478` β€” separate sub-lane rows. **Verify user-reachability** distinct from `/`; if so, queue separately. + - Any other partial form per audit. Output: one-row-per-partial-form table in PR body. +2. **Per-row decision** β€” for `Int / Int`: pick Result-shape `Result` where `DivError = DivideByZero | Overflow` (or worker-equivalent typed split that preserves distinct failure modes). **NOT a single-error `Result`** β€” signed integer division has two structurally distinct failure modes (zero divisor + signed overflow on `MIN / -1`), and collapsing them violates fail-closed C-8 (per `feedback_fail_closed_discipline`: each detectable problem is its own typed Diagnostic). **Option-shape (`Option`) also rejected** for the same reason β€” `None` carries no failure-mode information. **STOP-AND-ESCALATE for NonZero-typed-input shape** (e.g., `a / nz` rather than `divide_nz(a, nz)`) β€” that's a per-operand type-variance question deferred to a separate substrate brief. +3. **Algebra retype**: one-line change at `algebra.dag:182` to the total return type. **The total return type carries a typed-split error carrier** (e.g., `DivError`) per Slice Β§2 β€” surface the carrier declaration's location (likely `dsl/std/errors.dag` or a sibling under `dsl/std/algebra.dag`). +4. **Per-target realization migration** β€” each target reshapes from bare division to construct the typed-split Result idiomatically; **must distinguish divide-by-zero from overflow** (do NOT collapse to a single error variant): + - `rust.dag:816` β€” `rust_int_div` reshapes to explicit branching: `if rhs == 0 { Err(DivError::DivideByZero) } else if /* overflow check */ { Err(DivError::Overflow) } else { Ok(lhs / rhs) }`. Note: `i64::checked_div` collapses both failures to `None`, so it's NOT a one-line `ok_or` β€” the realization must split the cases. Worker authors the exact Rust idiom; surface in PR. + - `go.dag:742` β€” `go_int_div` reshapes to Go-idiomatic typed-split Result; same case-split discipline. + - `python.dag:486` + `python_target.rs:680` helper β€” reshape `__v3_idiv` to return typed-split Result; update test pin at `m1_4_emit_python_test.rs:108-109`. (Python's overflow semantics differ from Rust's β€” surface the per-target equivalence in PR body.) +5. **Audit fallback path** β€” `infer.rs:4003-4015` Rust-side primitive scaffold (general fallback for types whose `inhabits` chain doesn't reach an algebra Conj). Slice Β§1 audit confirms whether any types still resolve `Arithmetic(Div)` through that fallback; close those paths separately if so. +6. **Regression tests:** + - `Int / Int` returns `Result` with both `DivideByZero` and `Overflow` variants reachable. + - **Distinct typed-split coverage:** `1 / 0` produces `Err(DivideByZero)`; `i64::MIN / -1` produces `Err(Overflow)`. Each failure mode tests independently β€” collapsing them is a discipline violation per `feedback_fail_closed_discipline` C-8. + - `let result = a / b; match result { Ok(v) => ..., Err(DivError::DivideByZero) => ..., Err(DivError::Overflow) => ... }` compiles (full match coverage). + - Existing safe `/` code migrated. + - Spoofing test: any other partial form (per Slice Β§1 audit) does NOT accidentally inherit the new total shape. +7. **DB-8 fixed-point bit-identical** for emit output post-realization-migration. + +## Acceptance + +- [ ] Audit table in PR body enumerating all partial forms reachable from user code. +- [ ] For `Int / Int`: algebra retype to total return; 3 per-target realizations migrated; test pin updated. +- [ ] Typed-split error carrier shape (e.g., `DivError = DivideByZero | Overflow`) recorded with placement (declaration location) and per-target realization rationale. NonZero-typed-input was a STOP, not a worker autonomous path. +- [ ] Fallback path (`infer.rs:4003-4015`) audited; any open paths closed or queued. +- [ ] Regression tests cover positive (`/` returns total) + spoofing + existing-program migration. +- [ ] DB-8 fixed-point bit-identical. +- [ ] Cross-program signal: lane close β†’ Impossible-Bugs Manager β†’ R2 Release Manager. **Note:** this PR closes only `Int / Int`; `[i]` indexing, `quotient`/`remainder`, etc. are sibling per-class sub-lanes. Surface remaining sub-lanes in PR body for follow-up dispatch. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note. + +## STOP-AND-ESCALATE + +- **NonZero-typed-input shape chosen** (`a / nz` operator-syntax rather than `divide_nz(a, nz)` function syntax) β€” STOP. Per-operand type variance in algebra-operator carrier is a separate substrate brief. +- **Audit reveals additional partial forms not enumerated in design doc** β€” surface; queue as sibling sub-lanes; do not subsume in this PR. +- **Realization migration breaks emission for an existing target idiom** β€” surface; this is a target-realization design call, not a worker call. +- **`Result` requires authoring `DivideByZero` declaration** β€” verify it doesn't exist via audit; if not, surface placement decision (`std.errors.dag`?). +- **Asymmetric-operator interaction** β€” if the totality migration affects symmetric operators (`>`, `<`, etc.) that DB-11 explicitly strips refinements from, surface β€” the design doc treats those as separate; this PR shouldn't broaden. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- **Not predicate-entailment substrate.** Per design doc, M+ scope, reopens DB-11. Worker DOES NOT author predicate-entailment paths. +- Not authoring all sibling sub-lanes (indexing, quotient, remainder) in one PR β€” per-class sub-lanes per design doc Β§4. +- Not extending refinement-checking β€” orthogonal to this brief. +- Not addressing other T-ImpossibleBugs classes. + +## Cross-program note + +- **No producer prerequisite** β€” totality-by-omission needs no new substrate. +- **Producer:** this brief. +- **Consumer:** existing v3 type-checker / per-target emitters. +- **Downstream signal:** R2 Release Manager (Goal 4 partial close β€” `Int / Int` only; sibling sub-lanes queued separately). +- **Adjacent:** Modeling Manager β€” `Result` shape if not yet first-class in std/. Audit-time check. + +## Reporting + +Single PR, narrow scope (`Int / Int` totalization). Title: `feat(v3): T-ImpossibleBugs unhandled diagnostic paths β€” Int/Int totality via OrderedRing.div algebra retype + per-target realization migration`. Body cites this brief + design doc Β§4 + audit table + algebra retype + 3 realization migrations + DB-8 disposition. + +On merge: signal R2 Release Manager (partial Goal 4 close); surface remaining per-class sub-lanes for follow-up dispatch. diff --git a/docs/briefs/r2-modeling-dimensions-phantom-worker.md b/docs/briefs/r2-modeling-dimensions-phantom-worker.md new file mode 100644 index 00000000000..bc5f481eb01 --- /dev/null +++ b/docs/briefs/r2-modeling-dimensions-phantom-worker.md @@ -0,0 +1,81 @@ +# T-Modeling β€” `Dimension` phantom-parameter worker brief `(M; substrate already in place β€” dispatchable immediately)` + +> **Worker brief.** Reports through Modeling Manager (post-R2 spin-up) / +> Director (pre-spin-up). T-Modeling Goal 2 item. +> +> **NOT GATED.** Per +> [`r2-substrate-parametric-algebra-for-dimensions-subset.md`](r2-substrate-parametric-algebra-for-dimensions-subset.md)'s +> audit: `Declaration.phantom_params` and `PhantomParameter` already +> exist in `dag.rs:186, :217`; `phantom_unit_mismatch` already wired +> in `infer.rs:1057, :1132`. The producer lane is closed. +> **Dispatch immediately.** + +## Read first + +- **[`r2-substrate-parametric-algebra-for-dimensions-subset.md`](r2-substrate-parametric-algebra-for-dimensions-subset.md)** β€” producer brief (closed; documents the audit receipt confirming substrate is already in place). +- **[`src/v3/compiler/src/dag.rs:186, :217-220`](../../src/v3/compiler/src/dag.rs)** β€” `Declaration.phantom_params` + `PhantomParameter { parameter, algebra }` carrier shape. +- **[`src/v3/compiler/src/dag.rs:148-160`](../../src/v3/compiler/src/dag.rs)** β€” doc comment: *"The initial R2 Dimensions consumer needs only abelian-group closure, carried as a typed edge to the substrate algebra declaration."* The carrier was authored explicitly for this brief. +- **[`src/v3/compiler/src/infer.rs:1057, :1132`](../../src/v3/compiler/src/infer.rs)** β€” `phantom_unit_mismatch` (already-wired type-equivalence + unit-mismatch dispatch). +- **[`src/v3/compiler/src/dag.rs:1941`](../../src/v3/compiler/src/dag.rs)** β€” `AbelianGroup` algebra Conj cited as canonical authority for phantom-unit closure. +- **[`THESIS.md`](../../THESIS.md)** Β§"Enumerable impossible-bug classes" β€” unit-mismatch impossibility as Tier 1 thesis claim. +- **[`dsl/std/types.dag`](../../dsl/std/types.dag)** + **[`src/v3/std/algebra.dag`](../../src/v3/std/algebra.dag)** β€” algebra-attachment patterns; `AbelianGroup` for additive unit groups. +- **`feedback_state_space_vs_behavioral_invariants`** β€” unit-mismatch unrepresentable, not validated. + +## Frame + +The phantom-parameter substrate is already in place (`Declaration.phantom_params` + `PhantomParameter { parameter, algebra }` + `phantom_unit_mismatch` dispatch). This brief authors `Dimension` itself β€” a typed wrapper that **consumes** the existing substrate. Two `Dimension` and `Dimension` are structurally distinct types via the substrate's parameter+algebra equality; arithmetic that would mix them is a type error at compile time via `phantom_unit_mismatch`. + +After this lane closes, common dimension types (Meters, Seconds, Kilograms, Amperes β€” the SI base units, plus a small set of derived units) are declared in `src/v3/std/dimensions.dag` (or equivalent); user code mixing units produces typed diagnostics. + +## Slice + +1. **Verify substrate at HEAD.** Confirm `Declaration.phantom_params` and `phantom_unit_mismatch` are still present and shape-stable (per the closed producer brief audit). Surface drift if anything has changed. +2. **Author `Dimension` declaration** consuming the phantom-parameter carrier per producer brief's contract. +3. **Author core unit declarations** (worker picks scope; surface in PR): + - SI base units: `Meters`, `Seconds`, `Kilograms`, `Amperes`, `Kelvin`, `Moles`, `Candela`. + - Common derived: `Newtons` (kgΒ·m/sΒ²), `Joules`, `Hertz`. Possibly defer derived to a follow-up. +4. **Algebra-method dispatch** per producer brief's design choice. Add: `add`, `sub`, `mul_scalar`, `div_scalar` over same-dimension `Dimension`. Cross-dimension operations are typed errors. +5. **Diagnostic for unit-mismatch.** Add `meters + seconds` produces typed diagnostic. Per C-8. +6. **Regression tests:** + - `meters + meters` produces `meters` (same dimension). + - `meters + seconds` produces typed diagnostic at compile time. + - `meters * scalar(2.0)` produces `meters` (scalar lifts cleanly). + - Spoofing test: a non-Dimension wrapper with similar shape doesn't accidentally enforce unit-mismatch. +7. **DB-8 fixed-point bit-identical.** + +## Acceptance + +- [ ] `Dimension` declared in `src/v3/std/`; consumes producer's phantom-parameter carrier. +- [ ] Core SI base units declared (worker picks scope; surface). +- [ ] Algebra-method dispatch per producer brief's design. +- [ ] Unit-mismatch diagnostic per C-8. +- [ ] Regression tests cover positive + negative + scalar-lift + spoofing. +- [ ] DB-8 converges bit-identically. +- [ ] Cross-program signal: R2 Release Manager (Goal 2 Dimensions item) + Impossible-Bugs Manager (thesis claim). +- [ ] `cargo test` / clippy / fmt clean. + +## STOP-AND-ESCALATE + +- **Existing `phantom_params` carrier doesn't admit a needed pattern** (e.g., per-method algebra-dispatch shape, or higher-kinded extension). Surface; this is a substrate-extension call to Substrate Manager, NOT autonomous worker scope. Per `feedback_audit_adjacent_authority_first`, do not silently extend the carrier. +- **Algebra-method dispatch path requires runtime dispatch.** Per producer brief's STOP, surface β€” discipline call about static-vs-dynamic algebra dispatch. +- **Derived units (Newtons = kgΒ·m/sΒ²) require type-level computation** (multiplication of phantom parameters). If the producer's substrate doesn't support this, derived units defer to a follow-up; surface. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- Not authoring complete SI / Imperial unit system β€” minimal core + extensible. +- Not authoring conversion functions (Meters β†’ Feet) in this brief β€” those are user-space follow-ups. +- Not authoring the substrate carrier (producer's job). +- Not extending `Dimension` to higher-kinded patterns. + +## Cross-program note + +- **Producer:** Substrate Manager β†’ parametric-algebra-for-Dimensions. +- **Consumer:** this brief. +- **Downstream signals:** R2 Release Manager (Goal 2 close); Impossible-Bugs Manager (thesis claim). + +## Reporting + +Single PR. Title: `feat(v3): T-Modeling Dimension phantom-parameter β€” typed wrapper + core SI units consuming parametric-algebra substrate`. Body cites this brief + producer brief + signal-receipt + DB-8 disposition + scope of authored units. + +On merge: signal R2 Release Manager + Impossible-Bugs Manager. diff --git a/docs/briefs/r2-modeling-int-lit-magnitude-worker.md b/docs/briefs/r2-modeling-int-lit-magnitude-worker.md new file mode 100644 index 00000000000..2db33f06fab --- /dev/null +++ b/docs/briefs/r2-modeling-int-lit-magnitude-worker.md @@ -0,0 +1,85 @@ +# T-Modeling β€” Int-literal magnitude worker brief `(M; consumer of t-substrate-cardinality-int-lit-worker.md range-facts-only scope)` + +> **Worker brief.** Reports through Modeling Manager (post-R2 spin-up) / +> Director (pre-spin-up). T-Modeling Goal 2 item per +> [`docs/r2-structure.md`](../r2-structure.md). +> +> **Gated on:** Substrate Manager readiness signal for +> [`t-substrate-cardinality-int-lit-worker.md`](t-substrate-cardinality-int-lit-worker.md). +> **Do not dispatch until that signal posts.** +> +> **Scope reconciled with producer (post-`wise-pike-578` re-scope):** +> producer KEEPS `LiteralBits::Int(i64)` substrate-side; ranges are +> String-decimal facts; `i64::MIN`-as-single-token deferred to a +> sibling Int128/Word128 sub-lane. **This consumer brief operates +> against the i64-bounded carrier per producer's re-scope** β€” it does +> NOT widen IntLit, does NOT close `i64::MIN` representability, and +> does NOT ship anything the producer's deferred sibling sub-lane has +> not yet landed. + +## Read first + +- **[`docs/briefs/t-substrate-cardinality-int-lit-worker.md`](t-substrate-cardinality-int-lit-worker.md)** β€” **canonical producer brief** (post-`wise-pike-578` re-scoped). Read in full; this consumer brief consumes ONLY what producer landed: range-facts (String-decimal) + reconciliation narrowing + `MagnitudeOutOfRange` diagnostic, all against existing `LiteralBits::Int(i64)`. +- **[`docs/briefs/r2-substrate-cardinality-for-int-lit-subset.md`](r2-substrate-cardinality-for-int-lit-subset.md)** β€” closed-as-redundant routing doc; the producer authority is the `t-substrate-cardinality-int-lit-worker.md` brief above. +- **[`ROADMAP.md` Β§"Surface int-literals are concept-layer host-narrowed"](../../ROADMAP.md)** (`:355`) β€” the gap statement; the i64-bounded scope of this lane is the partial closure. +- **[`src/v3/std/tokenize.dag:30`](../../src/v3/std/tokenize.dag)** β€” `IntLit(Int)` declaration; **stays as-is** per producer's re-scope. +- **[PR #806](https://github.com/gunb-ai/gunbc/pull/806)** β€” t-substrate cardinality int (merged); confirm what landed and what's still consumer-side work. +- **[`THESIS.md`](../../THESIS.md)** β€” int-literal magnitude as Tier 1 thesis claim (note: full Tier 1 closure including `i64::MIN`-as-single-token requires the sibling Int128/Word128 sub-lane; this lane partial-closes). + +## Frame + +Producer landed: range facts (String-decimal `range_min_inclusive` / `range_max_inclusive` per integer algebra) + reconciliation magnitude-aware narrowing at `infer.rs:704-725` + `MagnitudeOutOfRange` typed diagnostic, **all against the existing `LiteralBits::Int(i64)` carrier**. Carrier widening (Int128/UInt128/Word128Carrier) is deferred to a sibling sub-lane. + +This consumer brief migrates downstream consumers (call sites that emit, query, or pattern-match on int-literal magnitude) to consume the new substrate facts where appropriate. **It does NOT widen `LiteralBits::Int`**; the i64-bounded carrier is producer's authority. + +## Slice (post-re-scope; range-facts consumption only) + +1. **Confirm Substrate readiness signal** from producer brief's PR. Read producer's PR body to confirm: range-facts shape (String-decimal), narrowing site (infer.rs:704-725), `MagnitudeOutOfRange` diagnostic placement. +2. **Audit downstream consumers** of int-literal magnitude β€” emitters, lens evaluators, codegen sites that do magnitude-based dispatch. Output: one-row-per-consumer table noting whether it consumes the new range-facts via the producer's narrowing or whether it operates downstream of narrowing without further consumption. +3. **Migrate consumers** that benefit from the new facts: + - Per-target emitter realizations that pick narrower target types based on literal magnitude (e.g., `let x: u8 = 5` should now reach Word8 idiomatically post-narrowing). + - Any lens consumer that previously assumed `Int64` for all int literals. +4. **Test coverage** β€” add or update tests proving the narrowing reaches consumers correctly: + - `let x: u8 = 5` produces u8-typed code at emit, not Int64. + - `let x: u8 = 256` produces `MagnitudeOutOfRange` diagnostic (already in producer; this brief verifies consumer-side reporting works). +5. **DB-8 fixed-point bit-identical** for all existing programs (existing programs that didn't trigger narrowing should be unaffected; programs that DID benefit from narrowing now produce narrower target code β€” surface any in PR body). + +## Acceptance + +- [ ] Downstream-consumer audit recorded in PR body (table per Slice Β§2). +- [ ] Consumer migrations land per Slice Β§3 audit. +- [ ] Test coverage for narrowing reaching consumers correctly. +- [ ] DB-8 fixed-point converges bit-identically (or surfaces any intentional drift from narrowing benefits). +- [ ] Cross-program signal back: lane close β†’ Modeling Manager β†’ R2 Release Manager. **Note:** Goal 2 int-lit closure is **partial** (i64-bounded); full closure including `i64::MIN`-as-single-token requires the sibling Int128/Word128 sub-lane. Surface this in cross-program signal so R2 Release Manager understands the scoped close. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. +- [ ] No `--no-verify` push without explicit cargo-unavailable note. + +## STOP-AND-ESCALATE + +- **Producer brief landed a different carrier shape than this brief assumes** (e.g., re-scope reverted, or new fields added to range-facts). Re-read producer; this brief's slice may need adjustment. +- **Audit reveals a consumer that genuinely needs the deferred Int128/Word128 carrier** (i.e., its dispatch logic requires representing magnitudes outside i64). STOP β€” that consumer waits on the sibling sub-lane; do not partial-migrate it. +- **Reconciliation narrowing site changed** between producer's authoring and worker's dispatch. Surface; producer brief may need refresh. +- **DB-8 drifts unexpectedly** β€” STOP immediately. +- **`i64::MIN`-as-single-token tests requested** β€” that's the deferred sibling sub-lane's scope; do NOT add such tests in this PR. + +## Non-goals + +- **NOT widening `LiteralBits::Int(i64)`** β€” explicitly producer's deferred sibling sub-lane. +- **NOT closing `i64::MIN`-as-single-token representability** β€” same. +- Not extending int-algebra semantics. +- Not authoring the producer carrier (producer brief's job). +- Not tokenizer-charclass phase-2 (separate T-Modeling item). +- Not full DB-11 alias-`where` closure (adjacent, not subsumed). + +## Cross-program note + +- **Producer:** Substrate Manager β†’ `t-substrate-cardinality-int-lit-worker.md` (range-facts-only re-scope). +- **Consumer:** this brief (Modeling Manager). +- **Sibling sub-lane (deferred; not part of this lane):** Int128/UInt128/Word128Carrier substrate work that closes `LiteralBits::Int` widening + `i64::MIN`-as-single-token. Tracked separately by Substrate Manager. +- **Downstream signal:** R2 Release Manager β€” Goal 2 int-lit **partial close** (i64-bounded scope). Full close requires sibling Int128/Word128 sub-lane completion. + +## Reporting + +Single PR. Title: `feat(v3): T-Modeling int-lit magnitude β€” consume range-facts substrate; narrowing reaches downstream consumers (i64-bounded)`. Body cites this brief + producer brief + signal-receipt + downstream-consumer audit table + DB-8 disposition + explicit note that full Goal 2 closure remains gated on sibling Int128/Word128 sub-lane. + +On merge: signal R2 Release Manager β€” Goal 2 partial close. diff --git a/docs/briefs/r2-modeling-secret-graduation-worker.md b/docs/briefs/r2-modeling-secret-graduation-worker.md new file mode 100644 index 00000000000..f5dead07694 --- /dev/null +++ b/docs/briefs/r2-modeling-secret-graduation-worker.md @@ -0,0 +1,72 @@ +# T-Modeling β€” `Secret` graduation worker brief `(M; consumer of T-Substrate nominal-opaque-for-Secret)` + +> **Worker brief.** Reports through Modeling Manager (post-R2 spin-up) / +> Director (pre-spin-up). T-Modeling Goal 2 item. +> +> **Gated on:** Substrate Manager readiness signal for +> [`r2-substrate-nominal-opaque-for-secret-subset.md`](r2-substrate-nominal-opaque-for-secret-subset.md). +> **Do not dispatch until that signal posts.** + +## Read first + +- **[`docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md`](r2-substrate-nominal-opaque-for-secret-subset.md)** β€” producer brief; defines the nominal-opacity carrier this worker consumes. +- **[`THESIS.md`](../../THESIS.md)** Β§"Enumerable impossible-bug classes" β€” `Secret` is a Tier 1 thesis claim. +- **[`dsl/std/types.dag`](../../dsl/std/types.dag)** β€” current type-aliasing patterns; the `Secret` declaration lands here. +- **`feedback_state_space_vs_behavioral_invariants`** β€” type-level enforcement preferred. + +## Frame + +Producer landed the nominal-opacity substrate carrier. This brief authors `Secret` itself as a typed wrapper that consumes the carrier β€” declarations of `Secret` are nominal-opaque, with specified accessors (`redact`, `compare_in_constant_time`) being the only structural-access path to inner `T`. + +After this lane closes, naive operations (logging, equality, serialization, structural pattern-match) on `Secret` produce typed diagnostics at compile time, not runtime warnings. + +## Slice + +1. **Confirm Substrate readiness signal.** Producer carrier in `src/v3/std/` with Rust mirror parity. +2. **Author `Secret` declaration** in `src/v3/std/secret.dag` (or appropriate location). Apply the nominal-opacity carrier per producer brief's contract. +3. **Author the gated accessors:** + - `redact: Secret -> RedactedString` (or worker-equivalent; surface choice) + - `compare_in_constant_time: Secret, Secret -> Bool` + - Any others surfaced during producer-brief design. +4. **Diagnostic for non-gated access.** When a structural lens or operation tries to read inside `Secret` outside the gated accessors, emit typed diagnostic. Per `feedback_fail_closed_discipline` C-8. +5. **Regression tests:** + - `Secret` declared; gated accessors work. + - Naive `==` / structural-walk / pattern-match on `Secret` produces typed diagnostic. + - Spoofing test: a non-Secret nominal type does NOT receive Secret-style opacity by accident. +6. **DB-8 fixed-point bit-identical.** + +## Acceptance + +- [ ] `Secret` declared in `src/v3/std/`; consumes producer's nominal-opacity carrier. +- [ ] Gated accessors authored. +- [ ] Diagnostic for non-gated access emitted per C-8. +- [ ] Regression tests cover positive + negative + spoofing. +- [ ] DB-8 converges bit-identically. +- [ ] Cross-program signal: lane close β†’ Modeling Manager β†’ R2 Release Manager (Goal 2 Secret item) + Impossible-Bugs Manager (thesis claim covered). +- [ ] `cargo test` / clippy / fmt clean. + +## STOP-AND-ESCALATE + +- **Producer carrier shape doesn't admit gated accessors cleanly.** Surface; producer brief may need extension. +- **Generic-walk discipline (per producer brief)** breaks existing lens fixtures (cost, complexity). Surface; this is a discipline call about lens contracts vs opacity. +- **Accessor-gating mechanism** doesn't fit modeled access patterns (e.g., needs runtime dispatch). Surface; nominal-opacity may need substrate refinement. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- Not extending `Secret` to general nominal-typed effects. +- Not authoring the substrate carrier (producer brief's job). +- Not module-system export-discipline redesign. +- Not authoring full encryption / cryptographic operations on `Secret` β€” only the structural opacity layer. + +## Cross-program note + +- **Producer:** Substrate Manager β†’ nominal-opaque-for-Secret. +- **Consumer:** this brief. +- **Downstream signals:** R2 Release Manager (Goal 2 close); Impossible-Bugs Manager (thesis claim covered structurally). + +## Reporting + +Single PR. Title: `feat(v3): T-Modeling Secret graduation β€” typed wrapper consuming nominal-opacity substrate; gated accessors`. Body cites this brief + producer brief + signal-receipt + DB-8 disposition. + +On merge: signal R2 Release Manager + Impossible-Bugs Manager. diff --git a/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md b/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md new file mode 100644 index 00000000000..270be5fdaa5 --- /dev/null +++ b/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md @@ -0,0 +1,74 @@ +# T-Modeling β€” Tokenizer charclass phase-2 worker brief `(M; consumer of T-Substrate ValueBody-list/sum)` + +> **Worker brief.** Reports through Modeling Manager (post-R2 spin-up) / +> Director (pre-spin-up). T-Modeling Goal 2 item β€” completes the +> tokenizer charclass migration started in phase-1. +> +> **Gated on:** Substrate Manager readiness signal for the T-Substrate +> ValueBody-list/sum sub-lane (worker brief #790). +> **Do not dispatch until that signal posts.** + +## Read first + +- **[#790 worker brief](https://github.com/gunb-ai/gunbc/pull/790)** β€” T-Substrate ValueBody-list/sum sub-lane producer brief. +- **[`src/v3/std/tokenize.dag`](../../src/v3/std/tokenize.dag)** β€” tokenizer authority; phase-1 lands the structural shape, phase-2 retypes consumers to `Char` / `List` / `CharClass`. +- **[#662](https://github.com/gunb-ai/gunbc/pull/662)** β€” "tokenize: reframe character-level scaffold as consumption gap" (merged); confirm phase-1 baseline. +- **[`docs/thesis/the-substrate-two-coordinated-shapes.md`](../thesis/the-substrate-two-coordinated-shapes.md)** β€” connective vocabulary; `Cardinality` / `Disj` semantics for charclass sum-types. +- **[`src/v3/std/unicode.dag`](../../src/v3/std/unicode.dag)** (if exists) β€” unicode authority; charclass dependency. + +## Frame + +Phase-1 (per #662 retrospective and ROADMAP entries) reframed the character-level scaffold as a consumption gap: tokenizer doesn't yet consume canonical `Char` / `List` / `CharClass` types because the substrate didn't admit `ValueBody::List` / sum-typed value bodies. + +Producer (T-Substrate ValueBody-list/sum sub-lane #790) lands that substrate. This brief migrates tokenizer consumers to retype against `Char` / `List` / `CharClass`, dropping any host-string scaffolding. + +After this lane closes: tokenizer charclass is structurally typed end-to-end; lens consumers (cost, complexity) walk charclass declarations as canonical `.dag` values; Engine sharpened-(b) (cross-lane consumer of the same producer) becomes dispatchable independently. + +## Slice + +1. **Confirm Substrate readiness signal** from #790 producer. +2. **Audit phase-1 baseline.** Confirm what phase-1 (#662 retrospective) landed β€” the structural shape β€” and what phase-2 must migrate (the consumer side). +3. **Migrate tokenizer charclass consumers** to consume `Char` / `List` / `CharClass` typed structures instead of host-string scaffolding. +4. **Drop host-string scaffolds** that phase-1 left as bridges. Surface what's removed in PR body. +5. **Regression tests:** + - Tokenizer produces `CharClass` typed outputs for charclass tokens. + - Lens fixtures (cost, complexity) walk `CharClass` declarations canonically. + - Spoofing: host-string fallbacks no longer resolve charclass dispatch. +6. **DB-8 fixed-point bit-identical.** + +## Acceptance + +- [ ] Tokenizer charclass consumers retyped to `Char` / `List` / `CharClass`. +- [ ] Phase-1 host-string scaffolds dropped (preferred), **OR** any residual scaffold has the full tracked-bridge triple: (1) **documented** in-line at the residual site explaining what's bridged + why; (2) **bounded** β€” explicit ROADMAP debt row with named owner / lane; (3) **named dissolution trigger** β€” concrete event/PR that closes it (not "TBD" or "future cleanup"). Per `INVARIANTS.md` P5; B4.4 shape (b) is the precedent for the triple. Residuals without all three are a STOP-AND-ESCALATE. +- [ ] Regression tests pass; lens fixtures walk canonical types. +- [ ] DB-8 converges bit-identically. +- [ ] Cross-program signal: lane close β†’ Modeling Manager β†’ R2 Release Manager (Goal 2 charclass-phase-2 item). +- [ ] **Independent of Engine sharpened-(b)** β€” this brief shares producer with Grounding Manager's Engine work but does not depend on Engine landing first. +- [ ] `cargo test` / clippy / fmt clean. + +## STOP-AND-ESCALATE + +- **Producer brief landed without `ValueBody::List` for the shapes tokenizer needs** β€” surface; tokenizer consumer can't migrate without the structural support. +- **`std.unicode` dependency surfaces.** If charclass-phase-2 needs `std.unicode` declarations not yet in std, surface β€” that's a producer-brief expansion call. +- **Engine sharpened-(b) (Grounding Manager's consumer of same producer) lands first and surfaces a different consumer pattern** β€” coordinate cross-program; the substrate may need refinement. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- Not authoring full Unicode tables β€” minimal what tokenizer needs. +- Not extending tokenizer beyond charclass β€” separate work. +- Not authoring the producer carrier (#790's job). +- Not engine sharpened-(b) consumer migration (Grounding Manager's territory; same producer, different consumer). + +## Cross-program note + +- **Producer:** Substrate Manager β†’ ValueBody-list/sum sub-lane (#790). +- **Consumer (this brief):** Modeling Manager. +- **Sibling consumer:** Grounding Manager β†’ Engine sharpened-(b) β€” independent dispatch; share producer signal but not consumer code. +- **Downstream signal:** R2 Release Manager (Goal 2 close). + +## Reporting + +Single PR. Title: `feat(v3): T-Modeling tokenizer charclass phase-2 β€” retype consumers to Char/List/CharClass per ValueBody-list/sum substrate`. Body cites this brief + #790 producer + #662 phase-1 retrospective + signal-receipt + DB-8 disposition. + +On merge: signal R2 Release Manager. diff --git a/docs/briefs/r2-substrate-cardinality-for-int-lit-subset.md b/docs/briefs/r2-substrate-cardinality-for-int-lit-subset.md new file mode 100644 index 00000000000..2154cb0cb50 --- /dev/null +++ b/docs/briefs/r2-substrate-cardinality-for-int-lit-subset.md @@ -0,0 +1,39 @@ +# T-Substrate sub-lane β€” Cardinality-for-int-lit subset `(REDUNDANT β€” superseded by existing t-substrate-cardinality-int-lit-worker.md)` + +> **DO NOT DISPATCH AGAINST THIS BRIEF.** The R2 spin-up authoring +> wave authored this as a producer scoping brief without first +> grepping for an existing authority. **Existing brief is at +> [`docs/briefs/t-substrate-cardinality-int-lit-worker.md`](t-substrate-cardinality-int-lit-worker.md)** β€” +> the authoritative scope decisions, post-`wise-pike-578` STOP-AND-ESCALATE +> re-scope (carrier-widening deferred to sibling sub-lane, +> String-decimal range facts, etc.). This file documents the audit +> receipt and routes consumers to the existing authority. + +## Authority audit β€” the brief already exists + +Per `feedback_audit_adjacent_authority_first` + `feedback_verify_thesis_claims`: grep before authoring. The existing authority covers the same scope: + +- **[`docs/briefs/t-substrate-cardinality-int-lit-worker.md`](t-substrate-cardinality-int-lit-worker.md)** β€” already authored; carries the canonical scope decisions: + - **Re-scoped 2026-04-25** post-`wise-pike-578` STOP-AND-ESCALATE: keep `LiteralBits::Int(i64)` substrate-side; carrier-widening (Int128/UInt128/Word128Carrier) deferred to sibling sub-lane. + - Range facts use String-decimal representation (width-independent; covers u64 bounds that exceed i64). + - Reconciliation narrowing at `infer.rs:704-725`; `MagnitudeOutOfRange` diagnostic per C-8. + - `i64::MIN` smoke test deferred to sibling sub-lane. + - 5 numbered consumer-side requirements, slice, acceptance. + +**My R2 spin-up brief was duplicate authoring.** Same pattern as the parametric-algebra-for-Dimensions reframe: assumed the brief didn't exist; would have caused single-authority violation. + +## Disposition + +- **This file: closed as redundant.** The existing authoritative brief is `t-substrate-cardinality-int-lit-worker.md`. All scope decisions, slice, acceptance, and STOP-AND-ESCALATE live there. +- **No producer-side work to author.** The existing brief is dispatchable as-is. +- **Consumer-side:** [`r2-modeling-int-lit-magnitude-worker.md`](r2-modeling-int-lit-magnitude-worker.md) is updated to cite the existing brief as its producer prerequisite. + +## Pattern signal + +This is the second R2 spin-up substrate brief closed as redundant (after parametric-algebra-for-Dimensions). The audit-first discipline applied at the time would have caught both. **Always grep `docs/briefs/` for existing authority before authoring R2 spin-up substrate briefs.** + +## Cross-program note + +- **Producer authority:** `t-substrate-cardinality-int-lit-worker.md` (existing). +- **Consumer:** Modeling Manager β†’ `r2-modeling-int-lit-magnitude-worker.md` (cites the existing brief). +- **Sibling sub-lane (deferred):** Int128/UInt128/Word128Carrier substrate work β€” closes the `i64::MIN`-as-single-token gap. Per the existing brief's re-scope. Tracked separately; not part of this lane. diff --git a/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md b/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md new file mode 100644 index 00000000000..39c997129dc --- /dev/null +++ b/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md @@ -0,0 +1,114 @@ +# T-Substrate sub-lane β€” Nominal-opaque-for-Secret subset `(M; substrate sub-lane scoping brief)` + +> **Substrate Manager program brief.** Scopes the nominal-opaque substrate +> work needed to unblock T-Modeling `Secret` (Goal 2). Per +> [`docs/r2-structure.md`](../r2-structure.md) Substrate Manager +> ownership; not full nominal-type-system substrate β€” narrowed to the +> `Secret` consumer. +> +> **Producer:** Substrate Manager (this brief). +> **Consumer:** Modeling Manager β€” `r2-modeling-secret-graduation-worker.md` +> (Wave 3). + +## Read first + +- **[`THESIS.md`](../../THESIS.md)** Β§"Enumerable impossible-bug classes" β€” `Secret` is one of the R2+ Tier 1 thesis claims; structural opacity is the impossible-bug-by-construction guarantee. +- **[`dsl/std/types.dag`](../../dsl/std/types.dag)** β€” current type system; how named types are namespaces (`feedback_naming_is_aliasing`); how `inhabits` edges work for algebra attachment. +- **[`src/v3/std/substrate.dag`](../../src/v3/std/substrate.dag)** β€” live substrate authority for `TypeConnective` + Declaration shape. +- **[`src/v3/spec/v3_l1.dag`](../../src/v3/spec/v3_l1.dag)** β€” sentinel meta-types; precedent for cross-cutting substrate fields like `DeclarationRef`. +- **`feedback_naming_is_aliasing`** β€” named types are namespaces; the compiler sees through. Nominal opacity is the deliberate exception β€” the brief's discipline anchor. +- **`feedback_state_space_vs_behavioral_invariants`** β€” type-level enforcement preferred over API-level enforcement. + +## Frame + +`Secret` is a thesis-level commitment: a typed wrapper such that consumers cannot read the inner `T` except through specified accessors (e.g., `redact`, `compare_in_constant_time`). The bug class made impossible: accidental disclosure of secret material via naive structural access (logging, serialization, equality comparison, etc.). + +**The substrate gap:** today, named types in gunbc are namespaces β€” the compiler sees through aliases. Nominal opacity is a **deliberate exception** to that discipline; it requires a substrate flag/carrier on declarations that says "this type's structure is hidden from generic consumers; access is gated." + +**Scope is narrow:** only what T-Modeling `Secret` needs. Full nominal-type-system substrate (e.g., for arbitrary nominal types with custom invariants, for nominal-typed effects, for general newtype patterns) is **out of scope** β€” those are separate substrate-capability lanes. + +## Pre-author authority audit (mandatory) + +**Before designing**, grep `src/v3/std/` + `src/v3/spec/` for: + +- existing nominal-opaque flag / carrier on declarations +- existing structural-access-gated patterns (e.g., `phantom`, `opaque`, `sealed` declarations) +- `inhabits` edge usage for nominal-vs-structural distinction +- existing accessor-gating patterns in std (e.g., methods declared in a way that's the ONLY structural access path to a type's interior) + +**If audit reveals existing authority sufficient, reframe as consumer migration.** + +## Open design questions (worker / Substrate Manager resolves at dispatch) + +1. **Carrier shape.** Worker-autonomous options (do NOT add a seventh `TypeConnective` variant β€” that's a C1 stop signal per THESIS substrate-shape lock; the 6 connectives `Atom | Conj | Disj | Arrow | Cardinality | Instantiation` are canonical and a 7th requires failed-dissolution evidence + Director substrate-design call, not autonomous worker pick): + - **Boolean flag on Declaration** (`is_nominal_opaque: Bool`) β€” the compiler reads it during structural-walk and refuses to descend. + - **Sealed-accessor pattern** β€” declaration carries a list of permitted-accessor `DeclarationRef`s; structural walks for any other purpose fail. + - **`inhabits`-edge-shape carrier** β€” declarations participate in opacity by their algebra-attachment shape rather than a separate flag (audit-time check whether the existing `inhabits` machinery admits this without new substrate). + Worker picks among these; surface choice + reasoning in PR. **STOP-AND-ESCALATE if all three options fail dissolution checks** β€” that's the precondition for proposing a 7th connective via Director substrate-design call, NOT a worker autonomous path. + +2. **Generic-walk discipline.** When a structural lens walks a Dag containing `Secret`, what happens at the opacity boundary? Options: + - Hard stop (lens emits opacity diagnostic, refuses to descend). + - Soft stop (lens treats `Secret` as opaque atom; structural walk continues but inner is invisible). + - Per-lens declaration (each lens declares whether it respects opacity). + Worker picks; surface in PR. + +3. **Accessor gating.** How does the substrate express "only `redact` and `compare_in_constant_time` may read Secret's interior"? Options: + - Accessor `DeclarationRef` list on the opaque type. + - Visibility/scope marker on the inner field declarations. + - Module-system-style export discipline. + Worker picks; this is the highest-leverage design call. + +4. **Generic parameter `T`.** Does `Secret` require all `T` to be opaque, or only `T` reads through Secret accessors are gated? Per thesis discipline: `T` itself stays structural; only access *through Secret* is gated. + +## Slice (worker fills at dispatch) + +**Same-PR consumer proof required** per `INVARIANTS.md` P2 boundary discipline (no landed boundary without a real consumer). Two acceptable shapes β€” worker picks; surface choice: + +- **Shape A (preferred): bundle with the T-Modeling `Secret` consumer.** This brief and `r2-modeling-secret-graduation-worker.md` land in the same PR; substrate carrier + `Secret` declaration + gated accessors + opacity diagnostic all together. Eliminates the producer-without-consumer window. +- **Shape B (fallback): bundle with a minimal structural-walk consumer proof.** If T-Modeling consumer is too large to land same-PR, this PR includes a minimal lens / structural-walk consumer that **reads the carrier and fails closed** when an opaque type is structurally walked outside gated accessors. The minimal consumer is the boundary proof; T-Modeling `Secret` consumes the same carrier in a follow-up. + +1. **Audit existing nominal-opaque substrate** (per audit section). +2. **Land minimal substrate carrier** in `src/v3/std/` per design choice. +3. **Lower the carrier** β€” declarations marked nominal-opaque get the substrate fact attached at lowering / parsing. +4. **Coproduct dissolution receipt** for any new TypeConnective variant. +5. **Document generic-walk discipline** in INVARIANTS.md or feedback memory β€” what does opacity mean for lens consumers? +6. **Same-PR consumer proof** per Shape A or B above. Surface the choice in PR body. +7. **Cross-program signal:** on merge, signal Modeling Manager that Secret is dispatchable (Shape A: jointly authored; Shape B: follow-up consumer). + +## Acceptance + +- [ ] Authority audit receipt recorded. +- [ ] Substrate carrier for nominal-opacity lands in `src/v3/std/` (canonical + Rust mirror). +- [ ] Coproduct dissolution receipt for any new variant. +- [ ] Generic-walk discipline documented (INVARIANTS.md or feedback memory). +- [ ] Accessor-gating mechanism documented in PR body. +- [ ] **Same-PR consumer proof** lands per Shape A (`Secret` consumer bundled) or Shape B (minimal structural-walk consumer with fail-closed opacity check). Choice surfaced in PR body. +- [ ] DB-8 fixed-point converges bit-identically. +- [ ] Cross-program readiness signal posted to Modeling Manager. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` / `cargo clippy --all-targets -- -D warnings` / `cargo fmt --all --check` clean. + +## STOP-AND-ESCALATE + +- **Scope expansion:** the nominal-opaque substrate generalizes naturally to other nominal types (e.g., `Phantom`, `Sealed`, custom newtypes). If the design surfaces a general-purpose nominal-type-system substrate, that's a re-scope decision, not a quiet expansion. +- **`inhabits` edge interaction.** Nominal opacity may interact with how `inhabits` walks the algebra-attachment graph β€” surface for design call if so. +- **Generic-walk discipline conflicts with existing lens behavior.** If hard-stop opacity breaks existing lens fixtures (cost, complexity, idempotency), surface; this is a discipline call about lens contracts, not a substrate call. +- **DB-8 drifts** β€” STOP immediately. + +## Non-goals + +- **Not full nominal-type-system substrate.** General nominal types, custom newtype patterns, nominal-typed effects β€” separate lanes. +- Not module-system export-discipline redesign β€” minimal targeted carrier. +- Not extending Secret semantics beyond the thesis-level commitment. +- Not authoring `Secret` itself β€” that's T-Modeling consumer territory. + +## Cross-program note + +- **Producer:** Substrate Manager (this brief). +- **Consumer:** Modeling Manager β†’ `r2-modeling-secret-graduation-worker.md` (gated on this lane's readiness signal). +- **Adjacent:** Impossible-Bugs Manager β€” `Secret`-leakage is a thesis-level impossible-bug class; the carrier is the substrate dependency for that proof. Heads-up to Impossible-Bugs Manager at landing. + +## Reporting + +Single PR. Title: `feat(v3): T-Substrate nominal-opaque-for-Secret subset β€” minimal carrier for T-Modeling Secret consumer`. Body cites this brief + audit receipt + design choice (carrier shape + walk discipline + accessor gating) + cross-program signal. + +On merge: signal Modeling Manager that Secret consumer is dispatchable; cc Impossible-Bugs Manager. diff --git a/docs/briefs/r2-substrate-parametric-algebra-for-dimensions-subset.md b/docs/briefs/r2-substrate-parametric-algebra-for-dimensions-subset.md new file mode 100644 index 00000000000..96c4c48776b --- /dev/null +++ b/docs/briefs/r2-substrate-parametric-algebra-for-dimensions-subset.md @@ -0,0 +1,64 @@ +# T-Substrate sub-lane β€” Parametric-algebra-for-Dimensions subset `(NO-OP / closed by audit; substrate already in place)` + +> **Substrate Manager program brief.** Originally framed as a producer +> sub-lane to land phantom-parameter substrate for T-Modeling +> `Dimension`. **Authority audit reveals substrate is already +> in place** β€” this lane is effectively closed pre-spin-up; T-Modeling +> Dimensions consumer brief +> ([`r2-modeling-dimensions-phantom-worker.md`](r2-modeling-dimensions-phantom-worker.md)) +> is dispatchable immediately against the existing carrier. + +## Authority audit β€” substrate is landed + +Per `feedback_audit_adjacent_authority_first`: grep before designing. The phantom-parameter substrate is **already first-class** in v3: + +- **[`src/v3/compiler/src/dag.rs:186`](../../src/v3/compiler/src/dag.rs)** β€” `Declaration.phantom_params: Vec`. The carrier exists on the canonical `Declaration` struct. +- **[`src/v3/compiler/src/dag.rs:217-220`](../../src/v3/compiler/src/dag.rs)** β€” `PhantomParameter { parameter: DeclarationId, algebra: DeclarationId }`. Two-edge carrier: parameter declaration + algebra declaration that governs closure. +- **[`src/v3/compiler/src/dag.rs:148-160`](../../src/v3/compiler/src/dag.rs)** β€” doc comment explicitly states: *"The initial R2 Dimensions consumer needs only abelian-group closure, carried as a typed edge to the substrate algebra declaration: matching phantom values compose, mismatched values fail closed as a unit mismatch."* The substrate was authored explicitly for the R2 Dimensions consumer. +- **[`src/v3/compiler/src/infer.rs:1057, :1132`](../../src/v3/compiler/src/infer.rs)** β€” `phantom_unit_mismatch` function exists; type-equivalence and unit-mismatch dispatch are already wired through inference. +- **[`src/v3/compiler/src/dag.rs:1941`](../../src/v3/compiler/src/dag.rs)** β€” `AbelianGroup` algebra Conj cited as canonical authority for phantom-unit closure. + +**Conclusion:** all four open design questions originally posed in this brief (carrier shape / type-equivalence rule / algebra-method dispatch / lifting-coercion) are **already resolved structurally** by the existing substrate. There is no gap to fill on the producer side. + +## Disposition + +- **Substrate side: closed.** No new carrier. No new variant. No new substrate-shape decisions required. The existing `phantom_params` carrier with its `(parameter, algebra)` shape is the substrate authority. +- **Consumer side: dispatchable now.** [`r2-modeling-dimensions-phantom-worker.md`](r2-modeling-dimensions-phantom-worker.md) consumes the existing carrier directly β€” no readiness signal from this lane is needed because the substrate is already landed. +- **No-op PR for this brief.** This brief documents the audit receipt and closes the lane. Optional follow-up: if Substrate Manager (post-spin-up) wants the brief deleted entirely as redundant scope, that's a tracking-doc cleanup; the audit receipt persists either way. + +## Why the original framing was wrong + +`feedback_verify_thesis_claims` violation on Director-side brief authoring: I assumed "the substrate gap" without grepping `phantom_params` / `PhantomParameter` first. The audit-first discipline applies to brief authoring, not just to worker dispatch. + +Pattern signal: this is the fourth such violation in the R2 spin-up wave (after nested-optional gating-on-substrate, unhandled-diagnostic path-default, unenumerated-effects 8-req-elision, and now this lane being framed as producer when it's already closed). All four follow the same shape β€” assumed substrate state without grep. + +## What's actually open (cross-program note) + +If anything is genuinely open on the Dimensions side, it's in **T-Modeling consumer territory**, not Substrate Manager: + +- Authoring `Dimension` itself (consumes `phantom_params`). +- Authoring core SI base unit declarations. +- Algebra-method dispatch decision (consumes existing `inhabits` algebra-attachment patterns + `phantom_unit_mismatch`). +- Lifting / coercion discipline (per design discipline: strictly nominal preferred). + +All of that is in [`r2-modeling-dimensions-phantom-worker.md`](r2-modeling-dimensions-phantom-worker.md); this brief defers entirely. + +## Acceptance (for the no-op disposition) + +- [ ] This document records the audit receipt + closes the lane. +- [ ] Cross-reference from `r2-modeling-dimensions-phantom-worker.md`'s "Read first" updated to consume `Declaration.phantom_params` directly (no producer signal needed). +- [ ] Substrate Manager (post-spin-up) confirms no producer work needed and surfaces this lane as closed in their working state. + +## Reporting + +This brief documents a closed lane. No PR needed; the audit receipt stays in this file. T-Modeling Dimensions consumer brief dispatches independently when Modeling Manager spins up. + +## Cross-program note + +- **Producer:** none required (substrate already landed). +- **Consumer:** Modeling Manager β†’ `r2-modeling-dimensions-phantom-worker.md` (dispatchable now). +- **Adjacent:** Impossible-Bugs Manager β€” unit-mismatch is a thesis-level impossible-bug class; the carrier is the substrate dependency for that proof. Heads-up at landing. + +## Lesson saved + +Per pattern across R2 spin-up reframes: **always grep the substrate before authoring producer briefs**, not just worker briefs. The discipline doesn't end at brief boundaries.