diff --git a/changelog.d/wpfacts-p3-b1-canonical-numbers.md b/changelog.d/wpfacts-p3-b1-canonical-numbers.md
new file mode 100644
index 00000000000..d52aea2d458
--- /dev/null
+++ b/changelog.d/wpfacts-p3-b1-canonical-numbers.md
@@ -0,0 +1 @@
+Performance: an element read whose value the whole-program facts prove a plain Number (every value stored into the array is a program Number or the audited Number result of a builtin) is compared with a bare `fcmp`, used as an arithmetic operand without an "is a Number" test, and passed to a Number parameter without an INT32 conversion at entry. A read that may also be `undefined` (a hole, or an index past the end) keeps exact JS equality: `undefined === undefined` is true and `NaN === NaN` false. Each builtin's Number result is audited against the runtime function that produces it (`perry-wpfacts/NUM_SEEDS.md`; a test keeps the table complete). `PERRY_VERIFY_FACTS=1` checks every trusted value is a plain double. `PERRY_FACTS_CANONICAL_NUMBERS=0` turns it off. A runtime built with `PERRY_FACTS_SABOTAGE=canonnum` (`scripts/p3-canonnum-runtime.sh`) is the negative control.
diff --git a/crates/perry-codegen/src/codegen/facts_number_locals.rs b/crates/perry-codegen/src/codegen/facts_number_locals.rs
index b9a838d43c7..3fce334aee4 100644
--- a/crates/perry-codegen/src/codegen/facts_number_locals.rs
+++ b/crates/perry-codegen/src/codegen/facts_number_locals.rs
@@ -171,7 +171,16 @@ pub(crate) fn none() -> &'static HashSet<u32> {
 
 /// The plain double of a Number argument: an INT32 box converts, every other
 /// Number is its own bits.
+///
+/// P3 B1, C4 (DESIGN-p3 rev 3.1 §2.3): a Number the facts prove is a plain
+/// double (every value reaching the parameter is a program Number or an
+/// audited builtin NUM, `perry-wpfacts/NUM_SEEDS.md`), so with
+/// `PERRY_FACTS_CANONICAL_NUMBERS` on the argument is taken as it is. The
+/// entry witness (`emit_param_witnesses`) checks it in check mode.
 pub(crate) fn emit_entry_number(blk: &mut crate::block::LlBlock, arg: &str) -> String {
+    if crate::expr::facts_canonical::enabled() {
+        return arg.to_string();
+    }
     let is_int = super::typed_entry::emit_int32_box_test(blk, arg);
     let bits = blk.bitcast_double_to_i64(arg);
     let low = blk.trunc(I64, &bits, I32);
diff --git a/crates/perry-codegen/src/codegen/facts_number_locals_tests.rs b/crates/perry-codegen/src/codegen/facts_number_locals_tests.rs
index 4420d565702..8d70c30c757 100644
--- a/crates/perry-codegen/src/codegen/facts_number_locals_tests.rs
+++ b/crates/perry-codegen/src/codegen/facts_number_locals_tests.rs
@@ -118,10 +118,21 @@ fn proven_bindings_take_raw_double_ops_and_own_no_root_slot() {
         0,
         "a proven Number binding never holds a pointer:\n{body}"
     );
-    assert!(
-        body.contains(crate::nanbox::INT32_TAG_I64),
-        "a proven parameter converts an INT32 box at entry:\n{body}"
-    );
+    // P3 B1, C4: a proven Number is a plain double (the NUM fact is audited,
+    // `perry-wpfacts/NUM_SEEDS.md`), so the parameter takes its argument's bits
+    // with no INT32 decode at entry; the entry witness checks it in check
+    // mode. `PERRY_FACTS_CANONICAL_NUMBERS=0` restores the decode.
+    if crate::expr::facts_canonical::enabled() {
+        assert!(
+            !body.contains(crate::nanbox::INT32_TAG_I64),
+            "a proven parameter takes its argument's bits at entry:\n{body}"
+        );
+    } else {
+        assert!(
+            body.contains(crate::nanbox::INT32_TAG_I64),
+            "a proven parameter converts an INT32 box at entry:\n{body}"
+        );
+    }
 }
 
 #[test]
diff --git a/crates/perry-codegen/src/codegen/program_facts_view.rs b/crates/perry-codegen/src/codegen/program_facts_view.rs
index 4912e9ff1f1..8b809739aa9 100644
--- a/crates/perry-codegen/src/codegen/program_facts_view.rs
+++ b/crates/perry-codegen/src/codegen/program_facts_view.rs
@@ -240,6 +240,10 @@ pub struct ElisionFacts {
     /// Method call byte offset → the call is a field element read of its
     /// receiver (wpfacts `ModuleBindings::field_read_calls`, b1).
     pub field_read_calls: std::collections::BTreeMap<u32, FactsFieldReadCall>,
+    /// Element reads (by `element_offset`) whose value the facts prove a
+    /// plain Number; `true` when it may also be `undefined` (wpfacts
+    /// `canonical_numbers`, P3 B1).
+    pub number_element_reads: std::collections::BTreeMap<u32, bool>,
     pub indexed_metadata_pristine: bool,
     pub numeric_functions: std::collections::BTreeMap<u32, FactsNumericFunction>,
     /// Class id → its own statics that hold their definition for the
@@ -296,6 +300,7 @@ impl ElisionFacts {
             && self.number_calls.is_empty()
             && self.element_reads.is_empty()
             && self.field_read_calls.is_empty()
+            && self.number_element_reads.is_empty()
             && self.locals.is_empty()
             && self.this_of.is_empty()
             && self.local_bodies.is_empty()
diff --git a/crates/perry-codegen/src/expr/binary.rs b/crates/perry-codegen/src/expr/binary.rs
index 932e83366ff..a8288deaccc 100644
--- a/crates/perry-codegen/src/expr/binary.rs
+++ b/crates/perry-codegen/src/expr/binary.rs
@@ -149,12 +149,18 @@ fn lower_guarded_numeric_add(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String>
     }
     let mut leaves = Vec::new();
     add_tree_leaves(expr, &mut leaves);
+    let facts: Vec<bool> = leaves
+        .iter()
+        .map(|leaf| facts_number_leaf(ctx, leaf))
+        .collect();
     let needs_test: Vec<bool> = leaves
         .iter()
-        .map(|leaf| !crate::type_analysis::expr_produces_canonical_raw_f64(ctx, leaf))
+        .zip(&facts)
+        .map(|(leaf, f)| !f && !crate::type_analysis::expr_produces_canonical_raw_f64(ctx, leaf))
         .collect();
 
     with_operands_rooted(ctx, &leaves, |ctx, values| {
+        witness_facts_leaves(ctx, values, &facts)?;
         let mut cond: Option<String> = None;
         for (value, is_tested) in values.iter().zip(needs_test.iter()) {
             if !is_tested {
@@ -235,6 +241,36 @@ fn lower_guarded_numeric_add(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String>
     })
 }
 
+/// P3 B1, C2 (`facts_canonical`): a guarded arithmetic leaf the facts prove a
+/// plain Number needs no "is a Number" test.
+fn facts_number_leaf(ctx: &FnCtx<'_>, leaf: &Expr) -> bool {
+    let proven = crate::expr::facts_canonical::of(ctx, leaf)
+        == Some(crate::expr::facts_canonical::Num::Number);
+    if proven {
+        crate::verify_facts::consumed(
+            crate::verify_facts::Fact::CanonicalNumber,
+            || serde_json::json!({ "arith": "leaf" }),
+        );
+        crate::facts_consumed::used();
+    }
+    proven
+}
+
+/// Check mode: each fact-trusted leaf is a plain double.
+fn witness_facts_leaves(ctx: &mut FnCtx<'_>, values: &[String], facts: &[bool]) -> Result<()> {
+    for (value, f) in values.iter().zip(facts) {
+        if *f {
+            crate::expr::facts_canonical::witness(
+                ctx,
+                value,
+                crate::expr::facts_canonical::Num::Number,
+                "arithmetic leaf",
+            )?;
+        }
+    }
+    Ok(())
+}
+
 /// The `+`-shaped guard for the arithmetic operators that cannot concatenate.
 ///
 /// `-`, `*` and `/` apply ToNumeric to both operands, so unlike `+` there is
@@ -262,13 +298,19 @@ fn lower_guarded_numeric_arith(
     fname: &str,
 ) -> Result<String> {
     let leaves = [left, right];
+    let facts: Vec<bool> = leaves
+        .iter()
+        .map(|leaf| facts_number_leaf(ctx, leaf))
+        .collect();
     let needs_test: Vec<bool> = leaves
         .iter()
-        .map(|leaf| !crate::type_analysis::expr_produces_canonical_raw_f64(ctx, leaf))
+        .zip(&facts)
+        .map(|(leaf, f)| !f && !crate::type_analysis::expr_produces_canonical_raw_f64(ctx, leaf))
         .collect();
     let range_guard = is_bitwise_op(op) && needs_test.contains(&true);
 
     with_operands_rooted(ctx, &leaves, |ctx, values| {
+        witness_facts_leaves(ctx, values, &facts)?;
         let mut cond: Option<String> = None;
         for (value, is_tested) in values.iter().zip(needs_test.iter()) {
             let is_num = if range_guard {
diff --git a/crates/perry-codegen/src/expr/compare.rs b/crates/perry-codegen/src/expr/compare.rs
index 77b6210a3d6..e0769082b64 100644
--- a/crates/perry-codegen/src/expr/compare.rs
+++ b/crates/perry-codegen/src/expr/compare.rs
@@ -1253,6 +1253,87 @@ fn lower_string_strict_eq_inline(
 /// A compare operand that is statically a number (not a BigInt, not a value
 /// that may come back boxed from a raw-f64 fallback): two of them take the
 /// bare `fcmp`.
+/// P3 B1, C1 (DESIGN-p3 rev 3.1 §2.3): a compare whose operands are both
+/// proven plain Numbers, or Number-or-undefined, at least one of them by the
+/// facts (`facts_canonical`). There is no INT32 prefix and no runtime helper:
+///
+/// - relational: the ordered `fcmp` (`undefined` is a NaN pattern, so every
+///   comparison with it is false, as in JS);
+/// - `===` with at least one plain Number: `fcmp oeq` (`une` for `!==`);
+/// - `===` of two Number-or-undefined: `fcmp oeq || (bits equal and
+///   undefined)`, and `!==` is its exact negation (REVIEW-p3 D1).
+///
+/// Check mode tests each fact-trusted operand (`facts_canonical::witness`).
+fn lower_facts_number_compare(
+    ctx: &mut FnCtx<'_>,
+    op: CompareOp,
+    left: &Expr,
+    right: &Expr,
+    l: &str,
+    r: &str,
+) -> Result<Option<String>> {
+    use super::facts_canonical::{self, Num};
+    if matches!(op, CompareOp::LooseEq | CompareOp::LooseNe) {
+        return Ok(None);
+    }
+    let fl = facts_canonical::of(ctx, left);
+    let fr = facts_canonical::of(ctx, right);
+    if fl.is_none() && fr.is_none() {
+        return Ok(None);
+    }
+    let side = |ctx: &FnCtx<'_>, e: &Expr, f: Option<Num>| {
+        f.or_else(|| compare_operand_is_numeric(ctx, e).then_some(Num::Number))
+    };
+    let (Some(kl), Some(kr)) = (side(ctx, left, fl), side(ctx, right, fr)) else {
+        return Ok(None);
+    };
+    crate::verify_facts::consumed(
+        crate::verify_facts::Fact::CanonicalNumber,
+        || serde_json::json!({ "compare": format!("{op:?}") }),
+    );
+    crate::facts_consumed::used();
+    if let Some(f) = fl {
+        facts_canonical::witness(ctx, l, f, "compare operand")?;
+    }
+    if let Some(f) = fr {
+        facts_canonical::witness(ctx, r, f, "compare operand")?;
+    }
+    let blk = ctx.block();
+    let bit = match op {
+        CompareOp::Lt => blk.fcmp("olt", l, r),
+        CompareOp::Le => blk.fcmp("ole", l, r),
+        CompareOp::Gt => blk.fcmp("ogt", l, r),
+        CompareOp::Ge => blk.fcmp("oge", l, r),
+        CompareOp::Eq | CompareOp::Ne
+            if kl == Num::NumberOrUndefined && kr == Num::NumberOrUndefined =>
+        {
+            let oeq = blk.fcmp("oeq", l, r);
+            let lb = blk.bitcast_double_to_i64(l);
+            let rb = blk.bitcast_double_to_i64(r);
+            let same = blk.icmp_eq(I64, &lb, &rb);
+            let undef = blk.icmp_eq(I64, &lb, crate::nanbox::TAG_UNDEFINED_I64);
+            let both_undef = blk.and(I1, &same, &undef);
+            let eq = blk.or(I1, &oeq, &both_undef);
+            if matches!(op, CompareOp::Ne) {
+                blk.xor(I1, &eq, "true")
+            } else {
+                eq
+            }
+        }
+        CompareOp::Eq => blk.fcmp("oeq", l, r),
+        CompareOp::Ne => blk.fcmp("une", l, r),
+        CompareOp::LooseEq | CompareOp::LooseNe => unreachable!(),
+    };
+    let tagged = blk.select(
+        I1,
+        &bit,
+        I64,
+        crate::nanbox::TAG_TRUE_I64,
+        crate::nanbox::TAG_FALSE_I64,
+    );
+    Ok(Some(blk.bitcast_i64_to_double(&tagged)))
+}
+
 fn compare_operand_is_numeric(ctx: &FnCtx<'_>, operand: &Expr) -> bool {
     is_numeric_expr(ctx, operand)
         && !expr_may_return_boxed_value_from_raw_f64_fallback(ctx, operand)
@@ -1893,6 +1974,12 @@ pub(crate) fn lower(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String> {
                     return Ok(blk.bitcast_i64_to_double(&result_bits));
                 }
 
+                // P3 B1, C1 (`facts_canonical`): both operands proven plain
+                // Numbers (or Number-or-undefined), at least one by the facts.
+                if let Some(v) = lower_facts_number_compare(ctx, *op, left, right, &l, &r)? {
+                    return Ok(v);
+                }
+
                 // An ordered relational compare (`<`, `<=`, `>`, `>=`) whose
                 // operands aren't BOTH statically numeric needs the full ECMAScript
                 // Abstract Relational Comparison: ToPrimitive (`{valueOf}`/`Date`),
diff --git a/crates/perry-codegen/src/expr/facts_canonical.rs b/crates/perry-codegen/src/expr/facts_canonical.rs
new file mode 100644
index 00000000000..d60f01072ca
--- /dev/null
+++ b/crates/perry-codegen/src/expr/facts_canonical.rs
@@ -0,0 +1,127 @@
+//! P3 B1 (DESIGN-p3-canonical-numbers rev 3.1 §2): consumers that drop an
+//! INT32 test because the facts prove a value a plain Number.
+//!
+//! The fact is wpfacts' NUM declaration (REVIEW-p3 R2): an element read whose
+//! value node holds only Number at every copy
+//! (`ElisionFacts::number_element_reads`), possibly with `undefined` for a
+//! hole or an index past the end. Every Number a node can hold is a program
+//! Number (codegen lowers literals and arithmetic to plain doubles) or comes
+//! from a builtin whose NUM seed is audited against its runtime function
+//! (`perry-wpfacts/NUM_SEEDS.md`). So such a value is a plain IEEE double and
+//! never an INT32-boxed word.
+//!
+//! The consumers:
+//! - C1 (`expr/compare.rs`): a compare whose operands are both proven lowers
+//!   to `fcmp`, with no INT32 prefix. Two Number-or-undefined operands keep
+//!   an identity arm for `undefined === undefined` (REVIEW-p3 D1).
+//! - C2 (`expr/binary.rs`): a guarded arithmetic leaf proven a Number needs
+//!   no "is a Number" test.
+//!
+//! Check mode (`PERRY_VERIFY_FACTS=1`): every operand a consumer trusts is
+//! tested "is a plain double" (`emit_plain_number_test`: outside the tag band
+//! and not HANDLE_TAG; REVIEW-p3 R7), or is exactly `undefined` when the
+//! fact allows it. A miss exits 86 (`Fact::CanonicalNumber`).
+//!
+//! `PERRY_FACTS_CANONICAL_NUMBERS=0` turns these consumers off (wpfacts then
+//! exports no element values either).
+
+use anyhow::Result;
+use perry_hir::{Expr, LogicalOp};
+
+use super::FnCtx;
+use crate::types::{DOUBLE, I1, I32, I64};
+
+/// What the facts prove about a value.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub(crate) enum Num {
+    /// A plain double.
+    Number,
+    /// A plain double or `undefined`.
+    NumberOrUndefined,
+}
+
+pub(crate) fn enabled() -> bool {
+    static ON: std::sync::OnceLock<bool> = std::sync::OnceLock::new();
+    *ON.get_or_init(|| {
+        !matches!(
+            std::env::var("PERRY_FACTS_CANONICAL_NUMBERS").as_deref(),
+            Ok("0") | Ok("off") | Ok("false")
+        )
+    })
+}
+
+/// The facts' answer for `e`, when they cover it.
+pub(crate) fn of(ctx: &FnCtx<'_>, e: &Expr) -> Option<Num> {
+    if !enabled() || ctx.wpfacts_off || ctx.wpfacts.interp_guard {
+        return None;
+    }
+    match e {
+        Expr::IndexGet { element_offset, .. } if *element_offset != 0 => ctx
+            .wpfacts
+            .number_element_reads
+            .get(element_offset)
+            .map(|&undef| {
+                if undef {
+                    Num::NumberOrUndefined
+                } else {
+                    Num::Number
+                }
+            }),
+        // `x ?? d`: `d` replaces exactly the `undefined` (and `null`, which a
+        // Number-or-undefined value never is).
+        Expr::Logical {
+            op: LogicalOp::Coalesce,
+            left,
+            right,
+        } => {
+            of(ctx, left)?;
+            let d = matches!(right.as_ref(), Expr::Integer(_) | Expr::Number(_))
+                || of(ctx, right) == Some(Num::Number);
+            d.then_some(Num::Number)
+        }
+        _ => None,
+    }
+}
+
+/// Check mode: the trusted `value` (the lowering of an operand `of` proved
+/// `fact`) is a plain double, or `undefined` where the fact allows it.
+pub(crate) fn witness(ctx: &mut FnCtx<'_>, value: &str, fact: Num, what: &str) -> Result<()> {
+    if !crate::verify_facts::enabled() {
+        return Ok(());
+    }
+    crate::verify_facts::covered(
+        crate::verify_facts::Fact::CanonicalNumber,
+        || serde_json::json!({ "site": what }),
+    );
+    let blk = ctx.block();
+    let plain = crate::codegen::emit_plain_number_test(blk, value);
+    let ok = if fact == Num::NumberOrUndefined {
+        let bits = blk.bitcast_double_to_i64(value);
+        let undef = blk.icmp_eq(I64, &bits, crate::nanbox::TAG_UNDEFINED_I64);
+        blk.or(I1, &plain, &undef)
+    } else {
+        plain
+    };
+    crate::verify_facts::tick(ctx);
+    let miss = ctx.new_block("canonical_number.verify_miss");
+    let next = ctx.new_block("canonical_number.admitted");
+    let (miss_l, next_l) = (ctx.block_label(miss), ctx.block_label(next));
+    ctx.block().cond_br(&ok, &next_l, &miss_l);
+    ctx.current_block = miss;
+    let site_arg = crate::verify_facts::site_arg(
+        ctx,
+        &format!("canonical number {what}"),
+        crate::verify_facts::Fact::CanonicalNumber,
+        &[],
+    );
+    let _ = crate::verify_facts::check(
+        ctx,
+        I32,
+        "perry_wpfacts_check_miss",
+        &[(DOUBLE, value)],
+        &site_arg,
+    );
+    ctx.block().unreachable();
+    ctx.current_block = next;
+    Ok(())
+}
diff --git a/crates/perry-codegen/src/expr/mod.rs b/crates/perry-codegen/src/expr/mod.rs
index 20a9a976790..13268aeb2d6 100644
--- a/crates/perry-codegen/src/expr/mod.rs
+++ b/crates/perry-codegen/src/expr/mod.rs
@@ -126,6 +126,7 @@ mod channel;
 #[cfg(test)]
 mod class_method_arguments_object_tests;
 pub(crate) mod collection_receiver;
+pub(crate) mod facts_canonical;
 pub(crate) mod facts_number;
 mod helpers;
 mod i32_fast_path;
diff --git a/crates/perry-codegen/src/verify_facts/coverage.rs b/crates/perry-codegen/src/verify_facts/coverage.rs
index 3c7204b7d96..58383742548 100644
--- a/crates/perry-codegen/src/verify_facts/coverage.rs
+++ b/crates/perry-codegen/src/verify_facts/coverage.rs
@@ -38,6 +38,7 @@ pub(crate) enum Fact {
     ProtoAdd,
     ElementRead,
     FieldReadCall,
+    CanonicalNumber,
 }
 impl Fact {
     pub(super) fn name(self) -> &'static str {
@@ -75,6 +76,7 @@ impl Fact {
             Self::ProtoAdd => "prototype add",
             Self::ElementRead => "proven element read",
             Self::FieldReadCall => "field read call",
+            Self::CanonicalNumber => "canonical number",
         }
     }
 }
diff --git a/crates/perry-runtime/src/child_process/v8_serde.rs b/crates/perry-runtime/src/child_process/v8_serde.rs
index c39cb82b34f..84b7908b3ed 100644
--- a/crates/perry-runtime/src/child_process/v8_serde.rs
+++ b/crates/perry-runtime/src/child_process/v8_serde.rs
@@ -1279,3 +1279,7 @@ fn make_typed_array(kind: u8, bytes: &[u8]) -> f64 {
     });
     cp_box_ptr(ta as *const u8)
 }
+
+#[cfg(test)]
+#[path = "v8_serde_canonical_tests.rs"]
+mod canonical_tests;
diff --git a/crates/perry-runtime/src/child_process/v8_serde_canonical_tests.rs b/crates/perry-runtime/src/child_process/v8_serde_canonical_tests.rs
new file mode 100644
index 00000000000..12d96812a8f
--- /dev/null
+++ b/crates/perry-runtime/src/child_process/v8_serde_canonical_tests.rs
@@ -0,0 +1,43 @@
+//! P3 B1 audit (perry-wpfacts/NUM_SEEDS.md, "int32-box producers"): a V8
+//! wire int32 (`'I'` + zigzag varint), as `v8.serialize` writes for small
+//! integers, deserializes to the raw double, never an INT32-tagged word.
+
+use super::{v8_deserialize, v8_serialize};
+
+/// `0xFF 0x0F` (version 15), then `'I'` and the zigzag varint of `n`.
+fn wire_int32(n: i32) -> Vec<u8> {
+    let mut z = ((n << 1) ^ (n >> 31)) as u32;
+    let mut out = vec![0xFF, 0x0F, b'I'];
+    loop {
+        let byte = (z & 0x7F) as u8;
+        z >>= 7;
+        if z == 0 {
+            out.push(byte);
+            break;
+        }
+        out.push(byte | 0x80);
+    }
+    out
+}
+
+#[test]
+fn a_wire_int32_deserializes_to_the_raw_double() {
+    for n in [0, 5, -7, 1, -1, i32::MAX, i32::MIN] {
+        let v = v8_deserialize(&wire_int32(n));
+        assert_eq!(v.to_bits(), (n as f64).to_bits(), "wire int32 {n}");
+    }
+}
+
+#[test]
+fn serialize_then_deserialize_keeps_small_integers_raw() {
+    for n in [0.0, 5.0, -7.0, 2147483647.0, -2147483648.0] {
+        let bytes = v8_serialize(n);
+        // Skip the version tag and its varint.
+        let mut at = 1;
+        while bytes[at] & 0x80 != 0 {
+            at += 1;
+        }
+        assert_eq!(bytes.get(at + 1), Some(&b'I'), "{n} is written as a wire int32");
+        assert_eq!(v8_deserialize(&bytes).to_bits(), f64::to_bits(n), "{n}");
+    }
+}
diff --git a/crates/perry-runtime/src/closure/dispatch/value_call.rs b/crates/perry-runtime/src/closure/dispatch/value_call.rs
index 6cb3f3e075a..22d80760fda 100644
--- a/crates/perry-runtime/src/closure/dispatch/value_call.rs
+++ b/crates/perry-runtime/src/closure/dispatch/value_call.rs
@@ -403,9 +403,13 @@ unsafe fn call_array_this(
         return dispatch_body_args(closure, info, this, &vec![0.0; n]);
     }
     let args = std::slice::from_raw_parts(args_ptr, n);
-    // V8 supplies INT32-tagged numbers; compiled code supplies doubles. Keep
-    // conversion at this bridge, and leave class references (the same tag)
-    // intact. Only a slice containing a numeric INT32 needs scratch storage.
+    // Defensive decode of INT32-tagged words; class references (the same tag)
+    // stay intact. No caller supplies one today: the V8 embedding that did
+    // (perry-jsruntime) was removed in #1696, `js_create_callback` is a stub
+    // (`closure/v8_stubs.rs`), and the remaining callers (perry-ffi
+    // `Closure::call`, ext-http) pass plain doubles (P3 B1 audit,
+    // perry-wpfacts/NUM_SEEDS.md). Deleted with the other INT32 consumers in
+    // P3 B4b. Only a slice containing a numeric INT32 needs scratch storage.
     let is_int = |raw: f64| {
         crate::value::is_int32_bits(raw.to_bits()) && crate::object::class_ref_id(raw).is_none()
     };
diff --git a/crates/perry-runtime/src/json/stringify_scalars.rs b/crates/perry-runtime/src/json/stringify_scalars.rs
index 7953e534140..20f88f56bd8 100644
--- a/crates/perry-runtime/src/json/stringify_scalars.rs
+++ b/crates/perry-runtime/src/json/stringify_scalars.rs
@@ -26,10 +26,11 @@ pub(crate) unsafe fn write_number(buf: &mut String, value: f64) {
     }
     // An int32 is NaN-boxed (INT32_TAG = 0x7FFE); its bits ARE an IEEE NaN, so it
     // would otherwise fall into the `is_nan()` → "null" arm below and silently
-    // drop the value. Decode and emit the signed integer. Integer columns from
-    // the sqlite binding (and other int32-tagged numbers) funnel here; numeric
-    // literals are stored as plain f64 doubles by codegen and never take this
-    // branch. Mirrors the BigInt funnel above.
+    // drop the value. Decode and emit the signed integer. No Number producer
+    // makes such a word today: sqlite integer columns are raw doubles
+    // (`perry-stdlib` sqlite `bind.rs` tests, #6561), and so are codegen's
+    // numbers (P3 B1 audit, perry-wpfacts/NUM_SEEDS.md). The arm stays until
+    // P3 B4b deletes the INT32 consumers. Mirrors the BigInt funnel above.
     if crate::value::is_int32_bits(value.to_bits()) {
         let n = (value.to_bits() & INT32_MASK) as u32 as i32;
         let mut itoa_buf = itoa::Buffer::new();
diff --git a/crates/perry-runtime/src/math.rs b/crates/perry-runtime/src/math.rs
index 5012c33f206..3dcfa6829f9 100644
--- a/crates/perry-runtime/src/math.rs
+++ b/crates/perry-runtime/src/math.rs
@@ -32,7 +32,19 @@ pub extern "C" fn js_math_trunc(value: f64) -> f64 {
 /// `js_math_round_value` (test262 Math/round/S15.8.2.15_A7).
 #[no_mangle]
 pub extern "C" fn js_math_round(value: f64) -> f64 {
-    crate::object::js_math_round_value(js_math_to_number(value))
+    let rounded = crate::object::js_math_round_value(js_math_to_number(value));
+    // P3 B1 negative control (DESIGN-p3 rev 3.1 §5, REVIEW-p3 D4): a runtime
+    // built with `PERRY_FACTS_SABOTAGE=canonnum` returns an INT32-boxed word
+    // from this declared-NUM builtin, so a consumer that trusts the NUM fact
+    // must be caught by its check-mode witness (rc 86). Build-time, so an
+    // ordinary build compiles the branch away.
+    if matches!(option_env!("PERRY_FACTS_SABOTAGE"), Some("canonnum"))
+        && rounded.fract() == 0.0
+        && rounded.abs() < 2_147_483_648.0
+    {
+        return f64::from_bits(crate::value::INT32_TAG | (rounded as i32 as u32 as u64));
+    }
+    rounded
 }
 
 /// Math.sign(x) -> number
diff --git a/crates/perry-stdlib/src/sqlite/bind.rs b/crates/perry-stdlib/src/sqlite/bind.rs
index 4da6f90f336..87dd858ae0d 100644
--- a/crates/perry-stdlib/src/sqlite/bind.rs
+++ b/crates/perry-stdlib/src/sqlite/bind.rs
@@ -655,6 +655,11 @@ mod tests {
         for n in [0i64, 5, -1, i32::MAX as i64, i32::MIN as i64, 1 << 40] {
             let v = unsafe { super::sqlite_value_to_jsvalue(&super::SqliteValue::Integer(n)) };
             assert_eq!(v.bits(), (n as f64).to_bits(), "INTEGER {n}");
+            // node:sqlite's column reader (`sqlite3_column_int64` ->
+            // `node_sqlite_integer_value`): the same raw double (P3 B1 audit,
+            // NUM_SEEDS.md "int32-box producers").
+            let v = unsafe { super::node_sqlite_integer_value(n, false) };
+            assert_eq!(v.bits(), (n as f64).to_bits(), "node:sqlite INTEGER {n}");
         }
     }
 
diff --git a/crates/perry-wpfacts/NUM_SEEDS.md b/crates/perry-wpfacts/NUM_SEEDS.md
new file mode 100644
index 00000000000..b913271da68
--- /dev/null
+++ b/crates/perry-wpfacts/NUM_SEEDS.md
@@ -0,0 +1,143 @@
+# NUM seed audit (P3 B1, DESIGN-p3 rev 3.1 §2.2, REVIEW-p3 D2)
+
+Every non-test use of `prim::NUM` in perry-wpfacts, one row each. A **seed** puts NUM into a node; its citation names the runtime function or the codegen lowering that produces the value, which must be a plain double (canonical IEEE, never a NaN-boxed tag). A **read/map** row tests the fact or maps a family to its prims and seeds nothing.
+
+There are no non-test callers of `JSValue::int32` in perry-runtime or perry-stdlib (DESIGN-p3 §1.1). So every runtime Number below is built by `JSValue::number` / `as f64` / f64 arithmetic. Raw-bits ingress (v8.deserialize, bun:ffi f64/f32) is not modeled by wpfacts (those values are ⊤) and is fixed separately (lane NANB).
+
+`tests/num_seeds_audit.rs` fails when the per-file count of `prim::NUM` uses differs from this table, so a new seed cannot land without a row.
+
+| file:line | kind | value and producer |
+|---|---|---|
+| `derive.rs:35` | read/map | read: tests or masks the fact, seeds nothing |
+| `gen_rest.rs:158` | seed | native-module `array.push` new length: perry-runtime array/push_pop.rs js_array_push_f64 (length re-read, `as f64`) |
+| `gen_rest.rs:170` | seed | native-module receiver method count: perry-runtime returns `as f64` (gen_rest.rs:166 comment); NUM joined with the call's own result node |
+| `gen_rest.rs:545` | seed | Expr::DateNow: perry-runtime date.rs js_date_now (f64 ms) |
+| `gen_rest.rs:549` | seed | Expr::DateParse: perry-runtime date.rs js_date_parse (f64, NaN on failure = canonical f64 NaN) |
+| `gen_rest.rs:556` | seed | Expr::DateUtc: perry-runtime date.rs js_date_utc (f64) |
+| `gen_rest.rs:617` | seed | HIR Math intrinsics (prim_kids): codegen expr/math_simple.rs (llvm.*.f64) and perry-runtime math.rs js_math_* (f64 arithmetic) |
+| `gen_rest.rs:637` | seed | `math_range` result (ToNumber of a Math operand): codegen expr/dispatch.rs lower_math_operand / js_math_to_number (f64) |
+| `gen_rest.rs:644` | seed | ParseInt/ParseFloat/NumberCoerce: perry-runtime builtins/numbers.rs js_parse_int, js_parse_float, js_number_coerce (f64) |
+| `gen_rest.rs:660` | seed | `+x` / ToNumber helper result: codegen unary lowering (fadd 0 / js_number_coerce, f64) |
+| `builtins.rs:1000` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins.rs:1640` | seed | timers: ret_tok(timer) + NUM, so NUM|timer object, never NUM-only. The NUM bit is a spurious over-approximation (REVIEW-p3 D2.5) |
+| `builtins.rs:1801` | seed | Array.from map-callback index: perry-runtime array iteration passes the index `as f64` |
+| `builtins.rs:1833` | seed | Array.from `this` length: NUM|UNDEF |
+| `builtins.rs:1917` | seed | Math namespace calls: codegen math_simple.rs intrinsics; perry-runtime math.rs js_math_round/js_math_trunc/js_math_sign/js_math_log1p/js_math_random (f64 arithmetic). Split per member at B1 |
+| `gen.rs:531` | seed | the shared NUM constant node (prim_const[0]); values flowing into it are audited at their own seed rows |
+| `gen.rs:1286` | seed | `arguments.length`: codegen lowers the argument count `as f64` (sitofp) |
+| `gen_call.rs:1063` | seed | js_iterator_delegate_kind (perry-runtime array/iterator_close.rs): returns a small kind code `as f64` |
+| `gen_expr.rs:889` | seed | `>>>` result: codegen expr/binary.rs lshr + uitofp (f64) |
+| `gen_expr.rs:899` | seed | unary `+`: codegen ToNumber (f64) |
+| `gen_expr.rs:1522` | seed | numeric enum member value: an HIR numeric literal, lowered as a double constant |
+| `solve.rs:46` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:236` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:776` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:790` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:1828` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:1840` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve.rs:1851` | read/map | read: tests or masks the fact, seeds nothing |
+| `bindings.rs:193` | read/map | read: tests or masks the fact, seeds nothing |
+| `bindings.rs:224` | read/map | read: tests or masks the fact, seeds nothing |
+| `bindings.rs:392` | read/map | read: tests or masks the fact, seeds nothing |
+| `bindings.rs:470` | read/map | read: tests or masks the fact, seeds nothing |
+| `bindings.rs:589` | read/map | read: tests or masks the fact, seeds nothing |
+| `dump.rs:470` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/arr_len.rs:42` | seed | array birth length `new Array(k)`: the header length `uitofp` |
+| `solve/lookup.rs:1289` | seed | array `.length` through the chain: header length `uitofp` (array/indexing.rs js_array_length -> u32) |
+| `solve/fields.rs:40` | seed | RegExp `lastIndex` at birth: the Number 0 |
+| `solve/native_value.rs:171` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/apply.rs:1309` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/apply.rs:1337` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/apply.rs:1456` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/apply.rs:1472` | read/map | read: tests or masks the fact, seeds nothing |
+| `solve/apply.rs:1473` | seed | numeric result of an arithmetic or `+` operator: codegen expr/binary.rs and expr/unary.rs lower it inline (fadd/fsub/fmul/fdiv, toint32 + sitofp), and the dynamic arm calls perry-runtime value/dynamic_arith.rs js_dynamic_string_or_number_add / dynamic_add_non_plain, which decodes an INT32 operand (`as_int32() as f64`) and returns `a_num + b_num` (f64) |
+| `solve/apply.rs:1486` | seed | numeric result of an arithmetic or `+` operator: codegen expr/binary.rs and expr/unary.rs lower it inline (fadd/fsub/fmul/fdiv, toint32 + sitofp), and the dynamic arm calls perry-runtime value/dynamic_arith.rs js_dynamic_string_or_number_add / dynamic_add_non_plain, which decodes an INT32 operand (`as_int32() as f64`) and returns `a_num + b_num` (f64) |
+| `solve/apply.rs:1492` | seed | numeric result of an arithmetic or `+` operator: codegen expr/binary.rs and expr/unary.rs lower it inline (fadd/fsub/fmul/fdiv, toint32 + sitofp), and the dynamic arm calls perry-runtime value/dynamic_arith.rs js_dynamic_string_or_number_add / dynamic_add_non_plain, which decodes an INT32 operand (`as_int32() as f64`) and returns `a_num + b_num` (f64) |
+| `solve/apply.rs:1502` | seed | numeric result of an arithmetic or `+` operator: codegen expr/binary.rs and expr/unary.rs lower it inline (fadd/fsub/fmul/fdiv, toint32 + sitofp), and the dynamic arm calls perry-runtime value/dynamic_arith.rs js_dynamic_string_or_number_add / dynamic_add_non_plain, which decodes an INT32 operand (`as_int32() as f64`) and returns `a_num + b_num` (f64) |
+| `solve/apply.rs:1503` | seed | numeric result of an arithmetic or `+` operator: codegen expr/binary.rs and expr/unary.rs lower it inline (fadd/fsub/fmul/fdiv, toint32 + sitofp), and the dynamic arm calls perry-runtime value/dynamic_arith.rs js_dynamic_string_or_number_add / dynamic_add_non_plain, which decodes an INT32 operand (`as_int32() as f64`) and returns `a_num + b_num` (f64) |
+| `solve/apply.rs:1513` | read/map | read: tests or masks the fact, seeds nothing |
+| `gen/primitives.rs:64` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `gen/primitives.rs:100` | seed | computed enum member: NUM|STR, not NUM-only (no consumer drops a test) |
+| `gen/primitives.rs:101` | seed | numeric enum member: a double constant |
+| `gen/primitives.rs:110` | seed | number literal without an interval: a double constant |
+| `gen/primitives.rs:121` | seed | number literal with its point interval: a double constant |
+| `gen/primitives.rs:194` | seed | Math rule result (unary): codegen math intrinsic / js_math_* (f64) |
+| `gen/primitives.rs:201` | seed | Math rule result (n-ary min/max): codegen logical_collections.rs lower_math_minmax_n (llvm.minimum/maximum) |
+| `gen/narrow.rs:810` | seed | narrowing bound node: an interval-only node over program Numbers; no runtime value |
+| `gen/glue.rs:228` | seed | arrayRecordIndex default: codegen array_record lowering, an i32 counter `sitofp` |
+| `gen/glue.rs:230` | seed | arrayRecordLength: codegen array_record payload length `uitofp` |
+| `gen/glue.rs:233` | seed | arrayRecordForUpdate: codegen `mode ? 0 : update` over program Numbers |
+| `builtins/loads.rs:292` | seed | string computed key: STR|NUM|UNDEF|BOOL, not NUM-only |
+| `builtins/loads.rs:381` | seed | global `NaN`/`Infinity`/`undefined`: NUM|UNDEF; the constants are canonical doubles |
+| `builtins/loads.rs:633` | seed | function `length`: closure arity `as f64`; joined with own fields (lookup.rs:221; REVIEW-p3 D2.1) |
+| `builtins/loads.rs:667` | seed | class `length`: as above |
+| `builtins/loads.rs:672` | seed | Array `length`: header length `uitofp` / array/indexing.rs js_array_length |
+| `builtins/loads.rs:677` | seed | array computed key: UNDEF|NUM plus a function token, not NUM-only |
+| `builtins/loads.rs:726` | seed | `.byteOffset` (B1-exposed): typedarray/access.rs, integer `as f64` |
+| `builtins/loads.rs:731` | seed | buffer `size`/`length`/`byteLength`/`byteOffset`: typedarray/access.rs js_typed_array_length, integer `as f64` |
+| `builtins/members.rs:81` | seed | Function.prototype `length` member: as loads.rs:633 |
+| `builtins/members.rs:111` | seed | Array.prototype `length` member: as loads.rs:672 |
+| `builtins/members.rs:147` | seed | String.prototype `length`: string length `as f64` |
+| `builtins/members.rs:242` | seed | Map/Set `size`: perry-runtime map.rs/set.rs js_map_size/js_set_size, `as f64` |
+| `builtins/members.rs:335` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins/members.rs:663` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins/members.rs:748` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins/members.rs:1373` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins/native_protocol.rs:61` | seed | EventEmitter `_` bookkeeping keys: NUM|UNDEF |
+| `builtins/native_protocol.rs:675` | seed | EventEmitter listenerCount/getMaxListeners: perry-runtime event emitter counts `as f64` |
+| `builtins/effects.rs:385` | read/map | family/realm/const mapping: no value of its own; the seeds that use it are audited at their own rows |
+| `builtins/constructors.rs:187` | seed | typed-array elements: NUM|BIGINT, not NUM-only |
+| `builtins/string_methods.rs:94` | seed | replacer argument: STR|NUM|UNDEF, not NUM-only |
+| `builtins/string_methods.rs:215` | seed | charCodeAt/indexOf/lastIndexOf: perry-runtime string/char_ops.rs js_string_char_code_at, string/slice_ops.rs js_string_index_of/js_string_last_index_of (i32/u16 `as f64`; NaN for charCodeAt out of range = canonical NaN) |
+| `builtins/string_methods.rs:216` | seed | codePointAt: NUM|UNDEF; string/char_ops.rs js_string_code_point_at |
+| `builtins/string_methods.rs:282` | seed | localeCompare: string/compare.rs js_string_locale_compare (-1/0/1 `as f64`) |
+| `builtins/string_methods.rs:350` | seed | @@search: RegExp search index `as f64` (string regexp path) |
+| `builtins/string_methods.rs:359` | seed | match record `index`: regexp match index `as f64` |
+| `builtins/string_methods.rs:436` | seed | split lastIndex: a modeled internal value (spec step), integer |
+| `builtins/string_methods.rs:451` | seed | split capture index: modeled internal integer |
+| `builtins/collections.rs:182` | seed | generator resume op code: a small integer the codegen generator step passes `as f64` |
+| `builtins/collections.rs:574` | seed | entries() index field: the iteration index `as f64` |
+| `builtins/collections.rs:588` | seed | callback index: array/iter_methods.rs, `as f64` |
+| `builtins/collections.rs:700` | seed | constructed length: header length `uitofp` |
+| `builtins/collections.rs:719` | seed | species length argument: an integer `as f64` |
+| `builtins/collections.rs:885` | seed | push/pop/shift/unshift/splice new length on array-likes: array/push_pop.rs, array/splice_slice.rs; also above 2^32 a plain double (REVIEW-p3 p4) |
+| `builtins/collections.rs:1003` | seed | index argument/result of the index-walking methods: array/search.rs js_array_indexOf_f64 -> i32, then codegen sitofp |
+| `builtins/collections.rs:1050` | seed | push(spread) result: as collections.rs:885 |
+| `builtins/collections.rs:1177` | seed | index-returning array methods (indexOf/findIndex/...): array/search.rs, array/iter_methods.rs js_array_findIndex (i32 `as f64`) |
+| `builtins/collections.rs:1194` | seed | lastIndexOf/findIndexOf: NUM|BOOL, not NUM-only |
+| `builtins/collections.rs:1410` | seed | Date getters/valueOf: perry-runtime date.rs js_date_get_* (f64) |
+| `builtins/collections.rs:1438` | seed | Date setters' result: date.rs (f64 time value) |
+| `builtins/collections.rs:1536` | seed | TextEncoder.encode result elements: as gen_rest/web.rs:36 |
+| `builtins/collections.rs:1543` | seed | encodeInto read/written: as gen_rest/web.rs:51 |
+| `builtins/collections.rs:1561` | seed | Timer @@toPrimitive: the timer id `as f64` |
+| `builtins/typed_array_methods.rs:69` | seed | buffer length: typedarray/access.rs, integer `as f64` |
+| `builtins/typed_array_methods.rs:76` | seed | fresh typed-array elements: NUM|BIGINT, not NUM-only |
+| `builtins/typed_array_methods.rs:91` | seed | typed-array callback index: typedarray/iterate.rs, `as f64` |
+| `builtins/typed_array_methods.rs:93` | seed | typed-array element: NUM|BIGINT, not NUM-only |
+| `builtins/typed_array_methods.rs:113` | seed | at(): NUM|BIGINT|UNDEF, not NUM-only |
+| `builtins/typed_array_methods.rs:142` | seed | indexOf/lastIndexOf/findIndex results: perry-runtime object/native_call_method/typed_array.rs:271 (`js_array_indexOf_jsvalue(..) as f64`, `js_array_last_index_of_jsvalue(..) as f64`), reached from object/typed_array_proto_thunks.rs ta_index_of_thunk / ta_last_index_of_thunk |
+| `builtins/typed_array_methods.rs:175` | seed | find/findLast: NUM|BIGINT|UNDEF, not NUM-only |
+| `builtins/typed_array_methods.rs:176` | seed | other typed-array Number results (length, reduce of numbers...): typedarray/*.rs, f64 |
+| `derive/element.rs:120` | read/map | read: tests or masks the fact, seeds nothing |
+| `gen_rest/web.rs:36` | seed | TextEncoder.encode result elements: a Uint8Array; typed-array element reads canonicalize (perry-runtime typedarray/access.rs; REVIEW-p3 t4/t5) |
+| `gen_rest/web.rs:51` | seed | TextEncoder.encodeInto `read`/`written`: perry-runtime text.rs, counts `as f64` |
+| `gen_rest/builtin_objects.rs:375` | seed | typed-array view elements (shared buffer): typed-array reads canonicalize NaN (typedarray/access.rs; t4/t5) |
+| `gen_rest/builtin_objects.rs:393` | seed | typed-array elements: as above |
+| `gen_rest/nodes.rs:33` | seed | typed-array elements: NUM|BIGINT, not NUM-only |
+| `gen_rest/collections.rs:15` | seed | push(...spread) new length: array/push_pop.rs, `as f64` |
+| `gen_rest/collections.rs:43` | seed | copyWithin operand ToNumber: operand conversion, not a value the program reads |
+| `gen_rest/collections.rs:48` | seed | copyWithin end operand ToNumber: as above |
+| `gen_rest/collections.rs:63` | seed | callback index argument: perry-runtime array/iter_methods.rs passes the index `as f64` |
+| `gen_rest/collections.rs:152` | seed | groupBy callback index: as above |
+| `gen_rest/collections.rs:213` | seed | callback index (from/forEach): as above |
+| `canonical_numbers.rs:49` | read/map | read: tests or masks the fact, seeds nothing (P3 B1's element-value test) |
+| `canonical_numbers.rs:50` | read/map | read: tests or masks the fact, seeds nothing (P3 B1's element-value test) |
+
+## INT32-box producers claimed by code comments (CWN, P3 B1)
+Two runtime comments claimed live INT32-tagged Number producers. Neither is live: no code path writes an INT32 word for
+a Number, and the comments were stale (fixed in P3 B1).
+
+| comment | code proof | running proof (qb9, main dda8f1e84 vs node 26.8.1) |
+|---|---|---|
+| claim at `perry-runtime/src/closure/dispatch/value_call.rs:410` "V8 supplies INT32-tagged numbers" | The V8 embedding (perry-jsruntime) was removed in #1696. `js_create_callback` is now only a stub that returns `undefined` (`closure/v8_stubs.rs:232`, and the weak Mach-O definition at :103), so nothing reaches `js_closure_v8_callback` with V8 values. The other entry, `js_closure_call_array`, is called by perry-ffi `Closure::call` (args are `JsValue`s, and `from_int32` is `n as f64`) and by ext-http (array elements). | `v8.deserialize(v8.serialize(5))`, an array `[5, -7, 0, 2147483647]` and an object `{a: 5, b: {c: 5}}`: `Object.is(x, 5)`, `x === 5`, `typeof x`, `x + 0.5` and the `Float64Array` round trip all match node. Raw bits: `v8_serde_canonical_tests.rs` asserts that a wire int32 (`'I'` + zigzag) deserializes to exactly `(n as f64).to_bits()` (`v8_serde.rs:727 int_to_value` is `v as f64`). |
+| claim at `perry-runtime/src/json/stringify_scalars.rs:33` "Integer columns from the sqlite binding" | All sqlite integer readers return `JSValue::number(n as f64)`: node:sqlite `bind.rs:400 node_sqlite_integer_value`; user-function arguments `sqlite_callbacks.rs:124 integer_value_checked`; bun:sqlite and better `bind.rs:18 sqlite_value_to_jsvalue`; the ext crate `perry-ext-better-sqlite3/src/lib.rs:90` via perry-ffi `from_int32` = `n as f64`. | node:sqlite `INTEGER` rows (5, -7, 2147483647) through `.all()` and `.get()`: all checks match node. Raw bits: the `bind.rs` test `integer_columns_are_raw_double_numbers` asserts `(n as f64).to_bits()` for both `sqlite_value_to_jsvalue` and `node_sqlite_integer_value`. |
diff --git a/crates/perry-wpfacts/src/bindings.rs b/crates/perry-wpfacts/src/bindings.rs
index a0ff8497326..0839e7be657 100644
--- a/crates/perry-wpfacts/src/bindings.rs
+++ b/crates/perry-wpfacts/src/bindings.rs
@@ -336,6 +336,10 @@ pub struct ModuleBindings {
     /// Method call byte offsets proven field element reads
     /// (`field_read_calls`, b1), sorted.
     pub field_read_calls: Vec<(u32, crate::field_read_calls::FieldReadCall)>,
+    /// Element reads whose value is a plain Number at every copy, by
+    /// `element_offset`, sorted; `true` when the value may also be
+    /// `undefined` (`canonical_numbers`, P3 B1).
+    pub number_element_reads: Vec<(u32, bool)>,
 }
 
 /// An element read `a[i]` whose every receiver is a program Array that
diff --git a/crates/perry-wpfacts/src/canonical_numbers.rs b/crates/perry-wpfacts/src/canonical_numbers.rs
new file mode 100644
index 00000000000..e5206c8a84f
--- /dev/null
+++ b/crates/perry-wpfacts/src/canonical_numbers.rs
@@ -0,0 +1,65 @@
+//! P3 B1 (DESIGN-p3-canonical-numbers rev 3.1 §2): element reads whose value
+//! the facts prove a Number, or a Number or `undefined`.
+//!
+//! The fact is the NUM declaration itself (REVIEW-p3 R2): a node holds only
+//! the Number primitive when every value reaching it is a program Number
+//! (literals and arithmetic, which codegen lowers to plain doubles) or comes
+//! from a builtin whose NUM seed is audited against its runtime producer
+//! (`NUM_SEEDS.md`, checked by `tests/num_seeds_audit.rs`). There is no
+//! separate encoding bit: a value the solver cannot see is ⊤, never NUM-only.
+//!
+//! An element read qualifies when, at every copy of the read, its value node
+//! holds Number (and possibly `undefined`, for a hole or an index past the
+//! end) and nothing else: no other primitive and no token. A copy that does
+//! not qualify drops the site.
+
+use crate::bindings::ModuleBindings;
+use crate::gen::Gen;
+use crate::model::prim;
+
+/// `PERRY_FACTS_CANONICAL_NUMBERS=0` exports nothing.
+pub fn enabled() -> bool {
+    !matches!(
+        std::env::var("PERRY_FACTS_CANONICAL_NUMBERS").as_deref(),
+        Ok("0") | Ok("off") | Ok("false")
+    )
+}
+
+/// Fill `ModuleBindings::number_element_reads` (module docs).
+pub(crate) fn collect(g: &Gen<'_>, bindings: &mut [ModuleBindings]) {
+    if g.m.aborted {
+        return;
+    }
+    // (module, offset) -> Some(may be undefined), or None once a copy fails.
+    let mut sites: std::collections::BTreeMap<(u32, u32), Option<bool>> = Default::default();
+    // A summarized body's value node has one copy per instance
+    // (`Inst::fresh`); the fact must hold for each of them too.
+    let mut copies: std::collections::HashMap<u32, Vec<u32>> = Default::default();
+    for inst in 0..g.m.sum.insts.len() as u32 {
+        g.m.inst_copies(inst, |orig, copy| {
+            copies.entry(orig).or_default().push(copy)
+        });
+    }
+    let nodes = g.element_values.iter().flat_map(|&(mi, offset, n)| {
+        std::iter::once(n)
+            .chain(copies.get(&n).into_iter().flatten().copied())
+            .map(move |c| (mi, offset, c))
+    });
+    for (mi, offset, n) in nodes {
+        let node = &g.m.nodes[n as usize];
+        let number = node.pts.is_empty()
+            && node.prim & prim::NUM != 0
+            && node.prim & !(prim::NUM | prim::UNDEF) == 0;
+        let undef = node.prim & prim::UNDEF != 0;
+        let entry = sites.entry((mi, offset)).or_insert(Some(false));
+        *entry = match (*entry, number) {
+            (Some(prev), true) => Some(prev || undef),
+            _ => None,
+        };
+    }
+    for ((mi, offset), fact) in sites {
+        if let (Some(undef), Some(mb)) = (fact, bindings.get_mut(mi as usize)) {
+            mb.number_element_reads.push((offset, undef));
+        }
+    }
+}
diff --git a/crates/perry-wpfacts/src/gen.rs b/crates/perry-wpfacts/src/gen.rs
index e730b139c27..f82cb917b4d 100644
--- a/crates/perry-wpfacts/src/gen.rs
+++ b/crates/perry-wpfacts/src/gen.rs
@@ -150,6 +150,9 @@ pub struct Gen<'a> {
     pub cjs_unknown_path: NodeId,
     pub read_sites: Vec<ReadSite>,
     pub(crate) element_sites: Vec<ElementSite>,
+    /// `(module, element_offset, value node)` of every `IndexGet` copy
+    /// (`canonical_numbers`, P3 B1).
+    pub(crate) element_values: Vec<(u32, u32, NodeId)>,
     /// Exports whose value is a class declaration (design §11.2).
     pub export_class: FxHashMap<(u32, Atom), TmplId>,
     /// Exports whose value is a function declaration, and the published
@@ -595,6 +598,7 @@ impl<'a> Gen<'a> {
             cjs_unknown_path,
             read_sites: Vec::new(),
             element_sites: Vec::new(),
+            element_values: Vec::new(),
             export_class: FxHashMap::default(),
             export_fn: FxHashMap::default(),
             fn_contracts: Vec::new(),
diff --git a/crates/perry-wpfacts/src/gen_expr.rs b/crates/perry-wpfacts/src/gen_expr.rs
index 2a62bdfa98e..5752f8c8488 100644
--- a/crates/perry-wpfacts/src/gen_expr.rs
+++ b/crates/perry-wpfacts/src/gen_expr.rs
@@ -651,6 +651,11 @@ impl<'a> Gen<'a> {
     pub(crate) fn expr(&mut self, fx: &Fx, e: &Expr) -> NodeId {
         let prev = std::mem::replace(&mut self.m.cur_fn, fx.f);
         let n = self.expr_inner(fx, e);
+        if let Expr::IndexGet { element_offset, .. } = e {
+            if *element_offset != 0 {
+                self.element_values.push((fx.module, *element_offset, n));
+            }
+        }
         if self.diagnostic.is_some() {
             self.diagnostic_expr(fx, e, n);
         }
diff --git a/crates/perry-wpfacts/src/lib.rs b/crates/perry-wpfacts/src/lib.rs
index 18f0c6765f7..63a6879972d 100644
--- a/crates/perry-wpfacts/src/lib.rs
+++ b/crates/perry-wpfacts/src/lib.rs
@@ -18,6 +18,7 @@
 
 pub mod bindings;
 mod builtins;
+pub mod canonical_numbers;
 mod ctor_phase;
 mod decl_units;
 pub mod delta;
@@ -874,6 +875,9 @@ fn compute_act<'a>(
             cfg.sabotage.as_deref() == Some("fieldreadcall"),
         );
     }
+    if canonical_numbers::enabled() {
+        canonical_numbers::collect(&g, &mut bindings);
+    }
     if g.m.aborted {
         // Over budget: claim nothing (sound), keep the shapes for the dump.
         templates.clear();
diff --git a/crates/perry-wpfacts/tests/num_seeds_audit.rs b/crates/perry-wpfacts/tests/num_seeds_audit.rs
new file mode 100644
index 00000000000..db871064b44
--- /dev/null
+++ b/crates/perry-wpfacts/tests/num_seeds_audit.rs
@@ -0,0 +1,109 @@
+//! P3 B1 (DESIGN-p3 rev 3.1 §2.2, REVIEW-p3 D2): every non-test use of
+//! `prim::NUM` in perry-wpfacts has a row in `NUM_SEEDS.md` citing the runtime
+//! function or lowering that produces the value. The counts are compared per
+//! file, so moving a line does not break the test; adding a seed does, until
+//! its row (and its audit) is added.
+
+use std::collections::BTreeMap;
+use std::path::{Path, PathBuf};
+
+/// `prim::NUM` uses outside `#[cfg(test)]` modules and test files.
+fn source_counts(root: &Path) -> BTreeMap<String, usize> {
+    let mut out = BTreeMap::new();
+    let mut stack = vec![root.to_path_buf()];
+    while let Some(dir) = stack.pop() {
+        for entry in std::fs::read_dir(&dir).unwrap() {
+            let path: PathBuf = entry.unwrap().path();
+            if path.is_dir() {
+                stack.push(path);
+                continue;
+            }
+            let rel = path
+                .strip_prefix(root)
+                .unwrap()
+                .to_string_lossy()
+                .replace('\\', "/");
+            let name = path.file_name().unwrap().to_string_lossy().to_string();
+            if !name.ends_with(".rs")
+                || name == "tests.rs"
+                || name.ends_with("_tests.rs")
+                || name.ends_with("_test.rs")
+                || rel.split('/').any(|c| c == "tests")
+            {
+                continue;
+            }
+            let text = std::fs::read_to_string(&path).unwrap();
+            let mut depth: i64 = 0;
+            let mut test_depth: Option<i64> = None;
+            let mut pending = false;
+            let mut n = 0;
+            for line in text.lines() {
+                let s = line.trim();
+                if s.starts_with("#[cfg(test)]") {
+                    pending = true;
+                }
+                if pending && s.starts_with("mod ") && s.ends_with(';')
+                    || pending && s.starts_with("pub mod ") && s.ends_with(';')
+                {
+                    pending = false;
+                }
+                if pending && line.contains('{') && test_depth.is_none() {
+                    test_depth = Some(depth);
+                    pending = false;
+                }
+                if test_depth.is_none() && line.contains("prim::NUM") && !s.starts_with("//") {
+                    n += 1;
+                }
+                depth += line.matches('{').count() as i64 - line.matches('}').count() as i64;
+                if let Some(d) = test_depth {
+                    if depth <= d {
+                        test_depth = None;
+                    }
+                }
+            }
+            if n > 0 {
+                out.insert(rel, n);
+            }
+        }
+    }
+    out
+}
+
+/// Rows of the audit table, per file.
+fn table_counts(table: &str) -> BTreeMap<String, usize> {
+    let mut out = BTreeMap::new();
+    for line in table.lines() {
+        let Some(rest) = line.strip_prefix("| `") else {
+            continue;
+        };
+        let loc = rest.split('`').next().unwrap();
+        let file = loc.rsplit_once(':').map_or(loc, |(f, _)| f);
+        *out.entry(file.to_string()).or_insert(0) += 1;
+    }
+    out
+}
+
+#[test]
+fn every_num_seed_has_an_audit_row() {
+    let crate_dir = Path::new(env!("CARGO_MANIFEST_DIR"));
+    let table = std::fs::read_to_string(crate_dir.join("NUM_SEEDS.md")).unwrap();
+    let rows = table_counts(&table);
+    let uses = source_counts(&crate_dir.join("src"));
+    assert_eq!(
+        uses, rows,
+        "prim::NUM uses (left) and NUM_SEEDS.md rows (right) differ: audit the new seed, cite its runtime producer, and add its row"
+    );
+}
+
+/// Every seed row cites a producer (no empty or placeholder citations).
+#[test]
+fn every_seed_row_cites_a_producer() {
+    let crate_dir = Path::new(env!("CARGO_MANIFEST_DIR"));
+    let table = std::fs::read_to_string(crate_dir.join("NUM_SEEDS.md")).unwrap();
+    for line in table.lines().filter(|l| l.starts_with("| `")) {
+        let cols: Vec<&str> = line.split(" | ").collect();
+        assert!(cols.len() >= 3, "malformed row: {line}");
+        let cit = cols[2].trim_end_matches(" |").trim();
+        assert!(cit.len() > 12, "row without a citation: {line}");
+    }
+}
diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs
index 989c80f67b2..22c9af40806 100644
--- a/crates/perry/src/commands/compile/compile_env.rs
+++ b/crates/perry/src/commands/compile/compile_env.rs
@@ -68,6 +68,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[
     "PERRY_FACTS_ARRAY_LENGTHS",
     "PERRY_FACTS_CONST_LENGTH",
     "PERRY_FACTS_FIELD_READ_CALLS",
+    "PERRY_FACTS_CANONICAL_NUMBERS",
     "PERRY_FACTS_GUARD_PRESENCE",
     "PERRY_FACTS_GUARD_RANGES",
     "PERRY_FACTS_SITE_ARGS",
diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs
index 300fdcff778..2039d583efb 100644
--- a/crates/perry/src/commands/compile/program_facts.rs
+++ b/crates/perry/src/commands/compile/program_facts.rs
@@ -532,6 +532,8 @@ fn elision_for(pf: &perry_wpfacts::ProgramFacts, path: &str) -> perry_codegen::E
             out.call_arg_ranges.insert(*offset, iv.clone());
         }
         out.number_calls.extend(mb.number_calls.iter().copied());
+        out.number_element_reads
+            .extend(mb.number_element_reads.iter().copied());
         for (offset, c) in &mb.field_read_calls {
             let default = match &c.default {
                 None => None,
diff --git a/scripts/check_file_size.sh b/scripts/check_file_size.sh
index f7eb273e690..9a0f55de63d 100755
--- a/scripts/check_file_size.sh
+++ b/scripts/check_file_size.sh
@@ -28,7 +28,7 @@ crates/perry-codegen/src/codegen/mod.rs	3565
 # Representation-aware HIR fact collection; further decomposition is tracked in #1435.
 crates/perry-codegen/src/collectors/hir_facts.rs	2760
 # Representation-aware expression dispatch; further decomposition is tracked in #1435.
-crates/perry-codegen/src/expr/mod.rs	2826
+crates/perry-codegen/src/expr/mod.rs	2827
 # Loop versioning and representation evidence share lowering state; decomposition is tracked in #1435.
 crates/perry-codegen/src/stmt/loops.rs	8290
 # Representation-aware map core; further decomposition is tracked in #1435.
diff --git a/scripts/p3-canonnum-runtime.sh b/scripts/p3-canonnum-runtime.sh
new file mode 100755
index 00000000000..c13dce591e9
--- /dev/null
+++ b/scripts/p3-canonnum-runtime.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+# P3 B1 negative control (DESIGN-p3 rev 3.1 §5, REVIEW-p3 D4): build a runtime
+# whose `js_math_round` returns an INT32-boxed word, for the S0 entry
+# `canonical-number-negative` (scripts/test-verify-facts-s0.py
+# --canonnum-runtime <target>/release).
+#
+#   scripts/p3-canonnum-runtime.sh <cargo-target-dir>
+#
+# The switch is build-time (`option_env!` in perry-runtime/src/math.rs), so the
+# archive must really be rebuilt: the script fails (STALE-ARCHIVE) when
+# libperry_runtime.a did not change.
+set -euo pipefail
+target=${1:?usage: p3-canonnum-runtime.sh <cargo-target-dir>}
+archive="$target/release/libperry_runtime.a"
+before=$(stat -c %Y "$archive" 2>/dev/null || stat -f %m "$archive" 2>/dev/null || echo 0)
+PERRY_FACTS_SABOTAGE=canonnum CARGO_TARGET_DIR="$target" cargo build-perry --release
+after=$(stat -c %Y "$archive" 2>/dev/null || stat -f %m "$archive")
+if [ "$after" = "$before" ]; then
+  echo "STALE-ARCHIVE: $archive was not rebuilt" >&2
+  exit 1
+fi
+bash "$(dirname "$0")/gc_call_effects/sidecars.sh" "$target/release"
+echo "canonnum runtime: $target/release"
diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py
index e5ce8628475..0c4585222d6 100644
--- a/scripts/test-verify-facts-s0.py
+++ b/scripts/test-verify-facts-s0.py
@@ -39,6 +39,9 @@ def main():
     parser.add_argument("--perry", type=Path, required=True)
     parser.add_argument("--node", default="node")
     parser.add_argument("--out", type=Path, required=True)
+    parser.add_argument("--canonnum-runtime", type=Path,
+                        help="target/release of a runtime built with PERRY_FACTS_SABOTAGE=canonnum "
+                             "(scripts/p3-canonnum-runtime.sh); without it only the correct arm runs")
     args = parser.parse_args()
     args.perry = args.perry.resolve()
     args.out = args.out.resolve()
@@ -120,6 +123,22 @@ def oracle(source, *argv):
                 assert observed.returncode == 0 and observed.stdout == oracle(source), observed
             save(arm, status=observed.returncode)
 
+    # P3 B1 (DESIGN-p3 rev 3.1 §5, REVIEW-p3 D4): this arm sabotages the
+    # RUNTIME, not the facts. `js_math_round` built with
+    # PERRY_FACTS_SABOTAGE=canonnum returns an INT32-boxed word, and the
+    # canonical-number witness must report it with rc 86 exactly.
+    source = fixtures / "canonical-number-negative.ts"
+    exe, e = compile_(source, "canonical-number-negative-correct")
+    observed = observe(exe, e)
+    assert observed.returncode == 0 and observed.stdout == oracle(source), observed
+    save("canonical-number-negative-correct", status=0)
+    if args.canonnum_runtime:
+        runtime = str(args.canonnum_runtime.resolve())
+        exe, e = compile_(source, "canonical-number-negative-false", PERRY_RUNTIME_DIR=runtime)
+        value = report(observe(exe, e))
+        assert value["predicate"] == "canonical number", value
+        save("canonical-number-negative-false", status=86)
+
     source = fixtures / "parallel-bodies.ts"
     exe, e = compile_(source, "parallel-bodies")
     observed = observe(exe, e)
diff --git a/scripts/verify_facts_s0/canonical-number-negative.ts b/scripts/verify_facts_s0/canonical-number-negative.ts
new file mode 100644
index 00000000000..14dd21a42bb
--- /dev/null
+++ b/scripts/verify_facts_s0/canonical-number-negative.ts
@@ -0,0 +1,22 @@
+// P3 B1 (DESIGN-p3 rev 3.1 §5): `Math.round` is a declared-NUM builtin. A
+// runtime built with PERRY_FACTS_SABOTAGE=canonnum returns an INT32-boxed word
+// from it. The value is stored into an array, and the element read the facts
+// prove a plain Number reaches a compare (C1), an arithmetic leaf (C2) and a
+// Number parameter (C4): the canonical-number witness must report it (rc 86).
+// The input is not a constant, so `Math.round` really runs.
+function twice(x: number): number {
+  return x * 2;
+}
+function run(seed: number): string {
+  const vals: number[] = [];
+  for (let i = 0; i < 4; i++) vals.push(Math.round(seed + i + 0.4));
+  let hits = 0;
+  let total = 0;
+  for (let i = 0; i < vals.length; i++) {
+    if (vals[i] === seed + i) hits++;
+    total = total + vals[i] * 3;
+    total += twice(vals[i]);
+  }
+  return hits + " " + total;
+}
+console.log(run(process.argv.length));
diff --git a/tests/parity/language/number/test_p3_canonical_numbers.ts b/tests/parity/language/number/test_p3_canonical_numbers.ts
new file mode 100644
index 00000000000..5cfd5d71261
--- /dev/null
+++ b/tests/parity/language/number/test_p3_canonical_numbers.ts
@@ -0,0 +1,86 @@
+// P3 B1 controls (DESIGN-p3 rev 3.1 §5): compares and arithmetic over element
+// reads the facts prove plain Numbers (C1, C2) and Number parameters (C4).
+// Every result must match node exactly, with the fact on, off and in check
+// mode. Loops run inside functions with parameter bounds.
+
+// Holey arrays and reads past the end: Number-or-undefined (REVIEW-p3 D1).
+const holey = [1, , 3];
+holey.length = 10;
+function same(i: number, j: number): boolean { return holey[i] === holey[j]; }
+function differ(i: number, j: number): boolean { return holey[i] !== holey[j]; }
+console.log(same(5, 6), same(1, 5), same(1, 20), same(0, 0), same(0, 2), differ(5, 6), differ(0, 2));
+function rel(i: number): string {
+  const v = holey[i];
+  return [v < 1, v <= 1, v > 1, v >= 1, !(v < 1)].join(",");
+}
+console.log(rel(0), rel(1), rel(2), rel(15));
+
+// NaN, -0, +0 (both operands proven Numbers).
+const z = [0, -0, NaN, 0 / 0, Infinity, -Infinity];
+function eq(i: number, j: number): boolean { return z[i] === z[j]; }
+console.log(eq(0, 1), eq(2, 2), eq(2, 3), eq(3, 3), eq(4, 4), eq(4, 5), eq(0, 9), eq(9, 9));
+function zrel(n: number): string {
+  let s = "";
+  for (let i = 0; i < n; i++) for (let j = 0; j < n; j++) s += (z[i] < z[j] ? "<" : z[i] > z[j] ? ">" : "=");
+  return s;
+}
+console.log(zrel(z.length));
+
+// `?? d` over a Number-or-undefined read is a Number: arithmetic (C2) and compare.
+const counts = [3, , 5];
+function sum(n: number): number {
+  let s = 0;
+  for (let i = 0; i < n; i++) s = s + (counts[i] ?? 0) * 2 - (counts[i] ?? 1);
+  return s;
+}
+console.log(sum(5), sum(0));
+
+// Builtin NUM producers stored and read back: Math.round, .length, push, indexOf.
+function produced(k: number): number[] {
+  const out: number[] = [];
+  out.push(Math.round(k + 0.4));
+  out.push(out.length);
+  out.push([5, 6, 7].indexOf(k));
+  out.push(out.push(9));
+  return out;
+}
+function useProduced(k: number): string {
+  const p = produced(k);
+  let s = "";
+  for (let i = 0; i < p.length; i++) s += (p[i] === k ? "k" : p[i] > k ? "+" : "-") + (p[i] * 3 | 0) + " ";
+  return s;
+}
+console.log(useProduced(6), useProduced(2));
+
+// int32 overflow to double, through arithmetic on proven reads.
+const big = [2147483647, -2147483648, 4294967295];
+function wrap(i: number): string {
+  const v = big[i];
+  return [v + 1, v * 2, v | 0, v >>> 0, v - 1 === 2147483646].join(",");
+}
+console.log(wrap(0), wrap(1), wrap(2));
+
+// A Number parameter (C4) fed by proven reads and literals.
+function half(x: number): number { return x / 2; }
+function halves(n: number): number {
+  let s = 0;
+  for (let i = 0; i < n; i++) s += half(z[i % 2]) + half(counts[0] ?? 0);
+  return s;
+}
+console.log(halves(4), Object.is(half(-0), -0));
+
+// Values the facts do not cover keep their tests: JSON.parse through any, BigInt.
+function parsed(text: string): string {
+  const xs: any[] = JSON.parse(text);
+  let s = "";
+  for (let i = 0; i < xs.length; i++) s += (xs[i] === 1) + ":" + (xs[i] + 1) + " ";
+  return s;
+}
+console.log(parsed("[1, \"1\", null, 2.5]"));
+const bigs = [1n, 2n];
+function bigsum(n: number): bigint {
+  let s = 0n;
+  for (let i = 0; i < n; i++) s = s + bigs[i] * 2n;
+  return s;
+}
+console.log(String(bigsum(2)));