diff --git a/changelog.d/6905-repsel-p2-specialized-abi.md b/changelog.d/6905-repsel-p2-specialized-abi.md
new file mode 100644
index 0000000000..ce832360b1
--- /dev/null
+++ b/changelog.d/6905-repsel-p2-specialized-abi.md
@@ -0,0 +1,11 @@
+Representation-selection Phase 2 (`docs/representation-selection-rfc.md` §5.4–§5.6): the specialized calling convention — bounded monomorphization. Statically-proven call sites now call a full-body specialized entry with raw-typed args (typed-array header ptr, raw i32/f64), chosen statically with no per-call guard.
+
+- Full-body specialized entries: `compile_function` parameterized on a call-site-derived rep tuple (`Boxed`/`I32`/`F64`/`TaPtr{kind, const_len}`); internal `{public}__spec_<mangle>` symbols emitted before the public bodies; mutually exclusive with `i64_specialized` and the typed_abi clone families; boxed return. `I32` params bind into Phase 1 canonical slots; `TaPtr` params bind as proven `BufferViewSlot`s with data pointer/length hoisted once at entry (sound: `GC_TYPE_TYPED_ARRAY`/`GC_TYPE_BUFFER` are non-movable, non-view typed arrays cannot detach or resize).
+- `collectors/spec_abi_sites.rs` pre-pass (ctx-free, two-phase): proves `TaPtr` bindings (single top-level binding, non-view construction form, never reassigned module-wide, never closure-referenced) and judges direct call sites; dominant-tuple selection with callee-side demotion. Tier A dispatch re-proves every slot at the call site by construction (direct call, no diamond); Tier B keeps the guarded-diamond shape for declaration-proven tuples. Closures/wrappers/cross-module paths only ever reach the public boxed symbol (source-ratchet test).
+- Proven-region tier: masked-window regions over fully compile-time-proven, undowngraded views lower as one guard-free fast copy (no probes, no alternate copies), and proven-view element stores join the region. New checked proven-view element access (`expr/proven_view_access.rs`): inline `icmp ult` bounds + bare load/store for dynamic exact-i32 indices, bit-exact with the runtime helpers.
+- wrap-i32 additive accumulators: `int_valued_ta_locals` admits straight-line `Add`/`Sub` chains over exact operands (in-bounds-proven int-TA reads via constant lengths, literals, bitwise results, sibling candidates) carrying the ToInt32 image in the canonical i32 slot; loop-carried additive writes, unproven operands, and index-position reads stay rejected.
+- FEAT_JSCVT: `toint32_wrap` emits `@llvm.aarch64.fjcvtzs` (spec-exact single-instruction ECMAScript ToInt32) on arm64 macOS targets (`PERRY_JSCVT` kill switch; iOS/tvOS device targets keep the portable tower — A7–A11 lack the instruction).
+- Audits: `clamp_detect` gains the missing `was_plain_async` gates; top-level `const` numeric module bindings fold into `compile_time_constants` (TDZ-flagged bindings excluded); typed-array-typed `PutValueSet` element writes route to `index_set`'s typed arm; never-bound shadow-slot clears elided; spec `TaPtr` params skip the redundant callee-side root bind.
+- Flags `PERRY_SPECIALIZED_ABI` (default on) and `PERRY_SPECIALIZED_ABI_MAX` (default 64) + `PERRY_JSCVT`, all object-cache-keyed; rejections recorded via the typed-clone rejection vocabulary; RFC §5.4/§8 updated — anti-bloat is proven by the empirical flag-on/off corpus measurement (the `binary-size` CI job only sees the compiler), measured at +0.0063% aggregate over a 32-binary corpus.
+
+RFC §7 acceptance met on the protocol box (min-of-9, cache-busted): real unrolled untyped bcryptjs `_encipher` (`enc_real.ts`) 834 → **126 ms vs Node 134 ms**, byte-exact; post-`-O3` specialized entry has zero `js_dyn_index_get`/`js_dynamic_*`/`js_typed_array_*` calls and zero kind guards (pure-i32 Feistel: `fadd 0`, `add i32 33`, `xor i32 50`). Four new routing gap tests (polymorphic coexistence, view+detach, reassignment, recursion/escape) pass byte-exact flag on/off and under `PERRY_GC_FORCE_EVACUATE=1`; full gap suite: no new untriaged failures.
diff --git a/crates/perry-codegen/src/block.rs b/crates/perry-codegen/src/block.rs
index 50d0d35d11..26614a2ea1 100644
--- a/crates/perry-codegen/src/block.rs
+++ b/crates/perry-codegen/src/block.rs
@@ -606,6 +606,18 @@ impl LlBlock {
     /// (poison otherwise); every clamped case is mathematically 0 anyway.
     pub fn toint32_wrap(&mut self, val: &str) -> String {
         use crate::types::{I1, I32, I64};
+        // ARMv8.3 FEAT_JSCVT: `fjcvtzs` IS ECMAScript ToInt32 in one
+        // instruction — truncate toward zero, wrap modulo 2^32, NaN/±Inf/-0
+        // → 0. Replaces the ~25-op branchless tower below on targets that
+        // have it (all Apple Silicon); the tower remains the portable path.
+        if crate::codegen::helpers::jscvt_enabled() {
+            let r = self.reg();
+            self.emit(format!(
+                "{} = call i32 @llvm.aarch64.fjcvtzs(double {})",
+                r, val
+            ));
+            return r;
+        }
         let bits = self.bitcast_double_to_i64(val);
         let exp_shifted = self.lshr(I64, &bits, "52");
         let bexp = self.and(I64, &exp_shifted, "2047");
diff --git a/crates/perry-codegen/src/codegen/closure.rs b/crates/perry-codegen/src/codegen/closure.rs
index 22b2388f22..7d080fd738 100644
--- a/crates/perry-codegen/src/codegen/closure.rs
+++ b/crates/perry-codegen/src/codegen/closure.rs
@@ -850,6 +850,9 @@ pub(super) fn compile_closure(
         integer_locals: native_facts.integer_locals(),
         not_bigint_locals: native_facts.not_bigint_locals(),
         unsigned_i32_locals: native_facts.unsigned_i32_locals(),
+        // Conservative: treat every slot as possibly-bound (param binds are
+        // emitted before FnCtx exists here), so clears never get skipped.
+        shadow_slots_bound: shadow_slot_map.values().copied().collect(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
@@ -866,6 +869,9 @@ pub(super) fn compile_closure(
         local_slot_reps: HashMap::new(),
         repsel_context_allows_canonical_i32: repsel_allows,
         repsel_closure_ref_locals: repsel_closure_refs,
+        spec_abi_functions: &cross_module.spec_abi_functions,
+        spec_ta_bindings: &cross_module.spec_ta_bindings,
+        spec_ta_ready: std::collections::HashSet::new(),
         i1_local_slots: HashMap::new(),
         index_used_locals: native_facts.index_used_locals(),
         strictly_i32_bounded_locals: native_facts.strictly_i32_bounded_locals(),
diff --git a/crates/perry-codegen/src/codegen/entry.rs b/crates/perry-codegen/src/codegen/entry.rs
index fc065753ee..68a41ed565 100644
--- a/crates/perry-codegen/src/codegen/entry.rs
+++ b/crates/perry-codegen/src/codegen/entry.rs
@@ -749,6 +749,7 @@ pub(super) fn compile_module_entry(
             integer_locals: main_native_facts.integer_locals(),
             not_bigint_locals: main_native_facts.not_bigint_locals(),
             unsigned_i32_locals: main_native_facts.unsigned_i32_locals(),
+            shadow_slots_bound: main_shadow_slot_map.values().copied().collect(),
             shadow_slot_map: main_shadow_slot_map,
             persistent_shadow_slots: std::collections::HashSet::new(),
             shadow_slot_clears_after_stmt: main_shadow_slot_clears_after_stmt,
@@ -768,6 +769,9 @@ pub(super) fn compile_module_entry(
             // import/init machinery; the win lives in function bodies).
             repsel_context_allows_canonical_i32: false,
             repsel_closure_ref_locals: std::collections::HashSet::new(),
+            spec_abi_functions: &cross_module.spec_abi_functions,
+            spec_ta_bindings: &cross_module.spec_ta_bindings,
+            spec_ta_ready: std::collections::HashSet::new(),
             i1_local_slots: HashMap::new(),
             index_used_locals: main_native_facts.index_used_locals(),
             strictly_i32_bounded_locals: main_native_facts.strictly_i32_bounded_locals(),
@@ -1360,6 +1364,7 @@ pub(super) fn compile_module_entry(
             integer_locals: init_native_facts.integer_locals(),
             not_bigint_locals: init_native_facts.not_bigint_locals(),
             unsigned_i32_locals: init_native_facts.unsigned_i32_locals(),
+            shadow_slots_bound: init_shadow_slot_map.values().copied().collect(),
             shadow_slot_map: init_shadow_slot_map,
             persistent_shadow_slots: std::collections::HashSet::new(),
             shadow_slot_clears_after_stmt: init_shadow_slot_clears_after_stmt,
@@ -1379,6 +1384,9 @@ pub(super) fn compile_module_entry(
             // import/init machinery; the win lives in function bodies).
             repsel_context_allows_canonical_i32: false,
             repsel_closure_ref_locals: std::collections::HashSet::new(),
+            spec_abi_functions: &cross_module.spec_abi_functions,
+            spec_ta_bindings: &cross_module.spec_ta_bindings,
+            spec_ta_ready: std::collections::HashSet::new(),
             i1_local_slots: HashMap::new(),
             index_used_locals: init_native_facts.index_used_locals(),
             strictly_i32_bounded_locals: init_native_facts.strictly_i32_bounded_locals(),
diff --git a/crates/perry-codegen/src/codegen/function.rs b/crates/perry-codegen/src/codegen/function.rs
index 0c962f3076..7f26971ebc 100644
--- a/crates/perry-codegen/src/codegen/function.rs
+++ b/crates/perry-codegen/src/codegen/function.rs
@@ -17,6 +17,10 @@ use crate::types::{LlvmType, DOUBLE, I1, I32, I64, I8, PTR};
 use super::helpers::shadow_stack_enabled;
 use super::helpers::{inline_hot_small_enabled, inline_hot_small_size_cap, INLINE_HOT_SMALL_MIN};
 use super::opts::CrossModuleCtx;
+use super::spec_abi::{
+    spec_function_name, spec_rep_llvm_ty, spec_ta_kind_class_name, spec_ta_kind_elem_width,
+    SpecFnPlan,
+};
 use super::typed_abi::{
     emit_typed_arg_guard, emit_typed_arg_to_raw, generic_function_body_name, lower_typed_f64_body,
     lower_typed_i1_body, lower_typed_i32_body, lower_typed_string_body, typed_f64_function_name,
@@ -337,12 +341,20 @@ pub(super) fn compile_function(
     closure_rest_params: &HashMap<u32, usize>,
     cross_module: &CrossModuleCtx,
     typed_public_trampoline: Option<TypedFunctionTrampolineKind>,
+    spec_entry: Option<&SpecFnPlan>,
 ) -> Result<()> {
     let public_llvm_name = func_names
         .get(&f.id)
         .cloned()
         .ok_or_else(|| anyhow!("function name not resolved for {}", f.name))?;
-    let llvm_name = if typed_public_trampoline.is_some() {
+    let llvm_name = if let Some(plan) = spec_entry {
+        // Spec entries are an ADDITIONAL internal symbol next to the ordinary
+        // public body — never combined with the typed_abi trampoline scheme
+        // (mutual exclusion is enforced at plan selection).
+        debug_assert!(typed_public_trampoline.is_none());
+        debug_assert_eq!(plan.reps.len(), f.params.len());
+        spec_function_name(&public_llvm_name, &plan.reps)
+    } else if typed_public_trampoline.is_some() {
         generic_function_body_name(&public_llvm_name)
     } else {
         public_llvm_name.clone()
@@ -350,17 +362,27 @@ pub(super) fn compile_function(
 
     // Phase A assumes all user-function params are `double`. Parameter
     // registers are named `%arg{LocalId}` so the body can store them into
-    // alloca slots keyed by the same HIR LocalId.
-    let params: Vec<(LlvmType, String)> = f
-        .params
-        .iter()
-        .map(|p| (DOUBLE, format!("%arg{}", p.id)))
-        .collect();
+    // alloca slots keyed by the same HIR LocalId. Specialized entries
+    // (representation-selection Phase 2) instead type each parameter register
+    // by its rep — raw i32, raw f64, or raw typed-array header pointer (i64).
+    let params: Vec<(LlvmType, String)> = match spec_entry {
+        Some(plan) => f
+            .params
+            .iter()
+            .zip(plan.reps.iter())
+            .map(|(p, rep)| (spec_rep_llvm_ty(*rep), format!("%arg{}", p.id)))
+            .collect(),
+        None => f
+            .params
+            .iter()
+            .map(|p| (DOUBLE, format!("%arg{}", p.id)))
+            .collect(),
+    };
 
     let ic_base = llmod.ic_counter;
     let buffer_alias_base = llmod.buffer_alias_counter;
     let lf = llmod.define_function(&llvm_name, DOUBLE, params);
-    if typed_public_trampoline.is_some() {
+    if typed_public_trampoline.is_some() || spec_entry.is_some() {
         lf.linkage = "internal".to_string();
     }
 
@@ -422,13 +444,61 @@ pub(super) fn compile_function(
     // Store each param into an alloca slot, collecting LocalId → slot
     // mappings. We release the &mut LlBlock at scope end before handing
     // the function over to the FnCtx lowering pass.
+    //
+    // Specialized entries bind per-rep:
+    //  - `I32` → straight into a canonical i32 slot (Phase 1 `SlotRep`
+    //    mechanism; the raw `%arg` i32 stores with ZERO conversions and no
+    //    double slot / no shadow binding — a number is never a GC root).
+    //    Plan selection guarantees the param is never reassigned and never
+    //    closure-referenced, so the canonical slot is trivially sound.
+    //  - `TaPtr` → NaN-box the raw header pointer ONCE into the ordinary
+    //    boxed double slot (all generic body paths stay correct). No callee
+    //    shadow binding is emitted — see the arm below: every route into this
+    //    entry is a Tier-A call whose argument is the caller's proven,
+    //    never-reassigned ROOTED binding, which keeps the header live for the
+    //    whole call.
+    //  - `Boxed`/`F64` → exactly today's binding (a raw f64 IS its box).
+    let mut spec_i32_param_slots: HashMap<u32, String> = HashMap::new();
+    let mut bound_param_slots: HashSet<u32> = HashSet::new();
     let locals: HashMap<u32, String> = {
         let blk = lf.block_mut(0).unwrap();
         let mut map = HashMap::new();
-        for p in &f.params {
+        for (idx, p) in f.params.iter().enumerate() {
             let arg_name = format!("%arg{}", p.id);
+            match spec_entry.map(|plan| plan.reps[idx]) {
+                Some(crate::collectors::SpecParamRep::I32) => {
+                    if crate::expr::canonical_i32_locals_enabled() {
+                        let slot = blk.alloca(I32);
+                        blk.store(I32, &arg_name, &slot);
+                        spec_i32_param_slots.insert(p.id, slot);
+                    } else {
+                        // Phase-1 kill switch: keep the boxed protocol; one
+                        // conversion at entry instead of one per call site.
+                        let as_f64 = blk.sitofp(I32, &arg_name, DOUBLE);
+                        let slot = blk.alloca(DOUBLE);
+                        blk.store(DOUBLE, &as_f64, &slot);
+                        map.insert(p.id, slot);
+                    }
+                    continue;
+                }
+                Some(crate::collectors::SpecParamRep::TaPtr { .. }) => {
+                    let boxed = crate::expr::nanbox_pointer_inline(blk, &arg_name);
+                    let slot = blk.alloca(DOUBLE);
+                    blk.store(DOUBLE, &boxed, &slot);
+                    // No callee-side shadow binding: every route into this
+                    // entry is a Tier-A call whose argument is a proven
+                    // never-reassigned rooted binding (module-global root or
+                    // caller-frame slot) that stays live for the whole call,
+                    // and typed-array storage is non-movable — the callee
+                    // root would be redundant TLS traffic on the hot path.
+                    map.insert(p.id, slot);
+                    continue;
+                }
+                _ => {}
+            }
             let slot = super::arguments::store_param_slot(blk, p, &boxed_vars, &arg_name);
             if let Some(slot_idx) = shadow_slot_map.get(&p.id).copied() {
+                bound_param_slots.insert(slot_idx);
                 blk.call_void(
                     "js_shadow_slot_bind",
                     &[(I32, &slot_idx.to_string()), (PTR, &slot)],
@@ -450,6 +520,27 @@ pub(super) fn compile_function(
     for p in &f.params {
         local_types.insert(p.id, p.ty.clone());
     }
+    // Specialized entry: stamp the proven reps over the (usually `Any`)
+    // declared types BEFORE the native-fact collectors run, so every type
+    // predicate (int-valued locals, typed-array receiver classification,
+    // integer index proofs) sees the by-construction proof. Sound because
+    // plan selection demoted any reassigned/closure-referenced param to
+    // `Boxed` — a stamped param provably holds this rep for the whole body.
+    if let Some(plan) = spec_entry {
+        for (p, rep) in f.params.iter().zip(plan.reps.iter()) {
+            match rep {
+                crate::collectors::SpecParamRep::I32 => {
+                    local_types.insert(p.id, perry_hir::types::Type::Int32);
+                }
+                crate::collectors::SpecParamRep::TaPtr { kind, .. } => {
+                    if let Some(class) = spec_ta_kind_class_name(*kind) {
+                        local_types.insert(p.id, perry_hir::types::Type::Named(class.to_string()));
+                    }
+                }
+                crate::collectors::SpecParamRep::Boxed | crate::collectors::SpecParamRep::F64 => {}
+            }
+        }
+    }
 
     // Pre-walk: which locals need to be boxed? A local is boxed when
     // it's captured by a closure AND written by someone (either the
@@ -466,7 +557,25 @@ pub(super) fn compile_function(
         .collect();
     let flat_const_ids: std::collections::HashSet<u32> =
         cross_module.flat_const_arrays.keys().copied().collect();
-    let native_facts = crate::collectors::collect_native_region_fact_graph(
+    // Spec-entry TaPtr params carry pre-pass-proven constant element counts —
+    // feed them to the fact collectors (in-bounds proofs for the wrap-i32
+    // additive admission).
+    let spec_ta_lens: HashMap<u32, i64> = spec_entry
+        .map(|plan| {
+            f.params
+                .iter()
+                .zip(plan.reps.iter())
+                .filter_map(|(p, rep)| match rep {
+                    crate::collectors::SpecParamRep::TaPtr {
+                        const_len: Some(len),
+                        ..
+                    } => Some((p.id, *len)),
+                    _ => None,
+                })
+                .collect()
+        })
+        .unwrap_or_default();
+    let native_facts = crate::collectors::collect_native_region_fact_graph_with_spec_lens(
         &f.body,
         &f.params,
         &flat_const_ids,
@@ -479,8 +588,23 @@ pub(super) fn compile_function(
         classes,
         &cross_module.compile_time_constants,
         &cross_module.module_dispatch,
+        &spec_ta_lens,
     );
 
+    if let Some(plan) = spec_entry {
+        if std::env::var("PERRY_REPSEL_DEBUG").as_deref() == Ok("1") {
+            eprintln!(
+                "repsel: spec entry '{}' tuple=[{}] [{}]",
+                f.name,
+                plan.reps
+                    .iter()
+                    .map(|r| r.label())
+                    .collect::<Vec<_>>()
+                    .join(","),
+                strings.module_prefix()
+            );
+        }
+    }
     // Representation-selection Phase 1: canonical-i32 locals are allowed in
     // plain synchronous function bodies only. Async / generator /
     // `was_plain_async` bodies route locals through shared cells (the
@@ -581,6 +705,7 @@ pub(super) fn compile_function(
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
+        shadow_slots_bound: bound_param_slots,
         arena_state_slot: None,
         class_keys_slots: HashMap::new(),
         cached_lengths: HashMap::new(),
@@ -590,10 +715,18 @@ pub(super) fn compile_function(
         masked_region_scalar_locals: std::collections::HashSet::new(),
         suppressed_cleared_shadow_slots: std::collections::HashSet::new(),
         class_field_loop_facts: Vec::new(),
-        i32_counter_slots: HashMap::new(),
-        local_slot_reps: HashMap::new(),
+        // Specialized entries seed the canonical-i32 registry with their raw
+        // i32 params (empty otherwise — identical to the pre-phase behavior).
+        local_slot_reps: spec_i32_param_slots
+            .keys()
+            .map(|id| (*id, crate::expr::SlotRep::I32))
+            .collect(),
+        i32_counter_slots: spec_i32_param_slots,
         repsel_context_allows_canonical_i32: repsel_allows,
         repsel_closure_ref_locals: repsel_closure_refs,
+        spec_abi_functions: &cross_module.spec_abi_functions,
+        spec_ta_bindings: &cross_module.spec_ta_bindings,
+        spec_ta_ready: std::collections::HashSet::new(),
         i1_local_slots: HashMap::new(),
         index_used_locals: native_facts.index_used_locals(),
         strictly_i32_bounded_locals: native_facts.strictly_i32_bounded_locals(),
@@ -735,10 +868,76 @@ pub(super) fn compile_function(
                 alias: AliasState::Unknown,
                 length_source: Some(LengthSource::Unknown),
                 native_owned: None,
+                // Declared-type hoist only — the construction form is unknown,
+                // so no inline-storage proof.
+                storage_inline_proven: false,
             },
         );
     }
 
+    // Representation-selection Phase 2: bind each `TaPtr` param as a PROVEN
+    // BufferViewSlot with the data pointer hoisted ONCE at entry (modeled on
+    // the Buffer-param hoist above). The call-site pre-pass proved a fresh
+    // non-view construction, so kind/data/length are fixed for the array's
+    // lifetime: element accesses lower through the strong bare-load machinery
+    // (`ta_int_elem_load_is_i32_provable`, `lower_typed_array_load`, the
+    // proven-view checked tier) with bounds checks against the entry length —
+    // and NEVER through the per-site guarded fast paths (`ta_param_f64_read`
+    // skips receivers with a registered view slot). GC note: the header stays
+    // live through the CALLER's proven never-reassigned rooted binding (a
+    // module-global root or the caller's own frame slot — the only routes into
+    // this entry are Tier-A calls whose args carry that proof); the hoisted
+    // data pointer stays valid because typed-array storage is non-movable
+    // (`gc/types.rs`: `GC_TYPE_TYPED_ARRAY`/`GC_TYPE_BUFFER` `movable: false`)
+    // and a non-view typed array cannot be detached or resized.
+    if let Some(plan) = spec_entry {
+        for (p, rep) in f.params.iter().zip(plan.reps.iter()) {
+            let crate::collectors::SpecParamRep::TaPtr { kind, const_len } = rep else {
+                continue;
+            };
+            let Some((elem, width)) = spec_ta_kind_elem_width(*kind) else {
+                continue;
+            };
+            let Some(param_slot) = ctx.locals.get(&p.id).cloned() else {
+                continue;
+            };
+            let blk = ctx.block();
+            let arg_val = blk.load(DOUBLE, &param_slot);
+            let handle = crate::expr::unbox_to_i64(blk, &arg_val);
+            let handle_ptr = blk.inttoptr(I64, &handle);
+            // TypedArrayHeader layout: length at +0, data at +16.
+            let data_ptr = blk.gep(I8, &handle_ptr, &[(I32, "16")]);
+            let data_slot = ctx.func.alloca_entry(PTR);
+            ctx.block().store(PTR, &data_ptr, &data_slot);
+            let scope_idx = ctx.buffer_alias_base + ctx.buffer_data_slots.len() as u32;
+            ctx.buffer_data_slots
+                .insert(p.id, (data_slot.clone(), scope_idx));
+            ctx.buffer_view_slots.insert(
+                p.id,
+                BufferViewSlot {
+                    data_slot,
+                    length_slot: None,
+                    scope_idx: Some(scope_idx),
+                    elem,
+                    element_width_bytes: width,
+                    index_unit: BufferIndexUnit::Element,
+                    view_byte_offset: Some(0),
+                    length_offset_from_data: -16,
+                    // Distinct `TaPtr` args are distinct fresh allocations
+                    // (the Tier A call-site match rejects duplicate locals),
+                    // so pairwise noalias holds by construction.
+                    alias: AliasState::NoAliasProven,
+                    length_source: Some(match const_len {
+                        Some(len) => LengthSource::Constant(*len),
+                        None => LengthSource::Unknown,
+                    }),
+                    native_owned: None,
+                    storage_inline_proven: true,
+                },
+            );
+        }
+    }
+
     if f.is_async {
         stmt::lower_async_rejecting_top_level_stmts(&mut ctx, &f.body)
             .with_context(|| format!("lowering async body of '{}'", f.name))?;
diff --git a/crates/perry-codegen/src/codegen/helpers.rs b/crates/perry-codegen/src/codegen/helpers.rs
index 0674e3f27d..c8bfdf5822 100644
--- a/crates/perry-codegen/src/codegen/helpers.rs
+++ b/crates/perry-codegen/src/codegen/helpers.rs
@@ -185,6 +185,30 @@ pub(crate) fn write_barriers_enabled() -> bool {
 
 thread_local! {
     static FULL_OUTLINE_IC: std::cell::Cell<bool> = const { std::cell::Cell::new(false) };
+    static JSCVT: std::cell::Cell<bool> = const { std::cell::Cell::new(false) };
+}
+
+/// FEAT_JSCVT (`fjcvtzs`) availability for the CURRENT module's target: the
+/// single-instruction, spec-exact ECMAScript `ToInt32` on ARMv8.3+. Only
+/// arm64 macOS triples opt in — every Apple Silicon Mac (M1+) is ≥ ARMv8.4,
+/// while iOS/tvOS device targets can still cover A7–A11 chips (ARMv8.0–8.2,
+/// no JSCVT — `fjcvtzs` would be an illegal instruction) and generic aarch64
+/// (Graviton2/Neoverse-N1) lacks it too. `PERRY_JSCVT=0/off/false` reverts
+/// `toint32_wrap` to the branchless shift/select tower (A/B bisection; keyed
+/// into the object cache). Same thread-local per-module discipline as
+/// `FULL_OUTLINE_IC` above.
+pub(crate) fn jscvt_enabled() -> bool {
+    JSCVT.with(|c| c.get())
+}
+
+pub(crate) fn set_jscvt_for_target(triple: &str) {
+    let env_off = matches!(
+        std::env::var("PERRY_JSCVT").as_deref(),
+        Ok("0") | Ok("off") | Ok("false")
+    );
+    let target_has_jscvt = (triple.starts_with("arm64") || triple.starts_with("aarch64"))
+        && (triple.contains("apple-macosx") || triple.contains("apple-darwin"));
+    JSCVT.with(|c| c.set(target_has_jscvt && !env_off));
 }
 
 /// Lever B (#5334) full-outline gate for class-field IC diamonds. Set ONCE per
diff --git a/crates/perry-codegen/src/codegen/method.rs b/crates/perry-codegen/src/codegen/method.rs
index a9fd211062..501a0ed485 100644
--- a/crates/perry-codegen/src/codegen/method.rs
+++ b/crates/perry-codegen/src/codegen/method.rs
@@ -473,6 +473,9 @@ pub(super) fn compile_method(
         integer_locals: native_facts.integer_locals(),
         not_bigint_locals: native_facts.not_bigint_locals(),
         unsigned_i32_locals: native_facts.unsigned_i32_locals(),
+        // Conservative: treat every slot as possibly-bound (param binds are
+        // emitted before FnCtx exists here), so clears never get skipped.
+        shadow_slots_bound: shadow_slot_map.values().copied().collect(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
@@ -489,6 +492,9 @@ pub(super) fn compile_method(
         local_slot_reps: HashMap::new(),
         repsel_context_allows_canonical_i32: repsel_allows,
         repsel_closure_ref_locals: repsel_closure_refs,
+        spec_abi_functions: &cross_module.spec_abi_functions,
+        spec_ta_bindings: &cross_module.spec_ta_bindings,
+        spec_ta_ready: std::collections::HashSet::new(),
         i1_local_slots: HashMap::new(),
         index_used_locals: native_facts.index_used_locals(),
         strictly_i32_bounded_locals: native_facts.strictly_i32_bounded_locals(),
@@ -1490,6 +1496,9 @@ pub(super) fn compile_static_method(
         integer_locals: native_facts.integer_locals(),
         not_bigint_locals: native_facts.not_bigint_locals(),
         unsigned_i32_locals: native_facts.unsigned_i32_locals(),
+        // Conservative: treat every slot as possibly-bound (param binds are
+        // emitted before FnCtx exists here), so clears never get skipped.
+        shadow_slots_bound: shadow_slot_map.values().copied().collect(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
@@ -1506,6 +1515,9 @@ pub(super) fn compile_static_method(
         local_slot_reps: HashMap::new(),
         repsel_context_allows_canonical_i32: repsel_allows,
         repsel_closure_ref_locals: repsel_closure_refs,
+        spec_abi_functions: &cross_module.spec_abi_functions,
+        spec_ta_bindings: &cross_module.spec_ta_bindings,
+        spec_ta_ready: std::collections::HashSet::new(),
         i1_local_slots: HashMap::new(),
         index_used_locals: native_facts.index_used_locals(),
         strictly_i32_bounded_locals: native_facts.strictly_i32_bounded_locals(),
diff --git a/crates/perry-codegen/src/codegen/mod.rs b/crates/perry-codegen/src/codegen/mod.rs
index 307e915e12..713cd747ee 100644
--- a/crates/perry-codegen/src/codegen/mod.rs
+++ b/crates/perry-codegen/src/codegen/mod.rs
@@ -55,6 +55,7 @@ mod method;
 mod method_registry;
 mod module_globals_emit;
 mod opts;
+mod spec_abi;
 mod string_pool;
 mod typed_abi;
 
@@ -68,6 +69,7 @@ pub use opts::{
     AppMetadata, CompileOptions, FpContractMode, ImportedClass, NamespaceEntry, NamespaceEntryKind,
 };
 pub(crate) use opts::{CrossModuleCtx, ImportedCtor};
+pub(crate) use spec_abi::{spec_abi_enabled, spec_function_name, SpecDispatch, SpecFnPlan};
 pub(crate) use typed_abi::{
     emit_typed_arg_guard, emit_typed_arg_to_raw, generic_closure_body_name,
     generic_function_body_name, generic_method_body_name, typed_f64_closure_name,
@@ -157,6 +159,9 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
     // afresh for every module — including the `false` case, to clear any prior
     // module's decision on this thread.
     set_full_outline_ic(decide_full_outline_ic(module_callable_count(hir)));
+    // FEAT_JSCVT decision is per-target (apple-arm64 only) — same
+    // set-per-module discipline as the outline gate above.
+    helpers::set_jscvt_for_target(&triple);
 
     let mut llmod = LlModule::new_with_fp_flags(&triple, fp_flags);
     // Null guard global: a zeroed i32 used as a safe dereference target
@@ -1090,6 +1095,45 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
             }
         }
     }
+    // Representation-selection Phase 2: top-level `const <name> = <numeric
+    // literal>` module bindings are compile-time constants by ECMAScript
+    // semantics (a `const` reassignment is a parse-time error), so their
+    // reads constant-fold — this is what proves `P[BLOWFISH_NUM_ROUNDS + 1]`
+    // in-bounds against a constant-length view. Excluded: any id carried by a
+    // `PreallocateBoxes`/`PreallocateTdzBoxes` statement — a box-backed slot
+    // holds a box pointer, and a TDZ-flagged binding must keep its
+    // ReferenceError on pre-declaration reads instead of folding to a value.
+    {
+        let mut prealloc_ids: std::collections::HashSet<u32> = std::collections::HashSet::new();
+        for s in &hir.init {
+            if let perry_hir::Stmt::PreallocateBoxes(ids)
+            | perry_hir::Stmt::PreallocateTdzBoxes(ids) = s
+            {
+                prealloc_ids.extend(ids.iter().copied());
+            }
+        }
+        for s in &hir.init {
+            if let perry_hir::Stmt::Let {
+                id,
+                mutable: false,
+                init: Some(init),
+                ..
+            } = s
+            {
+                if prealloc_ids.contains(id) {
+                    continue;
+                }
+                let value = match init {
+                    perry_hir::Expr::Integer(n) => Some(*n as f64),
+                    perry_hir::Expr::Number(n) if n.is_finite() => Some(*n),
+                    _ => None,
+                };
+                if let Some(value) = value {
+                    compile_time_constants.entry(*id).or_insert(value);
+                }
+            }
+        }
+    }
 
     // Issue #235: per-method explicit-param-count map covering BOTH local
     // classes (from `hir.classes`) AND imported classes (from
@@ -1577,6 +1621,10 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
             .filter(|f| crate::collectors::returns_i32_identity_arg(f))
             .map(|f| f.id)
             .collect(),
+        // Phase 2 spec-ABI plans are selected AFTER the i64-specialization
+        // pass (mutual exclusion), below; start empty here.
+        spec_abi_functions: std::collections::HashMap::new(),
+        spec_ta_bindings: std::collections::HashMap::new(),
         typed_f64_functions,
         typed_i32_functions,
         typed_i1_functions,
@@ -2079,6 +2127,142 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
         .typed_i1_function_param_reps
         .retain(|id, _| !i64_specialized.contains(id));
 
+    // ---- Representation-selection Phase 2: specialized-ABI plan selection.
+    // Runs AFTER the i64-specialization pass and the typed_abi clone sets so
+    // mutual exclusion is decidable; the entries themselves are emitted below
+    // in the pre-public loop. Bounded: one entry per function (the dominant
+    // tuple), `PERRY_SPECIALIZED_ABI_MAX` per module.
+    if spec_abi::spec_abi_enabled() {
+        let spec_facts = crate::collectors::collect_spec_abi_facts(hir);
+        let spec_budget = spec_abi::spec_abi_max();
+        let mut spec_emitted = 0usize;
+        for f in &hir.functions {
+            let Some(sites) = spec_facts.call_sites.get(&f.id) else {
+                continue;
+            };
+            let mut reject =
+                |reason: typed_abi::TypedCloneRejectionReason,
+                 records: &mut Vec<crate::native_value::NativeRepRecord>| {
+                    record_typed_clone_rejection(
+                        records,
+                        f.name.clone(),
+                        "spec_abi_entry_decision",
+                        reason,
+                        vec![
+                            "typed_clone_kind=spec_abi_entry".to_string(),
+                            format!("function_id={}", f.id),
+                            format!("symbol={}", f.name),
+                        ],
+                    );
+                };
+            if f.is_async || f.is_generator || f.was_plain_async {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::AsyncOrGenerator,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if !f.captures.is_empty() {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::Captures,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if f.params.iter().any(|p| p.default.is_some()) {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::ParamDefault,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if f.params.iter().any(|p| p.is_rest) {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::RestParam,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if f.params.iter().any(|p| p.arguments_object.is_some())
+                || func_synthetic_arguments.contains(&f.id)
+            {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::ArgumentsObject,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if cross_module.funcs_reading_dynamic_this.contains(&f.id) {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::SpecReadsDynamicThis,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if i64_specialized.contains(&f.id) {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::I64Specialized,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            if cross_module.typed_f64_functions.contains(&f.id)
+                || cross_module.typed_i32_functions.contains(&f.id)
+                || cross_module.typed_i1_functions.contains(&f.id)
+                || cross_module.typed_string_functions.contains(&f.id)
+            {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::SpecTypedCloneOverlap,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            // Callee-side demotion: params the raw ABI cannot accept keep the
+            // boxed protocol (reassigned params would stale the entry-bound
+            // proofs; closure-referenced params feed the capture machinery).
+            let closure_refs = crate::expr::collect_closure_referenced_locals(&f.body);
+            let reassigned = crate::collectors::reassigned_locals(&f.body);
+            let demoted: Vec<bool> = f
+                .params
+                .iter()
+                .map(|p| reassigned.contains(&p.id) || closure_refs.contains(&p.id))
+                .collect();
+            let plan = match spec_abi::select_dominant_tuple(sites, f.params.len(), &demoted) {
+                Some((reps, _matching_sites)) => SpecFnPlan {
+                    reps,
+                    dispatch: SpecDispatch::Static,
+                },
+                None => {
+                    // Tier B: declaration-derived tuple, runtime-guarded
+                    // dispatch. Only viable with ≥1 declared-Int32 param.
+                    let reps = spec_abi::declaration_tuple(&f.params, &demoted);
+                    if spec_abi::spec_tuple_is_viable(&reps) {
+                        SpecFnPlan {
+                            reps,
+                            dispatch: SpecDispatch::Guarded,
+                        }
+                    } else {
+                        reject(
+                            typed_abi::TypedCloneRejectionReason::SpecTupleUnproven,
+                            &mut typed_clone_rejection_records,
+                        );
+                        continue;
+                    }
+                }
+            };
+            if spec_emitted >= spec_budget {
+                reject(
+                    typed_abi::TypedCloneRejectionReason::SpecBudgetExceeded,
+                    &mut typed_clone_rejection_records,
+                );
+                continue;
+            }
+            spec_emitted += 1;
+            cross_module.spec_abi_functions.insert(f.id, plan);
+        }
+        cross_module.spec_ta_bindings = spec_facts.ta_bindings;
+    }
+
     // Emit internal typed-f64 clones before their public/generic wrappers. The
     // public wrapper keeps the JSValue ABI; it and direct proven numeric call
     // sites can call the internal clone.
@@ -2123,6 +2307,37 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
             .with_context(|| format!("lowering typed-string clone for function '{}'", f.name))?;
     }
 
+    // Representation-selection Phase 2: emit full-body specialized entries
+    // (`{public}__spec_...`, internal linkage) before the public bodies. Same
+    // real `compile_function`, parameterized on the plan's rep tuple.
+    for f in &hir.functions {
+        let Some(plan) = cross_module.spec_abi_functions.get(&f.id).cloned() else {
+            continue;
+        };
+        compile_function(
+            &mut llmod,
+            f,
+            &func_names,
+            &mut strings,
+            &class_table,
+            &method_names,
+            &module_globals,
+            &module_global_types,
+            &opts.import_function_prefixes,
+            &enum_table,
+            &static_field_globals,
+            &class_ids,
+            &func_signatures,
+            &func_synthetic_arguments,
+            &module_boxed_vars,
+            &closure_rest_params,
+            &cross_module,
+            None,
+            Some(&plan),
+        )
+        .with_context(|| format!("lowering specialized entry for function '{}'", f.name))?;
+    }
+
     // Lower each user function into the module (skip i64-specialized ones).
     for f in &hir.functions {
         if i64_specialized.contains(&f.id) {
@@ -2158,6 +2373,7 @@ pub fn compile_module(hir: &HirModule, opts: CompileOptions) -> Result<Vec<u8>>
             &closure_rest_params,
             &cross_module,
             typed_public_trampoline,
+            None,
         )
         .with_context(|| format!("lowering function '{}'", f.name))?;
     }
diff --git a/crates/perry-codegen/src/codegen/opts.rs b/crates/perry-codegen/src/codegen/opts.rs
index d96b784407..d3b5c81d59 100644
--- a/crates/perry-codegen/src/codegen/opts.rs
+++ b/crates/perry-codegen/src/codegen/opts.rs
@@ -737,6 +737,14 @@ pub(crate) struct CrossModuleCtx {
     pub returns_int_functions: std::collections::HashSet<u32>,
     /// Single-argument integer helpers that return the argument coerced to i32.
     pub i32_identity_functions: std::collections::HashSet<u32>,
+    /// Representation-selection Phase 2 (`codegen/spec_abi.rs`): FuncId →
+    /// specialization plan for functions with an emitted full-body specialized
+    /// entry (internal linkage, named by `spec_function_name`). Mutually
+    /// exclusive with the typed_abi clone families and `i64_specialized`.
+    pub spec_abi_functions: std::collections::HashMap<u32, super::spec_abi::SpecFnPlan>,
+    /// Phase 2 pre-pass: LocalIds proven to permanently hold one specific
+    /// non-view typed array (see `collectors/spec_abi_sites.rs`).
+    pub spec_ta_bindings: std::collections::HashMap<u32, crate::collectors::SpecTaBinding>,
     /// User functions that have a generated internal typed-f64 clone. The
     /// public wrapper keeps the JSValue ABI; direct numeric call sites may call
     /// the clone.
diff --git a/crates/perry-codegen/src/codegen/spec_abi.rs b/crates/perry-codegen/src/codegen/spec_abi.rs
new file mode 100644
index 0000000000..26767c5236
--- /dev/null
+++ b/crates/perry-codegen/src/codegen/spec_abi.rs
@@ -0,0 +1,318 @@
+//! Representation-selection Phase 2 (RFC `docs/representation-selection-rfc.md`
+//! §5.4): the specialized calling convention — bounded monomorphization.
+//!
+//! Generalizes the existing three-symbol typed_abi scheme in three directions:
+//!
+//! 1. **Full-body specialized entries.** The specialized clone is compiled by
+//!    the REAL `compile_function` parameterized on a representation tuple
+//!    (`SpecParamRep` per param) — loops, branches, calls, the unrolled
+//!    bcryptjs `_encipher` all lower through the ordinary statement lowerer.
+//!    The public boxed entry always exists and stays the permanent ABI.
+//! 2. **`TaPtr` params.** A proven typed-array param binds at entry as a
+//!    proven `BufferViewSlot` (data pointer + length hoisted ONCE from the
+//!    header — sound because typed-array storage never moves and a non-view
+//!    typed array cannot be detached or resized), so element accesses lower
+//!    through the strong bare-load machinery with bounds checks against the
+//!    entry-hoisted length — NEVER through the per-site guarded fast paths
+//!    (measured to LOSE on unrolled bodies: 834 → 2732 ms).
+//! 3. **Call-site-driven tuples + static dispatch.** The rep tuple comes from
+//!    the `collectors::spec_abi_sites` pre-pass (call sites, not declarations),
+//!    and statically-proven sites call the specialized symbol DIRECTLY — no
+//!    guard, no diamond, no phi. Declaration-only proofs keep the existing
+//!    guarded-diamond shape (`SpecDispatch::Guarded`).
+//!
+//! Specialized symbols are `internal` and reachable ONLY from same-module
+//! direct `FuncRef` call sites — closures, wrappers, exports, and every
+//! indirect path resolve to the public boxed symbol (asserted by
+//! `spec_abi_symbol_reachability` in the tests module).
+
+use std::collections::HashMap;
+
+pub(crate) use crate::collectors::SpecParamRep;
+use crate::types::{LlvmType, DOUBLE, I32, I64};
+
+/// `PERRY_SPECIALIZED_ABI` gate. Default on; `0`/`off`/`false` disables the
+/// whole phase (no specialized entries, no static dispatch). Keyed into the
+/// object cache (`object_cache.rs`) so A/B arms never share objects.
+pub(crate) fn spec_abi_enabled() -> bool {
+    use std::sync::OnceLock;
+    static CACHED: OnceLock<bool> = OnceLock::new();
+    *CACHED.get_or_init(|| {
+        !matches!(
+            std::env::var("PERRY_SPECIALIZED_ABI").as_deref(),
+            Ok("0") | Ok("off") | Ok("false")
+        )
+    })
+}
+
+/// `PERRY_SPECIALIZED_ABI_MAX`: module-wide cap on emitted specialized
+/// entries (anti-bloat budget). Default 64. Also object-cache-keyed.
+pub(crate) fn spec_abi_max() -> usize {
+    use std::sync::OnceLock;
+    static CACHED: OnceLock<usize> = OnceLock::new();
+    *CACHED.get_or_init(|| {
+        std::env::var("PERRY_SPECIALIZED_ABI_MAX")
+            .ok()
+            .and_then(|v| v.parse::<usize>().ok())
+            .unwrap_or(64)
+    })
+}
+
+/// How proven call sites reach the specialized entry.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub(crate) enum SpecDispatch {
+    /// Tier A: every non-Boxed slot proven BY CONSTRUCTION at the call site —
+    /// direct `call @{name}__spec_...` with raw args, no guard.
+    Static,
+    /// Tier B: reps proven only by declared types — the call site keeps the
+    /// runtime-guarded diamond (guard → spec entry / boxed fallback → phi).
+    Guarded,
+}
+
+/// The per-function specialization plan threaded through `CrossModuleCtx`.
+#[derive(Debug, Clone)]
+pub(crate) struct SpecFnPlan {
+    pub reps: Vec<SpecParamRep>,
+    pub dispatch: SpecDispatch,
+}
+
+impl SpecFnPlan {
+    /// Phase-2 budget: exactly ONE specialized entry per function (the
+    /// dominant tuple). Kept as an explicit constant so raising it later is a
+    /// knob, not a rewrite.
+    pub(crate) const MAX_ENTRIES_PER_FUNCTION: usize = 1;
+}
+
+/// LLVM parameter type for a rep slot.
+pub(crate) fn spec_rep_llvm_ty(rep: SpecParamRep) -> LlvmType {
+    match rep {
+        SpecParamRep::Boxed | SpecParamRep::F64 => DOUBLE,
+        SpecParamRep::I32 => I32,
+        SpecParamRep::TaPtr { .. } => I64,
+    }
+}
+
+/// Specialized-entry symbol: `{public}__spec_<label>_<label>...`. Labels are
+/// `[a-z0-9]`-only (`b`, `i32`, `f64`, `ta<kind>[x<len>]`), so the composed
+/// name is byte-stable under `sanitize`/`sanitize_member` (no `$`).
+pub(crate) fn spec_function_name(public_name: &str, reps: &[SpecParamRep]) -> String {
+    let mangle: Vec<String> = reps.iter().map(|r| r.label()).collect();
+    format!("{}__spec_{}", public_name, mangle.join("_"))
+}
+
+/// Element-kind → class name, for stamping `local_types` inside the
+/// specialized body so every type predicate sees the proof.
+pub(crate) fn spec_ta_kind_class_name(kind: u8) -> Option<&'static str> {
+    use perry_hir::*;
+    Some(match kind {
+        TYPED_ARRAY_KIND_INT8 => "Int8Array",
+        TYPED_ARRAY_KIND_UINT8 => "Uint8Array",
+        TYPED_ARRAY_KIND_UINT8_CLAMPED => "Uint8ClampedArray",
+        TYPED_ARRAY_KIND_INT16 => "Int16Array",
+        TYPED_ARRAY_KIND_UINT16 => "Uint16Array",
+        TYPED_ARRAY_KIND_INT32 => "Int32Array",
+        TYPED_ARRAY_KIND_UINT32 => "Uint32Array",
+        TYPED_ARRAY_KIND_FLOAT32 => "Float32Array",
+        TYPED_ARRAY_KIND_FLOAT64 => "Float64Array",
+        _ => return None,
+    })
+}
+
+/// Element kind → (`BufferElem`, width in bytes) for the entry-bound view
+/// slot. Mirrors `stmt/let_stmt.rs`'s private table.
+pub(crate) fn spec_ta_kind_elem_width(kind: u8) -> Option<(crate::native_value::BufferElem, u32)> {
+    use crate::native_value::BufferElem;
+    use perry_hir::*;
+    Some(match kind {
+        TYPED_ARRAY_KIND_INT8 => (BufferElem::I8, 1),
+        TYPED_ARRAY_KIND_UINT8 => (BufferElem::U8, 1),
+        TYPED_ARRAY_KIND_UINT8_CLAMPED => (BufferElem::U8Clamped, 1),
+        TYPED_ARRAY_KIND_INT16 => (BufferElem::I16, 2),
+        TYPED_ARRAY_KIND_UINT16 => (BufferElem::U16, 2),
+        TYPED_ARRAY_KIND_INT32 => (BufferElem::I32, 4),
+        TYPED_ARRAY_KIND_UINT32 => (BufferElem::U32, 4),
+        TYPED_ARRAY_KIND_FLOAT32 => (BufferElem::F32, 4),
+        TYPED_ARRAY_KIND_FLOAT64 => (BufferElem::F64, 8),
+        _ => return None,
+    })
+}
+
+/// Whether a tuple justifies emitting an entry at all: at least one slot whose
+/// specialized form actually removes work (`I32` canonical binding or `TaPtr`
+/// proven view). An all-`Boxed`/`F64` tuple is byte-identical to the public
+/// entry — pure bloat.
+pub(crate) fn spec_tuple_is_viable(reps: &[SpecParamRep]) -> bool {
+    reps.iter()
+        .any(|r| matches!(r, SpecParamRep::I32 | SpecParamRep::TaPtr { .. }))
+}
+
+/// Select the dominant viable tuple for `fid` from the pre-pass judgments,
+/// after demoting slots the CALLEE cannot accept in raw form (reassigned or
+/// closure-referenced params must keep the boxed protocol). Returns the tuple
+/// and how many sites match it exactly.
+pub(crate) fn select_dominant_tuple(
+    sites: &[Vec<SpecParamRep>],
+    param_count: usize,
+    demoted_params: &[bool],
+) -> Option<(Vec<SpecParamRep>, usize)> {
+    let mut counts: HashMap<Vec<SpecParamRep>, usize> = HashMap::new();
+    let mut order: Vec<Vec<SpecParamRep>> = Vec::new();
+    for site in sites {
+        if site.len() != param_count {
+            continue;
+        }
+        let tuple: Vec<SpecParamRep> = site
+            .iter()
+            .zip(demoted_params.iter())
+            .map(|(rep, demoted)| if *demoted { SpecParamRep::Boxed } else { *rep })
+            .collect();
+        if !spec_tuple_is_viable(&tuple) {
+            continue;
+        }
+        let entry = counts.entry(tuple.clone()).or_insert(0);
+        if *entry == 0 {
+            order.push(tuple);
+        }
+        *entry += 1;
+    }
+    // Dominant = most frequent; ties break by FIRST appearance in the
+    // deterministic walk order, keeping the object-cache input stable
+    // (`max_by_key` would return the LAST maximal element, so the strictly-
+    // greater comparison below is what pins the first appearance).
+    let mut best: Option<(Vec<SpecParamRep>, usize)> = None;
+    for tuple in order {
+        let n = counts.get(&tuple).copied().unwrap_or(0);
+        if best.as_ref().is_none_or(|(_, best_n)| n > *best_n) {
+            best = Some((tuple, n));
+        }
+    }
+    best
+}
+
+/// Declaration-derived tuple for the guarded (Tier B) dispatch: `Int32`-typed
+/// params become raw `I32`, everything else stays `Boxed`. `F64`-only tuples
+/// are non-viable by construction (`spec_tuple_is_viable`), so this only
+/// fires for functions with at least one declared-`Int32` param.
+pub(crate) fn declaration_tuple(
+    params: &[perry_hir::Param],
+    demoted_params: &[bool],
+) -> Vec<SpecParamRep> {
+    params
+        .iter()
+        .zip(demoted_params.iter())
+        .map(|(p, demoted)| {
+            if *demoted {
+                return SpecParamRep::Boxed;
+            }
+            match &p.ty {
+                perry_hir::types::Type::Int32 => SpecParamRep::I32,
+                _ => SpecParamRep::Boxed,
+            }
+        })
+        .collect()
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn mangle_is_sanitize_stable() {
+        let reps = [
+            SpecParamRep::TaPtr {
+                kind: 4,
+                const_len: Some(2),
+            },
+            SpecParamRep::I32,
+            SpecParamRep::TaPtr {
+                kind: 4,
+                const_len: None,
+            },
+            SpecParamRep::Boxed,
+            SpecParamRep::F64,
+        ];
+        let name = spec_function_name("perry_fn_m___encipher", &reps);
+        assert_eq!(name, "perry_fn_m___encipher__spec_ta4x2_i32_ta4_b_f64");
+        // Every char is symbol-safe: sanitize/sanitize_member must return the
+        // name byte-identical (no `$`, no unicode).
+        assert!(name.chars().all(|c| c.is_ascii_alphanumeric() || c == '_'));
+    }
+
+    #[test]
+    fn dominant_tuple_selection_demotes_and_counts() {
+        let ta = SpecParamRep::TaPtr {
+            kind: 4,
+            const_len: Some(8),
+        };
+        let sites = vec![
+            vec![ta, SpecParamRep::I32],
+            vec![ta, SpecParamRep::I32],
+            vec![SpecParamRep::Boxed, SpecParamRep::I32],
+        ];
+        let (tuple, n) = select_dominant_tuple(&sites, 2, &[false, false]).unwrap();
+        assert_eq!(tuple, vec![ta, SpecParamRep::I32]);
+        assert_eq!(n, 2);
+
+        // Demoting param 0 collapses all sites to (Boxed, I32) — still viable
+        // through the I32 slot.
+        let (tuple, n) = select_dominant_tuple(&sites, 2, &[true, false]).unwrap();
+        assert_eq!(tuple, vec![SpecParamRep::Boxed, SpecParamRep::I32]);
+        assert_eq!(n, 3);
+
+        // Arity-mismatched sites never count.
+        assert!(select_dominant_tuple(&sites, 3, &[false, false, false]).is_none());
+    }
+
+    /// The reachability ratchet: specialized symbols must NEVER be constructed
+    /// outside the allowlisted modules (naming + emission + direct-call
+    /// dispatch). A `__spec_` string appearing in a closure/wrapper emission
+    /// path would mean an indirect route to a raw-ABI entry — unsound by
+    /// construction. Scans this crate's sources at test time.
+    #[test]
+    fn spec_abi_symbol_reachability() {
+        let src_root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("src");
+        let allowed: [&str; 4] = [
+            "codegen/spec_abi.rs",    // naming + this test
+            "codegen/function.rs",    // entry emission
+            "codegen/mod.rs",         // eligibility/budget loop
+            "lower_call/func_ref.rs", // direct-call dispatch
+        ];
+        let mut offenders: Vec<String> = Vec::new();
+        fn visit(
+            dir: &std::path::Path,
+            root: &std::path::Path,
+            allowed: &[&str],
+            out: &mut Vec<String>,
+        ) {
+            for entry in std::fs::read_dir(dir).expect("read src dir") {
+                let path = entry.expect("dir entry").path();
+                if path.is_dir() {
+                    visit(&path, root, allowed, out);
+                    continue;
+                }
+                if path.extension().and_then(|e| e.to_str()) != Some("rs") {
+                    continue;
+                }
+                let rel = path
+                    .strip_prefix(root)
+                    .unwrap()
+                    .to_string_lossy()
+                    .replace('\\', "/");
+                if allowed.contains(&rel.as_str()) {
+                    continue;
+                }
+                let text = std::fs::read_to_string(&path).expect("read source file");
+                if text.contains("__spec_") {
+                    out.push(rel);
+                }
+            }
+        }
+        visit(&src_root, &src_root, &allowed, &mut offenders);
+        assert!(
+            offenders.is_empty(),
+            "specialized-ABI symbol fragments found outside the allowlist \
+             (closure/wrapper paths must only ever call the public boxed \
+             symbol): {offenders:?}"
+        );
+    }
+}
diff --git a/crates/perry-codegen/src/codegen/typed_abi.rs b/crates/perry-codegen/src/codegen/typed_abi.rs
index 7e51497f6c..944caa35a3 100644
--- a/crates/perry-codegen/src/codegen/typed_abi.rs
+++ b/crates/perry-codegen/src/codegen/typed_abi.rs
@@ -232,6 +232,17 @@ pub(crate) enum TypedCloneRejectionReason {
     ReceiverFieldNotOwn,
     ReceiverFieldNotF64,
     ThisEscape,
+    /// Spec-ABI (Phase 2): no call site proved a viable representation tuple.
+    SpecTupleUnproven,
+    /// Spec-ABI: the function already carries a typed_abi clone family —
+    /// mutually exclusive with a specialized entry in this phase.
+    SpecTypedCloneOverlap,
+    /// Spec-ABI: the module-wide `PERRY_SPECIALIZED_ABI_MAX` budget was
+    /// exhausted before this function's turn.
+    SpecBudgetExceeded,
+    /// Spec-ABI: the callee reads dynamic `this`, so direct call sites must
+    /// juggle the implicit-this slot and never take the raw-ABI route.
+    SpecReadsDynamicThis,
 }
 
 impl TypedCloneRejectionReason {
@@ -268,6 +279,10 @@ impl TypedCloneRejectionReason {
             Self::ReceiverFieldNotOwn => "receiver_field_not_own",
             Self::ReceiverFieldNotF64 => "receiver_field_not_f64",
             Self::ThisEscape => "this_escape",
+            Self::SpecTupleUnproven => "spec_tuple_unproven",
+            Self::SpecTypedCloneOverlap => "spec_typed_clone_overlap",
+            Self::SpecBudgetExceeded => "spec_budget_exceeded",
+            Self::SpecReadsDynamicThis => "spec_reads_dynamic_this",
         }
     }
 }
diff --git a/crates/perry-codegen/src/collectors/clamp_detect.rs b/crates/perry-codegen/src/collectors/clamp_detect.rs
index 1bfce7c446..560bbe1be7 100644
--- a/crates/perry-codegen/src/collectors/clamp_detect.rs
+++ b/crates/perry-codegen/src/collectors/clamp_detect.rs
@@ -1,7 +1,13 @@
+//! Clamp-pattern / integer-return detectors. All gates exclude
+//! `was_plain_async` alongside `is_async`/`is_generator`: the
+//! async-to-generator pre-pass rewrites a plain-async body into a state
+//! machine whose returns no longer mean what the pattern matchers assume
+//! (Phase 2 audit — the flag was previously missed here).
+
 use perry_hir::{BinaryOp, Expr, Function, Stmt};
 
 pub fn detect_clamp3(f: &Function) -> Option<(u32, u32, u32)> {
-    if f.is_async || f.is_generator || f.params.len() != 3 {
+    if f.is_async || f.is_generator || f.was_plain_async || f.params.len() != 3 {
         return None;
     }
     if !matches!(f.return_type, perry_hir::types::Type::Number) {
@@ -81,7 +87,7 @@ pub fn detect_clamp3(f: &Function) -> Option<(u32, u32, u32)> {
 /// argument-INdependent admission in `collect_integer_locals`) would put a
 /// truncating i32 shadow slot on a non-integer value.
 pub fn detect_clamp_u8(f: &Function) -> bool {
-    if f.is_async || f.is_generator || f.params.len() != 1 {
+    if f.is_async || f.is_generator || f.was_plain_async || f.params.len() != 1 {
         return false;
     }
     if f.body.len() != 3 {
@@ -146,7 +152,7 @@ pub fn detect_clamp_u8(f: &Function) -> bool {
 
 /// A function is i64-specializable if it's a pure numeric recursive fn.
 pub fn is_integer_specializable(f: &Function) -> bool {
-    if f.is_async || f.is_generator {
+    if f.is_async || f.is_generator || f.was_plain_async {
         return false;
     }
     if !matches!(f.return_type, perry_hir::types::Type::Number) {
@@ -166,7 +172,7 @@ pub fn is_integer_specializable(f: &Function) -> bool {
 /// treated as int-producing at call sites, enabling the i32 fast path for
 /// `h = userImul(h, p)` style patterns.
 pub fn returns_integer(f: &Function) -> bool {
-    if f.is_async || f.is_generator {
+    if f.is_async || f.is_generator || f.was_plain_async {
         return false;
     }
     if !matches!(f.return_type, perry_hir::types::Type::Number) {
@@ -176,7 +182,7 @@ pub fn returns_integer(f: &Function) -> bool {
 }
 
 pub fn returns_i32_identity_arg(f: &Function) -> bool {
-    if f.is_async || f.is_generator || f.params.len() != 1 {
+    if f.is_async || f.is_generator || f.was_plain_async || f.params.len() != 1 {
         return false;
     }
     if !matches!(f.return_type, perry_hir::types::Type::Number) {
diff --git a/crates/perry-codegen/src/collectors/hir_facts.rs b/crates/perry-codegen/src/collectors/hir_facts.rs
index 9cd9a59f3c..9755fd9900 100644
--- a/crates/perry-codegen/src/collectors/hir_facts.rs
+++ b/crates/perry-codegen/src/collectors/hir_facts.rs
@@ -328,6 +328,7 @@ pub(crate) fn collect_type_facts(
     classes: &HashMap<String, &perry_hir::Class>,
     compile_time_constants: &HashMap<u32, f64>,
     module_dispatch: &super::ModuleDispatchFacts,
+    spec_ta_lens: &HashMap<u32, i64>,
 ) -> TypeFacts {
     let mut integer_locals = super::integer_locals::collect_integer_locals(
         stmts,
@@ -344,8 +345,12 @@ pub(crate) fn collect_type_facts(
     // only pollute the fact for other consumers).
     let mut int_valued_ta_locals: HashSet<u32> = HashSet::new();
     if super::int_valued_ta_locals::enabled() {
-        let extra =
-            super::int_valued_ta_locals::collect_int_valued_ta_locals(stmts, params, binding_types);
+        let extra = super::int_valued_ta_locals::collect_int_valued_ta_locals(
+            stmts,
+            params,
+            binding_types,
+            spec_ta_lens,
+        );
         for id in extra {
             if !boxed_vars.contains(&id) && !module_globals.contains_key(&id) {
                 integer_locals.insert(id);
@@ -480,6 +485,41 @@ pub(crate) fn collect_native_region_fact_graph(
     classes: &HashMap<String, &perry_hir::Class>,
     compile_time_constants: &HashMap<u32, f64>,
     module_dispatch: &super::ModuleDispatchFacts,
+) -> NativeRegionFactGraph {
+    collect_native_region_fact_graph_with_spec_lens(
+        stmts,
+        params,
+        flat_const_ids,
+        clamp_fn_ids,
+        arg_dependent_clamp_fn_ids,
+        boxed_vars,
+        module_globals,
+        binding_types,
+        classes,
+        compile_time_constants,
+        module_dispatch,
+        &HashMap::new(),
+    )
+}
+
+/// Variant carrying spec-ABI `TaPtr` parameter lengths (representation-
+/// selection Phase 2): the call-site pre-pass proved these params hold
+/// non-view typed arrays with these constant element counts, which unlocks
+/// the wrap-i32 additive admission's in-bounds operand proof.
+#[allow(clippy::too_many_arguments)]
+pub(crate) fn collect_native_region_fact_graph_with_spec_lens(
+    stmts: &[Stmt],
+    params: &[perry_hir::Param],
+    flat_const_ids: &HashSet<u32>,
+    clamp_fn_ids: &HashSet<u32>,
+    arg_dependent_clamp_fn_ids: &HashSet<u32>,
+    boxed_vars: &HashSet<u32>,
+    module_globals: &HashMap<u32, String>,
+    binding_types: &HashMap<u32, perry_hir::types::Type>,
+    classes: &HashMap<String, &perry_hir::Class>,
+    compile_time_constants: &HashMap<u32, f64>,
+    module_dispatch: &super::ModuleDispatchFacts,
+    spec_ta_lens: &HashMap<u32, i64>,
 ) -> NativeRegionFactGraph {
     collect_type_facts(
         stmts,
@@ -493,6 +533,7 @@ pub(crate) fn collect_native_region_fact_graph(
         classes,
         compile_time_constants,
         module_dispatch,
+        spec_ta_lens,
     )
 }
 
@@ -518,6 +559,7 @@ pub(crate) fn collect_hir_facts(
         // No class table here, so no scalar-method summary can apply; the
         // conservative default keeps it that way if one ever could.
         &super::ModuleDispatchFacts::default(),
+        &HashMap::new(),
     )
 }
 
diff --git a/crates/perry-codegen/src/collectors/int_valued_ta_locals.rs b/crates/perry-codegen/src/collectors/int_valued_ta_locals.rs
index e786b66dad..9f6dce0c25 100644
--- a/crates/perry-codegen/src/collectors/int_valued_ta_locals.rs
+++ b/crates/perry-codegen/src/collectors/int_valued_ta_locals.rs
@@ -37,10 +37,17 @@
 //! 1. **Every write** produces an i32-representable value OR is an int-kind
 //!    typed-array element read (`Int8/Uint8/Uint8Clamped/Int16/Uint16/Int32` —
 //!    NOT `Uint32`, NOT the float / bigint kinds, NOT a plain-array `[]`):
-//!    a bitwise op (`& | ^ << >> >>>`), `~`, `Math.imul`, an i32 literal, or a
-//!    `Uint8ArrayGet`/`BufferIndexGet`. NOT additive `+`/`-`/`*` (can overflow
-//!    i32 — this is why `n` in `_encipher` stays f64), NOT a copy/call/anything
-//!    else.
+//!    a bitwise op (`& | ^ << >> >>>`), `~`, `Math.imul`, an i32 literal,
+//!    `undefined` (the hoisted-`var` seed — `ToInt32(undefined) == 0`, the
+//!    slot's seed value), or a `Uint8ArrayGet`/`BufferIndexGet`. NOT `*`
+//!    (a single product can exceed 2^53 and round). Additive `+`/`-` is
+//!    admitted ONLY under the wrap-i32 extension (`additive_write_admissible`,
+//!    representation-selection Phase 2): a STRAIGHT-LINE (never in-loop)
+//!    Add/Sub tree over exact-i32 operands (in-bounds-PROVEN int-TA reads,
+//!    literals, bitwise results, other candidates), where the slot carries the
+//!    ToInt32 image of the true value — sound because rule (2) makes the image
+//!    the only thing ever observed, and bounded straight-line chains keep the
+//!    true f64 intermediates exactly representable.
 //! 2. **Every observation** is in an integer-coercing context — the direct
 //!    operand of a bitwise binary/unary op, or the value stored into an
 //!    int-kind typed-array / `Uint8Array` / `Buffer` element. NEVER a context
@@ -62,9 +69,10 @@
 //! beats an unsound 1.42×). It requires the local to be `let`-declared (params
 //! excluded — their incoming argument is an unmodeled write), rejects `++`/`--`
 //! targets, rejects any local referenced inside a closure body, and does NOT
-//! chase copy chains (`m = l`). Anything unproven is simply left as f64. No
-//! fixpoint is required: rule (1) is judged per write structurally (no reliance
-//! on other candidates) and rule (2) is a single context-aware walk.
+//! chase copy chains (`m = l`). Anything unproven is simply left as f64.
+//! Rule (1)'s strict arm is judged per write structurally; the wrap-i32
+//! additive arm references other candidates, so admission and the rule-(2)
+//! walk run to a (small, monotone-shrinking) fixpoint.
 //!
 //! Gated by `PERRY_INT_VALUED_LOCALS` (default on; `=0`/`off`/`false` disables
 //! for A/B bisection — keyed into the object cache in `object_cache.rs`).
@@ -135,6 +143,12 @@ fn is_bitwise_binop(op: BinaryOp) -> bool {
 fn write_is_i32_producing_safe(e: &Expr, types: &HashMap<u32, HirType>) -> bool {
     match e {
         Expr::Integer(n) => super::i32_locals::integer_literal_fits_i32(*n),
+        // Hoisted-`var` seed (`var n, l = lr[off]` lowers as `Let{l,
+        // Undefined}` + `Let{l, lr[off]}`): `ToInt32(undefined) == 0`, which
+        // is exactly the value the i32 slot is seeded with, and rule (2)
+        // already guarantees every observation is ToInt32-coercing — so an
+        // `undefined` write is indistinguishable from the 0 it becomes.
+        Expr::Undefined => true,
         // Byte reads: `0` OOB, always integer.
         Expr::Uint8ArrayGet { .. } | Expr::BufferIndexGet { .. } => true,
         // Int-kind typed-array element read (possibly OOB → `undefined`).
@@ -154,8 +168,10 @@ fn write_is_i32_producing_safe(e: &Expr, types: &HashMap<u32, HirType>) -> bool
 /// One-pass structural facts gathered before eligibility is decided.
 #[derive(Default)]
 struct Facts<'a> {
-    /// Every write (Let init + `LocalSet` rhs) per local.
-    writes: HashMap<u32, Vec<&'a Expr>>,
+    /// Every write (Let init + `LocalSet` rhs) per local, with a flag for
+    /// "this write sits inside a loop" (additive writes must be straight-line
+    /// — see the wrap-i32 extension below).
+    writes: HashMap<u32, Vec<(&'a Expr, bool)>>,
     /// Locals introduced by a `Stmt::Let` (candidates must be `let`-declared —
     /// params carry an unmodeled incoming-argument write).
     let_declared: HashSet<u32>,
@@ -171,10 +187,327 @@ struct Facts<'a> {
     closure_refs: HashSet<u32>,
 }
 
+/// Wrap-i32 extension (representation-selection Phase 2): a write that is an
+/// `Add`/`Sub` tree over EXACT-i32 operands. `ToInt32(a + b) ==
+/// wrap32(ToInt32(a) + ToInt32(b))` whenever the true f64 intermediates stay
+/// exactly representable, so a local whose every observation is
+/// ToInt32-coercing may carry the WRAPPED image of an additive chain — the
+/// bcryptjs `n += S[...]` Feistel accumulator. Soundness needs three extra
+/// legs, all enforced by the caller:
+/// - operands must be undefined-free EXACT int32 values — an in-bounds-PROVEN
+///   int-TA read (static window < known constant length), an i32 literal, a
+///   bitwise/`~`/`Math.imul` result, a byte read, or another wrap-i32/strict
+///   candidate (whose slot holds the ToInt32 image by induction);
+/// - the additive write must be STRAIGHT-LINE (not inside any loop): a
+///   loop-carried additive chain grows the true float unboundedly until f64
+///   addition rounds (≥ 2^53) and the wrapped image diverges. Straight-line
+///   chains are bounded by the body's statement count (≪ 2^20 additions), so
+///   every true intermediate stays < 2^52 — exact;
+/// - candidate reads at additive-operand positions are blessed by the
+///   observation walk (`observe_additive_rhs`), everything else keeps the
+///   strict coercing rule (in particular an INDEX position is still
+///   disqualifying — a wrapped image used as an index could alias a
+///   different element than the true out-of-range value).
+fn additive_write_admissible(
+    e: &Expr,
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    pool: &HashSet<u32>,
+) -> bool {
+    match e {
+        Expr::Integer(n) => super::i32_locals::integer_literal_fits_i32(*n),
+        Expr::LocalGet(id) => pool.contains(id),
+        Expr::Uint8ArrayGet { .. } | Expr::BufferIndexGet { .. } => true,
+        // In-bounds-proven int-kind typed-array read: never `undefined`.
+        Expr::IndexGet { object, index } => {
+            receiver_is_int_kind_ta(object, types)
+                && matches!(object.as_ref(), Expr::LocalGet(arr)
+                if matches!(
+                    (ta_lens.get(arr), super::integer_locals::static_index_window(index)),
+                    (Some(len), Some((lo, hi))) if lo >= 0 && hi < *len
+                ))
+        }
+        // Exact ToInt32/ToUint32 producers regardless of operand shape.
+        Expr::Binary { op, .. } if is_bitwise_binop(*op) => true,
+        Expr::Unary {
+            op: UnaryOp::BitNot,
+            ..
+        } => true,
+        Expr::MathImul(_, _) => true,
+        Expr::Binary { op, left, right } if matches!(op, BinaryOp::Add | BinaryOp::Sub) => {
+            additive_write_admissible(left, types, ta_lens, pool)
+                && additive_write_admissible(right, types, ta_lens, pool)
+        }
+        _ => false,
+    }
+}
+
+// ---------------------------------------------------------------------------
+// Wrap-i32 flow leg: additive operands must be provably NUMBER-valued at the
+// write site. Pool membership alone is NOT enough — a pool member seeded by a
+// possibly-OOB int-TA read keeps the invariant `image == ToInt32(true)` (true
+// `undefined` → image 0), but that invariant does not survive an ADDITIVE
+// step: JS computes `undefined + 1 == NaN` (→ every later ToInt32 is 0) while
+// the image path computes `wrap(0 + 1) == 1`. So an additive `LocalGet`
+// operand is only admissible when, at that program point, every path since
+// the local's last write established a genuine Number (never `undefined`).
+// ---------------------------------------------------------------------------
+
+/// Does this RHS provably leave a NUMBER (never `undefined`) in the target?
+/// `numberish` is the flow set at the write site (for `LocalGet` copies and
+/// additive sub-trees).
+fn write_establishes_number(
+    e: &Expr,
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    numberish: &HashSet<u32>,
+) -> bool {
+    match e {
+        Expr::Integer(_) | Expr::Number(_) => true,
+        // Byte reads return `0` OOB — always a number.
+        Expr::Uint8ArrayGet { .. } | Expr::BufferIndexGet { .. } => true,
+        // Bitwise / `~` / `Math.imul` are number-or-throw (a throw means the
+        // write never completes).
+        Expr::Binary { op, .. } if is_bitwise_binop(*op) => true,
+        Expr::Unary {
+            op: UnaryOp::BitNot,
+            ..
+        } => true,
+        Expr::MathImul(_, _) => true,
+        // In-bounds-PROVEN int-kind typed-array read: never `undefined`.
+        Expr::IndexGet { object, index } => {
+            receiver_is_int_kind_ta(object, types)
+                && matches!(object.as_ref(), Expr::LocalGet(arr)
+                if matches!(
+                    (ta_lens.get(arr), super::integer_locals::static_index_window(index)),
+                    (Some(len), Some((lo, hi))) if lo >= 0 && hi < *len
+                ))
+        }
+        Expr::LocalGet(id) => numberish.contains(id),
+        Expr::Binary { op, left, right } if matches!(op, BinaryOp::Add | BinaryOp::Sub) => {
+            write_establishes_number(left, types, ta_lens, numberish)
+                && write_establishes_number(right, types, ta_lens, numberish)
+        }
+        _ => false,
+    }
+}
+
+/// `LocalGet` leaves on the Add/Sub SPINE of an additive write (the positions
+/// whose true value feeds a float add). Leaves inside bitwise sub-trees or
+/// index expressions are NOT spine leaves — a bitwise sub-result is a number
+/// regardless of what it coerced.
+fn additive_spine_locals_numberish(e: &Expr, numberish: &HashSet<u32>) -> bool {
+    match e {
+        Expr::LocalGet(id) => numberish.contains(id),
+        Expr::Binary { op, left, right } if matches!(op, BinaryOp::Add | BinaryOp::Sub) => {
+            additive_spine_locals_numberish(left, numberish)
+                && additive_spine_locals_numberish(right, numberish)
+        }
+        // Every other admissible leaf (in-bounds read, literal, bitwise,
+        // imul, byte read) is a number by construction.
+        _ => true,
+    }
+}
+
+/// One flow walk over the whole body: maintains the `numberish` set and flags
+/// every target of an additive-SHAPED write whose spine `LocalGet` operands
+/// were not all provably numbers at that point. Control-flow meets are plain
+/// intersections (claiming *less* numberish is always sound); a statement
+/// carrying multiple writes to one target only keeps it numberish when every
+/// such write establishes a number (robust to sub-expression evaluation
+/// order).
+fn additive_flow_invalid_targets(
+    stmts: &[Stmt],
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+) -> HashSet<u32> {
+    let mut invalid = HashSet::new();
+    let mut numberish = HashSet::new();
+    additive_flow_stmts(stmts, types, ta_lens, &mut numberish, &mut invalid);
+    invalid
+}
+
+fn additive_flow_stmts(
+    stmts: &[Stmt],
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    numberish: &mut HashSet<u32>,
+    invalid: &mut HashSet<u32>,
+) {
+    for s in stmts {
+        additive_flow_stmt(s, types, ta_lens, numberish, invalid);
+    }
+}
+
+fn additive_flow_stmt(
+    s: &Stmt,
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    numberish: &mut HashSet<u32>,
+    invalid: &mut HashSet<u32>,
+) {
+    match s {
+        Stmt::Let { id, init, .. } => match init {
+            Some(e) => additive_flow_expr_write(*id, e, types, ta_lens, numberish, invalid),
+            // `let x;` — undefined.
+            None => {
+                numberish.remove(id);
+            }
+        },
+        Stmt::Expr(e) | Stmt::Throw(e) => additive_flow_expr(e, types, ta_lens, numberish, invalid),
+        Stmt::Return(Some(e)) => additive_flow_expr(e, types, ta_lens, numberish, invalid),
+        Stmt::If {
+            condition,
+            then_branch,
+            else_branch,
+        } => {
+            additive_flow_expr(condition, types, ta_lens, numberish, invalid);
+            let mut then_set = numberish.clone();
+            additive_flow_stmts(then_branch, types, ta_lens, &mut then_set, invalid);
+            let mut else_set = numberish.clone();
+            if let Some(eb) = else_branch {
+                additive_flow_stmts(eb, types, ta_lens, &mut else_set, invalid);
+            }
+            *numberish = then_set.intersection(&else_set).copied().collect();
+        }
+        Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => {
+            // Zero-or-more (resp. one-or-more) executions: meet the pre-state
+            // with the post-body state. Walking the body with the PRE-state is
+            // conservative for later iterations too, since the walk can only
+            // remove entries the body would remove on any iteration.
+            let mut body_set = numberish.clone();
+            additive_flow_expr(condition, types, ta_lens, &mut body_set, invalid);
+            additive_flow_stmts(body, types, ta_lens, &mut body_set, invalid);
+            numberish.retain(|id| body_set.contains(id));
+        }
+        Stmt::For {
+            init,
+            condition,
+            update,
+            body,
+        } => {
+            if let Some(i) = init {
+                additive_flow_stmt(i, types, ta_lens, numberish, invalid);
+            }
+            let mut body_set = numberish.clone();
+            if let Some(c) = condition {
+                additive_flow_expr(c, types, ta_lens, &mut body_set, invalid);
+            }
+            if let Some(u) = update {
+                additive_flow_expr(u, types, ta_lens, &mut body_set, invalid);
+            }
+            additive_flow_stmts(body, types, ta_lens, &mut body_set, invalid);
+            numberish.retain(|id| body_set.contains(id));
+        }
+        Stmt::Labeled { body, .. } => additive_flow_stmt(body, types, ta_lens, numberish, invalid),
+        Stmt::Try {
+            body,
+            catch,
+            finally,
+        } => {
+            // The try body may partially execute; the catch entry state is
+            // unknown. Meet everything.
+            let mut body_set = numberish.clone();
+            additive_flow_stmts(body, types, ta_lens, &mut body_set, invalid);
+            numberish.retain(|id| body_set.contains(id));
+            if let Some(c) = catch {
+                let mut catch_set = numberish.clone();
+                additive_flow_stmts(&c.body, types, ta_lens, &mut catch_set, invalid);
+                numberish.retain(|id| catch_set.contains(id));
+            }
+            if let Some(f) = finally {
+                let mut fin_set = numberish.clone();
+                additive_flow_stmts(f, types, ta_lens, &mut fin_set, invalid);
+                numberish.retain(|id| fin_set.contains(id));
+            }
+        }
+        Stmt::Switch {
+            discriminant,
+            cases,
+        } => {
+            additive_flow_expr(discriminant, types, ta_lens, numberish, invalid);
+            let pre = numberish.clone();
+            for case in cases {
+                if let Some(t) = &case.test {
+                    additive_flow_expr(t, types, ta_lens, numberish, invalid);
+                }
+                let mut case_set = pre.clone();
+                additive_flow_stmts(&case.body, types, ta_lens, &mut case_set, invalid);
+                numberish.retain(|id| case_set.contains(id));
+            }
+        }
+        Stmt::Break
+        | Stmt::Continue
+        | Stmt::LabeledBreak(_)
+        | Stmt::LabeledContinue(_)
+        | Stmt::Return(None)
+        | Stmt::PreallocateBoxes(_)
+        | Stmt::PreallocateTdzBoxes(_) => {}
+    }
+}
+
+/// Process one WRITE (Let init or LocalSet rhs): validate an additive-shaped
+/// RHS's spine operands against the current `numberish` set, then update the
+/// target's numberish status from the RHS.
+fn additive_flow_expr_write(
+    target: u32,
+    rhs: &Expr,
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    numberish: &mut HashSet<u32>,
+    invalid: &mut HashSet<u32>,
+) {
+    // Walk nested writes inside the RHS first (their effects precede the
+    // outer store; any imprecision here only removes numberish entries).
+    additive_flow_expr(rhs, types, ta_lens, numberish, invalid);
+    if matches!(rhs, Expr::Binary { op, .. } if matches!(op, BinaryOp::Add | BinaryOp::Sub))
+        && !additive_spine_locals_numberish(rhs, numberish)
+    {
+        invalid.insert(target);
+    }
+    if write_establishes_number(rhs, types, ta_lens, numberish) {
+        numberish.insert(target);
+    } else {
+        numberish.remove(&target);
+    }
+}
+
+fn additive_flow_expr(
+    e: &Expr,
+    types: &HashMap<u32, HirType>,
+    ta_lens: &HashMap<u32, i64>,
+    numberish: &mut HashSet<u32>,
+    invalid: &mut HashSet<u32>,
+) {
+    match e {
+        Expr::LocalSet(id, rhs) => {
+            additive_flow_expr_write(*id, rhs, types, ta_lens, numberish, invalid);
+        }
+        // `x++` may produce a BigInt (ToNumeric preserves kind) — drop.
+        Expr::Update { id, .. } => {
+            numberish.remove(id);
+        }
+        // A closure body can run at any time and write anything — drop every
+        // local it references (candidates referencing closures are excluded
+        // anyway; this keeps NON-candidate operand bookkeeping honest).
+        Expr::Closure { .. } => {
+            let mut refs = HashSet::new();
+            collect_closure_refs(e, &mut refs);
+            numberish.retain(|id| !refs.contains(id));
+        }
+        _ => {
+            perry_hir::walker::walk_expr_children(e, &mut |c| {
+                additive_flow_expr(c, types, ta_lens, numberish, invalid)
+            });
+        }
+    }
+}
+
 pub fn collect_int_valued_ta_locals(
     stmts: &[Stmt],
     params: &[Param],
     binding_types: &HashMap<u32, HirType>,
+    extra_ta_lens: &HashMap<u32, i64>,
 ) -> HashSet<u32> {
     // Declared-type map (params + let bindings), used to classify typed-array
     // receivers. Params are included so `lr: Int32Array` resolves.
@@ -182,57 +515,128 @@ pub fn collect_int_valued_ta_locals(
     for p in params {
         types.entry(p.id).or_insert_with(|| p.ty.clone());
     }
+    // Constant typed-array lengths for the wrap-i32 in-bounds proof: in-body
+    // literal-length const views plus caller-supplied lengths (spec-ABI
+    // `TaPtr` params carry theirs from the call-site pre-pass).
+    let mut ta_lens = super::integer_locals::collect_const_int_ta_views(stmts);
+    for (id, len) in extra_ta_lens {
+        ta_lens.entry(*id).or_insert(*len);
+    }
 
     let mut facts = Facts::default();
-    collect_facts(stmts, &types, &mut facts);
+    collect_facts(stmts, &types, false, &mut facts);
+    // Flow leg of the wrap-i32 additive extension: targets of additive-shaped
+    // writes whose spine operands were not provably NUMBERS at the write site
+    // (an `undefined`-able operand breaks `image == ToInt32(true)` through a
+    // float add — `undefined + 1` is NaN→0, the image path would say 1).
+    let additive_invalid = additive_flow_invalid_targets(stmts, &types, &ta_lens);
 
     // Rule (1) admission. A candidate is a `let`-declared local with ≥1
-    // int-TA-read write, whose EVERY write is i32-producing-safe, that is not a
-    // `++`/`--` target and not referenced in a closure.
-    let mut candidates: HashSet<u32> = HashSet::new();
-    for (&id, ws) in &facts.writes {
-        if !facts.let_declared.contains(&id)
-            || !facts.seeded.contains(&id)
-            || facts.update_targets.contains(&id)
-            || facts.closure_refs.contains(&id)
-        {
-            continue;
-        }
-        if ws.iter().all(|w| write_is_i32_producing_safe(w, &types)) {
-            candidates.insert(id);
+    // int-TA-read write, whose EVERY write is i32-producing-safe (or, in the
+    // wrap-i32 extension, a straight-line additive tree over exact operands),
+    // that is not a `++`/`--` target and not referenced in a closure.
+    // Additive operands may reference OTHER candidates, so admission runs to a
+    // fixpoint from an optimistic pool.
+    let base_ok = |id: u32, facts: &Facts<'_>| {
+        facts.let_declared.contains(&id)
+            && facts.seeded.contains(&id)
+            && !facts.update_targets.contains(&id)
+            && !facts.closure_refs.contains(&id)
+    };
+    let mut pool: HashSet<u32> = facts
+        .writes
+        .keys()
+        .copied()
+        .filter(|id| base_ok(*id, &facts))
+        .collect();
+    loop {
+        let before = pool.len();
+        let snapshot = pool.clone();
+        pool.retain(|id| {
+            facts.writes[id].iter().all(|(w, in_loop)| {
+                write_is_i32_producing_safe(w, &types)
+                    || (!in_loop
+                        && !additive_invalid.contains(id)
+                        && additive_write_admissible(w, &types, &ta_lens, &snapshot))
+            })
+        });
+        if pool.len() == before {
+            break;
         }
     }
+    let mut candidates = pool;
     if candidates.is_empty() {
         return candidates;
     }
 
     // Rule (2) observation check: disqualify any candidate read in a
-    // non-`ToInt32`-coercing position.
-    let mut disqualified: HashSet<u32> = HashSet::new();
-    observe_stmts(stmts, &candidates, &types, &mut disqualified);
-
-    candidates.retain(|id| !disqualified.contains(id));
+    // non-`ToInt32`-coercing position (additive-operand positions inside a
+    // candidate's own admissible additive write are blessed). Disqualifying a
+    // candidate can invalidate another candidate's additive operand, so this
+    // also runs to a fixpoint.
+    loop {
+        let mut disqualified: HashSet<u32> = HashSet::new();
+        let additive_ctx = AdditiveCtx {
+            ta_lens: &ta_lens,
+            pool: &candidates,
+        };
+        observe_stmts(stmts, &candidates, &types, &additive_ctx, &mut disqualified);
+        if disqualified.is_empty() {
+            break;
+        }
+        candidates.retain(|id| !disqualified.contains(id));
+        // A shrunken pool can turn a previously-admissible additive write
+        // inadmissible — re-run rule (1) against the new pool.
+        let mut changed = true;
+        while changed {
+            let before = candidates.len();
+            let snapshot = candidates.clone();
+            candidates.retain(|id| {
+                facts.writes[id].iter().all(|(w, in_loop)| {
+                    write_is_i32_producing_safe(w, &types)
+                        || (!in_loop
+                            && !additive_invalid.contains(id)
+                            && additive_write_admissible(w, &types, &ta_lens, &snapshot))
+                })
+            });
+            changed = candidates.len() != before;
+        }
+        if candidates.is_empty() {
+            return candidates;
+        }
+    }
     candidates
 }
 
+/// Context for the additive-operand blessing in the observation walk.
+struct AdditiveCtx<'a> {
+    ta_lens: &'a HashMap<u32, i64>,
+    pool: &'a HashSet<u32>,
+}
+
 // ---------------------------------------------------------------------------
 // Fact collection (writes / seeds / update targets / closure refs).
 // ---------------------------------------------------------------------------
 
-fn collect_facts<'a>(stmts: &'a [Stmt], types: &HashMap<u32, HirType>, facts: &mut Facts<'a>) {
+fn collect_facts<'a>(
+    stmts: &'a [Stmt],
+    types: &HashMap<u32, HirType>,
+    in_loop: bool,
+    facts: &mut Facts<'a>,
+) {
     for s in stmts {
         match s {
             Stmt::Let { id, init, .. } => {
                 facts.let_declared.insert(*id);
                 if let Some(e) = init {
-                    record_write(*id, e, types, facts);
-                    collect_facts_expr(e, types, facts);
+                    record_write(*id, e, types, in_loop, facts);
+                    collect_facts_expr(e, types, in_loop, facts);
                 }
             }
-            Stmt::Expr(e) | Stmt::Throw(e) => collect_facts_expr(e, types, facts),
+            Stmt::Expr(e) | Stmt::Throw(e) => collect_facts_expr(e, types, in_loop, facts),
             Stmt::Return(opt) => {
                 if let Some(e) = opt {
-                    collect_facts_expr(e, types, facts);
+                    collect_facts_expr(e, types, in_loop, facts);
                 }
             }
             Stmt::If {
@@ -240,19 +644,19 @@ fn collect_facts<'a>(stmts: &'a [Stmt], types: &HashMap<u32, HirType>, facts: &m
                 then_branch,
                 else_branch,
             } => {
-                collect_facts_expr(condition, types, facts);
-                collect_facts(then_branch, types, facts);
+                collect_facts_expr(condition, types, in_loop, facts);
+                collect_facts(then_branch, types, in_loop, facts);
                 if let Some(eb) = else_branch {
-                    collect_facts(eb, types, facts);
+                    collect_facts(eb, types, in_loop, facts);
                 }
             }
             Stmt::While { condition, body } => {
-                collect_facts_expr(condition, types, facts);
-                collect_facts(body, types, facts);
+                collect_facts_expr(condition, types, true, facts);
+                collect_facts(body, types, true, facts);
             }
             Stmt::DoWhile { body, condition } => {
-                collect_facts(body, types, facts);
-                collect_facts_expr(condition, types, facts);
+                collect_facts(body, types, true, facts);
+                collect_facts_expr(condition, types, true, facts);
             }
             Stmt::For {
                 init,
@@ -261,42 +665,42 @@ fn collect_facts<'a>(stmts: &'a [Stmt], types: &HashMap<u32, HirType>, facts: &m
                 body,
             } => {
                 if let Some(i) = init {
-                    collect_facts(std::slice::from_ref(i.as_ref()), types, facts);
+                    collect_facts(std::slice::from_ref(i.as_ref()), types, in_loop, facts);
                 }
                 if let Some(c) = condition {
-                    collect_facts_expr(c, types, facts);
+                    collect_facts_expr(c, types, true, facts);
                 }
                 if let Some(u) = update {
-                    collect_facts_expr(u, types, facts);
+                    collect_facts_expr(u, types, true, facts);
                 }
-                collect_facts(body, types, facts);
+                collect_facts(body, types, true, facts);
             }
             Stmt::Labeled { body, .. } => {
-                collect_facts(std::slice::from_ref(body.as_ref()), types, facts);
+                collect_facts(std::slice::from_ref(body.as_ref()), types, in_loop, facts);
             }
             Stmt::Try {
                 body,
                 catch,
                 finally,
             } => {
-                collect_facts(body, types, facts);
+                collect_facts(body, types, in_loop, facts);
                 if let Some(c) = catch {
-                    collect_facts(&c.body, types, facts);
+                    collect_facts(&c.body, types, in_loop, facts);
                 }
                 if let Some(f) = finally {
-                    collect_facts(f, types, facts);
+                    collect_facts(f, types, in_loop, facts);
                 }
             }
             Stmt::Switch {
                 discriminant,
                 cases,
             } => {
-                collect_facts_expr(discriminant, types, facts);
+                collect_facts_expr(discriminant, types, in_loop, facts);
                 for case in cases {
                     if let Some(t) = &case.test {
-                        collect_facts_expr(t, types, facts);
+                        collect_facts_expr(t, types, in_loop, facts);
                     }
-                    collect_facts(&case.body, types, facts);
+                    collect_facts(&case.body, types, in_loop, facts);
                 }
             }
             Stmt::Break
@@ -309,17 +713,28 @@ fn collect_facts<'a>(stmts: &'a [Stmt], types: &HashMap<u32, HirType>, facts: &m
     }
 }
 
-fn record_write<'a>(id: u32, rhs: &'a Expr, types: &HashMap<u32, HirType>, facts: &mut Facts<'a>) {
-    facts.writes.entry(id).or_default().push(rhs);
+fn record_write<'a>(
+    id: u32,
+    rhs: &'a Expr,
+    types: &HashMap<u32, HirType>,
+    in_loop: bool,
+    facts: &mut Facts<'a>,
+) {
+    facts.writes.entry(id).or_default().push((rhs, in_loop));
     if is_int_kind_ta_read(rhs, types) {
         facts.seeded.insert(id);
     }
 }
 
-fn collect_facts_expr<'a>(e: &'a Expr, types: &HashMap<u32, HirType>, facts: &mut Facts<'a>) {
+fn collect_facts_expr<'a>(
+    e: &'a Expr,
+    types: &HashMap<u32, HirType>,
+    in_loop: bool,
+    facts: &mut Facts<'a>,
+) {
     match e {
         Expr::LocalSet(id, rhs) => {
-            record_write(*id, rhs, types, facts);
+            record_write(*id, rhs, types, in_loop, facts);
         }
         Expr::Update { id, .. } => {
             facts.update_targets.insert(*id);
@@ -329,12 +744,14 @@ fn collect_facts_expr<'a>(e: &'a Expr, types: &HashMap<u32, HirType>, facts: &mu
             collect_closure_refs(e, &mut facts.closure_refs);
             // Still descend to record nested `Update` targets on ENCLOSING
             // locals (defensive; those ids are already in `closure_refs`).
-            perry_hir::walker::walk_expr_children(e, &mut |c| collect_facts_expr(c, types, facts));
+            perry_hir::walker::walk_expr_children(e, &mut |c| {
+                collect_facts_expr(c, types, in_loop, facts)
+            });
             return;
         }
         _ => {}
     }
-    perry_hir::walker::walk_expr_children(e, &mut |c| collect_facts_expr(c, types, facts));
+    perry_hir::walker::walk_expr_children(e, &mut |c| collect_facts_expr(c, types, in_loop, facts));
 }
 
 /// Collect every local id read or written anywhere inside `e` (used to exclude
@@ -467,19 +884,28 @@ fn observe_stmts(
     stmts: &[Stmt],
     cands: &HashSet<u32>,
     types: &HashMap<u32, HirType>,
+    additive: &AdditiveCtx<'_>,
     disq: &mut HashSet<u32>,
 ) {
     for s in stmts {
         match s {
-            Stmt::Let { init, .. } => {
+            Stmt::Let { id, init, .. } => {
                 if let Some(e) = init {
-                    observe(e, false, cands, types, disq);
+                    // Same additive blessing as the `LocalSet` arm — a
+                    // candidate's Let-init may be an admissible additive tree.
+                    if cands.contains(id)
+                        && additive_write_admissible(e, types, additive.ta_lens, additive.pool)
+                    {
+                        observe_additive_rhs(e, cands, types, additive, disq);
+                    } else {
+                        observe(e, false, cands, types, additive, disq);
+                    }
                 }
             }
-            Stmt::Expr(e) | Stmt::Throw(e) => observe(e, false, cands, types, disq),
+            Stmt::Expr(e) | Stmt::Throw(e) => observe(e, false, cands, types, additive, disq),
             Stmt::Return(opt) => {
                 if let Some(e) = opt {
-                    observe(e, false, cands, types, disq);
+                    observe(e, false, cands, types, additive, disq);
                 }
             }
             Stmt::If {
@@ -487,19 +913,19 @@ fn observe_stmts(
                 then_branch,
                 else_branch,
             } => {
-                observe(condition, false, cands, types, disq);
-                observe_stmts(then_branch, cands, types, disq);
+                observe(condition, false, cands, types, additive, disq);
+                observe_stmts(then_branch, cands, types, additive, disq);
                 if let Some(eb) = else_branch {
-                    observe_stmts(eb, cands, types, disq);
+                    observe_stmts(eb, cands, types, additive, disq);
                 }
             }
             Stmt::While { condition, body } => {
-                observe(condition, false, cands, types, disq);
-                observe_stmts(body, cands, types, disq);
+                observe(condition, false, cands, types, additive, disq);
+                observe_stmts(body, cands, types, additive, disq);
             }
             Stmt::DoWhile { body, condition } => {
-                observe_stmts(body, cands, types, disq);
-                observe(condition, false, cands, types, disq);
+                observe_stmts(body, cands, types, additive, disq);
+                observe(condition, false, cands, types, additive, disq);
             }
             Stmt::For {
                 init,
@@ -508,42 +934,54 @@ fn observe_stmts(
                 body,
             } => {
                 if let Some(i) = init {
-                    observe_stmts(std::slice::from_ref(i.as_ref()), cands, types, disq);
+                    observe_stmts(
+                        std::slice::from_ref(i.as_ref()),
+                        cands,
+                        types,
+                        additive,
+                        disq,
+                    );
                 }
                 if let Some(c) = condition {
-                    observe(c, false, cands, types, disq);
+                    observe(c, false, cands, types, additive, disq);
                 }
                 if let Some(u) = update {
-                    observe(u, false, cands, types, disq);
+                    observe(u, false, cands, types, additive, disq);
                 }
-                observe_stmts(body, cands, types, disq);
+                observe_stmts(body, cands, types, additive, disq);
             }
             Stmt::Labeled { body, .. } => {
-                observe_stmts(std::slice::from_ref(body.as_ref()), cands, types, disq);
+                observe_stmts(
+                    std::slice::from_ref(body.as_ref()),
+                    cands,
+                    types,
+                    additive,
+                    disq,
+                );
             }
             Stmt::Try {
                 body,
                 catch,
                 finally,
             } => {
-                observe_stmts(body, cands, types, disq);
+                observe_stmts(body, cands, types, additive, disq);
                 if let Some(c) = catch {
-                    observe_stmts(&c.body, cands, types, disq);
+                    observe_stmts(&c.body, cands, types, additive, disq);
                 }
                 if let Some(f) = finally {
-                    observe_stmts(f, cands, types, disq);
+                    observe_stmts(f, cands, types, additive, disq);
                 }
             }
             Stmt::Switch {
                 discriminant,
                 cases,
             } => {
-                observe(discriminant, false, cands, types, disq);
+                observe(discriminant, false, cands, types, additive, disq);
                 for case in cases {
                     if let Some(t) = &case.test {
-                        observe(t, false, cands, types, disq);
+                        observe(t, false, cands, types, additive, disq);
                     }
-                    observe_stmts(&case.body, cands, types, disq);
+                    observe_stmts(&case.body, cands, types, additive, disq);
                 }
             }
             _ => {}
@@ -556,6 +994,7 @@ fn observe(
     coercing: bool,
     cands: &HashSet<u32>,
     types: &HashMap<u32, HirType>,
+    additive: &AdditiveCtx<'_>,
     disq: &mut HashSet<u32>,
 ) {
     match e {
@@ -574,13 +1013,20 @@ fn observe(
         // Bitwise binary: both operands are `ToInt32`-coerced.
         Expr::Binary { op, left, right } => {
             let c = is_bitwise_binop(*op);
-            observe(left, c, cands, types, disq);
-            observe(right, c, cands, types, disq);
+            observe(left, c, cands, types, additive, disq);
+            observe(right, c, cands, types, additive, disq);
         }
         // `~x` coerces its operand via `ToInt32`; `-x`/`+x`/`!x` do NOT make an
         // `undefined`-vs-integer distinction disappear.
         Expr::Unary { op, operand } => {
-            observe(operand, matches!(op, UnaryOp::BitNot), cands, types, disq);
+            observe(
+                operand,
+                matches!(op, UnaryOp::BitNot),
+                cands,
+                types,
+                additive,
+                disq,
+            );
         }
         // Store into a typed-array element: the value is coerced (`ToInt32` /
         // `ToUint8` / …) iff the receiver is an int-kind typed array. The index
@@ -593,25 +1039,26 @@ fn observe(
             receiver,
             ..
         } => {
-            observe(target, false, cands, types, disq);
-            observe(key, false, cands, types, disq);
-            observe(receiver, false, cands, types, disq);
+            observe(target, false, cands, types, additive, disq);
+            observe(key, false, cands, types, additive, disq);
+            observe(receiver, false, cands, types, additive, disq);
             let store_coercing =
                 receiver_is_int_kind_ta(receiver, types) || receiver_is_int_kind_ta(target, types);
-            observe(value, store_coercing, cands, types, disq);
+            observe(value, store_coercing, cands, types, additive, disq);
         }
         Expr::IndexSet {
             object,
             index,
             value,
         } => {
-            observe(object, false, cands, types, disq);
-            observe(index, false, cands, types, disq);
+            observe(object, false, cands, types, additive, disq);
+            observe(index, false, cands, types, additive, disq);
             observe(
                 value,
                 receiver_is_int_kind_ta(object, types),
                 cands,
                 types,
+                additive,
                 disq,
             );
         }
@@ -622,24 +1069,32 @@ fn observe(
             index,
             value,
         } => {
-            observe(array, false, cands, types, disq);
-            observe(index, false, cands, types, disq);
-            observe(value, true, cands, types, disq);
+            observe(array, false, cands, types, additive, disq);
+            observe(index, false, cands, types, additive, disq);
+            observe(value, true, cands, types, additive, disq);
         }
         Expr::BufferIndexSet {
             buffer,
             index,
             value,
         } => {
-            observe(buffer, false, cands, types, disq);
-            observe(index, false, cands, types, disq);
-            observe(value, true, cands, types, disq);
+            observe(buffer, false, cands, types, additive, disq);
+            observe(index, false, cands, types, additive, disq);
+            observe(value, true, cands, types, additive, disq);
         }
         // Assignment rhs: a bare `LocalGet(cand)` here is a copy (not modeled),
         // so it is non-coercing. Nested bitwise sub-expressions re-establish
-        // coercing-ness for their own operands.
-        Expr::LocalSet(_, value) => {
-            observe(value, false, cands, types, disq);
+        // coercing-ness for their own operands. EXCEPTION (wrap-i32): a
+        // candidate's own admissible additive write blesses candidate reads
+        // at its Add/Sub-operand positions.
+        Expr::LocalSet(target, value) => {
+            if cands.contains(target)
+                && additive_write_admissible(value, types, additive.ta_lens, additive.pool)
+            {
+                observe_additive_rhs(value, cands, types, additive, disq);
+            } else {
+                observe(value, false, cands, types, additive, disq);
+            }
         }
         // Closure-touched candidates are already excluded; do not descend.
         Expr::Closure { .. } => {}
@@ -647,11 +1102,62 @@ fn observe(
         // so any candidate read there disqualifies it.
         _ => {
             perry_hir::walker::walk_expr_children(e, &mut |c| {
-                observe(c, false, cands, types, disq)
+                observe(c, false, cands, types, additive, disq)
             });
         }
     }
 }
 
+/// Observation walk for an ADMISSIBLE additive write's RHS: candidate reads at
+/// Add/Sub-operand chain positions are blessed (the slot's ToInt32 image is
+/// exact there — see `additive_write_admissible`); every other nested position
+/// (typed-array INDEX expressions, unmodeled shapes) keeps the strict rule.
+fn observe_additive_rhs(
+    e: &Expr,
+    cands: &HashSet<u32>,
+    types: &HashMap<u32, HirType>,
+    additive: &AdditiveCtx<'_>,
+    disq: &mut HashSet<u32>,
+) {
+    match e {
+        // Blessed operand read of a candidate (or a plain non-candidate read
+        // — no constraint either way).
+        Expr::LocalGet(_) | Expr::Integer(_) | Expr::Number(_) => {}
+        Expr::Binary { op, left, right } if matches!(op, BinaryOp::Add | BinaryOp::Sub) => {
+            observe_additive_rhs(left, cands, types, additive, disq);
+            observe_additive_rhs(right, cands, types, additive, disq);
+        }
+        // Bitwise/`~`/`imul` operands are ToInt32/ToUint32-coerced — the
+        // strict walk already treats those positions as coercing.
+        Expr::Binary { op, left, right } if is_bitwise_binop(*op) => {
+            observe(left, true, cands, types, additive, disq);
+            observe(right, true, cands, types, additive, disq);
+        }
+        Expr::Unary {
+            op: UnaryOp::BitNot,
+            operand,
+        } => {
+            observe(operand, true, cands, types, additive, disq);
+        }
+        Expr::MathImul(left, right) => {
+            observe(left, true, cands, types, additive, disq);
+            observe(right, true, cands, types, additive, disq);
+        }
+        // In-bounds-proven typed-array read operand: its INDEX is walked with
+        // the strict (non-coercing) rule — a wrapped image used as an index
+        // would be disqualifying, exactly as in ordinary code.
+        Expr::IndexGet { object, index } => {
+            observe(object, false, cands, types, additive, disq);
+            observe(index, false, cands, types, additive, disq);
+        }
+        Expr::Uint8ArrayGet { .. } | Expr::BufferIndexGet { .. } => {
+            observe(e, false, cands, types, additive, disq);
+        }
+        // Anything else in an "admissible" tree would be a grammar bug —
+        // fall back to the strict walk (disqualifying, never unsound).
+        _ => observe(e, false, cands, types, additive, disq),
+    }
+}
+
 #[cfg(test)]
 mod tests;
diff --git a/crates/perry-codegen/src/collectors/int_valued_ta_locals/tests.rs b/crates/perry-codegen/src/collectors/int_valued_ta_locals/tests.rs
index dc2b740dfc..90a6bfa91f 100644
--- a/crates/perry-codegen/src/collectors/int_valued_ta_locals/tests.rs
+++ b/crates/perry-codegen/src/collectors/int_valued_ta_locals/tests.rs
@@ -61,7 +61,7 @@ fn number_param(id: u32) -> Param {
 }
 
 fn run(stmts: &[Stmt], params: &[Param]) -> HashSet<u32> {
-    collect_int_valued_ta_locals(stmts, params, &HashMap::new())
+    collect_int_valued_ta_locals(stmts, params, &HashMap::new(), &HashMap::new())
 }
 
 #[test]
@@ -234,9 +234,202 @@ fn non_int_kind_typed_array_read_not_seeded() {
         let_stmt(5, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
         set(5, xor(Expr::LocalGet(5), Expr::Integer(3))),
     ];
-    let got = collect_int_valued_ta_locals(&stmts, &params, &binding_types);
+    let got = collect_int_valued_ta_locals(&stmts, &params, &binding_types, &HashMap::new());
     assert!(
         !got.contains(&5),
         "float64 read wrongly seeded a candidate: {got:?}"
     );
 }
+
+/// Masked read on a constant-length receiver: `S[x >>> 24]`-style, provably
+/// in-bounds (window ⊂ [0, len)).
+fn masked_read(arr_id: u32, src: Expr, shift: i64) -> Expr {
+    idx_get(arr_id, bin(BinaryOp::UShr, src, Expr::Integer(shift)))
+}
+
+#[test]
+fn wrap_i32_additive_chain_with_proven_operands_is_admitted() {
+    // The `_encipher` `n` shape: straight-line additive chain whose TA-read
+    // operands carry static windows within a KNOWN constant length.
+    //   var n;              (Let n = undefined — hoisted var seed)
+    //   n = S[l >>> 24];    (possibly-OOB whole-write: seed rule)
+    //   n = n + S[l >>> 24];   (additive: operand window [0,255] < 1024)
+    //   n = n ^ S[l >>> 24];
+    //   l = l ^ n;          (n observed only in bitwise)
+    let params = [int32_array_param(0), number_param(1)];
+    let mut lens = HashMap::new();
+    lens.insert(0u32, 1024i64);
+    let stmts = vec![
+        let_stmt(9, HirType::Any, Some(Expr::Undefined)),
+        let_stmt(8, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
+        set(9, masked_read(0, Expr::LocalGet(8), 24)),
+        set(
+            9,
+            bin(
+                BinaryOp::Add,
+                Expr::LocalGet(9),
+                masked_read(0, Expr::LocalGet(8), 24),
+            ),
+        ),
+        set(
+            9,
+            xor(Expr::LocalGet(9), masked_read(0, Expr::LocalGet(8), 24)),
+        ),
+        set(8, xor(Expr::LocalGet(8), Expr::LocalGet(9))),
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &lens);
+    assert!(
+        got.contains(&9),
+        "wrap-i32 additive accumulator wrongly excluded: {got:?}"
+    );
+    assert!(got.contains(&8), "feistel half wrongly excluded: {got:?}");
+}
+
+#[test]
+fn wrap_i32_additive_inside_loop_is_rejected() {
+    // The same additive write INSIDE a loop: unbounded accumulation makes the
+    // true f64 value exceed 2^53 (rounding), diverging from the wrapped image.
+    let params = [int32_array_param(0), number_param(1)];
+    let mut lens = HashMap::new();
+    lens.insert(0u32, 1024i64);
+    let stmts = vec![
+        let_stmt(9, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
+        Stmt::While {
+            condition: Expr::Bool(true),
+            body: vec![set(
+                9,
+                bin(
+                    BinaryOp::Add,
+                    Expr::LocalGet(9),
+                    masked_read(0, Expr::Integer(0x7fff_ffff), 24),
+                ),
+            )],
+        },
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &lens);
+    assert!(
+        !got.contains(&9),
+        "loop-carried additive chain wrongly admitted: {got:?}"
+    );
+}
+
+#[test]
+fn wrap_i32_candidate_as_bare_index_is_rejected() {
+    // A wrapped image used as a BARE index could alias a different element
+    // than the true out-of-range value — index positions stay disqualifying.
+    let params = [int32_array_param(0), number_param(1)];
+    let mut lens = HashMap::new();
+    lens.insert(0u32, 1024i64);
+    let stmts = vec![
+        let_stmt(9, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
+        set(
+            9,
+            bin(
+                BinaryOp::Add,
+                Expr::LocalGet(9),
+                masked_read(0, Expr::LocalGet(1), 24),
+            ),
+        ),
+        let_stmt(10, HirType::Any, Some(idx_get(0, Expr::LocalGet(9)))),
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &lens);
+    assert!(
+        !got.contains(&9),
+        "bare-index wrap-i32 candidate wrongly admitted: {got:?}"
+    );
+}
+
+#[test]
+fn wrap_i32_additive_operand_with_possibly_undefined_value_is_rejected() {
+    // The operand's LAST write before the additive step is a possibly-OOB
+    // read (dynamic index): its true value can be `undefined`, and
+    // `undefined + 1` is NaN (→ ToInt32 0) while the wrapped image would be
+    // `0 + 1 == 1` — the flow leg must reject the additive write even though
+    // the operand IS a pool member.
+    let params = [int32_array_param(0), number_param(1)];
+    let mut lens = HashMap::new();
+    lens.insert(0u32, 1024i64);
+    let stmts = vec![
+        // let m = S[off];        (possibly OOB — seeds m, but NOT numberish)
+        let_stmt(9, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
+        // let n = m + S[0 >>> 24];  (additive with non-numberish operand m)
+        let_stmt(
+            10,
+            HirType::Any,
+            Some(bin(
+                BinaryOp::Add,
+                Expr::LocalGet(9),
+                masked_read(0, Expr::Integer(0), 24),
+            )),
+        ),
+        set(10, xor(Expr::LocalGet(10), Expr::Integer(1))),
+        set(9, xor(Expr::LocalGet(9), Expr::Integer(1))),
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &lens);
+    assert!(
+        !got.contains(&10),
+        "additive over possibly-undefined operand wrongly admitted: {got:?}"
+    );
+    // m is disqualified too: once n's additive write is inadmissible, n is no
+    // longer a candidate, so m's read inside `m + S[...]` is an ordinary
+    // NON-coercing observation (rule 2) — its true `undefined` would be
+    // distinguishable there.
+    assert!(
+        !got.contains(&9),
+        "operand read in a non-candidate additive position must disqualify: {got:?}"
+    );
+}
+
+#[test]
+fn wrap_i32_additive_operand_reset_in_bounds_is_admitted() {
+    // Same shape, but the operand is RESET by an in-bounds-proven read before
+    // the additive step (the enc_real `n = S[l >>> 24]; n += S[...]` flow) —
+    // the flow leg must keep it.
+    let params = [int32_array_param(0), number_param(1)];
+    let mut lens = HashMap::new();
+    lens.insert(0u32, 1024i64);
+    let stmts = vec![
+        let_stmt(9, HirType::Any, Some(Expr::Undefined)),
+        // reset: in-bounds-proven (window [0,255] < 1024)
+        set(9, masked_read(0, Expr::LocalGet(1), 24)),
+        set(
+            9,
+            bin(
+                BinaryOp::Add,
+                Expr::LocalGet(9),
+                masked_read(0, Expr::LocalGet(1), 24),
+            ),
+        ),
+        set(9, xor(Expr::LocalGet(9), Expr::Integer(1))),
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &lens);
+    assert!(
+        got.contains(&9),
+        "in-bounds-reset additive accumulator wrongly rejected: {got:?}"
+    );
+}
+
+#[test]
+fn wrap_i32_additive_without_length_proof_is_rejected() {
+    // No known constant length for the receiver → the TA-read ADD operand
+    // could be an OOB `undefined` (true value NaN-poisons the chain, wrapped
+    // image would not) — inadmissible.
+    let params = [int32_array_param(0), number_param(1)];
+    let stmts = vec![
+        let_stmt(9, HirType::Any, Some(idx_get(0, Expr::LocalGet(1)))),
+        set(
+            9,
+            bin(
+                BinaryOp::Add,
+                Expr::LocalGet(9),
+                masked_read(0, Expr::LocalGet(1), 24),
+            ),
+        ),
+        set(9, xor(Expr::LocalGet(9), Expr::Integer(1))),
+    ];
+    let got = collect_int_valued_ta_locals(&stmts, &params, &HashMap::new(), &HashMap::new());
+    assert!(
+        !got.contains(&9),
+        "length-unproven additive operand wrongly admitted: {got:?}"
+    );
+}
diff --git a/crates/perry-codegen/src/collectors/mod.rs b/crates/perry-codegen/src/collectors/mod.rs
index 0cadb86003..990067ad93 100644
--- a/crates/perry-codegen/src/collectors/mod.rs
+++ b/crates/perry-codegen/src/collectors/mod.rs
@@ -27,6 +27,7 @@ mod refs;
 mod scalar_method_dispatch;
 mod scalar_methods;
 mod shadow_slots;
+mod spec_abi_sites;
 mod this_as_value;
 mod uppercase_strings;
 
@@ -44,7 +45,10 @@ pub(crate) use closures::collect_closures_in_stmts;
 pub(crate) use escape_arrays::{const_index, MAX_SCALAR_OBJECT_FIELDS};
 pub(crate) use escape_check::{check_escapes_in_stmts, find_new_candidates};
 pub(crate) use escape_news::MAX_SCALAR_ARRAY_LEN;
-pub(crate) use hir_facts::{collect_native_region_fact_graph, NativeRegionFactGraph};
+pub(crate) use hir_facts::{
+    collect_native_region_fact_graph, collect_native_region_fact_graph_with_spec_lens,
+    NativeRegionFactGraph,
+};
 pub(crate) use hot_callees::collect_hot_loop_callees;
 pub(crate) use i32_locals::{
     collect_integer_let_ids, collect_localset_ids_in_stmts, is_strictly_i32_bounded_expr,
@@ -66,6 +70,9 @@ pub(crate) use scalar_methods::simple_scalar_method_summary;
 pub(crate) use shadow_slots::{
     collect_declared_shadow_slots_in_stmts, collect_shadow_slot_clear_points,
 };
+pub(crate) use spec_abi_sites::{
+    collect_spec_abi_facts, local_is_reassigned, reassigned_locals, SpecParamRep, SpecTaBinding,
+};
 pub(crate) use this_as_value::{
     class_chain_extends_builtin_error, class_chain_has_unmodeled_base, class_uses_this_as_value,
 };
diff --git a/crates/perry-codegen/src/collectors/spec_abi_sites.rs b/crates/perry-codegen/src/collectors/spec_abi_sites.rs
new file mode 100644
index 0000000000..5eb506df12
--- /dev/null
+++ b/crates/perry-codegen/src/collectors/spec_abi_sites.rs
@@ -0,0 +1,670 @@
+//! Representation-selection Phase 2 (RFC `docs/representation-selection-rfc.md`
+//! §5.4): whole-module, ctx-free pre-pass that derives **call-site
+//! representation judgments** for direct user-function calls, so codegen can
+//! emit one bounded specialized entry per function and route statically-proven
+//! sites to it with **no per-call guard**.
+//!
+//! Collectors run before any `FnCtx` exists (same two-phase constraint as
+//! `integer_locals`), so every judgment here is purely syntactic and
+//! module-global:
+//!
+//! - **`TaPtr { kind, const_len }`** — the arg is a local/module binding whose
+//!   SINGLE, top-level `let`/`const` binding is `new Int32Array(x)` (or another
+//!   numeric typed-array kind) in a **non-view construction form**: `x` absent,
+//!   an integer-literal length, or a local proven to be a plain array (its own
+//!   single binding is an array literal, never reassigned). The binding local is
+//!   never reassigned anywhere in the module (`LocalSet`/`GlobalSet`/`Update`)
+//!   and never referenced inside any closure body — so at every dominated call
+//!   site the slot still holds that exact typed array, whose header address,
+//!   element kind, and length are fixed for the program's lifetime (typed-array
+//!   storage is non-movable: `gc/types.rs` marks `GC_TYPE_TYPED_ARRAY` /
+//!   `GC_TYPE_BUFFER` `movable: false`, and a non-view typed array cannot be
+//!   detached). `const_len` is `Some` when the length is an integer literal or
+//!   the element count of an array-literal source whose uses provably cannot
+//!   change its length.
+//! - **`I32`** — integer literal in i32 range.
+//! - **`F64`** — any other numeric literal (a JS number's NaN-box IS its
+//!   double bits, so raw-f64 passing is bit-identical).
+//! - anything else → **`Boxed`** (always sound; the public boxed entry remains
+//!   the permanent ABI).
+//!
+//! **Dominance** is judged structurally: a binding only "proves" for call
+//! sites that appear in a LATER top-level statement of the same body (walking
+//! nested branches/loops but never descending into closure bodies, which
+//! execute at unknown times). Codegen mirrors the same rule at lowering time
+//! via `FnCtx::spec_ta_ready`, so a collector/lowering disagreement can only
+//! lose the fast path, never route an unproven value.
+//!
+//! Under-approximation is free everywhere: an unjudged/unproven site simply
+//! keeps today's boxed call path.
+
+use std::collections::{HashMap, HashSet};
+
+use perry_hir::{Expr, Module, Stmt};
+
+/// Per-parameter representation for a specialized entry. `Boxed` slots keep
+/// the NaN-boxed `double` ABI; the others receive raw machine values.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub enum SpecParamRep {
+    /// NaN-boxed double — today's uniform ABI, always sound.
+    Boxed,
+    /// Raw signed i32. Caller proves the value by construction (literal).
+    I32,
+    /// Raw double (bit-identical to the boxed form for numbers).
+    F64,
+    /// Raw `TypedArrayHeader*` of a proven non-view typed array.
+    TaPtr {
+        /// `perry_hir::TYPED_ARRAY_KIND_*` element kind.
+        kind: u8,
+        /// Compile-time-constant element count, when proven.
+        const_len: Option<i64>,
+    },
+}
+
+impl SpecParamRep {
+    /// Symbol-mangle label. `[a-z0-9]` only so the composed symbol survives
+    /// `sanitize`/`sanitize_member` byte-identically.
+    pub fn label(&self) -> String {
+        match self {
+            Self::Boxed => "b".to_string(),
+            Self::I32 => "i32".to_string(),
+            Self::F64 => "f64".to_string(),
+            Self::TaPtr { kind, const_len } => match const_len {
+                Some(len) => format!("ta{kind}x{len}"),
+                None => format!("ta{kind}"),
+            },
+        }
+    }
+}
+
+/// A module binding proven to permanently hold one specific non-view typed
+/// array (see module docs for the exact proof obligations).
+#[derive(Debug, Clone, Copy)]
+pub struct SpecTaBinding {
+    pub kind: u8,
+    pub const_len: Option<i64>,
+}
+
+/// Result of the pre-pass: proven typed-array bindings plus the per-callee
+/// judged direct call sites.
+#[derive(Debug, Default)]
+pub struct SpecAbiModuleFacts {
+    /// LocalId → proof for bindings usable as `TaPtr` args.
+    pub ta_bindings: HashMap<u32, SpecTaBinding>,
+    /// FuncId → one judged rep vector per direct `FuncRef` call site found in
+    /// the module init or a function body (closure bodies excluded).
+    pub call_sites: HashMap<u32, Vec<Vec<SpecParamRep>>>,
+}
+
+/// Numeric (non-BigInt, non-Float16) typed-array kinds — the set with a
+/// `BufferElem` representation in codegen.
+pub(crate) fn spec_ta_kind_is_numeric(kind: u8) -> bool {
+    use perry_hir::*;
+    matches!(
+        kind,
+        TYPED_ARRAY_KIND_INT8
+            | TYPED_ARRAY_KIND_UINT8
+            | TYPED_ARRAY_KIND_UINT8_CLAMPED
+            | TYPED_ARRAY_KIND_INT16
+            | TYPED_ARRAY_KIND_UINT16
+            | TYPED_ARRAY_KIND_INT32
+            | TYPED_ARRAY_KIND_UINT32
+            | TYPED_ARRAY_KIND_FLOAT32
+            | TYPED_ARRAY_KIND_FLOAT64
+    )
+}
+
+/// Every local reassigned (`LocalSet`/`GlobalSet`/`Update`) anywhere in
+/// `stmts`, including inside nested closure bodies. Element writes
+/// (`x[i] = v`) and method calls are NOT reassignments — they cannot change
+/// which typed array the binding refers to, its kind, or its length.
+/// Scan once and probe the set when checking several ids against one body.
+pub(crate) fn reassigned_locals(stmts: &[Stmt]) -> HashSet<u32> {
+    let mut scan = ModuleScan::default();
+    walk_stmts(stmts, 0, &mut scan);
+    scan.writes
+}
+
+/// Single-id convenience over [`reassigned_locals`].
+pub(crate) fn local_is_reassigned(stmts: &[Stmt], id: u32) -> bool {
+    reassigned_locals(stmts).contains(&id)
+}
+
+/// Module-wide structural facts gathered in one walk.
+#[derive(Default)]
+struct ModuleScan {
+    /// Reassignment targets (`LocalSet` / `GlobalSet` / `Update`), any depth.
+    writes: HashSet<u32>,
+    /// Locals referenced (read or written) inside any closure body, plus every
+    /// closure capture list entry.
+    closure_refs: HashSet<u32>,
+    /// `Stmt::Let` occurrence count per id (a sound binding must be unique).
+    let_counts: HashMap<u32, u32>,
+    /// Uses of a local in any position other than `x[i]` read/write receiver
+    /// or `new TypedArray(x)` constructor-argument. Such a use can't reassign
+    /// the binding, but CAN change an array's length (`x.push(...)`,
+    /// `g(x)`, `x.length = n`), so it only demotes `const_len`, not the
+    /// binding proof itself.
+    len_unsafe_uses: HashSet<u32>,
+    /// Ids listed in `PreallocateBoxes` / `PreallocateTdzBoxes`: the slot (or
+    /// module global) holds a BOX pointer, not the value — masking such a slot
+    /// value would yield the box address, so these can never be `TaPtr`
+    /// bindings.
+    boxed_prealloc: HashSet<u32>,
+}
+
+fn record_expr_use(e: &Expr, depth: u32, scan: &mut ModuleScan) {
+    match e {
+        Expr::LocalGet(id) => {
+            scan.len_unsafe_uses.insert(*id);
+            if depth > 0 {
+                scan.closure_refs.insert(*id);
+            }
+        }
+        Expr::LocalSet(id, value) | Expr::GlobalSet(id, value) => {
+            scan.writes.insert(*id);
+            if depth > 0 {
+                scan.closure_refs.insert(*id);
+            }
+            record_expr_use(value, depth, scan);
+        }
+        Expr::Update { id, .. } => {
+            scan.writes.insert(*id);
+            if depth > 0 {
+                scan.closure_refs.insert(*id);
+            }
+            perry_hir::walker::walk_expr_children(e, &mut |c| record_expr_use(c, depth, scan));
+        }
+        // Element-access receiver position is length-safe; everything nested
+        // below it (index/value) is scanned normally.
+        Expr::IndexGet { object, index } => {
+            record_receiver_use(object, depth, scan);
+            record_expr_use(index, depth, scan);
+        }
+        Expr::IndexSet {
+            object,
+            index,
+            value,
+        } => {
+            record_receiver_use(object, depth, scan);
+            record_expr_use(index, depth, scan);
+            record_expr_use(value, depth, scan);
+        }
+        Expr::PutValueSet {
+            target,
+            key,
+            value,
+            receiver,
+            ..
+        } => {
+            record_receiver_use(target, depth, scan);
+            record_receiver_use(receiver, depth, scan);
+            record_expr_use(key, depth, scan);
+            record_expr_use(value, depth, scan);
+        }
+        // `new Int32Array(src)` consumes `src` by COPY (non-view: the arg is
+        // not an ArrayBuffer when the binding proof later demands it), so the
+        // ctor-arg position cannot change `src`'s length afterwards. Length
+        // reads are also safe.
+        Expr::TypedArrayNew { arg: Some(arg), .. } => {
+            if let Expr::LocalGet(id) = arg.as_ref() {
+                if depth > 0 {
+                    scan.closure_refs.insert(*id);
+                }
+            } else {
+                record_expr_use(arg, depth, scan);
+            }
+        }
+        Expr::Closure {
+            body,
+            captures,
+            params,
+            ..
+        } => {
+            for c in captures {
+                scan.closure_refs.insert(*c);
+            }
+            for p in params {
+                if let Some(default) = &p.default {
+                    record_expr_use(default, depth + 1, scan);
+                }
+            }
+            walk_stmts(body, depth + 1, scan);
+            // Defaults/keys hidden in the closure expr's other children.
+            perry_hir::walker::walk_expr_children(e, &mut |c| {
+                // The body statements were walked above; walk_expr_children
+                // only yields child *expressions*, so this cannot re-enter the
+                // body statement list.
+                record_expr_use(c, depth + 1, scan)
+            });
+        }
+        _ => {
+            perry_hir::walker::walk_expr_children(e, &mut |c| record_expr_use(c, depth, scan));
+        }
+    }
+}
+
+/// Receiver position of an element access: a bare local read there is
+/// length-safe (element loads/stores don't resize typed arrays and can't
+/// reassign the binding). Anything more complex is scanned normally.
+fn record_receiver_use(object: &Expr, depth: u32, scan: &mut ModuleScan) {
+    if let Expr::LocalGet(id) = object {
+        if depth > 0 {
+            scan.closure_refs.insert(*id);
+        }
+    } else {
+        record_expr_use(object, depth, scan);
+    }
+}
+
+fn walk_stmts(stmts: &[Stmt], depth: u32, scan: &mut ModuleScan) {
+    for s in stmts {
+        walk_stmt(s, depth, scan);
+    }
+}
+
+fn walk_stmt(s: &Stmt, depth: u32, scan: &mut ModuleScan) {
+    match s {
+        Stmt::Let { id, init, .. } => {
+            *scan.let_counts.entry(*id).or_insert(0) += 1;
+            if depth > 0 {
+                scan.closure_refs.insert(*id);
+            }
+            if let Some(e) = init {
+                record_expr_use(e, depth, scan);
+            }
+        }
+        Stmt::Expr(e) | Stmt::Throw(e) => record_expr_use(e, depth, scan),
+        Stmt::Return(Some(e)) => record_expr_use(e, depth, scan),
+        Stmt::PreallocateBoxes(ids) | Stmt::PreallocateTdzBoxes(ids) => {
+            scan.boxed_prealloc.extend(ids.iter().copied());
+        }
+        Stmt::Return(None)
+        | Stmt::Break
+        | Stmt::Continue
+        | Stmt::LabeledBreak(_)
+        | Stmt::LabeledContinue(_) => {}
+        Stmt::If {
+            condition,
+            then_branch,
+            else_branch,
+        } => {
+            record_expr_use(condition, depth, scan);
+            walk_stmts(then_branch, depth, scan);
+            if let Some(eb) = else_branch {
+                walk_stmts(eb, depth, scan);
+            }
+        }
+        Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => {
+            record_expr_use(condition, depth, scan);
+            walk_stmts(body, depth, scan);
+        }
+        Stmt::For {
+            init,
+            condition,
+            update,
+            body,
+        } => {
+            if let Some(i) = init {
+                walk_stmt(i, depth, scan);
+            }
+            if let Some(c) = condition {
+                record_expr_use(c, depth, scan);
+            }
+            if let Some(u) = update {
+                record_expr_use(u, depth, scan);
+            }
+            walk_stmts(body, depth, scan);
+        }
+        Stmt::Labeled { body, .. } => walk_stmt(body, depth, scan),
+        Stmt::Try {
+            body,
+            catch,
+            finally,
+        } => {
+            walk_stmts(body, depth, scan);
+            if let Some(c) = catch {
+                walk_stmts(&c.body, depth, scan);
+            }
+            if let Some(f) = finally {
+                walk_stmts(f, depth, scan);
+            }
+        }
+        Stmt::Switch {
+            discriminant,
+            cases,
+        } => {
+            record_expr_use(discriminant, depth, scan);
+            for case in cases {
+                if let Some(t) = &case.test {
+                    record_expr_use(t, depth, scan);
+                }
+                walk_stmts(&case.body, depth, scan);
+            }
+        }
+    }
+}
+
+/// All executable bodies of the module: init, every function, every class
+/// member body (constructors, methods, accessors, computed members, field
+/// initializers). The write/closure scan must see all of them — a reassignment
+/// hiding in a class method must disqualify a binding.
+fn scan_whole_module(hir: &Module) -> ModuleScan {
+    let mut scan = ModuleScan::default();
+    walk_stmts(&hir.init, 0, &mut scan);
+    for f in &hir.functions {
+        walk_stmts(&f.body, 0, &mut scan);
+    }
+    for c in &hir.classes {
+        if let Some(ctor) = &c.constructor {
+            walk_stmts(&ctor.body, 0, &mut scan);
+        }
+        for m in c.methods.iter().chain(c.static_methods.iter()) {
+            walk_stmts(&m.body, 0, &mut scan);
+        }
+        for (_, g) in &c.getters {
+            walk_stmts(&g.body, 0, &mut scan);
+        }
+        for (_, s) in &c.setters {
+            walk_stmts(&s.body, 0, &mut scan);
+        }
+        for cm in &c.computed_members {
+            record_expr_use(&cm.key_expr, 0, &mut scan);
+            walk_stmts(&cm.function.body, 0, &mut scan);
+        }
+        for field in c.fields.iter().chain(c.static_fields.iter()) {
+            if let Some(key) = &field.key_expr {
+                record_expr_use(key, 0, &mut scan);
+            }
+            if let Some(init) = &field.init {
+                record_expr_use(init, 0, &mut scan);
+            }
+        }
+    }
+    scan
+}
+
+/// Length of an array-literal expression when every element occupies exactly
+/// one slot (no spread).
+fn array_literal_len(e: &Expr) -> Option<i64> {
+    match e {
+        Expr::Array(elements) => Some(elements.len() as i64),
+        Expr::ArraySpread(elements) => {
+            if elements
+                .iter()
+                .any(|el| matches!(el, perry_hir::ArrayElement::Spread(_)))
+            {
+                None
+            } else {
+                Some(elements.len() as i64)
+            }
+        }
+        _ => None,
+    }
+}
+
+/// Judge the `new TypedArray(arg)` constructor argument: `Some(const_len)`
+/// when the construction is provably NON-VIEW (arg is a length or a plain
+/// array — never an ArrayBuffer), `None` when the form is unproven.
+fn judge_ctor_arg(
+    arg: Option<&Expr>,
+    array_literal_locals: &HashMap<u32, Option<i64>>,
+) -> Option<Option<i64>> {
+    match arg {
+        None => Some(Some(0)),
+        Some(Expr::Integer(n)) if (0..=16_000_000).contains(n) => Some(Some(*n)),
+        Some(Expr::Number(f))
+            if f.is_finite() && f.fract() == 0.0 && *f >= 0.0 && *f <= 16_000_000.0 =>
+        {
+            Some(Some(*f as i64))
+        }
+        // A local whose single binding is an array literal, never reassigned:
+        // definitely a plain array (copy construction, non-view). The length
+        // is constant only when no use of the source could have resized it.
+        Some(Expr::LocalGet(id)) => array_literal_locals.get(id).map(|len| *len),
+        _ => None,
+    }
+}
+
+/// One body's sequential site walk: top-level `Stmt::Let`s of proven bindings
+/// make the binding "ready"; every direct `FuncRef` call anywhere below a
+/// top-level statement is judged against the currently-ready set. Closure
+/// bodies are never descended (they run at unknown times).
+fn judge_sites_in_body(
+    stmts: &[Stmt],
+    ta_bindings: &HashMap<u32, SpecTaBinding>,
+    out: &mut HashMap<u32, Vec<Vec<SpecParamRep>>>,
+) {
+    let mut ready: HashSet<u32> = HashSet::new();
+    for s in stmts {
+        judge_stmt(s, ta_bindings, &ready, out);
+        if let Stmt::Let { id, .. } = s {
+            if ta_bindings.contains_key(id) {
+                ready.insert(*id);
+            }
+        }
+    }
+}
+
+fn judge_stmt(
+    s: &Stmt,
+    ta: &HashMap<u32, SpecTaBinding>,
+    ready: &HashSet<u32>,
+    out: &mut HashMap<u32, Vec<Vec<SpecParamRep>>>,
+) {
+    match s {
+        Stmt::Let { init: Some(e), .. } => judge_expr(e, ta, ready, out),
+        Stmt::Let { init: None, .. } => {}
+        Stmt::Expr(e) | Stmt::Throw(e) => judge_expr(e, ta, ready, out),
+        Stmt::Return(opt) => {
+            if let Some(e) = opt {
+                judge_expr(e, ta, ready, out);
+            }
+        }
+        Stmt::If {
+            condition,
+            then_branch,
+            else_branch,
+        } => {
+            judge_expr(condition, ta, ready, out);
+            for st in then_branch {
+                judge_stmt(st, ta, ready, out);
+            }
+            if let Some(eb) = else_branch {
+                for st in eb {
+                    judge_stmt(st, ta, ready, out);
+                }
+            }
+        }
+        Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => {
+            judge_expr(condition, ta, ready, out);
+            for st in body {
+                judge_stmt(st, ta, ready, out);
+            }
+        }
+        Stmt::For {
+            init,
+            condition,
+            update,
+            body,
+        } => {
+            if let Some(i) = init {
+                judge_stmt(i, ta, ready, out);
+            }
+            if let Some(c) = condition {
+                judge_expr(c, ta, ready, out);
+            }
+            if let Some(u) = update {
+                judge_expr(u, ta, ready, out);
+            }
+            for st in body {
+                judge_stmt(st, ta, ready, out);
+            }
+        }
+        Stmt::Labeled { body, .. } => judge_stmt(body, ta, ready, out),
+        Stmt::Try {
+            body,
+            catch,
+            finally,
+        } => {
+            for st in body {
+                judge_stmt(st, ta, ready, out);
+            }
+            if let Some(c) = catch {
+                for st in &c.body {
+                    judge_stmt(st, ta, ready, out);
+                }
+            }
+            if let Some(f) = finally {
+                for st in f {
+                    judge_stmt(st, ta, ready, out);
+                }
+            }
+        }
+        Stmt::Switch {
+            discriminant,
+            cases,
+        } => {
+            judge_expr(discriminant, ta, ready, out);
+            for case in cases {
+                if let Some(t) = &case.test {
+                    judge_expr(t, ta, ready, out);
+                }
+                for st in &case.body {
+                    judge_stmt(st, ta, ready, out);
+                }
+            }
+        }
+        _ => {}
+    }
+}
+
+/// Judge one argument expression. This is the collector twin of the
+/// lowering-time per-slot match in `lower_call/func_ref.rs` — both must accept
+/// the same shapes (the collector chooses the tuple; the lowering-time check
+/// is the one that is load-bearing for soundness).
+pub(crate) fn judge_arg(
+    arg: &Expr,
+    ta: &HashMap<u32, SpecTaBinding>,
+    ready: &HashSet<u32>,
+) -> SpecParamRep {
+    match arg {
+        Expr::Integer(n) if i32::try_from(*n).is_ok() => SpecParamRep::I32,
+        Expr::Integer(_) => SpecParamRep::F64,
+        Expr::Number(_) => SpecParamRep::F64,
+        Expr::LocalGet(id) => match ta.get(id) {
+            Some(binding) if ready.contains(id) => SpecParamRep::TaPtr {
+                kind: binding.kind,
+                const_len: binding.const_len,
+            },
+            _ => SpecParamRep::Boxed,
+        },
+        _ => SpecParamRep::Boxed,
+    }
+}
+
+fn judge_expr(
+    e: &Expr,
+    ta: &HashMap<u32, SpecTaBinding>,
+    ready: &HashSet<u32>,
+    out: &mut HashMap<u32, Vec<Vec<SpecParamRep>>>,
+) {
+    if let Expr::Call { callee, args, .. } = e {
+        if let Expr::FuncRef(fid) = callee.as_ref() {
+            let judged: Vec<SpecParamRep> = args.iter().map(|a| judge_arg(a, ta, ready)).collect();
+            out.entry(*fid).or_default().push(judged);
+        }
+    }
+    // Closures execute at unknown times relative to the bindings — never
+    // judge call sites inside them (their sites keep the boxed path).
+    if matches!(e, Expr::Closure { .. }) {
+        return;
+    }
+    perry_hir::walker::walk_expr_children(e, &mut |c| judge_expr(c, ta, ready, out));
+}
+
+/// Run the whole pre-pass on a module.
+pub fn collect_spec_abi_facts(hir: &Module) -> SpecAbiModuleFacts {
+    let scan = scan_whole_module(hir);
+
+    // Array-literal-bound, never-reassigned, non-closure-referenced locals:
+    // proven plain arrays. Value is `Some(len)` when additionally no use could
+    // have changed the length before/after construction (conservatively: the
+    // local has NO uses outside element-access-receiver / TA-ctor-arg
+    // positions — `len_unsafe_uses` records everything else).
+    let mut array_literal_locals: HashMap<u32, Option<i64>> = HashMap::new();
+    let mut collect_array_literals = |stmts: &[Stmt]| {
+        for s in stmts {
+            if let Stmt::Let {
+                id, init: Some(e), ..
+            } = s
+            {
+                if scan.let_counts.get(id).copied() == Some(1)
+                    && !scan.writes.contains(id)
+                    && !scan.closure_refs.contains(id)
+                {
+                    if let Some(len) = array_literal_len(e) {
+                        let exact = !scan.len_unsafe_uses.contains(id);
+                        array_literal_locals.insert(*id, exact.then_some(len));
+                    }
+                }
+            }
+        }
+    };
+    collect_array_literals(&hir.init);
+    for f in &hir.functions {
+        collect_array_literals(&f.body);
+    }
+
+    // Proven typed-array bindings: single TOP-LEVEL `let`/`const` bound to a
+    // provably-non-view `TypedArrayNew` of a numeric kind, never reassigned,
+    // never referenced by a closure.
+    let mut ta_bindings: HashMap<u32, SpecTaBinding> = HashMap::new();
+    let mut collect_ta = |stmts: &[Stmt]| {
+        for s in stmts {
+            if let Stmt::Let {
+                id,
+                init: Some(Expr::TypedArrayNew { kind, arg }),
+                ..
+            } = s
+            {
+                if !spec_ta_kind_is_numeric(*kind)
+                    || scan.let_counts.get(id).copied() != Some(1)
+                    || scan.writes.contains(id)
+                    || scan.closure_refs.contains(id)
+                    || scan.boxed_prealloc.contains(id)
+                {
+                    continue;
+                }
+                if let Some(const_len) = judge_ctor_arg(arg.as_deref(), &array_literal_locals) {
+                    ta_bindings.insert(
+                        *id,
+                        SpecTaBinding {
+                            kind: *kind,
+                            const_len,
+                        },
+                    );
+                }
+            }
+        }
+    };
+    collect_ta(&hir.init);
+    for f in &hir.functions {
+        collect_ta(&f.body);
+    }
+
+    // Judge every direct call site in init + function bodies.
+    let mut call_sites: HashMap<u32, Vec<Vec<SpecParamRep>>> = HashMap::new();
+    judge_sites_in_body(&hir.init, &ta_bindings, &mut call_sites);
+    for f in &hir.functions {
+        judge_sites_in_body(&f.body, &ta_bindings, &mut call_sites);
+    }
+
+    SpecAbiModuleFacts {
+        ta_bindings,
+        call_sites,
+    }
+}
+
+#[cfg(test)]
+mod tests;
diff --git a/crates/perry-codegen/src/collectors/spec_abi_sites/tests.rs b/crates/perry-codegen/src/collectors/spec_abi_sites/tests.rs
new file mode 100644
index 0000000000..d3d8b6353b
--- /dev/null
+++ b/crates/perry-codegen/src/collectors/spec_abi_sites/tests.rs
@@ -0,0 +1,345 @@
+use super::*;
+use perry_hir::types::Type;
+use perry_hir::{Function, Module, TYPED_ARRAY_KIND_INT32};
+
+fn let_stmt(id: u32, mutable: bool, init: Expr) -> Stmt {
+    Stmt::Let {
+        id,
+        name: format!("v{id}"),
+        ty: Type::Any,
+        mutable,
+        init: Some(init),
+    }
+}
+
+fn ta_new(kind: u8, arg: Option<Expr>) -> Expr {
+    Expr::TypedArrayNew {
+        kind,
+        arg: arg.map(Box::new),
+    }
+}
+
+fn call(fid: u32, args: Vec<Expr>) -> Expr {
+    Expr::Call {
+        callee: Box::new(Expr::FuncRef(fid)),
+        args,
+        type_args: vec![],
+        byte_offset: 0,
+    }
+}
+
+fn func(id: u32, body: Vec<Stmt>) -> Function {
+    Function {
+        id,
+        name: format!("f{id}"),
+        type_params: vec![],
+        params: vec![],
+        return_type: Type::Any,
+        body,
+        is_async: false,
+        is_generator: false,
+        is_strict: false,
+        is_exported: false,
+        captures: vec![],
+        decorators: vec![],
+        was_plain_async: false,
+        was_unrolled: false,
+    }
+}
+
+fn module_with_init(init: Vec<Stmt>) -> Module {
+    let mut m = Module::new("spec_abi_test");
+    m.init = init;
+    m
+}
+
+#[test]
+fn literal_length_binding_and_dominated_site() {
+    // const P = new Int32Array(4); f(P, 0, 1.5);
+    let m = module_with_init(vec![
+        let_stmt(
+            10,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(call(
+            7,
+            vec![Expr::LocalGet(10), Expr::Integer(0), Expr::Number(1.5)],
+        )),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    let b = facts.ta_bindings.get(&10).expect("binding proven");
+    assert_eq!(b.kind, TYPED_ARRAY_KIND_INT32);
+    assert_eq!(b.const_len, Some(4));
+    let sites = facts.call_sites.get(&7).expect("site judged");
+    assert_eq!(
+        sites[0],
+        vec![
+            SpecParamRep::TaPtr {
+                kind: TYPED_ARRAY_KIND_INT32,
+                const_len: Some(4)
+            },
+            SpecParamRep::I32,
+            SpecParamRep::F64,
+        ]
+    );
+}
+
+#[test]
+fn array_literal_source_counts_elements() {
+    // var A = [1,2,3]; const P = new Int32Array(A); f(P)
+    let m = module_with_init(vec![
+        let_stmt(
+            1,
+            true,
+            Expr::Array(vec![Expr::Integer(1), Expr::Integer(2), Expr::Integer(3)]),
+        ),
+        let_stmt(
+            2,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::LocalGet(1))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(2)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert_eq!(
+        facts.ta_bindings.get(&2).map(|b| b.const_len),
+        Some(Some(3))
+    );
+}
+
+#[test]
+fn unproven_ctor_arg_rejects_binding() {
+    // Potential view form: `new Int32Array(x)` where x's provenance is
+    // unknown (could be an ArrayBuffer) — must NOT prove.
+    let m = module_with_init(vec![
+        let_stmt(1, false, Expr::Undefined),
+        let_stmt(
+            2,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::LocalGet(1))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(2)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&2));
+    assert_eq!(
+        facts.call_sites.get(&7).unwrap()[0],
+        vec![SpecParamRep::Boxed]
+    );
+}
+
+#[test]
+fn reassignment_rejects_binding() {
+    // let P = new Int32Array(4); P = undefined; f(P)
+    let m = module_with_init(vec![
+        let_stmt(
+            3,
+            true,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(Expr::LocalSet(3, Box::new(Expr::Undefined))),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(3)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&3));
+}
+
+#[test]
+fn reassignment_in_another_function_rejects_binding() {
+    // The write scan is module-wide: a reassignment hiding in a different
+    // function body must disqualify the init-scope binding.
+    let mut m = module_with_init(vec![
+        let_stmt(
+            3,
+            true,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(3)])),
+    ]);
+    m.functions.push(func(
+        7,
+        vec![Stmt::Expr(Expr::LocalSet(3, Box::new(Expr::Undefined)))],
+    ));
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&3));
+}
+
+#[test]
+fn closure_reference_rejects_binding() {
+    let closure = Expr::Closure {
+        func_id: 99,
+        params: vec![],
+        return_type: Type::Any,
+        body: vec![Stmt::Return(Some(Expr::LocalGet(3)))],
+        captures: vec![3],
+        mutable_captures: vec![],
+        captures_this: false,
+        captures_new_target: false,
+        enclosing_class: None,
+        is_arrow: true,
+        is_async: false,
+        is_generator: false,
+        is_strict: false,
+    };
+    let m = module_with_init(vec![
+        let_stmt(
+            3,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        let_stmt(4, false, closure),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(3)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&3));
+}
+
+#[test]
+fn call_before_binding_is_not_dominated() {
+    // f(P) textually BEFORE the Let: the sequential judgment must not prove.
+    let m = module_with_init(vec![
+        Stmt::Expr(call(7, vec![Expr::LocalGet(10)])),
+        let_stmt(
+            10,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(10)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    let sites = facts.call_sites.get(&7).unwrap();
+    assert_eq!(sites[0], vec![SpecParamRep::Boxed]);
+    assert!(matches!(sites[1][0], SpecParamRep::TaPtr { .. }));
+}
+
+#[test]
+fn site_nested_in_loop_after_toplevel_let_is_proven() {
+    // The enc_real shape: Lets, then `for (...) f(lr, 0, P, S)`.
+    let m = module_with_init(vec![
+        let_stmt(
+            10,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(2))),
+        ),
+        Stmt::While {
+            condition: Expr::Bool(true),
+            body: vec![Stmt::Expr(call(
+                7,
+                vec![Expr::LocalGet(10), Expr::Integer(0)],
+            ))],
+        },
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    let sites = facts.call_sites.get(&7).unwrap();
+    assert!(matches!(sites[0][0], SpecParamRep::TaPtr { .. }));
+    assert_eq!(sites[0][1], SpecParamRep::I32);
+}
+
+#[test]
+fn sites_inside_closures_are_never_judged() {
+    let closure = Expr::Closure {
+        func_id: 99,
+        params: vec![],
+        return_type: Type::Any,
+        body: vec![Stmt::Expr(call(7, vec![Expr::Integer(1)]))],
+        captures: vec![],
+        mutable_captures: vec![],
+        captures_this: false,
+        captures_new_target: false,
+        enclosing_class: None,
+        is_arrow: true,
+        is_async: false,
+        is_generator: false,
+        is_strict: false,
+    };
+    let m = module_with_init(vec![let_stmt(4, false, closure)]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(facts.call_sites.get(&7).is_none());
+}
+
+#[test]
+fn length_unsafe_source_use_demotes_const_len_only() {
+    // var A = [1,2]; g(A); const P = new Int32Array(A): A stays a proven
+    // plain array (never reassigned) so P is still non-view, but its length
+    // is no longer a compile-time constant.
+    let m = module_with_init(vec![
+        let_stmt(
+            1,
+            true,
+            Expr::Array(vec![Expr::Integer(1), Expr::Integer(2)]),
+        ),
+        Stmt::Expr(call(8, vec![Expr::LocalGet(1)])),
+        let_stmt(
+            2,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::LocalGet(1))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(2)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    let b = facts.ta_bindings.get(&2).expect("still non-view-proven");
+    assert_eq!(b.const_len, None);
+}
+
+#[test]
+fn bigint_kind_binding_is_rejected() {
+    // BigInt64Array elements are BigInt, not Number — never a `TaPtr` binding.
+    let m = module_with_init(vec![
+        let_stmt(
+            3,
+            false,
+            ta_new(perry_hir::TYPED_ARRAY_KIND_BIGINT64, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(3)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&3));
+    assert_eq!(
+        facts.call_sites.get(&7).unwrap()[0],
+        vec![SpecParamRep::Boxed]
+    );
+}
+
+#[test]
+fn boxed_prealloc_binding_is_rejected() {
+    // A TDZ/prealloc-flagged id's slot holds a BOX pointer, not the value —
+    // masking it would yield the box address, so it can never prove `TaPtr`.
+    let m = module_with_init(vec![
+        Stmt::PreallocateTdzBoxes(vec![3]),
+        let_stmt(
+            3,
+            false,
+            ta_new(TYPED_ARRAY_KIND_INT32, Some(Expr::Integer(4))),
+        ),
+        Stmt::Expr(call(7, vec![Expr::LocalGet(3)])),
+    ]);
+    let facts = collect_spec_abi_facts(&m);
+    assert!(!facts.ta_bindings.contains_key(&3));
+    assert_eq!(
+        facts.call_sites.get(&7).unwrap()[0],
+        vec![SpecParamRep::Boxed]
+    );
+}
+
+#[test]
+fn local_is_reassigned_sees_closure_writes() {
+    let closure = Expr::Closure {
+        func_id: 99,
+        params: vec![],
+        return_type: Type::Any,
+        body: vec![Stmt::Expr(Expr::LocalSet(5, Box::new(Expr::Integer(1))))],
+        captures: vec![5],
+        mutable_captures: vec![5],
+        captures_this: false,
+        captures_new_target: false,
+        enclosing_class: None,
+        is_arrow: true,
+        is_async: false,
+        is_generator: false,
+        is_strict: false,
+    };
+    let stmts = vec![let_stmt(4, false, closure)];
+    assert!(local_is_reassigned(&stmts, 5));
+    assert!(!local_is_reassigned(&stmts, 6));
+}
diff --git a/crates/perry-codegen/src/expr/buffer_access.rs b/crates/perry-codegen/src/expr/buffer_access.rs
index 4d41ca24f1..d80d4f9270 100644
--- a/crates/perry-codegen/src/expr/buffer_access.rs
+++ b/crates/perry-codegen/src/expr/buffer_access.rs
@@ -237,7 +237,7 @@ fn lower_value_i32(ctx: &mut FnCtx<'_>, value: &Expr) -> Result<String> {
     }
 }
 
-fn can_lower_integer_typed_array_store_value(ctx: &FnCtx<'_>, value: &Expr) -> bool {
+pub(crate) fn can_lower_integer_typed_array_store_value(ctx: &FnCtx<'_>, value: &Expr) -> bool {
     can_lower_expr_as_i32(
         value,
         &ctx.i32_counter_slots,
diff --git a/crates/perry-codegen/src/expr/buffer_views.rs b/crates/perry-codegen/src/expr/buffer_views.rs
index 1f0f02f6f3..bc93862302 100644
--- a/crates/perry-codegen/src/expr/buffer_views.rs
+++ b/crates/perry-codegen/src/expr/buffer_views.rs
@@ -285,6 +285,10 @@ pub(crate) fn update_buffer_view_for_assignment(
                 alias: AliasState::MayAlias,
                 length_source: Some(LengthSource::Unknown),
                 native_owned: None,
+                // Reassignment refresh: `Uint8ArrayNew` with a non-literal arg
+                // can be the view form (`new Uint8Array(buffer)`), so the
+                // inline-storage proof is not re-established here.
+                storage_inline_proven: false,
             },
         );
     } else {
diff --git a/crates/perry-codegen/src/expr/index_get.rs b/crates/perry-codegen/src/expr/index_get.rs
index 0b776c474d..4ec238e44b 100644
--- a/crates/perry-codegen/src/expr/index_get.rs
+++ b/crates/perry-codegen/src/expr/index_get.rs
@@ -74,18 +74,7 @@ pub(crate) fn numeric_index_has_integer_array_index_proof(ctx: &FnCtx<'_>, index
     }
 }
 
-fn bitand_has_nonnegative_i32_mask(left: &Expr, right: &Expr) -> bool {
-    fn mask(expr: &Expr) -> Option<i64> {
-        match expr {
-            Expr::Integer(i) => Some(*i),
-            Expr::Number(n) if n.is_finite() && n.fract() == 0.0 => Some(*n as i64),
-            _ => None,
-        }
-    }
-    mask(left)
-        .or_else(|| mask(right))
-        .is_some_and(|mask| (0..=i32::MAX as i64).contains(&mask))
-}
+use super::proven_view_access::bitand_has_nonnegative_i32_mask;
 
 /// #6011: decompose a packed-loop index expression into `(counter_local_id,
 /// constant_offset)`. Matches `i`, `i + c`, `c + i`, and `i - c` with a small
@@ -1411,6 +1400,11 @@ pub(crate) fn lower(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String> {
                         MaterializationReason::RuntimeApi,
                     ));
                 }
+                // Phase 2 checked tier: see expr/proven_view_access.rs.
+                if let Some(v) = super::try_lower_proven_view_checked_f64_load(ctx, object, index)?
+                {
+                    return Ok(v);
+                }
                 if typed_array_index_needs_runtime_key(ctx, object.as_ref(), index.as_ref()) {
                     let arr_box = lower_expr(ctx, object)?;
                     let key_box = lower_expr(ctx, index)?;
diff --git a/crates/perry-codegen/src/expr/index_set.rs b/crates/perry-codegen/src/expr/index_set.rs
index 95a6f1eba0..30f5d49f7f 100644
--- a/crates/perry-codegen/src/expr/index_set.rs
+++ b/crates/perry-codegen/src/expr/index_set.rs
@@ -749,6 +749,21 @@ pub(crate) fn lower(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String> {
                         MaterializationReason::FunctionAbi,
                     ));
                 }
+                // Phase 2: storage-proven view with a dynamic (bounds-unproven)
+                // exact-i32 index — inline checked store (OOB = silent no-op),
+                // no kind guard, no runtime call.
+                if let Some(stored) =
+                    super::try_lower_proven_view_checked_store(ctx, object, index, value)?
+                {
+                    if ctx.discard_expr_value {
+                        return Ok(double_literal(0.0));
+                    }
+                    return Ok(materialize_js_value(
+                        ctx,
+                        stored,
+                        MaterializationReason::FunctionAbi,
+                    ));
+                }
                 if typed_array_index_needs_runtime_key(ctx, object.as_ref(), index.as_ref()) {
                     let arr_box = lower_expr(ctx, object)?;
                     let idx_double = lower_expr(ctx, index)?;
diff --git a/crates/perry-codegen/src/expr/mod.rs b/crates/perry-codegen/src/expr/mod.rs
index e8549a085e..79e72cf653 100644
--- a/crates/perry-codegen/src/expr/mod.rs
+++ b/crates/perry-codegen/src/expr/mod.rs
@@ -45,6 +45,7 @@ mod object_literal;
 mod pod_layout_constants;
 mod pod_record;
 mod property_get_names;
+mod proven_view_access;
 mod range_facts;
 mod strings;
 mod typed_feedback;
@@ -55,9 +56,9 @@ mod write_barrier;
 pub(crate) use crate::native_value::{materialize_js_value, materialize_js_value_without_record};
 pub(crate) use array_literal::lower_array_literal;
 pub(crate) use buffer_access::{
-    access_facts_for_spec, emit_buffer_access_pointer, lower_buffer_access_proof,
-    lower_buffer_load, lower_buffer_store, lower_typed_array_load, lower_typed_array_store,
-    BufferAccessSpec,
+    access_facts_for_spec, can_lower_integer_typed_array_store_value, emit_buffer_access_pointer,
+    lower_buffer_access_proof, lower_buffer_load, lower_buffer_store, lower_typed_array_load,
+    lower_typed_array_store, BufferAccessSpec,
 };
 pub(crate) use buffer_views::{
     alias_buffer_view_slot, attach_native_owned_view_fact, buffer_access_materialization_reason,
@@ -93,6 +94,10 @@ pub(crate) use pod_record::{
     lower_and_store_initial_pod_field, lower_pod_local_reassignment, materialize_pod_local,
     try_lower_pod_field_get, try_lower_pod_field_set,
 };
+pub(crate) use proven_view_access::{
+    index_is_exact_i32_shape, local_is_proven_int_store_view,
+    try_lower_proven_view_checked_f64_load, try_lower_proven_view_checked_store,
+};
 pub(crate) use range_facts::{
     bounds_for_buffer_access_width, effective_alias_state_for_access,
     guarded_buffer_indices_for_condition, int_range_expr, invalidate_local_write_facts,
@@ -633,6 +638,13 @@ pub(crate) struct FnCtx<'a> {
     /// cleared after lowering that statement. Built once per user function
     /// from HIR local-reference last-use information.
     pub shadow_slot_clears_after_stmt: std::collections::HashMap<usize, Vec<u32>>,
+    /// Slot indices that have had at least one `js_shadow_slot_bind` (or
+    /// value-set) emitted so far. Slots start zeroed and are only ever
+    /// written through the bind/set helpers, so a scheduled CLEAR of a
+    /// never-bound slot is a provable no-op (`js_shadow_slot_set(idx, 0)` on
+    /// a slot that already holds 0) — `emit_shadow_slot_clear` skips it.
+    /// Seeded at construction with the entry-bound parameter slots.
+    pub shadow_slots_bound: std::collections::HashSet<u32>,
 
     /// Cached pointer to this function's `InlineArenaState` slot —
     /// allocated lazily on the first `new ClassName()` site that uses
@@ -762,6 +774,24 @@ pub(crate) struct FnCtx<'a> {
     /// `repsel_context_allows_canonical_i32` is false.
     pub repsel_closure_ref_locals: std::collections::HashSet<u32>,
 
+    /// Representation-selection Phase 2 (`codegen/spec_abi.rs`): FuncId →
+    /// specialization plan for functions that have an emitted specialized
+    /// entry in this module. Direct `FuncRef` call sites consult this to
+    /// dispatch statically-proven sites to the raw-ABI symbol.
+    pub spec_abi_functions: &'a std::collections::HashMap<u32, crate::codegen::SpecFnPlan>,
+
+    /// Phase 2 pre-pass output (`collectors/spec_abi_sites.rs`): LocalIds
+    /// proven to permanently hold one specific non-view typed array. A call
+    /// arg `LocalGet(id)` matches a `TaPtr` slot only when `id` is here AND in
+    /// `spec_ta_ready` (its binding statement already lowered at top level).
+    pub spec_ta_bindings: &'a std::collections::HashMap<u32, crate::collectors::SpecTaBinding>,
+
+    /// Dominance mirror for `spec_ta_bindings`: ids whose top-level binding
+    /// `Stmt::Let` has been lowered in THIS body (inserted by
+    /// `stmt::lower_top_level_stmts`). A proven binding is only usable at call
+    /// sites it dominates; closure bodies get their own (empty) set.
+    pub spec_ta_ready: std::collections::HashSet<u32>,
+
     /// Parallel `i1` slots for ordinary boolean locals that have stayed inside
     /// the representation-first subset. The generic `double` slot remains as a
     /// compatibility shadow for existing lowering paths, but typed consumers
diff --git a/crates/perry-codegen/src/expr/proven_view_access.rs b/crates/perry-codegen/src/expr/proven_view_access.rs
new file mode 100644
index 0000000000..4034a4e90a
--- /dev/null
+++ b/crates/perry-codegen/src/expr/proven_view_access.rs
@@ -0,0 +1,429 @@
+//! Representation-selection Phase 2: **guard-free checked-native element
+//! access** for storage-proven typed-array views.
+//!
+//! `expr/buffer_access.rs`'s bare-load tier requires a static bounds proof
+//! (`bounds_for_buffer_access_width`). When the index is dynamic (`lr[off]`
+//! with an arbitrary i32 `off` — the bcryptjs `_encipher` entry/exit reads and
+//! writes), that proof cannot exist, and the access previously fell back to a
+//! `js_typed_array_get`/`js_typed_array_index_set_dynamic` runtime call or to
+//! the per-site KIND-GUARDED inline path (`ta_param_f64_read.rs` — measured to
+//! LOSE on unrolled bodies).
+//!
+//! This tier serves receivers whose `BufferViewSlot` carries
+//! `storage_inline_proven` (fresh non-view construction: literal-length
+//! `new TA(n)` let-bindings, or a specialized-entry `TaPtr` param whose
+//! call-site pre-pass proved the construction). For those, element kind,
+//! data pointer, and length are fixed for the array's lifetime, so the access
+//! needs NO kind guard, NO view guard, and NO runtime call — just:
+//!
+//! ```text
+//!   %in = icmp ult i32 %idx, %len      ; len loaded once from the header
+//!   br %in, load/store, oob
+//!   load:  bare element load → f64     (store: bare element store)
+//!   oob:   TAG_UNDEFINED               (store: no-op)
+//! ```
+//!
+//! Bit-exact with the runtime helpers: an in-bounds read yields the numeric
+//! element; OOB / negative / wrapped indices fail the UNSIGNED compare and
+//! yield the `TAG_UNDEFINED` double (reads) or silently skip (writes) —
+//! exactly ECMAScript's IntegerIndexedExotic [[Get]]/[[Set]].
+//!
+//! Index soundness: only shapes proven to be EXACT signed-i32 integers are
+//! accepted (`index_is_exact_i32_shape`) — a fractional or >2^31 index must
+//! keep the runtime path, because an `fptosi`/wrapped i32 could alias a
+//! different (in-bounds) element.
+
+use anyhow::Result;
+use perry_hir::{BinaryOp, Expr};
+
+use super::{can_lower_expr_as_i32, lower_expr_as_i32, lower_expr_native, FnCtx};
+use crate::nanbox::{double_literal, TAG_UNDEFINED};
+use crate::native_value::{
+    BoundsState, BufferAccessMode, BufferElem, BufferIndexUnit, ExpectedNativeRep, LoweredValue,
+};
+use crate::types::{DOUBLE, F32, I16, I32, I64, I8, PTR};
+
+/// `x & <mask>` with a compile-time non-negative i32 mask literal on either
+/// side: the result is a non-negative integer array index for ANY `x`.
+/// (Hosted here from `index_get.rs` for the file-size gate.)
+pub(crate) fn bitand_has_nonnegative_i32_mask(left: &Expr, right: &Expr) -> bool {
+    fn mask(expr: &Expr) -> Option<i64> {
+        match expr {
+            Expr::Integer(i) => Some(*i),
+            Expr::Number(n) if n.is_finite() && n.fract() == 0.0 => Some(*n as i64),
+            _ => None,
+        }
+    }
+    mask(left)
+        .or_else(|| mask(right))
+        .is_some_and(|mask| (0..=i32::MAX as i64).contains(&mask))
+}
+
+/// Small additive offsets keep the wrap analysis trivial: `local + c` with
+/// `0 <= c <= 2^20` can only wrap PAST `i32::MAX`, landing negative, which the
+/// unsigned bounds compare rejects — indistinguishable from the true
+/// (out-of-bounds) index.
+const MAX_ADDEND: i64 = 1 << 20;
+
+/// `true` when `index`'s runtime value is provably an exact signed-i32 (or
+/// safely-wrapping, see `MAX_ADDEND`) integer, so `lower_expr_as_i32` +
+/// unsigned bounds compare reproduces JS semantics exactly.
+pub(crate) fn index_is_exact_i32_shape(ctx: &FnCtx<'_>, index: &Expr) -> bool {
+    if let Some((lo, hi)) = crate::collectors::static_index_window(index) {
+        if lo >= 0 && hi <= i64::from(i32::MAX) {
+            return true;
+        }
+    }
+    match index {
+        Expr::Integer(n) => i32::try_from(*n).is_ok(),
+        Expr::Number(n) => {
+            n.is_finite()
+                && n.fract() == 0.0
+                && *n >= f64::from(i32::MIN)
+                && *n <= f64::from(i32::MAX)
+        }
+        // A canonical-i32 local IS a true signed i32 by construction (Phase 1
+        // slot rep) — including `U32`, whose bit pattern compares correctly
+        // under the unsigned bounds check when read BARE.
+        Expr::LocalGet(id) => ctx.local_slot_reps.contains_key(id),
+        Expr::Binary { op, left, right } if matches!(op, BinaryOp::Add) => {
+            match (left.as_ref(), right.as_ref()) {
+                (Expr::LocalGet(id), Expr::Integer(c)) | (Expr::Integer(c), Expr::LocalGet(id)) => {
+                    // SIGNED reps only: a `U32` local's value near 2^32 is a
+                    // NEGATIVE i32 bit pattern, and `+ c` can wrap it UP
+                    // through zero into a valid index (`bits(-1) + 2 == 1`)
+                    // while the true JS index (4294967297) must read
+                    // `undefined`. The signed wrap argument (`i32::MAX + c` →
+                    // negative → rejected by `icmp ult`) holds only for `I32`.
+                    matches!(ctx.local_slot_reps.get(id), Some(crate::expr::SlotRep::I32))
+                        && (0..=MAX_ADDEND).contains(c)
+                }
+                _ => false,
+            }
+        }
+        _ => false,
+    }
+}
+
+/// `true` when `id` is a proven-inline-storage integer-element view eligible
+/// as a checked-store receiver (`expr/proven_view_access` store tier and the
+/// masked-window region's proven store suffix).
+pub(crate) fn local_is_proven_int_store_view(ctx: &FnCtx<'_>, id: u32) -> bool {
+    // Mirror `proven_view_for`'s closure gate: a captured receiver could be
+    // reassigned between proof and access (also independently caught by the
+    // alias/scope downgrade, kept here for consistency).
+    if ctx.closure_captures.contains_key(&id) {
+        return false;
+    }
+    ctx.buffer_view_slots.get(&id).is_some_and(|view| {
+        view.storage_inline_proven
+            && view.native_owned.is_none()
+            && view.index_unit == BufferIndexUnit::Element
+            && view.alias.allows_noalias()
+            && view.scope_idx.is_some()
+            && matches!(
+                view.elem,
+                BufferElem::I8
+                    | BufferElem::U8
+                    | BufferElem::I16
+                    | BufferElem::U16
+                    | BufferElem::I32
+                    | BufferElem::U32
+            )
+    })
+}
+
+/// The proven view for `object`, when every gate for the checked tier holds.
+fn proven_view_for(
+    ctx: &FnCtx<'_>,
+    object: &Expr,
+    index: &Expr,
+) -> Option<(u32, crate::native_value::BufferViewSlot)> {
+    if ctx.disable_buffer_fast_path {
+        return None;
+    }
+    let Expr::LocalGet(id) = object else {
+        return None;
+    };
+    let view = ctx.buffer_view_slots.get(id)?.clone();
+    if !view.storage_inline_proven
+        || view.native_owned.is_some()
+        || view.index_unit != BufferIndexUnit::Element
+    {
+        return None;
+    }
+    // Downgrade marker: hazard paths clear `scope_idx` / demote `alias` when
+    // the tracked data pointer can no longer be trusted (reassignment
+    // refresh, aliasing, escapes). Mirror `lower_typed_array_load`'s gates so
+    // this tier can never read through a stale slot.
+    if !view.alias.allows_noalias() || view.scope_idx.is_none() {
+        return None;
+    }
+    // A closure-captured receiver can be reassigned between proof and access.
+    if ctx.closure_captures.contains_key(id) {
+        return None;
+    }
+    if !index_is_exact_i32_shape(ctx, index) {
+        return None;
+    }
+    if !can_lower_expr_as_i32(
+        index,
+        &ctx.i32_counter_slots,
+        ctx.flat_const_arrays,
+        &ctx.array_row_aliases,
+        ctx.integer_locals,
+        ctx.clamp3_functions,
+        ctx.clamp_u8_functions,
+        ctx.integer_returning_functions,
+        ctx.i32_identity_functions,
+    ) {
+        return None;
+    }
+    Some((*id, view))
+}
+
+/// Data pointer + entry-derived length for the proven view. The length load
+/// is `invariant` — a non-view typed array's length is immutable.
+fn load_data_and_len(
+    ctx: &mut FnCtx<'_>,
+    view: &crate::native_value::BufferViewSlot,
+) -> (String, String) {
+    let blk = ctx.block();
+    let data_ptr = blk.load(PTR, &view.data_slot);
+    let len = if let Some(length_slot) = view.length_slot.as_ref() {
+        blk.load(I32, length_slot)
+    } else {
+        let len_ptr = blk.gep(
+            I8,
+            &data_ptr,
+            &[(I32, &view.length_offset_from_data.to_string())],
+        );
+        blk.load_invariant(I32, &len_ptr)
+    };
+    (data_ptr, len)
+}
+
+fn elem_llvm_ty(elem: &BufferElem) -> crate::types::LlvmType {
+    match elem {
+        BufferElem::I8 | BufferElem::U8 | BufferElem::U8Clamped => I8,
+        BufferElem::I16 | BufferElem::U16 => I16,
+        BufferElem::I32 | BufferElem::U32 => I32,
+        BufferElem::F32 => F32,
+        BufferElem::F64 => DOUBLE,
+    }
+}
+
+/// Inline checked f64 element read (`object[index]` in a boxed/numeric
+/// context). Returns the DOUBLE SSA value: numeric element in-bounds,
+/// `TAG_UNDEFINED` OOB — bit-exact with `js_typed_array_get`.
+pub(crate) fn try_lower_proven_view_checked_f64_load(
+    ctx: &mut FnCtx<'_>,
+    object: &Expr,
+    index: &Expr,
+) -> Result<Option<String>> {
+    let Some((id, view)) = proven_view_for(ctx, object, index) else {
+        return Ok(None);
+    };
+    let idx_i32 = lower_expr_as_i32(ctx, index)?;
+    let (data_ptr, len) = load_data_and_len(ctx, &view);
+
+    let load_idx = ctx.new_block("pview.get.load");
+    let oob_idx = ctx.new_block("pview.get.oob");
+    let merge_idx = ctx.new_block("pview.get.merge");
+    let load_label = ctx.block_label(load_idx);
+    let oob_label = ctx.block_label(oob_idx);
+    let merge_label = ctx.block_label(merge_idx);
+
+    {
+        let blk = ctx.block();
+        // `ult` rejects negative / wrapped indices too (huge unsigned).
+        let in_bounds = blk.icmp_ult(I32, &idx_i32, &len);
+        blk.cond_br(&in_bounds, &load_label, &oob_label);
+    }
+
+    ctx.current_block = load_idx;
+    let (load_val, load_end) = {
+        let blk = ctx.block();
+        let idx_i64 = blk.zext(I32, &idx_i32, I64);
+        let byte_off = if view.element_width_bytes > 1 {
+            blk.shl(
+                I64,
+                &idx_i64,
+                &view.element_width_bytes.trailing_zeros().to_string(),
+            )
+        } else {
+            idx_i64
+        };
+        let elem_ptr = blk.gep(I8, &data_ptr, &[(I64, &byte_off)]);
+        let raw = blk.load(elem_llvm_ty(&view.elem), &elem_ptr);
+        let val = match view.elem {
+            BufferElem::I8 => blk.sitofp(I8, &raw, DOUBLE),
+            BufferElem::U8 | BufferElem::U8Clamped => blk.uitofp(I8, &raw, DOUBLE),
+            BufferElem::I16 => blk.sitofp(I16, &raw, DOUBLE),
+            BufferElem::U16 => blk.uitofp(I16, &raw, DOUBLE),
+            BufferElem::I32 => blk.sitofp(I32, &raw, DOUBLE),
+            BufferElem::U32 => blk.uitofp(I32, &raw, DOUBLE),
+            BufferElem::F32 => blk.fpext(F32, &raw, DOUBLE),
+            BufferElem::F64 => raw,
+        };
+        let end = blk.label.clone();
+        blk.br(&merge_label);
+        (val, end)
+    };
+
+    ctx.current_block = oob_idx;
+    let (oob_val, oob_end) = {
+        let blk = ctx.block();
+        let end = blk.label.clone();
+        blk.br(&merge_label);
+        (double_literal(f64::from_bits(TAG_UNDEFINED)), end)
+    };
+
+    ctx.current_block = merge_idx;
+    let result = ctx.block().phi(
+        DOUBLE,
+        &[
+            (load_val.as_str(), load_end.as_str()),
+            (oob_val.as_str(), oob_end.as_str()),
+        ],
+    );
+    let lowered = LoweredValue::js_value(result.clone());
+    ctx.record_lowered_value_with_access_mode(
+        "TypedArrayGet",
+        Some(id),
+        "TypedArrayGet.proven_view_checked",
+        &lowered,
+        Some(BoundsState::Unknown),
+        Some(view.alias.clone()),
+        Some(BufferAccessMode::CheckedNative),
+        None,
+        false,
+        false,
+        vec!["proven_view=checked_inline; guards=none".to_string()],
+    );
+    Ok(Some(result))
+}
+
+/// Inline checked element write (`object[index] = value`). The value is
+/// evaluated and coerced BEFORE the bounds check (spec order); an OOB write is
+/// a silent no-op. Returns the lowered (coerced-native) RHS so the assignment
+/// expression value matches the proven fast-store tier.
+pub(crate) fn try_lower_proven_view_checked_store(
+    ctx: &mut FnCtx<'_>,
+    object: &Expr,
+    index: &Expr,
+    value: &Expr,
+) -> Result<Option<LoweredValue>> {
+    let Some((id, view)) = proven_view_for(ctx, object, index) else {
+        return Ok(None);
+    };
+    // Same value-shape gates as `lower_typed_array_store`: integer kinds need
+    // a proven ToInt32-exact value, float kinds a proven number. U8Clamped
+    // stores keep the runtime clamping helper.
+    let int_kind = matches!(
+        view.elem,
+        BufferElem::I8
+            | BufferElem::U8
+            | BufferElem::I16
+            | BufferElem::U16
+            | BufferElem::I32
+            | BufferElem::U32
+    );
+    if matches!(view.elem, BufferElem::U8Clamped) {
+        return Ok(None);
+    }
+    // The ctx-free store gate misses proven typed-array-read operands
+    // (`r ^ P[17]`); the region-aware predicate is the crate's established
+    // "lowerable as exact i32 with ToInt32 semantics" contract and covers
+    // them (its IndexGet arm requires the same bounds proofs the unchecked
+    // load emitter does).
+    if int_kind
+        && !super::can_lower_integer_typed_array_store_value(ctx, value)
+        && !super::can_lower_expr_as_i32_in_current_region(ctx, value)
+    {
+        return Ok(None);
+    }
+    if matches!(view.elem, BufferElem::F32 | BufferElem::F64)
+        && !crate::type_analysis::is_numeric_expr(ctx, value)
+    {
+        return Ok(None);
+    }
+
+    let idx_i32 = lower_expr_as_i32(ctx, index)?;
+    let value_native = if int_kind {
+        let expected = if matches!(view.elem, BufferElem::U32) {
+            ExpectedNativeRep::U32
+        } else {
+            ExpectedNativeRep::I32
+        };
+        lower_expr_native(ctx, value, expected)?
+    } else {
+        lower_expr_native(ctx, value, ExpectedNativeRep::F64)?
+    };
+    let (data_ptr, len) = load_data_and_len(ctx, &view);
+
+    let store_idx = ctx.new_block("pview.set.store");
+    let done_idx = ctx.new_block("pview.set.done");
+    let store_label = ctx.block_label(store_idx);
+    let done_label = ctx.block_label(done_idx);
+
+    {
+        let blk = ctx.block();
+        let in_bounds = blk.icmp_ult(I32, &idx_i32, &len);
+        blk.cond_br(&in_bounds, &store_label, &done_label);
+    }
+
+    ctx.current_block = store_idx;
+    {
+        let blk = ctx.block();
+        let idx_i64 = blk.zext(I32, &idx_i32, I64);
+        let byte_off = if view.element_width_bytes > 1 {
+            blk.shl(
+                I64,
+                &idx_i64,
+                &view.element_width_bytes.trailing_zeros().to_string(),
+            )
+        } else {
+            idx_i64
+        };
+        let elem_ptr = blk.gep(I8, &data_ptr, &[(I64, &byte_off)]);
+        match view.elem {
+            BufferElem::I8 | BufferElem::U8 => {
+                let byte = blk.trunc(I32, &value_native.value, I8);
+                blk.store(I8, &byte, &elem_ptr);
+            }
+            BufferElem::I16 | BufferElem::U16 => {
+                let half = blk.trunc(I32, &value_native.value, I16);
+                blk.store(I16, &half, &elem_ptr);
+            }
+            BufferElem::I32 | BufferElem::U32 => {
+                blk.store(I32, &value_native.value, &elem_ptr);
+            }
+            BufferElem::F32 => {
+                let narrow = blk.fptrunc(DOUBLE, &value_native.value, F32);
+                blk.store(F32, &narrow, &elem_ptr);
+            }
+            BufferElem::F64 => {
+                blk.store(DOUBLE, &value_native.value, &elem_ptr);
+            }
+            BufferElem::U8Clamped => unreachable!("gated above"),
+        }
+        blk.br(&done_label);
+    }
+    ctx.current_block = done_idx;
+
+    ctx.record_lowered_value_with_access_mode(
+        "TypedArraySet",
+        Some(id),
+        "TypedArraySet.proven_view_checked",
+        &value_native,
+        Some(BoundsState::Unknown),
+        Some(view.alias.clone()),
+        Some(BufferAccessMode::CheckedNative),
+        None,
+        false,
+        false,
+        vec!["proven_view=checked_inline; guards=none".to_string()],
+    );
+    Ok(Some(value_native))
+}
diff --git a/crates/perry-codegen/src/expr/proxy_reflect.rs b/crates/perry-codegen/src/expr/proxy_reflect.rs
index 7aa7b4ec34..0af64c14cd 100644
--- a/crates/perry-codegen/src/expr/proxy_reflect.rs
+++ b/crates/perry-codegen/src/expr/proxy_reflect.rs
@@ -992,7 +992,27 @@ fn put_value_index_fast_path(ctx: &FnCtx<'_>, target: &Expr, key: &Expr, receive
         key,
         Expr::String(_) | Expr::WtfString(_) | Expr::SymbolFor(_)
     ) || is_string_expr(ctx, key);
-    recv_unknown && !key_is_static_string_or_symbol
+    // Representation-selection Phase 2: a receiver statically typed as a
+    // numeric typed array also belongs on `index_set::lower`'s typed-array
+    // arm — that file carries the proven-view / checked-native element-store
+    // tiers plus the same dynamic-key dispatcher this path would reach, so
+    // element writes on typed receivers (the spec-ABI `lr[off] = …` shape)
+    // stop routing through the generic write-IC.
+    let recv_typed_array = matches!(
+        crate::type_analysis::receiver_class_name(ctx, target).as_deref(),
+        Some(
+            "Int8Array"
+                | "Uint8Array"
+                | "Uint8ClampedArray"
+                | "Int16Array"
+                | "Uint16Array"
+                | "Int32Array"
+                | "Uint32Array"
+                | "Float32Array"
+                | "Float64Array"
+        )
+    );
+    (recv_unknown || recv_typed_array) && !key_is_static_string_or_symbol
 }
 
 fn try_lower_process_env_put_value_set(
diff --git a/crates/perry-codegen/src/expr/range_facts.rs b/crates/perry-codegen/src/expr/range_facts.rs
index 5d47d08a78..67930b4969 100644
--- a/crates/perry-codegen/src/expr/range_facts.rs
+++ b/crates/perry-codegen/src/expr/range_facts.rs
@@ -721,7 +721,16 @@ fn range_bounds_for_buffer_access(
     let Some(view) = ctx.buffer_view_slots.get(&buffer_local_id) else {
         return BoundsState::Unknown;
     };
-    let Some(index_range) = int_range_expr(ctx, index) else {
+    // Ctx-aware range facts first; fall back to the ctx-free syntactic window
+    // (`collectors::static_index_window`) — it proves the masked/shift index
+    // shapes (`x >>> 24`, `0x100 | (x & 0xff)`) for ANY operand, which the
+    // local-fact ranges cannot see for untyped/param-seeded values. Together
+    // with a constant-length view this turns the bcryptjs S-box reads into
+    // bare in-bounds loads.
+    let index_range = int_range_expr(ctx, index).or_else(|| {
+        crate::collectors::static_index_window(index).map(|(lo, hi)| IntRange { min: lo, max: hi })
+    });
+    let Some(index_range) = index_range else {
         return BoundsState::Unknown;
     };
     let Some(length_range) = view
diff --git a/crates/perry-codegen/src/expr/shadow_slot.rs b/crates/perry-codegen/src/expr/shadow_slot.rs
index 2d4149dd35..31cc27a714 100644
--- a/crates/perry-codegen/src/expr/shadow_slot.rs
+++ b/crates/perry-codegen/src/expr/shadow_slot.rs
@@ -60,6 +60,12 @@ pub(crate) fn emit_shadow_slot_clear(ctx: &mut FnCtx<'_>, slot_idx: u32) {
     if ctx.persistent_shadow_slots.contains(&slot_idx) {
         return;
     }
+    // Never-bound slot: it provably still holds its initial 0 (slots are only
+    // written through bind/set, and every value-set site binds first), so the
+    // clear would be a redundant `js_shadow_slot_set(idx, 0)` TLS hit.
+    if !ctx.shadow_slots_bound.contains(&slot_idx) {
+        return;
+    }
     // #6794 follow-up (b): the slot was already cleared to 0 for a currently
     // shadow-suppressed masked-window-region local, and suppression blocks every
     // subsequent write to it (`emit_shadow_slot_update_for_expr`), so it provably
@@ -103,6 +109,7 @@ pub(crate) fn enable_persistent_shadow_slot_for_array_alias(
     if !ctx.persistent_shadow_slots.insert(slot_idx) {
         return;
     }
+    ctx.shadow_slots_bound.insert(slot_idx);
     let slot_idx_string = slot_idx.to_string();
     ctx.func.entry_setup_call_void(
         "js_shadow_slot_bind",
@@ -120,6 +127,7 @@ pub(crate) fn emit_shadow_slot_bind_for_local(ctx: &mut FnCtx<'_>, local_id: u32
     let Some(local_slot) = ctx.locals.get(&local_id).cloned() else {
         return;
     };
+    ctx.shadow_slots_bound.insert(slot_idx);
     ctx.block().call_void(
         "js_shadow_slot_bind",
         &[(I32, &slot_idx.to_string()), (PTR, &local_slot)],
diff --git a/crates/perry-codegen/src/lower_call/func_ref.rs b/crates/perry-codegen/src/lower_call/func_ref.rs
index d676137851..6b833d4fe6 100644
--- a/crates/perry-codegen/src/lower_call/func_ref.rs
+++ b/crates/perry-codegen/src/lower_call/func_ref.rs
@@ -53,6 +53,229 @@ fn typed_i32_signature_note(arg_count: usize) -> String {
     }
 }
 
+/// Representation-selection Phase 2, Tier A: statically-proven dispatch to a
+/// specialized entry — direct call with raw args, no guard, no diamond, no
+/// phi. Every non-`Boxed` slot must be proven BY CONSTRUCTION at this exact
+/// call site (this check, not the collector, is the load-bearing soundness
+/// gate — a mismatch silently keeps today's boxed path):
+///
+/// - `I32` — integer literal in i32 range.
+/// - `F64` — numeric literal (bit-identical raw double).
+/// - `TaPtr` — `LocalGet` of a pre-pass-proven, never-reassigned,
+///   non-closure-referenced typed-array binding whose kind/const-len match
+///   the slot, whose top-level `Stmt::Let` has lowered in THIS body
+///   (`spec_ta_ready` — the dominance mirror), and which is not box-backed.
+///   All `TaPtr` args must be DISTINCT locals: distinct proven bindings are
+///   distinct fresh allocations, which is what justifies the entry's
+///   pairwise-noalias view slots.
+fn try_emit_spec_static_call(
+    ctx: &mut FnCtx<'_>,
+    fname: &str,
+    plan: &crate::codegen::SpecFnPlan,
+    args: &[Expr],
+    lowered: &[String],
+) -> Option<String> {
+    use crate::collectors::SpecParamRep;
+    if plan.reps.len() != args.len() || plan.reps.len() != lowered.len() {
+        return None;
+    }
+    // Per-slot proof + raw-arg plan (no IR emitted until every slot matches).
+    enum RawArg {
+        Double(usize),
+        I32Const(i64),
+        TaPtr(usize),
+    }
+    let mut raw_plan: Vec<RawArg> = Vec::with_capacity(args.len());
+    let mut ta_locals: Vec<u32> = Vec::new();
+    for (i, (rep, arg)) in plan.reps.iter().zip(args.iter()).enumerate() {
+        match rep {
+            SpecParamRep::Boxed => raw_plan.push(RawArg::Double(i)),
+            SpecParamRep::F64 => match arg {
+                Expr::Number(_) | Expr::Integer(_) => raw_plan.push(RawArg::Double(i)),
+                _ => return None,
+            },
+            SpecParamRep::I32 => match arg {
+                Expr::Integer(n) if i32::try_from(*n).is_ok() => {
+                    raw_plan.push(RawArg::I32Const(*n))
+                }
+                _ => return None,
+            },
+            SpecParamRep::TaPtr { kind, const_len } => {
+                let Expr::LocalGet(id) = arg else {
+                    return None;
+                };
+                let Some(binding) = ctx.spec_ta_bindings.get(id) else {
+                    return None;
+                };
+                if binding.kind != *kind
+                    || binding.const_len != *const_len
+                    || !ctx.spec_ta_ready.contains(id)
+                    || ctx.boxed_vars.contains(id)
+                    || ctx.prealloc_boxes.contains(id)
+                    || ctx.tdz_boxes.contains(id)
+                    || ta_locals.contains(id)
+                {
+                    return None;
+                }
+                ta_locals.push(*id);
+                raw_plan.push(RawArg::TaPtr(i));
+            }
+        }
+    }
+
+    let spec_name = crate::codegen::spec_function_name(fname, &plan.reps);
+    let mut raw_args_storage: Vec<(crate::types::LlvmType, String)> =
+        Vec::with_capacity(raw_plan.len());
+    for entry in &raw_plan {
+        match entry {
+            RawArg::Double(i) => raw_args_storage.push((DOUBLE, lowered[*i].clone())),
+            RawArg::I32Const(n) => raw_args_storage.push((I32, n.to_string())),
+            RawArg::TaPtr(i) => {
+                let blk = ctx.block();
+                let bits = blk.bitcast_double_to_i64(&lowered[*i]);
+                let raw = blk.and(I64, &bits, crate::nanbox::POINTER_MASK_I64);
+                raw_args_storage.push((I64, raw));
+            }
+        }
+    }
+    let call_args: Vec<(crate::types::LlvmType, &str)> = raw_args_storage
+        .iter()
+        .map(|(ty, v)| (*ty, v.as_str()))
+        .collect();
+    let result = ctx.block().call(DOUBLE, &spec_name, &call_args);
+    let tuple_note: Vec<String> = plan.reps.iter().map(|r| r.label()).collect();
+    ctx.record_lowered_value(
+        "Call",
+        None,
+        "spec_abi_static_call",
+        &LoweredValue::js_value(result.clone()),
+        None,
+        None,
+        None,
+        false,
+        false,
+        vec![
+            format!("spec_call=static; symbol={spec_name}"),
+            format!("tuple={}", tuple_note.join(",")),
+        ],
+    );
+    Some(result)
+}
+
+/// Phase 2, Tier B: declaration-proven reps keep the existing runtime-guarded
+/// diamond shape — guard each raw slot, call the specialized entry on the
+/// fast arm, the PUBLIC boxed body on the fallback arm, merge with a phi.
+fn try_emit_spec_guarded_call(
+    ctx: &mut FnCtx<'_>,
+    fname: &str,
+    plan: &crate::codegen::SpecFnPlan,
+    args: &[Expr],
+    lowered: &[String],
+) -> Option<String> {
+    use crate::collectors::SpecParamRep;
+    if plan.reps.len() != args.len() || plan.reps.len() != lowered.len() {
+        return None;
+    }
+    // Static filter first (same spirit as typed_param_reps_match_args): only
+    // sites whose args are statically i32-shaped take the guarded route.
+    for (rep, arg) in plan.reps.iter().zip(args.iter()) {
+        match rep {
+            SpecParamRep::I32 => {
+                if !is_i32_expr(ctx, arg) {
+                    return None;
+                }
+            }
+            SpecParamRep::Boxed => {}
+            // Declaration tuples only contain I32/Boxed slots in this phase.
+            _ => return None,
+        }
+    }
+
+    let spec_name = crate::codegen::spec_function_name(fname, &plan.reps);
+    let mut guard: Option<String> = None;
+    for (value, rep) in lowered.iter().zip(plan.reps.iter()) {
+        if !matches!(rep, SpecParamRep::I32) {
+            continue;
+        }
+        let ok = crate::codegen::emit_typed_arg_guard(
+            ctx.block(),
+            crate::codegen::TypedParamRep::I32,
+            value,
+        );
+        guard = Some(match guard {
+            Some(prev) => ctx.block().and(I1, &prev, &ok),
+            None => ok,
+        });
+    }
+    let fast_idx = ctx.new_block("spec_guarded_call.fast");
+    let fallback_idx = ctx.new_block("spec_guarded_call.fallback");
+    let merge_idx = ctx.new_block("spec_guarded_call.merge");
+    let fast_label = ctx.block_label(fast_idx);
+    let fallback_label = ctx.block_label(fallback_idx);
+    let merge_label = ctx.block_label(merge_idx);
+    if let Some(guard) = guard {
+        ctx.block().cond_br(&guard, &fast_label, &fallback_label);
+    } else {
+        ctx.block().br(&fast_label);
+    }
+
+    ctx.current_block = fast_idx;
+    let mut raw_storage: Vec<(crate::types::LlvmType, String)> = Vec::with_capacity(lowered.len());
+    for (value, rep) in lowered.iter().zip(plan.reps.iter()) {
+        match rep {
+            SpecParamRep::I32 => {
+                let raw = crate::codegen::emit_typed_arg_to_raw(
+                    ctx.block(),
+                    crate::codegen::TypedParamRep::I32,
+                    value,
+                );
+                raw_storage.push((I32, raw));
+            }
+            _ => raw_storage.push((DOUBLE, value.clone())),
+        }
+    }
+    let fast_args: Vec<(crate::types::LlvmType, &str)> = raw_storage
+        .iter()
+        .map(|(ty, v)| (*ty, v.as_str()))
+        .collect();
+    let fast_value = ctx.block().call(DOUBLE, &spec_name, &fast_args);
+    let after_fast = ctx.block().label.clone();
+    if !ctx.block().is_terminated() {
+        ctx.block().br(&merge_label);
+    }
+
+    ctx.current_block = fallback_idx;
+    let boxed_args: Vec<(crate::types::LlvmType, &str)> =
+        lowered.iter().map(|v| (DOUBLE, v.as_str())).collect();
+    let fallback_value = ctx.block().call(DOUBLE, fname, &boxed_args);
+    let after_fallback = ctx.block().label.clone();
+    if !ctx.block().is_terminated() {
+        ctx.block().br(&merge_label);
+    }
+
+    ctx.current_block = merge_idx;
+    let result = ctx.block().phi(
+        DOUBLE,
+        &[
+            (fast_value.as_str(), after_fast.as_str()),
+            (fallback_value.as_str(), after_fallback.as_str()),
+        ],
+    );
+    ctx.record_lowered_value(
+        "Call",
+        None,
+        "spec_abi_guarded_call",
+        &LoweredValue::js_value(result.clone()),
+        None,
+        None,
+        None,
+        false,
+        false,
+        vec![format!("spec_call=guarded; symbol={spec_name}")],
+    );
+    Some(result)
+}
+
 fn typed_signature_note(
     ret: &str,
     reps: &[crate::codegen::TypedParamRep],
@@ -282,6 +505,34 @@ pub fn try_lower_func_ref_call(
     } else {
         None
     };
+    // Representation-selection Phase 2: specialized-ABI dispatch. Tier A
+    // (static, guard-free) fires only when every slot's proof holds AT THIS
+    // SITE; Tier B keeps the guarded-diamond shape. Any mismatch falls
+    // through to the existing typed/generic chain — the public boxed entry is
+    // the permanent fallback ABI.
+    let spec_result: Option<String> = if crate::codegen::spec_abi_enabled()
+        && !resets_this
+        && !has_rest
+        && !ctx.func_synthetic_arguments.contains(fid)
+        && declared_count == args.len()
+    {
+        match ctx.spec_abi_functions.get(fid).cloned() {
+            Some(plan) => match plan.dispatch {
+                crate::codegen::SpecDispatch::Static => {
+                    try_emit_spec_static_call(ctx, &fname, &plan, args, &lowered)
+                }
+                crate::codegen::SpecDispatch::Guarded => {
+                    try_emit_spec_guarded_call(ctx, &fname, &plan, args, &lowered)
+                }
+            },
+            None => None,
+        }
+    } else {
+        None
+    };
+    // No `spec_result.is_none()` gate on the typed-clone candidate arms: plan
+    // selection makes the spec and typed-clone sets mutually exclusive, and
+    // the `if let` chain below consumes `spec_result` first anyway.
     let typed_f64_call_param_reps = if !resets_this
         && !has_rest
         && !ctx.func_synthetic_arguments.contains(fid)
@@ -334,7 +585,9 @@ pub fn try_lower_func_ref_call(
     } else {
         None
     };
-    let result = if let Some(reps) = typed_f64_call_param_reps {
+    let result = if let Some(spec) = spec_result {
+        spec
+    } else if let Some(reps) = typed_f64_call_param_reps {
         let typed_name = crate::codegen::typed_f64_function_name(&fname);
         let generic_body_name = crate::codegen::generic_function_body_name(&fname);
         let mut guard: Option<String> = None;
diff --git a/crates/perry-codegen/src/native_value/buffer.rs b/crates/perry-codegen/src/native_value/buffer.rs
index 9938df0539..4b0d8dd818 100644
--- a/crates/perry-codegen/src/native_value/buffer.rs
+++ b/crates/perry-codegen/src/native_value/buffer.rs
@@ -183,6 +183,15 @@ pub(crate) struct BufferViewSlot {
     pub alias: AliasState,
     pub length_source: Option<LengthSource>,
     pub native_owned: Option<NativeOwnedViewSlot>,
+    /// Representation-selection Phase 2: `true` when the receiver is PROVEN to
+    /// be a freshly-constructed inline-storage (non-view) typed array /
+    /// buffer — the construction form was a length or plain-array source,
+    /// never an `ArrayBuffer`. Such storage never moves (GC marks
+    /// `GC_TYPE_TYPED_ARRAY`/`GC_TYPE_BUFFER` non-movable), cannot be
+    /// detached, and its length is immutable, so the checked-native element
+    /// access tier (`expr/proven_view_access.rs`) may derive data/length from
+    /// the header with a plain bounds compare and NO kind/view guard.
+    pub storage_inline_proven: bool,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
diff --git a/crates/perry-codegen/src/runtime_decls/strings.rs b/crates/perry-codegen/src/runtime_decls/strings.rs
index c6b937c41a..96972267ea 100644
--- a/crates/perry-codegen/src/runtime_decls/strings.rs
+++ b/crates/perry-codegen/src/runtime_decls/strings.rs
@@ -126,6 +126,13 @@ pub fn declare_phase_b_strings(module: &mut LlModule) {
     module.declare_function("llvm.bswap.i16", I16, &[I16]);
     module.declare_function("llvm.bswap.i32", I32, &[I32]);
     module.declare_function("llvm.bswap.i64", I64, &[I64]);
+    // ARMv8.3 FEAT_JSCVT: spec-exact single-instruction ECMAScript ToInt32,
+    // emitted by `LlBlock::toint32_wrap` on apple-arm64 targets only (the
+    // declare is target-conditional — an aarch64 intrinsic in an x86 module
+    // would be rejected by the backend).
+    if crate::codegen::helpers::jscvt_enabled() {
+        module.declare_function("llvm.aarch64.fjcvtzs", I32, &[DOUBLE]);
+    }
     module.declare_function("llvm.memset.p0.i64", VOID, &[PTR, I8, I64, I1]);
     module.declare_function("llvm.memmove.p0.p0.i64", VOID, &[PTR, PTR, I64, I1]);
     // Keep js_math_pow for now — Math.pow has overflow / NaN
diff --git a/crates/perry-codegen/src/stmt/let_buffer_views.rs b/crates/perry-codegen/src/stmt/let_buffer_views.rs
new file mode 100644
index 0000000000..91c12c9f21
--- /dev/null
+++ b/crates/perry-codegen/src/stmt/let_buffer_views.rs
@@ -0,0 +1,324 @@
+//! Buffer/typed-array view-slot registration for `Stmt::Let` bindings.
+//! Mechanically extracted from `let_stmt.rs` (file-size gate); behavior
+//! unchanged. `pub(super)` — consumed only by the `stmt` module.
+
+use crate::expr::FnCtx;
+use crate::native_value::{
+    AliasState, BufferElem, BufferIndexUnit, BufferViewSlot, LengthSource, NativeOwnedViewSlot,
+};
+use crate::types::{I32, I64, I8, PTR};
+
+pub(super) struct BufferViewInit {
+    elem: BufferElem,
+    element_width_bytes: u32,
+    index_unit: BufferIndexUnit,
+    data_offset_bytes: i32,
+    length_offset_from_data: i32,
+    length_source: LengthSource,
+    native_owner_local_id: Option<u32>,
+    native_byte_offset: Option<i64>,
+    native_byte_length: Option<i64>,
+    /// See `BufferViewSlot::storage_inline_proven` — true only when the
+    /// construction form proves fresh inline (non-view) storage.
+    storage_inline_proven: bool,
+}
+
+pub(super) fn register_noalias_buffer_view(
+    ctx: &mut FnCtx<'_>,
+    id: u32,
+    init_expr: &perry_hir::Expr,
+    value: &str,
+) {
+    let Some(init) = buffer_view_init_for_expr(ctx, init_expr) else {
+        return;
+    };
+    let blk = ctx.block();
+    let handle = crate::expr::unbox_to_i64(blk, value);
+    let handle_ptr = blk.inttoptr(I64, &handle);
+    let data_ptr = if init.native_owner_local_id.is_some() {
+        // Arena views store a POINTER at `data_offset_bytes` (24) rather than
+        // inline data — load through it instead of gep-ing past it.
+        let data_field = blk.gep(
+            I8,
+            &handle_ptr,
+            &[(I32, &init.data_offset_bytes.to_string())],
+        );
+        blk.load(PTR, &data_field)
+    } else {
+        blk.gep(
+            I8,
+            &handle_ptr,
+            &[(I32, &init.data_offset_bytes.to_string())],
+        )
+    };
+    let data_slot = ctx.func.alloca_entry(PTR);
+    ctx.block().store(PTR, &data_ptr, &data_slot);
+    let length_slot = if init.native_owner_local_id.is_some() {
+        let len_field = ctx.block().gep(I8, &handle_ptr, &[(I32, "0")]);
+        let len_value = ctx.block().load(I32, &len_field);
+        let slot = ctx.func.alloca_entry(I32);
+        ctx.block().store(I32, &len_value, &slot);
+        Some(slot)
+    } else {
+        None
+    };
+    let scope_idx = ctx.buffer_alias_base + ctx.buffer_data_slots.len() as u32;
+    ctx.buffer_data_slots
+        .insert(id, (data_slot.clone(), scope_idx));
+    let native_owned = match init.native_owner_local_id {
+        Some(owner_local_id) => {
+            let owner_local_id = crate::expr::native_arena_canonical_owner_id(ctx, owner_local_id);
+            Some(NativeOwnedViewSlot {
+                owner_local_id,
+                byte_offset: init.native_byte_offset,
+                byte_length: init.native_byte_length,
+                owner_rooted: true,
+                disposed: false,
+                pointer_free_backing: true,
+            })
+        }
+        None => None,
+    };
+    ctx.buffer_view_slots.insert(
+        id,
+        BufferViewSlot {
+            data_slot,
+            length_slot,
+            scope_idx: Some(scope_idx),
+            elem: init.elem,
+            element_width_bytes: init.element_width_bytes,
+            index_unit: init.index_unit,
+            view_byte_offset: Some(0),
+            length_offset_from_data: init.length_offset_from_data,
+            alias: AliasState::NoAliasProven,
+            length_source: Some(init.length_source),
+            native_owned,
+            storage_inline_proven: init.storage_inline_proven,
+        },
+    );
+}
+
+/// A constructor argument that is a literal element count (or absent) proves
+/// fresh inline storage: the view form (`new TA(arrayBuffer)`) requires a
+/// pointer-valued argument, which a numeric literal can never be.
+pub(super) fn ctor_arg_is_literal_length(arg: Option<&perry_hir::Expr>) -> bool {
+    match arg {
+        None => true,
+        Some(perry_hir::Expr::Integer(_)) => true,
+        Some(perry_hir::Expr::Number(n)) => n.is_finite() && n.fract() == 0.0,
+        _ => false,
+    }
+}
+
+fn buffer_view_init_for_expr(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> Option<BufferViewInit> {
+    match expr {
+        perry_hir::Expr::NativeMethodCall {
+            module,
+            method,
+            object: None,
+            ..
+        } if module == "buffer" && method == "copyBytesFrom" => Some(BufferViewInit {
+            elem: BufferElem::U8,
+            element_width_bytes: 1,
+            index_unit: BufferIndexUnit::Byte,
+            data_offset_bytes: 8,
+            length_offset_from_data: -8,
+            length_source: buffer_alloc_length_source(ctx, expr),
+            native_owner_local_id: None,
+            native_byte_offset: None,
+            native_byte_length: None,
+            // copyBytesFrom always allocates a fresh inline buffer.
+            storage_inline_proven: true,
+        }),
+        perry_hir::Expr::BufferAlloc { .. } | perry_hir::Expr::BufferAllocUnsafe(_) => {
+            Some(BufferViewInit {
+                elem: BufferElem::U8,
+                element_width_bytes: 1,
+                index_unit: BufferIndexUnit::Byte,
+                data_offset_bytes: 8,
+                length_offset_from_data: -8,
+                length_source: buffer_alloc_length_source(ctx, expr),
+                native_owner_local_id: None,
+                native_byte_offset: None,
+                native_byte_length: None,
+                // Buffer.alloc/allocUnsafe always allocate fresh inline bytes.
+                storage_inline_proven: true,
+            })
+        }
+        perry_hir::Expr::Uint8ArrayNew(arg) => Some(BufferViewInit {
+            elem: BufferElem::U8,
+            element_width_bytes: 1,
+            index_unit: BufferIndexUnit::Byte,
+            data_offset_bytes: 8,
+            length_offset_from_data: -8,
+            length_source: buffer_alloc_length_source(ctx, expr),
+            native_owner_local_id: None,
+            native_byte_offset: None,
+            native_byte_length: None,
+            // `new Uint8Array(buffer)` is the VIEW form — only a literal
+            // length (or no argument) proves inline storage.
+            storage_inline_proven: ctor_arg_is_literal_length(arg.as_deref()),
+        }),
+        perry_hir::Expr::TypedArrayNew { kind, arg } => {
+            let (elem, width) = typed_array_elem_width_for_kind(*kind)?;
+            Some(BufferViewInit {
+                elem,
+                element_width_bytes: width,
+                index_unit: BufferIndexUnit::Element,
+                data_offset_bytes: 16,
+                length_offset_from_data: -16,
+                length_source: buffer_alloc_length_source(ctx, expr),
+                native_owner_local_id: None,
+                native_byte_offset: None,
+                native_byte_length: None,
+                // Same view-form hazard as Uint8ArrayNew: only a literal
+                // length proves the non-view construction here (the pre-pass
+                // proves the plain-array-source form separately for params).
+                storage_inline_proven: ctor_arg_is_literal_length(arg.as_deref()),
+            })
+        }
+        perry_hir::Expr::NativeArenaView {
+            owner,
+            kind,
+            byte_offset,
+            length,
+        } => {
+            let (elem, width) = typed_array_elem_width_for_kind(*kind)?;
+            let owner_local_id = match owner.as_ref() {
+                perry_hir::Expr::LocalGet(id) => Some(*id),
+                _ => None,
+            }?;
+            let byte_offset_const = const_i64_expr(byte_offset);
+            let length_const = const_i64_expr(length);
+            let native_byte_length = length_const.and_then(|len| len.checked_mul(width as i64));
+            Some(BufferViewInit {
+                elem,
+                element_width_bytes: width,
+                index_unit: BufferIndexUnit::Element,
+                data_offset_bytes: 24,
+                length_offset_from_data: 0,
+                length_source: length_source_from_expr(ctx, length)
+                    .unwrap_or(LengthSource::Unknown),
+                native_owner_local_id: Some(owner_local_id),
+                native_byte_offset: byte_offset_const,
+                native_byte_length,
+                // Arena views have their own owner/dispose lifecycle — never
+                // eligible for the proven checked tier.
+                storage_inline_proven: false,
+            })
+        }
+        _ => None,
+    }
+}
+
+fn typed_array_elem_width_for_kind(kind: u8) -> Option<(BufferElem, u32)> {
+    match kind {
+        perry_hir::TYPED_ARRAY_KIND_INT8 => Some((BufferElem::I8, 1)),
+        perry_hir::TYPED_ARRAY_KIND_UINT8 => Some((BufferElem::U8, 1)),
+        perry_hir::TYPED_ARRAY_KIND_UINT8_CLAMPED => Some((BufferElem::U8Clamped, 1)),
+        perry_hir::TYPED_ARRAY_KIND_INT16 => Some((BufferElem::I16, 2)),
+        perry_hir::TYPED_ARRAY_KIND_UINT16 => Some((BufferElem::U16, 2)),
+        perry_hir::TYPED_ARRAY_KIND_INT32 => Some((BufferElem::I32, 4)),
+        perry_hir::TYPED_ARRAY_KIND_UINT32 => Some((BufferElem::U32, 4)),
+        perry_hir::TYPED_ARRAY_KIND_FLOAT32 => Some((BufferElem::F32, 4)),
+        perry_hir::TYPED_ARRAY_KIND_FLOAT64 => Some((BufferElem::F64, 8)),
+        _ => None,
+    }
+}
+
+pub(super) fn math_min_length_buffer_ids(expr: &perry_hir::Expr) -> Option<Vec<u32>> {
+    let perry_hir::Expr::MathMin(args) = expr else {
+        return None;
+    };
+    if args.len() < 2 {
+        return None;
+    }
+    let mut out = Vec::new();
+    for arg in args {
+        if let Some(id) = length_of_local_buffer_id(arg) {
+            out.push(id);
+        } else {
+            return None;
+        }
+    }
+    out.sort_unstable();
+    out.dedup();
+    (!out.is_empty()).then_some(out)
+}
+
+fn length_of_local_buffer_id(expr: &perry_hir::Expr) -> Option<u32> {
+    match expr {
+        perry_hir::Expr::Uint8ArrayLength(inner) | perry_hir::Expr::BufferLength(inner) => {
+            match inner.as_ref() {
+                perry_hir::Expr::LocalGet(id) => Some(*id),
+                _ => None,
+            }
+        }
+        perry_hir::Expr::PropertyGet {
+            object, property, ..
+        } if property == "length" => match object.as_ref() {
+            perry_hir::Expr::LocalGet(id) => Some(*id),
+            _ => None,
+        },
+        _ => None,
+    }
+}
+
+fn buffer_alloc_length_source(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> LengthSource {
+    let len = match expr {
+        perry_hir::Expr::BufferAlloc { size, .. } => Some(size.as_ref()),
+        perry_hir::Expr::BufferAllocUnsafe(size) => Some(size.as_ref()),
+        perry_hir::Expr::Uint8ArrayNew(Some(size)) => Some(size.as_ref()),
+        perry_hir::Expr::TypedArrayNew {
+            arg: Some(size), ..
+        } => Some(size.as_ref()),
+        perry_hir::Expr::TypedArrayNew { arg: None, .. } => {
+            return LengthSource::Constant(0);
+        }
+        perry_hir::Expr::NativeMethodCall {
+            module,
+            method,
+            object: None,
+            ..
+        } if module == "buffer" && method == "copyBytesFrom" => None,
+        perry_hir::Expr::NativeArenaView { length, .. } => Some(length.as_ref()),
+        _ => None,
+    };
+    len.and_then(|expr| length_source_from_expr(ctx, expr))
+        .unwrap_or(LengthSource::Unknown)
+}
+
+fn const_i64_expr(expr: &perry_hir::Expr) -> Option<i64> {
+    match expr {
+        perry_hir::Expr::Integer(n) => Some(*n),
+        perry_hir::Expr::Number(n) if n.is_finite() && n.fract() == 0.0 => Some(*n as i64),
+        _ => None,
+    }
+}
+
+fn length_source_from_expr(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> Option<LengthSource> {
+    if let Some(range) = crate::expr::int_range_expr(ctx, expr) {
+        if range.min == range.max {
+            return Some(LengthSource::Constant(range.min));
+        }
+    }
+    match expr {
+        perry_hir::Expr::Integer(n) => Some(LengthSource::Constant(*n)),
+        perry_hir::Expr::LocalGet(id) => Some(LengthSource::Local { id: *id, addend: 0 }),
+        perry_hir::Expr::Binary {
+            op: perry_hir::BinaryOp::Add,
+            left,
+            right,
+        } => match (left.as_ref(), right.as_ref()) {
+            (perry_hir::Expr::LocalGet(id), perry_hir::Expr::Integer(addend))
+            | (perry_hir::Expr::Integer(addend), perry_hir::Expr::LocalGet(id)) => {
+                Some(LengthSource::Local {
+                    id: *id,
+                    addend: *addend,
+                })
+            }
+            _ => None,
+        },
+        _ => None,
+    }
+}
diff --git a/crates/perry-codegen/src/stmt/let_stmt.rs b/crates/perry-codegen/src/stmt/let_stmt.rs
index 2ba7e2622c..700ab8323d 100644
--- a/crates/perry-codegen/src/stmt/let_stmt.rs
+++ b/crates/perry-codegen/src/stmt/let_stmt.rs
@@ -2,6 +2,7 @@
 
 use super::*;
 
+use super::let_buffer_views::{math_min_length_buffer_ids, register_noalias_buffer_view};
 use super::unused_expr::lower_unused_expr;
 use crate::expr::{
     box_i1_for_compat_shadow, emit_root_nanbox_store_on_block,
@@ -9,9 +10,8 @@ use crate::expr::{
     lower_expr_with_expected_type, unbox_str_handle,
 };
 use crate::native_value::{
-    AliasState, BufferAccessMode, BufferElem, BufferIndexUnit, BufferViewSlot, LengthSource,
-    LoweredValue, MaterializationReason, NativeOwnedViewSlot, NativeRep, PodLayoutDecision,
-    PodLocal, SemanticKind,
+    BufferAccessMode, LoweredValue, MaterializationReason, NativeRep, PodLayoutDecision, PodLocal,
+    SemanticKind,
 };
 use crate::type_analysis::is_string_expr;
 use crate::types::{DOUBLE, I1, I32, I64, I8, PTR};
@@ -1127,6 +1127,44 @@ pub(crate) fn lower_let(
         }
         return Ok(());
     }
+    // Re-declaration of an already-canonical local: `var n, l = lr[off]`
+    // hoisting lowers as TWO `Stmt::Let`s for the same id (an `undefined`
+    // seed, then the real init). The first Let selected canonical-i32
+    // storage; the second must route its init into the SAME canonical slot —
+    // falling through to the plain path would allocate a double slot that
+    // shadows the canonical one (reads through `local_slot_reps` would see a
+    // stale 0). Mirrors the canonical branch's init lowering exactly.
+    if ctx.local_slot_reps.contains_key(&id) {
+        if let Some(init_expr) = init {
+            let i32_slots = ctx.i32_counter_slots.clone();
+            let flat_ca = ctx.flat_const_arrays.clone();
+            let ara = ctx.array_row_aliases.clone();
+            let int_locals = ctx.integer_locals.clone();
+            if crate::expr::can_lower_expr_as_i32(
+                init_expr,
+                &i32_slots,
+                &flat_ca,
+                &ara,
+                &int_locals,
+                ctx.clamp3_functions,
+                ctx.clamp_u8_functions,
+                ctx.integer_returning_functions,
+                ctx.i32_identity_functions,
+            ) {
+                let v_i32 = crate::expr::lower_expr_as_i32(ctx, init_expr)?;
+                let slot = ctx
+                    .i32_counter_slots
+                    .get(&id)
+                    .cloned()
+                    .expect("canonical local must have an i32 slot");
+                ctx.block().store(I32, &v_i32, &slot);
+            } else {
+                let v = lower_expr_with_expected_type(ctx, init_expr, Some(&refined_ty))?;
+                crate::expr::store_canonical_local_from_double(ctx, id, &v, Some(init_expr));
+            }
+        }
+        return Ok(());
+    }
     // Int32 eligibility (issue #48 / #436 / repsel Phase 1). Computed BEFORE
     // any storage is allocated so the canonical-i32 path can skip the double
     // slot entirely. See the block comments below (kept at their historical
@@ -1711,274 +1749,6 @@ fn buffer_local_alias_source(expr: &perry_hir::Expr) -> Option<u32> {
     }
 }
 
-struct BufferViewInit {
-    elem: BufferElem,
-    element_width_bytes: u32,
-    index_unit: BufferIndexUnit,
-    data_offset_bytes: i32,
-    length_offset_from_data: i32,
-    length_source: LengthSource,
-    native_owner_local_id: Option<u32>,
-    native_byte_offset: Option<i64>,
-    native_byte_length: Option<i64>,
-}
-
-fn register_noalias_buffer_view(
-    ctx: &mut FnCtx<'_>,
-    id: u32,
-    init_expr: &perry_hir::Expr,
-    value: &str,
-) {
-    let Some(init) = buffer_view_init_for_expr(ctx, init_expr) else {
-        return;
-    };
-    let blk = ctx.block();
-    let handle = crate::expr::unbox_to_i64(blk, value);
-    let handle_ptr = blk.inttoptr(I64, &handle);
-    let data_ptr = if init.native_owner_local_id.is_some() {
-        let data_field = blk.gep(I8, &handle_ptr, &[(I32, "24")]);
-        blk.load(PTR, &data_field)
-    } else {
-        blk.gep(
-            I8,
-            &handle_ptr,
-            &[(I32, &init.data_offset_bytes.to_string())],
-        )
-    };
-    let data_slot = ctx.func.alloca_entry(PTR);
-    ctx.block().store(PTR, &data_ptr, &data_slot);
-    let length_slot = if init.native_owner_local_id.is_some() {
-        let len_field = ctx.block().gep(I8, &handle_ptr, &[(I32, "0")]);
-        let len_value = ctx.block().load(I32, &len_field);
-        let slot = ctx.func.alloca_entry(I32);
-        ctx.block().store(I32, &len_value, &slot);
-        Some(slot)
-    } else {
-        None
-    };
-    let scope_idx = ctx.buffer_alias_base + ctx.buffer_data_slots.len() as u32;
-    ctx.buffer_data_slots
-        .insert(id, (data_slot.clone(), scope_idx));
-    let native_owned = match init.native_owner_local_id {
-        Some(owner_local_id) => {
-            let owner_local_id = crate::expr::native_arena_canonical_owner_id(ctx, owner_local_id);
-            Some(NativeOwnedViewSlot {
-                owner_local_id,
-                byte_offset: init.native_byte_offset,
-                byte_length: init.native_byte_length,
-                owner_rooted: true,
-                disposed: false,
-                pointer_free_backing: true,
-            })
-        }
-        None => None,
-    };
-    ctx.buffer_view_slots.insert(
-        id,
-        BufferViewSlot {
-            data_slot,
-            length_slot,
-            scope_idx: Some(scope_idx),
-            elem: init.elem,
-            element_width_bytes: init.element_width_bytes,
-            index_unit: init.index_unit,
-            view_byte_offset: Some(0),
-            length_offset_from_data: init.length_offset_from_data,
-            alias: AliasState::NoAliasProven,
-            length_source: Some(init.length_source),
-            native_owned,
-        },
-    );
-}
-
-fn buffer_view_init_for_expr(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> Option<BufferViewInit> {
-    match expr {
-        perry_hir::Expr::NativeMethodCall {
-            module,
-            method,
-            object: None,
-            ..
-        } if module == "buffer" && method == "copyBytesFrom" => Some(BufferViewInit {
-            elem: BufferElem::U8,
-            element_width_bytes: 1,
-            index_unit: BufferIndexUnit::Byte,
-            data_offset_bytes: 8,
-            length_offset_from_data: -8,
-            length_source: buffer_alloc_length_source(ctx, expr),
-            native_owner_local_id: None,
-            native_byte_offset: None,
-            native_byte_length: None,
-        }),
-        perry_hir::Expr::BufferAlloc { .. }
-        | perry_hir::Expr::BufferAllocUnsafe(_)
-        | perry_hir::Expr::Uint8ArrayNew(_) => Some(BufferViewInit {
-            elem: BufferElem::U8,
-            element_width_bytes: 1,
-            index_unit: BufferIndexUnit::Byte,
-            data_offset_bytes: 8,
-            length_offset_from_data: -8,
-            length_source: buffer_alloc_length_source(ctx, expr),
-            native_owner_local_id: None,
-            native_byte_offset: None,
-            native_byte_length: None,
-        }),
-        perry_hir::Expr::TypedArrayNew { kind, .. } => {
-            let (elem, width) = typed_array_elem_width_for_kind(*kind)?;
-            Some(BufferViewInit {
-                elem,
-                element_width_bytes: width,
-                index_unit: BufferIndexUnit::Element,
-                data_offset_bytes: 16,
-                length_offset_from_data: -16,
-                length_source: buffer_alloc_length_source(ctx, expr),
-                native_owner_local_id: None,
-                native_byte_offset: None,
-                native_byte_length: None,
-            })
-        }
-        perry_hir::Expr::NativeArenaView {
-            owner,
-            kind,
-            byte_offset,
-            length,
-        } => {
-            let (elem, width) = typed_array_elem_width_for_kind(*kind)?;
-            let owner_local_id = match owner.as_ref() {
-                perry_hir::Expr::LocalGet(id) => Some(*id),
-                _ => None,
-            }?;
-            let byte_offset_const = const_i64_expr(byte_offset);
-            let length_const = const_i64_expr(length);
-            let native_byte_length = length_const.and_then(|len| len.checked_mul(width as i64));
-            Some(BufferViewInit {
-                elem,
-                element_width_bytes: width,
-                index_unit: BufferIndexUnit::Element,
-                data_offset_bytes: 24,
-                length_offset_from_data: 0,
-                length_source: length_source_from_expr(ctx, length)
-                    .unwrap_or(LengthSource::Unknown),
-                native_owner_local_id: Some(owner_local_id),
-                native_byte_offset: byte_offset_const,
-                native_byte_length,
-            })
-        }
-        _ => None,
-    }
-}
-
-fn typed_array_elem_width_for_kind(kind: u8) -> Option<(BufferElem, u32)> {
-    match kind {
-        perry_hir::TYPED_ARRAY_KIND_INT8 => Some((BufferElem::I8, 1)),
-        perry_hir::TYPED_ARRAY_KIND_UINT8 => Some((BufferElem::U8, 1)),
-        perry_hir::TYPED_ARRAY_KIND_UINT8_CLAMPED => Some((BufferElem::U8Clamped, 1)),
-        perry_hir::TYPED_ARRAY_KIND_INT16 => Some((BufferElem::I16, 2)),
-        perry_hir::TYPED_ARRAY_KIND_UINT16 => Some((BufferElem::U16, 2)),
-        perry_hir::TYPED_ARRAY_KIND_INT32 => Some((BufferElem::I32, 4)),
-        perry_hir::TYPED_ARRAY_KIND_UINT32 => Some((BufferElem::U32, 4)),
-        perry_hir::TYPED_ARRAY_KIND_FLOAT32 => Some((BufferElem::F32, 4)),
-        perry_hir::TYPED_ARRAY_KIND_FLOAT64 => Some((BufferElem::F64, 8)),
-        _ => None,
-    }
-}
-
-fn math_min_length_buffer_ids(expr: &perry_hir::Expr) -> Option<Vec<u32>> {
-    let perry_hir::Expr::MathMin(args) = expr else {
-        return None;
-    };
-    if args.len() < 2 {
-        return None;
-    }
-    let mut out = Vec::new();
-    for arg in args {
-        if let Some(id) = length_of_local_buffer_id(arg) {
-            out.push(id);
-        } else {
-            return None;
-        }
-    }
-    out.sort_unstable();
-    out.dedup();
-    (!out.is_empty()).then_some(out)
-}
-
-fn length_of_local_buffer_id(expr: &perry_hir::Expr) -> Option<u32> {
-    match expr {
-        perry_hir::Expr::Uint8ArrayLength(inner) | perry_hir::Expr::BufferLength(inner) => {
-            match inner.as_ref() {
-                perry_hir::Expr::LocalGet(id) => Some(*id),
-                _ => None,
-            }
-        }
-        perry_hir::Expr::PropertyGet {
-            object, property, ..
-        } if property == "length" => match object.as_ref() {
-            perry_hir::Expr::LocalGet(id) => Some(*id),
-            _ => None,
-        },
-        _ => None,
-    }
-}
-
-fn buffer_alloc_length_source(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> LengthSource {
-    let len = match expr {
-        perry_hir::Expr::BufferAlloc { size, .. } => Some(size.as_ref()),
-        perry_hir::Expr::BufferAllocUnsafe(size) => Some(size.as_ref()),
-        perry_hir::Expr::Uint8ArrayNew(Some(size)) => Some(size.as_ref()),
-        perry_hir::Expr::TypedArrayNew {
-            arg: Some(size), ..
-        } => Some(size.as_ref()),
-        perry_hir::Expr::TypedArrayNew { arg: None, .. } => {
-            return LengthSource::Constant(0);
-        }
-        perry_hir::Expr::NativeMethodCall {
-            module,
-            method,
-            object: None,
-            ..
-        } if module == "buffer" && method == "copyBytesFrom" => None,
-        perry_hir::Expr::NativeArenaView { length, .. } => Some(length.as_ref()),
-        _ => None,
-    };
-    len.and_then(|expr| length_source_from_expr(ctx, expr))
-        .unwrap_or(LengthSource::Unknown)
-}
-
-fn const_i64_expr(expr: &perry_hir::Expr) -> Option<i64> {
-    match expr {
-        perry_hir::Expr::Integer(n) => Some(*n),
-        perry_hir::Expr::Number(n) if n.is_finite() && n.fract() == 0.0 => Some(*n as i64),
-        _ => None,
-    }
-}
-
-fn length_source_from_expr(ctx: &FnCtx<'_>, expr: &perry_hir::Expr) -> Option<LengthSource> {
-    if let Some(range) = crate::expr::int_range_expr(ctx, expr) {
-        if range.min == range.max {
-            return Some(LengthSource::Constant(range.min));
-        }
-    }
-    match expr {
-        perry_hir::Expr::Integer(n) => Some(LengthSource::Constant(*n)),
-        perry_hir::Expr::LocalGet(id) => Some(LengthSource::Local { id: *id, addend: 0 }),
-        perry_hir::Expr::Binary {
-            op: perry_hir::BinaryOp::Add,
-            left,
-            right,
-        } => match (left.as_ref(), right.as_ref()) {
-            (perry_hir::Expr::LocalGet(id), perry_hir::Expr::Integer(addend))
-            | (perry_hir::Expr::Integer(addend), perry_hir::Expr::LocalGet(id)) => {
-                Some(LengthSource::Local {
-                    id: *id,
-                    addend: *addend,
-                })
-            }
-            _ => None,
-        },
-        _ => None,
-    }
-}
-
 /// Extract all field names (parent chain + own) and the constructor for
 /// a class, cloning everything out of `ctx.classes` so the immutable
 /// borrow is released before the caller mutates `ctx`.
diff --git a/crates/perry-codegen/src/stmt/loops.rs b/crates/perry-codegen/src/stmt/loops.rs
index a414ea5abd..2434785617 100644
--- a/crates/perry-codegen/src/stmt/loops.rs
+++ b/crates/perry-codegen/src/stmt/loops.rs
@@ -895,7 +895,7 @@ fn record_packed_f64_range_access(
     entry.written |= written;
 }
 
-fn record_packed_f64_range_static_access(
+pub(super) fn record_packed_f64_range_static_access(
     accesses: &mut std::collections::BTreeMap<u32, PackedF64RangeArrayAccess>,
     array_id: u32,
     lo: i64,
diff --git a/crates/perry-codegen/src/stmt/masked_window_region.rs b/crates/perry-codegen/src/stmt/masked_window_region.rs
index ae2a5cdcae..557bc0e35f 100644
--- a/crates/perry-codegen/src/stmt/masked_window_region.rs
+++ b/crates/perry-codegen/src/stmt/masked_window_region.rs
@@ -44,7 +44,8 @@ use perry_hir::{Expr, Stmt};
 
 use super::loops::{
     local_is_number_array, local_is_untyped_candidate, packed_f64_range_loop_pure_expr_collect,
-    packed_loop_array_binding_storage_is_addressable, PackedF64RangeArrayAccess,
+    packed_loop_array_binding_storage_is_addressable, record_packed_f64_range_static_access,
+    PackedF64RangeArrayAccess,
 };
 use super::{emit_shadow_clears_after_stmt, lower_stmt};
 use crate::expr::{
@@ -68,6 +69,13 @@ pub(super) struct MaskedWindowRegionArray {
     /// Merged static window over every tracked read of this array.
     pub lo: i64,
     pub hi: i64,
+    /// Representation-selection Phase 2: the binding carries a
+    /// `storage_inline_proven` I32 `BufferViewSlot` whose CONSTANT length
+    /// covers the merged window — the ta_i32 classification is a compile-time
+    /// fact, so no runtime probe is needed for this array. When EVERY region
+    /// array is proven, the region lowers as a single guard-free fast copy
+    /// (no probes, no plain/slow copies, no branches).
+    pub proven_ta_i32: bool,
 }
 
 /// One scheduled fast-copy type refinement: after lowering the statement at
@@ -280,6 +288,105 @@ fn region_i32_bounded_write_locals(stmts: &[Stmt]) -> std::collections::HashSet<
     written
 }
 
+/// Phase 2: decompose a region-admissible proven-view element store —
+/// `IndexSet`/`PutValueSet` on a `storage_inline_proven` integer-element view
+/// receiver with an exact-i32 index shape. Element writes cannot rebind the
+/// receiver, resize it, or move its storage (non-view typed arrays are
+/// non-movable and non-detachable), and the checked-store lowering emits no
+/// calls, so the statement is safe inside every region copy.
+fn proven_view_store_parts<'e>(
+    ctx: &FnCtx<'_>,
+    expr: &'e Expr,
+) -> Option<(u32, &'e Expr, &'e Expr)> {
+    let (object, index, value) = match expr {
+        Expr::IndexSet {
+            object,
+            index,
+            value,
+        } => (object, index, value),
+        Expr::PutValueSet {
+            target,
+            key,
+            value,
+            receiver,
+            ..
+        } => {
+            let (Expr::LocalGet(t), Expr::LocalGet(r)) = (target.as_ref(), receiver.as_ref())
+            else {
+                return None;
+            };
+            if t != r {
+                return None;
+            }
+            (target, key, value)
+        }
+        _ => return None,
+    };
+    let Expr::LocalGet(id) = object.as_ref() else {
+        return None;
+    };
+    if !crate::expr::local_is_proven_int_store_view(ctx, *id) {
+        return None;
+    }
+    if !crate::expr::index_is_exact_i32_shape(ctx, index) {
+        return None;
+    }
+    Some((*id, index, value))
+}
+
+/// Ctx-aware operand collect for admitted proven-view stores: the same pure
+/// shapes as `packed_f64_range_loop_pure_expr_collect`, plus two ctx-backed
+/// index forms the ctx-free walk cannot see — a compile-time-constant index
+/// (`P[BLOWFISH_NUM_ROUNDS + 1]`, resolved through module-const folding) is a
+/// tracked single-element window, and an exact-i32 dynamic index on a proven
+/// inline view (`lr[off]`) is a pure UNTRACKED read (it lowers per-access
+/// through the checked tier in every copy).
+fn region_store_operand_collect(
+    ctx: &FnCtx<'_>,
+    expr: &Expr,
+    accesses: &mut std::collections::BTreeMap<u32, PackedF64RangeArrayAccess>,
+) -> bool {
+    match expr {
+        Expr::IndexGet { object, index } => {
+            let Expr::LocalGet(arr_id) = object.as_ref() else {
+                return false;
+            };
+            let window = crate::collectors::static_index_window(index).or_else(|| {
+                crate::expr::int_range_expr(ctx, index)
+                    .filter(|range| range.min == range.max)
+                    .map(|range| (range.min, range.max))
+            });
+            if let Some((lo, hi)) = window {
+                if lo < 0 || hi >= i64::from(i32::MAX) {
+                    return false;
+                }
+                if !region_store_operand_collect(ctx, index, accesses) {
+                    return false;
+                }
+                record_packed_f64_range_static_access(accesses, *arr_id, lo, hi);
+                return true;
+            }
+            crate::expr::local_is_proven_int_store_view(ctx, *arr_id)
+                && crate::expr::index_is_exact_i32_shape(ctx, index)
+                && region_store_operand_collect(ctx, index, accesses)
+        }
+        Expr::LocalGet(_)
+        | Expr::Number(_)
+        | Expr::Integer(_)
+        | Expr::Bool(_)
+        | Expr::Null
+        | Expr::Undefined => true,
+        Expr::Binary { left, right, .. } | Expr::Compare { left, right, .. } => {
+            region_store_operand_collect(ctx, left, accesses)
+                && region_store_operand_collect(ctx, right, accesses)
+        }
+        Expr::Unary { operand, .. } | Expr::NumberCoerce(operand) => {
+            region_store_operand_collect(ctx, operand, accesses)
+        }
+        _ => false,
+    }
+}
+
 /// Match a masked-window region starting at `stmts[0]`. Returns `None` when
 /// the run is too short, tracks no eligible array, or carries fewer than
 /// [`REGION_MIN_TRACKED_READS`] tracked reads.
@@ -293,6 +400,11 @@ pub(super) fn try_match_masked_window_region(
     let mut accesses: std::collections::BTreeMap<u32, PackedF64RangeArrayAccess> =
         std::collections::BTreeMap::new();
     let mut written: std::collections::HashSet<u32> = std::collections::HashSet::new();
+    // Phase 2: receivers of admitted proven-view element STORES. An element
+    // write never rebinds/resizes/moves a proven inline typed array, so such
+    // statements are region-safe — but a stored-to array must never be in the
+    // masked-READ eligible set (kept read-only).
+    let mut store_receivers: std::collections::HashSet<u32> = std::collections::HashSet::new();
     let mut len = 0usize;
     for stmt in stmts {
         let ok = match stmt {
@@ -316,6 +428,23 @@ pub(super) fn try_match_masked_window_region(
                 true
             }
             Stmt::Expr(expr) => {
+                if let Some((receiver_id, index, value)) = proven_view_store_parts(ctx, expr) {
+                    // Admit the store: its index/value sub-expressions are held
+                    // to the ctx-aware collect rule (their masked reads join
+                    // the tracked set — `lr[off] = r ^ P[K + 1]` tracks the
+                    // `P[...]` read, resolving `K` through compile-time
+                    // constants).
+                    let mut trial = accesses.clone();
+                    if region_store_operand_collect(ctx, index, &mut trial)
+                        && region_store_operand_collect(ctx, value, &mut trial)
+                    {
+                        accesses = trial;
+                        store_receivers.insert(receiver_id);
+                        len += 1;
+                        continue;
+                    }
+                    break;
+                }
                 let mut trial = accesses.clone();
                 if packed_f64_range_loop_pure_expr_collect(
                     expr,
@@ -344,8 +473,13 @@ pub(super) fn try_match_masked_window_region(
     for access in accesses.values() {
         // A binding written anywhere in the region (`S = T` rebinding, or a
         // tracked store) is dropped from the eligible set — its reads keep
-        // the ordinary per-access lowering in every copy.
-        if access.written || written.contains(&access.array_id) {
+        // the ordinary per-access lowering in every copy. Element-STORE
+        // receivers (admitted proven-view stores) are likewise kept out: the
+        // eligible read set stays read-only.
+        if access.written
+            || written.contains(&access.array_id)
+            || store_receivers.contains(&access.array_id)
+        {
             continue;
         }
         if access.counter.is_some() {
@@ -372,7 +506,31 @@ pub(super) fn try_match_masked_window_region(
         {
             continue;
         }
-        if !local_is_number_array(ctx, access.array_id)
+        // Phase 2 proven class: an inline-storage-proven Int32 view whose
+        // constant length covers the window classifies as ta_i32 at COMPILE
+        // time (kind fixed at construction, length immutable, storage
+        // non-movable, in-window reads in-bounds by arithmetic). Requires an
+        // undowngraded view (`allows_noalias` + `scope_idx`) exactly like the
+        // sibling proven tiers — hazard paths (closure capture, unknown-call
+        // escape, aliasing) clear those markers when the tracked data slot can
+        // no longer be trusted, and this tier emits NO runtime re-validation.
+        let proven_ta_i32 = ctx
+            .buffer_view_slots
+            .get(&access.array_id)
+            .is_some_and(|view| {
+                view.storage_inline_proven
+                    && view.native_owned.is_none()
+                    && view.alias.allows_noalias()
+                    && view.scope_idx.is_some()
+                    && view.index_unit == crate::native_value::BufferIndexUnit::Element
+                    && matches!(view.elem, crate::native_value::BufferElem::I32)
+                    && matches!(
+                        view.length_source,
+                        Some(crate::native_value::LengthSource::Constant(len)) if hi < len
+                    )
+            });
+        if !proven_ta_i32
+            && !local_is_number_array(ctx, access.array_id)
             && !local_is_untyped_candidate(ctx, access.array_id)
         {
             continue;
@@ -381,12 +539,25 @@ pub(super) fn try_match_masked_window_region(
             array_id: access.array_id,
             lo,
             hi,
+            proven_ta_i32,
         });
     }
     if arrays.is_empty() {
         return None;
     }
 
+    if std::env::var("PERRY_REPSEL_DEBUG").as_deref() == Ok("1") {
+        eprintln!(
+            "masked-region match in {}: len={} arrays={:?} stores={:?}",
+            ctx.source_function,
+            len,
+            arrays
+                .iter()
+                .map(|a| (a.array_id, a.lo, a.hi, a.proven_ta_i32))
+                .collect::<Vec<_>>(),
+            store_receivers
+        );
+    }
     let eligible: std::collections::HashSet<u32> =
         arrays.iter().map(|array| array.array_id).collect();
     let mut reads = 0usize;
@@ -672,6 +843,47 @@ pub(super) fn lower_masked_window_region(
     emit_shadow_clears: bool,
     region: &MaskedWindowRegion,
 ) -> Result<()> {
+    // Phase 2: when EVERY region array is compile-time-proven ta_i32 (spec-ABI
+    // `TaPtr` params, literal-length local views), the runtime classification
+    // is a foregone conclusion — emit ONE fast copy straight-line: no probe
+    // calls, no plain/slow copies, no branches, no merge. The data pointer
+    // comes from the entry-hoisted view slot (stable: typed-array storage
+    // never moves and the region admits no reassignment of the binding).
+    if region.arrays.iter().all(|array| array.proven_ta_i32) {
+        let ta_scope_id = ctx.next_loop_proof_scope_id();
+        for array in &region.arrays {
+            let view = ctx
+                .buffer_view_slots
+                .get(&array.array_id)
+                .cloned()
+                .expect("proven region array must have a view slot");
+            let data_ptr_val = ctx.block().load(crate::types::PTR, &view.data_slot);
+            let data_i64 = ctx.block().ptrtoint(&data_ptr_val, I64);
+            ctx.masked_window_array_facts.push(MaskedWindowArrayFact {
+                array_local_id: array.array_id,
+                scope_id: ta_scope_id,
+                guard_id: "masked_region_ta_i32_proven".to_string(),
+                min_idx: array.lo,
+                max_idx_exclusive: array.hi + 1,
+                values_i32: true,
+                elem: MaskedWindowElem::TaI32 { data_ptr: data_i64 },
+            });
+        }
+        let privatize = ctx.try_depth == 0;
+        let result = lower_region_copy(
+            ctx,
+            region_stmts,
+            base_idx,
+            emit_shadow_clears,
+            &region.refinements,
+            privatize,
+            true,
+        );
+        ctx.masked_window_array_facts
+            .retain(|fact| fact.scope_id != ta_scope_id);
+        return result;
+    }
+
     let ta_pre_idx = ctx.new_block("masked_region.ta_i32.preheader");
     let try_plain_idx = ctx.new_block("masked_region.try_plain");
     let plain_pre_idx = ctx.new_block("masked_region.plain_f64.preheader");
diff --git a/crates/perry-codegen/src/stmt/mod.rs b/crates/perry-codegen/src/stmt/mod.rs
index 81ad41ad6e..7885e33520 100644
--- a/crates/perry-codegen/src/stmt/mod.rs
+++ b/crates/perry-codegen/src/stmt/mod.rs
@@ -12,6 +12,7 @@ use crate::native_value::{LoweredValue, MaterializationReason};
 use crate::types::DOUBLE;
 
 mod if_stmt;
+mod let_buffer_views;
 mod let_stmt;
 mod loops;
 mod masked_window_region;
@@ -203,6 +204,19 @@ fn lower_stmts_inner(ctx: &mut FnCtx<'_>, stmts: &[Stmt], emit_shadow_clears: bo
             continue;
         }
         lower_stmt(ctx, &stmts[i])?;
+        // Representation-selection Phase 2: a TOP-LEVEL `Stmt::Let` of a
+        // pre-pass-proven typed-array binding makes the binding "ready" — the
+        // dominance mirror of the collector's sequential judgment. Later call
+        // sites (at any nesting below later top-level statements, but never
+        // inside closures, which get their own empty set) may then match the
+        // binding against a `TaPtr` slot. Nested Lets never insert.
+        if emit_shadow_clears {
+            if let Stmt::Let { id, .. } = &stmts[i] {
+                if ctx.spec_ta_bindings.contains_key(id) {
+                    ctx.spec_ta_ready.insert(*id);
+                }
+            }
+        }
         // If an earlier statement already terminated the current block
         // (e.g. return in a straight-line sequence), any following statement
         // would emit dead code. Anvil silently drops these at the block
diff --git a/crates/perry-codegen/tests/native_proof_buffer_views.rs b/crates/perry-codegen/tests/native_proof_buffer_views.rs
index 6c827940cb..3b312f218a 100644
--- a/crates/perry-codegen/tests/native_proof_buffer_views.rs
+++ b/crates/perry-codegen/tests/native_proof_buffer_views.rs
@@ -1935,13 +1935,29 @@ fn reassigned_typed_array_store_records_runtime_fallback() {
         }),
         "expected reassigned typed-array store to record runtime fallback:\n{artifact:#}"
     );
+    // The read must never take an UNCHECKED native path on a reassigned
+    // receiver. Two conforming lowerings exist: the runtime-call fallback
+    // (`slow_path` / dynamic_fallback) and, since #6883, the inline
+    // kind-GUARDED checked read (`checked_f64_param` / checked_native) —
+    // whose runtime guard re-validates the receiver on every access, so a
+    // reassignment can never serve stale data. What this asserts is the
+    // absence of the guard-free proven/unchecked forms.
     assert!(
         records.iter().any(|record| {
             record["expr_kind"] == "TypedArrayGet"
-                && record["consumer"] == "TypedArrayGet.slow_path"
-                && record["access_mode"] == "dynamic_fallback"
-                && !record["fallback_reason"].is_null()
+                && ((record["consumer"] == "TypedArrayGet.slow_path"
+                    && record["access_mode"] == "dynamic_fallback")
+                    || (record["consumer"] == "TypedArrayGet.checked_f64_param"
+                        && record["access_mode"] == "checked_native"))
+        }),
+        "expected reassigned typed-array read to stay on a runtime-checked path:\n{artifact:#}"
+    );
+    assert!(
+        !records.iter().any(|record| {
+            record["expr_kind"] == "TypedArrayGet"
+                && (record["consumer"] == "TypedArrayGet.proven_view_checked"
+                    || record["access_mode"] == "unchecked_native")
         }),
-        "expected reassigned typed-array read to record runtime fallback:\n{artifact:#}"
+        "reassigned typed-array read must never take a proven/unchecked form:\n{artifact:#}"
     );
 }
diff --git a/crates/perry/src/commands/compile/object_cache.rs b/crates/perry/src/commands/compile/object_cache.rs
index 5f4af42122..555a0b8676 100644
--- a/crates/perry/src/commands/compile/object_cache.rs
+++ b/crates/perry/src/commands/compile/object_cache.rs
@@ -970,6 +970,24 @@ fn compute_object_cache_key_with_env(
             .as_deref()
             .unwrap_or(""),
     );
+    // Representation-selection Phase 2 — specialized calling convention:
+    // `PERRY_SPECIALIZED_ABI=0/off/false` removes the specialized entries and
+    // their static/guarded dispatch sites; `PERRY_SPECIALIZED_ABI_MAX`
+    // changes which functions get an entry. Both change emitted IR / .o
+    // bytes — an unkeyed flag would make A/B arms silently share objects.
+    h.field(
+        "env_specialized_abi",
+        env_var("PERRY_SPECIALIZED_ABI").as_deref().unwrap_or(""),
+    );
+    h.field(
+        "env_specialized_abi_max",
+        env_var("PERRY_SPECIALIZED_ABI_MAX")
+            .as_deref()
+            .unwrap_or(""),
+    );
+    // FEAT_JSCVT ToInt32 (`fjcvtzs` on apple-arm64): flipping it changes
+    // every `toint32_wrap` emission site's IR, so it must key the cache.
+    h.field("env_jscvt", env_var("PERRY_JSCVT").as_deref().unwrap_or(""));
 
     h.finish()
 }
diff --git a/crates/perry/src/commands/compile/object_cache/object_cache_tests.rs b/crates/perry/src/commands/compile/object_cache/object_cache_tests.rs
index 1e33a4d95b..38e9c3e358 100644
--- a/crates/perry/src/commands/compile/object_cache/object_cache_tests.rs
+++ b/crates/perry/src/commands/compile/object_cache/object_cache_tests.rs
@@ -617,6 +617,11 @@ fn key_changes_with_codegen_env_vars() {
         "PERRY_INT_VALUED_LOCALS",
         // Representation-selection Phase 1: canonical unboxed i32 locals.
         "PERRY_CANONICAL_I32_LOCALS",
+        // Representation-selection Phase 2: specialized calling convention.
+        "PERRY_SPECIALIZED_ABI",
+        "PERRY_SPECIALIZED_ABI_MAX",
+        // FEAT_JSCVT single-instruction ToInt32 (apple-arm64).
+        "PERRY_JSCVT",
     ] {
         // Sample state without the var, with the var, and with a different
         // value — all three keys must be distinct.
diff --git a/docs/representation-selection-rfc.md b/docs/representation-selection-rfc.md
index cac98c71de..09ac426e1d 100644
--- a/docs/representation-selection-rfc.md
+++ b/docs/representation-selection-rfc.md
@@ -136,9 +136,13 @@ Functions are specialized on the **representation tuple** of (params, return):
 - **Specialization key** = the representation tuple. Entries are **cached/deduplicated per key** —
   all call sites proving the same tuple share one specialized body.
 - **Budgets:** per-function specialization count cap (start: 2 — boxed + one dominant tuple) and a
-  module-wide code-size budget; monitored by the existing `binary-size` CI check. When a budget is
-  exceeded, additional call sites route to the **boxed entry** (always present, always correct).
-  Cold/polymorphic callers never specialize.
+  module-wide entry cap (`PERRY_SPECIALIZED_ABI_MAX`, default 64). When a budget is exceeded,
+  additional call sites route to the **boxed entry** (always present, always correct).
+  Cold/polymorphic callers never specialize. Anti-bloat is proven **empirically**: the
+  `binary-size` CI job measures the COMPILER binary, not user output, so it cannot see
+  monomorphization bloat — instead, a large real corpus is compiled with the flag on vs. off
+  (`PERRY_SPECIALIZED_ABI=0`, object cache cleared between arms) and the emitted binaries must be
+  within ~1% of each other.
 - The boxed entry is the permanent fallback ABI; specialization is purely additive.
 
 ### 5.5 Boundary transitions
@@ -244,7 +248,8 @@ is not load-luck.
   acceptance contracts (§5.5) must throw/route, never coerce. The central correctness burden —
   §5.2's barrier list is the checklist.
 - **Compile-time cost** of interprocedural inference (summaries, caching, on-demand analysis).
-- **Code size** from monomorphization (bounded by §5.4 budgets + `binary-size` CI).
+- **Code size** from monomorphization (bounded by §5.4 budgets; proven by the flag-on/off
+  emitted-binary corpus measurement — the `binary-size` CI job only sees the compiler itself).
 - **GC complexity:** pointer reps under a moving collector (§5.6) — the rebase-after-safepoint
   contract must be enforced mechanically (a lint/verifier pass over region-local derived pointers).
 - **Scope:** Perry's single largest architectural line — HIR, type system, codegen, ABI, GC, object
diff --git a/test-files/test_gap_specabi_polymorphic_coexist.ts b/test-files/test_gap_specabi_polymorphic_coexist.ts
new file mode 100644
index 0000000000..358ea0e0c5
--- /dev/null
+++ b/test-files/test_gap_specabi_polymorphic_coexist.ts
@@ -0,0 +1,42 @@
+// Representation-selection Phase 2 (spec-ABI) routing: statically-proven call
+// sites may take the specialized raw-ABI entry while polymorphic/unproven
+// sites keep the boxed public path — every route must produce Node-identical
+// output, including an out-of-bounds write through the specialized entry
+// (silent no-op) and a differently-shaped typed-array site (tuple mismatch →
+// boxed fallback).
+function mix(t: any, o: any, a: any, b: any) {
+  let x = t[o];
+  x ^= a[0];
+  x += a[1];
+  x ^= b[x & 3];
+  t[o] = x;
+  t[o + 1] = (x >>> 3) | 0;
+  return t;
+}
+
+const T = new Int32Array(4);
+const A = new Int32Array([0x1234, 7]);
+const B = new Int32Array([11, 22, 33, 44]);
+T[0] = 0x0f0f0f0f | 0;
+for (let i = 0; i < 1000; i++) mix(T, 0, A, B);
+console.log("proven:", T[0] | 0, T[1] | 0, T[2] | 0, T[3] | 0);
+
+// Same proven shape, but the trailing write lands out of bounds (o+1 == 4):
+// an OOB typed-array store is a silent no-op on every route.
+mix(T, 3, A, B);
+console.log("oob-write:", T[0] | 0, T[1] | 0, T[2] | 0, T[3] | 0);
+
+// Polymorphic site: plain arrays through the very same function.
+const t2: any = [9, 8, 7, 6];
+const a2: any = [5, 6];
+const b2: any = [1, 1, 1, 1];
+mix(t2, 0, a2, b2);
+console.log("poly:", t2[0], t2[1], t2[2], t2[3]);
+
+// Differently-shaped typed-array site (length 1): tuple mismatch keeps the
+// boxed path; reading t[5] yields undefined, so x goes NaN and the stores
+// coerce it to 0.
+const small = new Int32Array(1);
+small[0] = 123;
+mix(small, 5, A, B);
+console.log("mismatch:", small[0] | 0);
diff --git a/test-files/test_gap_specabi_reassign.ts b/test-files/test_gap_specabi_reassign.ts
new file mode 100644
index 0000000000..cd49236570
--- /dev/null
+++ b/test-files/test_gap_specabi_reassign.ts
@@ -0,0 +1,20 @@
+// Spec-ABI soundness: a reassigned binding must never prove TaPtr — after
+// `P = ...`, every call must observe the NEW value through the boxed path.
+function first(a: any) {
+  return a[0];
+}
+
+let P = new Int32Array(4);
+P[0] = 42;
+console.log("before:", first(P));
+
+P = new Int32Array([7, 8]);
+console.log("after:", first(P));
+
+// NOTE: reassigning P to a PLAIN array (`P = [99]`) trips the pre-existing
+// declared-type staleness bug tracked as #6906 (reads through the reassigned
+// binding return undefined), independent of the spec-ABI routing this test
+// gates — kept out so the test can gate on the routing property.
+P = new Int32Array(1);
+P[0] = 99;
+console.log("third:", first(P), P.length);
diff --git a/test-files/test_gap_specabi_recursion_escape.ts b/test-files/test_gap_specabi_recursion_escape.ts
new file mode 100644
index 0000000000..407daa9e31
--- /dev/null
+++ b/test-files/test_gap_specabi_recursion_escape.ts
@@ -0,0 +1,23 @@
+// Spec-ABI routing: a recursive function may specialize for its proven outer
+// site while the recursive inner site (unproven args) keeps the boxed path;
+// a function reference escaping as a VALUE (`const g = fill`) goes through
+// the closure wrapper, which only ever calls the public boxed symbol.
+// All routes must agree with Node byte-for-byte.
+function fill(t: any, i: any, v: any): any {
+  if (i >= 4) return t;
+  t[i] = v ^ (i << 2);
+  return fill(t, i + 1, v);
+}
+
+const T = new Int32Array(4);
+fill(T, 0, 5);
+console.log("direct:", T[0] | 0, T[1] | 0, T[2] | 0, T[3] | 0);
+
+const g = fill;
+const T2 = new Int32Array(4);
+g(T2, 0, 9);
+console.log("escaped:", T2[0] | 0, T2[1] | 0, T2[2] | 0, T2[3] | 0);
+
+// The returned value is the same typed array (identity through the boxed
+// return path).
+console.log("identity:", fill(T, 4, 0) === T);
diff --git a/test-files/test_gap_specabi_view_detach.ts b/test-files/test_gap_specabi_view_detach.ts
new file mode 100644
index 0000000000..31dc325f2f
--- /dev/null
+++ b/test-files/test_gap_specabi_view_detach.ts
@@ -0,0 +1,29 @@
+// Spec-ABI soundness: a typed array created in VIEW form
+// (`new Int32Array(buffer)`) must never take the guard-free specialized
+// entry — its storage belongs to an ArrayBuffer that can be detached by
+// `buffer.transfer()`. Outputs must stay byte-exact before and after detach.
+function sum3(a: any) {
+  let s = 0;
+  s += a[0];
+  s += a[1];
+  s += a[2];
+  return s;
+}
+
+const P = new Int32Array(3);
+P[0] = 10;
+P[1] = 20;
+P[2] = 30;
+console.log("inline:", sum3(P));
+
+const buf = new ArrayBuffer(12);
+const V = new Int32Array(buf);
+V[0] = 1;
+V[1] = 2;
+V[2] = 3;
+console.log("view:", sum3(V));
+
+const moved = buf.transfer();
+// Detached view: every element read is undefined, so the sum is NaN.
+console.log("detached:", sum3(V));
+console.log("byteLength:", buf.byteLength, moved.byteLength);