From 68a2a2fdf5caa873ccecbb36253d023e3e5fe991 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 10:49:58 -0400 Subject: [PATCH 01/10] WIP: nested optional --- ...iblebugs-nested-optional-flatten-design.md | 151 ++++++++++++++++++ 1 file changed, 151 insertions(+) create mode 100644 docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md new file mode 100644 index 00000000000..1b31d77da15 --- /dev/null +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -0,0 +1,151 @@ +# T-ImpossibleBugs nested-optional flatten — design/scoping doc + +> **Output of `bright-moth-390` per the redirected scoping brief** +> ([`t-impossiblebugs-nested-optional-flatten-worker.md`](t-impossiblebugs-nested-optional-flatten-worker.md)). +> No code changes. Investigation result + Director-actionable recommendation. + +## TL;DR + +**Recommendation: bypass-feasible.** v3 substrate already has `TypeConnective::Cardinality { element, bound: CardinalityBound }` as a first-class connective (`src/v3/compiler/src/dag.rs:395`); the cardinality-substrate gate THESIS:343 names is the **v2** state described in `docs/architecture.md:109`, and v3 is past it. `T??` parses today, lowers to nested `Cardinality { bound: AtMostOne, .. }`, and is structurally distinct from `T?` only because nothing collapses the outer wrap. A two-line guard in `lower.rs` closes the bug class without touching substrate. Implementation lane is **XS**. + +## Q1 — Surface-upstream check: does `T??` parse? + +**Yes, `T??` parses cleanly. No rejection at parse, desugar, or lower.** + +Parser (`src/v3/compiler/src/parse_generated.rs:881-892`): + +```rust +fn parse_type_expr(&mut self) -> Result { + let mut ty = self.parse_atom_type()?; + while matches!(self.peek().kind, TokenKind::Question) { + let q = self.bump().clone(); + let start = ty.span().byte_start; + ty = SurfaceType::Optional { + inner: Box::new(ty), + span: SourceSpan::new(self.file, start, q.span.byte_end), + }; + } + Ok(ty) +} +``` + +The `while`-loop consumes any number of trailing `?` tokens. `T??` produces `SurfaceType::Optional { inner: SurfaceType::Optional { inner: T } }`. `T???` produces three nested layers. No diagnostic, no error. + +Tokenizer (`src/v3/compiler/src/tokenize_generated.rs:240`) maps `b'?'` to `TokenKind::Question`; nothing else gates double-`?`. + +**The dissolution does NOT live one layer upstream of algebra.** Surface accepts the nested form by construction. + +## Q2 — Substrate-attachment: what's the cardinality state in v3? + +**v3 substrate is past the cardinality bridge.** `architecture.md:109` describes the **v2** state — `return_cardinality` enum on Node with 142 construction sites, marked "Bridge — dissolve into edge existence." v3 has done that dissolution: `TypeConnective::Cardinality` is a first-class variant of the connective sum at `src/v3/compiler/src/dag.rs:395-398`: + +```rust +Cardinality { + element: DeclarationId, + bound: CardinalityBound, +}, +``` + +`CardinalityBound` (`src/v3/compiler/src/dag_scalar_generated.rs:21-25`): + +```rust +pub enum CardinalityBound { + Exact(u32), + AtMostOne, + Unbounded, +} +``` + +Lowering (`src/v3/compiler/src/lower.rs:1949-1968` and parallel arm at `:2044-2047`) maps `SurfaceType::Optional { inner }` to `TypeConnective::Cardinality { element: lower(inner), bound: AtMostOne }`. Recursive: `T??` becomes + +``` +Cardinality { + element: Cardinality { + element: , + bound: AtMostOne, + }, + bound: AtMostOne, +} +``` + +No collapse step exists. The matching code path (`infer.rs:1918-1965`, `bind_expected_decl_to_actual_context`) walks both expected and actual `Cardinality` recursively; nested-optional binds to nested-optional and not to single-optional. So today `T?` and `T??` are *distinct* DAG types. + +**Note on `OptionalOf` (algebra.dag:423).** `OptionalOf { inner: AlgebraTypeTemplate }` is a separate construct: it's a variant of the algebra-template enum used in std-method signatures (e.g., `first() -> OptionalOf` at algebra.dag:558). It does *not* participate in user-surface `T?` lowering; user code never produces an `OptionalOf` directly. The two systems are parallel: + +- User surface `T?` → `SurfaceType::Optional` → `TypeConnective::Cardinality { bound: AtMostOne }`. +- Std-algebra method declarations → `OptionalOf` (algebra-template only; resolves through algebra-instantiation, not generic type lowering). + +Flattening user-surface nested-optional therefore does not touch `OptionalOf`. (If `OptionalOf>` ever appears in std method declarations as an authoring mistake, that's a separate issue scoped to `dsl/std/algebra.dag`; out of scope here.) + +## Q3 — Bypass feasibility: per-construction-site flatten + +**Yes — clean two-line guard at `SurfaceType::Optional` lowering arms.** + +The algebraic property: `AtMostOne ∧ AtMostOne = AtMostOne`. In partial-function terms: `Option>` is observationally equivalent to `Option` because the cardinality semantics of `AtMostOne` is idempotent under self-composition (`min(1, min(1, n)) = min(1, n)`). This is the math of `AtMostOne`, not invented vocabulary. + +**Two arms to edit** (`src/v3/compiler/src/lower.rs`): + +1. `:1949-1968` — `type_to_declaration_id` `SurfaceType::Optional` arm: after lowering `inner`, check if `dag.declaration(element).connective` matches `TypeConnective::Cardinality { bound: CardinalityBound::AtMostOne, .. }`. If yes, return `element` directly without wrapping. +2. `:2044-2047` — `type_to_connective` `SurfaceType::Optional` arm: same guard; if inner already AtMostOne-wrapped, return the inner's connective (or its element-as-connective) instead of constructing a fresh wrap. + +The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: + +| Surface | Lowered | Flatten? | Reason | +|---|---|---|---| +| `T??` | `Cardinality, AtMostOne>` | **YES → `T?`** | `min(1, min(1, n)) = min(1, n)` | +| `List?` | `Cardinality, AtMostOne>` | **NO** | Optional-list ≠ list (`None` ≠ empty list) | +| `T?[]` (`List`) | `Cardinality, Unbounded>` | **NO** | List of optionals — outer is Unbounded | +| `[T; 3]?` | `Cardinality, AtMostOne>` | **NO** | Optional-fixed-array; `None` ≠ array of zeros | + +The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMostOne`. All other combinations stay distinct shapes. + +## Q4 — Recommendation: bypass implementation brief shape + +**Outcome: (a) bypass-feasible.** Director can fast-track an implementation brief (XS, not S). + +### Implementation-brief shape + +**Title:** `feat(v3): T-ImpossibleBugs — `T??` flattens to `T?` at lower (closes nested-optional flatten class)` + +**Reqs:** + +1. **Idempotent flatten in lower.** `SurfaceType::Optional` lowering arms in `src/v3/compiler/src/lower.rs:1949` and `:2044` add a guard: when the lowered inner element's connective is `TypeConnective::Cardinality { bound: AtMostOne, .. }`, return the inner element directly without constructing an outer wrap. Specific to `AtMostOne ∧ AtMostOne`; other bound combinations untouched. +2. **Span policy.** The flattened declaration uses the inner declaration's existing span (the user wrote `T??` syntactically; the type they got is structurally the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at lower. Document this in PR body. +3. **Test fixture.** A v3 compiler test asserting `T??` and `T?` produce the same `DeclarationId` (or the same `TypeConnective` shape modulo declaration identity); pattern-matching against `T??` requires only one level of unwrap. Place under `src/v3/compiler/tests/integration/`. + +**STOPs:** + +- **Any consumer matches on outer-`AtMostOne` over inner-`AtMostOne` as a meaningful distinct type** (audit `infer.rs` `Cardinality` arms before editing) — if so, that consumer carries a hidden assumption that flatten breaks. STOP and surface. +- **Lowering arm has a hidden caller path that needs the outer wrap for span/identity reasons** — STOP. +- **Generalization pressure to flatten `List>` or `Set>` falls out of the same guard** — it does not (those are `Unbounded ∧ Unbounded`, not idempotent in the same algebraic sense; they're legitimately distinct). STOP if the implementer is tempted. +- **DB-8 fixed-point drifts** — STOP immediately. + +**Dispatch profile:** XS, single PR, single worker. ~10-line code diff + 1 test fixture + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. + +**Acceptance:** + +- `T??` and `T?` produce the same lowered shape (test). +- `List?`, `T?[]`, `[T; 3]?` all preserve their distinct shapes (test). +- `cargo test --workspace --exclude v2-compiler-tests` clean. +- `cargo test -p v2-compiler-tests` clean. +- `clippy --all-targets -- -D warnings` clean. +- `cargo fmt --all --check` clean. +- DB-8 fixed-point converges bit-identically. +- SG-0 census deltas as needed. + +### Why not "needs upstream substrate design" + +The cardinality substrate THESIS:343 names as the gate is the **v2** state (`return_cardinality` enum, 142 sites). v3 has already promoted Cardinality to a first-class connective. There is no upstream substrate work to do — the substrate is in place; only the idempotent-meet rule at the construction site is missing. Adding that rule is not substrate redesign; it's a one-site invariant attached to existing substrate. + +### Why not "park" + +The bypass is small (XS), well-scoped (specific to `AtMostOne ∧ AtMostOne`), structurally grounded (algebraic idempotence of `AtMostOne`), and the substrate prerequisite is already met. Parking would be conservative beyond what the evidence supports. + +## Cross-manager note + +- **Zero-Floor Manager:** no current overlap. The bypass is a lower-stage rule, not substrate-extension; SG-0 census may show a delta if the test fixture lands. +- **Grounding Manager:** no overlap. + +## Closing signal + +`bright-moth-390` recommends Director author the bypass implementation brief described in §Q4 and dispatch to the next idle worker. No upstream blockers identified. The cardinality-substrate gate THESIS:343 names is closed (in v3) by virtue of `TypeConnective::Cardinality` being a first-class connective, not a bridge enum. From 6b1ddf7a66aba608a6d52ebdf390369160cba98f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 11:01:57 -0400 Subject: [PATCH 02/10] =?UTF-8?q?docs(briefs):=20tighten=20Q3=20line=20:89?= =?UTF-8?q?=20=E2=80=94=20clarify=20type=5Fto=5Fconnective=20contract?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit openai-pro review flagged ambiguous "(or its element-as-connective)" parenthetical: could be misread as peeling T?? to T instead of T?, contradicting the acceptance criterion. Replace with explicit "return/clone the inner's TypeConnective::Cardinality verbatim, do NOT peel to element-as-connective" so the impl worker cannot mis-interpret. Non-blocking finding from PR #798 review (APPROVE_WITH_COMMENTS). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 1b31d77da15..86ecb3007d6 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -86,7 +86,7 @@ The algebraic property: `AtMostOne ∧ AtMostOne = AtMostOne`. In partial-functi **Two arms to edit** (`src/v3/compiler/src/lower.rs`): 1. `:1949-1968` — `type_to_declaration_id` `SurfaceType::Optional` arm: after lowering `inner`, check if `dag.declaration(element).connective` matches `TypeConnective::Cardinality { bound: CardinalityBound::AtMostOne, .. }`. If yes, return `element` directly without wrapping. -2. `:2044-2047` — `type_to_connective` `SurfaceType::Optional` arm: same guard; if inner already AtMostOne-wrapped, return the inner's connective (or its element-as-connective) instead of constructing a fresh wrap. +2. `:2044-2047` — `type_to_connective` `SurfaceType::Optional` arm: same guard. If the lowered inner declaration's connective is `TypeConnective::Cardinality { element, bound: AtMostOne }`, return/clone that connective verbatim — i.e. `TypeConnective::Cardinality { element, bound: AtMostOne }` reusing the *inner's* `element` (which is the underlying `T`'s declaration). **Do NOT** peel to `element`-as-connective, which would collapse `T??` to `T` instead of `T?` and contradict acceptance below. The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: From 94559a238c84e5e3e74895a5ed92459241bf4cf0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 11:09:00 -0400 Subject: [PATCH 03/10] =?UTF-8?q?docs(briefs):=20address=20PR=20#798=20BLO?= =?UTF-8?q?CKING=20=E2=80=94=20substrate-constructor=20invariant,=20not=20?= =?UTF-8?q?lower-only=20guard?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gpt-5-5-pro review correctly flagged that the lower-only guard proposed in §Q3 leaves nested Cardinality<_, AtMostOne> representable through other DAG construction paths — violating "illegal states unrepresentable" and reducing enforcement to API-level. Audit confirms a substantive blocker: infer.rs:2902-2916 (concretize_decl_with_subst) constructs Cardinality directly during generic-instantiation. Example: `fn foo(x: T?) -> T?` with `T = Int?` produces Cardinality,AtMostOne> here, never passing through lower.rs. Revision: - §TL;DR: lane is S (not XS); single substrate-level helper. - §Q3: full audit table of all hand-Rust Cardinality construction sites; helper contract at the substrate constructor; "Do NOT peel to element-as-element" anti-pattern called out per gpt-5-5-pro Q3-line:89 finding (now structural). - §Q4: reqs reframed — req 1 is the helper, req 2 is route-all-sites, req 4 adds the generic-instantiation test (the path the original lower-only design missed). New STOP for "construction path missed in audit"; absorbed gpt-5-5-pro non-blocking diagnostic-roundtrip STOP and OptionalOf-out-of-scope STOP. - Dispatch profile: S, ~30-line diff, 3 test fixtures. Co-Authored-By: Claude Opus 4.7 (1M context) --- ...iblebugs-nested-optional-flatten-design.md | 67 +++++++++++++++---- 1 file changed, 54 insertions(+), 13 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 86ecb3007d6..65302203416 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -6,7 +6,7 @@ ## TL;DR -**Recommendation: bypass-feasible.** v3 substrate already has `TypeConnective::Cardinality { element, bound: CardinalityBound }` as a first-class connective (`src/v3/compiler/src/dag.rs:395`); the cardinality-substrate gate THESIS:343 names is the **v2** state described in `docs/architecture.md:109`, and v3 is past it. `T??` parses today, lowers to nested `Cardinality { bound: AtMostOne, .. }`, and is structurally distinct from `T?` only because nothing collapses the outer wrap. A two-line guard in `lower.rs` closes the bug class without touching substrate. Implementation lane is **XS**. +**Recommendation: bypass-feasible.** v3 substrate already has `TypeConnective::Cardinality { element, bound: CardinalityBound }` as a first-class connective (`src/v3/compiler/src/dag.rs:395`); the cardinality-substrate gate THESIS:343 names is the **v2** state described in `docs/architecture.md:109`, and v3 is past it. `T??` parses today, lowers to nested `Cardinality { bound: AtMostOne, .. }`, and is structurally distinct from `T?` only because nothing collapses the outer wrap. A single substrate-level helper enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at every `Cardinality` construction site (3 hand-Rust sites: `lower.rs` ×2, `infer.rs` ×1) closes the bug class without touching substrate shape. Implementation lane is **S**. (Original draft proposed lower-only XS; revised post-PR #798 review — see §Q3 *Revision*.) ## Q1 — Surface-upstream check: does `T??` parse? @@ -77,16 +77,50 @@ No collapse step exists. The matching code path (`infer.rs:1918-1965`, `bind_exp Flattening user-surface nested-optional therefore does not touch `OptionalOf`. (If `OptionalOf>` ever appears in std method declarations as an authoring mistake, that's a separate issue scoped to `dsl/std/algebra.dag`; out of scope here.) -## Q3 — Bypass feasibility: per-construction-site flatten +## Q3 — Bypass feasibility: substrate-constructor invariant -**Yes — clean two-line guard at `SurfaceType::Optional` lowering arms.** +**Yes — single helper enforced at every `TypeConnective::Cardinality` construction site.** The algebraic property: `AtMostOne ∧ AtMostOne = AtMostOne`. In partial-function terms: `Option>` is observationally equivalent to `Option` because the cardinality semantics of `AtMostOne` is idempotent under self-composition (`min(1, min(1, n)) = min(1, n)`). This is the math of `AtMostOne`, not invented vocabulary. -**Two arms to edit** (`src/v3/compiler/src/lower.rs`): +### Revision per PR #798 review (2026-04-25) -1. `:1949-1968` — `type_to_declaration_id` `SurfaceType::Optional` arm: after lowering `inner`, check if `dag.declaration(element).connective` matches `TypeConnective::Cardinality { bound: CardinalityBound::AtMostOne, .. }`. If yes, return `element` directly without wrapping. -2. `:2044-2047` — `type_to_connective` `SurfaceType::Optional` arm: same guard. If the lowered inner declaration's connective is `TypeConnective::Cardinality { element, bound: AtMostOne }`, return/clone that connective verbatim — i.e. `TypeConnective::Cardinality { element, bound: AtMostOne }` reusing the *inner's* `element` (which is the underlying `T`'s declaration). **Do NOT** peel to `element`-as-connective, which would collapse `T??` to `T` instead of `T?` and contradict acceptance below. +The initial framing of this section proposed a lower-only guard at the two `SurfaceType::Optional` arms. **A reviewer (gpt-5-5-pro, blocking) correctly flagged that this leaves the illegal state representable through other DAG construction paths**, violating "illegal states unrepresentable" and reducing the rule to API-level enforcement. + +Audit of all hand-Rust `TypeConnective::Cardinality` construction sites confirms multiple paths: + +| File:line | Path | Hand-Rust? | +|---|---|---| +| `src/v3/compiler/src/lower.rs:1949-1968` | `type_to_declaration_id` `SurfaceType::Optional` arm | yes | +| `src/v3/compiler/src/lower.rs:2044-2047` | `type_to_connective` `SurfaceType::Optional` arm | yes | +| `src/v3/compiler/src/infer.rs:2902-2916` | `concretize_decl_with_subst` substitutes through Cardinality | **yes — killer case** | +| `src/v3/compiler/src/dag/builder.rs:920` | `push_test_declaration` (test scaffolding) | test-only | +| `src/v3/compiler/src/bootstrap_std_generated.rs` (~22 sites) | regenerated from std/ declarations | generated | + +The `infer.rs:2902` path is the substantive blocker: when `fn foo(x: T?) -> T?` is instantiated with `T = Int?`, substitution produces `Cardinality, AtMostOne>` *here*, never passing through `lower.rs`. A lower-only guard misses every generic-instantiation case. + +### Corrected design: single substrate-level helper + +Introduce one helper in `src/v3/compiler/src/dag/builder.rs` (or adjacent — implementer's call) with this contract: + +```rust +/// Allocate a Cardinality declaration enforcing the AtMostOne∧AtMostOne +/// idempotence invariant. If `bound == AtMostOne` and `element`'s +/// connective is `Cardinality { bound: AtMostOne, .. }`, return `element` +/// directly without allocating a fresh outer wrap. +fn alloc_cardinality_decl( + dag: &mut Dag, + element: DeclarationId, + bound: CardinalityBound, + span: SourceSpan, +) -> DeclarationId +``` + +All three hand-Rust construction sites (`lower.rs:1949`, `lower.rs:2044`, `infer.rs:2902`) route through this helper. The helper is the **single point of enforcement**; nested `AtMostOne ∧ AtMostOne` literally cannot be constructed, satisfying "illegal states unrepresentable" structurally rather than by-convention. + +`bootstrap_std_generated.rs` sites are regenerated from `dsl/std/` declarations; `dsl/std/` does not author user-surface `T??`, so those sites are not at risk *today*, but the regen path should also call the helper as a defense-in-depth measure (the regen emitter sits in `regen_bootstrap_emit.rs` — implementer audits whether the helper-call needs to be wired through codegen). If the helper lives in a module that codegen can import, the regen output naturally inherits the invariant. + +The `:2044` arm is `type_to_connective`, which returns `TypeConnective` directly (not a `DeclarationId`). The helper's contract returns `DeclarationId`; for `:2044`, the implementer either (a) restructures the caller to use the helper-then-resolve-to-connective path, or (b) extracts a sibling helper `cardinality_connective(dag, element, bound) -> TypeConnective` that applies the same predicate inline. Either is acceptable; both must converge on the same idempotence rule. The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: @@ -105,22 +139,29 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos ### Implementation-brief shape -**Title:** `feat(v3): T-ImpossibleBugs — `T??` flattens to `T?` at lower (closes nested-optional flatten class)` +**Title:** `feat(v3): T-ImpossibleBugs — `T??` flattens to `T?` via Cardinality-constructor invariant (closes nested-optional flatten class)` **Reqs:** -1. **Idempotent flatten in lower.** `SurfaceType::Optional` lowering arms in `src/v3/compiler/src/lower.rs:1949` and `:2044` add a guard: when the lowered inner element's connective is `TypeConnective::Cardinality { bound: AtMostOne, .. }`, return the inner element directly without constructing an outer wrap. Specific to `AtMostOne ∧ AtMostOne`; other bound combinations untouched. -2. **Span policy.** The flattened declaration uses the inner declaration's existing span (the user wrote `T??` syntactically; the type they got is structurally the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at lower. Document this in PR body. -3. **Test fixture.** A v3 compiler test asserting `T??` and `T?` produce the same `DeclarationId` (or the same `TypeConnective` shape modulo declaration identity); pattern-matching against `T??` requires only one level of unwrap. Place under `src/v3/compiler/tests/integration/`. +1. **Substrate-level idempotence helper.** Add `alloc_cardinality_decl` (or equivalent) in `src/v3/compiler/src/dag/builder.rs` enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at allocation time. When `bound == AtMostOne` and `element`'s connective is `Cardinality { bound: AtMostOne, .. }`, return `element` directly without allocating a fresh outer wrap. Specific to `AtMostOne ∧ AtMostOne`; `Unbounded`, `Exact(n)`, and mixed-bound combinations untouched. **Do NOT** peel to `element`-as-element (would collapse `T??` to `T` instead of `T?` and contradict acceptance below) — the helper returns the existing inner *declaration* (its connective is already `Cardinality`), not its element-of-element. +2. **Route all hand-Rust construction sites through the helper.** `lower.rs:1949` and `infer.rs:2902` call the new helper instead of constructing `TypeConnective::Cardinality { ... }` and pushing a declaration directly. `lower.rs:2044` (`type_to_connective` returns `TypeConnective` not `DeclarationId`) gets a sibling helper or restructured caller per §Q3. +3. **Span policy.** When flatten triggers, reuse the inner declaration's span (the user wrote `T??`; the type they got is the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at the substrate constructor. Verify no diagnostic / hover / error-printer round-trips `T??` back to the user as `T?` confusingly (per gpt-5-5-pro non-blocking observation on PR #798). +4. **Test fixtures.** + - `T??` and `T?` produce the same `DeclarationId` after lowering (test). + - Generic-instantiation case: `fn foo(x: T?) -> T?` instantiated with `T = Int?` produces a `Cardinality` return type, **not** `Cardinality, AtMostOne>` (test that exercises `concretize_decl_with_subst`; this is the path the original lower-only design missed). + - `List?`, `T?[]`, `[T; 3]?` preserve their distinct shapes (test). + - Place under `src/v3/compiler/tests/integration/`. **STOPs:** - **Any consumer matches on outer-`AtMostOne` over inner-`AtMostOne` as a meaningful distinct type** (audit `infer.rs` `Cardinality` arms before editing) — if so, that consumer carries a hidden assumption that flatten breaks. STOP and surface. -- **Lowering arm has a hidden caller path that needs the outer wrap for span/identity reasons** — STOP. -- **Generalization pressure to flatten `List>` or `Set>` falls out of the same guard** — it does not (those are `Unbounded ∧ Unbounded`, not idempotent in the same algebraic sense; they're legitimately distinct). STOP if the implementer is tempted. +- **A construction path was missed in the audit** — if `cargo test` reveals nested `Cardinality<_, AtMostOne>` produced by a path other than the three hand-Rust sites named, STOP and audit before extending the helper rollout. +- **Diagnostic/hover/error-printer surface confuses the user** — if any user-facing surface re-prints types and round-trips `T??` ambiguously, STOP and surface (per gpt-5-5-pro observation). +- **Generalization pressure to flatten `List>` or `Set>` falls out of the same helper** — it does not (those are `Unbounded ∧ Unbounded`, not idempotent in the same algebraic sense; they're legitimately distinct). The helper's predicate is exactly `outer == AtMostOne && inner == AtMostOne`. STOP if the implementer is tempted to widen. +- **`OptionalOf>` in std-method authoring** is a separate brief (algebra-template lint), not in scope here. STOP if the implementer is tempted to fold it in. - **DB-8 fixed-point drifts** — STOP immediately. -**Dispatch profile:** XS, single PR, single worker. ~10-line code diff + 1 test fixture + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. +**Dispatch profile:** S (revised from XS post-#798 review). Single PR, single worker. ~30-line code diff (helper + 2-3 routed call sites + sibling for `:2044` arm) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. **Acceptance:** From 28336e7886cf24ffb6907f5ffaaaa9435912bad7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 11:39:47 -0400 Subject: [PATCH 04/10] =?UTF-8?q?docs(briefs):=20address=20PR=20#798=20BLO?= =?UTF-8?q?CKING=20=E2=80=94=20single=20predicate,=20no=20sibling=20helper?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review at sha 30eb14ce flagged §Q3 line :123 as a parallel- authority violation: the prior wording permitted a sibling helper applying the same AtMostOne∧AtMostOne predicate inline, immediately after claiming single point of enforcement. That leaves two authorities for one substrate invariant — INVARIANTS.md P2 Boundary Discipline violation. Tightened §Q3: - Mandate ONE shared predicate (`cardinality_idempotent_target`) consumed by both `alloc_cardinality_decl` (DeclarationId path) and the `lower.rs:2044` `type_to_connective` caller. - Explicit "no sibling helper" requirement; if the return-type shape of `type_to_connective` makes factoring awkward, restructure the caller through `alloc_cardinality_decl` rather than introducing a second authority. Q4 req 2 and dispatch-profile updated to match. Co-Authored-By: Claude Opus 4.7 (1M context) --- ...t-impossiblebugs-nested-optional-flatten-design.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 65302203416..669c85fa5a4 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -120,7 +120,12 @@ All three hand-Rust construction sites (`lower.rs:1949`, `lower.rs:2044`, `infer `bootstrap_std_generated.rs` sites are regenerated from `dsl/std/` declarations; `dsl/std/` does not author user-surface `T??`, so those sites are not at risk *today*, but the regen path should also call the helper as a defense-in-depth measure (the regen emitter sits in `regen_bootstrap_emit.rs` — implementer audits whether the helper-call needs to be wired through codegen). If the helper lives in a module that codegen can import, the regen output naturally inherits the invariant. -The `:2044` arm is `type_to_connective`, which returns `TypeConnective` directly (not a `DeclarationId`). The helper's contract returns `DeclarationId`; for `:2044`, the implementer either (a) restructures the caller to use the helper-then-resolve-to-connective path, or (b) extracts a sibling helper `cardinality_connective(dag, element, bound) -> TypeConnective` that applies the same predicate inline. Either is acceptable; both must converge on the same idempotence rule. +The `:2044` arm is `type_to_connective`, which returns `TypeConnective` directly (not a `DeclarationId`). To preserve single-authority enforcement, factor the idempotence rule into **one shared predicate** (e.g. `cardinality_idempotent_target(dag, element, bound) -> Option` returning `Some(inner)` when the rule fires and `None` otherwise). Both call sites consume this predicate: + +- `alloc_cardinality_decl` (the `DeclarationId`-returning helper) calls the predicate and short-circuits to the inner declaration when it fires; otherwise allocates a fresh declaration. +- The `:2044` `type_to_connective` caller calls the predicate too: when it fires, the caller's enclosing context (`type_to_declaration_id` allocates a declaration around the connective the arm returns) gets the inner declaration's connective by reading `dag.declaration(inner).connective`; when it doesn't fire, the caller emits the literal `TypeConnective::Cardinality { element, bound: AtMostOne }`. + +**Single-authority requirement (per PR #798 Codex review):** the rule MUST be implemented in exactly one place — the predicate. No sibling helper that re-applies the predicate inline. A second authority for the same substrate invariant violates INVARIANTS.md P2 Boundary Discipline. The implementer's task is to factor the predicate so both call sites are pure consumers; if `type_to_connective`'s return type makes a clean factoring awkward, restructure the caller (lower.rs:2044's caller wraps the result in a fresh declaration anyway — route that wrap-and-allocate path through `alloc_cardinality_decl` instead). The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: @@ -144,7 +149,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos **Reqs:** 1. **Substrate-level idempotence helper.** Add `alloc_cardinality_decl` (or equivalent) in `src/v3/compiler/src/dag/builder.rs` enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at allocation time. When `bound == AtMostOne` and `element`'s connective is `Cardinality { bound: AtMostOne, .. }`, return `element` directly without allocating a fresh outer wrap. Specific to `AtMostOne ∧ AtMostOne`; `Unbounded`, `Exact(n)`, and mixed-bound combinations untouched. **Do NOT** peel to `element`-as-element (would collapse `T??` to `T` instead of `T?` and contradict acceptance below) — the helper returns the existing inner *declaration* (its connective is already `Cardinality`), not its element-of-element. -2. **Route all hand-Rust construction sites through the helper.** `lower.rs:1949` and `infer.rs:2902` call the new helper instead of constructing `TypeConnective::Cardinality { ... }` and pushing a declaration directly. `lower.rs:2044` (`type_to_connective` returns `TypeConnective` not `DeclarationId`) gets a sibling helper or restructured caller per §Q3. +2. **Route all hand-Rust construction sites through one shared predicate.** `lower.rs:1949` and `infer.rs:2902` call `alloc_cardinality_decl`. `lower.rs:2044` (`type_to_connective`) consumes the same `cardinality_idempotent_target` predicate per §Q3 — **no sibling helper** that re-applies the rule inline. Single authority for the substrate invariant; both call sites are pure consumers of the predicate. 3. **Span policy.** When flatten triggers, reuse the inner declaration's span (the user wrote `T??`; the type they got is the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at the substrate constructor. Verify no diagnostic / hover / error-printer round-trips `T??` back to the user as `T?` confusingly (per gpt-5-5-pro non-blocking observation on PR #798). 4. **Test fixtures.** - `T??` and `T?` produce the same `DeclarationId` after lowering (test). @@ -161,7 +166,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos - **`OptionalOf>` in std-method authoring** is a separate brief (algebra-template lint), not in scope here. STOP if the implementer is tempted to fold it in. - **DB-8 fixed-point drifts** — STOP immediately. -**Dispatch profile:** S (revised from XS post-#798 review). Single PR, single worker. ~30-line code diff (helper + 2-3 routed call sites + sibling for `:2044` arm) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. +**Dispatch profile:** S (revised from XS post-#798 review). Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 3 routed call sites consuming the predicate) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. **Acceptance:** From efa02ac7dd7fa6b16ebed31f4a2a2326f90156c7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 12:12:06 -0400 Subject: [PATCH 05/10] WIP: nested optional --- docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 669c85fa5a4..746bae1e402 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -166,7 +166,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos - **`OptionalOf>` in std-method authoring** is a separate brief (algebra-template lint), not in scope here. STOP if the implementer is tempted to fold it in. - **DB-8 fixed-point drifts** — STOP immediately. -**Dispatch profile:** S (revised from XS post-#798 review). Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 3 routed call sites consuming the predicate) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. +**Dispatch profile:** S. Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 3 routed call sites consuming the predicate) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. **Acceptance:** From 9af32f3e5336121425bd2c09b89683942939cff2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 12:17:28 -0400 Subject: [PATCH 06/10] =?UTF-8?q?docs(briefs):=20address=20PR=20#798=20BLO?= =?UTF-8?q?CKING=20=E2=80=94=20shape=20assertion,=20not=20DeclarationId=20?= =?UTF-8?q?equality?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review at sha efa02ac7 flagged §Q4 req-4 sub-bullet :155: asserting `T??` and `T?` produce the same DeclarationId pins allocation identity, not behavior. The proposed helper returns the inner declaration created while lowering T??; an independently lowered T? is a different anonymous declaration with the same shape. DeclarationId equality requires interning machinery the helper neither has nor should require, and would force a correct implementation to fail. Violates TESTING.md behavior-driven discipline. Fix: assert shape — no nested Cardinality<_, AtMostOne> in the lowered result, via structural walk. Same change applied to the acceptance bullet at :173. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../t-impossiblebugs-nested-optional-flatten-design.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 746bae1e402..8198edb8830 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -152,8 +152,8 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos 2. **Route all hand-Rust construction sites through one shared predicate.** `lower.rs:1949` and `infer.rs:2902` call `alloc_cardinality_decl`. `lower.rs:2044` (`type_to_connective`) consumes the same `cardinality_idempotent_target` predicate per §Q3 — **no sibling helper** that re-applies the rule inline. Single authority for the substrate invariant; both call sites are pure consumers of the predicate. 3. **Span policy.** When flatten triggers, reuse the inner declaration's span (the user wrote `T??`; the type they got is the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at the substrate constructor. Verify no diagnostic / hover / error-printer round-trips `T??` back to the user as `T?` confusingly (per gpt-5-5-pro non-blocking observation on PR #798). 4. **Test fixtures.** - - `T??` and `T?` produce the same `DeclarationId` after lowering (test). - - Generic-instantiation case: `fn foo(x: T?) -> T?` instantiated with `T = Int?` produces a `Cardinality` return type, **not** `Cardinality, AtMostOne>` (test that exercises `concretize_decl_with_subst`; this is the path the original lower-only design missed). + - **Shape assertion (not identity).** `T??` lowered shape contains no nested `Cardinality { bound: AtMostOne, .. }` whose `element`'s connective is also `Cardinality { bound: AtMostOne, .. }` — i.e. a single `AtMostOne` wrap around the underlying type, equivalent to `T?`'s shape. Assert via structural walk over the resulting declaration, **not** raw `DeclarationId` equality with an independently lowered `T?` (declaration identity is an interning concern; the invariant is shape, per `TESTING.md` behavior-driven discipline). + - Generic-instantiation case: `fn foo(x: T?) -> T?` instantiated with `T = Int?` produces a return-type shape with one `AtMostOne` wrap around `Int`, **not** two nested `AtMostOne` wraps (test that exercises `concretize_decl_with_subst`; this is the path the original lower-only design missed). Same shape-level assertion, not `DeclarationId`-level. - `List?`, `T?[]`, `[T; 3]?` preserve their distinct shapes (test). - Place under `src/v3/compiler/tests/integration/`. @@ -170,7 +170,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos **Acceptance:** -- `T??` and `T?` produce the same lowered shape (test). +- `T??` lowers to a shape with no nested `Cardinality<_, AtMostOne>` (test; structural walk, not `DeclarationId` equality). - `List?`, `T?[]`, `[T; 3]?` all preserve their distinct shapes (test). - `cargo test --workspace --exclude v2-compiler-tests` clean. - `cargo test -p v2-compiler-tests` clean. From f7d8d7e1cc6adaa3f51300033aa8b17f76d57374 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 12:37:23 -0400 Subject: [PATCH 07/10] =?UTF-8?q?docs(briefs):=20resolve=20XS/S=20inconsis?= =?UTF-8?q?tency=20=E2=80=94=20single=20authority=20on=20lane=20size=20=3D?= =?UTF-8?q?=20S?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review at sha 2c5a98a0 (NON-BLOCKING) flagged §Q4:143 saying 'XS, not S' while §Dispatch profile:169 says 'S' — two authorities for the same execution metadata, INVARIANTS.md P2 violation. Fix: §Q4 outcome and §why-not-park both reference 'S' as the live lane size, citing §Dispatch profile as authority. Remaining 'XS' mentions are explicit revision-history references (TL;DR and §Q4 outcome) marked 'original draft', not active claims. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../briefs/t-impossiblebugs-nested-optional-flatten-design.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 8198edb8830..d585ae6cbf2 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -140,7 +140,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos ## Q4 — Recommendation: bypass implementation brief shape -**Outcome: (a) bypass-feasible.** Director can fast-track an implementation brief (XS, not S). +**Outcome: (a) bypass-feasible.** Director can fast-track an implementation brief at lane size **S** (see §Dispatch profile below; original draft sized XS based on a lower-only design that PR #798 review correctly rejected). ### Implementation-brief shape @@ -185,7 +185,7 @@ The cardinality substrate THESIS:343 names as the gate is the **v2** state (`ret ### Why not "park" -The bypass is small (XS), well-scoped (specific to `AtMostOne ∧ AtMostOne`), structurally grounded (algebraic idempotence of `AtMostOne`), and the substrate prerequisite is already met. Parking would be conservative beyond what the evidence supports. +The bypass is small (S; see §Dispatch profile), well-scoped (specific to `AtMostOne ∧ AtMostOne`), structurally grounded (algebraic idempotence of `AtMostOne`), and the substrate prerequisite is already met. Parking would be conservative beyond what the evidence supports. ## Cross-manager note From eded728c4a7eee6c6def769f54b87c171a06704b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 12:45:06 -0400 Subject: [PATCH 08/10] WIP: nested optional --- ...iblebugs-nested-optional-flatten-design.md | 49 +++++++++++-------- 1 file changed, 28 insertions(+), 21 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index d585ae6cbf2..a29b42d31c7 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -99,33 +99,40 @@ Audit of all hand-Rust `TypeConnective::Cardinality` construction sites confirms The `infer.rs:2902` path is the substantive blocker: when `fn foo(x: T?) -> T?` is instantiated with `T = Int?`, substitution produces `Cardinality, AtMostOne>` *here*, never passing through `lower.rs`. A lower-only guard misses every generic-instantiation case. -### Corrected design: single substrate-level helper +### Corrected design: single substrate-level helper (canonical sketch) -Introduce one helper in `src/v3/compiler/src/dag/builder.rs` (or adjacent — implementer's call) with this contract: +Introduce one helper in `src/v3/compiler/src/dag/builder.rs` (or adjacent — implementer's call) enforcing the rule at allocation, plus one predicate that owns the rule itself. All construction paths — including the codegen emitter for `bootstrap_std_generated.rs` (~22 sites) — route through the helper. Nested `AtMostOne ∧ AtMostOne` literally cannot be constructed, satisfying "illegal states unrepresentable" structurally rather than by-convention. + +One predicate, one allocator helper, three (+ codegen) call sites: ```rust -/// Allocate a Cardinality declaration enforcing the AtMostOne∧AtMostOne -/// idempotence invariant. If `bound == AtMostOne` and `element`'s -/// connective is `Cardinality { bound: AtMostOne, .. }`, return `element` -/// directly without allocating a fresh outer wrap. +// The predicate. The ONLY place the AtMostOne∧AtMostOne rule lives. +fn cardinality_idempotent_target( + dag: &Dag, element: DeclarationId, bound: CardinalityBound, +) -> Option; +// Returns Some(inner_decl) when the rule fires (outer == AtMostOne AND +// element's connective is Cardinality { bound: AtMostOne, .. }); else None. + +// The allocator. Single substrate-constructor authority for Cardinality +// declarations. fn alloc_cardinality_decl( - dag: &mut Dag, - element: DeclarationId, - bound: CardinalityBound, - span: SourceSpan, -) -> DeclarationId + dag: &mut Dag, element: DeclarationId, bound: CardinalityBound, span: SourceSpan, +) -> DeclarationId { + if let Some(inner) = cardinality_idempotent_target(dag, element, bound) { + return inner; + } + // ... allocate fresh declaration with TypeConnective::Cardinality { element, bound } +} ``` -All three hand-Rust construction sites (`lower.rs:1949`, `lower.rs:2044`, `infer.rs:2902`) route through this helper. The helper is the **single point of enforcement**; nested `AtMostOne ∧ AtMostOne` literally cannot be constructed, satisfying "illegal states unrepresentable" structurally rather than by-convention. - -`bootstrap_std_generated.rs` sites are regenerated from `dsl/std/` declarations; `dsl/std/` does not author user-surface `T??`, so those sites are not at risk *today*, but the regen path should also call the helper as a defense-in-depth measure (the regen emitter sits in `regen_bootstrap_emit.rs` — implementer audits whether the helper-call needs to be wired through codegen). If the helper lives in a module that codegen can import, the regen output naturally inherits the invariant. - -The `:2044` arm is `type_to_connective`, which returns `TypeConnective` directly (not a `DeclarationId`). To preserve single-authority enforcement, factor the idempotence rule into **one shared predicate** (e.g. `cardinality_idempotent_target(dag, element, bound) -> Option` returning `Some(inner)` when the rule fires and `None` otherwise). Both call sites consume this predicate: +**All call sites consume `alloc_cardinality_decl`** (not the predicate directly, not literal `TypeConnective::Cardinality { ... }`): -- `alloc_cardinality_decl` (the `DeclarationId`-returning helper) calls the predicate and short-circuits to the inner declaration when it fires; otherwise allocates a fresh declaration. -- The `:2044` `type_to_connective` caller calls the predicate too: when it fires, the caller's enclosing context (`type_to_declaration_id` allocates a declaration around the connective the arm returns) gets the inner declaration's connective by reading `dag.declaration(inner).connective`; when it doesn't fire, the caller emits the literal `TypeConnective::Cardinality { element, bound: AtMostOne }`. +- `lower.rs:1949` (`type_to_declaration_id` Optional arm) — direct call, returns `DeclarationId`. +- `lower.rs:2044` (`type_to_connective` Optional arm) — restructure the caller (`type_to_declaration_id`'s enclosing wrap-and-allocate) to call `alloc_cardinality_decl` instead of constructing a `TypeConnective::Cardinality` and pushing a declaration around it. The `:2044` arm's literal connective construction is the path of last resort and is replaced. +- `infer.rs:2902` (`concretize_decl_with_subst`) — direct call, returns `DeclarationId`. +- `regen_bootstrap_emit.rs` (codegen for `bootstrap_std_generated.rs`) — emit calls to `alloc_cardinality_decl` instead of literal `TypeConnective::Cardinality { ... }` struct-init in regen output. -**Single-authority requirement (per PR #798 Codex review):** the rule MUST be implemented in exactly one place — the predicate. No sibling helper that re-applies the predicate inline. A second authority for the same substrate invariant violates INVARIANTS.md P2 Boundary Discipline. The implementer's task is to factor the predicate so both call sites are pure consumers; if `type_to_connective`'s return type makes a clean factoring awkward, restructure the caller (lower.rs:2044's caller wraps the result in a fresh declaration anyway — route that wrap-and-allocate path through `alloc_cardinality_decl` instead). +**Single-authority requirement (per PR #798 Codex review):** the rule lives in exactly one place — `cardinality_idempotent_target`. No sibling helper that re-applies the rule. No literal `TypeConnective::Cardinality` construction outside `alloc_cardinality_decl`'s body. A second authority violates INVARIANTS.md P2 Boundary Discipline. The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: @@ -149,7 +156,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos **Reqs:** 1. **Substrate-level idempotence helper.** Add `alloc_cardinality_decl` (or equivalent) in `src/v3/compiler/src/dag/builder.rs` enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at allocation time. When `bound == AtMostOne` and `element`'s connective is `Cardinality { bound: AtMostOne, .. }`, return `element` directly without allocating a fresh outer wrap. Specific to `AtMostOne ∧ AtMostOne`; `Unbounded`, `Exact(n)`, and mixed-bound combinations untouched. **Do NOT** peel to `element`-as-element (would collapse `T??` to `T` instead of `T?` and contradict acceptance below) — the helper returns the existing inner *declaration* (its connective is already `Cardinality`), not its element-of-element. -2. **Route all hand-Rust construction sites through one shared predicate.** `lower.rs:1949` and `infer.rs:2902` call `alloc_cardinality_decl`. `lower.rs:2044` (`type_to_connective`) consumes the same `cardinality_idempotent_target` predicate per §Q3 — **no sibling helper** that re-applies the rule inline. Single authority for the substrate invariant; both call sites are pure consumers of the predicate. +2. **Route ALL Cardinality construction paths through `alloc_cardinality_decl`** per the §Q3 canonical sketch: `lower.rs:1949`, `lower.rs:2044` (via caller restructure), `infer.rs:2902`, and `regen_bootstrap_emit.rs` (codegen emits helper calls, not literal `TypeConnective::Cardinality { ... }` struct-init in `bootstrap_std_generated.rs`). The rule lives only in `cardinality_idempotent_target`. **No sibling helper. No literal `TypeConnective::Cardinality` construction outside `alloc_cardinality_decl`'s body** (including in regen output). Single authority for the substrate invariant. 3. **Span policy.** When flatten triggers, reuse the inner declaration's span (the user wrote `T??`; the type they got is the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at the substrate constructor. Verify no diagnostic / hover / error-printer round-trips `T??` back to the user as `T?` confusingly (per gpt-5-5-pro non-blocking observation on PR #798). 4. **Test fixtures.** - **Shape assertion (not identity).** `T??` lowered shape contains no nested `Cardinality { bound: AtMostOne, .. }` whose `element`'s connective is also `Cardinality { bound: AtMostOne, .. }` — i.e. a single `AtMostOne` wrap around the underlying type, equivalent to `T?`'s shape. Assert via structural walk over the resulting declaration, **not** raw `DeclarationId` equality with an independently lowered `T?` (declaration identity is an interning concern; the invariant is shape, per `TESTING.md` behavior-driven discipline). @@ -166,7 +173,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos - **`OptionalOf>` in std-method authoring** is a separate brief (algebra-template lint), not in scope here. STOP if the implementer is tempted to fold it in. - **DB-8 fixed-point drifts** — STOP immediately. -**Dispatch profile:** S. Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 3 routed call sites consuming the predicate) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. +**Dispatch profile:** S. Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 4 routed paths consuming it: `lower.rs:1949`, `lower.rs:2044` via caller restructure, `infer.rs:2902`, and `regen_bootstrap_emit.rs` codegen) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. **Acceptance:** From 3cce220ff924d932a81e39459041ede2f1ec885b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 12:57:58 -0400 Subject: [PATCH 09/10] =?UTF-8?q?docs(briefs):=20address=20PR=20#798=20BLO?= =?UTF-8?q?CKING=20=E2=80=94=20mechanical=20API=20closure,=20not=20by-conv?= =?UTF-8?q?ention?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex review at sha eded728c correctly flagged that "all callers route through alloc_cardinality_decl" is convention-level — a future caller can still write literal TypeConnective::Cardinality {...} directly. Per modeling-discipline practice 6 (API-level enforcement over convention), the substrate invariant must be mechanically enforced. Updates: - §Q3 adds new "API closure: mechanical, not conventional" section spec'ing the refactor of TypeConnective::Cardinality's payload to a module-private CardinalityPayload struct whose constructor (pub(super) fn new) is reachable only from the module owning alloc_cardinality_decl. The variant becomes *mechanically* unconstructible outside the allocator — no caller, present or future, can bypass the predicate. - Pattern-match destructure stays public via accessor methods. - TL;DR + Q4 outcome + Q4 req 1 + dispatch profile updated to reflect API closure as part of req 1, not a follow-up. - Lane re-sized S → M: ~30 destructure sites need migration to accessor-style. Director-call flagged if M is too large; the bounded-scaffold-with-dissolution alternative is named but explicitly rejected as contradicting practice 6 and feedback_construction_over_ratchets. Co-Authored-By: Claude Opus 4.7 (1M context) --- ...iblebugs-nested-optional-flatten-design.md | 57 +++++++++++++++++-- 1 file changed, 52 insertions(+), 5 deletions(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index a29b42d31c7..0f98397f2e2 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -6,7 +6,7 @@ ## TL;DR -**Recommendation: bypass-feasible.** v3 substrate already has `TypeConnective::Cardinality { element, bound: CardinalityBound }` as a first-class connective (`src/v3/compiler/src/dag.rs:395`); the cardinality-substrate gate THESIS:343 names is the **v2** state described in `docs/architecture.md:109`, and v3 is past it. `T??` parses today, lowers to nested `Cardinality { bound: AtMostOne, .. }`, and is structurally distinct from `T?` only because nothing collapses the outer wrap. A single substrate-level helper enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at every `Cardinality` construction site (3 hand-Rust sites: `lower.rs` ×2, `infer.rs` ×1) closes the bug class without touching substrate shape. Implementation lane is **S**. (Original draft proposed lower-only XS; revised post-PR #798 review — see §Q3 *Revision*.) +**Recommendation: bypass-feasible.** v3 substrate already has `TypeConnective::Cardinality { element, bound: CardinalityBound }` as a first-class connective (`src/v3/compiler/src/dag.rs:395`); the cardinality-substrate gate THESIS:343 names is the **v2** state described in `docs/architecture.md:109`, and v3 is past it. `T??` parses today, lowers to nested `Cardinality { bound: AtMostOne, .. }`, and is structurally distinct from `T?` only because nothing collapses the outer wrap. The fix is (a) one predicate `cardinality_idempotent_target` owning the `AtMostOne ∧ AtMostOne` rule, (b) one allocator `alloc_cardinality_decl` that consults it, and **(c) API closure on `TypeConnective::Cardinality`'s payload** so the variant cannot be constructed outside the allocator — mechanical enforcement of "illegal states unrepresentable," not by-convention. Implementation lane is **M** (revised from S after API-closure requirement landed; see §Q3 *API closure*). (Original draft proposed lower-only XS, then constructor-helper-by-convention S; revised post-PR #798 review — see §Q3 *Revision*.) ## Q1 — Surface-upstream check: does `T??` parse? @@ -132,7 +132,54 @@ fn alloc_cardinality_decl( - `infer.rs:2902` (`concretize_decl_with_subst`) — direct call, returns `DeclarationId`. - `regen_bootstrap_emit.rs` (codegen for `bootstrap_std_generated.rs`) — emit calls to `alloc_cardinality_decl` instead of literal `TypeConnective::Cardinality { ... }` struct-init in regen output. -**Single-authority requirement (per PR #798 Codex review):** the rule lives in exactly one place — `cardinality_idempotent_target`. No sibling helper that re-applies the rule. No literal `TypeConnective::Cardinality` construction outside `alloc_cardinality_decl`'s body. A second authority violates INVARIANTS.md P2 Boundary Discipline. +**Single-authority requirement (per PR #798 Codex review #1):** the rule lives in exactly one place — `cardinality_idempotent_target`. No sibling helper that re-applies the rule. No literal `TypeConnective::Cardinality` construction outside `alloc_cardinality_decl`'s body. A second authority violates INVARIANTS.md P2 Boundary Discipline. + +### API closure: mechanical, not conventional (per PR #798 Codex review #2) + +A second Codex review correctly flagged that "all call sites consume `alloc_cardinality_decl`" is **convention-level** — a future caller can still write literal `TypeConnective::Cardinality { element, bound }` directly. Per `docs/modeling-discipline.md` practice 6 (API-level enforcement over convention), the substrate invariant must be mechanically enforced: the constructor API must be closed so the variant **cannot be constructed** outside `alloc_cardinality_decl`. + +Concretely, in Rust this means refactoring `TypeConnective::Cardinality`'s payload from a struct-variant with public fields: + +```rust +// BEFORE — payload is publicly constructible anywhere TypeConnective is in scope. +enum TypeConnective { + Cardinality { element: DeclarationId, bound: CardinalityBound }, + ... +} +``` + +…to a tuple-variant carrying a payload struct whose constructor is module-private: + +```rust +// AFTER — payload's only constructor is `pub(super) fn new` reachable +// only from the module that owns alloc_cardinality_decl. Callers outside +// the module CANNOT construct CardinalityPayload, therefore CANNOT +// construct TypeConnective::Cardinality. Pattern-matching destructure +// stays public via accessor methods. +mod cardinality_payload { + pub struct CardinalityPayload { + element: DeclarationId, + bound: CardinalityBound, + } + impl CardinalityPayload { + pub(super) fn new(element: DeclarationId, bound: CardinalityBound) -> Self { + Self { element, bound } + } + pub fn element(&self) -> DeclarationId { self.element } + pub fn bound(&self) -> &CardinalityBound { &self.bound } + } +} +enum TypeConnective { + Cardinality(CardinalityPayload), + ... +} +``` + +`alloc_cardinality_decl` becomes the **only** function that calls `CardinalityPayload::new`. Nested `AtMostOne ∧ AtMostOne` is then mechanically unrepresentable — no caller, present or future, can bypass the predicate. This is "illegal states unrepresentable" by type-system enforcement, not by-convention/by-review. + +**Scope impact:** every existing destructure of `TypeConnective::Cardinality { element, bound }` (currently struct-variant style, ~30 sites grepped) becomes `TypeConnective::Cardinality(p) => { let element = p.element(); let bound = p.bound(); ... }` or equivalent. Mechanical, but pervasive. + +**Lane re-size:** API closure bumps the lane from S → M (~30-line core diff plus pattern-match migration across the compiler). The reviewer offered an alternative — keep the public-literal surface bounded with a dissolution trigger — but this contradicts modeling-discipline practice 6 and `feedback_construction_over_ratchets` (model first; violations dissolve). The recommendation is mechanical closure (M lane), not bounded scaffold. **Director-call** if M is too large for this slot — explicitly noted, not deferred to implementer. The guard is **specific to AtMostOne ∧ AtMostOne**. The other shapes are not idempotent and stay distinct: @@ -147,7 +194,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos ## Q4 — Recommendation: bypass implementation brief shape -**Outcome: (a) bypass-feasible.** Director can fast-track an implementation brief at lane size **S** (see §Dispatch profile below; original draft sized XS based on a lower-only design that PR #798 review correctly rejected). +**Outcome: (a) bypass-feasible.** Director authors an implementation brief at lane size **M** (see §Dispatch profile below; sized to include API closure per §Q3 *API closure*. Earlier drafts sized XS / S correspond to rejected designs — lower-only sugar and helper-by-convention respectively). ### Implementation-brief shape @@ -155,7 +202,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos **Reqs:** -1. **Substrate-level idempotence helper.** Add `alloc_cardinality_decl` (or equivalent) in `src/v3/compiler/src/dag/builder.rs` enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at allocation time. When `bound == AtMostOne` and `element`'s connective is `Cardinality { bound: AtMostOne, .. }`, return `element` directly without allocating a fresh outer wrap. Specific to `AtMostOne ∧ AtMostOne`; `Unbounded`, `Exact(n)`, and mixed-bound combinations untouched. **Do NOT** peel to `element`-as-element (would collapse `T??` to `T` instead of `T?` and contradict acceptance below) — the helper returns the existing inner *declaration* (its connective is already `Cardinality`), not its element-of-element. +1. **Substrate-level idempotence helper + API closure.** Add `alloc_cardinality_decl` (or equivalent) in `src/v3/compiler/src/dag/builder.rs` enforcing `AtMostOne ∧ AtMostOne = AtMostOne` at allocation time. When `bound == AtMostOne` and `element`'s connective is `Cardinality { bound: AtMostOne, .. }`, return `element` directly without allocating a fresh outer wrap. Specific to `AtMostOne ∧ AtMostOne`; `Unbounded`, `Exact(n)`, and mixed-bound combinations untouched. **Do NOT** peel to `element`-as-element (would collapse `T??` to `T` instead of `T?` and contradict acceptance below) — the helper returns the existing inner *declaration* (its connective is already `Cardinality`), not its element-of-element. **Additionally close the `TypeConnective::Cardinality` constructor API** per §Q3 *API closure* — refactor the payload to a module-private struct so the variant cannot be constructed outside `alloc_cardinality_decl`. Pattern-match destructure stays public via accessor methods on the payload. 2. **Route ALL Cardinality construction paths through `alloc_cardinality_decl`** per the §Q3 canonical sketch: `lower.rs:1949`, `lower.rs:2044` (via caller restructure), `infer.rs:2902`, and `regen_bootstrap_emit.rs` (codegen emits helper calls, not literal `TypeConnective::Cardinality { ... }` struct-init in `bootstrap_std_generated.rs`). The rule lives only in `cardinality_idempotent_target`. **No sibling helper. No literal `TypeConnective::Cardinality` construction outside `alloc_cardinality_decl`'s body** (including in regen output). Single authority for the substrate invariant. 3. **Span policy.** When flatten triggers, reuse the inner declaration's span (the user wrote `T??`; the type they got is the inner `T?`'s declaration). No info-level "flattened to" hint — *"impossible by construction"* per discipline; the second `?` is silently absorbed at the substrate constructor. Verify no diagnostic / hover / error-printer round-trips `T??` back to the user as `T?` confusingly (per gpt-5-5-pro non-blocking observation on PR #798). 4. **Test fixtures.** @@ -173,7 +220,7 @@ The guard predicate is exactly: outer bound `AtMostOne` *and* inner bound `AtMos - **`OptionalOf>` in std-method authoring** is a separate brief (algebra-template lint), not in scope here. STOP if the implementer is tempted to fold it in. - **DB-8 fixed-point drifts** — STOP immediately. -**Dispatch profile:** S. Single PR, single worker. ~30-line code diff (one predicate + `alloc_cardinality_decl` helper + 4 routed paths consuming it: `lower.rs:1949`, `lower.rs:2044` via caller restructure, `infer.rs:2902`, and `regen_bootstrap_emit.rs` codegen) + 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. +**Dispatch profile:** M. Single PR, single worker. Core diff: one predicate + `alloc_cardinality_decl` helper + `CardinalityPayload` module-private payload + accessor methods + 4 routed construction paths (`lower.rs:1949`, `lower.rs:2044` via caller restructure, `infer.rs:2902`, `regen_bootstrap_emit.rs` codegen). Plus pattern-match migration: every existing `TypeConnective::Cardinality { element, bound }` destructure (~30 sites grepped) → `TypeConnective::Cardinality(p) => { ... p.element() ... p.bound() ... }`. Mechanical but pervasive. 3 test fixtures + PR-body doc. Not gated on any other lane. Independent of the other two T-ImpossibleBugs classes. **Director-call**: if M is too large for this slot, the alternative is bounded-scaffold convention with a tracked dissolution trigger to API closure — but that contradicts modeling-discipline practice 6 and `feedback_construction_over_ratchets`. Recommendation is M lane, mechanical closure. **Acceptance:** From b2475c8e6c6fbb52ef93b2125e3548e62cfd6322 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Apr 2026 13:01:12 -0400 Subject: [PATCH 10/10] =?UTF-8?q?docs(briefs):=20fix=20stale=20S=20sizing?= =?UTF-8?q?=20in=20=C2=A7Why-not-park=20(now=20M=20after=20API-closure=20r?= =?UTF-8?q?evision)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Claude API review at sha 3cce220f flagged §Q4 'Why not park' still saying '(S; see §Dispatch profile)' while TL;DR and §Dispatch profile both size the lane M post-API-closure. Single authority for lane size = M. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md index 0f98397f2e2..117921674c9 100644 --- a/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md +++ b/docs/briefs/t-impossiblebugs-nested-optional-flatten-design.md @@ -239,7 +239,7 @@ The cardinality substrate THESIS:343 names as the gate is the **v2** state (`ret ### Why not "park" -The bypass is small (S; see §Dispatch profile), well-scoped (specific to `AtMostOne ∧ AtMostOne`), structurally grounded (algebraic idempotence of `AtMostOne`), and the substrate prerequisite is already met. Parking would be conservative beyond what the evidence supports. +The bypass is bounded (M; see §Dispatch profile), well-scoped (specific to `AtMostOne ∧ AtMostOne`), structurally grounded (algebraic idempotence of `AtMostOne`), and the substrate prerequisite is already met. Parking would be conservative beyond what the evidence supports. ## Cross-manager note