docs← Back to article

Markdown for LLMs

WebAssembly: the i32 spec-tests run

The source Markdown for this article. Copy it into your assistant or download it as a text file.

Download this articlePlain text ↗
# WebAssembly: the i32 spec-tests run

**Result:** 19 line-cases drawn from 14 directives of the official
`i32.wast` integer test script were checked on 2 October 2026. The Arxo
package `w3c.wasm_core` 0.1.0, run with `law` 0.1.1, returned the recorded
value or trap in 19 of 19 cases, with zero mismatches. The numbers belong
to that package version, that engine version, and that pinned copy of the
test script — file `test/core/i32.wast` of WebAssembly/spec at `main`
commit `608711107b7f1edb13efd57b7d79b49477462d36` (22 September 2026),
pinned by SHA-256 `f3b7e8fd641893ea0989a8ab801fce0654d276d27b5cad9cf482291a422cffe8`.
No third-party engine was executed in this run: the comparison is against
the literals written in the `.wast` directives themselves.

## The task and the reference

WebAssembly ships an official conformance script: `.wast` files that assert
exact values and exact traps for each instruction. The script is an
external reference — it is maintained with the specification, not with
either side of this comparison. The run takes a sample of its integer
cases: wrap-around addition, subtraction and multiplication, signed and
unsigned division and remainder including division by zero and the
signed-division overflow, plus equality tests and the is-zero test. Each
case carries the case facts and the question copied verbatim from the
translated test suite of the package, and the expectation is the literal
of the `.wast` directive. The public description of the language and its
test suite is at the
[WebAssembly specification site](https://webassembly.github.io/).

## What "agreement" means here

Arxo returns an evaluation document with a proof graph; the `.wast`
directive records a value or a trap. A case agrees when the outcome
projected from the Arxo answer — the value, or the fact that evaluation
traps — equals the literal of the directive. The contract compares the
outcome only. The trap message text is identical on both sides
(`integer divide by zero`, `integer overflow`) because the package carries
the same wording; that wording match is noted for information and is not
part of the comparison.

## Results

| Case | `.wast` line / directive | Expectation (literal) | Arxo answer | Outcome |
|---|---|---|---|---|
| W01 | 37 `add(1,1)=2` | value 2 | TRUE_ONLY | match |
| W02 | 41 `add(0x7fffffff,1)=0x80000000` | value 2147483648 | TRUE_ONLY | match |
| W03 | 49 `sub(0x7fffffff,-1)=0x80000000` | value 2147483648 | TRUE_ONLY | match |
| W04 | 59 `mul(0x80000000,-1)=0x80000000` | value 2147483648 | TRUE_ONLY | match |
| W05 | 61 `mul(0x01234567,0x76543210)=0x358e7470` | value 898528368 | TRUE_ONLY | match |
| W06a | 74 `div_s(5,2)=2` | value 2 | TRUE_ONLY | match |
| W06b | 75 `div_s(-5,2)=-2` | value -2 | TRUE_ONLY | match |
| W07 | 64 trap `div_s(1,0)` | trap | TRUE_ONLY | match |
| W08 | 66 trap `div_s(0x80000000,-1)` | trap | TRUE_ONLY | match |
| W09 | 85 trap `div_u(1,0)` | trap | TRUE_ONLY | match |
| W10 | 102 trap `rem_s(1,0)` | trap | TRUE_ONLY | match |
| W11 | 123 trap `rem_u(1,0)` | trap | TRUE_ONLY | match |
| W12 | 286 `eqz(0)=1` | value 1 | TRUE_ONLY | match |
| W13a | 292 `eq(0,0)=1` | value 1 | TRUE_ONLY | match |
| W13b | 293 `eq(1,1)=1` | value 1 | TRUE_ONLY | match |
| W13c | 294 `eq(-1,1)=0` | value 0 | TRUE_ONLY | match |
| W14a | 68 `div_s(1,1)=1` | value 1 | TRUE_ONLY | match |
| W14b | 69 `div_s(0,1)=0` | value 0 | TRUE_ONLY | match |
| W14c | 70 `div_s(0,-1)=0` | value 0 | TRUE_ONLY | match |

Grouped: wrap-around arithmetic W01–W06 (8 line-cases), traps W07–W11 (5),
comparisons W12–W14 (6). Every case carries a proof graph reaching the
specification sections on integer operations (4.3.2) and on expression
evaluation (4.6).

## Where the two systems behave differently

On this bank there are no differences to report: the recorded literal and
the Arxo answer coincide on all 19 line-cases, values and traps alike.

## Where the model stops

Validation directives (`assert_invalid`, `assert_malformed`) are outside
this run by contract: the run executes instructions, it does not validate
modules, so those directives were never asked. Instructions the package
does not support — bit operations, extensions, 64-bit integers, floats,
memory, calls — are untouched by the bank. And 14 directives are a sample,
not the whole `i32.wast` script and not the whole specification: agreement
on the bank is not a claim of general equivalence between implementations.

## Reproducing the run

Pin the reference first: `i32.wast` at the commit above, confirmed by the
SHA-256 shown in the Result paragraph. Pin the Arxo side: package
`w3c.wasm_core` 0.1.0 with `law` 0.1.1 (program hash
`sha256:5dd6446a587f754c2a651643ac7560c38adf9d3160253cad4830ae17dfdd43b2`
covers all 19 answers). Each case is one call of the form
`law ask w3c.wasm_core --case W01 --query-id main --format json`, asking
the truth of the expected value or trap; the recorded evaluation document
holds the proof graph and the result hash for independent inspection.