diff --git a/compiler/src/codegen.rs b/compiler/src/codegen.rs
index da54d39..fcaf859 100644
--- a/compiler/src/codegen.rs
+++ b/compiler/src/codegen.rs
@@ -188,14 +188,15 @@ pub fn emit(module: &IrModule, module_name: &str) -> Result<String, CodegenError
     // SPEC-helper-check-propagation: a helper a fallible body executes and that can overflow
     // gets a checked copy, and only the bodies somebody calls are emitted (DP-P8).
     let checked = crate::ir::checked_helpers(module);
+    let loop_free = crate::ir::loop_free_functions(module);
     let plain = plain_bodies(module, &checked);
     for f in &module.functions {
         if plain.contains(f.name.as_str()) {
-            emit_function(f, &checked, &mut out)?;
+            emit_function(f, &checked, &loop_free, &mut out)?;
             out.push('\n');
         }
         if checked.contains(&f.name) {
-            emit_checked_copy(f, &checked, &mut out)?;
+            emit_checked_copy(f, &checked, &loop_free, &mut out)?;
             out.push('\n');
         }
     }
@@ -265,6 +266,7 @@ fn plain_bodies<'a>(module: &'a IrModule, checked: &BTreeSet<String>) -> BTreeSe
 fn emit_checked_copy(
     f: &IrFunction,
     checked: &BTreeSet<String>,
+    loop_free: &BTreeSet<String>,
     out: &mut String,
 ) -> Result<(), CodegenError> {
     // Only infallible functions are members, and an infallible function returns a scalar:
@@ -291,6 +293,7 @@ fn emit_checked_copy(
     let cx = Cx {
         abi: RetAbi::Fallible,
         checked,
+        loop_free,
     };
     for s in &f.body {
         emit_stmt(s, 1, cx, out);
@@ -302,6 +305,7 @@ fn emit_checked_copy(
 fn emit_function(
     f: &IrFunction,
     checked: &BTreeSet<String>,
+    loop_free: &BTreeSet<String>,
     out: &mut String,
 ) -> Result<(), CodegenError> {
     // An array return has no `return` statement -- the value IS the caller's buffer, and the
@@ -364,6 +368,7 @@ fn emit_function(
     let cx = Cx {
         abi: shape,
         checked,
+        loop_free,
     };
     for s in &f.body {
         emit_stmt(s, 1, cx, out);
@@ -601,6 +606,9 @@ impl RetAbi {
 struct Cx<'a> {
     abi: RetAbi,
     checked: &'a BTreeSet<String>,
+    /// `ir::loop_free_functions` — which calls may be leaves of a pure arithmetic tree
+    /// (SPEC-wide-intermediates DP-W2).
+    loop_free: &'a BTreeSet<String>,
 }
 
 fn emit_stmt(s: &IrStmt, indent: usize, cx: Cx<'_>, out: &mut String) {
@@ -877,8 +885,227 @@ fn overflow_bail(abi: RetAbi) -> Option<String> {
     }
 }
 
+/// An i32 arithmetic node: `+ - * / %` on i32 operands, or unary `-` on one.
+fn is_i32_arith(e: &IrExpr) -> bool {
+    match &e.kind {
+        IrExprKind::Binary { op, lhs, .. } => {
+            lhs.ty == IrType::I32
+                && match op {
+                    IrBinOp::Add | IrBinOp::Sub | IrBinOp::Mul | IrBinOp::Div | IrBinOp::Rem => {
+                        true
+                    }
+                    IrBinOp::Lt
+                    | IrBinOp::Gt
+                    | IrBinOp::Le
+                    | IrBinOp::Ge
+                    | IrBinOp::Eq
+                    | IrBinOp::Ne
+                    | IrBinOp::And
+                    | IrBinOp::Or => false,
+                }
+        }
+        IrExprKind::Unary { op, operand } => {
+            operand.ty == IrType::I32
+                && match op {
+                    IrUnOp::Neg => true,
+                    IrUnOp::Not => false,
+                }
+        }
+        IrExprKind::Index { .. }
+        | IrExprKind::Len { .. }
+        | IrExprKind::ByteLen(_)
+        | IrExprKind::ByteSlice { .. }
+        | IrExprKind::Fixed { .. }
+        | IrExprKind::Call { .. }
+        | IrExprKind::Concat(_)
+        | IrExprKind::Cast { .. }
+        | IrExprKind::ConstF64(_)
+        | IrExprKind::ConstStr(_)
+        | IrExprKind::ConstI32(_)
+        | IrExprKind::ConstBool(_)
+        | IrExprKind::Var(_) => false,
+    }
+}
+
+/// May this i32 expression be part of a PURE arithmetic tree (`SPEC-wide-intermediates` §2.1)?
+///
+/// An arithmetic node over pure children, or a leaf that cannot run forever and can fail only
+/// with `-3`: a variable, an i32 constant, `len(xs)`, or a call to a loop-free infallible
+/// function whose arguments are leaves too and carry no string (DP-W2). With such leaves,
+/// computing the tree exactly and checking once at its root changes no status a host can
+/// observe — a real overflow still fails before anything evaluated after the tree runs.
+///
+/// What is NOT a leaf is the whole point: an array read can fail with `-2` and would then
+/// overtake a real overflow; a call with a `while` could run forever where today's check fails
+/// first (both measured on the FULL variant, §9-71.4); `byte_len`, and a callee that takes a
+/// string, loop to the NUL byte — bounded only by the host's contract.
+fn is_pure(e: &IrExpr, cx: Cx<'_>) -> bool {
+    if is_i32_arith(e) {
+        return match &e.kind {
+            IrExprKind::Binary { lhs, rhs, .. } => is_pure(lhs, cx) && is_pure(rhs, cx),
+            IrExprKind::Unary { operand, .. } => is_pure(operand, cx),
+            IrExprKind::Index { .. }
+            | IrExprKind::Len { .. }
+            | IrExprKind::ByteLen(_)
+            | IrExprKind::ByteSlice { .. }
+            | IrExprKind::Fixed { .. }
+            | IrExprKind::Call { .. }
+            | IrExprKind::Concat(_)
+            | IrExprKind::Cast { .. }
+            | IrExprKind::ConstF64(_)
+            | IrExprKind::ConstStr(_)
+            | IrExprKind::ConstI32(_)
+            | IrExprKind::ConstBool(_)
+            | IrExprKind::Var(_) => false,
+        };
+    }
+    match &e.kind {
+        IrExprKind::Var(_) | IrExprKind::ConstI32(_) | IrExprKind::Len { .. } => true,
+        IrExprKind::Call { name, args } => {
+            cx.loop_free.contains(name) && args.iter().all(|a| is_leaf_argument(a, cx))
+        }
+        IrExprKind::Index { .. }
+        | IrExprKind::ByteLen(_)
+        | IrExprKind::ByteSlice { .. }
+        | IrExprKind::Fixed { .. }
+        | IrExprKind::Concat(_)
+        | IrExprKind::Cast { .. }
+        | IrExprKind::Unary { .. }
+        | IrExprKind::Binary { .. }
+        | IrExprKind::ConstF64(_)
+        | IrExprKind::ConstStr(_)
+        | IrExprKind::ConstBool(_) => false,
+    }
+}
+
+/// An argument of a call leaf: no string, and itself a variable, a constant, or pure.
+fn is_leaf_argument(a: &IrExpr, cx: Cx<'_>) -> bool {
+    if a.ty == IrType::Str {
+        return false;
+    }
+    match &a.kind {
+        IrExprKind::Var(_)
+        | IrExprKind::ConstI32(_)
+        | IrExprKind::ConstF64(_)
+        | IrExprKind::ConstBool(_) => true,
+        IrExprKind::Index { .. }
+        | IrExprKind::Len { .. }
+        | IrExprKind::ByteLen(_)
+        | IrExprKind::ByteSlice { .. }
+        | IrExprKind::Fixed { .. }
+        | IrExprKind::Call { .. }
+        | IrExprKind::Concat(_)
+        | IrExprKind::Cast { .. }
+        | IrExprKind::Unary { .. }
+        | IrExprKind::Binary { .. }
+        | IrExprKind::ConstStr(_) => is_pure(a, cx),
+    }
+}
+
+/// The exact (i64) value of a pure tree, operands bound left to right (§2.2). Only emitted in a
+/// fallible context: `+ - *`, `/` and unary `-` still fail with `-3` if i64 itself overflows
+/// (DP-W5), a zero divisor gives `0` (DP-N4) and `%` is the true remainder (DP-O5). `bail` is
+/// the fallible context's `overflow_bail`, which [`emit_wide`] has already found.
+fn emit_exact(e: &IrExpr, cx: Cx<'_>, bail: &str) -> String {
+    if !is_i32_arith(e) {
+        return format!("(({}) as i64)", emit_expr(e, cx));
+    }
+    let checked = |method: &str| {
+        format!("match __wl.{method}(__wr) {{ Some(__o) => __o, None => {{ {bail} }} }}")
+    };
+    match &e.kind {
+        IrExprKind::Binary { op, lhs, rhs } => {
+            let l = emit_exact(lhs, cx, bail);
+            let r = emit_exact(rhs, cx, bail);
+            let body = match op {
+                IrBinOp::Add => checked("checked_add"),
+                IrBinOp::Sub => checked("checked_sub"),
+                IrBinOp::Mul => checked("checked_mul"),
+                IrBinOp::Div => format!(
+                    "if __wr == 0 {{ 0i64 }} else {{ {} }}",
+                    checked("checked_div")
+                ),
+                IrBinOp::Rem => {
+                    "if __wr == 0 { 0i64 } else { __wl.wrapping_rem(__wr) }".to_string()
+                }
+                IrBinOp::Lt
+                | IrBinOp::Gt
+                | IrBinOp::Le
+                | IrBinOp::Ge
+                | IrBinOp::Eq
+                | IrBinOp::Ne
+                | IrBinOp::And
+                | IrBinOp::Or => unreachable!("is_i32_arith admits arithmetic operators only"),
+            };
+            format!("{{ let __wl: i64 = {l}; let __wr: i64 = {r}; {body} }}")
+        }
+        IrExprKind::Unary { operand, .. } => format!(
+            "(match ({}).checked_neg() {{ Some(__o) => __o, None => {{ {bail} }} }})",
+            emit_exact(operand, cx, bail)
+        ),
+        IrExprKind::Index { .. }
+        | IrExprKind::Len { .. }
+        | IrExprKind::ByteLen(_)
+        | IrExprKind::ByteSlice { .. }
+        | IrExprKind::Fixed { .. }
+        | IrExprKind::Call { .. }
+        | IrExprKind::Concat(_)
+        | IrExprKind::Cast { .. }
+        | IrExprKind::ConstF64(_)
+        | IrExprKind::ConstStr(_)
+        | IrExprKind::ConstI32(_)
+        | IrExprKind::ConstBool(_)
+        | IrExprKind::Var(_) => unreachable!("is_i32_arith admits Binary and Unary only"),
+    }
+}
+
+/// `SPEC-wide-intermediates`: in a fallible body a pure tree is computed exactly and narrowed
+/// ONCE, at its root — whatever takes the value (`let`, argument, index, `as f64`, `return`, an
+/// impure parent). A comparison whose two sides are pure compares the exact values and narrows
+/// nothing (DP-W4). `None` means the ordinary lowering below applies.
+fn emit_wide(e: &IrExpr, cx: Cx<'_>) -> Option<String> {
+    let bail = overflow_bail(cx.abi)?;
+    if is_i32_arith(e) && is_pure(e, cx) {
+        return Some(format!(
+            "(match i32::try_from({}) {{ Ok(__n) => __n, Err(_) => {{ {bail} }} }})",
+            emit_exact(e, cx, &bail)
+        ));
+    }
+    let IrExprKind::Binary { op, lhs, rhs } = &e.kind else {
+        return None;
+    };
+    let comparison = match op {
+        IrBinOp::Lt | IrBinOp::Gt | IrBinOp::Le | IrBinOp::Ge | IrBinOp::Eq | IrBinOp::Ne => true,
+        IrBinOp::Add
+        | IrBinOp::Sub
+        | IrBinOp::Mul
+        | IrBinOp::Div
+        | IrBinOp::Rem
+        | IrBinOp::And
+        | IrBinOp::Or => false,
+    };
+    // Typeck gives both sides of a comparison one type, so `lhs` answers for `rhs` too.
+    if comparison
+        && lhs.ty == IrType::I32
+        && (is_i32_arith(lhs) || is_i32_arith(rhs))
+        && is_pure(lhs, cx)
+        && is_pure(rhs, cx)
+    {
+        return Some(format!(
+            "{{ let __wl: i64 = {}; let __wr: i64 = {}; __wl {} __wr }}",
+            emit_exact(lhs, cx, &bail),
+            emit_exact(rhs, cx, &bail),
+            op_str(*op)
+        ));
+    }
+    None
+}
+
 fn emit_expr(e: &IrExpr, cx: Cx<'_>) -> String {
     let abi = cx.abi;
+    if let Some(wide) = emit_wide(e, cx) {
+        return wide;
+    }
     match &e.kind {
         // `xs[i]`, bounds-checked (SPEC-array-input 2.3).
         //
diff --git a/compiler/src/ir.rs b/compiler/src/ir.rs
index 1ef0b86..f9bb26c 100644
--- a/compiler/src/ir.rs
+++ b/compiler/src/ir.rs
@@ -761,6 +761,53 @@ pub fn module_can_fail_overflow(module: &IrModule) -> bool {
     })
 }
 
+/// The infallible functions that always return: no `while` in their body, and none in any
+/// module function they call (`SPEC-wide-intermediates` §2.1, DP-W2). Recursion is rejected, so
+/// such a call terminates; a name that is not a module function is a built-in rounder, which
+/// terminates too.
+///
+/// A call to one of these — with no string argument — may be a leaf of a pure arithmetic tree:
+/// it cannot run forever, and under helper check propagation it can fail only with `-3`, so
+/// deferring the tree's own check past it changes nothing a host can observe. The string
+/// condition is the caller's to check (codegen): a callee that takes a string runs `==` or
+/// `byte_len` over it, loops bounded only by the host's NUL contract.
+pub fn loop_free_functions(module: &IrModule) -> BTreeSet<String> {
+    fn has_while(body: &[IrStmt]) -> bool {
+        body.iter().any(|s| match s {
+            IrStmt::While { .. } => true,
+            IrStmt::If { body, .. } => has_while(body),
+            IrStmt::ResultSet { .. }
+            | IrStmt::ResultLen(_)
+            | IrStmt::Return(_)
+            | IrStmt::Let { .. }
+            | IrStmt::Assign { .. }
+            | IrStmt::AssignOut { .. }
+            | IrStmt::TryCall { .. }
+            | IrStmt::Fail(_) => false,
+        })
+    }
+    let names: BTreeSet<&str> = module.functions.iter().map(|f| f.name.as_str()).collect();
+    let mut free: BTreeSet<String> = BTreeSet::new();
+    // Fixed point over the DAG: a function joins once every module function it calls has.
+    loop {
+        let before = free.len();
+        for f in module.functions.iter().filter(|f| !f.fallible) {
+            if free.contains(&f.name) || has_while(&f.body) {
+                continue;
+            }
+            if expression_callees(&f.body)
+                .into_iter()
+                .all(|c| free.contains(c) || !names.contains(c))
+            {
+                free.insert(f.name.clone());
+            }
+        }
+        if free.len() == before {
+            return free;
+        }
+    }
+}
+
 /// Does this body compare a span anywhere? — `SPEC-string-slice-compare` DP-C2.
 ///
 /// The companion to [`first_index`], and it exists for the same stated reason: `check_expr`
diff --git a/compiler/tests/golden/generated.rs.txt b/compiler/tests/golden/generated.rs.txt
index e7d4a5f..406f4a6 100644
--- a/compiler/tests/golden/generated.rs.txt
+++ b/compiler/tests/golden/generated.rs.txt
@@ -301,8 +301,8 @@ fn ml_fn_allocate(stock: *const i32, stock_len: i32, want: i32, ml_buf: *mut i32
             if __i < 0 || __i >= __n { return -2; }
             unsafe { *ml_buf.add(__i as usize) = take; }
         }
-        left = (match (left).checked_sub(take) { Some(__o) => __o, None => { return -3; } });
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
+        left = (match i32::try_from({ let __wl: i64 = ((left) as i64); let __wr: i64 = ((take) as i64); match __wl.checked_sub(__wr) { Some(__o) => __o, None => { return -3; } } }) { Ok(__n) => __n, Err(_) => { return -3; } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return -3; } } }) { Ok(__n) => __n, Err(_) => { return -3; } });
     }
     0
 }
@@ -328,7 +328,7 @@ fn ml_fn_in_stock(stock: *const i32, stock_len: i32, ml_buf: *mut bool, ml_cap:
             if __i < 0 || __i >= __n { return -2; }
             unsafe { *ml_buf.add(__i as usize) = ({ let __i = i; if __i < 0 || __i >= stock_len { return -2; } unsafe { *stock.add(__i as usize) } } > 0i32); }
         }
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return -3; } } }) { Ok(__n) => __n, Err(_) => { return -3; } });
     }
     0
 }
@@ -354,7 +354,7 @@ pub extern "C" fn ml_module_abi_version() -> u32 { 1 }
 pub extern "C" fn ml_iface_hash_basket() -> u64 { 0x5D04BA666CC0CBC6 }
 
 fn ml_ck_line_total(q: i32, p: i32) -> Result<i32, i32> {
-    return Ok((match (q).checked_mul(p) { Some(__o) => __o, None => { return Err(-3); } }));
+    return Ok((match i32::try_from({ let __wl: i64 = ((q) as i64); let __wr: i64 = ((p) as i64); match __wl.checked_mul(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }));
 }
 
 fn ml_fn_basket_total(qty: *const i32, qty_len: i32, price: *const i32, price_len: i32, cap: i32) -> Result<i32, i32> {
@@ -366,12 +366,12 @@ fn ml_fn_basket_total(qty: *const i32, qty_len: i32, price: *const i32, price_le
     while (i < qty_len) {
         let line = (match ml_ck_line_total({ let __i = i; if __i < 0 || __i >= qty_len { return Err(-2); } unsafe { *qty.add(__i as usize) } }, { let __i = i; if __i < 0 || __i >= price_len { return Err(-2); } unsafe { *price.add(__i as usize) } }) { Ok(__v) => __v, Err(__e) => { return Err(__e); } });
         if (line > cap) {
-            total = (match (total).checked_add(cap) { Some(__o) => __o, None => { return Err(-3); } });
+            total = (match i32::try_from({ let __wl: i64 = ((total) as i64); let __wr: i64 = ((cap) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
         }
         if (line <= cap) {
-            total = (match (total).checked_add(line) { Some(__o) => __o, None => { return Err(-3); } });
+            total = (match i32::try_from({ let __wl: i64 = ((total) as i64); let __wr: i64 = ((line) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
         }
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
     }
     return Ok(total);
 }
@@ -387,7 +387,7 @@ fn ml_fn_largest(xs: *const f64, xs_len: i32, floor: f64) -> Result<f64, i32> {
         if ({ let __i = i; if __i < 0 || __i >= xs_len { return Err(-2); } unsafe { *xs.add(__i as usize) } } > best) {
             best = { let __i = i; if __i < 0 || __i >= xs_len { return Err(-2); } unsafe { *xs.add(__i as usize) } };
         }
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
     }
     return Ok(best);
 }
@@ -410,7 +410,7 @@ fn ml_fn_any_set(flags: *const bool, flags_len: i32) -> Result<bool, i32> {
         if { let __i = i; if __i < 0 || __i >= flags_len { return Err(-2); } unsafe { *flags.add(__i as usize) } } {
             return Ok(true);
         }
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
     }
     return Ok(false);
 }
@@ -1356,7 +1356,7 @@ fn ml_fn_replay(start: i32, events: *const i32, events_len: i32) -> Result<i32,
     let mut i = 0i32;
     while (i < events_len) {
         s = match ml_fn_next_state(s, { let __i = i; if __i < 0 || __i >= events_len { return Err(-2); } unsafe { *events.add(__i as usize) } }) { Ok(__v) => __v, Err(__e) => return Err(__e) };
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return Err(-3); } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
     }
     return Ok(s);
 }
@@ -1436,7 +1436,7 @@ fn ml_fn_boxes_checked(qty: i32, per_box: i32) -> Result<i32, i32> {
     if (per_box == 0i32) {
         return Err(1);
     }
-    return Ok({ let __l = qty; let __d = per_box; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return Err(-3); } else { __l.wrapping_div(__d) } });
+    return Ok((match i32::try_from({ let __wl: i64 = ((qty) as i64); let __wr: i64 = ((per_box) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return Err(-3); } } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }));
 }
 #[no_mangle]
 pub extern "C" fn mlx_boxes_checked(qty: i32, per_box: i32, out_value: *mut i32) -> i32 {
@@ -1630,7 +1630,7 @@ fn ml_fn_receipt_line(item: *const u8, qty: i32, unit_price: i32, ml_buf: *mut u
     let __p1 = b" x \0".as_ptr();
     let __p2 = qty;
     let __p3 = b" = \0".as_ptr();
-    let __p4 = (match (qty).checked_mul(unit_price) { Some(__o) => __o, None => { return -3; } });
+    let __p4 = (match i32::try_from({ let __wl: i64 = ((qty) as i64); let __wr: i64 = ((unit_price) as i64); match __wl.checked_mul(__wr) { Some(__o) => __o, None => { return -3; } } }) { Ok(__n) => __n, Err(_) => { return -3; } });
     let mut __n: i32 = 1;
     __n += ml_slen(__p0);
     __n += ml_slen(__p1);
@@ -1786,9 +1786,9 @@ fn ml_fn_schedule(principal: i32, months: i32, ml_buf: *mut i32, ml_cap: i32, ml
         {
             let __i = i;
             if __i < 0 || __i >= __n { return -2; }
-            unsafe { *ml_buf.add(__i as usize) = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return -3; } else { __l.wrapping_div(__d) } }; }
+            unsafe { *ml_buf.add(__i as usize) = (match i32::try_from({ let __wl: i64 = ((principal) as i64); let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return -3; } } } }) { Ok(__n) => __n, Err(_) => { return -3; } }); }
         }
-        i = (match (i).checked_add(1i32) { Some(__o) => __o, None => { return -3; } });
+        i = (match i32::try_from({ let __wl: i64 = ((i) as i64); let __wr: i64 = ((1i32) as i64); match __wl.checked_add(__wr) { Some(__o) => __o, None => { return -3; } } }) { Ok(__n) => __n, Err(_) => { return -3; } });
     }
     0
 }
@@ -1806,9 +1806,9 @@ fn ml_fn_one_payment(principal: i32, months: i32, month: i32) -> Result<i32, i32
     if (month >= months) {
         return Err(1);
     }
-    let base = { let __l = principal; let __d = months; if __d == 0 { 0i32 } else if __d == -1 && __l == i32::MIN { return Err(-3); } else { __l.wrapping_div(__d) } };
+    let base = (match i32::try_from({ let __wl: i64 = ((principal) as i64); let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { match __wl.checked_div(__wr) { Some(__o) => __o, None => { return Err(-3); } } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } });
     if (month == 0i32) {
-        return Ok((match (base).checked_add({ let __l = principal; let __d = months; if __d == 0 { 0i32 } else { __l.wrapping_rem(__d) } }) { Some(__o) => __o, None => { return Err(-3); } }));
+        return Ok((match i32::try_from({ let __wl: i64 = ((base) as i64); let __wr: i64 = { let __wl: i64 = ((principal) as i64); let __wr: i64 = ((months) as i64); if __wr == 0 { 0i64 } else { __wl.wrapping_rem(__wr) } }; match __wl.checked_add(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }));
     }
     return Ok(base);
 }
@@ -1893,7 +1893,7 @@ fn ml_fn_bump(n: i32) -> Result<i32, i32> {
     if (n < 0i32) {
         return Err(1);
     }
-    return Ok((match (n).checked_sub(7i32) { Some(__o) => __o, None => { return Err(-3); } }));
+    return Ok((match i32::try_from({ let __wl: i64 = ((n) as i64); let __wr: i64 = ((7i32) as i64); match __wl.checked_sub(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }));
 }
 #[no_mangle]
 pub extern "C" fn mlx_bump(n: i32, out_value: *mut i32) -> i32 {
@@ -1941,7 +1941,7 @@ fn ml_fn_grade(n: i32, tier: *mut i32) -> Result<i32, i32> {
         return Err(1);
     }
     unsafe { *tier = 1i32; }
-    return Ok((match (n).checked_mul(10i32) { Some(__o) => __o, None => { return Err(-3); } }));
+    return Ok((match i32::try_from({ let __wl: i64 = ((n) as i64); let __wr: i64 = ((10i32) as i64); match __wl.checked_mul(__wr) { Some(__o) => __o, None => { return Err(-3); } } }) { Ok(__n) => __n, Err(_) => { return Err(-3); } }));
 }
 #[no_mangle]
 pub extern "C" fn mlx_grade(n: i32, tier: *mut i32, out_value: *mut i32) -> i32 {
diff --git a/docs/HOST_ABI.md b/docs/HOST_ABI.md
index 62394a4..d84b45d 100644
--- a/docs/HOST_ABI.md
+++ b/docs/HOST_ABI.md
@@ -58,6 +58,8 @@
   `+ - *`, 단항 `-`, `i32::MIN / -1`, 그리고 NaN이거나 절단 뒤 i32 밖인 변환. **호스트가 무한 함수를 직접
   부르면 그대로 wrap·포화한다** — status 채널이 없다. 생성 `.h`·`.pas`는 그 상수를 **낼 수 있는 모듈에만**
   선언하고, 헬퍼를 거쳐서만 낼 수 있는 모듈도 그렇다. `-3`도 절단이 아니다(아래 Q12 표).
+  **순수 산술 식은 정확히 계산되고 i32로 좁혀지는 자리에서 한 번 검사된다**(`SPEC-wide-intermediates`) —
+  중간값만 넘치는 `a * b / b`는 `-3`이 아니라 `a`다(`b ≠ 0`일 때 — `b = 0`이면 여전히 `0`). 시그니처·지문·생성 바인딩은 바뀌지 않는다.
 - 마샬링은 **스칼라와 문자열**: `f64`/`bool`/`i32`, 그리고 아래에 적은 범위의 `string`.
   (이 줄은 "스칼라만"이었다 — 바로 아래 두 줄이 문자열 입력과 반환을 구현됐다고 적는 동안
   그대로 남아 있었다. 한 불릿이 자기 자신과 모순됐다.) 실패 가능 함수는 D17대로
diff --git a/docs/LANGUAGE.md b/docs/LANGUAGE.md
index dc90417..3d85c37 100644
--- a/docs/LANGUAGE.md
+++ b/docs/LANGUAGE.md
@@ -155,11 +155,23 @@
     산술에서 틀린다. **조용하다** — 무한 함수에는 호스트가 들을 채널이 없다(D17).
   - **같은 헬퍼가 부르는 쪽에 따라 다르게 동작한다.** `fn sq(x: i32) -> i32 { return x * x }`는
     `!` 함수가 부르면 `sq(46341)`이 `-3`, 무한 함수가 부르면 `-2147479015`다(측정,
-    `helper_check_propagation.rs`). 그 대신 식을 헬퍼로 빼도 답이 바뀌지 않는다. **의도한 wrap을
-    쓰는 탈출구는 없다** — 무한 헬퍼가 그 역할을 하던 규칙은 뒤집혔다(DP-P10). 리터럴만의 오버플로(`2147483647 + 1`)는
-    컴파일 에러가 아니라 **실행 시 `-3`**이다(DP-O9). 참값이 i32에 드는데 중간값만 넘쳐도
-    실패한다(`a * 2 / 2`가 `a = 2^30`에서 `-3`, 측정) — 정답을 주는 것은 `i64`뿐이고, 그것은
-    아래 공백 블록에 있다.
+    `helper_check_propagation.rs`). **의도한 wrap을 쓰는 탈출구는 없다** — 무한 헬퍼가 그 역할을
+    하던 규칙은 뒤집혔다(DP-P10).
+  - **`!` 문맥의 순수 산술 식은 정확히 계산되고, 값이 i32가 되어야 하는 자리에서 한 번 검사된다**
+    (SPEC-wide-intermediates). 잎이 변수 · i32 상수 · `len` · **`while`이 없고 문자열을 받지 않는 무한
+    함수의 호출**뿐인 식은 i64로 계산해, 그 값을 받는 자리(`let` · 대입 · `return` · 인자 · 인덱스 ·
+    `as f64` · 순수하지 않은 부모 연산)에서 i32로 좁힌다 — 들지 않으면 `-3`. 그래서 `a * 2 / 2`는
+    `a = 2^30`에서도 `a`, `(a + b) / 2`는 `a = b = 2000000000`에서 `2000000000`, 비교 `a + b > 0`은
+    정확한 값끼리라 `i32::MAX, 1`에서 `true`다. 리터럴만의 식도 같다: `2147483647 + 1`은 실행 시 `-3`,
+    `2147483647 + 1 - 1`은 `2147483647`(DP-O9를 정확한 값 기준으로 다시 썼다). i64마저 넘치면 `-3`
+    (전부 측정, `wide_intermediates.rs`). 배열 읽기 · `while`이 있는 호출 · 문자열을 받는 호출이 든
+    연산자는 오늘처럼 **그 자리에서** 검사된다 — 그래서 `a * b + xs[5]`는 `-3`이고 뒤의 인덱스 실패가
+    진짜 오버플로를 앞지르지 않는다. 무한 본문은 그대로 연산자마다 wrap한다. **후속 백엔드 주의:**
+    C는 부호 있는 정수의 오버플로를 정의하지 않으므로, D19가 열어 둔 C-emit 백엔드는 이 계산을
+    **검사하는 64비트 연산으로 명시적으로** 구현해야 한다 — 위 평가 순서 경고와 같은 부류다.
+  - **대가 — 좁히는 자리로 빼면 답이 바뀐다.** 중간값을 `let`에 담거나 헬퍼로 빼서 그 `return`을
+    지나게 하면 거기서 좁혀진다: `x * x / x`는 `46341`에서 `46341`인데 `let t = x * x  return t / x`와
+    `sq(x) / x`는 `-3`이다(측정, `wide_intermediates.rs`). 정답을 끝까지 주는 것은 `i64` 타입뿐이고, 그것은 아래 공백 블록에 있다.
 - **`f64`의 `/`는 전역이 아니다 — `inf`·`NaN`이 그대로 호스트로 간다**(2026-09-16 실측,
   `STATUS.md` §9-61). 바로 위 두 항목이 `i32`에 대해 말하는 것과 **반대**이고, 그 대비가 이 줄의
   이유다. 로드된 모듈에서 잰 값:
diff --git a/docs/STATUS.md b/docs/STATUS.md
index 9a99329..c23ddb5 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -235,9 +235,10 @@
 >
 > **▶ 다음 세션 — 여기서 시작한다.** 순서대로:
 >
-> 1. **넓은 중간값 SPEC 확인 — 사용자 결정.** 초안은 `docs/slices/SPEC-wide-intermediates.md`이고 §4의 DP-W1~W11이
->    확인을 기다린다(방향 포함). 헬퍼 체크 전파 뒤로 네 변형을 다시 쟀고, 권고는 **순수 트리만**(멈춤·앞지름 없이 참값이
->    드는데 `-3`인 행 59 → 20)이다. 시험 구현은 로컬 브랜치 `exp/wide2-local`에 있다(푸시 안 함).
+> 1. **넓은 중간값 — 확정(2026-09-27), 구현 중.** `docs/slices/SPEC-wide-intermediates.md`의 DP-W1~W11을 권고안대로
+>    확인받았다(**순수 트리만** — 멈춤·앞지름 없이 참값이 드는데 `-3`인 행 59 → 20). §6 작업 1(codegen)이 들어가면 남는 것은
+>    작업 2 — 기존 예제의 한 식을 실제 C 호스트로 재고, 626행을 구현본으로 다시 잰다. 시험 구현은 로컬 브랜치
+>    `exp/wide2-local`에 있다(푸시 안 함).
 > 2. **작은 항목**: C# 호스트(Phase 4) · LSP(Phase 3, 큰 일).
 > 3. **외부**: `X1`·`X2` — Delphi가 있는 CI 러너. 이 저장소 안에서는 닫히지 않는다.
 >
diff --git a/docs/slices/README.md b/docs/slices/README.md
index f1d7c2f..a1245f0 100644
--- a/docs/slices/README.md
+++ b/docs/slices/README.md
@@ -64,7 +64,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방
 | [상수 선언 `const` · `export const`](SPEC-constants.md) | ✅ **구현 완료** (2026-09-26) | 이름 붙은 리터럴 — `export const`만 헤더(`ML_<MODULE>_CONST_<NAME>`)와 지문에 나가, 번호를 바꾼 모듈을 게이트가 거부한다 | #325 / #326·#327 |
 | [체크드 정수 산술](SPEC-checked-arithmetic.md) | ✅ **구현 완료** (2026-09-26) | `!` 본문의 i32 오버플로와 `f64 as i32`가 `ML_ST_OVERFLOW`(`-3`)로 실패한다 — 조용한 오답 161행 중 101이 status가 된다 | §9-69 / #334 · §9-70 |
 | [헬퍼 체크 전파](SPEC-helper-check-propagation.md) | ✅ **구현 완료** (2026-09-26) | `!` 함수가 부른 무한 함수(export 포함)의 산술도 검사하고 `-3`을 전파한다 — 조용한 오답 60 → 44 | §9-71 / #339 · §9-72 |
-| [넓은 중간값](SPEC-wide-intermediates.md) | 🔨 **SPEC 초안 · 확인 대기** (2026-09-26) | `!` 문맥의 순수 산술 식을 정확히 계산하고 뿌리에서만 좁힌다 — 참값이 드는데 `-3`인 행 59 → 20, DP-W1~W11 확인 대기 | §9-71 · §9-72 / — |
+| [넓은 중간값](SPEC-wide-intermediates.md) | 🔨 **확정 · 구현 중** (2026-09-27) | `!` 문맥의 순수 산술 식을 정확히 계산하고 뿌리에서만 좁힌다 — 참값이 드는데 `-3`인 행 59 → 20(시험 구현) | §9-71 · §9-72 / #341 |
 
 > **2026-09-25에 행을 한 줄로 접었다.** 접기 전의 서술은 [`../history/slices-index.md`](../history/slices-index.md)에
 > 바이트 그대로 있다. **새 행도 한 줄로 쓴다** — 행당 400 B(`every_slice_index_row_is_one_line`)이고, 경위는 그
@@ -127,7 +127,7 @@ TDD 구현 → Grok 검증 → PR** 순서를 따른다(`CLAUDE.md` "개발 방
 두 번째 호스트(C#, ROADMAP Phase 4), 그리고 ROADMAP Phase 2가 이름만 두고 설계가 없던 둘 —
 **인터페이스 정의 파일**(설계부터)과 **개발/배포 빌드 분리**(D13, `SECURITY.md` P1).
 *(2026-09-25 로드맵 검토에서 더했다 — Phase 2의 다섯 항목 중 이 둘이 이 목록에 없었다.)*
-§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **넓은 중간값**(SPEC 초안이 있다, 위 색인), **`wrapping_*` 내장 함수**(무한 헬퍼라는 탈출구(DP-O7)가 §9-72로 사라졌다 — 필요가 측정되면), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자,
+§7(§9-69, 12개 도메인 72규칙과 귀속 대조)이 더한 후보: **넓은 중간값**(SPEC 확정 · 구현 중, 위 색인), **`wrapping_*` 내장 함수**(무한 헬퍼라는 탈출구(DP-O7)가 §9-72로 사라졌다 — 필요가 측정되면), **i64**(§9-71: 옵트인이라 귀속 대조에서 51행이 빠졌다), **입력 문자열의 인코딩 계약**(닫힌 DP-S2의 재개 — `OPEN_QUESTIONS.md` Q17이 (A)로 열어 두었고 재검토 조건은 거기 있다), 비트 연산자,
 지역 작업 배열, 수학 내장 함수, 문자 단위 길이.
 **struct는 §9-1이 강제되지 않는다고 결론냈다** — 고르려면 그 절을 먼저 읽는다(§9-69도 귀속 0으로 다시 확인했다).
 배열도 같은 결론이었고(§9-9가 다섯 번째로), **입력은 그 사실을 SPEC 첫 절에 적은 채로 열렸다**.
diff --git a/docs/slices/SPEC-wide-intermediates.md b/docs/slices/SPEC-wide-intermediates.md
index e2f98ed..06af8ca 100644
--- a/docs/slices/SPEC-wide-intermediates.md
+++ b/docs/slices/SPEC-wide-intermediates.md
@@ -1,8 +1,7 @@
 # SPEC — 넓은 중간값 (순수 산술 식은 정확히 계산하고, 뿌리에서만 좁힌다)
 
-- **상태: 초안. 사용자 확인 전이며 제품 코드는 한 줄도 쓰지 않았다.**
-  - 이 문서가 묻는 것은 **§4의 결정 전부**다 — 방향(DP-W1)도 아직 확인받지 않았다. §9-72.7이 가장 가까운 후보로 적었고,
-    사용자가 *"후속작업을 이어서"* 를 요청했다(2026-09-26).
+- **상태: 확정 · 구현 중.** §4의 DP-W1~W11을 사용자가 권고안대로 확인했다(2026-09-27). §6의 작업 1이 codegen이고,
+  작업 2(실제 C 호스트 · 626행 재측정)가 슬라이스를 닫는다.
 - 선행: `SPEC-checked-arithmetic.md`(§2.1 — 검사 자리는 **연산자** · DP-O9 — 리터럴만의 오버플로는 실행 시 `-3`) ·
   `SPEC-helper-check-propagation.md`(검사된 사본도 fallible 문맥이다)
 - 관련 결정: **D17**(음수 status 예약) · **D19**(C-emit 백엔드의 여지)
@@ -139,6 +138,8 @@ DP-O9(*"리터럴만의 오버플로는 실행 시 `-3`"*)는 *"정확한 값이
 
 - **`let` 추출이 답을 바꾼다** — `let`은 좁히는 자리다. `return a*b/b`는 값, `let t = a*b  return t/b`는 `-3`. 지역 변수의
   폭은 i32로 둔다(넓히면 언어 모델이 바뀐다).
+- **헬퍼로 빼도 답이 바뀐다** — 헬퍼의 `return`도 좁히는 자리다. `x*x/x`는 `46341`에서 `46341`, `sq(x)/x`는 `-3`
+  (구현 중 측정, `wide_intermediates.rs`). 호출 잎은 헬퍼가 **돌려준 i32**를 잎으로 받을 뿐 그 안의 식을 넓히지 않는다.
 - **같은 식이 문맥에 따라 다르다** — 무한 본문에서는 연산자마다 wrap한다. 체크드 산술이 이미 만든 차이가 넓어진다.
 - **배열 읽기가 든 식은 좋아지지 않는다** — 표본에서 3행(PURE+CALL과 FULL의 차이, stateful R4). 배열 읽기를 잎으로 받으면
   (PURE+INDEX) 되찾지만 §0.3의 두 번째 위험 — 뒤의 `-2`가 진짜 오버플로를 앞지르는 것 — 을 다시 연다.
@@ -174,7 +175,7 @@ MSVC 19.44는 `<stdckdint.h>`·`__builtin_mul_overflow`를 받지 않는다(§9-
 
 ---
 
-## 4. 설계 결정 (확인 요청)
+## 4. 설계 결정 (확정 — 사용자 확인 2026-09-27)
 
 | DP | 결정 | 대안 | 근거 |
 |---|---|---|---|
diff --git a/hosts/rust-oracle/tests/checked_arithmetic.rs b/hosts/rust-oracle/tests/checked_arithmetic.rs
index 913d3bb..2a84b69 100644
--- a/hosts/rust-oracle/tests/checked_arithmetic.rs
+++ b/hosts/rust-oracle/tests/checked_arithmetic.rs
@@ -196,20 +196,21 @@ fn infallible_bodies_still_wrap_and_literals_are_checked() {
     drop(m);
 }
 
-/// **The cost the SPEC names (§0.3): a true answer that fits still fails if a step does not.**
+/// **The cost this SPEC named (§0.3) — and `SPEC-wide-intermediates` removed for pure trees.**
 ///
-/// `a * 2 / 2` is `a` for every i32, but the product is a value of its own and 2^31 is not an
-/// i32. Pinned because `LANGUAGE.md` states it as the price of the rule, and a stated price with
-/// no measurement is the kind of sentence that drifts.
+/// `a * 2 / 2` is `a` for every i32. Under checked arithmetic alone the product was a value of
+/// its own and 2^31 failed with -3; `a * 2 / 2` is a PURE tree (variables and constants), so it
+/// is now computed exactly and answers `a`. The price moved to where a value IS narrowed — a
+/// `let` — which `wide_intermediates.rs` measures (`split`).
 #[test]
-fn an_intermediate_overflow_fails_even_when_the_answer_fits() {
+fn an_intermediate_overflow_in_a_pure_tree_no_longer_fails() {
     let (_out, m) = load("mid");
     let mid: Un = sym(&m, b"mlx_mid\0");
     assert_eq!(un(mid, 1073741823), (0, 1073741823));
     assert_eq!(
         un(mid, 1073741824),
-        (OVERFLOW, -7),
-        "the answer 2^30 fits; the product 2^31 does not"
+        (0, 1073741824),
+        "the answer 2^30 fits; the product 2^31 is computed exactly and never stored"
     );
     drop(m);
 }
diff --git a/hosts/rust-oracle/tests/helper_check_propagation.rs b/hosts/rust-oracle/tests/helper_check_propagation.rs
index 8b73fae..6a350f7 100644
--- a/hosts/rust-oracle/tests/helper_check_propagation.rs
+++ b/hosts/rust-oracle/tests/helper_check_propagation.rs
@@ -20,7 +20,10 @@ fn sq(x: i32) -> i32 { return x * x }
 fn h3(x: i32) -> i32 { return x * x }
 fn h2(x: i32) -> i32 { return h3(x) + 1 }
 fn h1(x: i32) -> i32 { return h2(x) - 1 }
-fn big(a: i32, b: i32) -> bool { return a * b > 100 }
+fn big(a: i32, b: i32) -> bool {
+  let t = a * b
+  return t > 100
+}
 fn toi(x: f64) -> f64 { return (x as i32) as f64 }
 export fn wmul(a: i32, b: i32) -> i32 { return a * b }
 fn viaint(a: i32, b: i32) -> i32 { return wmul(a, b) }
@@ -154,7 +157,9 @@ fn bool_and_f64_helpers_are_checked() {
     };
     assert_eq!(p(10, 11), (0, true));
     assert_eq!(p(10, 10), (0, false));
-    assert_eq!(p(65536, 65536).0, OVERFLOW, "a * b in a bool helper");
+    // Through a `let`, which narrows: a comparison of the bare product would be exact since
+    // SPEC-wide-intermediates (DP-W4) and answer `true`.
+    assert_eq!(p(65536, 65536).0, OVERFLOW, "a * b stored in a bool helper");
 
     let conv: Conv = sym(&m, b"mlx_conv\0");
     let c = |x: f64| {
diff --git a/hosts/rust-oracle/tests/wide_intermediates.rs b/hosts/rust-oracle/tests/wide_intermediates.rs
new file mode 100644
index 0000000..ad1c790
--- /dev/null
+++ b/hosts/rust-oracle/tests/wide_intermediates.rs
@@ -0,0 +1,302 @@
+//! Wide intermediates — the values a loaded module returns
+//! (`SPEC-wide-intermediates` acceptance A, B, C, D and E).
+//!
+//! In a fallible body a PURE arithmetic tree — leaves that are variables, i32 constants, `len`,
+//! or calls to loop-free infallible functions without string arguments — is computed exactly
+//! (i64) and checked once, where its value has to become an i32. Everything else keeps the
+//! checked-arithmetic rule: the check stands at the operator.
+#![cfg(windows)]
+
+use std::sync::mpsc;
+use std::time::Duration;
+
+use ml_oracle::Module;
+use mlc::emit::emit_artifacts;
+
+mod common;
+
+const OVERFLOW: i32 = mlc::abi::ML_ST_OVERFLOW;
+const OUT_OF_RANGE: i32 = mlc::abi::ML_ST_INDEX_OUT_OF_RANGE;
+
+const SRC: &str = "
+error E_BIG = 1
+fn rate(g: i32) -> i32 {
+  if g == 1 { return 5 }
+  return 0
+}
+fn cnt(n: i32) -> i32 {
+  let mut i = 0
+  while i < n { i = i + 1 }
+  return i
+}
+fn spin(n: i32) -> i32 {
+  let mut i = 0
+  while i < n { i = i + 0 }
+  return i
+}
+fn blen(s: string) -> i32 { return byte_len(s) }
+fn h(a: i32, b: i32) -> i32 { return a * b / b }
+export fn quot(a: i32, b: i32) -> i32! { return a * b / b }
+export fn avg(a: i32, b: i32) -> i32! { return (a + b) / 2 }
+export fn half(a: i32) -> i32! { return a * 2 / 2 }
+export fn prod(a: i32, b: i32) -> i32! { return a * b }
+export fn deep(a: i32, b: i32, c: i32) -> i32! { return a * b * c / (b * c) }
+export fn quot_div(a: i32, b: i32, d: i32) -> i32! { return a * b / d }
+export fn split(a: i32, b: i32) -> i32! {
+  let t = a * b
+  return t / b
+}
+export fn idx_after(xs: [i32], a: i32, b: i32) -> i32! { return a * b + xs[5] }
+export fn idx_exact(xs: [i32], a: i32, b: i32) -> i32! { return a * b / b + xs[5] }
+export fn idx_before(xs: [i32], a: i32, b: i32) -> i32! { return xs[5] + a * b }
+export fn call_leaf(p: i32, g: i32) -> i32! { return p * rate(g) / 100 }
+export fn call_while(p: i32, n: i32) -> i32! { return p * cnt(n) / 100 }
+export fn call_str(s: string, p: i32) -> i32! { return p * blen(s) / 100 }
+export fn direct_blen(s: string, p: i32) -> i32! { return p * byte_len(s) / 100 }
+export fn hang(a: i32, b: i32, n: i32) -> i32! { return a * b + spin(n) }
+export fn cmp(a: i32, b: i32) -> bool! { return a + b > 0 }
+export fn tof_exact(a: i32, b: i32) -> f64! { return (a * b / b) as f64 }
+export fn tof_over(a: i32, b: i32) -> f64! { return (a * b) as f64 }
+export fn lit_fits() -> i32! { return 2147483647 + 1 - 1 }
+export fn lit_over() -> i32! { return 2147483647 + 1 }
+export fn plain(a: i32, b: i32) -> i32 { return a * b / b }
+export fn via_copy(a: i32, b: i32) -> i32! { return h(a, b) }
+export fn dom(a: i32, b: i32) -> i32! {
+  if a * b / b > 1000 { fail E_BIG }
+  return 0
+}
+fn id(x: i32) -> i32 { return x }
+export fn len_leaf(xs: [i32], a: i32) -> i32! { return a * len(xs) / len(xs) }
+export fn at_assign(a: i32, b: i32) -> i32! {
+  let mut t = 0
+  t = a * b / b
+  return t
+}
+export fn at_arg(a: i32, b: i32) -> i32! { return id(a * b / b) }
+export fn at_arg_over(a: i32, b: i32) -> i32! { return id(a * b) }
+export fn at_index(xs: [i32], a: i32, b: i32) -> i32! { return xs[a * b / b - 99999] }
+fn sq(x: i32) -> i32 { return x * x }
+export fn inl(x: i32) -> i32! { return x * x / x }
+export fn ext(x: i32) -> i32! { return sq(x) / x }
+export fn ext_let(x: i32) -> i32! {
+  let t = x * x
+  return t / x
+}
+";
+
+type Bin = extern "C" fn(i32, i32, *mut i32) -> i32;
+type Tri = extern "C" fn(i32, i32, i32, *mut i32) -> i32;
+type Un = extern "C" fn(i32, *mut i32) -> i32;
+type Idx = extern "C" fn(*const i32, i32, i32, i32, *mut i32) -> i32;
+type Arr1 = extern "C" fn(*const i32, i32, i32, *mut i32) -> i32;
+type Str = extern "C" fn(*const core::ffi::c_char, i32, *mut i32) -> i32;
+type Cmp = extern "C" fn(i32, i32, *mut bool) -> i32;
+type Tof = extern "C" fn(i32, i32, *mut f64) -> i32;
+type Nil = extern "C" fn(*mut i32) -> i32;
+type Plain = extern "C" fn(i32, i32) -> i32;
+
+/// Each test builds into its own directory: the tag is part of the path, and tests in one binary
+/// share a process id, so a shared tag would have them racing on one build tree.
+fn load(tag: &str) -> (common::TempOut, Module) {
+    let out = common::TempOut::new(&format!("wide_{tag}"));
+    let arts = emit_artifacts(SRC, "wide", &out).expect("emit wide");
+    let m = Module::load(arts.dll.to_str().unwrap()).expect("load wide.dll");
+    (out, m)
+}
+
+fn sym<T>(m: &Module, name: &[u8]) -> T {
+    let p = m.symbol(name).unwrap();
+    unsafe { std::mem::transmute_copy(&p) }
+}
+
+fn bin(f: Bin, a: i32, b: i32) -> (i32, i32) {
+    let mut v = -7;
+    (f(a, b, &mut v), v)
+}
+
+fn tri(f: Tri, a: i32, b: i32, c: i32) -> (i32, i32) {
+    let mut v = -7;
+    (f(a, b, c, &mut v), v)
+}
+
+/// **Acceptance A: a pure tree is exact, and checked once.**
+#[test]
+fn a_pure_tree_answers_exactly_and_fails_only_when_the_value_does_not_fit() {
+    let (_out, m) = load("exact");
+    let quot: Bin = sym(&m, b"mlx_quot\0");
+    let avg: Bin = sym(&m, b"mlx_avg\0");
+    let half: Un = sym(&m, b"mlx_half\0");
+    let prod: Bin = sym(&m, b"mlx_prod\0");
+    let deep: Tri = sym(&m, b"mlx_deep\0");
+    let quot_div: Tri = sym(&m, b"mlx_quot_div\0");
+    let split: Bin = sym(&m, b"mlx_split\0");
+
+    // Only an intermediate overflows; the answer fits.
+    assert_eq!(bin(quot, 100000, 100000), (0, 100000));
+    assert_eq!(bin(avg, 2000000000, 2000000000), (0, 2000000000));
+    let mut v = -7;
+    assert_eq!((half(1073741824, &mut v), v), (0, 1073741824));
+    // The exact value itself does not fit: still -3.
+    assert_eq!(bin(prod, 100000, 100000), (OVERFLOW, -7));
+    // "Exact" is bounded by i64 (DP-W5).
+    assert_eq!(tri(deep, 5, 1000000, 1000000), (0, 5));
+    assert_eq!(tri(deep, 5, i32::MAX, i32::MAX), (OVERFLOW, -7));
+    // A zero divisor under an exact product is DP-N4's 0.
+    assert_eq!(tri(quot_div, 100000, 100000, 0), (0, 0));
+    // The price (§2.6): a `let` is a narrowing point.
+    assert_eq!(bin(split, 100000, 100000), (OVERFLOW, -7));
+
+    // `len` is a leaf: 2^30 * 2 overflows only in the middle.
+    let len_leaf: Arr1 = sym(&m, b"mlx_len_leaf\0");
+    let xs = [1i32, 2];
+    let mut v = -7;
+    assert_eq!(
+        (len_leaf(xs.as_ptr(), 2, 1073741824, &mut v), v),
+        (0, 1073741824)
+    );
+    // Every place that takes the value narrows it once, and only there (DP-W3): an assignment,
+    // an argument, an index.
+    let at_assign: Bin = sym(&m, b"mlx_at_assign\0");
+    let at_arg: Bin = sym(&m, b"mlx_at_arg\0");
+    let at_arg_over: Bin = sym(&m, b"mlx_at_arg_over\0");
+    assert_eq!(bin(at_assign, 100000, 100000), (0, 100000));
+    assert_eq!(bin(at_arg, 100000, 100000), (0, 100000));
+    assert_eq!(bin(at_arg_over, 100000, 100000), (OVERFLOW, -7));
+    let at_index: Idx = sym(&m, b"mlx_at_index\0");
+    let mut v = -7;
+    assert_eq!(
+        (at_index(xs.as_ptr(), 2, 100000, 100000, &mut v), v),
+        (0, 2)
+    );
+    drop(m);
+}
+
+/// **Acceptance B: an impure operator keeps its check where it stands.**
+///
+/// `a*b + xs[5]`: the overflow is real and comes first, so it answers (-3) — the index behind it
+/// never overtakes it. `a*b/b + xs[5]`: the pure part has an exact value, so the next operation
+/// that really fails answers (-2). `xs[5] + a*b`: the index is evaluated first, today and now.
+#[test]
+fn an_impure_operator_keeps_its_check_in_place() {
+    let (_out, m) = load("impure");
+    let xs = [1i32, 2];
+    let run = |name: &[u8]| {
+        let f: Idx = sym(&m, name);
+        let mut v = -7;
+        f(xs.as_ptr(), 2, 100000, 100000, &mut v)
+    };
+    assert_eq!(run(b"mlx_idx_after\0"), OVERFLOW);
+    assert_eq!(run(b"mlx_idx_exact\0"), OUT_OF_RANGE);
+    assert_eq!(run(b"mlx_idx_before\0"), OUT_OF_RANGE);
+
+    // Call leaves: a loop-free helper is a leaf; a helper with `while`, one that takes a
+    // string, and `byte_len` itself are not — the product is checked at the operator, as today.
+    let call_leaf: Bin = sym(&m, b"mlx_call_leaf\0");
+    let call_while: Bin = sym(&m, b"mlx_call_while\0");
+    assert_eq!(bin(call_leaf, 500000000, 1), (0, 25000000));
+    assert_eq!(bin(call_while, 500000000, 5), (OVERFLOW, -7));
+    for name in [&b"mlx_call_str\0"[..], b"mlx_direct_blen\0"] {
+        let f: Str = sym(&m, name);
+        let mut v = -7;
+        assert_eq!(
+            (f(c"abcde".as_ptr(), 500000000, &mut v), v),
+            (OVERFLOW, -7),
+            "{}",
+            String::from_utf8_lossy(&name[..name.len() - 1])
+        );
+    }
+    drop(m);
+}
+
+/// **Acceptance C: no hang.** `spin` never returns for n > 0; it has a `while`, so it is not a
+/// leaf and the real overflow before it fails first — exactly as today. Run on a thread with a
+/// deadline, because a regression would never return; on timeout the module is leaked rather
+/// than unloaded under a running thread.
+#[test]
+fn a_failure_that_came_first_still_comes_first() {
+    let (out, m) = load("hang");
+    let hang: Tri = sym(&m, b"mlx_hang\0");
+    let (tx, rx) = mpsc::channel();
+    std::thread::spawn(move || {
+        let mut v = -7;
+        let st = hang(100000, 100000, 5, &mut v);
+        let _ = tx.send((st, v));
+    });
+    match rx.recv_timeout(Duration::from_secs(10)) {
+        Ok(r) => assert_eq!(r, (OVERFLOW, -7)),
+        Err(_) => {
+            std::mem::forget(m);
+            std::mem::forget(out);
+            panic!("mlx_hang did not return within 10 s: the overflow check was deferred past a `while`");
+        }
+    }
+    drop(m);
+}
+
+/// **Acceptance D: comparisons, `as f64`, literals, and a domain `fail`.**
+#[test]
+fn comparisons_conversions_literals_and_domain_errors_see_the_exact_value() {
+    let (_out, m) = load("cmp");
+    let cmp: Cmp = sym(&m, b"mlx_cmp\0");
+    let mut b = false;
+    assert_eq!(
+        (cmp(i32::MAX, 1, &mut b), b),
+        (0, true),
+        "exact, not wrapped"
+    );
+
+    let tof_exact: Tof = sym(&m, b"mlx_tof_exact\0");
+    let tof_over: Tof = sym(&m, b"mlx_tof_over\0");
+    let mut x = -7.0;
+    assert_eq!((tof_exact(100000, 100000, &mut x), x), (0, 100000.0));
+    // DP-W6: narrowed to i32 before the conversion, so a value past i32 is -3, not a rounded f64.
+    let mut x = -7.0;
+    assert_eq!((tof_over(100000, 100000, &mut x), x), (OVERFLOW, -7.0));
+
+    // DP-W7: DP-O9 restated — a literal expression fails only if its exact value does not fit.
+    let lit_fits: Nil = sym(&m, b"mlx_lit_fits\0");
+    let lit_over: Nil = sym(&m, b"mlx_lit_over\0");
+    let mut v = -7;
+    assert_eq!((lit_fits(&mut v), v), (0, i32::MAX));
+    let mut v = -7;
+    assert_eq!((lit_over(&mut v), v), (OVERFLOW, -7));
+
+    // The exact value exists, so the domain rule answers instead of -3.
+    let dom: Bin = sym(&m, b"mlx_dom\0");
+    assert_eq!(bin(dom, 100000, 100000), (1, -7));
+    assert_eq!(bin(dom, 10, 10), (0, 0));
+    drop(m);
+}
+
+/// **Acceptance E: infallible bodies keep wrapping; a checked copy widens too.**
+#[test]
+fn infallible_bodies_are_unchanged_and_checked_copies_widen() {
+    let (_out, m) = load("plain");
+    // 100000 * 100000 wraps to 1410065408; / 100000 = 14100 — today's answer, unchanged (DP-W10).
+    let plain: Plain = sym(&m, b"mlx_plain\0");
+    assert_eq!(plain(100000, 100000), 14100);
+    // The same expression in a helper under a `!` caller runs as its checked copy, which is a
+    // fallible body: exact.
+    let via_copy: Bin = sym(&m, b"mlx_via_copy\0");
+    assert_eq!(bin(via_copy, 100000, 100000), (0, 100000));
+    drop(m);
+}
+
+/// **The price (§2.6): a narrowing point in the middle of a computation narrows there.**
+///
+/// The same arithmetic three ways, at 46341 (46341² does not fit i32): inline it is one pure
+/// tree and exact; through a `let`, or through a helper whose `return` narrows, the product is
+/// checked on its own and fails. `LANGUAGE.md` quotes these three values.
+#[test]
+fn extracting_the_intermediate_moves_the_check_to_where_it_is_stored() {
+    let (_out, m) = load("price");
+    let one = |name: &[u8], x: i32| {
+        let f: Un = sym(&m, name);
+        let mut v = -7;
+        (f(x, &mut v), v)
+    };
+    assert_eq!(one(b"mlx_inl\0", 46341), (0, 46341));
+    assert_eq!(one(b"mlx_ext_let\0", 46341), (OVERFLOW, -7));
+    assert_eq!(one(b"mlx_ext\0", 46341), (OVERFLOW, -7));
+    drop(m);
+}