f3cfb2ecf1
spec-tests/ holds test/core's scripts at a named commit, under their Apache-2.0 licence, unpacked by a script that checks the digest first. spectest now fails on what it only used to print, and the step runs it and the differential on them. R12's reason said the rule kept a checker small. It doesn't: R2 comes first, so a checker holds a full validator anyway. The rule stands, for what a sink's engine runs. The custom-section row now says the identifier is the section's contents. Co-Authored-By: Claude Opus 5.5 <[email protected]>
40 lines
2.5 KiB
Shell
40 lines
2.5 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/**
|
|
# 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.
|
|
#
|
|
# 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.
|
|
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"
|