diff --git a/DESIGN.md b/DESIGN.md index a4ff1df07af..792e06e7eab 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -88,7 +88,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - **enforcement intent — ask once, compile forever.** The operator's recurring standing directives (enforce complexity repo-wide; lenses must be live; lenses must self-apply; scope must not silently narrow; model must not carry dual representations; a failure arm must refuse, never widen — no absorbing fallbacks, §5) are redundant governance work (§2) re-paid each conversation — the operator performing the missing meta-lens by hand. Model each as a durable `StandingIntent` row and gate the relationship (intent ⇄ `LensContract` ⇄ coverage receipt) fail-closed: a mechanism *claiming enforcement* is complete only when it satisfies the `StandingIntent` — named live consumer, declared scope not narrowed, red control, self-application or explicit exemption — else Unknown/Refused, never silently green. One new authority (`StandingIntent`); everything else extends existing machinery — the registry (`LensRegistryEntryV0` → `LensContract`), reusing `ConstructionJustification` / `subject_roster` and consuming `intent_linearity` / `self_applying_lenses` for the fractal (§7) layer (the same property applied to the code, the lens, the subject producer, the registry, and the acceptance template). Default enforcement scope = whole corpus; under-scope is a failing receipt unless explicitly justified. → [enforcement-intent design](docs/plans/enforcement-intent-design.md) - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked) - **hollow-alias construction wall — DRAFT, design-note-first (sharp-bee-290 mandate).** A bodyless (`PhantomData`-collapsing) declaration reached by construction is a §5 unwritable-class candidate, not a validation check: `GroupCompletion` (PR #7197, infra-blocked) and `FieldOfFractions` (PR #7210, record body { num, denom } content-reviewed clean pending CI + approvals) are two grounded specimens, neither merged to main yet; a third, the emit-side companion, is the `checkpoint_scalar_phantom` class — a checkpoint scalar (arity 0 in Rust) reached with a phantom type arg (`GroupCompletion`, `Compose>`) cannot legally render as `i64` (E0109), documented in-code at `src/v1/stage0/src/v1_compiler_emit_rust.rs:746` and converging with vivid's ~50-finding `checkpoint_scalar_phantom` E0107 bucket and loyal-raven's dotted-path `GroupCompletion` E0308 finding — tracked as Root-4, separately gated, not this note's scope. This note's own rule: bodyless + construction-reached ⇒ refuse; bodyless + `= Node`-aliased (the existing 11-occurrence declared-abstract idiom) ⇒ legitimate; bodyless + never construction-reached (pure type-tag, e.g. `Hardware`) ⇒ legitimate. Sequencing is lens-first (a pure structural `Node`-tree reader, not grep — the doc's own census section is a case study in why grep false-positives ~1,739 hits), promoted to a typechecker refusal only once proven zero-false-positive corpus-wide. No code lands from this note yet. → [hollow-alias construction wall](docs/plans/hollow-alias-construction-wall.md) -- the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) +- the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) · **Next layer (PR #7197, open, not yet merged):** `dag/std/algebra.dag:38`'s `GroupCompletion` is hollow (bodyless — no fields at all), forked a second time by `src/v2/std/integer.dag`'s independent redeclaration — the emitted-Rust operator-trait surface #5428 left uncovered renders it as `PhantomData`. PR #7197 grounds `GroupCompletion` as the Grothendieck pair construction (`{pos: M, neg: M}`) at its single authority, deletes the v2 duplicate in favor of importing it (§2/§3), collapses a native-`Int`-fielded pair construction in `eval_record_lit` (mirrors #5428's `Succ{prev}` collapse), and swaps the emitter's zero-param alias-decl branch to the single-authority `rust_scalar_checkpoint_render_base` so the `Int → i64` checkpoint fires under both corpus representations. Content-reviewed clean; CI in progress. → [GroupCompletion pair-construction design](docs/plans/groupcompletion-pair-construction-design.md) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) - floor shared-computation memoization — M1 entry-closure memo LANDED (#6999, merge dc2aa25684); post-merge validation (msg_1879f052) shows ~0% batch-wall recovery on capped hosts — fixes are mechanism-correct but discovery loads each entry once/worker; residual ~18min owed to #6848 once-per-entry bare-reference fixpoint + cap-saturation throttle (§1.4). Receipts: [floor-time namespace-walk diagnosis](docs/plans/floor-time-namespace-walk-regression-diagnosis.md) §5. M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md) - **#6985 witness-discovery cascade — diagnosis-complete, two confirmed failure classes, both block further stripping.** The initial `pullable()`-never-pulls-arity-zero read was refuted by execution on the `parallelism.dag` restore (DESIGN §5). Two real classes were then confirmed by execution: **Class A** — a re-export-through-partial-strip (qualified-import/re-export mismatch), closed by import-from-definer wave ordering or PR-4 (namespace-resolution-design.md §8). **Class B** — a stripped file's own bare cross-module references resolve only by **pool-membership coincidence**: `resolve_in` finds the target module exactly when some *unrelated* unstripped import elsewhere in the currently-assembled closure has already dragged it into the pool, never from the bare-reference closure itself binding it. A reconciliation probe on an already-stripped `dag/extdeps` file (`bmc/types.dag`) reproduced the identical failure under a narrower closure, confirming this is corpus-wide accidental coverage, not a per-file property — batch-1's ~74 files are green today only because enough unrelated files elsewhere still happen to import the same targets. **This blocks all further `dag/**` import-stripping** until a closure-independent binding fix or a provable-coverage construction check lands. Named side findings, not yet fixed: a LOUDNESS gap (an opaque unlocatable diagnostic for some but not all Class B failure shapes) and an untested zero-arity fn/data-by-value claim. → [import-strip witness-discovery cascade diagnosis](docs/plans/import-strip-witness-discovery-cascade-diagnosis.md) diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag index 30dbc8996d2..45f73e6478b 100644 --- a/dag/gunbc/design_document.dag +++ b/dag/gunbc/design_document.dag @@ -139,7 +139,7 @@ fn open_threads_blocks() -> List { li(text: "**enforcement intent — ask once, compile forever.** The operator's recurring standing directives (enforce complexity repo-wide; lenses must be live; lenses must self-apply; scope must not silently narrow; model must not carry dual representations; a failure arm must refuse, never widen — no absorbing fallbacks, §5) are redundant governance work (§2) re-paid each conversation — the operator performing the missing meta-lens by hand. Model each as a durable `StandingIntent` row and gate the relationship (intent ⇄ `LensContract` ⇄ coverage receipt) fail-closed: a mechanism *claiming enforcement* is complete only when it satisfies the `StandingIntent` — named live consumer, declared scope not narrowed, red control, self-application or explicit exemption — else Unknown/Refused, never silently green. One new authority (`StandingIntent`); everything else extends existing machinery — the registry (`LensRegistryEntryV0` → `LensContract`), reusing `ConstructionJustification` / `subject_roster` and consuming `intent_linearity` / `self_applying_lenses` for the fractal (§7) layer (the same property applied to the code, the lens, the subject producer, the registry, and the acceptance template). Default enforcement scope = whole corpus; under-scope is a failing receipt unless explicitly justified. → [enforcement-intent design](docs/plans/enforcement-intent-design.md)"), li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"), li(text: "**hollow-alias construction wall — DRAFT, design-note-first (sharp-bee-290 mandate).** A bodyless (`PhantomData`-collapsing) declaration reached by construction is a §5 unwritable-class candidate, not a validation check: `GroupCompletion` (PR #7197, infra-blocked) and `FieldOfFractions` (PR #7210, record body \{ num, denom \} content-reviewed clean pending CI + approvals) are two grounded specimens, neither merged to main yet; a third, the emit-side companion, is the `checkpoint_scalar_phantom` class — a checkpoint scalar (arity 0 in Rust) reached with a phantom type arg (`GroupCompletion`, `Compose>`) cannot legally render as `i64` (E0109), documented in-code at `src/v1/stage0/src/v1_compiler_emit_rust.rs:746` and converging with vivid's ~50-finding `checkpoint_scalar_phantom` E0107 bucket and loyal-raven's dotted-path `GroupCompletion` E0308 finding — tracked as Root-4, separately gated, not this note's scope. This note's own rule: bodyless + construction-reached ⇒ refuse; bodyless + `= Node`-aliased (the existing 11-occurrence declared-abstract idiom) ⇒ legitimate; bodyless + never construction-reached (pure type-tag, e.g. `Hardware`) ⇒ legitimate. Sequencing is lens-first (a pure structural `Node`-tree reader, not grep — the doc's own census section is a case study in why grep false-positives ~1,739 hits), promoted to a typechecker refusal only once proven zero-false-positive corpus-wide. No code lands from this note yet. → [hollow-alias construction wall](docs/plans/hollow-alias-construction-wall.md)"), - li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"), + li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) · **Next layer (PR #7197, open, not yet merged):** `dag/std/algebra.dag:38`'s `GroupCompletion` is hollow (bodyless — no fields at all), forked a second time by `src/v2/std/integer.dag`'s independent redeclaration — the emitted-Rust operator-trait surface #5428 left uncovered renders it as `PhantomData`. PR #7197 grounds `GroupCompletion` as the Grothendieck pair construction (`\{pos: M, neg: M\}`) at its single authority, deletes the v2 duplicate in favor of importing it (§2/§3), collapses a native-`Int`-fielded pair construction in `eval_record_lit` (mirrors #5428's `Succ\{prev\}` collapse), and swaps the emitter's zero-param alias-decl branch to the single-authority `rust_scalar_checkpoint_render_base` so the `Int → i64` checkpoint fires under both corpus representations. Content-reviewed clean; CI in progress. → [GroupCompletion pair-construction design](docs/plans/groupcompletion-pair-construction-design.md)"), li(text: "the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.)"), li(text: "floor shared-computation memoization — M1 entry-closure memo LANDED (#6999, merge dc2aa25684); post-merge validation (msg_1879f052) shows ~0% batch-wall recovery on capped hosts — fixes are mechanism-correct but discovery loads each entry once/worker; residual ~18min owed to #6848 once-per-entry bare-reference fixpoint + cap-saturation throttle (§1.4). Receipts: [floor-time namespace-walk diagnosis](docs/plans/floor-time-namespace-walk-regression-diagnosis.md) §5. M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md)"), li(text: "**#6985 witness-discovery cascade — diagnosis-complete, two confirmed failure classes, both block further stripping.** The initial `pullable()`-never-pulls-arity-zero read was refuted by execution on the `parallelism.dag` restore (DESIGN §5). Two real classes were then confirmed by execution: **Class A** — a re-export-through-partial-strip (qualified-import/re-export mismatch), closed by import-from-definer wave ordering or PR-4 (namespace-resolution-design.md §8). **Class B** — a stripped file's own bare cross-module references resolve only by **pool-membership coincidence**: `resolve_in` finds the target module exactly when some *unrelated* unstripped import elsewhere in the currently-assembled closure has already dragged it into the pool, never from the bare-reference closure itself binding it. A reconciliation probe on an already-stripped `dag/extdeps` file (`bmc/types.dag`) reproduced the identical failure under a narrower closure, confirming this is corpus-wide accidental coverage, not a per-file property — batch-1's ~74 files are green today only because enough unrelated files elsewhere still happen to import the same targets. **This blocks all further `dag/**` import-stripping** until a closure-independent binding fix or a provable-coverage construction check lands. Named side findings, not yet fixed: a LOUDNESS gap (an opaque unlocatable diagnostic for some but not all Class B failure shapes) and an untested zero-arity fn/data-by-value claim. → [import-strip witness-discovery cascade diagnosis](docs/plans/import-strip-witness-discovery-cascade-diagnosis.md)"), diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 00fa3903c5b..b31d2ce2d62 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -35,7 +35,10 @@ type AbelianGroup { } -type GroupCompletion +type GroupCompletion { + pos: M + neg: M +} type FieldOfFractions diff --git a/dag/test/retirement/group_completion_construction_retained.dag b/dag/test/retirement/group_completion_construction_retained.dag new file mode 100644 index 00000000000..36dac3b31d9 --- /dev/null +++ b/dag/test/retirement/group_completion_construction_retained.dag @@ -0,0 +1,9 @@ +module test.retirement.group_completion_construction_retained + + +data group_completion_construction_retention: TestModuleRetirement = TestModuleRetirement { + module: "group_completion_construction_test.rs", + disposition: RetainedNonMigratable { + reason: "This witness guards the eval_record_lit construction-side collapse for GroupCompletion \{ pos, neg \} (PR #7197): a plain-record construction with native Value::Int fields must reduce directly to Value::Int(pos - neg), mirroring #5428's Succ\{prev\} collapse, rather than allocating a boxed Value::Record. The assertions pattern-match on the host interpreter's internal Value enum (Value::Int vs Value::Record) to catch a regression to the boxed representation even when the arithmetic result stays numerically correct — that representation-strategy distinction has no observable surface from within a .dag program (the language has no reflection over Value's native-vs-boxed shape), so it cannot migrate to an exact-stem test dag floor witness. Retained until src/v1 deletes at v2 self-host; not migration debt and not a delete candidate." + } +} diff --git a/docs/plans/groupcompletion-pair-construction-design.md b/docs/plans/groupcompletion-pair-construction-design.md new file mode 100644 index 00000000000..e7c88747e93 --- /dev/null +++ b/docs/plans/groupcompletion-pair-construction-design.md @@ -0,0 +1,130 @@ +# Design — the completion pattern: `GroupCompletion` and `FieldOfFractions` + +**Status:** `GroupCompletion` SIGNED (law grain, sharp-bee-290, 2026-07-25, mandate `msg_6fc2ba88-549b-491e-9b6f-ab949539d682`) and IMPLEMENTED — PR #7197. §2 model fix + §3-eval construction-side collapse + (b) emitter checkpoint-order fix landed together per the mandate's hard condition #1. `FieldOfFractions` MODEL grounding SIGNED under the same completion doctrine (law grain, sharp-bee-290, 2026-07-25, mandate `msg_7a83651e-f370-4b2a-8786-e5c0d81aeaa5` — nod 1: "one grounding doctrine, not two"); its REALIZATION section (§7.3 below) is drafted but **HELD, awaiting explicit sign** before implementation — it is materially new, not the checkpoint trick. Linked from [DESIGN.md](../../DESIGN.md) open threads (numeric-tower bullet). + +Owner: eager-crane-304 (completion-pattern grounding lane). Sequence: **GroupCompletion (done)** → **FieldOfFractions model (this note) → FieldOfFractions realization (pending sign, §7.3)** → hollow-alias WALL (design-note-first, capstone, generalizes both specimens — separate note) → Bool → C. + +## 0. The completion pattern, stated once (operator ruling, mandate `msg_7a83651e`) + +`GroupCompletion` and `FieldOfFractions` are not two anemias of the same *shape* — they are **one algebraic move**, instantiated at two different algebraic strengths, and the operator's ruling is to state the move once and derive both from it rather than risk the two definitions drifting apart (exactly the redundancy §2/§3 forbid): + +> **The completion construction.** Given an algebraic structure `S` with a partial "inverse" operation missing (a commutative monoid `M` lacking subtraction; a commutative ring `R` lacking division by non-zero-divisors), freely adjoin the missing inverses by taking **ordered pairs** `(a, b) ∈ S×S` — read as "`a` combined with the formal inverse of `b`" — quotiented by the equivalence relation that says two pairs denote the same completed value iff cross-combining with the *other* pair's second component agrees: +> - **Additive strength (Grothendieck group completion):** `M` a commutative monoid, pair `(pos, neg)` denotes `pos - neg`, `(a,b) ~ (c,d) iff a+d = b+c` (uses only `M`'s `+`). +> - **Multiplicative strength (field of fractions):** `R` a commutative ring (integral domain, no zero divisors), pair `(num, denom)` denotes `num / denom`, `(a,b) ~ (c,d) iff a*d = c*b` (uses only `R`'s `*`). + +Both are the **same categorical construction** (a left adjoint / free completion functor) read under the additive vs. multiplicative interpretation of the ambient structure's single binary operation — which is *why* they get one doctrine, not two: the equivalence-relation shape (`a∘d = b∘c` for the ambient op `∘`), the record-of-two-fields carrier shape, and the "record carries the pair, doc-string carries the law, no structural law-checking machinery" precedent (§7.1 below) are identical between them; only which operation of `M`/`R` is being freely inverted differs. A reader who has understood one instantiation should be able to predict the other without re-deriving it — that is the test that this is one law, not two coincidentally-similar ones. + +Realization, in contrast, **does not transfer between the two instantiations** — see §7.3. + +## 7.1 Specimen 1 — `GroupCompletion` (additive strength, IMPLEMENTED) + +### 1. The anemia (confirmed by reading, not assumed) + +`dag/std/algebra.dag:38` declares + +``` +type GroupCompletion +``` + +with **no body and no `=` alias RHS** — a genuinely hollow declaration, zero fields. `dag/std/integer.dag:21` builds the whole integer tower on it (`type Int = AbelianGroup>`, chained through `dag/std/nat.dag:6 Nat = CommutativeSemiring` — the `dag/std` tower's own algebra-witness-composition style). `src/v2/std/integer.dag:22-23` builds a **second, independently-declared, equally hollow** `type GroupCompletion` / `type Int = GroupCompletion`, this one chained through `v2.std.nat`'s real Peano `Nat = Zero | Succ{prev:Nat}`. + +Confirmed root cause of the emitter symptom: a type declared with no body renders in `src/v1/05_emit_rust.dag` as a `PhantomData` marker (traced: `rust_phantom_marker_inner`/`rust_phantom_field_name`, lines 3480-3490, 4378, 4634, 8178, 9660 — a bodyless generic type becomes a Rust tuple struct or field wrapping `PhantomData`, carrying **no data at all**). A `GroupCompletion` (= `Int`) value therefore has nothing to hold an actual integer, which is the direct cause of the `expected i64 found GroupCompletion>` E0308 cluster and the riding E0369 (missing `Add`/`Sub`/`Mul`/`Ord` impls — nothing to implement them *over*) measured in the deep-seven probe (`docs/probes/gate1_repr_mismatch_e0308_diagnosis_2026-07-24.md`, `COPRODUCT_NATIVE_NUMERIC` bucket, Root 4). + +**A second, independent defect stacked on top:** `src/v2/std/integer.dag:22`'s local `type GroupCompletion` is a **§3 fork** — a second declaration of the same concept `std.algebra` already names, not imported. This duplicates the hollowness (fixing only `dag/std/algebra.dag`'s copy would leave the v2 corpus's own copy — the one the deep-seven probe actually compiles through — still bodyless). + +### 2. The model fix — Grothendieck pair construction + +Ground `GroupCompletion` at its single authority, `dag/std/algebra.dag:38`, as the standard construction that freely completes a commutative monoid to a group: pairs `(pos, neg) ∈ M×M` denoting `pos - neg`, quotiented by `(a,b) ~ (c,d) iff a+d = b+c`. + +``` +type GroupCompletion { + pos: M + neg: M +} +``` + +This mirrors the file's existing convention exactly — `Group`/`AbelianGroup`/`Ring` etc. are all plain records of their operations, none of them encode their algebraic *laws* structurally (no law-checking machinery exists for Monoid/Group associativity either) — so a record carrying the pair with the equivalence relation documented as a doc-string, not enforced structurally, is consistent with every neighboring declaration in this file, not a new pattern invented for this one type. + +**De-fork (§3, same PR):** delete `src/v2/std/integer.dag:22`'s local `type GroupCompletion`; add `GroupCompletion` to its existing `import std.algebra { Cons, Empty, FreeMonoid, AbelianGroup, OrderedRing, Ordering, Less, Equal, Greater }` (line 3). One declaration, both towers reference it. + +`dag/std/algebra.dag:43`'s `type FieldOfFractions` is the second instantiation of the §0 completion pattern (the analogous construction for fields — pairs `(num, denom)` with `(a,b)~(c,d) iff a*d = c*b`) — designed in §7.2/§7.3 below, folded into this same note per the operator's nod-1 ruling rather than a separate design file. + +### 3. Construction-side native grounding — mirroring #5428 exactly + +`v1_interpreter.rs` grounds Peano `Nat` construction-side today: `eval_var` (`Zero` bound as a `VariantValueBinding` → `Value::Int(0)`, line 2041) and `eval_record_lit` (`Succ{prev: Value::Int(p)}` → `Value::Int(p+1)` directly, no boxed `Value::Variant` ever built, line 4256-4261) — the coproduct is the *model*, native `Value::Int` is the *realization*, collapsed at the moment of construction, verified by `match_pattern`'s symmetric `Value::Int(n)` destructuring against `Zero`/`Succ{prev}` patterns (lines 2742-2770). + +The mirrored construction-side collapse for the pair: in `eval_record_lit`, when constructing `GroupCompletion{pos, neg}` (no `parent_enum` — this is a plain record type, not a coproduct variant, so it takes the `else` branch at line 4268 today) and both `pos`/`neg` evaluate to native `Value::Int`, collapse directly to `Value::Int(pos - neg)` rather than building a boxed `Value::Record`. Symmetric `match_pattern` support (destructuring a native `Value::Int(n)` against a `GroupCompletion{pos, neg}` pattern) needs the canonical-representative choice for the inverse direction — `(max(n,0), max(-n,0))` — analogous to how `Succ{prev}` reconstructs `n-1` from `Value::Int(n)`. I have not found any corpus site that destructures `GroupCompletion{pos,neg}` directly today (same as Nat's `Succ{prev}` pattern match was presumably rare pre-#5428), so this arm is defensive completeness, not a currently-exercised path — flagging so you can confirm it's worth landing now vs. deferring to an actual witness. + +### 4. Open question — the deep-seven Rust-emission side (need your ruling before I implement this part) + +§3 is unconditional (the v1 seed interpreter has no `corpus_repr` axis — it just executes `.dag`). The **emitted-Rust** side is where I'm not confident which shape you intend, and your doctrine text ("native realization grounds to the machine-width Int axis") is consistent with more than one construction: + +- **(a)** Once `GroupCompletion` has a real body, it emits as a genuine 2-field Rust struct under `FaithfulFreeMonoid` (the deep-seven probe's corpus_repr) instead of `PhantomData` — this alone kills the E0308 (`expected i64 found GroupCompletion>` becomes a real, non-phantom, non-mismatched type), but `int_add(a,b){ a + b }` (`src/v2/std/integer.dag:863`, and `int_sub`/`int_compare`/etc., all written directly against Rust's `+`/`-`/`<`/`==` operators) then needs `impl Add/Sub/Mul/PartialOrd/PartialEq for GroupCompletion` generically derived from `M`'s own impls (pairwise on `pos`/`neg`, canonicalizing through the equivalence relation). That is **exactly** Root 4 / sub-wall #2 from the gate1 diagnosis ("trait-derive-completeness predicate... same shape as the #6776 wrap-decision predicate, applied to a different axis") — already identified, not yet owned, not part of what I've scoped here. +- **(b)** `Int` already has its own Rust checkpoint (`dag/extdeps/languages/rust/types.dag:16`, `{dag_name: "Int", target_type: "i64", ...}`, single-authority, precedent for `Int8`…`UInt128`'s `Compose>` rows grounding to bounded machine ints by *derivation* rather than by body). The checkpoint lookup fires on the leaf name reached *after* alias unfolding; today unfolding walks past `Int` down to `GroupCompletion`, so the existing `Int → i64` row never gets consulted. If `Int` is meant to stay unconditionally native (always `i64`, regardless of `corpus_repr`) — which is what "grounds to the machine-width Int axis" most directly reads as — the fix is making checkpoint lookup consult **each alias-unfolding step**, not only the fully-peeled leaf, so the already-registered `Int` row wins before reaching the (now real, but not machine-native) `GroupCompletion` struct underneath it. This is *not* a new name-match rule on `GroupCompletion` (nothing new keys off that name) — it reuses the single authority that already exists for `Int` — but I want your confirmation this isn't the shape of patch your mandate rules out, since it still touches `05_emit_rust.dag`. + +I did not want to guess between (a) and (b) and land the wrong one under a "model-before-implement" mandate — this is the one place your ruling changes what I build. My read: (b) is what actually burns down the deep-seven NUMERIC_TOWER count measurably (native `i64`, zero new trait-impl surface); (a) alone converts E0308 into a differently-shaped E0369 until sub-wall #2 lands separately, which may not be this lane's job to also build. + +### 5. Discriminating RED (green-by-execution, not typecheck) + +Witness, modeled on `ct_diagnostics_carrier_grounding_test` (`src/v1/compiler_tests_rust.dag:553-593`) plus the pair-shaped fixture pattern in `ct_rust_btree_set_ord_eligibility_test` (`shaped_type_node`/`named_type_node`, lines 598-623): + +- **Interpreter witness** (§3): evaluate `GroupCompletion{pos: 5, neg: 2}` and `GroupCompletion{pos: 1, neg: 4}` through `eval_record_lit`; assert both collapse to native `Value::Int(3)` / `Value::Int(-3)` (not `Value::Record`); assert `nat_add`-style combination of the two matches native `Value::Int` subtraction — the same shape as `cross_representation_equality_test` (`src/v1/tests/src/cross_representation_equality_test.rs`), red if the pair ever surfaces as a boxed record where arithmetic expects a native int. +- **Emitter witness** (§4, once (a) vs (b) is settled): render `GroupCompletion` (built via `shaped_type_node("GroupCompletion", [named_type_node("Nat")])`) through `render_rust_type(..., RustCorpusRepr::FaithfulFreeMonoid, ...)` and assert the emitted string is no longer `GroupCompletion>`-with-`PhantomData`-body (path (a): assert real `pos`/`neg` fields present; path (b): assert `"i64"`). +- **Deep-seven burn-down measurement — DONE, measured post-fix (2026-07-25):** reran the classifier-v3 probe (`gunbc compile --source-root dag --source-root src/v2 --entry --target rust --dependency-pool-index primary-precedence` → `cssl_assemble` → `cargo build --release --lib`) across 5 of the 7 modules probed directly — `06_translate`, `04_infer`, `05_eval`, `emit_host`, `materialization_carriers`; `05_emit` and `emit_module` skipped as byte-identical to `06_translate` per the 2026-07-24 baseline doc, an assumption re-verified this pass by running `05_emit` directly post-drift (byte-identical histogram, `GroupCompletion` mentions = 0). Baseline (2026-07-24, pre-fix): 3 occurrences of the `expected i64 found GroupCompletion>` shape in `06_translate` alone, 1–5% share across all 6 deep-family modules. **Measured post-fix: the `GroupCompletion>` COPRODUCT_NATIVE_NUMERIC marker is zero across all 7** (a clean, drift-immune signal vs. raw aggregate E0308 counts, which are confounded by ~5 unrelated commits that landed on `main` between the baseline and this measurement). **Residue found, not absorbed:** `materialization_carriers` retains 3 `GroupCompletion<...CommutativeSemiring...>` mismatches (`std/measure.dag`'s `Measure`, a non-Int base) — Root-4 arithmetic-trait-derivation, out of this lane's scope per §4(a) above, tracked separately by sharp-bee-290 (confirmed distinct from silent-badger-23's #7174 scope). This rerun is the receipt; a reused-authority-pattern-plus-cargo-checks-pass without it would not have been accepted as a fix per the mandate. + +### 6. Scope boundary + +`v2.std.integer`'s own modeled arithmetic (`int_add`, `int_sub`, `int_compare`, … lines 863-995) is **not touched** — those already delegate to native operators, which is exactly what this design makes valid again. `v2.std.nat`'s real Peano `Nat = Zero | Succ{prev:Nat}` is **not touched** — it stays the faithfully-modeled recursive type; only `GroupCompletion` (its own separate concept, one layer up) gets a body. Nothing in this design proposes routing by the literal name `"GroupCompletion"` at the emitter as a special case disconnected from the model — every consumer (interpreter, emitter, checkpoint table) reads the same single grounded declaration. + +## 7.2 Specimen 2 — `FieldOfFractions` (multiplicative strength, MODEL SIGNED) + +### 1. The anemia (confirmed by reading) + +`dag/std/algebra.dag:43` declares + +``` +type FieldOfFractions +``` + +— no body, no `=` alias RHS, the same genuinely-hollow shape as `GroupCompletion` was before §7.1. Two consumers chain through it, both in `dag/std`: + +- `dag/std/rational.dag:4` — `type Rational = Field>` +- `dag/std/float.dag:10` — `type Real = ApproximateField>` (and `Real32`/`Real64`/`Float32`/`Float64`/`Float` compose on top of `Real`) + +**No §3 fork exists for `FieldOfFractions`** — confirmed by corpus-wide grep (`grep -rn "FieldOfFractions" --include=*.dag .` and a direct scan of `src/v2/std/`): the only declaration is `dag/std/algebra.dag:43`; `Rational`/`Real` both reference it via `import std.algebra { Field, FieldOfFractions }`, no independent redeclaration anywhere in `src/v2`. This is a genuine difference from the `GroupCompletion` specimen, not an oversight on my part — the §7.1 de-fork step (§7.1.2, "delete `src/v2/std/integer.dag:22`'s local declaration") **has no analogue here**: there is nothing to de-fork, only a body to add. + +The emitter symptom this anemia would cause is the same `PhantomData` collapse as §7.1.1 — a bodyless `FieldOfFractions` renders as a marker carrying no data — but it is **not yet measured** in the deep-seven probe the way `GroupCompletion` was, because `Rational`/`Real`/`Float` are not among the 7 modules that probe covers; this note does not claim a measured pre-fix baseline for `FieldOfFractions` the way §7.1.5 has one for `GroupCompletion` (flagged honestly rather than reusing the `GroupCompletion` numbers by association — the two anemias are the same *pattern*, not the same *measurement*). + +### 2. The model fix — field of fractions pair construction + +Ground `FieldOfFractions` at its single authority, `dag/std/algebra.dag:43`, as the §0 completion pattern under multiplicative strength: pairs `(num, denom) ∈ R×R` denoting `num / denom`, quotiented by `(a,b) ~ (c,d) iff a*d = c*b`. + +``` +type FieldOfFractions { + num: R + denom: R +} +``` + +Same convention-fit argument as §7.1.2: `Field`/`Ring`/`OrderedRing` etc. in `algebra.dag` are all plain records of operations with laws documented, not structurally enforced — a record carrying `(num, denom)` with the cross-multiplication equivalence as a doc-string is the existing house style, not a new pattern. No de-fork step is needed (§7.2.1) — this is a pure add-body. + +**What this model fix does NOT do:** it does not choose a canonical/reduced representative (e.g. dividing by `gcd(num, denom)`), does not forbid `denom = 0` structurally (no refinement-type machinery exists in this corpus to express "non-zero" as part of the type, matching `GroupCompletion`'s equally-unenforced law), and does not specify construction-side collapse behavior — that is §7.3, held pending sign because (unlike §7.1.3) there is no native scalar for it to collapse *into*. + +### 3. The realization — materially NEW, not the checkpoint trick (HELD pending sign) + +This is the section the operator asked to see before I implement anything here (mandate `msg_7a83651e`, nod 1). It is presented for sign, not landed. + +**Why §7.1's realization path does not transfer:** `GroupCompletion` (= `Int`) had an escape hatch `FieldOfFractions` does not — `Int` already owns a registered Rust checkpoint (`dag/extdeps/languages/rust/types.dag:16`, `Int → i64`), so §7.1's realization fix was "make the existing checkpoint lookup fire earlier in the alias-unfolding walk" (§7.1.4(b)) — zero new trait-impl surface, because native `i64` arithmetic was already correct. **`Rational` has no machine-scalar checkpoint** — there is no `rational → f64`-style row in `dag/extdeps/languages/rust/types.dag` today, and inventing one would be dishonest: `f64` is lossy (not the field of fractions over `Int`, a different real-number approximation entirely — that's precisely what `Real`/`ApproximateField` already names as a *distinct* type from `Rational`/`Field`). So the (b) collapse-to-native-scalar move is **not available** for this specimen; a fabricated checkpoint here would be exactly the "forbidden dodge" the mandate names (§5's workaround trap — routing around a genuine modeling gap with a plausible-looking shortcut). + +**What realization actually requires:** `Rational`/`Real` values must realize as genuine `{num, denom}` structs, in both places a value lives: + +- **Interpreter (`v1_interpreter.rs`):** `eval_record_lit` constructing `FieldOfFractions{num, denom}` builds a real `Value::Record` — **no collapse arm**, unlike §7.1.3's `GroupCompletion → Value::Int`. This is a smaller change than §7.1.3, not a larger one: the "no fix needed" branch (`eval_record_lit`'s existing `else` path building `Value::Record`) is already correct once the type has a body; nothing new to write here beyond confirming no accidental collapse gets added by analogy-copying §7.1.3's code without checking the checkpoint precondition first. +- **Emitted Rust (`05_emit_rust.dag` / `v1_compiler_emit_rust.rs`):** once `FieldOfFractions` has a body, it stops emitting as `PhantomData` and starts emitting as a real 2-field struct (the §7.1.4(a) path, not (a)+(b) — there is no (b) here). `v2.std.rational`'s modeled arithmetic (if/when it exists — not yet audited as part of this note) would need `impl Add/Sub/Mul/PartialOrd/PartialEq for FieldOfFractions` generically derived from `R`'s own `Ring`/`OrderedRing` witnesses, cross-multiplying per the §0 equivalence relation. **This is the same Root-4 arithmetic-trait-derivation gap** the `materialization_carriers`/`Measure` residue (§7.1.5) already surfaced and sharp-bee-290 is routing separately — `FieldOfFractions` realization is a *second site* that couples to that same missing derivation, not a new independent gap. + +**Staging (this is the ask for your sign):** land the §7.2 MODEL grounding (body only) now, under the already-signed completion doctrine — it is decidable, bounded, and has no dependency on Root-4. **Stage the emit/arithmetic REALIZATION burn-down behind Root-4**, with a declared dissolution trigger: *when the Root-4 generic-operator-trait-derivation predicate lands (silent-badger-23 / gate1 sub-wall #2), `FieldOfFractions`'s `Add`/`Sub`/`Mul`/`Ord` impls are generated by that same predicate, not hand-written per-type here.* Until then, a `FieldOfFractions` value type-checks and interprets correctly (§7.2.3 interpreter path) but is not claimed to compile to arithmetic-correct emitted Rust — that residue is named and counted, exactly as §7.1.5 named the `Measure` residue, never silently absorbed. + +### 4. Discriminating RED (for the model half only — realization RED is written when §7.3 realization is signed) + +- **Model witness:** construct `FieldOfFractions{num: 3, denom: 4}` through the interpreter and assert it evaluates to a `Value::Record{type_name: "FieldOfFractions", fields: [("num", 3), ("denom", 4)]}` — i.e. explicitly assert it does **NOT** collapse to a native scalar (the negative-space complement of §7.1.5's interpreter witness — red if some future edit accidentally adds a collapse arm here by pattern-matching §7.1.3 without checking the no-checkpoint precondition). +- **De-fork non-regression witness:** assert `grep -rn "type FieldOfFractions" --include=*.dag .` returns exactly one declaration (`dag/std/algebra.dag`) — red if a future edit reintroduces a v2-local fork the way `GroupCompletion` had one. +- **Realization RED is deferred to §7.3 sign-off** — no emitter witness is written until the realization section above is signed, per DESIGN §5 ("done means green-by-execution," which does not apply to work not yet authorized to start). diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index 31590bb0187..ec5ad54a52d 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -4428,7 +4428,7 @@ fn emit_typed_item(item: Node, module_name: String, registry: Map concat(rust_visibility_prefix(), rust_items().type_alias_keyword, " ", item_text, " = ", host, ";") Absent => diff --git a/src/v1/compiler_tests_rust.dag b/src/v1/compiler_tests_rust.dag index 08909d49c8f..38fd6770f24 100644 --- a/src/v1/compiler_tests_rust.dag +++ b/src/v1/compiler_tests_rust.dag @@ -547,7 +547,48 @@ fn ct_coercion_tests() -> String { " // =========================================================================\n\n", test_fns |> join(separator: "\n"), ct_rust_btree_set_ord_eligibility_test(), - ct_diagnostics_carrier_grounding_test()) + ct_diagnostics_carrier_grounding_test(), + ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test()) +} + +fn ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test() -> String { + concat( + " #[test]\n", + " fn groupcompletion_int_checkpoint_fires_under_faithful_corpus() {\n", + " // Discriminating witness for the (b) checkpoint-order fix (sharp-bee-290 sign-off,\n", + " // msg_6fc2ba88-549b-491e-9b6f-ab949539d682): emit_typed_item's zero-param alias-decl\n", + " // branch calls rust_scalar_checkpoint_render_base (the single-authority checkpoint\n", + " // lookup), not the HostNative-only rust_seed_host_numeric_alias, so the Int -> i64\n", + " // checkpoint row (dag/extdeps/languages/rust/types.dag) fires BEFORE the RHS\n", + " // (GroupCompletion) is unfolded — under BOTH corpus representations. A\n", + " // regression that narrows this back to the HostNative-only alias makes the\n", + " // FaithfulFreeMonoid arm return None, which is what this witness guards.\n", + " assert_eq!(\n", + " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n", + " \"Int\".to_string(),\n", + " crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid\n", + " ),\n", + " Some(\"i64\".to_string())\n", + " );\n", + " assert_eq!(\n", + " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n", + " \"Int\".to_string(),\n", + " crate::v1_compiler_infer_emit_info::RustCorpusRepr::HostNative\n", + " ),\n", + " Some(\"i64\".to_string())\n", + " );\n", + " // GroupCompletion itself has no checkpoint row and is not the seed host numeric\n", + " // alias, so the checkpoint correctly declines to render it directly (the RHS\n", + " // unfolding path handles it as a real 2-field struct) — the checkpoint fires ONLY\n", + " // for the Int/Nat leaf name, never widening to the container type.\n", + " assert_eq!(\n", + " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n", + " \"GroupCompletion\".to_string(),\n", + " crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid\n", + " ),\n", + " None\n", + " );\n", + " }\n\n") } fn ct_diagnostics_carrier_grounding_test() -> String { diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 5afe49293c0..dd67ec91918 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -24781,6 +24781,14 @@ fn compute_inert_carrier_data(files: &[(String, String)]) -> InertCarrierData { *self_block_refs.entry(name.clone()).or_insert(0) += inert_carrier_count_token(&block, &name); for v in inert_carrier_variant_names(&block) { + if v == name { + // A single-variant coproduct whose variant name equals the type + // name (`type X = X { .. }`) already had its occurrences tallied + // above via `name`; tallying it again here as a "variant" double- + // counts every reference and can zero out external consumption + // even when the type has real callers. + continue; + } *self_block_refs.entry(v.clone()).or_insert(0) += inert_carrier_count_token(&block, &v); type_variants.entry(name.clone()).or_default().push(v); diff --git a/src/v1/stage0/src/compiler_tests.rs b/src/v1/stage0/src/compiler_tests.rs index 1f3c6bb1581..38f4aa91368 100644 --- a/src/v1/stage0/src/compiler_tests.rs +++ b/src/v1/stage0/src/compiler_tests.rs @@ -1162,6 +1162,43 @@ mod compiler_tests { ); } + #[test] + fn groupcompletion_int_checkpoint_fires_under_faithful_corpus() { + // Discriminating witness for the (b) checkpoint-order fix (sharp-bee-290 sign-off, + // msg_6fc2ba88-549b-491e-9b6f-ab949539d682): emit_typed_item's zero-param alias-decl + // branch calls rust_scalar_checkpoint_render_base (the single-authority checkpoint + // lookup), not the HostNative-only rust_seed_host_numeric_alias, so the Int -> i64 + // checkpoint row (dag/extdeps/languages/rust/types.dag) fires BEFORE the RHS + // (GroupCompletion) is unfolded — under BOTH corpus representations. A + // regression that narrows this back to the HostNative-only alias makes the + // FaithfulFreeMonoid arm return None, which is what this witness guards. + assert_eq!( + crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base( + "Int".to_string(), + crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid + ), + Some("i64".to_string()) + ); + assert_eq!( + crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base( + "Int".to_string(), + crate::v1_compiler_infer_emit_info::RustCorpusRepr::HostNative + ), + Some("i64".to_string()) + ); + // GroupCompletion itself has no checkpoint row and is not the seed host numeric + // alias, so the checkpoint correctly declines to render it directly (the RHS + // unfolding path handles it as a real 2-field struct) — the checkpoint fires ONLY + // for the Int/Nat leaf name, never widening to the container type. + assert_eq!( + crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base( + "GroupCompletion".to_string(), + crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid + ), + None + ); + } + /// Return current process RSS in bytes (macOS via mach_task_basic_info). fn get_rss_bytes() -> u64 { #[cfg(target_os = "macos")] diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index 21284ec02e0..d66be3d6938 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -61,8 +61,12 @@ pub struct AbelianGroup { pub _phantom: std::marker::PhantomData, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct GroupCompletion(pub std::marker::PhantomData); +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct GroupCompletion { + pub pos: M, + pub neg: M, + pub _phantom: std::marker::PhantomData, +} #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct FieldOfFractions(pub std::marker::PhantomData); diff --git a/src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs b/src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs index fb32f5fdd82..0ed9bfe46ba 100644 --- a/src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs +++ b/src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs @@ -88,10 +88,14 @@ pub fn ct_coercion_tests() -> String { } __result }); - v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(" // =========================================================================\n".to_string(), " // Coercion registry tests (auto-generated from data declarations)\n".to_string()), " // =========================================================================\n\n".to_string()), test_fns.clone().join(&"\n".to_string())), ct_rust_btree_set_ord_eligibility_test()), ct_diagnostics_carrier_grounding_test()) + v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(" // =========================================================================\n".to_string(), " // Coercion registry tests (auto-generated from data declarations)\n".to_string()), " // =========================================================================\n\n".to_string()), test_fns.clone().join(&"\n".to_string())), ct_rust_btree_set_ord_eligibility_test()), ct_diagnostics_carrier_grounding_test()), ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test()) } } +pub fn ct_groupcompletion_checkpoint_fires_under_faithful_corpus_test() -> String { + v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(" #[test]\n".to_string(), " fn groupcompletion_int_checkpoint_fires_under_faithful_corpus() {\n".to_string()), " // Discriminating witness for the (b) checkpoint-order fix (sharp-bee-290 sign-off,\n".to_string()), " // msg_6fc2ba88-549b-491e-9b6f-ab949539d682): emit_typed_item's zero-param alias-decl\n".to_string()), " // branch calls rust_scalar_checkpoint_render_base (the single-authority checkpoint\n".to_string()), " // lookup), not the HostNative-only rust_seed_host_numeric_alias, so the Int -> i64\n".to_string()), " // checkpoint row (dag/extdeps/languages/rust/types.dag) fires BEFORE the RHS\n".to_string()), " // (GroupCompletion) is unfolded — under BOTH corpus representations. A\n".to_string()), " // regression that narrows this back to the HostNative-only alias makes the\n".to_string()), " // FaithfulFreeMonoid arm return None, which is what this witness guards.\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n".to_string()), " \"Int\".to_string(),\n".to_string()), " crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid\n".to_string()), " ),\n".to_string()), " Some(\"i64\".to_string())\n".to_string()), " );\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n".to_string()), " \"Int\".to_string(),\n".to_string()), " crate::v1_compiler_infer_emit_info::RustCorpusRepr::HostNative\n".to_string()), " ),\n".to_string()), " Some(\"i64\".to_string())\n".to_string()), " );\n".to_string()), " // GroupCompletion itself has no checkpoint row and is not the seed host numeric\n".to_string()), " // alias, so the checkpoint correctly declines to render it directly (the RHS\n".to_string()), " // unfolding path handles it as a real 2-field struct) — the checkpoint fires ONLY\n".to_string()), " // for the Int/Nat leaf name, never widening to the container type.\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::rust_scalar_checkpoint_render_base(\n".to_string()), " \"GroupCompletion\".to_string(),\n".to_string()), " crate::v1_compiler_infer_emit_info::RustCorpusRepr::FaithfulFreeMonoid\n".to_string()), " ),\n".to_string()), " None\n".to_string()), " );\n".to_string()), " }\n\n".to_string()) +} + pub fn ct_diagnostics_carrier_grounding_test() -> String { v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(" #[test]\n".to_string(), " fn diagnostics_carrier_grounds_to_native_option() {\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_host_diagnostics_carrier_alias(\"Diagnostics\".to_string()));\n".to_string()), " assert!(!crate::v1_compiler_emit_rust::is_host_diagnostics_carrier_alias(\"Optional\".to_string()));\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_grounded_coproduct_native_alias(\"Diagnostics\".to_string()));\n".to_string()), " let empty_shared = std::rc::Rc::new(im::OrdSet::new());\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::render_rust_diagnostics_carrier_applied(empty_shared.clone()),\n".to_string()), " \"Option\"\n".to_string()), " );\n".to_string()), " let mut shared_ned_inner = im::OrdSet::new();\n".to_string()), " shared_ned_inner.insert(\"NonEmptyDiagnostics\".to_string());\n".to_string()), " let shared_ned = std::rc::Rc::new(shared_ned_inner);\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::render_rust_diagnostics_carrier_applied(shared_ned),\n".to_string()), " \"Option>\"\n".to_string()), " );\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_some_like_variant_name(\"Some\".to_string()));\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_some_like_variant_name(\"Present\".to_string()));\n".to_string()), " assert!(!crate::v1_compiler_emit_rust::is_some_like_variant_name(\"None\".to_string()));\n".to_string()), " assert!(!crate::v1_compiler_emit_rust::is_some_like_variant_name(\"Absent\".to_string()));\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_optional_like_parent_name(\"Diagnostics\".to_string()));\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_optional_like_parent_name(\"Optional\".to_string()));\n".to_string()), " assert!(!crate::v1_compiler_emit_rust::is_optional_like_parent_name(\"Witness\".to_string()));\n".to_string()), " let diagnostics_node = named_type_node(\"Diagnostics\");\n".to_string()), " let source_indices = std::rc::Rc::new(HashMap::new());\n".to_string()), " assert!(crate::v1_compiler_emit_rust::is_host_diagnostics_carrier_type(diagnostics_node.clone(), source_indices.clone()));\n".to_string()), " let empty_emit = crate::v1_compiler_infer_emit_info::empty_emit_graph_info();\n".to_string()), " assert_eq!(\n".to_string()), " crate::v1_compiler_emit_rust::render_rust_type(\n".to_string()), " diagnostics_node,\n".to_string()), " empty_shared,\n".to_string()), " crate::v1_compiler_infer_emit_info::RustCorpusRepr::HostNative,\n".to_string()), " source_indices,\n".to_string()), " empty_emit\n".to_string()), " ),\n".to_string()), " \"Option\"\n".to_string()), " );\n".to_string()), " }\n\n".to_string()) } diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index e4bdbc1a7d7..418d957b672 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -11225,7 +11225,7 @@ pub fn emit_typed_item( env.source_indices.clone(), ) } else { - match rust_seed_host_numeric_alias( + match rust_scalar_checkpoint_render_base( item_text.clone(), emit_info.corpus_repr.clone(), ) { diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 243fb919a38..0f4e9d87d1d 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -2739,6 +2739,10 @@ fn match_pattern( } _ => None, }, + // GroupCompletion{pos,neg} destructuring against a native Value::Int is + // deliberately unhandled here (no corpus site exercises it yet, #5-scoped + // deferral) — an unmatched pattern name falls through to `_ => None` below, + // refusing rather than fabricating a wrong (pos, neg) pair. Value::Int(n) if name_last == "Zero" || name_last == "Succ" => match name_last { "Zero" => { if *n == 0 { @@ -4266,6 +4270,14 @@ fn eval_record_lit( fields: Rc::new(fields), }) } else { + if type_name == "GroupCompletion" { + if let (Some(Value::Int(pos)), Some(Value::Int(neg))) = ( + fields_get(&fields, ctx.sym("pos")), + fields_get(&fields, ctx.sym("neg")), + ) { + return Ok(Value::Int(pos - neg)); + } + } Ok(Value::Record { type_name: ctx.sym(&type_name), fields: Rc::new(fields), diff --git a/src/v1/tests/src/group_completion_construction_test.rs b/src/v1/tests/src/group_completion_construction_test.rs new file mode 100644 index 00000000000..b7e0adcce1c --- /dev/null +++ b/src/v1/tests/src/group_completion_construction_test.rs @@ -0,0 +1,93 @@ +use std::rc::Rc; + +use v1_compiler::cli_run; +use v1_compiler::v1_compiler_compile::{compile_to_resolved, ResolvedPipelineResult}; +use v1_compiler::v1_interpreter::{self, ExecutionMode, Value}; + +use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root}; + +// Discriminating witness for the §2/§3 GroupCompletion grounding (sharp-bee-290 sign-off, +// msg_6fc2ba88-549b-491e-9b6f-ab949539d682): `GroupCompletion = { pos: M, neg: M }` is +// now a real 2-field record at its single authority (dag/std/algebra.dag), and +// `eval_record_lit` collapses a plain-record `GroupCompletion{pos, neg}` construction with +// native `Value::Int` fields directly to `Value::Int(pos - neg)` — mirroring #5428's +// Succ{prev} construction-side collapse — rather than building a boxed `Value::Record`. +// A regression that reintroduces a boxed record (or a wrong pair-to-int reduction) fails +// this witness; a regression that leaves the type hollow (no `pos`/`neg` fields at all) +// fails to resolve at all, which this witness's `assert_resolved` also guards. +const RECEIPTS_SOURCE: &str = r#" +module test.group_completion_construction + +import v2.std.logic { Bool } +import std.algebra { GroupCompletion } + +fn positive_pair() -> Int { GroupCompletion { pos: 5, neg: 2 } } +fn negative_pair() -> Int { GroupCompletion { pos: 1, neg: 4 } } +fn zero_pair() -> Int { GroupCompletion { pos: 3, neg: 3 } } + +fn collapsed_pair_arithmetic() -> Bool { + (GroupCompletion { pos: 5, neg: 2 }) + (GroupCompletion { pos: 1, neg: 4 }) == 0 +} +"#; + +fn assert_resolved(resolved: &ResolvedPipelineResult) { + let msgs: Vec = resolved + .diagnostics + .iter() + .map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone())) + .filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use ")) + .collect(); + assert!( + msgs.is_empty() && resolved.graph.is_some(), + "receipts source should resolve cleanly, got {:?} (graph present: {})", + msgs, + resolved.graph.is_some(), + ); +} + +fn with_receipts_ctx(body: impl FnOnce(&v1_interpreter::InterpContext) -> R) -> R { + let ws = workspace_root(); + let roots = [ws.join("src/v2"), ws.join("dag")]; + let sources = + resolve_imports_transitively_with_source_roots("test.dag", RECEIPTS_SOURCE, &roots); + let resolved = compile_to_resolved(Rc::new(sources.into())); + assert_resolved(&resolved); + let graph = resolved.graph.as_ref().expect("graph"); + let ctx = + cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet); + body(&ctx) +} + +#[test] +fn group_completion_pair_collapses_to_native_int() { + with_receipts_ctx(|ctx| { + for (f, expected) in [ + ("positive_pair", 3i64), + ("negative_pair", -3i64), + ("zero_pair", 0i64), + ] { + match v1_interpreter::run_in_context(ctx, f, false) { + Ok(Value::Int(n)) if n == expected => {} + other => panic!( + "{f}: expected native Value::Int({expected}) — a construction-side collapse \ + regression (a boxed Value::Record, or a wrong pos-neg reduction) surfaces \ + here; got {other:?}" + ), + } + } + }); +} + +#[test] +fn group_completion_pairs_combine_via_native_arithmetic() { + with_receipts_ctx(|ctx| { + match v1_interpreter::run_in_context(ctx, "collapsed_pair_arithmetic", false) { + Ok(Value::Bool(true)) => {} + other => panic!( + "collapsed_pair_arithmetic: expected Bool(true) — both pairs collapse to \ + native Value::Int (3 and -3) and combine via ordinary native addition; a \ + boxed-record straddle here means the collapse did not fire; got {other:?}" + ), + } + }); +} diff --git a/src/v1/tests/src/lib.rs b/src/v1/tests/src/lib.rs index 3b18398da03..055f32966fa 100644 --- a/src/v1/tests/src/lib.rs +++ b/src/v1/tests/src/lib.rs @@ -71,6 +71,8 @@ mod global_bare_corpus_census_test; #[cfg(test)] mod global_bare_variant_locals_receipt_test; #[cfg(test)] +mod group_completion_construction_test; +#[cfg(test)] mod gunbhub_serve_program_test; #[cfg(test)] mod html_markup_smoke_test; diff --git a/src/v2/std/integer.dag b/src/v2/std/integer.dag index b502b448c04..b34aafee8b1 100644 --- a/src/v2/std/integer.dag +++ b/src/v2/std/integer.dag @@ -1,6 +1,6 @@ module v2.std.integer -import std.algebra { Cons, Empty, FreeMonoid, AbelianGroup, OrderedRing, Ordering, Less, Equal, Greater } +import std.algebra { Cons, Empty, FreeMonoid, AbelianGroup, GroupCompletion, OrderedRing, Ordering, Less, Equal, Greater } import std.error_primitives { DivError, Result, DivideByZero, Ok, Err } import v2.std.algebra { TailAbsent, TailFound, fold_list, fold_list_node, length } import v2.std.collection { Absent, List, Optional, Present, list_at_optional, optional_absent, optional_present } @@ -19,7 +19,6 @@ import v2.std.machine { } import v2.std.nat { Nat } import v2.std.text { Char, CharAbsent, CharFound, String, string_head, string_tail } -type GroupCompletion type Int = GroupCompletion type UInt = v2.std.nat.Nat type Compose