From 71c2cdbaf2977eeb4611efe99fa3722ba0d58018 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 17 Aug 2026 09:56:14 +0200 Subject: [PATCH 1/3] fix(codegen): restore native ABI evidence proofs --- benchmarks/compiler_output/workloads.toml | 112 +++++++++--------- .../src/codegen/module_globals_emit.rs | 20 ++++ .../src/collectors/ptr_numarray.rs | 46 +++++-- .../perry-codegen/src/collectors/ptr_shape.rs | 8 +- .../src/collectors/ptr_shape_numeric.rs | 59 ++++++++- .../src/lower_call/buffer_intrinsic.rs | 4 +- .../src/type_analysis/numeric.rs | 10 ++ crates/perry-codegen/src/type_analysis/pod.rs | 13 ++ .../perry-codegen/src/type_analysis/refine.rs | 21 ++++ .../tests/native_proof_buffer_views.rs | 53 +++++++++ tests/test_native_abi_contract.sh | 23 +++- 11 files changed, 289 insertions(+), 80 deletions(-) diff --git a/benchmarks/compiler_output/workloads.toml b/benchmarks/compiler_output/workloads.toml index b64bbbe5a8..63e1383df1 100644 --- a/benchmarks/compiler_output/workloads.toml +++ b/benchmarks/compiler_output/workloads.toml @@ -402,7 +402,11 @@ detail = "buffer_slow_path_calls" [workloads.h1_native_rep_equivalence] source = "benchmarks/compiler_output/fixtures/h1_native_rep_equivalence.ts" kind = "native_rep" -allowed_hot_loop_runtime_calls = ["js_gc_loop_safepoint"] +# The erased-annotation body remains the permanent semantics path. Buffer +# parameters cannot reuse the typed-array-header specialized ABI: Buffer's +# object layout is distinct even though indexed storage is byte-addressable. +allow_dynamic_property_runtime = true +allowed_hot_loop_runtime_calls = ["js_gc_loop_safepoint", "js_uint8array_set"] [workloads.h1_native_rep_equivalence.vectorization] min_vectorized_loops = 0 @@ -428,7 +432,8 @@ gc_collections_traced = 0 write_barriers_static = 1 write_barriers_traced = 0 boxed_number_allocations_static = 0 -buffer_slow_path_accesses_static = 0 +# One set helper each in the public body, wrapper, and the call-site inline. +buffer_slow_path_accesses_static = 3 [[workloads.h1_native_rep_equivalence.ir_checks]] name = "h1_i32_phi_path" @@ -447,11 +452,11 @@ regex_none = ["@js_buffer_get", "@js_buffer_set"] detail = "positive H1 fixture has no generic JS buffer helpers" [[workloads.h1_native_rep_equivalence.counter_checks]] -name = "h1_no_buffer_slow_path" +name = "h1_generic_fallback_slow_path_budget" section = "llvm_after" counter = "buffer_slow_path_calls" -equals = 0 -detail = "buffer_slow_path_calls" +equals = 3 +detail = "Buffer-parameter body/wrapper/call-site keep exactly three fallback set sites" [[workloads.h1_native_rep_equivalence.named_regions]] name = "direct_bounded" @@ -501,7 +506,9 @@ no_conversions = true [[workloads.h1_native_rep_equivalence.named_regions.selectors]] function_contains = "main" label_any = ["for.body.2.i"] -counter_min = { load_i8 = 1, store_i8 = 1 } +# The Buffer parameter's erased runtime class still proves the raw read and +# loop bounds; the write remains on the semantics-preserving runtime fallback. +counter_min = { load_i8 = 1 } [workloads.h1_buffer_fastpath_bench] source = "benchmarks/compiler_output/fixtures/h1_buffer_fastpath_bench.ts" @@ -751,9 +758,9 @@ rejected_fact_state = "invalidated" rejected_fact_reason = "runtime_api" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_set_fast_f64" -expr_kind = "NumericArrayIndexSet" -consumer = "js_array_numeric_set_f64_unboxed" +name = "numeric_array_literal_get_fast_f64" +expr_kind = "NumArrayIndexGet" +consumer = "ptr_numarray.guard_free_load" native_rep_name = "f64" access_mode = "checked_native" bounds_state = "proven_or_guarded" @@ -761,47 +768,24 @@ consumed_fact_kind = "raw_f64_layout" consumed_fact_state = "consumed" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_set_guard_consumed" -expr_kind = "NumericArrayIndexSet" -consumer = "js_array_numeric_set_f64_unboxed" +name = "numeric_array_literal_set_fast_f64" +expr_kind = "NumArrayIndexSet" +consumer = "ptr_numarray.guard_free_store" native_rep_name = "f64" access_mode = "checked_native" bounds_state = "proven_or_guarded" -consumed_fact_kind = "bounds" +consumed_fact_kind = "raw_f64_layout" consumed_fact_state = "consumed" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_set_dynamic_fallback" -expr_kind = "NumericArrayIndexSet" -consumer_contains = "fallback" -access_mode = "dynamic_fallback" -materialization_reason = "runtime_api" -fallback_reason = "runtime_api" -rejected_fact_kind = "raw_f64_layout" -rejected_fact_state = "rejected" -rejected_fact_reason = "runtime_api" - -[[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_set_dynamic_fallback_invalidates_layout" -expr_kind = "NumericArrayIndexSet" -consumer_contains = "fallback" -access_mode = "dynamic_fallback" -materialization_reason = "runtime_api" -fallback_reason = "runtime_api" -rejected_fact_kind = "raw_f64_layout" -rejected_fact_state = "invalidated" -rejected_fact_reason = "runtime_api" - -[[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_set_materialization_hazard_invalidated" -expr_kind = "NumericArrayIndexSet" -consumer_contains = "fallback" -access_mode = "dynamic_fallback" -materialization_reason = "runtime_api" -fallback_reason = "runtime_api" -rejected_fact_kind = "materialization_hazard" -rejected_fact_state = "invalidated" -rejected_fact_reason = "runtime_api" +name = "numeric_array_literal_set_bounds_consumed" +expr_kind = "NumArrayIndexSet" +consumer = "ptr_numarray.guard_free_store" +native_rep_name = "f64" +access_mode = "checked_native" +bounds_state = "proven_or_guarded" +consumed_fact_kind = "bounds" +consumed_fact_state = "consumed" [workloads.packed_f64_loop_versioning] source = "benchmarks/compiler_output/fixtures/packed_f64_loop_versioning.ts" @@ -1439,7 +1423,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 +1513,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 +1535,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 +1871,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" diff --git a/crates/perry-codegen/src/codegen/module_globals_emit.rs b/crates/perry-codegen/src/codegen/module_globals_emit.rs index 51eb5f3f52..93188fdeb7 100644 --- a/crates/perry-codegen/src/codegen/module_globals_emit.rs +++ b/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 => { diff --git a/crates/perry-codegen/src/collectors/ptr_numarray.rs b/crates/perry-codegen/src/collectors/ptr_numarray.rs index 9e40bb5b20..09ce8f5962 100644 --- a/crates/perry-codegen/src/collectors/ptr_numarray.rs +++ b/crates/perry-codegen/src/collectors/ptr_numarray.rs @@ -4,7 +4,7 @@ //! //! ## What this proves //! -//! A function-local `let a = new Array(n)` / `let a: number[] = []` qualifies +//! A function-local `let a = new Array(n)` / numeric array literal qualifies //! as a **numeric-array pointer local** when static analysis proves that for //! the local's entire lifetime: //! @@ -24,9 +24,9 @@ //! * **Provenance**: the local is initialized by exactly one `Stmt::Let` whose //! init is `new Array()` (runtime hole-fills every slot, sets //! `GC_ARRAY_RAW_F64_HOLES`, and stamps the pointer-free GC layout — -//! `js_array_constructor_single`) or an EMPTY array literal `[]` (length 0; -//! nothing to observe until a numeric push). Density: `new Array(n)` ⇒ -//! `HolesOK`; `[]` ⇒ `Dense`. +//! `js_array_constructor_single`) or an all-numeric array literal (the +//! literal classifier allocates packed raw-f64 storage). Density: +//! `new Array(n)` ⇒ `HolesOK`; a numeric literal ⇒ `Dense`. //! * **Containment**: every use of the local is an element read, an element //! write whose VALUE is numeric-by-construction (a non-number store would //! break invariant 1 — such a local is disqualified outright, not just @@ -412,12 +412,20 @@ impl<'a> UseWalk<'a> { }), _ => None, }, - // Empty array literal: length 0, nothing to observe until a - // (numeric-only, by containment) push. - Expr::Array(elems) if elems.is_empty() => Some(NumArrayLocal { - density: NumArrayDensity::Dense, - proven_initial_length: 0, - }), + // All-numeric literals allocate packed raw-f64 storage. The use + // walk below proves every later write remains numeric, so a + // non-empty literal has the same Dense invariant as `[]` rather + // than needing the guarded tier to rediscover its layout (#8225). + Expr::Array(elems) + if elems + .iter() + .all(|elem| matches!(elem, Expr::Integer(_) | Expr::Number(_))) => + { + Some(NumArrayLocal { + density: NumArrayDensity::Dense, + proven_initial_length: elems.len() as i64, + }) + } _ => None, } } @@ -1002,7 +1010,7 @@ mod tests { } #[test] - fn promotes_alloc_and_empty_literal_provenance() { + fn promotes_alloc_and_numeric_literal_provenance() { let alloc = collect(&[ alloc_let(8), Stmt::Expr(index_set(ARR, Expr::Integer(0), Expr::Number(1.5))), @@ -1018,6 +1026,17 @@ mod tests { let fact = empty.get(&ARR).expect("[] should promote"); assert_eq!(fact.density, NumArrayDensity::Dense); assert_eq!(fact.proven_initial_length, 0); + + let nonempty = collect(&[let_with( + ARR, + num_array_ty(), + Expr::Array(vec![Expr::Number(1.25), Expr::Integer(2)]), + )]); + let fact = nonempty + .get(&ARR) + .expect("an all-numeric literal should promote"); + assert_eq!(fact.density, NumArrayDensity::Dense); + assert_eq!(fact.proven_initial_length, 2); } #[test] @@ -1162,11 +1181,12 @@ mod tests { num_array_ty(), new_array(vec![Expr::LocalGet(OTHER)]) )])); - // Non-empty literal (first-increment scope). + // A non-numeric literal does not establish packed raw-f64 storage, + // even when its erased declaration says `number[]`. assert!(!is_promoted(&[let_with( ARR, num_array_ty(), - Expr::Array(vec![Expr::Number(1.0)]) + Expr::Array(vec![Expr::String("not a number".to_string())]) )])); // Re-declared binding: provenance is not single-Let. assert!(!is_promoted(&[alloc_let(4), alloc_let(4)])); diff --git a/crates/perry-codegen/src/collectors/ptr_shape.rs b/crates/perry-codegen/src/collectors/ptr_shape.rs index 1a8afb68f6..4750f15fd4 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape.rs +++ b/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) -> 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 diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index b4346d0d27..69150f2e22 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/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>> = HashMap::new(); let mut let_bound: HashSet = HashSet::new(); super::super::not_bigint_locals::collect_writes(stmts, &mut writes, &mut let_bound); + // The standalone #8105 consumer does not run the Ptr 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 = HashSet::new(); let empty_fields: HashSet = HashSet::new(); let mut numeric: HashSet = 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,46 @@ 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 numeric_storage = matches!( + init, + Expr::BufferAlloc { .. } + | Expr::BufferAllocUnsafe(_) + | Expr::Uint8ArrayNew(_) + | Expr::Uint8ArrayFrom(_) + | Expr::TypedArrayNew { .. } + | Expr::NativeArenaView { .. } + ) || 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 +571,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 diff --git a/crates/perry-codegen/src/lower_call/buffer_intrinsic.rs b/crates/perry-codegen/src/lower_call/buffer_intrinsic.rs index cd3ad7e5a4..917e86f07a 100644 --- a/crates/perry-codegen/src/lower_call/buffer_intrinsic.rs +++ b/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)) } diff --git a/crates/perry-codegen/src/type_analysis/numeric.rs b/crates/perry-codegen/src/type_analysis/numeric.rs index 786ed31127..9add423b67 100644 --- a/crates/perry-codegen/src/type_analysis/numeric.rs +++ b/crates/perry-codegen/src/type_analysis/numeric.rs @@ -425,6 +425,16 @@ 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.contains_key(arr_id) { + return true; + } match ctx.stable_local_type_proof(arr_id) { Some(HirType::Array(elem)) => { matches!(**elem, HirType::Number | HirType::Int32) diff --git a/crates/perry-codegen/src/type_analysis/pod.rs b/crates/perry-codegen/src/type_analysis/pod.rs index 005515018a..825754d831 100644 --- a/crates/perry-codegen/src/type_analysis/pod.rs +++ b/crates/perry-codegen/src/type_analysis/pod.rs @@ -555,6 +555,19 @@ 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.contains_key(arr_id) { + 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. diff --git a/crates/perry-codegen/src/type_analysis/refine.rs b/crates/perry-codegen/src/type_analysis/refine.rs index 94bf23519d..909565ee45 100644 --- a/crates/perry-codegen/src/type_analysis/refine.rs +++ b/crates/perry-codegen/src/type_analysis/refine.rs @@ -248,6 +248,27 @@ pub(crate) fn proven_type_from_init(ctx: &FnCtx<'_>, init: &Expr) -> Option { Some(HirType::Named("Uint8Array".to_string())) } + // Buffer shares Uint8Array's byte storage, but its runtime class + // identity is stronger: losing it makes Buffer-only numeric methods + // such as readUInt32BE fall through to generic property dispatch. + Expr::BufferAlloc { .. } | Expr::BufferAllocUnsafe(_) => { + Some(HirType::Named("Buffer".to_string())) + } + // #8225: NativeArena views are compiler-owned HIR constructors, not + // calls selected from erasable TypeScript metadata. Losing this + // runtime-derived identity when annotation trust was tightened made + // every numeric read look declared-only: the cold `+` arm regained + // js_dynamic_string_or_number_add/js_number_coerce and the native ABI + // evidence packet went red. The kind is the allocation contract, so it + // is the same strength of proof as Uint8ArrayNew above. + Expr::TypedArrayNew { .. } | Expr::NativeArenaView { .. } => { + hir_inferred_refinable_type(ctx, init) + } + Expr::NativeArenaAlloc(_) => Some(HirType::Named("NativeArenaOwner".to_string())), + Expr::NativePodView { + view_type: Some(view_type), + .. + } => Some(view_type.clone()), Expr::Object(_) | Expr::ObjectSpread { .. } => Some(HirType::Object(Default::default())), Expr::Closure { is_async, diff --git a/crates/perry-codegen/tests/native_proof_buffer_views.rs b/crates/perry-codegen/tests/native_proof_buffer_views.rs index 9b270fb476..30f2b96996 100644 --- a/crates/perry-codegen/tests/native_proof_buffer_views.rs +++ b/crates/perry-codegen/tests/native_proof_buffer_views.rs @@ -628,6 +628,7 @@ fn artifact_records_buffer_read_u32_and_unsigned_materialization() { && record["native_rep_name"] == "u32" && record["llvm_ty"] == "i32" && record["native_value_state"] == "region_local" + && record["buffer_view_pointer_state"]["state"] == "stable" }), "expected region-local u32 buffer numeric read record:\n{artifact:#}" ); @@ -1099,6 +1100,58 @@ fn artifact_records_native_owned_typed_array_facts() { assert_eq!(artifact["summary"]["native_owned_view_count"], 4); } +#[test] +fn native_owned_view_identity_keeps_numeric_add_on_the_native_path() { + let layout_ty = pod_type(&[("value", Type::Named("PerryU32".to_string()))]); + let body = vec![ + native_arena_owner_let(1, "owner", int(64), false), + native_arena_view_let( + 2, + "view", + 1, + "Float64Array", + perry_hir::TYPED_ARRAY_KIND_FLOAT64, + int(0), + int(8), + ), + number_let( + 5, + "layoutIndex", + false, + Expr::Binary { + op: BinaryOp::Div, + left: Box::new(Expr::PodLayoutSizeOf { + ty: layout_ty.clone(), + }), + right: Box::new(Expr::PodLayoutSizeOf { ty: layout_ty }), + }, + ), + number_let( + 3, + "sum", + true, + add(index_get(2, local(5)), index_get(2, int(1))), + ), + for_loop( + 4, + int(8), + vec![Stmt::Expr(Expr::LocalSet( + 3, + Box::new(add(local(3), index_get(2, local(4)))), + ))], + ), + Stmt::Expr(Expr::NativeArenaDispose(Box::new(local(1)))), + Stmt::Return(Some(local(3))), + ]; + + let ir = compile_ir("native_owned_view_numeric_add.ts", body); + assert!( + !ir.contains("call double @js_dynamic_string_or_number_add") + && !ir.contains("call double @js_number_coerce"), + "a compiler-owned typed view is a runtime type proof, not an erasable annotation:\n{ir}" + ); +} + #[test] fn native_owned_typed_array_owner_alias_dispose_invalidates_views() { let dispose_through_alias = compile_artifact_json( diff --git a/tests/test_native_abi_contract.sh b/tests/test_native_abi_contract.sh index 5e429a85e0..01dda62a7b 100755 --- a/tests/test_native_abi_contract.sh +++ b/tests/test_native_abi_contract.sh @@ -228,6 +228,23 @@ function throughDynamicBoundary(value: any): any { return value; } +// Keep the Buffer-read representation proof in a function with no native ABI +// calls. Whole-function escape analysis must conservatively deopt views in the +// ABI exercise below; this helper makes the BufferNumericRead assertion test a +// genuinely non-escaping buffer instead of depending on unrelated call order. +function readNativeBufferChecksum(): number { + const readBuf = Buffer.alloc(8); + readBuf[0] = 18; + readBuf[1] = 52; + readBuf[2] = 86; + readBuf[3] = 120; + readBuf[4] = 0; + readBuf[5] = 0; + readBuf[6] = 200; + readBuf[7] = 64; + return readBuf.readUInt32BE(0) + readBuf.readFloatLE(4); +} + export function runNativeAbiContract(): number { const buf = Buffer.alloc(12); buf[0] = 18; @@ -249,8 +266,7 @@ export function runNativeAbiContract(): number { const promise = Promise.resolve(1); const packet: AbiPacket = { tag: 7, gain: 1.5, total: 2.25, count: 4 }; const bufferLen = buf.length; - const bufferU32 = buf.readUInt32BE(0); - const bufferF32 = buf.readFloatLE(4); + const bufferReadChecksum = readNativeBufferChecksum(); if (abi_contract_check_all(u32Value, u64Value, usizeValue, f32Value, bufferLen, buf, handle, promise) !== 777) { return 10; @@ -268,8 +284,7 @@ export function runNativeAbiContract(): number { if (nativeBufferLen !== 12) return 70; if (!nativePromise) return 75; if (bufferLen !== 12) return 80; - if (bufferU32 !== 305419896) return 90; - if (bufferF32 !== 6.25) return 100; + if (bufferReadChecksum !== 305419902.25) return 90; return 1; } EOF From ddbc78a31f0a35994524fea0ee7dc1e5977e968b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 17 Aug 2026 10:10:40 +0200 Subject: [PATCH 2/3] docs(changelog): note native ABI evidence fix --- changelog.d/8302-native-abi-evidence-proofs.md | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 changelog.d/8302-native-abi-evidence-proofs.md diff --git a/changelog.d/8302-native-abi-evidence-proofs.md b/changelog.d/8302-native-abi-evidence-proofs.md new file mode 100644 index 0000000000..916b99142a --- /dev/null +++ b/changelog.d/8302-native-abi-evidence-proofs.md @@ -0,0 +1,6 @@ +### 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. From d7727e30e264d9b3fb44b9456a10778d7a5cbaee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Mon, 17 Aug 2026 16:03:33 +0200 Subject: [PATCH 3/3] fix(codegen): preserve guarded native proof semantics --- benchmarks/compiler_output/workloads.toml | 72 +++++++++++-------- .../8302-native-abi-evidence-proofs.md | 16 +++++ .../src/collectors/ptr_numarray.rs | 46 ++++-------- .../ptr_shape_group_numeric_tests.rs | 44 ++++++++++++ .../src/collectors/ptr_shape_numeric.rs | 21 +++++- .../perry-codegen/src/native_value/buffer.rs | 20 ++++++ .../src/type_analysis/numeric.rs | 6 +- crates/perry-codegen/src/type_analysis/pod.rs | 6 +- .../tests/native_proof_buffer_views.rs | 31 ++++++++ 9 files changed, 197 insertions(+), 65 deletions(-) diff --git a/benchmarks/compiler_output/workloads.toml b/benchmarks/compiler_output/workloads.toml index 63e1383df1..bf0ce9180f 100644 --- a/benchmarks/compiler_output/workloads.toml +++ b/benchmarks/compiler_output/workloads.toml @@ -402,11 +402,7 @@ detail = "buffer_slow_path_calls" [workloads.h1_native_rep_equivalence] source = "benchmarks/compiler_output/fixtures/h1_native_rep_equivalence.ts" kind = "native_rep" -# The erased-annotation body remains the permanent semantics path. Buffer -# parameters cannot reuse the typed-array-header specialized ABI: Buffer's -# object layout is distinct even though indexed storage is byte-addressable. -allow_dynamic_property_runtime = true -allowed_hot_loop_runtime_calls = ["js_gc_loop_safepoint", "js_uint8array_set"] +allowed_hot_loop_runtime_calls = ["js_gc_loop_safepoint"] [workloads.h1_native_rep_equivalence.vectorization] min_vectorized_loops = 0 @@ -432,8 +428,7 @@ gc_collections_traced = 0 write_barriers_static = 1 write_barriers_traced = 0 boxed_number_allocations_static = 0 -# One set helper each in the public body, wrapper, and the call-site inline. -buffer_slow_path_accesses_static = 3 +buffer_slow_path_accesses_static = 0 [[workloads.h1_native_rep_equivalence.ir_checks]] name = "h1_i32_phi_path" @@ -452,11 +447,11 @@ regex_none = ["@js_buffer_get", "@js_buffer_set"] detail = "positive H1 fixture has no generic JS buffer helpers" [[workloads.h1_native_rep_equivalence.counter_checks]] -name = "h1_generic_fallback_slow_path_budget" +name = "h1_no_buffer_slow_path" section = "llvm_after" counter = "buffer_slow_path_calls" -equals = 3 -detail = "Buffer-parameter body/wrapper/call-site keep exactly three fallback set sites" +equals = 0 +detail = "buffer_slow_path_calls" [[workloads.h1_native_rep_equivalence.named_regions]] name = "direct_bounded" @@ -506,9 +501,7 @@ no_conversions = true [[workloads.h1_native_rep_equivalence.named_regions.selectors]] function_contains = "main" label_any = ["for.body.2.i"] -# The Buffer parameter's erased runtime class still proves the raw read and -# loop bounds; the write remains on the semantics-preserving runtime fallback. -counter_min = { load_i8 = 1 } +counter_min = { load_i8 = 1, store_i8 = 1 } [workloads.h1_buffer_fastpath_bench] source = "benchmarks/compiler_output/fixtures/h1_buffer_fastpath_bench.ts" @@ -758,9 +751,9 @@ rejected_fact_state = "invalidated" rejected_fact_reason = "runtime_api" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_literal_get_fast_f64" -expr_kind = "NumArrayIndexGet" -consumer = "ptr_numarray.guard_free_load" +name = "numeric_array_set_fast_f64" +expr_kind = "NumericArrayIndexSet" +consumer = "js_array_numeric_set_f64_unboxed" native_rep_name = "f64" access_mode = "checked_native" bounds_state = "proven_or_guarded" @@ -768,24 +761,47 @@ consumed_fact_kind = "raw_f64_layout" consumed_fact_state = "consumed" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_literal_set_fast_f64" -expr_kind = "NumArrayIndexSet" -consumer = "ptr_numarray.guard_free_store" +name = "numeric_array_set_guard_consumed" +expr_kind = "NumericArrayIndexSet" +consumer = "js_array_numeric_set_f64_unboxed" native_rep_name = "f64" access_mode = "checked_native" bounds_state = "proven_or_guarded" -consumed_fact_kind = "raw_f64_layout" +consumed_fact_kind = "bounds" consumed_fact_state = "consumed" [[workloads.numeric_arrays.native_rep_checks.require_records]] -name = "numeric_array_literal_set_bounds_consumed" -expr_kind = "NumArrayIndexSet" -consumer = "ptr_numarray.guard_free_store" -native_rep_name = "f64" -access_mode = "checked_native" -bounds_state = "proven_or_guarded" -consumed_fact_kind = "bounds" -consumed_fact_state = "consumed" +name = "numeric_array_set_dynamic_fallback" +expr_kind = "NumericArrayIndexSet" +consumer_contains = "fallback" +access_mode = "dynamic_fallback" +materialization_reason = "runtime_api" +fallback_reason = "runtime_api" +rejected_fact_kind = "raw_f64_layout" +rejected_fact_state = "rejected" +rejected_fact_reason = "runtime_api" + +[[workloads.numeric_arrays.native_rep_checks.require_records]] +name = "numeric_array_set_dynamic_fallback_invalidates_layout" +expr_kind = "NumericArrayIndexSet" +consumer_contains = "fallback" +access_mode = "dynamic_fallback" +materialization_reason = "runtime_api" +fallback_reason = "runtime_api" +rejected_fact_kind = "raw_f64_layout" +rejected_fact_state = "invalidated" +rejected_fact_reason = "runtime_api" + +[[workloads.numeric_arrays.native_rep_checks.require_records]] +name = "numeric_array_set_materialization_hazard_invalidated" +expr_kind = "NumericArrayIndexSet" +consumer_contains = "fallback" +access_mode = "dynamic_fallback" +materialization_reason = "runtime_api" +fallback_reason = "runtime_api" +rejected_fact_kind = "materialization_hazard" +rejected_fact_state = "invalidated" +rejected_fact_reason = "runtime_api" [workloads.packed_f64_loop_versioning] source = "benchmarks/compiler_output/fixtures/packed_f64_loop_versioning.ts" diff --git a/changelog.d/8302-native-abi-evidence-proofs.md b/changelog.d/8302-native-abi-evidence-proofs.md index 916b99142a..612d8fa39c 100644 --- a/changelog.d/8302-native-abi-evidence-proofs.md +++ b/changelog.d/8302-native-abi-evidence-proofs.md @@ -4,3 +4,19 @@ 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. diff --git a/crates/perry-codegen/src/collectors/ptr_numarray.rs b/crates/perry-codegen/src/collectors/ptr_numarray.rs index 09ce8f5962..9e40bb5b20 100644 --- a/crates/perry-codegen/src/collectors/ptr_numarray.rs +++ b/crates/perry-codegen/src/collectors/ptr_numarray.rs @@ -4,7 +4,7 @@ //! //! ## What this proves //! -//! A function-local `let a = new Array(n)` / numeric array literal qualifies +//! A function-local `let a = new Array(n)` / `let a: number[] = []` qualifies //! as a **numeric-array pointer local** when static analysis proves that for //! the local's entire lifetime: //! @@ -24,9 +24,9 @@ //! * **Provenance**: the local is initialized by exactly one `Stmt::Let` whose //! init is `new Array()` (runtime hole-fills every slot, sets //! `GC_ARRAY_RAW_F64_HOLES`, and stamps the pointer-free GC layout — -//! `js_array_constructor_single`) or an all-numeric array literal (the -//! literal classifier allocates packed raw-f64 storage). Density: -//! `new Array(n)` ⇒ `HolesOK`; a numeric literal ⇒ `Dense`. +//! `js_array_constructor_single`) or an EMPTY array literal `[]` (length 0; +//! nothing to observe until a numeric push). Density: `new Array(n)` ⇒ +//! `HolesOK`; `[]` ⇒ `Dense`. //! * **Containment**: every use of the local is an element read, an element //! write whose VALUE is numeric-by-construction (a non-number store would //! break invariant 1 — such a local is disqualified outright, not just @@ -412,20 +412,12 @@ impl<'a> UseWalk<'a> { }), _ => None, }, - // All-numeric literals allocate packed raw-f64 storage. The use - // walk below proves every later write remains numeric, so a - // non-empty literal has the same Dense invariant as `[]` rather - // than needing the guarded tier to rediscover its layout (#8225). - Expr::Array(elems) - if elems - .iter() - .all(|elem| matches!(elem, Expr::Integer(_) | Expr::Number(_))) => - { - Some(NumArrayLocal { - density: NumArrayDensity::Dense, - proven_initial_length: elems.len() as i64, - }) - } + // Empty array literal: length 0, nothing to observe until a + // (numeric-only, by containment) push. + Expr::Array(elems) if elems.is_empty() => Some(NumArrayLocal { + density: NumArrayDensity::Dense, + proven_initial_length: 0, + }), _ => None, } } @@ -1010,7 +1002,7 @@ mod tests { } #[test] - fn promotes_alloc_and_numeric_literal_provenance() { + fn promotes_alloc_and_empty_literal_provenance() { let alloc = collect(&[ alloc_let(8), Stmt::Expr(index_set(ARR, Expr::Integer(0), Expr::Number(1.5))), @@ -1026,17 +1018,6 @@ mod tests { let fact = empty.get(&ARR).expect("[] should promote"); assert_eq!(fact.density, NumArrayDensity::Dense); assert_eq!(fact.proven_initial_length, 0); - - let nonempty = collect(&[let_with( - ARR, - num_array_ty(), - Expr::Array(vec![Expr::Number(1.25), Expr::Integer(2)]), - )]); - let fact = nonempty - .get(&ARR) - .expect("an all-numeric literal should promote"); - assert_eq!(fact.density, NumArrayDensity::Dense); - assert_eq!(fact.proven_initial_length, 2); } #[test] @@ -1181,12 +1162,11 @@ mod tests { num_array_ty(), new_array(vec![Expr::LocalGet(OTHER)]) )])); - // A non-numeric literal does not establish packed raw-f64 storage, - // even when its erased declaration says `number[]`. + // Non-empty literal (first-increment scope). assert!(!is_promoted(&[let_with( ARR, num_array_ty(), - Expr::Array(vec![Expr::String("not a number".to_string())]) + Expr::Array(vec![Expr::Number(1.0)]) )])); // Re-declared binding: provenance is not single-Let. assert!(!is_promoted(&[alloc_let(4), alloc_let(4)])); diff --git a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs index f54d154d20..44871f092b 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs +++ b/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] diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index 69150f2e22..f4e5ee07bc 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs @@ -540,14 +540,31 @@ pub(super) fn expr_numeric_by_construction( 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(_) - | Expr::TypedArrayNew { .. } - | Expr::NativeArenaView { .. } + ) || matches!( + init, + Expr::TypedArrayNew { kind, .. } | Expr::NativeArenaView { kind, .. } + if number_valued_typed_array_kind(*kind) ) || matches!( init, Expr::Array(elements) diff --git a/crates/perry-codegen/src/native_value/buffer.rs b/crates/perry-codegen/src/native_value/buffer.rs index f5a26c18f2..426abb71b6 100644 --- a/crates/perry-codegen/src/native_value/buffer.rs +++ b/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 { diff --git a/crates/perry-codegen/src/type_analysis/numeric.rs b/crates/perry-codegen/src/type_analysis/numeric.rs index 9add423b67..55cd06008c 100644 --- a/crates/perry-codegen/src/type_analysis/numeric.rs +++ b/crates/perry-codegen/src/type_analysis/numeric.rs @@ -432,7 +432,11 @@ pub(crate) fn is_numeric_expr(ctx: &FnCtx<'_>, e: &Expr) -> bool { // 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.contains_key(arr_id) { + 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) { diff --git a/crates/perry-codegen/src/type_analysis/pod.rs b/crates/perry-codegen/src/type_analysis/pod.rs index 825754d831..2ffa92c4c6 100644 --- a/crates/perry-codegen/src/type_analysis/pod.rs +++ b/crates/perry-codegen/src/type_analysis/pod.rs @@ -565,7 +565,11 @@ pub(crate) fn numeric_proof_is_declared_only(ctx: &FnCtx<'_>, expr: &Expr) -> bo // 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.contains_key(arr_id) { + if ctx + .buffer_view_slots + .get(arr_id) + .is_some_and(|view| view.elem.is_number_valued()) + { return false; } } diff --git a/crates/perry-codegen/tests/native_proof_buffer_views.rs b/crates/perry-codegen/tests/native_proof_buffer_views.rs index 30f2b96996..e030c3ef6d 100644 --- a/crates/perry-codegen/tests/native_proof_buffer_views.rs +++ b/crates/perry-codegen/tests/native_proof_buffer_views.rs @@ -1152,6 +1152,37 @@ fn native_owned_view_identity_keeps_numeric_add_on_the_native_path() { ); } +#[test] +fn bigint_typed_view_addition_keeps_dynamic_bigint_dispatch() { + for (class_name, kind) in [ + ("BigInt64Array", perry_hir::TYPED_ARRAY_KIND_BIGINT64), + ("BigUint64Array", perry_hir::TYPED_ARRAY_KIND_BIGUINT64), + ] { + let module = module_with_classes_and_params( + &format!("{}_addition.ts", class_name.to_ascii_lowercase()), + Vec::new(), + Vec::new(), + Type::Any, + vec![ + typed_array_let(1, "view", class_name, kind, int(1)), + Stmt::Let { + id: 2, + name: "sum".to_string(), + ty: Type::Any, + mutable: false, + init: Some(add(index_get(1, int(0)), int(1))), + }, + Stmt::Return(Some(local(2))), + ], + ); + let ir = compile_ir_for_module_with_opts(module, empty_opts()); + assert!( + ir.contains("call double @js_dynamic_string_or_number_add"), + "{class_name} indexed reads are BigInt values and must preserve mixed-addition TypeError semantics:\n{ir}" + ); + } +} + #[test] fn native_owned_typed_array_owner_alias_dispose_invalidates_views() { let dispose_through_alias = compile_artifact_json(