051f5e9c16
- module-check.sh holds wai-int-module/record/ to its manifest and at the integer level by both checkers; gives wai-web's package of record one verdict from both at each level (refused R3 27, refused R5 1452); refuses the module of record with a planted float instruction (R3) and a planted relaxed vector instruction (R4) at the offsets plant.py gives; and checks the module corpus against the committed corpora. - wai-web-wasm.yml: both checkers give demo/pkg-node, demo/pkg-platform and the package of record the same verdict at each level, and hold the module of record. - wai-int-module.yml: build.sh, then every case on wasmtime (Cranelift, Winch), Wasmi and Node on Linux x86_64 and Linux arm64, the module of record and a fresh build; a planted float that Wasmi refuses and a planted relaxed instruction that no engine compiles; and the module of record in Chromium from Playwright 1.60.0's pinned image. Pull requests and pushes that touch the module or waism.md, and nightly. - wai-conformance.yml's trigger takes wai/wai-int-module/**. Co-Authored-By: Claude Opus 5.5 <[email protected]>
92 lines
5.4 KiB
Shell
92 lines
5.4 KiB
Shell
# step: WAISM profile · the Rust checker, check-module.mjs and their differential
|
|
# order: 780
|
|
# paths: wai/extensions/waism.md wai/wai-module-check/** wai/wai-int-module/** wai/wai-web/reach/record/**
|
|
# working-directory: wai/wai-module-check
|
|
#
|
|
# The WAISM profile (extensions/waism.md): its two checkers,
|
|
# held to the same corpora and to each other. planted/build.py rebuilds the checker corpus
|
|
# of §9.1 from each module's construction, byte for byte, with the verdicts their rows state.
|
|
# The Rust checker (wasmparser, pinned) runs tests/module_rules.rs (every module its verdict,
|
|
# every planted module exactly its rule, every rule a planted module, the levels differing
|
|
# only in R3) and then the corpus itself; check-module.mjs, the second implementation,
|
|
# written from the text with no dependency and sharing no code with it, runs the same
|
|
# corpus. Both then run the validation limits' corpus (§4.2: each limit at its value and one
|
|
# past it), which build.py generates here, being too large to commit. Last, the differential:
|
|
# examples/differential.rs writes 10,000 modules from wasm-smith, from its committed seed,
|
|
# and two mutated copies of each, with the Rust checker's verdicts, and differential.mjs
|
|
# requires check-module.mjs to give every one the same verdict at both levels. The same two
|
|
# hold to WebAssembly's own specification tests, a pinned copy in spec-tests/: they are the
|
|
# refusals, one construct at a time.
|
|
#
|
|
# Then the two checkers on the modules of record. The operator-set module
|
|
# (../wai-int-module/record/, its scalar and its SIMD128 build) is held at the integer level
|
|
# by both, each file the SHA-256 its manifest states. wai-web's package of record
|
|
# (../wai-web/reach/record/wai_web_bg.wasm) is no WAISM module, and both checkers give it one
|
|
# verdict at each level, the same. A float instruction planted in the module of record, and
|
|
# a relaxed vector instruction, are each refused by both at the rule and the offset the plant
|
|
# gives (../wai-int-module/plant.py): the check can fail on the module it holds. Last, the
|
|
# module's corpus is the committed corpora's (../wai-int-module/corpus.py --check).
|
|
#
|
|
# The paths this step brings to the workflow's trigger, and why:
|
|
# wai/extensions/waism.md: the rules, the limits and the corpus the checkers
|
|
# implement.
|
|
# wai/wai-module-check/**: the checkers, the corpus and its generator, and the differential.
|
|
# wai/wai-int-module/**: the module of record, its manifest, its plant and its corpus.
|
|
# wai/wai-web/reach/record/**: wai-web's package of record, which both checkers read.
|
|
set -euo pipefail
|
|
python3 -I planted/build.py --check
|
|
cargo test --locked --release
|
|
cargo run --locked --release -q -- --cases planted
|
|
node check-module.mjs --cases planted
|
|
python3 -I planted/build.py --limits "$RUNNER_TEMP/module-limits"
|
|
cargo run --locked --release -q -- --cases "$RUNNER_TEMP/module-limits"
|
|
node check-module.mjs --cases "$RUNNER_TEMP/module-limits"
|
|
rm -rf "$RUNNER_TEMP/module-limits"
|
|
cargo run --locked --release -q --example differential -- --out "$RUNNER_TEMP/module-differential"
|
|
node differential.mjs "$RUNNER_TEMP/module-differential"
|
|
rm -rf "$RUNNER_TEMP/module-differential"
|
|
python3 -I spec-tests/extract.py "$RUNNER_TEMP/module-spec"
|
|
cargo run --locked --release -q --example spectest -- --wast "$RUNNER_TEMP/module-spec/core" --out "$RUNNER_TEMP/module-spec-out"
|
|
node differential.mjs "$RUNNER_TEMP/module-spec-out"
|
|
rm -rf "$RUNNER_TEMP/module-spec" "$RUNNER_TEMP/module-spec-out"
|
|
|
|
# One verdict from both checkers, or a failure naming both.
|
|
both() {
|
|
local r j
|
|
r=$(cargo run --locked --release -q -- --level "$1" "$2" || true)
|
|
j=$(node check-module.mjs --level "$1" "$2" || true)
|
|
if [ "$r" != "$j" ]; then
|
|
echo "module-check: $2 at the $1 level: the Rust checker says '$r', check-module.mjs '$j'" >&2
|
|
return 1
|
|
fi
|
|
echo "$r"
|
|
}
|
|
python3 -I -c '
|
|
import hashlib, json, sys
|
|
m = json.load(open("../wai-int-module/record/manifest.json"))
|
|
for name, f in m["files"].items():
|
|
got = hashlib.sha256(open("../wai-int-module/record/" + name, "rb").read()).hexdigest()
|
|
want = f["sha256"]
|
|
if got != want:
|
|
sys.exit("module-check: record/%s has SHA-256 %s, not the %s its manifest states" % (name, got, want))
|
|
print("module-check: record/ holds the files its manifest states")
|
|
'
|
|
for m in ../wai-int-module/record/wai_int.wasm ../wai-int-module/record/wai_int.simd128.wasm; do
|
|
v=$(both integer "$m")
|
|
[ "$v" = held ] || { echo "module-check: $m is not held at the integer level: $v" >&2; exit 1; }
|
|
echo "module-check: $m: held at the integer level by both checkers"
|
|
done
|
|
for level in integer float; do
|
|
v=$(both "$level" ../wai-web/reach/record/wai_web_bg.wasm)
|
|
echo "module-check: wai-web's package of record at the $level level: $v, from both checkers"
|
|
done
|
|
for p in float relaxed; do
|
|
python3 -I ../wai-int-module/plant.py "$p" ../wai-int-module/record/wai_int.wasm "$RUNNER_TEMP/planted-$p.wasm" > "$RUNNER_TEMP/planted-$p.txt"
|
|
while read -r level want; do
|
|
got=$(both "$level" "$RUNNER_TEMP/planted-$p.wasm")
|
|
[ "$got" = "$want" ] || { echo "module-check: the module of record with a planted $p instruction, at the $level level: $got, not $want" >&2; exit 1; }
|
|
echo "module-check: the module of record with a planted $p instruction, at the $level level: $got, from both checkers"
|
|
done < "$RUNNER_TEMP/planted-$p.txt"
|
|
rm -f "$RUNNER_TEMP/planted-$p.wasm" "$RUNNER_TEMP/planted-$p.txt"
|
|
done
|
|
python3 -I ../wai-int-module/corpus.py --check
|