Summary
The web/Wasm backend (src/wasm.rs, the build_web lowering) allocates its per-function scratch locals (the i32 wide pair, the u8 pair, the usize pair) at index layout.declarations.len(), but every other local in the same function is indexed at parameter_count + layout.declarations.len(). In any function with at least one parameter the scratch indices therefore point at the wrong locals:
- i32 add/sub/mul/div/rem/neg in a function with parameters: the i64 scratch index lands on an i32 local, so the emitted module fails Wasm validation at instantiation.
semaprax build --target web still exits 0 and prints built web package.
- u8 or usize arithmetic in a function with parameters and
let bindings: the scratch pair has the same Wasm type (i32/i64) as the locals it aliases, so validation passes and the program silently computes the wrong value. Interpreter and native lanes return the right value.
This violates the first non-negotiable invariant in AGENTS.md (equivalent checked behavior on every backend). The committed examples/integers_i32.spx is affected: run and build --target native return 7, the web package fails to instantiate.
Observed on semaprax 0.3.0 built from main at 5c6e7a4b (debug profile), macOS arm64, node v24.3.0.
Reproducers
A. Invalid module (i32 arithmetic with a parameter)
i32mulparam.spx:
module probe.i32mulparam;
@id("probe.dbl")
fn dbl(value: i32) -> i32
{
value * 2i32
}
@id("app.main")
fn main() -> i64
{
if dbl(4i32) == 8i32 { 7 } else { 9 }
}
semaprax run i32mulparam.spx # 7
semaprax build i32mulparam.spx --target native -o n && ./n # 7
semaprax build i32mulparam.spx --target web -o web # exit 0, "built web package"
node --input-type=module -e '
import { readFile } from "node:fs/promises";
import { instantiateBytes } from "./web/semaprax.js";
const { instance } = await instantiateBytes(await readFile("./web/app.wasm"));
console.log(instance.exports.semaprax_main());'
Node output:
WebAssembly.instantiate(): Compiling function #7 failed: local.set[0] expected type i32, found i64.extend_i32_s of type i64 @+182
The same failure occurs with unary negation (-value where value: i32 is a parameter), and with -o for --target wasm. Negating or multiplying an i32 let binding inside a zero-parameter function works, which is what hides the bug from the existing tests.
B. Silent wrong result (u8 arithmetic with parameters and lets)
u8clobber.spx:
module probe.u8clobber;
@id("probe.combine")
fn combine(left: u8, right: u8) -> u8
{
let first = left + right;
let second = left + 1u8;
first + second
}
@id("app.main")
fn main() -> i64
{
if combine(1u8, 2u8) == 5u8 { 7 } else { 9 }
}
| lane |
result |
semaprax run |
7 |
native (build --target native) |
7 |
web (build --target web, semaprax_main() via node) |
9 |
Replacing every u8 with usize (1usize, 2usize, 5usize) gives the same disagreement (interpreter 7, native 7, web 9).
Root cause
src/wasm.rs, function-body emission loop starting near line 1496 (for (function, _) in &executable_functions):
// let bindings (collect_locals, ~line 3190): parameter offset applied
let index = parameter_count + layout.declarations.len() as u32;
// scratch locals (~lines 1530-1560): parameter offset missing
layout.wide_scratch = [
layout.declarations.len() as u32,
layout.declarations.len() as u32 + 1,
];
...
let left_index = layout.declarations.len() as u32; // u8_scratch
...
let left_index = layout.declarations.len() as u32; // usize_scratch
Wasm local indices count parameters first, then declared locals, so the scratch indices must be function.params.len() as u32 + layout.declarations.len() as u32. With combine(left, right) above the real layout is 0=left 1=right 2=result 3=first 4=second 5,6=scratch, but u8_scratch is computed as (3, 4), so the second addition's scratch writes overwrite first and second.
Users of the scratch: emit_expr UnaryOp::Neg i32 branch (~line 3507), emit_i32_checked_binary (~line 4329), the u8 arithmetic path (~line 3688), and the usize arithmetic path. Only the allocation sites need to change; the consumers read layout.*_scratch.
Suggested fix
- In the three allocation sites add
function.params.len() as u32 + to the index computation (or introduce one helper fn next_local_index(&self, parameter_count) -> u32 used by collect_locals and the scratch allocation so they cannot drift again).
- Add regression tests to the Wasm harness that already executes modules through Node (see
tests/scalar_status_backend_equivalence.rs for the pattern, and tests/wasm/ for the harness modules; AGENTS.md asks for tests as modules of the owning harness, not new top-level files): one program per scratch kind (i32 neg, i32 binary, u8, usize) inside a function with two parameters and two let bindings, asserting the exported value equals the interpreter's. Also assert that the emitted bytes validate with wasmparser (already a dependency) before the Node step, so an invalid module fails the build rather than only failing at instantiation.
- Consider making
build --target web run wasmparser::validate on the produced bytes and fail closed with a diagnostic; today an invalid module is written and the command exits 0.
- Update
CHANGELOG.md; no spec change is needed (the web ABI is unchanged).
Verification
scripts/quality.sh changed # or the full profile; the touched path routes to the Wasm gates
plus the three reproducers above returning the same value on all three lanes.
Summary
The web/Wasm backend (
src/wasm.rs, thebuild_weblowering) allocates its per-function scratch locals (the i32 wide pair, the u8 pair, the usize pair) at indexlayout.declarations.len(), but every other local in the same function is indexed atparameter_count + layout.declarations.len(). In any function with at least one parameter the scratch indices therefore point at the wrong locals:semaprax build --target webstill exits 0 and printsbuilt web package.letbindings: the scratch pair has the same Wasm type (i32/i64) as the locals it aliases, so validation passes and the program silently computes the wrong value. Interpreter and native lanes return the right value.This violates the first non-negotiable invariant in
AGENTS.md(equivalent checked behavior on every backend). The committedexamples/integers_i32.spxis affected:runandbuild --target nativereturn 7, the web package fails to instantiate.Observed on
semaprax 0.3.0built from main at5c6e7a4b(debug profile), macOS arm64, node v24.3.0.Reproducers
A. Invalid module (i32 arithmetic with a parameter)
i32mulparam.spx:Node output:
The same failure occurs with unary negation (
-valuewherevalue: i32is a parameter), and with-ofor--target wasm. Negating or multiplying an i32letbinding inside a zero-parameter function works, which is what hides the bug from the existing tests.B. Silent wrong result (u8 arithmetic with parameters and lets)
u8clobber.spx:semaprax runbuild --target native)build --target web,semaprax_main()via node)Replacing every
u8withusize(1usize,2usize,5usize) gives the same disagreement (interpreter 7, native 7, web 9).Root cause
src/wasm.rs, function-body emission loop starting near line 1496 (for (function, _) in &executable_functions):Wasm local indices count parameters first, then declared locals, so the scratch indices must be
function.params.len() as u32 + layout.declarations.len() as u32. Withcombine(left, right)above the real layout is0=left 1=right 2=result 3=first 4=second 5,6=scratch, butu8_scratchis computed as(3, 4), so the second addition's scratch writes overwritefirstandsecond.Users of the scratch:
emit_exprUnaryOp::Negi32 branch (~line 3507),emit_i32_checked_binary(~line 4329), the u8 arithmetic path (~line 3688), and the usize arithmetic path. Only the allocation sites need to change; the consumers readlayout.*_scratch.Suggested fix
function.params.len() as u32 +to the index computation (or introduce one helperfn next_local_index(&self, parameter_count) -> u32used bycollect_localsand the scratch allocation so they cannot drift again).tests/scalar_status_backend_equivalence.rsfor the pattern, andtests/wasm/for the harness modules;AGENTS.mdasks for tests as modules of the owning harness, not new top-level files): one program per scratch kind (i32 neg, i32 binary, u8, usize) inside a function with two parameters and twoletbindings, asserting the exported value equals the interpreter's. Also assert that the emitted bytes validate withwasmparser(already a dependency) before the Node step, so an invalid module fails the build rather than only failing at instantiation.build --target webrunwasmparser::validateon the produced bytes and fail closed with a diagnostic; today an invalid module is written and the command exits 0.CHANGELOG.md; no spec change is needed (the web ABI is unchanged).Verification
scripts/quality.sh changed # or the full profile; the touched path routes to the Wasm gatesplus the three reproducers above returning the same value on all three lanes.