diff --git a/docs/briefs/r1-surface-manager.md b/docs/briefs/r1-surface-manager.md index 997d3f04909..0425af232f4 100644 --- a/docs/briefs/r1-surface-manager.md +++ b/docs/briefs/r1-surface-manager.md @@ -1,5 +1,18 @@ # R1 Surface Manager Brief +> **πŸ”„ SUPERSEDED 2026-04-26 by [`r1-closure-manager.md`](r1-closure-manager.md).** +> R1 gate-close authority now lives with the R1 Closure Manager (PR #847) +> under strict-interpretation reading: every gate in `ROADMAP.md Β§"Lane +> acceptance β€” .dag gates"` must be a `.dag` `TestClaim` that compiles AND +> evaluates true. Implementation receipts are necessary but **not sufficient**. +> The "Working state" section below was originally written under a more +> permissive reading where receipt-landed counted as gate-closed; that +> conflation is corrected in the table β€” implementation receipts and `.dag` +> gate status are now tracked as separate columns. Gates remain owned by +> R1 Closure Manager lanes (R1C-A through R1C-F) until they evaluate. +> This brief stays in-tree as a historical receipt of the lane sequencing; +> new R1 dispatch happens under R1 Closure Manager, not here. + ## Orient before reading - Product direction: [PR #672](https://github.com/gunb-ai/gunbc/pull/672) @@ -120,45 +133,39 @@ for a principal engineer to verify in one evening. ## Working state -Lane-owner dispatch status (update as sub-deliverables close): - -**T-P0 (closed on current ancestry):** -- [x] `repeat_string` fix landed (brief: `p0-render-repeat-string.md`) -- [x] `REST_OPS` drift resolved (brief: `p0-rest-ops-drift.md`) -- [x] `no_profile_sentinel` audit completed (brief: `p0-bug-no-profile-sentinel.md`) - -**T-Sub:** -- [x] `sub_match_over_user_sum` gate compiles + passes (Day-1) - (PR #702, merged 2026-04-24 β€” `TestClaim` + suite in - `src/v3/compiler/tests/fixtures/r1_gates.dag` run through - `TestRunner`; #690 prior receipt confirmed structural match) -- [x] `sub_type_alias_where_lowers` parse + lower receipt landed - (DB-11 parse + lower substrate landed in PR #703, 2026-04-24 β€” - `SurfaceItem::TypeAlias` carries `refinement`; formal `.dag` - gate remains tied to the [ext] predicate path if release wants - a first-class `TestClaim` for this surface) -- [ ] `sub_charclass_in_std_unicode` phase-2 handed off with concrete - substrate/load-set blockers - (phase-1 tokenizer half landed in PR #693 + ROADMAP row #706, - 2026-04-24 β€” `CharClass` + `char_in_class` in `std.unicode`, - tokenizer calls `tokenize_char_class::byte_matches`; quiet-gull-882 - confirmed structural `CharClass` consumption from lowered - `tokenize.dag` is blocked by top-level `ValueBody` list/sum support - plus a `std.unicode` bootstrap/load-set decision) - -**T-Emit:** -- [x] Rust harden β€” `emit_rust_fixtures_rustc_green` gate test landed - (PR #694, merged 2026-04-24 β€” `#[ignore]`d named gate sweeps - 9 program fixtures + 5 reflected-module fixtures through the - batched rustc roundtrip; baseline `rustc_roundtrip_*` tests all - green) -- [ ] PR #650 generic-bound fidelity β€” `emit_generic_bounds_survive` - passes (PR #676 in review β€” session `vivid-cat-794`) -- [ ] Python/Go reconcile β€” `emit_omni_demo_fixtures_green` passes - across all three targets (cross-target progress 2026-04-24: - `Behavior::Loop` emission for Python + Go in #692; Python - operator-realization parity for `*` / `!=` / int comparisons - in #691; omni gate still pending) +> **Reading note (2026-04-26 SUPERSEDED amendment).** Implementation receipts +> (`Impl` column) record that the underlying feature work is in-tree. `.dag` +> gate status (`Gate` column) records whether the corresponding `TestClaim` +> in `ROADMAP.md Β§"Lane acceptance β€” .dag gates"` exists, compiles, and +> evaluates true under the strict-interpretation reading. Gate columns are +> closed only when both halves are true; the implementation-only `[x]` markings +> below are deliberately separated from gate close so the conflation that +> existed before this amendment doesn't recur. Gate-close authority is +> R1 Closure Manager (`docs/briefs/r1-closure-manager.md`). + +**T-P0 β€” implementation closed on current ancestry; `.dag` gates owned by R1 Closure R1C-B:** + +| Item | Impl | Gate (`.dag` TestClaim) | Owner | +|---|---|---|---| +| `repeat_string` | [x] (brief: `p0-render-repeat-string.md`) | [ ] `p0_repeat_string_correct` `[Day 1]` | R1C-B | +| `REST_OPS` drift | [x] (brief: `p0-rest-ops-drift.md`) | [ ] `p0_rest_ops_aligned` `[ext]` | R1C-B | +| `no_profile_sentinel` | [x] (brief: `p0-bug-no-profile-sentinel.md`) | [ ] `p0_no_fabrication_sentinel` `[ext]` | R1C-B | + +**T-Sub β€” `.dag` gates: 1 closed, 1 receipt-only, 1 substrate-deferred:** + +| Item | Impl | Gate (`.dag` TestClaim) | Owner | +|---|---|---|---| +| `sub_match_over_user_sum` (Day-1) | [x] PR #702 | [x] `TestClaim` + suite in `r1_gates.dag` runs through `TestRunner` | gate evaluates; closed | +| `sub_type_alias_where_lowers` (`[ext]`) | [x] PR #703 (DB-11 parse+lower) | [ ] `[ext]` predicate path TestClaim **not yet authored** | R1C-C (#879 in flight) | +| `sub_charclass_in_std_unicode` phase-2 | [x partial] PR #693 (phase-1 tokenizer half) | [ ] reclassified to **R2 T-Substrate** per 2026-04-24 amendment (Class 5 Gap 3) β€” no longer an R1 gate | R2 Substrate Manager | + +**T-Emit β€” implementation in flight; all three `.dag` gates owned by R1 Closure R1C-E:** + +| Item | Impl | Gate (`.dag` TestClaim) | Owner | +|---|---|---|---| +| Rust harden | [x] PR #694 (host-harness gate test, `#[ignore]`-able sweep) | [ ] `emit_rust_fixtures_rustc_green` `[ext: ExecuteCommand]` β€” host harness is **not** the `.dag` gate; R1C-E wraps it | R1C-E | +| Generic-bound fidelity | [partial] PR #676 in review | [ ] `emit_generic_bounds_survive` `[ext]` | R1C-E | +| Python/Go reconcile | [partial] #691 (Python parity) + #692 (`Behavior::Loop`) | [ ] `emit_omni_demo_fixtures_green` `[ext: ForAllTargets + ExecuteCommand]` | R1C-E | Decisions log (append as they happen): diff --git a/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md b/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md index e59ed0eabc3..d3314241914 100644 --- a/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md +++ b/docs/briefs/r2-impossible-bugs-nested-optional-flatten-worker.md @@ -18,8 +18,8 @@ - **[`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`). +- **[`src/v3/compiler/src/lower.rs:2129, :2226`](../../src/v3/compiler/src/lower.rs)** β€” `SurfaceType::Optional` lowering arms (lowering path + TypeConnective construction). Verify by grep `SurfaceType::Optional` at HEAD before editing. +- **[`src/v3/compiler/src/infer.rs:3129`](../../src/v3/compiler/src/infer.rs)** β€” `concretize_decl_with_subst` definition (the **killer construction site** per design doc β€” substitution path that bypasses `lower.rs`); call sites at `:2643, :2645, :3104, :3152, :3162, :3190` (grep `concretize_decl_with_subst` at HEAD for the live set). - **[`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. diff --git a/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md b/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md index cba2fbd5f84..6671f126e51 100644 --- a/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md +++ b/docs/briefs/r2-impossible-bugs-unenumerated-effects-worker.md @@ -65,7 +65,7 @@ Per design doc default: retire (path ii). ## 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. +- **OperationEffect retirement decision (path (i) vs (ii)) is NOT a STOP β€” the audit verdict IS this lane's deliverable.** Slice Β§2 + Acceptance Β§2 own producing the verdict (path-i existence-proof OR path-ii existence-proof) with structural justification + per-primitive receipt in PR body. The follow-up β€” actual `OperationEffect` enum retirement (path ii: enum + `derive_op_effect` + `idempotency.dag` re-anchor) or normalized-derived-view authoring (path i) β€” dispatches as a **sibling sub-lane** to Impossible-Bugs Manager based on the verdict; Director does not need to be in the loop for the verdict itself. **STOP only if** the audit reveals a primitive whose signature shape can't be made to derive cleanly **even after resource-threading migration (Slice Β§3)** β€” i.e., a substrate gap not anticipated by the design doc Q5.5 binary. That's an unscoped substrate-shape question, not a retain-vs-retire pick. - **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. diff --git a/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md b/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md index 40d5ed26021..d7101089889 100644 --- a/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md +++ b/docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md @@ -20,9 +20,9 @@ - **[`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`). +- **[`src/v3/spec/rust.dag:832`](../../src/v3/spec/rust.dag)** β€” `rust_int_div` realization (renders bare `{lhs} / {rhs}`). (`:816` is `rust_int_sub` β€” verify by grep `rust_int_div` at HEAD.) +- **[`src/v3/spec/go.dag:758`](../../src/v3/spec/go.dag)** β€” `go_int_div` realization (same shape). (`:742` is `go_int_sub`.) +- **[`src/v3/spec/python.dag:500`](../../src/v3/spec/python.dag)** β€” `python_int_div` realization (renders via `__v3_idiv` helper at `src/v3/compiler/src/emit/python_target.rs:680`; pinned by `m1_4_emit_python_test.rs:108-109`). (`:486` is inside `python_int_sub`.) - **[`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. @@ -47,9 +47,9 @@ Per design doc Β§4: the bug class closes by **removing the partial form**. For ` 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.) + - `rust.dag:832` (`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:758` (`go_int_div`) β€” reshapes to Go-idiomatic typed-split Result; same case-split discipline. + - `python.dag:500` (`python_int_div`) + `src/v3/compiler/src/emit/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. @@ -76,7 +76,7 @@ Per design doc Β§4: the bug class closes by **removing the partial form**. For ` - **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`?). +- **`Result` requires authoring `DivError` (with `DivideByZero | Overflow` variants) declaration** β€” verify the typed-split carrier doesn't exist via audit; if not, surface placement decision (`dsl/std/errors.dag`?). Single-error `Result` shape is explicitly rejected per Slice Β§2; STOP if any reading drifts back to a single-variant carrier. - **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. diff --git a/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md b/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md index 270be5fdaa5..9cbc4477eec 100644 --- a/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md +++ b/docs/briefs/r2-modeling-tokenizer-charclass-phase2-worker.md @@ -14,7 +14,7 @@ - **[`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. +- **[`dsl/std/unicode.dag`](../../dsl/std/unicode.dag)** β€” unicode authority; charclass dependency. ## Frame diff --git a/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md b/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md index 39c997129dc..1cf9857d34d 100644 --- a/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md +++ b/docs/briefs/r2-substrate-nominal-opaque-for-secret-subset.md @@ -12,7 +12,9 @@ ## 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. +- **[`docs/r2-structure.md`](../r2-structure.md)** Β§Goal 2 (lines 36, 42) + Β§Lane structure (`Secret` graduation) β€” locked R2 authority for the `Secret` nominal-opaque graduation as a Modeling-faithfulness Tier-1 R2 commitment. +- **[`ROADMAP.md:424`](../../ROADMAP.md)** post-merge-debt row β€” `Secret` nominal-wrapper graduation: `dsl/std/types.dag:237` declares `Secret = String` (alias); the substrate distinction between nominal-opaque and alias is the structural delta. **Cited by R2 Goal 2.** +- **[`docs/thesis/compositional-modeling.md` Part 4](../thesis/compositional-modeling.md)** β€” original thesis-doc surface; structural opacity argument. (THESIS.md Β§"Enumerable impossible-bug classes" lists `[R2+]` nested-optional / unenumerated-effects / unhandled-diagnostic-paths; `Secret` is **not** in that list β€” claim authority lives in r2-structure.md + ROADMAP, not THESIS.md, until/unless THESIS.md adds the entry.) - **[`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`.