c2e52d1e16
Some checks failed
wai-det-jpegai WAISM float-level module of record / does this change touch it (push) Successful in 25s
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (push) Has been cancelled
WAI breaking changes and the conformance runner / WAI breaking · does this change touch WAI (push) Successful in 8s
WAI breaking changes and the conformance runner / WAI breaking · wire, record and API against main · linux (push) Successful in 50s
WAI breaking changes and the conformance runner / WAI breaking and conform · their tests, and the independent verifiers through wai conform · linux (push) Successful in 7m10s
wai-det-jpegai WAISM float-level module of record / linux · both checkers, F1, F2 on wasmtime (Cranelift, Winch, Pulley) and Wasmi, the planted faults (push) Successful in 13m54s
wai-det-jpegai WAISM float-level module of record / linux-arm64 · both checkers, F1, F2 on wasmtime (Cranelift, Winch, Pulley) and Wasmi, the planted faults (push) Failing after 14m33s
One WebAssembly module with the interface of waism §5 and nothing else, decoding
wai.image.jpegai through wai-rs's exact decoder, the integer weight bundle arriving as the set
(the file sequence of norm.json and weights/*.json). Refusals are the capability's codes; a
codestream outside the decoder's configuration traps. Both checkers hold it at the float level
and refuse it R3 at the integer level. record/ keeps the module of record, built on Linux
x86_64 over main at 373fe3594 and named by its SHA-256 (53d54e58…, 666,425 bytes).
corpus.json, written by corpus.py from committed files: the reference codestream over the
pinned jpegai/v1 bundle, to the native exact decoder's pinned RGB8 (dbc494a5…), and three
refusal fixtures. host/ runs the probe on each engine first, in the same process (§6 check 10),
then every case on an instance of its own: wasmtime 50.0.1 with Cranelift, Winch and Pulley,
each with its NaN canonicalisation on and off, and Wasmi 2.0.0 built with `deterministic`.
What ran (rb, slot limiter):
- Linux x86_64 (Framework): F1 holds, the probe's bytes on the four engines with the NaN rule
set and other bytes on the three without it; the planted probe fails F1. F2: the module of
record gives every case the corpus's on all four engines, one run digest c7025bbc….
- Linux arm64 (Thor): build.sh with both checkers; F1 holds and the planted probe fails it; F2
on the module of record and on this host's own build (ffb2c94f…, other bytes): eight runs,
the same run digest. module-check.sh in full passes.
- The planted decoder (feature planted-nan-branch) gives the pinned RGB8 on the four engines
the probe holds, another output on the three with the rule unset run past the probe, and the
probe refuses those engines first (module_probe_mismatch), on both hosts.
- wai registry export --check, wai ops export --check and wai breaking against main: clean.
module-check.sh holds record/ to its manifest and both verdicts; wai-det-jpegai.yml runs the
build, F1, F2 and the planted faults on linux and linux-arm64.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
118 lines
6.8 KiB
Shell
118 lines
6.8 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-det-jpegai/** 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 float level's module of record (../wai-det-jpegai/record/, the JPEG AI exact decoder) is
|
|
# the file its manifest states, held at the float level and refused R3 at the integer level by
|
|
# both, and its corpus is the committed files' (../wai-det-jpegai/corpus.py --check). §9.3's
|
|
# probe, and the probe with a NaN-dependent branch planted, are in planted/ and held at the
|
|
# float level by both through the corpus above.
|
|
#
|
|
# 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-det-jpegai/**: the float level's module of record, its manifest 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
|
|
python3 -I -c '
|
|
import hashlib, json, sys
|
|
m = json.load(open("../wai-det-jpegai/record/manifest.json"))
|
|
for name, f in m["files"].items():
|
|
got = hashlib.sha256(open("../wai-det-jpegai/record/" + name, "rb").read()).hexdigest()
|
|
if got != f["sha256"]:
|
|
sys.exit("module-check: wai-det-jpegai/record/%s has SHA-256 %s, not the %s its manifest states" % (name, got, f["sha256"]))
|
|
print("module-check: wai-det-jpegai/record/ holds the files its manifest states")
|
|
'
|
|
m=../wai-det-jpegai/record/wai_det_jpegai.wasm
|
|
v=$(both float "$m")
|
|
[ "$v" = held ] || { echo "module-check: $m is not held at the float level: $v" >&2; exit 1; }
|
|
v=$(both integer "$m")
|
|
case "$v" in
|
|
"refused R3 "*) ;;
|
|
*) echo "module-check: $m at the integer level: $v, not refused R3" >&2; exit 1 ;;
|
|
esac
|
|
echo "module-check: $m: held at the float level, $v at the integer level, by both checkers"
|
|
python3 -I ../wai-det-jpegai/corpus.py --check
|