bench_buffer_readwrite's 1.16× is an accident of the benchmark being written at top level. The same loop in a function — where all real code lives — is 12×:
const buf = new Uint8Array(1_000_000); // module scope
// top level: let s=0; for (i<SIZE) s += buf[i]; → 46 ms (node 44)
// in a function: same loop → 560 ms (node 38)
// typed param: function f(b: Uint8Array) { ... } → 547 ms (node 38)
Root cause, walked to the exact gate
The in-function read emits two calls per element: js_uint8array_index_get_value + js_dynamic_string_or_number_add (the boxed result poisons the accumulator's numeric proof — the same chicken-and-egg #9303 fixed for the range tier).
The routing: Expr::Uint8ArrayGet (arrays_finds.rs:~921) → lower_buffer_load requires a tracked fresh view (buffer_view_slots) with proven bounds, so module-global / param / alias receivers always bail → the #6088 per-element fallback. A locally-constructed array inlines fully (7-instruction loop) because view tracking applies; nothing else does.
is_width_tracked_typed_array_receiver (index_get.rs:143) lists every typed-array kind except Uint8Array — so u8 receivers also never reach the try_lower_ta_param_f64_read checked-inline arm that other kinds get. Discriminators, all structural (emitted-call census per variant): literal vs global vs .length bound — all fail identically (not the index proof); |0 numeric context — flips to a cheaper helper, only 12%; local-constructed — fully inline.
The failed fix, and why — do not repeat it
Wiring try_lower_ta_param_f64_read into the Uint8ArrayGet arm (its own module-global proof arm admits Uint8Array, and its guard claims misses defer safely) compiles, traces ADMITTED, and returns wrong answers: every in-bounds read comes back undefined (chk=NaN where node says 6374692800), and it is slower (1838 ms — per-element guard-miss into the deferral helper). The checked load's length/kind derivation evidently assumes param/view context rather than deriving from the receiver header, so for this receiver the bound check fails on every access. Caught by the correctness battery before commit; reverted; main unaffected.
What a correct fix needs
Either teach lower_checked_typed_array_f64_load to derive data pointer + length from the receiver header per access (guard-validated, receiver-agnostic — then the wiring above becomes correct), or admit Uint8Array to the width-tracked list with a runtime kind guard that distinguishes Buffer-backed receivers. In both cases the accumulator's numeric proof follows automatically (proven by the local-constructed case, where the add is native once the read inlines).
Impact: this is the buffer hot path for every function-shaped workload — cc/pi are full of these loops. Worth more than the whole remaining suite delta.
Not claimed; I have the fixtures and the emitted-call census harness ready to hand over (/tmp/score/proof_arm.ts, idx_proof.ts, u8_adv*.ts).
bench_buffer_readwrite's 1.16× is an accident of the benchmark being written at top level. The same loop in a function — where all real code lives — is 12×:Root cause, walked to the exact gate
The in-function read emits two calls per element:
js_uint8array_index_get_value+js_dynamic_string_or_number_add(the boxed result poisons the accumulator's numeric proof — the same chicken-and-egg #9303 fixed for the range tier).The routing:
Expr::Uint8ArrayGet(arrays_finds.rs:~921) →lower_buffer_loadrequires a tracked fresh view (buffer_view_slots) with proven bounds, so module-global / param / alias receivers always bail → the #6088 per-element fallback. A locally-constructed array inlines fully (7-instruction loop) because view tracking applies; nothing else does.is_width_tracked_typed_array_receiver(index_get.rs:143) lists every typed-array kind exceptUint8Array— so u8 receivers also never reach thetry_lower_ta_param_f64_readchecked-inline arm that other kinds get. Discriminators, all structural (emitted-call census per variant): literal vs global vs.lengthbound — all fail identically (not the index proof);|0numeric context — flips to a cheaper helper, only 12%; local-constructed — fully inline.The failed fix, and why — do not repeat it
Wiring
try_lower_ta_param_f64_readinto theUint8ArrayGetarm (its own module-global proof arm admitsUint8Array, and its guard claims misses defer safely) compiles, traces ADMITTED, and returns wrong answers: every in-bounds read comes backundefined(chk=NaNwhere node says 6374692800), and it is slower (1838 ms — per-element guard-miss into the deferral helper). The checked load's length/kind derivation evidently assumes param/view context rather than deriving from the receiver header, so for this receiver the bound check fails on every access. Caught by the correctness battery before commit; reverted; main unaffected.What a correct fix needs
Either teach
lower_checked_typed_array_f64_loadto derive data pointer + length from the receiver header per access (guard-validated, receiver-agnostic — then the wiring above becomes correct), or admitUint8Arrayto the width-tracked list with a runtime kind guard that distinguishes Buffer-backed receivers. In both cases the accumulator's numeric proof follows automatically (proven by the local-constructed case, where the add is native once the read inlines).Impact: this is the buffer hot path for every function-shaped workload — cc/pi are full of these loops. Worth more than the whole remaining suite delta.
Not claimed; I have the fixtures and the emitted-call census harness ready to hand over (
/tmp/score/proof_arm.ts,idx_proof.ts,u8_adv*.ts).