--verify-native-regions accepts a stale TypedArray buffer-view pointer #7220

Summary

--verify-native-regions exits successfully for a program whose generated binary returns the wrong value because an unchecked native typed-array store uses a data pointer cached before .buffer is exposed to another view.

The compiler correctness reproduction is #7219. This issue is specifically about the verifier accepting the invalid native-view lifetime/provenance state.

Minimal reproduction

function reproduce(): number {
    const words = new Uint32Array(1);
    const bytes = new Uint8Array(words.buffer);
    words[0] = 0x01020304;
    return bytes[0] + bytes[1] + bytes[2] + bytes[3];
}

const expected = 10;
const actual = reproduce();
console.log(JSON.stringify({ expected, actual, passed: actual === expected }));

Command and output

> perry compile alias-pure-repro.ts -o alias-verified.exe --no-cache --verify-native-regions
Collecting modules...
Found 1 module(s): 1 native, 0 JavaScript
Generating code...
Linking (runtime-only)...
Wrote executable: alias-verified.exe

> ./alias-verified.exe
{expected:10,actual:0,passed:false}

The compile exits with status 0 and emits no native-region verification diagnostic.

For comparison, the same source compiled with --disable-buffer-fast-path returns the expected result:

{expected:10,actual:10,passed:true}

Verification artifact evidence

Compiling with --verify-native-regions --trace llvm records the failing store as an unchecked native access and rejects no facts:

{
  expr_kind: TypedArraySet.array,
  native_rep_name: buffer_view,
  access_mode: unchecked_native,
  bounds_state: {
    proven: {
      proof: explicit_guard
    }
  },
  alias_state: may_alias,
  emitted_inbounds: true,
  emitted_noalias: false,
  rejected_facts: []
}

The emitted LLVM caches the original typed-array data pointer before js_uint8array_new(words.buffer), then reloads that unchanged slot for the later direct store. Bounds and alias state alone do not establish that the cached storage pointer remains valid after the backing ArrayBuffer is exposed/materialized.

Environment

• Perry: 0.5.1277
• Source commit: dd83c7e92968619a1f1f30b253ac03826462e2e7
• Host: Windows 11 x86_64

Expected

One of these should happen:

1. Code generation invalidates or refreshes the tracked BufferViewSlot, falls back to a checked/runtime store, and verification succeeds on a binary that prints actual:10; or
2. If unchecked code is still emitted, --verify-native-regions rejects it because the buffer-view pointer lifetime/provenance is not valid across the .buffer escape/materialization.

A verifier regression should cover pointer validity across typedArray.buffer access and construction of a second view, independently of bounds and noalias checks.