fix(codegen): restore native ABI evidence proofs

benchmarks/compiler_output/workloads.toml

@@ -1439,7 +1439,13 @@ equals = "width_aware_buffer_kernels:38314632556\n"
 detail = "width-aware buffer and typed-array semantic checksum"
 
 [workloads.width_aware_buffer_kernels.native_rep_checks]
-allow_materialization_reasons = ["function_abi", "runtime_api", "unknown_alias", "unknown_bounds"]
+allow_materialization_reasons = [
+  "function_abi",
+  "runtime_api",
+  "unknown_alias",
+  "unknown_bounds",
+  "unknown_call_escape",
+]
 
 [[workloads.width_aware_buffer_kernels.native_rep_checks.require_records]]
 name = "buffer_read_u32_be"
@@ -1523,14 +1529,14 @@ notes_contains = "typed_array_fallback=untracked_or_unproven"
 min = 2
 
 [[workloads.width_aware_buffer_kernels.native_rep_checks.require_records]]
-name = "typed_array_bounds_get_fallback"
+name = "typed_array_unproven_get_fallback"
 source_function = "typedArrayHazards"
 expr_kind = "TypedArrayGet"
 consumer = "TypedArrayGet.slow_path"
 native_rep_name = "js_value"
 access_mode = "dynamic_fallback"
 bounds_state = "unknown"
-materialization_reason = "unknown_bounds"
+materialization_reason = "unknown_call_escape"
 notes_contains = "typed_array_fallback=untracked_or_unproven"
 
 [[workloads.width_aware_buffer_kernels.native_rep_checks.require_records]]
@@ -1545,17 +1551,6 @@ materialization_reason = "unknown_alias"
 notes_contains = "typed_array_fallback=untracked_or_unproven"
 min = 2
 
-[[workloads.width_aware_buffer_kernels.native_rep_checks.require_records]]
-name = "typed_array_bounds_set_fallback"
-source_function = "typedArrayHazards"
-expr_kind = "TypedArraySet"
-consumer = "TypedArraySet.slow_path"
-native_rep_name = "js_value"
-access_mode = "dynamic_fallback"
-bounds_state = "unknown"
-materialization_reason = "unknown_bounds"
-notes_contains = "typed_array_fallback=untracked_or_unproven"
-
 [workloads.native_owned_typed_views]
 source = "benchmarks/compiler_output/fixtures/native_owned_typed_views.ts"
 kind = "native_owned_typed_views"
@@ -1892,10 +1887,27 @@ kind = "native_abi_packet_typed"
 allow_hot_loop_conversions = true
 allow_dynamic_property_runtime = true
 allowed_hot_loop_runtime_calls = [
+  "js_dynamic_string_or_number_add",
+  "js_number_coerce",
   "js_shadow_frame_push",
   "js_shadow_slot_bind",
 ]
 
+# #8094's public trampoline contains a guarded specialized clone and the
+# semantics-preserving generic fallback. LLVM may inline both into the public
+# symbol, so the global hot-loop census legitimately sees dynamic helpers from
+# the fallback. Pin the actual optimization contract on the pre-opt clone: its
+# successful-guard body must remain free of those helpers (#8225).
+[[workloads.native_abi_packet_typed.ir_checks]]
+name = "packet_typed_specialized_clone_has_no_dynamic_numeric_helpers"
+section = "llvm_before"
+function_contains = "$spec_"
+regex_none = [
+  "call double @js_dynamic_string_or_number_add",
+  "call double @js_number_coerce",
+]
+detail = "the guarded typed-packet clone keeps numeric additions native while the generic fallback preserves erased-annotation semantics"
+
 [workloads.native_abi_packet_typed.vectorization]
 min_vectorized_loops = 0
 scalar_baseline = "allowed: packet evidence compares typed ABI shape against the boxed/control packet"

changelog.d/8302-native-abi-evidence-proofs.md

@@ -0,0 +1,22 @@
+### Fixed
+
+- Restored native ABI evidence for compiler-owned Buffer, typed-array, arena,
+  POD-layout, and packed numeric-array values. Buffer numeric reads now retain
+  stable pointer facts (including `native_u32`), while optimized native paths
+  stay distinct from semantics-preserving erased-annotation fallbacks.
+
+  The failure came from runtime-derived identities being dropped after
+  TypeScript annotation trust was tightened: constructor facts were not carried
+  through `crates/perry-codegen/src/codegen/module_globals_emit.rs` and
+  `crates/perry-codegen/src/type_analysis/refine.rs`, Buffer numeric reads in
+  `crates/perry-codegen/src/lower_call/buffer_intrinsic.rs` did not attach their
+  view facts, and `crates/perry-codegen/src/collectors/ptr_shape_numeric.rs` did
+  not recognize native-view or POD-layout values as Number-producing. The repair
+  preserves those facts while explicitly excluding BigInt-backed typed arrays
+  and retaining guarded array stores. Regression coverage in
+  `crates/perry-codegen/tests/native_proof_buffer_views.rs`,
+  `crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs`, and
+  `tests/test_native_abi_contract.sh` verifies the restored `u32`/`f32` records,
+  native numeric additions, BigInt mixed-add dispatch, and the full native-ABI
+  contract; the native ABI compiler-output suite validates the optimized and
+  fallback IR gates.

crates/perry-codegen/src/codegen/module_globals_emit.rs

@@ -46,6 +46,26 @@ fn module_global_runtime_type(
         Expr::String(_) | Expr::WtfString(_) | Expr::I18nString { .. } | Expr::TypeOf(_) => {
             Some(Type::String)
         }
+        // Compiler-owned allocation HIR establishes these runtime classes
+        // independently of the erased binding annotation. Keep module-global
+        // facts aligned with `proven_type_from_init`; otherwise a value that
+        // becomes global only because a helper references it loses the same
+        // constructor proof that a function-local binding retains (#8225).
+        Expr::BufferAlloc { .. } | Expr::BufferAllocUnsafe(_) => {
+            Some(Type::Named("Buffer".to_string()))
+        }
+        Expr::Uint8ArrayNew(_) | Expr::Uint8ArrayFrom(_) => {
+            Some(Type::Named("Uint8Array".to_string()))
+        }
+        Expr::TypedArrayNew { kind, .. } | Expr::NativeArenaView { kind, .. } => {
+            super::spec_abi::spec_ta_kind_class_name(*kind)
+                .map(|class| Type::Named(class.to_string()))
+        }
+        Expr::NativeArenaAlloc(_) => Some(Type::Named("NativeArenaOwner".to_string())),
+        Expr::NativePodView {
+            view_type: Some(view_type),
+            ..
+        } => Some(view_type.clone()),
         Expr::New { class_name, .. }
             if class_name == "SharedArrayBuffer" && shared_array_buffer_is_intrinsic =>
         {

crates/perry-codegen/src/collectors/ptr_shape.rs

@@ -1945,7 +1945,13 @@ pub(in crate::collectors) use numeric::collect_numeric_by_construction_locals as
 /// Conservative "cannot be a BigInt" for the spec Number-path argument.
 fn expr_provably_not_bigint(e: &Expr, not_bigint_locals: &HashSet<u32>) -> bool {
     match e {
-        Expr::Number(_) | Expr::Integer(_) | Expr::String(_) | Expr::Bool(_) => true,
+        Expr::Number(_)
+        | Expr::Integer(_)
+        | Expr::String(_)
+        | Expr::Bool(_)
+        | Expr::PodLayoutSizeOf { .. }
+        | Expr::PodLayoutAlignOf { .. }
+        | Expr::PodLayoutOffsetOf { .. } => true,
         Expr::LocalGet(id) => not_bigint_locals.contains(id),
         Expr::Unary { op, operand } => match op {
             perry_hir::UnaryOp::Pos => true, // `+x` throws for BigInt

crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs

@@ -688,6 +688,50 @@ fn numeric_accumulator_is_numeric_by_construction() {
     assert!(numeric_locals_of(&stmts).contains(&3));
 }
 
+#[test]
+fn bigint_typed_view_addition_is_not_numeric_by_construction() {
+    for (offset, kind) in [
+        perry_hir::TYPED_ARRAY_KIND_BIGINT64,
+        perry_hir::TYPED_ARRAY_KIND_BIGUINT64,
+    ]
+    .into_iter()
+    .enumerate()
+    {
+        let view_id = 30 + offset as u32 * 2;
+        let sum_id = view_id + 1;
+        let stmts = vec![
+            Stmt::Let {
+                id: view_id,
+                name: format!("bigint_view_{offset}"),
+                ty: Type::Any,
+                mutable: false,
+                init: Some(Expr::TypedArrayNew {
+                    kind,
+                    arg: Some(Box::new(Expr::Integer(1))),
+                }),
+            },
+            Stmt::Let {
+                id: sum_id,
+                name: format!("mixed_sum_{offset}"),
+                ty: Type::Any,
+                mutable: false,
+                init: Some(Expr::Binary {
+                    op: BinaryOp::Add,
+                    left: Box::new(Expr::IndexGet {
+                        object: Box::new(Expr::LocalGet(view_id)),
+                        index: Box::new(Expr::Integer(0)),
+                    }),
+                    right: Box::new(Expr::Integer(1)),
+                }),
+            },
+        ];
+        assert!(
+            !numeric_locals_of(&stmts).contains(&sum_id),
+            "BigInt typed-array reads must retain mixed-addition TypeError semantics"
+        );
+    }
+}
+
 /// The poisons, one per rule: a no-init `Let` (undefined until assigned), a
 /// string write anywhere, a boxed id, and a param-like id with no `Let`.
 #[test]

crates/perry-codegen/src/collectors/ptr_shape_numeric.rs

@@ -437,6 +437,18 @@ pub(in crate::collectors) fn collect_numeric_by_construction_locals<'a>(
     let mut writes: HashMap<u32, Vec<Option<&'a Expr>>> = HashMap::new();
     let mut let_bound: HashSet<u32> = HashSet::new();
     super::super::not_bigint_locals::collect_writes(stmts, &mut writes, &mut let_bound);
+    // The standalone #8105 consumer does not run the Ptr<Shape> provenance
+    // walk that normally supplies `const_local_inits`. Reconstruct the same
+    // safe fact from the shared exhaustive write set: one initialized write
+    // means the binding's value is stable even when its source spelling was
+    // `let`. This lets the Add proof inspect compiler-owned typed-view
+    // constructors without trusting their erased annotation.
+    let mut stable_local_inits = const_local_inits.clone();
+    for (&id, local_writes) in &writes {
+        if let [Some(init)] = local_writes.as_slice() {
+            stable_local_inits.entry(id).or_insert(Some(*init));
+        }
+    }
     let empty_members: HashSet<u32> = HashSet::new();
     let empty_fields: HashSet<String> = HashSet::new();
     let mut numeric: HashSet<u32> = let_bound
@@ -457,7 +469,7 @@ pub(in crate::collectors) fn collect_numeric_by_construction_locals<'a>(
                             &empty_members,
                             &empty_fields,
                             not_bigint_locals,
-                            const_local_inits,
+                            &stable_local_inits,
                             &numeric,
                             0,
                         ),
@@ -511,8 +523,63 @@ pub(super) fn expr_numeric_by_construction(
             depth + 1,
         )
     };
+    // A numeric index into one of these compiler-owned constructors can only
+    // produce a Number or `undefined` (for an out-of-bounds read). Either is
+    // safe on one side of `+` once the other operand has the same property:
+    // neither operand can select string concatenation, and ToNumber(undefined)
+    // produces the Number NaN. Keep this weaker fact local to the Add rule;
+    // an out-of-bounds read is not itself a Number and must not become a
+    // general raw-f64 proof.
+    let numeric_view_value_or_undefined = |x: &Expr| {
+        let Expr::IndexGet { object, index } = x else {
+            return false;
+        };
+        let Expr::LocalGet(view_id) = object.as_ref() else {
+            return false;
+        };
+        let Some(Some(init)) = const_local_inits.get(view_id) else {
+            return false;
+        };
+        let number_valued_typed_array_kind = |kind: u8| {
+            matches!(
+                kind,
+                perry_hir::TYPED_ARRAY_KIND_INT8
+                    | perry_hir::TYPED_ARRAY_KIND_UINT8
+                    | perry_hir::TYPED_ARRAY_KIND_UINT8_CLAMPED
+                    | perry_hir::TYPED_ARRAY_KIND_INT16
+                    | perry_hir::TYPED_ARRAY_KIND_UINT16
+                    | perry_hir::TYPED_ARRAY_KIND_INT32
+                    | perry_hir::TYPED_ARRAY_KIND_UINT32
+                    | perry_hir::TYPED_ARRAY_KIND_FLOAT16
+                    | perry_hir::TYPED_ARRAY_KIND_FLOAT32
+                    | perry_hir::TYPED_ARRAY_KIND_FLOAT64
+            )
+        };
+        let numeric_storage = matches!(
+            init,
+            Expr::BufferAlloc { .. }
+                | Expr::BufferAllocUnsafe(_)
+                | Expr::Uint8ArrayNew(_)
+                | Expr::Uint8ArrayFrom(_)
+        ) || matches!(
+            init,
+            Expr::TypedArrayNew { kind, .. } | Expr::NativeArenaView { kind, .. }
+                if number_valued_typed_array_kind(*kind)
+        ) || matches!(
+            init,
+            Expr::Array(elements)
+                if elements
+                    .iter()
+                    .all(|element| matches!(element, Expr::Integer(_) | Expr::Number(_)))
+        );
+        numeric_storage && rec(index)
+    };
     match e {
-        Expr::Number(_) | Expr::Integer(_) => true,
+        Expr::Number(_)
+        | Expr::Integer(_)
+        | Expr::PodLayoutSizeOf { .. }
+        | Expr::PodLayoutAlignOf { .. }
+        | Expr::PodLayoutOffsetOf { .. } => true,
         Expr::Unary { op, operand } => match op {
             perry_hir::UnaryOp::Neg | perry_hir::UnaryOp::Pos | perry_hir::UnaryOp::BitNot => {
                 rec(operand)
@@ -521,7 +588,10 @@ pub(super) fn expr_numeric_by_construction(
         },
         Expr::Binary { op, left, right } => match op {
             // `+` concatenates strings; both sides must be numbers.
-            BinaryOp::Add => rec(left) && rec(right),
+            BinaryOp::Add => {
+                (rec(left) || numeric_view_value_or_undefined(left))
+                    && (rec(right) || numeric_view_value_or_undefined(right))
+            }
             // `- * / %` produce a BigInt only for BigInt⊗BigInt; mixing a
             // BigInt with anything else THROWS (no value is stored). ONE
             // provably-non-BigInt operand therefore forces the completed

crates/perry-codegen/src/lower_call/buffer_intrinsic.rs

@@ -8,7 +8,7 @@
 use anyhow::Result;
 use perry_hir::Expr;
 
-use crate::expr::{access_facts_for_spec, BufferAccessSpec, FnCtx};
+use crate::expr::{access_facts_for_spec, attach_buffer_view_facts, BufferAccessSpec, FnCtx};
 use crate::native_value::{BufferEndian, LoweredValue};
 use crate::types::{F32, I32};
 
@@ -479,6 +479,7 @@ pub(super) fn try_emit_buffer_read_intrinsic(
         proof.may_emit_noalias,
         vec![format!("width_bytes={}", spec.width_bytes)],
     );
+    attach_buffer_view_facts(ctx, &proof.view);
     let result_consumer = match result.rep.name() {
         "i32" => "BufferNumericRead.native_i32",
         "u32" => "BufferNumericRead.native_u32",
@@ -506,6 +507,7 @@ pub(super) fn try_emit_buffer_read_intrinsic(
             format!("endian={:?}", spec.endian),
         ],
     );
+    attach_buffer_view_facts(ctx, &proof.view);
     Ok(Some(result))
 }
 

crates/perry-codegen/src/native_value/buffer.rs

@@ -16,6 +16,26 @@ pub(crate) enum BufferElem {
     F64,
 }
 
+impl BufferElem {
+    /// Whether an indexed read produces a JavaScript Number. Keep this
+    /// exhaustive so adding a BigInt-backed element representation cannot
+    /// silently broaden numeric-expression proofs.
+    pub(crate) fn is_number_valued(&self) -> bool {
+        matches!(
+            self,
+            Self::I8
+                | Self::U8
+                | Self::U8Clamped
+                | Self::I16
+                | Self::U16
+                | Self::I32
+                | Self::U32
+                | Self::F32
+                | Self::F64
+        )
+    }
+}
+
 #[derive(Debug, Clone, Copy, Serialize, PartialEq, Eq)]
 #[serde(rename_all = "snake_case")]
 pub(crate) enum BufferIndexUnit {

crates/perry-codegen/src/type_analysis/numeric.rs

@@ -425,6 +425,20 @@ pub(crate) fn is_numeric_expr(ctx: &FnCtx<'_>, e: &Expr) -> bool {
             let Expr::LocalGet(arr_id) = object.as_ref() else {
                 return false;
             };
+            if ctx.native_facts.num_array_local(*arr_id).is_some() {
+                return true;
+            }
+            // #8225: tracked BufferViewSlots come from compiler-owned
+            // Buffer/typed-array constructors (including NativeArena views),
+            // and every representable element kind is numeric. This runtime
+            // fact is stronger than the erasable declaration consulted below.
+            if ctx
+                .buffer_view_slots
+                .get(arr_id)
+                .is_some_and(|view| view.elem.is_number_valued())
+            {
+                return true;
+            }
             match ctx.stable_local_type_proof(arr_id) {
                 Some(HirType::Array(elem)) => {
                     matches!(**elem, HirType::Number | HirType::Int32)

crates/perry-codegen/src/type_analysis/pod.rs

@@ -555,6 +555,23 @@ pub(crate) fn numeric_proof_is_declared_only(ctx: &FnCtx<'_>, expr: &Expr) -> bo
                 if crate::expr::masked_window_fact_for_index(ctx, *arr_id, index).is_some() {
                     return false;
                 }
+                if ctx.native_facts.num_array_local(*arr_id).is_some() {
+                    return false;
+                }
+                // #8225: a live BufferViewSlot is compiler-owned runtime
+                // evidence for a typed-array/buffer representation. Its
+                // element load cannot produce a string: the checked slow arm
+                // is at worst `undefined` (coerced separately when needed),
+                // while a proven native-owned access is a raw numeric load.
+                // Do not discard that stronger fact and reclassify the read
+                // from its erasable source annotation.
+                if ctx
+                    .buffer_view_slots
+                    .get(arr_id)
+                    .is_some_and(|view| view.elem.is_number_valued())
+                {
+                    return false;
+                }
             }
             // A typed array's storage is native bytes — a non-numeric store is
             // converted on the way in, so the read cannot surface one.