# 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