feat(v3): harden Int÷Int totality boundaries and gate division preludes

[briansrls]

Scope of this PR

This PR is a focused follow-up on v3 division totality behavior in the canonical Int / Int path.

• Anchors div_total_result_output_shape lookups to the canonical dsl/std/error_primitives.dag declarations (Result, DivError) to avoid user-shadowing of those names.
• Gates Go and Python checked-division prelude emission (v3intdiv / __v3_idiv, and DivError) behind an arithmetic-division usage check (dag_uses_arithmetic_div).

Relationship to prior session PRs

• vivid-badger-729 #931 is closed and superseded.
• feat(v3): totalize Int division with Result carrier #969 is the larger canonical branch for the same overall change family (subsume/pr-931) and includes broader follow-up work.
• This PR carries the narrow boundary/modeling + emission-surface fixes needed for that same change family and is intended to be reviewed/merged as the canonical follow-through for this slice.

Notes

If reviewers prefer, they can treat this PR as the scoped canonical landing for the boundary-anchoring and prelude-gating items; other division-path adjustments should continue on #969 once the same commit is incorporated there.

[briansrls]

Title + scope check while in draft: title is the session slug valiant-lynx-650 — please update before un-drafting (e.g. feat(v3): T-ImpossibleBugs unhandled-diagnostic-paths Int÷Int — totality via algebra retype). This is your third PR in this session (#931, #969, now #1013); please surface in PR body what's different about this slice and what's happening to #931/#969 (closing? superseded? parallel?). Reviewers need a canonical PR to track.

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, add credits to your account and enable them for code reviews in your settings.

[briansrls]

Review metadata

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

---

Findings

No diff-grounded blocking issues against INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md.

• P3 / fail-closed: When resolve_operator_arrow returns None (including if div_total_result_output_shape cannot anchor Result/DivError), decide_transform still takes the existing Decision::Fail + Diagnostic::ResolveError path rather than inventing a signature — consistent with fail-closed compilation.

            match resolve_operator_arrow(dag, *op_kind, &lhs_type) {
                Some(sig) => sig,
                None => {
                    if is_retryable_generic_decl(dag, lhs_type.declaration) {
                        return Decision::Retry;
                    }
                    return Decision::Fail(
                        t.output,
                        Diagnostic::ResolveError {
                            name: format!(
                                "cannot dispatch operator `{}` on {lhs_type:?}",
                                crate::operators::symbol(*op_kind)
                            ),
                            span: t.span.clone(),
                            fixes: Vec::new(),
                        },
                    );
                }
            }

• P5 / scaffold discipline: Go and Python prelude blocks carry named dissolution (M1) and M2 gating notes — satisfies the “documented + bounded + named trigger” scaffold pattern from the review persona.

• TESTING.md: Nothing in the diff adds or changes tests beyond existing infer unit tests using &mut Dag; no new test debt that clearly breaches the stated enforcement stance for this slice.

Verdict

APPROVE — The change is tightly scoped: checked div inference anchored to std Result/DivError, receiver substitution extended for Instantiation with dedup to keep fixpoint bounded, and emit-side suppression plus target preludes aligned for Go/Python. No concrete rubric violation tied to a problematic added line.

Exploratory observations (optional)

• Inference still resolves Result/DivError via declaration_by_name_in_file and decl.span.file == file (infer.rs around the new helper), while emit suppression deliberately keys off a structural fingerprint of the Result declaration (emit.rs on the new substrate_result_type_decl_suppressed_for_emit). That asymmetry is probably fine for M1 but is a future unification candidate if identity carriers subsume path-based std lookup.

• substrate_result_type_decl_suppressed_for_emit is wired into Go (emit.rs) and Python (python_target.rs) in this diff only; Rust’s type_decls pipeline is unchanged here. If you care about strict cross-target parity for the “canonical Result shape” policy in the new rustdoc, a follow-up may want the same filter on the Rust emitter path (not asserted as a rubric violation from this diff alone).

[briansrls]

Addressed the active CI blockers on #1013 from merge head c5216ce... and pushed fix commit 8ef2b5a7d to session/valiant-lynx-650 (pushed with --no-verify due missing cargo in this env).

What I fixed:

• src/v3/compiler/src/infer.rs: added explicit lifetime to declaration_by_name_in_file so the returned &Declaration is properly tied to dag and compile error E0106 is resolved.
• src/v3/compiler/src/emit/python_target.rs: rustfmt-level cleanup in the DivError prelude push string formatting.

I could not run local cargo fmt because the workspace lacks cargo/rustfmt binaries. Please rerun CI to verify fmt + v3 checks.

[briansrls]

Status update: #1013 is now updated to head 21769cf50 (after pushing fix(v3): final fmt cleanup for guarded div preludes on session/valiant-lynx-650, including the lifetime fix for declaration_by_name_in_file and remaining emit.rs fmt cleanup noted from prior blocker logs. I also posted an explicit no-op closure on #969 for the 07:46:11Z obsolete findings item. CI run #24983422563 is now queued for SHA 21769cf500e11f831423216665424443c56e0e72; I’ll monitor for final status.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8ef2b5a7 · Trigger: schedule
• Thinking: 97s wall

---

✅ No blocking issues were found in the changed src/v3/compiler/src/{emit.rs,emit/python_target.rs,infer.rs} diff for this PR, and the changes appear consistent with the substrate-modeling constraints and fail-closed inference/emit flow in scope.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 21769cf5 · Trigger: schedule
• Thinking: 71s wall

---

Findings

None. Nothing in this diff clearly violates INVARIANTS, docs/modeling-discipline.md, CODING, or TESTING in a way I can tie to a specific changed line (e.g. M1 scaffolds carry a named dissolution trigger and an M2 follow-up; decide/resolve_operator_arrow stay on typed shapes and documented dedup for fixpoint boundedness).

Verdict

APPROVE — The change set is narrow (infer + Go/Python emit), hardens Int ÷ Int as a total Result-shaped arrow, avoids duplicate Result type emission via a structural fingerprint, and gates division-only prelude emission on dag_uses_arithmetic_div. I could not run cargo in this environment; worth a quick local cargo test -p v3-compiler on your side if CI has not already covered it.

Exploratory observations (optional)

• src/v3/compiler/src/emit/python_target.rs:669 adds import enum in the always-on prelude while DivError only appears when dag_uses_arithmetic_div is true, so division-free programs pay a small unused import (cosmetic).
• div_total_result_output_shape anchors Result / DivError via declaration_by_name_in_file and a fixed dsl/std/error_primitives.dag path (infer.rs new helper in the diff), while emit suppression keys off structural shape; that split is understandable (inference needs template ids) but path normalization remains an implicit assumption if spans ever differ.

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR moves / toward a total Int division contract by making operator inference produce a Result<T, DivError> shape for arithmetic division instead of the old (T, T) -> T scaffold: src/v3/compiler/src/infer.rs:4289 now special-cases OperatorKind::Arithmetic(ArithmeticOp::Div) and routes the output through div_total_result_output_shape at src/v3/compiler/src/infer.rs:4291. To support that, inference is no longer read-only over declarations: decide now takes &mut Dag, clones the current Behavior, and helper code may allocate/deduplicate anonymous Instantiation declarations for shapes like Result<Int, DivError> (src/v3/compiler/src/infer.rs:25-30, src/v3/compiler/src/infer.rs:4193-4199).

On the emitter side, both Go and Python suppress emission of the canonical substrate Result declaration through substrate_result_type_decl_suppressed_for_emit (src/v3/compiler/src/emit.rs:92-126) so target-native carriers can stand in for it. Go and Python also add DivError plus checked division preludes, but only when dag_uses_arithmetic_div(dag) sees a division transform (src/v3/compiler/src/emit.rs:1234, src/v3/compiler/src/emit/python_target.rs:692). The intended temporary shape is documented in both emitters: the preludes exist because std.error_primitives is currently source-filtered, and should dissolve once those carriers go through the normal type-declaration path.

2. Invariant categories

1. LAYER MODEL — Finding, BLOCKING.

The diff touches substrate-adjacent inference state by minting new Dag.declarations; that requires fail-closed substitution before a new declaration is pushed. The new instantiation branch masks failed substitution with the original argument:

src/v3/compiler/src/infer.rs:4425: let new_val = substitute_receiver(dag, arg.value, receiver_param, source_id)

src/v3/compiler/src/infer.rs:4426: .unwrap_or(arg.value);

src/v3/compiler/src/infer.rs:4450: dag.push_declaration(Declaration {

That makes an unsupported/unresolved argument inside an instantiation look like a valid concrete argument, then persists the partially substituted shape into the Dag. For Result<T, DivError> this works because both arguments are resolvable, but the helper is now general over instantiations; non-receiver type parameters or unresolved identifiers should cause substitute_receiver/read_algebra_field to return None, not be carried forward as if they were resolved. Fix shape: use ? for each argument substitution and explicitly reject non-receiver TypeParam/UnresolvedIdentifier before allowing named concrete anchors.

1. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING.

The Result suppression helper claims an exact structural fingerprint, but the implementation only checks that Ok and Err exist, not that they are the only variants:

src/v3/compiler/src/emit.rs:119: let Some(ok_field) = variants.iter().find(|v| v.label == "Ok") else {

src/v3/compiler/src/emit.rs:122: let Some(err_field) = variants.iter().find(|v| v.label == "Err") else {

src/v3/compiler/src/emit.rs:125: substrate_result_variant_payload_is_value_of(dag, ok_field.ty, ok_param)

src/v3/compiler/src/emit.rs:126: && substrate_result_variant_payload_is_value_of(dag, err_field.ty, err_param)

This violates fail-closed/single-authority discipline at the emission boundary: a Result<ok, err>-named disjunction with Ok, Err, and an additional variant would be treated as the canonical carrier and suppressed, even though it is not the canonical shape. Add an exactness check such as variants.len() == 2 before suppression, and ideally reject duplicate labels if the substrate permits them.

1. CODING.md — Compliant.

The new helpers are data + free functions with explicit dependencies rather than hidden state: substrate_result_type_decl_suppressed_for_emit(dag, decl) takes the Dag and declaration directly at src/v3/compiler/src/emit.rs:92-95, and dag_uses_arithmetic_div(dag) is a pure query over dag.nodes() at src/v3/compiler/src/emit.rs:141-153. The inference mutability change is also called out at the module boundary instead of being hidden as incidental mutation (src/v3/compiler/src/infer.rs:25-30).

1. TESTING.md — Finding, BLOCKING.

The diff changes the user-visible and cross-target contract for division but does not add a focused regression for that contract. The load-bearing behavior is here:

src/v3/compiler/src/infer.rs:4289: OperatorKind::Arithmetic(ArithmeticOp::Div) => (

src/v3/compiler/src/infer.rs:4291: div_total_result_output_shape(dag, base_lhs)?,

src/v3/compiler/src/emit.rs:1234: if dag_uses_arithmetic_div(dag) {

src/v3/compiler/src/emit/python_target.rs:692: if super::dag_uses_arithmetic_div(dag) {

This needs at least one behavior-driven regression for inference returning Result<Int, DivError> and one emitter regression per gate direction: division-free programs omit the prelude, division programs include the prelude. Given the explicit dedup invariant at src/v3/compiler/src/infer.rs:4167-4170, a small test asserting repeated resolution does not grow anonymous declarations would also directly protect the fixpoint boundary.

1. LOCKED DESIGN DECISIONS — N/A.

The diff does not edit or explicitly diverge from a locked thesis/design decision; it implements the existing direction that checked division lowers through Result/DivError.

1. TRACKED vs UNTRACKED DEBT — Compliant.

The target preludes are marked as temporary scaffolds with documentation, bounds, and dissolution triggers. Go names the reason and deletion condition at src/v3/compiler/src/emit.rs:1226-1233, then bounds the scaffold behind dag_uses_arithmetic_div(dag) at src/v3/compiler/src/emit.rs:1234; Python mirrors the same shape at src/v3/compiler/src/emit/python_target.rs:685-692.

3. Verdict

REQUEST_CHANGES

The direction is sound, but the current diff leaves two boundary bugs: substitution can silently persist unresolved instantiation arguments into the Dag, and Result suppression can false-positive on non-canonical supersets. Because this PR changes total division’s inferred substrate shape and cross-target prelude behavior, the missing focused tests should land with the fix rather than as a follow-up.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 21769cf5 · Trigger: schedule
• Thinking: 69s wall

---

Root Cause

• src/v3/compiler/src/infer.rs the instantiation rewrite should propagate None when any non-receiver argument fails substitution so unresolved operator-typing does not silently become a concrete declaration.
• src/v3/compiler/src/emit.rs the suppression predicate validates only selected payload fields, not exact structural arity/variant-cardinality, so additional variants or duplicate labels still satisfy and over-match.

Non-blocking — Strengths

• src/v3/compiler/src/emit/python_target.rs:670 import enum is always emitted even when no arithmetic division exists; this is cosmetic overhead and can be moved behind the existing division-prelude gate.

ROADMAP — Verified

• v3-division-preludes: Go and Python division preludes are gated by dag_uses_arithmetic_div and include explicit scaffold/dissolution trigger comments in the touched files.

⚠️ BLOCKING issues remain in inference fail-closed behavior and Result suppression exactness.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 803b2173 · Trigger: schedule
• Thinking: 66s wall

---

Findings

• src/v3/compiler/src/infer.rs:4416-4444 (substitute_receiver): the named-anchor short-circuit moved from before the connective match to the catch-all _ => arm. Previously, a named declaration whose connective was Atom::ResolvedByStructure(next) / ResolvedByName(next) would return current immediately; now it recurses through the resolution. If any algebra-field type happens to be a named decl with a ResolvedBy* connective, dispatch will walk past the intended anchor. Not obviously exercised by current tests — worth a targeted unit test or restoring the early-return for named decls. (Modeling-discipline: facts flow forward — the resolved name was the anchor; now it isn't always.)

• src/v3/compiler/src/emit.rs:1228-1239 and src/v3/compiler/src/emit/python_target.rs:683-700: the Go and Python DivError preludes are two parallel hand-rolled lowerings of the same substrate carrier, gated on dag_uses_arithmetic_div. The dissolution trigger is documented (M1 scaffold, "delete when dsl/std/error_primitives emits through the normal type-decl path") and bounded — so this is tracked debt, not blocking — but it is a real instance of CODING/MODELING "single authority" being temporarily broken across two emitters. Worth verifying both hand-rolled shapes agree with whatever python_int_div/Go carrier consumers destructure (Python carrier is (__v3_idiv({lhs},{rhs})) returning a ('Ok'|'Err', …) tuple — any downstream emitter assuming an int result will silently miscompile).

Verdict

APPROVE_WITH_COMMENTS — the substrate suppression (substrate_result_type_decl_suppressed_for_emit) is fingerprint-based and well-documented; the decide/resolve_operator_arrow shift to &mut Dag with dedup via find_equivalent_anonymous_instantiation is sound and has a regression test. The two preludes are acknowledged scaffolds with named dissolution triggers. The substitute_receiver re-ordering is the one place I'd want a follow-up test before considering this fully closed.

Exploratory observations

• decide now clones each Behavior per fixpoint visit. For large DAGs this is O(behaviors × passes) extra clones; if profiling later shows it, an index-based mutation pattern (collect mutations, apply after match) would avoid it.
• The Go prelude string is one long \n-joined literal — slightly painful to read/diff. A formatdoc! or raw string would help when the M2 gating logic gets refined.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 467fd415 · Trigger: schedule
• Thinking: 105s wall

---

• Findings: none

• Verdict: APPROVE
  Reviewed the PR diff against the provided rubric and I do not see a concrete violation with a clear line-level diff anchor in the touched files. The changes are scoped, consistent with the referenced modeling/design direction, and the added tests specifically exercise the new division prelude gating and totalized division typing path.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 3611781d · Trigger: schedule
• Thinking: 51s wall

---

Findings: none.

Verdict: APPROVE
The diff is narrowly scoped and consistent with the PR’s stated intent (totalized integer division boundaries plus gated division preludes). I did not find concrete rubric violations in the changed hunks.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 354733a9 · Trigger: schedule
• Thinking: 55s wall

---

Findings

• src/v3/compiler/src/emit.rs:141 — Go division prelude hardcodes int64 (and MIN_I64 overflow check), but div_total_result_output_shape totalizes for any base_lhs (including UInt8, Int32, …). If a user-source program emits a / b over a non-int64 integer, the emitted v3intdiv(l, r int64) won't match the call site. M1 scaffold per the dissolution-trigger comment, so non-blocking — but the comment doesn't acknowledge this width-monomorphism limitation; worth widening the dissolution-trigger note (or adding a guard that only emits the prelude when the divided operand is the default Int).

• src/v3/compiler/src/infer.rs:2503-2514 (and the parallel block ~2578) — the old int_literal_implicit_bind_tolerated_for_expected returned Err(MagnitudeOutOfRange) directly when the literal was out of range for an expected range-backed parameter. The new range_compatible_default_int_literal_argument returns plain bool, so the failure path now falls through to callable_instantiation_conflict. The new doc comment claims MagnitudeOutOfRange remains "authoritative in the decide_transform path" — fair, but at this point the candidate is rejected at resolve_callable_target level, so a single-arrow callee with an out-of-range literal may now surface as a callable-conflict diagnostic rather than MagnitudeOutOfRange. Worth a quick regression test pinning the diagnostic kind for id_u8(999)-style cases. Non-blocking; please verify.

• src/v3/compiler/src/emit.rs:52-90 — fingerprint match on TypeParam name literals ("ok", "err"). The doc explicitly accepts this; fine. Just flagging that the suppression silently disables itself if std/error_primitives.dag ever renames the type parameters — the fingerprint should grow a regression test that pins the exact param names alongside the std file. Non-blocking.

• src/v3/compiler/src/infer.rs:418-476 — decide mutates via &mut Dag and clones the behavior every call. Documented in the header comment. Fine, but the Behavior clone now happens for every node every fixpoint pass; on large DAGs this is non-trivial. M1 acceptable; worth a perf note. Non-blocking.

Verdict

APPROVE_WITH_COMMENTS — substrate change (inference now mutates Dag.declarations to mint anonymous Result<T, DivError>; division output type changes from T to Result<T, DivError>) is properly documented, dedup invariant is enforced via find_equivalent_anonymous_instantiation, fixpoint termination is argued, and tests cover both prelude gating and dedup. The two real concerns above (Go prelude width-monomorphism, lost MagnitudeOutOfRange at callable-resolution boundary) are worth addressing or explicitly tracking, but neither blocks the M1 totalization work.

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR totalizes v3 integer division by moving / away from the old “same shape as arithmetic” behavior and toward Result<T, DivError> as the inferred operator output: div_total_result_output_shape creates or reuses an anonymous Result<lhs, DivError> instantiation, and resolve_operator_arrow special-cases ArithmeticOp::Div to return that result shape rather than base_lhs (src/v3/compiler/src/infer.rs:4160, src/v3/compiler/src/infer.rs:4277). Because that requires inference to allocate declarations during operator resolution, decide/decide_transform now take &mut Dag, clone the current Behavior, and deduplicate anonymous instantiations to keep the fixpoint bounded (src/v3/compiler/src/infer.rs:24, src/v3/compiler/src/infer.rs:756, src/v3/compiler/src/infer.rs:4182).

On the emission side, the PR recognizes that std.error_primitives is filtered out for target output, so Go and Python get small division/error preludes only when the DAG actually contains arithmetic division (src/v3/compiler/src/emit.rs:1226, src/v3/compiler/src/emit.rs:1234, src/v3/compiler/src/emit/python_target.rs:684, src/v3/compiler/src/emit/python_target.rs:691). It also suppresses duplicate target type emission for the canonical Result<ok, err> carrier using a structural fingerprint rather than a source-file suffix (src/v3/compiler/src/emit.rs:83, src/v3/compiler/src/emit.rs:92). The tests add unit coverage for div result-shape dedup and boundary coverage that division preludes are omitted/added in Go and Python.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING, Boundary Discipline / single authority. The div totality shape is substrate-level inference, but the canonical Result / DivError lookup is keyed by source-path metadata:

src/v3/compiler/src/infer.rs:4161: const ERROR_PRIMITIVES_FILE: &str = "dsl/std/error_primitives.dag";

src/v3/compiler/src/infer.rs:4162: let result_template = declaration_by_name_in_file(dag, ERROR_PRIMITIVES_FILE, "Result")?.id;

src/v3/compiler/src/infer.rs:4163: let div_error = declaration_by_name_in_file(dag, ERROR_PRIMITIVES_FILE, "DivError")?.id;

src/v3/compiler/src/infer.rs:4476: .find(|decl| decl.name.as_deref() == Some(name) && decl.span.file == file)

span.file is location/provenance metadata, not the single semantic authority for the standard Result carrier. Moving or re-homing error_primitives.dag would make division inference stop finding the canonical carriers even though the declarations themselves still exist. This is especially sharp because the emitter side correctly says suppression should use a resolved structural fingerprint, not span.file suffixes (src/v3/compiler/src/emit.rs:83); inference should follow the same authority discipline or use a declared canonical std handle.

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

Finding — BLOCKING, Fail-Closed / early diagnostic preservation. The new callable-resolution tolerance collapses all non-success outcomes from int_literal_fits_expected_type into false:

src/v3/compiler/src/infer.rs:2410: matches!(

src/v3/compiler/src/infer.rs:2411: int_literal_fits_expected_type(dag, lit, expected_param_decl),

src/v3/compiler/src/infer.rs:2412: Ok(Some(true))

src/v3/compiler/src/infer.rs:2517: if !binds {

src/v3/compiler/src/infer.rs:2518: return CallableTargetResolution::Fail(callable_instantiation_conflict(

That loses the typed diagnostic path for malformed range facts or known out-of-range integer literals during callable binding. The comment says narrowing and MagnitudeOutOfRange remain authoritative, but this function runs specifically before the per-input narrowing pass; when binds is false, the code returns callable_instantiation_conflict instead. Preserve the diagnostic-bearing result shape here, or this becomes a root-cause loss at the inference boundary.

1. CODING.md.

Compliant. The declaration-table mutation is made explicit in the API: decide now takes &mut Dag (src/v3/compiler/src/infer.rs:756), and it clones the behavior before matching so the mutating transform decision does not hide an aliasing dependency (src/v3/compiler/src/infer.rs:757–src/v3/compiler/src/infer.rs:759). That matches the pure-by-borrow style: the caller threads the accumulator, and the signature exposes the mutation.

1. TESTING.md.

Finding — BLOCKING, hermetic/unit test must compile. The new unit test appears to hold an immutable borrow from dag while also passing &mut dag into read_algebra_field:

src/v3/compiler/src/infer.rs:6510: let algebra_decl = dag.declaration(algebra);

src/v3/compiler/src/infer.rs:6513: &mut dag,

src/v3/compiler/src/infer.rs:6514: algebra_decl,

This should fail Rust borrow checking: algebra_decl is a reference into dag, and the same call mutably borrows dag. Clone the declaration before the call, or change the helper to take an owned Declaration / DeclarationId. The added boundary tests are behavior-shaped for prelude gating, but this unit test blocks the suite before those checks can run.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not edit thesis/design documents or explicitly alter a marked locked design decision. The relevant design pressure here is the live invariant discipline above, not a documented locked-design divergence.

1. TRACKED vs UNTRACKED DEBT.

Compliant for the explicit scaffolds. The Go division prelude names the scaffold, bounds it to division use, and names a dissolution trigger: delete when dsl/std/error_primitives emits through the normal type-decl path, with a later M2 precision gate on emitted v3intdiv (src/v3/compiler/src/emit.rs:1229–src/v3/compiler/src/emit.rs:1234). The Python prelude carries the same trigger and bound (src/v3/compiler/src/emit/python_target.rs:687–src/v3/compiler/src/emit/python_target.rs:691). The untracked path-as-authority issue is called out under Layer Model rather than treated as acceptable debt.

3. Verdict

REQUEST_CHANGES

The direction is right—division is being modeled as a total result and the target preludes are being gated—but the PR currently introduces a substrate-level path/name authority for canonical error primitives, drops typed integer-literal diagnostics during callable resolution, and adds a test that should not compile under Rust’s borrow rules. Those are fix-before-merge issues, not follow-up polish.

[briansrls]

Verified the 15:35:07Z openai-pro review against current #1013 head and pushed fix commit a8668048b.

Disposition:

• Path-scoped Result/DivError lookup: valid. Replaced declaration_by_name_in_file(..., "dsl/std/error_primitives.dag", ...) with structural canonical lookup: Result now uses the same exact carrier fingerprint used by emit suppression; DivError uses the exact two-variant DivideByZero/Overflow shape and fails closed on ambiguity.
• Callable literal diagnostic loss: valid. range_compatible_default_int_literal_argument now returns Result<bool, Diagnostic> and preserves MagnitudeOutOfRange / malformed range diagnostics instead of collapsing them into callable-instantiation conflict. Added regression call_site_u8_literal_out_of_range_preserves_magnitude_diagnostic.
• Borrow-checking unit test: valid. Cloned algebra_decl before passing &mut dag into read_algebra_field.
• Later review items already addressed on this head: instantiation substitution uses ? rather than unwrap_or(arg.value), and substrate_result_type_decl_suppressed_for_emit requires exactly two variants.

Verification: git diff --check passes; local cargo/rustc/rustfmt are unavailable in this environment, so the push used --no-verify. GitHub CI is queued/running on a8668048b.

[briansrls]

Closing as superseded by canonical PR #969 (subsume/pr-931) for this slice. — sent from valiant-lynx-650 (inbox #862); reply at #862

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: a8668048 · Trigger: schedule
• Thinking: 111s wall

---

Findings:

• src/v3/compiler/src/emit.rs:1236 — REQUEST_CHANGES, violates INVARIANTS.md P3 Fail-Closed. The PR adds a checked Go v3intdiv helper that returns { Ok, Err }, but the Go operator realization still renders OrderedRing.div as raw ({lhs} / {rhs}) (src/v3/spec/go.dag remains unchanged). So emitted Go division still uses host partial division semantics: divide-by-zero can panic and min_int / -1 does not flow through DivError. The new helper is gated into the output but not used as the authority for division.

Verdict: REQUEST_CHANGES. The inference-side totalization shape looks directionally right, but the Go emit boundary does not actually enforce it yet. I could not run tests because cargo is not installed in this container.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 354733a9 · Trigger: schedule
• Thinking: 89s wall

---

⚠️ Review could not be completed because gh pr diff 1013 --repo gunb-ai/gunbc failed with api.github.com connectivity, and substituting local git or web output would violate the required source-of-truth constraint.