diff --git a/crates/perry-api-manifest/src/entries/part_1.rs b/crates/perry-api-manifest/src/entries/part_1.rs
index 962158dad1..a54e5e058e 100644
--- a/crates/perry-api-manifest/src/entries/part_1.rs
+++ b/crates/perry-api-manifest/src/entries/part_1.rs
@@ -349,6 +349,7 @@ pub(crate) const API_MANIFEST_PART_1: &[ApiEntry] = &[
     method("ws", "on", true, None),
     method("ws", "send", true, None),
     method("ws", "close", true, None),
+    method("ws", "readyState", true, None),
     // Node-compatible WebSocket ready-state constants. The `ws` package
     // exposes these on both the module/default export and WebSocket class:
     // CONNECTING=0, OPEN=1, CLOSING=2, CLOSED=3.
diff --git a/crates/perry-codegen/src/expr/mod.rs b/crates/perry-codegen/src/expr/mod.rs
index fa04f9bab1..f1b1f6f0c3 100644
--- a/crates/perry-codegen/src/expr/mod.rs
+++ b/crates/perry-codegen/src/expr/mod.rs
@@ -1766,6 +1766,25 @@ fn lower_numeric_binary_value(
         return Ok(None);
     }
 
+    // Hand this proven shape to `binary::lower`, which owns the existing
+    // integer remainder and negative-zero repair. This must run before operand
+    // lowering so returning `None` emits no dead loads or duplicate records.
+    if matches!(op, BinaryOp::Mod)
+        && matches!(
+            left,
+            Expr::LocalGet(id)
+                if ctx.i32_counter_slots.contains_key(id)
+                    && !ctx.unsigned_i32_locals.contains(id)
+        )
+        && matches!(
+            right,
+            Expr::Integer(value)
+                if i32::try_from(*value).is_ok_and(|divisor| divisor > 0)
+        )
+    {
+        return Ok(None);
+    }
+
     let Some(left) = lower_numeric_operand_value(ctx, left)? else {
         return Ok(None);
     };
diff --git a/crates/perry-codegen/tests/native_proof_regressions.rs b/crates/perry-codegen/tests/native_proof_regressions.rs
index 7315b2d930..a9111731e4 100644
--- a/crates/perry-codegen/tests/native_proof_regressions.rs
+++ b/crates/perry-codegen/tests/native_proof_regressions.rs
@@ -1317,7 +1317,7 @@ fn artifact_schema_v6_records_pod_dynamic_write_fallback() {
 }
 
 #[test]
-fn pod_field_read_after_dynamic_materialization_uses_number_coerce() {
+fn pod_field_read_after_dynamic_materialization_uses_dynamic_numeric_sub() {
     let packet_ty = pod_type(&[
         ("tag", Type::Named("PerryU32".to_string())),
         ("gain", Type::Named("PerryF32".to_string())),
@@ -1346,8 +1346,16 @@ fn pod_field_read_after_dynamic_materialization_uses_number_coerce() {
 
     let ir = compile_ir("pod_dynamic_materialized_read_coerce.ts", body);
     assert!(
-        ir.contains("call double @js_number_coerce"),
-        "POD field reads after dynamic materialization must not feed boxed JSValue fallbacks into raw numeric arithmetic:\n{ir}"
+        ir.contains("call double @js_object_get_field_by_name_f64"),
+        "materialized POD field reads must preserve boxed JSValue bits:\n{ir}"
+    );
+    assert!(
+        ir.contains("call double @js_dynamic_sub"),
+        "materialized POD field reads must use coercing dynamic arithmetic:\n{ir}"
+    );
+    assert!(
+        !ir.contains("fsub double"),
+        "materialized POD field reads must not feed boxed JSValue bits into raw arithmetic:\n{ir}"
     );
 }
 
@@ -13379,3 +13387,6 @@ fn put_value_set_index_keeps_the_numeric_array_fast_path() {
 
 #[path = "native_proof_regressions/invalidation.rs"]
 mod invalidation;
+
+#[path = "native_proof_regressions/integer_modulo.rs"]
+mod integer_modulo;
diff --git a/crates/perry-codegen/tests/native_proof_regressions/integer_modulo.rs b/crates/perry-codegen/tests/native_proof_regressions/integer_modulo.rs
new file mode 100644
index 0000000000..0ed81ea144
--- /dev/null
+++ b/crates/perry-codegen/tests/native_proof_regressions/integer_modulo.rs
@@ -0,0 +1,144 @@
+use super::*;
+
+fn modulo(left: Expr, right: Expr) -> Expr {
+    Expr::Binary {
+        op: BinaryOp::Mod,
+        left: Box::new(left),
+        right: Box::new(right),
+    }
+}
+
+fn factorial_shaped_ir(divisor: Expr) -> String {
+    compile_ir(
+        "value_first_i32_modulo.ts",
+        vec![
+            number_let(1, "sum", true, int(0)),
+            number_let(3, "iterations", false, int(64)),
+            for_loop(
+                2,
+                local(3),
+                vec![Stmt::Expr(Expr::LocalSet(
+                    1,
+                    Box::new(add(local(1), modulo(local(2), divisor))),
+                ))],
+            ),
+            Stmt::Return(Some(local(1))),
+        ],
+    )
+}
+
+fn assert_integer_modulo_with_negative_zero_repair(ir: &str) {
+    assert!(
+        ir.contains("srem i64"),
+        "signed i32 counter modulo a positive Expr::Integer should reach the existing integer remainder path:\n{ir}"
+    );
+    assert!(
+        !ir.contains("frem double"),
+        "eligible signed i32 counter modulo must not retain floating remainder:\n{ir}"
+    );
+    assert!(
+        ir.contains("icmp eq i64")
+            && ir.contains("fcmp olt double")
+            && ir.contains("fneg double")
+            && ir.contains("select i1"),
+        "integer remainder must retain the existing IEEE-754 negative-zero repair:\n{ir}"
+    );
+}
+
+fn assert_floating_modulo(ir: &str) {
+    assert!(
+        ir.contains("frem double"),
+        "ineligible modulo shape must remain on floating remainder:\n{ir}"
+    );
+    assert!(
+        !ir.contains("srem i64") && !ir.contains("srem i32"),
+        "ineligible modulo shape must not emit integer remainder:\n{ir}"
+    );
+}
+
+#[test]
+fn i32_counter_mod_positive_literal_reaches_integer_fast_path() {
+    assert_integer_modulo_with_negative_zero_repair(&factorial_shaped_ir(int(1000)));
+}
+
+#[test]
+fn i32_counter_mod_unsafe_or_nonliteral_divisors_keep_frem() {
+    let cases = [
+        ("integral_number", number(1000.0)),
+        ("zero", int(0)),
+        ("negative", int(-1)),
+        ("fractional", number(2.5)),
+        ("out_of_i32", int(i64::from(i32::MAX) + 1)),
+    ];
+    for (case, divisor) in cases {
+        let ir = factorial_shaped_ir(divisor);
+        assert!(
+            ir.contains("frem double"),
+            "{case} divisor must remain on floating remainder:\n{ir}"
+        );
+        assert!(
+            !ir.contains("srem i64") && !ir.contains("srem i32"),
+            "{case} divisor must not emit integer remainder:\n{ir}"
+        );
+    }
+
+    let dynamic_ir = compile_ir(
+        "value_first_i32_modulo_dynamic_divisor.ts",
+        vec![
+            number_let(1, "sum", true, int(0)),
+            number_let(3, "divisor", false, int(7)),
+            number_let(4, "iterations", false, int(64)),
+            for_loop(
+                2,
+                local(4),
+                vec![Stmt::Expr(Expr::LocalSet(
+                    1,
+                    Box::new(add(local(1), modulo(local(2), local(3)))),
+                ))],
+            ),
+            Stmt::Return(Some(local(1))),
+        ],
+    );
+    assert_floating_modulo(&dynamic_ir);
+}
+
+#[test]
+fn non_i32_left_operands_keep_frem() {
+    let f64_ir = compile_ir(
+        "value_first_f64_modulo.ts",
+        vec![
+            number_let(1, "value", false, number(5.5)),
+            Stmt::Return(Some(modulo(local(1), int(2)))),
+        ],
+    );
+    assert_floating_modulo(&f64_ir);
+
+    // A `>>> 0` initializer plus only `>>> 0` writes is the harness's existing
+    // way to obtain an unsigned i32 shadow slot. The specialization must not
+    // treat its native bit pattern as a signed dividend.
+    let u32_ir = compile_ir(
+        "value_first_u32_modulo.ts",
+        vec![
+            number_let(1, "sum", true, int(0)),
+            number_let(3, "iterations", false, int(64)),
+            Stmt::For {
+                init: Some(Box::new(number_let(2, "i", true, ushr_zero(int(0))))),
+                condition: Some(Expr::Compare {
+                    op: CompareOp::Lt,
+                    left: Box::new(local(2)),
+                    right: Box::new(local(3)),
+                }),
+                update: Some(Expr::LocalSet(
+                    2,
+                    Box::new(ushr_zero(add(local(2), int(1)))),
+                )),
+                body: vec![Stmt::Expr(Expr::LocalSet(
+                    1,
+                    Box::new(add(local(1), modulo(local(2), int(7)))),
+                ))],
+            },
+            Stmt::Return(Some(local(1))),
+        ],
+    );
+    assert_floating_modulo(&u32_ir);
+}
diff --git a/docs/src/api/reference.md b/docs/src/api/reference.md
index bde1092bca..f867cbc66b 100644
--- a/docs/src/api/reference.md
+++ b/docs/src/api/reference.md
@@ -2,7 +2,7 @@
 
 This page is auto-generated from Perry's compile-time API manifest (`perry-api-manifest::API_MANIFEST`). It is the source of truth for what `perry compile` accepts; references to symbols not listed here produce `R005 UnimplementedApi` (issue #463). Stubs (#464) are flagged ⚠ — they link cleanly but no-op at runtime on the chosen target.
 
-Total: 2829 entries across 117 modules.
+Total: 2830 entries across 117 modules.
 
 ## Modules
 
@@ -3754,6 +3754,7 @@ Total: 2829 entries across 117 modules.
 - `handleUpgrade` — instance
 - `on` — instance
 - `on` — instance *(class: `Client`)*
+- `readyState` — instance
 - `send` — instance
 - `send` — instance *(class: `Client`)*
 - `sendToClient` — module
diff --git a/test-files/test_gap_numeric_remainder_i32.ts b/test-files/test_gap_numeric_remainder_i32.ts
new file mode 100644
index 0000000000..adbaacdd26
--- /dev/null
+++ b/test-files/test_gap_numeric_remainder_i32.ts
@@ -0,0 +1,27 @@
+let sum = 0;
+for (let i = 0; i < 10000; i++) {
+    sum = sum + (i % 1000);
+}
+console.log("positive-loop:" + sum);
+
+let sawNegativeZero = false;
+for (let i = -6; i <= 0; i++) {
+    const value = i % 3;
+    if (Object.is(value, -0)) {
+        sawNegativeZero = true;
+    }
+}
+console.log("negative-loop-zero:" + sawNegativeZero);
+
+console.log("fractional:" + (5.5 % 2));
+console.log("nan:" + (NaN % 2));
+console.log("infinity:" + (Infinity % 2));
+console.log("zero-divisor:" + (5 % 0));
+console.log("infinite-divisor:" + (5 % Infinity));
+console.log("negative-zero:" + Object.is(-0 % 3, -0));
+
+let dynamicZero = 0;
+console.log("dynamic-zero-divisor:" + (5 % dynamicZero));
+console.log("negative-divisor:" + (5 % -2));
+console.log("min-i32-negative-one:" + Object.is(-2147483648 % -1, -0));
+console.log("wide-safe-integer:" + (9007199254740991 % 97));