open-standards/wai/wai-module-check/tests/module_rules.rs
Transaction Science a2e11f6ff2 waism: the probe of §9.3 and its vectors, and the probe with a NaN-dependent branch planted
planted/build.py now writes §9.3's probe beside the checker corpus: probe.wasm, whose wai_run
loads each case's operands from a data segment at run time, runs the twelve operations of the
table and stores each result in order (80 bytes), in a memory of one page whose minimum is its
maximum; and probe.txt, each case's operands and the result the deterministic profile
prescribes, and the probe's bytes. probe-nan-branch.wasm is the probe with a branch after each
operation on whether its result is a NaN, writing the canonical NaN itself.

Both checkers hold both at the float level and refuse them R3 at the integer level
(cases.txt; tests/module_rules.rs). What the planted copy breaks is F1, a property of the probe
on engines that no checker decides; the next commit's host shows the probe holds it and the
planted copy fails it.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-11-09 18:37:15 -05:00

195 lines
7.4 KiB
Rust

//! The checker held to the checker corpus of waism §9.1
//! (`planted/cases.txt`, which `planted/build.py` writes from each module's construction).
//!
//! - Every module gets the verdict stated, at every level and under every caps stated.
//! - Every planted module breaks exactly the rule its row names, at the item it names, and
//! no other: the checker's full list of findings for it is that one, but for the two rows
//! §9.1 says break a second rule, and the relaxed instruction that also takes
//! floating-point lanes at the integer level.
//! - Every rule from R1 to R12 is broken by a planted module (§11).
//! - The levels differ only in R3 (§4.3).
//! - The verdict is one line of ASCII.
use std::path::PathBuf;
use wai_module_check::{check, findings, level_of, Caps, Finding, Level, Verdict};
struct Case {
name: String,
level: Level,
caps: Caps,
caps_text: String,
verdict: String,
derived: bool,
}
fn planted() -> PathBuf {
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("planted")
}
fn cases() -> Vec<Case> {
let text = std::fs::read_to_string(planted().join("cases.txt")).expect("planted/cases.txt");
let mut out = Vec::new();
for line in text.lines() {
if line.starts_with('#') || line.trim().is_empty() {
continue;
}
let (body, comment) = match line.split_once(" #") {
Some((b, c)) => (b, c.trim()),
None => (line, ""),
};
let mut parts = body.splitn(4, ' ');
let name = parts.next().unwrap().to_string();
let level = Level::parse(parts.next().unwrap()).expect("a level");
let caps_text = parts.next().unwrap().to_string();
let caps = Caps::parse(&caps_text).expect("caps");
let verdict = parts.next().unwrap().to_string();
out.push(Case {
name,
level,
caps,
caps_text,
verdict,
derived: comment == "derived",
});
}
assert!(out.len() > 80, "cases.txt holds {} verdicts", out.len());
out
}
fn module(name: &str) -> Vec<u8> {
std::fs::read(planted().join(format!("{name}.wasm"))).unwrap_or_else(|e| panic!("{name}.wasm: {e}"))
}
#[test]
fn every_module_gets_the_verdict_stated() {
let mut wrong = Vec::new();
for c in cases() {
let got = check(&module(&c.name), c.level, &c.caps).to_string();
if got != c.verdict {
wrong.push(format!(
"{} {} {}: {got}, not {}",
c.name,
c.level.name(),
c.caps_text,
c.verdict
));
}
}
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
}
/// The rules §9.1 states a planted row breaks besides its own, at the level stated:
/// `import-memory` defines no memory (R6, at the module's length); `no-memory` lacks the
/// export `memory` (R10, there too); `f32x4.relaxed_madd` takes `f32x4` lanes (R3, at the
/// integer level, where it is the row's other rule).
fn also_broken(name: &str, level: Level) -> &'static [u8] {
match (name, level) {
("import-memory", _) => &[6],
("no-memory", _) => &[10],
("relaxed-madd", Level::Integer) => &[4],
_ => &[],
}
}
#[test]
fn every_planted_module_breaks_its_rule_and_no_other() {
// A module may break its rule at more than one item (`scalar-float` holds three
// floating-point instructions); it breaks no other rule.
let mut wrong = Vec::new();
let mut seen = 0;
for c in cases() {
let bytes = module(&c.name);
let Some(rest) = c.verdict.strip_prefix("refused R") else {
// A held module breaks nothing.
assert_eq!(findings(&bytes, c.level, &c.caps), Ok(vec![]), "{}", c.name);
continue;
};
let (rule, offset) = rest.split_once(' ').unwrap();
let rule: u8 = rule.parse().unwrap();
if rule <= 2 {
// R1 and R2 stop the reading; nothing else is decided.
continue;
}
let first = Finding {
offset: offset.parse().unwrap(),
rule,
};
let got = findings(&bytes, c.level, &c.caps).expect("meets R1 and R2");
let mut rules: Vec<u8> = got.iter().map(|f| f.rule).collect();
rules.sort();
rules.dedup();
let mut want = vec![rule];
want.extend_from_slice(also_broken(&c.name, c.level));
want.sort();
seen += 1;
if got.first() != Some(&first) || rules != want {
wrong.push(format!("{} {}: {got:?}; the rules {want:?}, first {first:?}", c.name, c.level.name()));
}
}
assert!(seen > 60, "{seen} refusals checked");
assert!(wrong.is_empty(), "{}", wrong.join("\n"));
}
#[test]
fn every_rule_has_a_planted_module() {
// §11: every rule of §4.1 that a checker decides is broken by a planted module of §9.1,
// in a verdict the text states (not one this corpus derives).
let cases = cases();
for rule in 1..=12 {
let prefix = format!("refused R{rule} ");
assert!(
cases.iter().any(|c| !c.derived && c.verdict.starts_with(&prefix)),
"no planted module of §9.1 is refused R{rule}"
);
}
}
#[test]
fn the_levels_differ_only_in_r3() {
// §4.3: a module refused R3 at the integer level is checked at the float level; every
// other verdict is the same at both.
for c in cases() {
let bytes = module(&c.name);
let int = check(&bytes, Level::Integer, &c.caps);
let float = check(&bytes, Level::Float, &c.caps);
if !matches!(int, Verdict::Refused { rule: 3, .. }) {
assert_eq!(int, float, "{}", c.name);
}
assert!(!matches!(float, Verdict::Refused { rule: 3, .. }), "{}", c.name);
}
}
#[test]
fn a_sink_holds_each_module_at_the_level_its_rows_give() {
// §6, check 9b: the integer level where it is held there, else the float level where
// the integer level refused it by R3 and the float level holds it.
let held_int = ["minimal-int", "vector-int", "bulk-and-sign", "fixed-table", "fixed-memory", "custom-section"];
for name in held_int {
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Integer), "{name}");
}
// The probe of §9.3 meets R1 to R12 at the float level, and so does the probe with a
// NaN-dependent branch planted: what it breaks is F1, which no checker decides.
for name in ["minimal-float", "scalar-float", "float-vector", "float-load", "float-unreachable", "probe", "probe-nan-branch"] {
assert_eq!(level_of(&module(name), &Caps::PROFILE).0, Some(Level::Float), "{name}");
}
// relaxed-madd: refused R3 at the integer level, then R4 at the float level.
let (level, verdict) = level_of(&module("relaxed-madd"), &Caps::PROFILE);
assert_eq!(level, None);
assert!(matches!(verdict, Verdict::Refused { rule: 4, .. }));
}
#[test]
fn the_verdict_is_one_line_of_ascii() {
for c in cases() {
let v = check(&module(&c.name), c.level, &c.caps).to_string();
assert!(v.is_ascii() && !v.contains('\n'), "{v:?}");
let ok = v == "held"
|| v.strip_prefix("refused R").is_some_and(|rest| {
let (n, at) = rest.split_once(' ').unwrap_or(("", ""));
n.parse::<u8>().is_ok_and(|n| (1..=12).contains(&n))
&& (at == "-" || at.bytes().all(|b| b.is_ascii_digit()))
});
assert!(ok, "{v:?}");
}
}