Skip to content

GroupCompletion grounding lane — numeric tower next layer, design-note-first #7197

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
briansrls merged 1 commit into from
Jul 26, 2026
Merged

GroupCompletion grounding lane — numeric tower next layer, design-note-first #7197

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion DESIGN.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<M>` (PR #7197, infra-blocked) and `FieldOfFractions<R>` (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<Nat>`, `Compose<Int, MachineWidth<>>`) cannot legally render as `i64<T>` (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<v2.std.nat.Nat>` 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<M>` 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<M>` 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)
Expand Down
56 changes: 40 additions & 16 deletions dag/extdeps/languages/rust/emit.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,29 +291,53 @@ fn rust_qualified_module_mod_filename(qualified_module: String) -> String {
concat(rust_qualified_module_mod_basename(qualified_module: qualified_module), ".rs")
}

data rust_repr_grounding_arm_b_dissolve_on: String = "Interim CommutativeSemiring<Magnitude> carrier arithmetic stubs dissolve when GroupCompletion pair arithmetic bodies land (#7197, eager-crane numeric-tower lane — NOT silent-badger-23); replace fail-closed unimplemented! stubs with grounded operations. Do not retain PartialEq<i64> cross-representation bridge — numeric-tower grounding replaces the straddle."
data rust_repr_grounding_arm_b_dissolve_on: String = "GroupCompletion<M> pos/neg pair arithmetic (#7197): Grothendieck add (componentwise), ring-completion mul ((ac+bd, ad+bc)), div on canonical representative (pos-neg)/(rhs.pos-rhs.neg) with zero neg; no PartialEq<i64> cross-representation bridge."

data rust_repr_grounding_arm_b_stub_inventory: String = "MARKED scaffold (§6): four fail-closed unimplemented! bodies emitted into src/v1/stage0/src/std_algebra.rs from this authority — Add:91, Mul:97, Div:103, PartialEq<i64>:108 (line refs stable post-regen; probe via grep 'interim CommutativeSemiring'). Dissolve owner: #7197 eager-crane. std_types.rs From<Bool> (real match body, not a stub) is out of scope for this inventory."

fn rust_supplemental_impls_commutative_semiring_magnitude() -> String {
fn rust_supplemental_impls_group_completion() -> String {
concat(
"\n// repr-grounding arm (b): Nat carrier arithmetic (v1 seed emit; ",
"\n// repr-grounding arm (b): GroupCompletion<M> carrier arithmetic (v1 seed emit; ",
rust_repr_grounding_arm_b_dissolve_on,
")\n",
"impl std::ops::Add for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
" type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
" fn add(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
"impl<M> std::ops::Neg for GroupCompletion<M> {\n",
" type Output = Self;\n",
" fn neg(self) -> Self::Output {\n",
" GroupCompletion { pos: self.neg, neg: self.pos, _phantom: std::marker::PhantomData }\n",
" }\n",
"}\n",
"impl<M> std::ops::Add for GroupCompletion<M>\n",
"where M: std::ops::Add<Output = M>,\n",
"{\n",
" type Output = Self;\n",
" fn add(self, rhs: Self) -> Self::Output {\n",
" GroupCompletion { pos: self.pos + rhs.pos, neg: self.neg + rhs.neg, _phantom: std::marker::PhantomData }\n",
" }\n",
"}\n",
"impl std::ops::Mul for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
" type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
" fn mul(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
"impl<M> std::ops::Sub for GroupCompletion<M>\n",
"where M: std::ops::Add<Output = M> + std::ops::Neg<Output = M>,\n",
"{\n",
" type Output = Self;\n",
" fn sub(self, rhs: Self) -> Self::Output { self + (-rhs) }\n",
"}\n",
"impl std::ops::Div for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
" type Output = std::rc::Rc<CommutativeSemiring<crate::std_magnitude::Magnitude>>;\n",
" fn div(self, _rhs: Self) -> Self::Output { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
"impl<M> std::ops::Mul for GroupCompletion<M>\n",
"where M: std::ops::Add<Output = M> + std::ops::Mul<Output = M> + Clone,\n",
"{\n",
" type Output = Self;\n",
" fn mul(self, rhs: Self) -> Self::Output {\n",
" GroupCompletion {\n",
" pos: self.pos.clone() * rhs.pos.clone() + self.neg.clone() * rhs.neg.clone(),\n",
" neg: self.pos * rhs.neg + self.neg * rhs.pos,\n",
" _phantom: std::marker::PhantomData,\n",
" }\n",
" }\n",
"}\n",
"impl std::cmp::PartialEq<i64> for CommutativeSemiring<crate::std_magnitude::Magnitude> {\n",
" fn eq(&self, _other: &i64) -> bool { unimplemented!(\"interim CommutativeSemiring<Magnitude> stub — see #7197\") }\n",
"impl<M> std::ops::Div for GroupCompletion<M>\n",
"where M: std::ops::Add<Output = M> + std::ops::Sub<Output = M> + std::ops::Div<Output = M> + Default,\n",
"{\n",
" type Output = Self;\n",
" fn div(self, rhs: Self) -> Self::Output {\n",
" let q = (self.pos - self.neg) / (rhs.pos - rhs.neg);\n",
" GroupCompletion { pos: q, neg: M::default(), _phantom: std::marker::PhantomData }\n",
" }\n",
"}\n"
)
}
Expand Down
Loading
Loading