feat(v3): totalize Int division with Result carrier

[briansrls]

Summary

• Totalizes v3 Int / Int inference through Result<Int, DivError> instead of a plain Int return.
• Adds the std.error_primitives algebraic carrier declarations and target prelude support needed by current emitters.
• Updates generated/bootstrap surfaces, parse manifests, and parity/boundary tests for the new carrier shape.

Relationship to #931

#969 (subsume/pr-931) is the canonical successor/subsuming branch for #931 (session/vivid-badger-729). It contains #931 plus the follow-up valiant-lynx delta and the current main conflict resolution.

Reviewers should treat #969 as the branch to carry forward once it is ready; #931 can be closed after #969 is green and no longer needed as an intermediate review artifact.

Verification

• cargo check -p v3-compiler
• cargo fmt --all --check via pre-push hook

Notes

regen_bootstrap could not be rerun in this container after the conflict merge because compiling with bootstrap-regen-fresh was SIGKILLed, and an existing generator binary on disk was for a different architecture.

[briansrls]

Verified the 2026-04-28T00:03:12Z inline blocker at emit.rs:131: this finding was valid for program-mode top-level binds. A bind named __v3_int_div, v3intdiv, or __v3_idiv shares the emitted program scope with the checked-division prelude helper and could shadow it for later division calls.

Fixed on current branch in pushed commits 03d0995cf / 68a12cae6: div_prelude_reserved_name_collision now also checks top_level_binds, and Rust/Go/Python pass their bind lists into the shared collision gate. Added regression coverage for all three targets:

• emit_rust_fails_closed_on_div_prelude_top_level_bind_collision
• emit_go_fails_closed_on_div_prelude_top_level_bind_collision
• emit_python_fails_closed_on_div_prelude_top_level_bind_collision

Verification: CARGO_TARGET_DIR=/tmp/gunbc-v3-target-bind-collision cargo test -p v3-compiler div_prelude_top_level_bind_collision -- --nocapture passed: 3 passed. New PR run is in progress; fmt has already passed.

— sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Verified the 2026-04-28T00:03:12Z inline blocker at emit.rs:206: this finding was valid. The prelude reachability scan included top-level binds and function declarations but did not include emitted type declarations, so a type field like Result<Int, DivError> or Go Result<Int, String> could render carrier names without the required prelude.

Fixed on current branch in pushed commits 53d3edcf9 / 07a96e0e5: dag_needs_div_error_prelude and dag_needs_go_result_prelude now include type_decls in the structural reachability walk. Added regression coverage for field-only usage:

• Rust emit_rust_emits_diverror_prelude_for_result_field_without_division
• Go emit_go_emits_result_carrier_for_result_field_without_division
• Go emit_go_emits_diverror_prelude_for_result_field_without_division
• Python emit_python_emits_diverror_prelude_for_result_field_without_division

Verification: CARGO_TARGET_DIR=/tmp/gunbc-v3-target-type-prelude cargo test -p v3-compiler result_field_without_division -- --nocapture passed: 4 passed. New PR run is in progress; fmt has passed.

— sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Verified the 2026-04-28T00:03:12Z inline blocker at dsl/std/algebra.dag:184 against current code. I do not think this is a current code finding.

Current std usage keeps OrderedRing on the signed integer carrier path: dsl/std/integer.dag declares Int8/Int16/Int32/Int64 as OrderedRing<...> and explicitly notes OrderedRing has signed arithmetic via negate; Float is modeled separately as Field in dsl/std/float.dag; I did not find an unbounded or non-integer OrderedRing inhabitant in the current std surface. The new / lowering is also target-realized only through the integer division operator realizations (rust_int_div, go_int_div, python_int_div) and the runtime checks map the bounded signed integer failure modes: divide by zero and min-int / -1 overflow.

So while a future M9 generalization may want a more parameterized division-error family before introducing non-bounded OrderedRing inhabitants, this PR does not currently make a non-Int OrderedRing inherit Int-only runtime behavior. No source change is required for this item as stated.

— sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 07a96e0e · Trigger: schedule
• Thinking: 33s wall

---

Findings

None that clearly violate INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md on the substance of this change.

• P3 / DB-1 (typed failure): OrderedRing.div moves to Result<T, DivError>; emit lowers / to checked helpers and collision checks fail closed instead of silently merging names — consistent with fail-closed + structured carriers.
• Practice 4 (coproduct / scaffold): dsl/std/error_primitives.dag annotates Result and DivError as YELLOW with explicit dissolution language (substrate-owned vs filtered emit / prelude).
• P5 (scaffold + trigger): Rust (rust_target.rs prelude + format!(…) for Main), Go, and Python paths carry named dissolution triggers in comments — satisfies “documented + bounded + named” for a bridge, not an undocumented steady-state duplicate authority.
• Inference: div_total_result_output_shape + substitute_receiver dedup/find_equivalent_anonymous_instantiation are documented so the fixpoint does not mint unbounded anonymous instantiations — aligns with P4-adjacent bounded-forward behavior and Practice 3 (facts carried forward intentionally).
• expect in infer.rs: New expect("std Result") / expect("std DivError") appear under #[cfg(test)] tests (e.g. 6507:6508:src/v3/compiler/src/infer.rs), not library hot paths — CODING.md allows unwrap/expect in test code.

Verdict

APPROVE — The diff matches the thesis: total integer division with a typed Result carrier, substrate declarations in error_primitives.dag, inference wired to the canonical std shapes with dedup invariants, and emit-side preludes/collisions treated as explicit, trigger-named scaffolds rather than silent defaults. I do not see a concrete rubric violation tied to a specific diff hunk.

Exploratory observations (optional)

• TESTING.md discourages pinning diagnostics via substring checks; new collision tests use message.contains("DivError") / contains("__v3_int_div") on EmitError::UnsupportedBehavior (e.g. 327:329:src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs). Variant matching is already structural; trimming substring reliance later would reduce churn if wording changes — non-blocking.
• emit.rs documents global structural suppression for substrate-shaped Result while inference keys canonical Result/DivError off dsl/std/error_primitives.dag — intentional asymmetry is explained; worth remembering if future edits split or rename that file.
• .github/workflows/ci.yml drops target/ from a cache path list — unrelated to the division feature; fine if intentional for CI, just scope noise for reviewers.

[briansrls]

Verified the bundled 2026-04-28T00:03:12Z blocking review against current head. Status by item:

1. Prelude reserved-name checking missing top-level bind names: valid, fixed in pushed commits 03d0995cf / 68a12cae6. The shared div_prelude_reserved_name_collision now checks top-level binds in addition to type/function declarations, and Rust/Go/Python all pass their bind lists. Added bind-collision tests for all three helpers. Verification: CARGO_TARGET_DIR=/tmp/gunbc-v3-target-bind-collision cargo test -p v3-compiler div_prelude_top_level_bind_collision -- --nocapture passed: 3 passed.

2. Prelude reachability missing emitted type declarations: valid, fixed in pushed commits 53d3edcf9 / 07a96e0e5. dag_needs_div_error_prelude and dag_needs_go_result_prelude now walk type_decls as well as binds/functions. Added field-only Result/DivError tests for Rust, Go, and Python. Verification: CARGO_TARGET_DIR=/tmp/gunbc-v3-target-type-prelude cargo test -p v3-compiler result_field_without_division -- --nocapture passed: 4 passed.

3. Generic OrderedRing.div / DivError modeling objection: verified separately and I do not think this is a current code finding as stated. Current std usage keeps OrderedRing on the signed integer carrier path (Int8/Int16/Int32/Int64 in dsl/std/integer.dag), while Float is a separate Field; the target realizations for / are integer-specific. A future M9 generalization may want a parameterized division-error family before adding non-bounded OrderedRing inhabitants, but this PR does not currently make a non-Int OrderedRing inherit Int-only runtime behavior.

Latest PR run after the source fixes: fmt and v3 have passed; ci and self_host_ratchet are still pending.

— sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c3909671 · Trigger: schedule
• Thinking: 262s wall

---

BLOCKING (2)

Root Cause

• src/v3/compiler/src/emit.rs Go prelude reserved-name authority is incomplete → enumerate every injected prelude identifier and check it against the full emitted identifier set before injecting helpers.

⚠️ The prior lookup/reachability fixes are mostly in place, but checked-division/Result prelude emission still has fail-open namespace collisions.

[briansrls]

BLOCKING: Fail-closed: DivError collision detection still only checks type declarations, so a user function or program Bind named DivError can collide with or shadow the injected DivError carrier.

[briansrls]

Invariant violation: BLOCKING: Fail-closed: the Go Result prelude injects v3Result/v3Ok/v3Err without checking those reserved names against user-emitted declarations, so explicit Result use can emit invalid Go.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: d8668082 · Trigger: schedule
• Thinking: 101s wall

---

Findings (if any):

• src/v3/compiler/tests/boundary/m1_4_emit_python_test.rs:168–172, src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:327–331 (and the analogous Go case src/v3/compiler/tests/boundary/m1_3_emit_go_test.rs:382–386): new tests assert on a substring of an error/diagnostic message (message.contains("DivError")). TESTING.md explicitly discourages pinning error text and prefers matching on structured shapes (variant + fields). NON-BLOCKING — the outer matches! on the typed emit error is good; dropping the contains in favor of a stable structured field or a dedicated collision variant would align fully with the doc.

Verdict: APPROVE_WITH_COMMENTS — Substrate change (OrderedRing.div → Result<T, DivError> in dsl/std/algebra.dag with dsl/std/error_primitives.dag carriers, 🟡 annotations + named dissolution text) matches P3 fail-closed / P1 faithfulness for total division; inference changes document the dedup/fixpoint contract and add focused unit tests. No blocking invariant breach spotted in the reviewed hunks.

Exploratory (optional): .github/workflows/ci.yml drops target/ from the cache paths list — looks orthogonal to “totalize Int division”; worth confirming it was intentional (CI perf vs cache correctness). infer.rs anchors canonical Result/DivError via decl.span.file == "dsl/std/error_primitives.dag" plus structural guards — reasonable for M1, but it is path-shaped authority if the file ever moves or duplicates load.

[briansrls]

Verified the 2026-04-28T00:52:41Z inline blocker at emit.rs:131 against current head d8668082f. This is already addressed.

Current div_prelude_reserved_name_collision takes top_level_binds and checks bind.name == helper_name; Go, Rust, and Python all pass top_level_binds.iter() into that shared gate before injecting their checked-division helpers. Regression tests are present for all three targets:

• emit_rust_fails_closed_on_div_prelude_top_level_bind_collision
• emit_go_fails_closed_on_div_prelude_top_level_bind_collision
• emit_python_fails_closed_on_div_prelude_top_level_bind_collision

Prior verification for this fix: CARGO_TARGET_DIR=/tmp/gunbc-v3-target-bind-collision cargo test -p v3-compiler div_prelude_top_level_bind_collision -- --nocapture passed: 3 passed. No additional source change is needed for this repeated/stale item.

— sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 7c57819c · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR makes integer-style division explicit about failure instead of pretending every division produces a value. It introduces a new bootstrap-early std.error_primitives module with Result<ok, err> and DivError, then changes OrderedRing.div from fn(T, T) -> T to fn(T, T) -> Result<T, DivError> at dsl/std/algebra.dag:184. The rest of the diff wires that new std module into the v2/v3 bootstrap closure: v2 gets a generated std_error_primitives.rs, the resolver exempts the new module from the implicit std.types dependency, v3 includes the file in bootstrap fixtures, and generated v3 DAG fixtures are regenerated with the extra declarations and shifted IDs.

The intended direction is good: division by zero and signed MIN / -1 overflow become modeled outcomes rather than target-side panics or raw / behavior. The load-bearing concern is that the new carrier is now part of substrate algebra, so its type parameters, target realizations, and tests need to be exact rather than “close enough.”

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING. This is a substrate change: dsl/std/algebra.dag:184 changes the generic algebra witness to div: fn(T, T) -> Result<T, DivError>, but the error carrier is explicitly documented as “signed integer division” at dsl/std/error_primitives.dag:14 (// 🟡 STRUCTURAL-CARRIER: signed integer division (Int / Int) failure modes). That makes an Int-specific failure domain part of every OrderedRing<T> witness. Under illegal-states-unrepresentable/modeling-faithfulness discipline, a generic OrderedRing<T> should not structurally admit DivError::Overflow unless the carrier has signed machine-int overflow semantics. Either the division error needs to be a generic algebra-level error model, or the DivError totalization should live at the integer operation/realization layer rather than on the generic OrderedRing<T> field. This is substrate, so I would not merge it as-is. chatgpt-review-38107a92-17a8-42…

1. INVARIANTS.md + modeling-discipline.md.

Finding — BLOCKING. The new Result declares its type params as ok and err (dsl/std/error_primitives.dag:12, type Result<ok, err> = Ok { value: ok } | Err { value: err }), and the generated bootstrap confirms those as AtomPayload::TypeParam("ok") / AtomPayload::TypeParam("err") at src/v3/compiler/src/bootstrap_generated.rs:20-21. But the target realizations for that same Result use {key} and {value} placeholders, for example src/v3/compiler/src/bootstrap_generated.rs:1233 contains ::core::result::Result<{key}, {value}>, with analogous Go/Python carriers at src/v3/compiler/src/bootstrap_generated.rs:1035 and src/v3/compiler/src/bootstrap_generated.rs:1132. That creates two authorities for the same generic arguments: substrate says ok/err, target strings say key/value. Unless the emitter has an undocumented positional special case for two-argument generics, this will either leave placeholders unsubstituted or bind the wrong convention. This violates single-authority metadata / facts-flow-forward: the target realization should use {ok} / {err}, or the carrier should intentionally name its params key / value everywhere. chatgpt-review-e3a95e0d-6860-4b…

1. CODING.md.

Compliant. The implementation-facing Rust shape follows the typed-carrier convention rather than a primitive/sentinel return: src/v2/stage0/src/std_algebra.rs:79 changes div to Rc<dyn Fn(T, T) -> Rc<Result<T, DivError>>>, so callers are forced to handle Ok vs Err instead of receiving a fabricated T. That matches the structured-result guidance in CODING.md. chatgpt-review-7eebc4ff-499c-44…

1. TESTING.md.

Finding — BLOCKING. The contract change at dsl/std/algebra.dag:184 is semantic, but the diff only updates bootstrap/parse fixture inclusion such as src/v2/tests/src/bootstrap.rs:513 and src/v2/tests/src/parse.rs:676; it does not add behavior-driven tests for the new division outcomes. For this change I would expect at least minimal coverage that ordinary division returns Ok, divisor zero returns Err(DivideByZero), signed MIN / -1 returns Err(Overflow), and the Rust/Go/Python target realizations compile or evaluate through the new carrier. Without those tests, the {key}/{value} mismatch above can survive regeneration unnoticed. This is a high-risk fail-closed substrate/target boundary, so the gap is blocking under the test discipline. chatgpt-review-ecde774c-f742-4a…

1. LOCKED DESIGN DECISIONS.

N/A — I did not see this diff reference or modify a design item marked locked; the changes are in std algebra/error carriers, bootstrap fixture generation, and generated v2/v3 outputs.

1. TRACKED vs UNTRACKED DEBT.

Compliant. The new carrier bridge is at least explicitly named and bounded in the source comments: dsl/std/error_primitives.dag:8-11 marks Result as a structural carrier and says it is temporary until target realizations consume the declaration directly, and dsl/std/error_primitives.dag:15-17 gives the corresponding trigger for DivError/target preludes. That satisfies the “documented, bounded, named dissolution trigger” shape for the temporary mirror.

3. Verdict

REQUEST_CHANGES. The direction is right, but the PR currently lands an Int-specific error carrier on a generic substrate algebra field and appears to mismatch Result’s declared type-parameter names with target realization placeholders. The missing behavior tests make those substrate/target issues too easy to miss.