888cc3ba20
The install steps' comment said every WAI workflow that runs wasmtime pins one
version and passes both determinism settings, but nothing enforced it: a step
that ran a stock or differently pinned wasmtime would have merged green.
scripts/check-wasmtime-pin.py now fails, in the repository checks, any workflow
that
1. downloads a wasmtime release other than 50.0.1, or checks it against any
SHA-256 but that archive's;
2. installs wasmtime another way (cargo install, the install script, an action);
3. runs wasmtime (run, serve, compile, or a module given to it) or names it as
a CARGO_TARGET_*_RUNNER without -W nan-canonicalization=y and
-W relaxed-simd-deterministic=y.
It also fails when it finds no download or no run, so a check that looked in
the wrong place cannot pass. On this tree it finds the downloads and runs it
should. Its self-test (scripts/check-wasmtime-pin-selftest.sh) passes a scratch
workflow shaped like these and fails each way of breaking it that the
self-test lists, matching the reason in the output.
The comment's relaxed_madd claim was measured on arm64 only. It now rests on
both architectures, measured on an arm64 macOS host and an x86_64 Linux host
with a small probe (wasmtime 50.0.1's release for the host, checked against
the digest the release lists):
host Darwin arm64; wasmtime 50.0.1 (c307ec81d 2026-10-29)
f32.add(bits 0x7fa00001, 1.0) [no flags]: 0x7fe00001
f32x4.relaxed_madd(1+2^-12, 1+2^-12, -(1+2^-11)) [no flags]: 0x33800000
f32.add(bits 0x7fa00001, 1.0) [both flags]: 0x7fc00000
f32x4.relaxed_madd(1+2^-12, 1+2^-12, -(1+2^-11)) [both flags]: 0x33800000
an unknown -W option is refused: error: failed to parse -W / --wasm option:
unknown option: no-such-option
host Linux x86_64; wasmtime 50.0.1 (c307ec81d 2026-10-29)
(the same five lines, bit for bit)
0x33800000 is 2^-24, the fused result; the unfused fadd(fmul) gives 0. So the
NaN setting takes effect on both, and relaxed_madd is fused on both with and
without the relaxed setting. That matches 50.0.1's source (the
wasmtime-internal-cranelift crate, read from the registry): the translator
lowers F32x4/F64x2RelaxedMadd through fma_f32x4/fma_f64x2
(src/translate/code_translator.rs L2530-2539), which emit a native fma on a
host that has one, a fused library call under relaxed-simd-deterministic on a
host that has none, and the unfused fmul and fadd only on a host with no FMA
and the setting off (src/func_environ.rs L5907-5925). The setting is what
makes the result fused on every host. And since an unknown -W option stops
wasmtime, a run that exits 0 with the two flags has parsed them.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
316 lines
14 KiB
YAML
316 lines
14 KiB
YAML
name: wai-ops integer operators
|
|
|
|
# The integer operator set (wai/extensions/integer-operators.md), checked on every
|
|
# fabric leg the corpus has today. Every leg recomputes every vector file of
|
|
# wai/ops-conformance/ from its inputs and requires the committed bytes:
|
|
#
|
|
# - Linux x86_64, Linux arm64 and macOS arm64, natively, debug and release: the
|
|
# unit tests (the bound rules against hand-computed values among them), the
|
|
# goldens (every committed parameter set lowered, loaded through load step 8 and
|
|
# decoded through the interpreter to its committed output digest), the step-8
|
|
# and verdict tests and the doc tests; `wai-verify vectors verify`, which also
|
|
# re-lowers every set, recomputes its bounds certificate from the committed
|
|
# lowered graphs and regenerates the whole corpus, so every certificate is
|
|
# byte-identical on every leg; and `wai-verify bounds` on the falsification sets
|
|
# of integer-operators §14.3, which must exit 1, and on committed sets, which
|
|
# must exit 0 under their profile;
|
|
# - WASI (wasm32-wasip2) under wasmtime, a 32-bit target: the same tests, and the
|
|
# same `vectors verify`;
|
|
# - a browser's engine (wasm32-unknown-unknown) under Node: the recomputation of
|
|
# every vector file;
|
|
# - the independent checker, tools/wai_ops_check.py: Python standard library only,
|
|
# sharing no code with wai-ops, rewrites every vector file and every lowered graph,
|
|
# and, as a second certifier, every certificate, the falsification sets' included
|
|
# (each must fail the profile it claims).
|
|
#
|
|
# There is no Windows leg: the Windows runner has been offline since 2026-08-28.
|
|
|
|
# One run per branch at a time. A push supersedes the run before it.
|
|
#
|
|
# There is one `macos` runner and it is the dev Mac, so every macOS job in this repo
|
|
# queues on it; only the newest commit's verdict is wanted, so older runs are
|
|
# cancelled. `cancel-in-progress: true` also applies to `main`, which advances by
|
|
# merge commits whose tree contains the commits before them.
|
|
concurrency:
|
|
group: ${{ github.workflow }}-${{ github.ref }}
|
|
cancel-in-progress: true
|
|
|
|
on:
|
|
pull_request:
|
|
paths:
|
|
- 'wai/wai-ops/**'
|
|
# The certifier, the lowerings and the corpus tool, and the Kani host they share.
|
|
- 'wai/wai-verify/**'
|
|
- 'wai/ops-conformance/**'
|
|
- 'wai/tools/wai_ops_*.py'
|
|
# The text the checker is held to.
|
|
- 'wai/extensions/integer-operators.md'
|
|
# Every committed parameter set the corpus lowers, and the digests the goldens
|
|
# compare against (neural-conformance/sha256.json among them).
|
|
- 'wai/neural-conformance/**'
|
|
- 'wai/wai-rs/tests/vectors/int_hyper/**'
|
|
- 'wai/wai-rs/tests/vectors/int_audio/**'
|
|
- 'wai/wai-rs/tests/vectors/int_splat/**'
|
|
- 'wai/wai-rs/tests/vectors/int_mlicpp/**'
|
|
- 'wai/wai-rs/tests/vectors/int_world/**'
|
|
- 'wai/wai-rs/tests/vectors/int_world2/**'
|
|
- '.github/workflows/wai-ops.yml'
|
|
push:
|
|
branches:
|
|
- main
|
|
paths:
|
|
- 'wai/wai-ops/**'
|
|
# The certifier, the lowerings and the corpus tool, and the Kani host they share.
|
|
- 'wai/wai-verify/**'
|
|
- 'wai/ops-conformance/**'
|
|
- 'wai/tools/wai_ops_*.py'
|
|
- 'wai/extensions/integer-operators.md'
|
|
- 'wai/neural-conformance/**'
|
|
- 'wai/wai-rs/tests/vectors/int_hyper/**'
|
|
- 'wai/wai-rs/tests/vectors/int_audio/**'
|
|
- 'wai/wai-rs/tests/vectors/int_splat/**'
|
|
- 'wai/wai-rs/tests/vectors/int_mlicpp/**'
|
|
- 'wai/wai-rs/tests/vectors/int_world/**'
|
|
- 'wai/wai-rs/tests/vectors/int_world2/**'
|
|
- '.github/workflows/wai-ops.yml'
|
|
|
|
jobs:
|
|
# Does this pull request's own diff touch the paths below? This forge matches a
|
|
# workflow's `paths:` against the push, so a merge of main into a branch fires the
|
|
# workflow whatever the pull request changes; every job here waits on this answer.
|
|
# A push to main, a schedule, or anything the script cannot determine answers
|
|
# `true` (scripts/pr-touches-paths.py).
|
|
relevant:
|
|
name: does this change touch it
|
|
runs-on: linux
|
|
outputs:
|
|
run: ${{ steps.gate.outputs.run }}
|
|
steps:
|
|
- uses: actions/checkout@v5
|
|
with:
|
|
fetch-depth: 0
|
|
- id: gate
|
|
run: |
|
|
set -euo pipefail
|
|
r=$(python3 scripts/pr-touches-paths.py .github/workflows/wai-ops.yml \
|
|
"${{ github.event.pull_request.base.sha }}" \
|
|
"${{ github.event.pull_request.head.sha }}")
|
|
echo "this change touches wai-ops: $r"
|
|
echo "run=$r" >> "$GITHUB_OUTPUT"
|
|
|
|
native:
|
|
needs: relevant
|
|
if: needs.relevant.outputs.run == 'true'
|
|
name: ${{ matrix.label }}
|
|
runs-on: ${{ matrix.os }}
|
|
timeout-minutes: 40
|
|
strategy:
|
|
fail-fast: false
|
|
matrix:
|
|
include:
|
|
- { os: linux, label: linux-x86_64 }
|
|
- { os: linux-arm64, label: linux-aarch64 }
|
|
- { os: macos, label: macos-arm64 }
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
# The docker images ship no Rust; the macOS host has it, but launchd's PATH omits
|
|
# ~/.cargo/bin.
|
|
- name: Install Rust 1.98.0
|
|
shell: bash
|
|
run: |
|
|
export PATH="$HOME/.cargo/bin:$PATH"
|
|
command -v rustup >/dev/null 2>&1 || \
|
|
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain 1.98.0
|
|
rustup toolchain install 1.98.0 --profile minimal
|
|
rustup default 1.98.0
|
|
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
|
|
|
|
- name: Unit, goldens, step-8, verdict and doc tests, debug
|
|
working-directory: wai/wai-ops
|
|
shell: bash
|
|
run: cargo test --locked
|
|
|
|
- name: Unit, goldens, step-8 and verdict tests, release
|
|
working-directory: wai/wai-ops
|
|
shell: bash
|
|
run: cargo test --locked --release
|
|
|
|
- name: Build wai-verify, and its own tests (the witness through the interpreter; --check's path)
|
|
working-directory: wai/wai-verify
|
|
shell: bash
|
|
run: |
|
|
set -euo pipefail
|
|
cargo build --locked --release --features cli --bin wai-verify
|
|
cargo test --locked --release --features cli --bin wai-verify
|
|
|
|
- name: Every vector file recomputed, every set re-lowered and certified, the corpus regenerated
|
|
working-directory: wai
|
|
shell: bash
|
|
run: wai-verify/target/release/wai-verify vectors verify .
|
|
|
|
# The exit status of `wai-verify bounds` (0: the verdict meets the profile, 1: it
|
|
# fails it, 3: a difference from the committed certificate), on the sets whose
|
|
# verdict integer-operators §14.3 and the design's predictions fix.
|
|
- name: The falsification sets fail their profile; committed sets meet theirs
|
|
working-directory: wai
|
|
shell: bash
|
|
run: |
|
|
set -euo pipefail
|
|
V=wai-verify/target/release/wai-verify
|
|
C=ops-conformance/certificates/wai.neural.int_synth
|
|
T="${RUNNER_TEMP:-/tmp}"
|
|
bounds() {
|
|
local want=$1; shift
|
|
set +e; "$V" bounds "$@" --out "$T/cert.json"; local got=$?; set -e
|
|
[ "$got" = "$want" ] || { echo "::error::wai-verify bounds $* exited $got, not $want"; exit 1; }
|
|
}
|
|
# One unit past i64 under acc64, and a claim of acc32 one weight past it.
|
|
bounds 1 ops-conformance/sets/overflow_acc64/int_synth.json --capability wai.neural.int_synth --profile acc64 \
|
|
--check $C/b35460f39f31a559e97e66b8dde4597a309cbc44199c40097f935dd8e6e7305a.json
|
|
bounds 1 ops-conformance/sets/claim_acc32/int_synth.json --capability wai.neural.int_synth --profile acc32 \
|
|
--check $C/76916c8f85da7663c09fba8cb091d628ed38328b680563285b8056cec82fd1ac.json
|
|
# facade meets acc32; photo meets acc64 and fails acc32 (at node 6, convT.acc).
|
|
bounds 0 neural-conformance/vectors/facade/int_synth.json --capability wai.neural.int_synth --profile acc32 \
|
|
--check $C/c6a362696d61605931ef4da98ae630362dcd73ea6be7864db6e61d6c5abbcd24.json
|
|
bounds 0 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth --profile acc64 \
|
|
--check $C/50868e72f5f1599569c413ed1f67ab8610fa0b3c17919162cbf370f49275125c.json
|
|
# With --witness, a node-local graph for each failing node: photo's node 6, whose
|
|
# input attains convT.acc's upper end. With --advise, the clamps that would let
|
|
# the overflow set meet acc64.
|
|
bounds 1 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth --profile acc32 \
|
|
--witness "$T/witness"
|
|
test -s "$T/witness/synth-6.json"
|
|
grep -q '"acc":"26172239136"' "$T/witness/synth-6.json"
|
|
bounds 1 ops-conformance/sets/overflow_acc64/int_synth.json --capability wai.neural.int_synth --advise acc64
|
|
# A certificate that is not the committed one is exit 3.
|
|
bounds 3 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth \
|
|
--check $C/c6a362696d61605931ef4da98ae630362dcd73ea6be7864db6e61d6c5abbcd24.json
|
|
|
|
wasip2:
|
|
needs: relevant
|
|
if: needs.relevant.outputs.run == 'true'
|
|
name: wasm32-wasip2 (wasmtime)
|
|
runs-on: linux
|
|
timeout-minutes: 30
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
- name: Install Rust 1.98.0 with the wasm32-wasip2 target
|
|
shell: bash
|
|
run: |
|
|
export PATH="$HOME/.cargo/bin:$PATH"
|
|
command -v rustup >/dev/null 2>&1 || \
|
|
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain 1.98.0
|
|
rustup toolchain install 1.98.0 --profile minimal
|
|
rustup default 1.98.0
|
|
rustup target add wasm32-wasip2
|
|
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
|
|
|
|
# The release binary, pinned by version and SHA-256, rather than a build from source.
|
|
# Every WAI workflow that runs wasmtime pins this one version, and every run passes
|
|
# -W nan-canonicalization=y -W relaxed-simd-deterministic=y: every NaN a float
|
|
# instruction makes is the canonical one, and each relaxed SIMD instruction has one
|
|
# behaviour on every host. A stock wasmtime leaves both off. The fixed relaxed
|
|
# behaviour is the engine's own: on 50.0.1 relaxed_madd is fused (measured on arm64 and
|
|
# x86_64), where WebAssembly's deterministic profile prescribes the unfused result.
|
|
# The repository checks (scripts/check-wasmtime-pin.py) fail a workflow that pins another
|
|
# release or runs wasmtime without both settings.
|
|
- name: Install wasmtime 50.0.1
|
|
shell: bash
|
|
run: |
|
|
set -euo pipefail
|
|
[ "$(uname -m)" = x86_64 ] || { echo "::error::the pinned wasmtime archive is x86_64; this host is $(uname -m)"; exit 1; }
|
|
if ! command -v xz >/dev/null 2>&1; then
|
|
SUDO=""; [ "$(id -u)" -ne 0 ] && SUDO="sudo"
|
|
$SUDO apt-get update -qq
|
|
$SUDO apt-get install -y -qq xz-utils
|
|
fi
|
|
v=50.0.1
|
|
f="wasmtime-v$v-x86_64-linux.tar.xz"
|
|
curl --proto '=https' --tlsv1.2 -sSfL -o "$RUNNER_TEMP/$f" \
|
|
"https://github.com/bytecodealliance/wasmtime/releases/download/v$v/$f"
|
|
echo "685466455dd42a14774a86c36c8f2e45cbb9bd6d92a850139315df60a75498a5 $RUNNER_TEMP/$f" | sha256sum -c -
|
|
tar -xJf "$RUNNER_TEMP/$f" -C "$RUNNER_TEMP"
|
|
echo "$RUNNER_TEMP/wasmtime-v$v-x86_64-linux" >> "$GITHUB_PATH"
|
|
|
|
# The tests read committed files through CARGO_MANIFEST_DIR/.., so the wai
|
|
# directory is preopened at its own absolute path.
|
|
- name: Unit, goldens, step-8 and verdict tests, under WASI
|
|
working-directory: wai/wai-ops
|
|
shell: bash
|
|
run: |
|
|
set -euo pipefail
|
|
W=$(cd .. && pwd)
|
|
CARGO_TARGET_WASM32_WASIP2_RUNNER="wasmtime run -W nan-canonicalization=y -W relaxed-simd-deterministic=y --dir $W::$W" \
|
|
cargo test --locked --release --target wasm32-wasip2
|
|
|
|
- name: Build wai-verify for wasm32-wasip2
|
|
working-directory: wai/wai-verify
|
|
shell: bash
|
|
run: cargo build --locked --release --features cli --target wasm32-wasip2 --bin wai-verify
|
|
|
|
- name: Every vector file recomputed, every set re-lowered and certified, the corpus regenerated, under WASI
|
|
working-directory: wai
|
|
shell: bash
|
|
run: |
|
|
set -euo pipefail
|
|
wasmtime --version
|
|
wasmtime run -W nan-canonicalization=y -W relaxed-simd-deterministic=y --dir .::/wai wai-verify/target/wasm32-wasip2/release/wai-verify.wasm vectors verify /wai
|
|
|
|
node:
|
|
needs: relevant
|
|
if: needs.relevant.outputs.run == 'true'
|
|
name: wasm32 under Node
|
|
runs-on: linux
|
|
timeout-minutes: 30
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
- name: Install Rust 1.98.0 with the wasm32 target
|
|
shell: bash
|
|
run: |
|
|
export PATH="$HOME/.cargo/bin:$PATH"
|
|
command -v rustup >/dev/null 2>&1 || \
|
|
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain 1.98.0
|
|
rustup toolchain install 1.98.0 --profile minimal
|
|
rustup default 1.98.0
|
|
rustup target add wasm32-unknown-unknown
|
|
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
|
|
|
|
- uses: actions/setup-node@v4
|
|
with:
|
|
node-version: '22'
|
|
|
|
- name: Build the recomputation for wasm32-unknown-unknown
|
|
working-directory: wai/wai-ops/node
|
|
shell: bash
|
|
run: cargo build --locked --release --target wasm32-unknown-unknown
|
|
|
|
- name: Every vector file recomputed under Node
|
|
working-directory: wai/wai-ops/node
|
|
shell: bash
|
|
run: node verify.mjs target/wasm32-unknown-unknown/release/wai_ops_node.wasm ../../ops-conformance
|
|
|
|
checker:
|
|
needs: relevant
|
|
if: needs.relevant.outputs.run == 'true'
|
|
name: independent checker (Python)
|
|
runs-on: linux
|
|
timeout-minutes: 20
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
- uses: actions/setup-python@v5
|
|
with:
|
|
python-version: '3.11'
|
|
|
|
# Standard library only, so it needs nothing installed.
|
|
- name: wai_ops_check.py rewrites every vector file, every lowered graph and every certificate
|
|
working-directory: wai
|
|
shell: bash
|
|
run: python3 -I tools/wai_ops_check.py ops-conformance
|
|
|
|
- name: Every workflow declares a concurrency group
|
|
shell: bash
|
|
run: bash scripts/check-workflow-concurrency.sh
|