//! The shipped WGSL modules held, on naga 30.0.1's IR (the translator wgpu runs them
//! through), to the rules the `decode-equivalence` tier on a GPU rests on
//! (determinism-tiers §5, *Claiming the tier on a GPU*). No adapter is needed: these run
//! on every leg.
//!
//! 1. Each module parses, and validates with every validation flag and no capability:
//!    so no `f16`, no 64-bit type, no subgroup or quad operation, no extension.
//! 2. Every entry point is a compute entry point; the globals are exactly the six
//!    bindings of `wgsl/common.wgsl`, and there is no workgroup or private memory.
//! 3. Every scalar, in the type arena and in the type of every expression, is `bool`,
//!    `i32` or `u32`; every literal is one of those. No floating-point value exists.
//! 4. Every expression is one of a closed list: no derivative, image, ray-query,
//!    subgroup or cooperative-matrix expression; every built-in function is one of the
//!    integer functions the semantics suite tests; every conversion is between `bool`,
//!    `i32` and `u32`.
//! 5. In the kernels (every module but `semantics`, which exists to evaluate them), every
//!    shift amount is a literal in 0..=31 or masked to 0..=31 (`e & 31u`), and every
//!    `clamp` has literal bounds in order: the two integer operations whose WGSL result
//!    naga 30.0.1 does not produce itself in MSL, HLSL and SPIR-V
//!    (`semantics::UNGUARDED`) are reached only where every backend defines them. No
//!    kernel shifts a signed value left: MSL leaves a left shift of a negative or
//!    overflowing signed value undefined, and naga writes the shift as it is, so a kernel
//!    shifts the `u32` and bitcasts.
//! 6. The only atomic operation is `atomicOr`, its result unused, and no `atomicLoad` or
//!    `atomicStore` reaches an atomic word (naga lowers both to a plain load and store
//!    through a pointer to it, which this rule reads): so every atomic operation on a word
//!    is of one kind, and no result depends on the order in which invocations reach it;
//!    there is no barrier.
//! 7. Every integer operation the kernels use (by operator and by signedness) is one the
//!    semantics suite runs on every adapter (`src/semantics.rs`).
//! 8. Each module translates to MSL 2.4, HLSL shader model 5.1 and SPIR-V; the MSL and
//!    HLSL carry naga's guards for every guarded operation the module uses (signed
//!    arithmetic through unsigned, found by its nesting, `as_type<int>(as_type<uint>(`
//!    and `asint(asuint(`, not by a bitcast; `naga_div`, `naga_mod`, `naga_neg`,
//!    `naga_abs`), and
//!    the MSL guards for division vanish when `emit_int_div_checks` is turned off,
//!    which is what the crate must never do.
//!
//! Then each planted violation (a floating-point value, `f16`, a subgroup operation, an
//! `atomicAdd`, an atomic's result read, an `atomicLoad`, an `atomicStore`, `atomicOr`
//! and `atomicStore` on one word, a workgroup variable and barrier, a storage barrier
//! alone, an unmasked shift, a signed left shift, a run-time `clamp`) is shown to be refused, by the rule it
//! breaks.

use std::collections::BTreeSet;

use naga::back::{hlsl, msl, spv};
use naga::valid::{Capabilities, ModuleInfo, ValidationFlags, Validator};
use naga::{AddressSpace, AtomicFunction, BinaryOperator, Block, Expression, Literal, MathFunction, Module, Scalar, ScalarKind, ShaderStage, Statement, StorageAccess, TypeInner, UnaryOperator};
use wai_ops_gpu::kernels::Sources;
use wai_ops_gpu::semantics::Op;

type Check<T = ()> = Result<T, String>;

/// Step 1.
fn compile(text: &str) -> Check<(Module, ModuleInfo)> {
    let module = naga::front::wgsl::parse_str(text).map_err(|e| format!("rule 1: parse: {}", e.emit_to_string(text)))?;
    let info = Validator::new(ValidationFlags::all(), Capabilities::empty()).validate(&module).map_err(|e| format!("rule 1: validation: {}", e.emit_to_string(text)))?;
    Ok((module, info))
}

/// The functions and entry points, with their expression-info tables.
fn functions<'a>(m: &'a Module, info: &'a ModuleInfo) -> Vec<(String, &'a naga::Function, &'a naga::valid::FunctionInfo)> {
    let mut v: Vec<(String, &naga::Function, &naga::valid::FunctionInfo)> = m.functions.iter().map(|(h, f)| (f.name.clone().unwrap_or_default(), f, &info[h])).collect();
    for (i, e) in m.entry_points.iter().enumerate() {
        v.push((e.name.clone(), &e.function, info.get_entry_point(i)));
    }
    v
}

/// Step 2.
fn interface(m: &Module) -> Check {
    for e in &m.entry_points {
        if e.stage != ShaderStage::Compute {
            return Err(format!("rule 2: entry point `{}` is a {:?} stage", e.name, e.stage));
        }
        if e.workgroup_size_overrides.is_some() || e.workgroup_size[1] != 1 || e.workgroup_size[2] != 1 {
            return Err(format!("rule 2: entry point `{}` has workgroup size {:?}", e.name, e.workgroup_size));
        }
    }
    let mut found = Vec::new();
    for (_, v) in m.global_variables.iter() {
        let name = v.name.clone().unwrap_or_default();
        let space = match v.space {
            AddressSpace::Uniform => "uniform",
            AddressSpace::Storage { access } if access == StorageAccess::LOAD => "read",
            AddressSpace::Storage { access } if access.contains(StorageAccess::LOAD | StorageAccess::STORE) => "read_write",
            other => return Err(format!("rule 2: global `{name}` is in address space {other:?}")),
        };
        let b = v.binding.ok_or(format!("rule 2: global `{name}` has no binding"))?;
        found.push((b.group, b.binding, space));
    }
    found.sort();
    let want = vec![(0, 0, "uniform"), (0, 1, "read"), (0, 2, "read"), (0, 3, "read"), (0, 4, "read_write"), (0, 5, "read_write")];
    if found != want {
        return Err(format!("rule 2: the globals are {found:?}, not the six bindings of common.wgsl"));
    }
    Ok(())
}

fn scalar_ok(s: Scalar) -> bool {
    s.kind == ScalarKind::Bool || (matches!(s.kind, ScalarKind::Sint | ScalarKind::Uint) && s.width == 4)
}

fn type_ok(t: &TypeInner) -> Check {
    match *t {
        TypeInner::Scalar(s) | TypeInner::Vector { scalar: s, .. } | TypeInner::Atomic(s) | TypeInner::ValuePointer { scalar: s, .. } => {
            if scalar_ok(s) { Ok(()) } else { Err(format!("{:?} of width {}", s.kind, s.width)) }
        }
        TypeInner::Pointer { .. } | TypeInner::Array { .. } | TypeInner::Struct { .. } => Ok(()),
        ref other => Err(format!("{other:?}")),
    }
}

/// Step 3.
fn types(m: &Module, info: &ModuleInfo) -> Check {
    for (_, t) in m.types.iter() {
        type_ok(&t.inner).map_err(|e| format!("rule 3: the type {} is not made of bool, i32 and u32: {e}", t.name.clone().unwrap_or_default()))?;
    }
    for (name, f, fi) in functions(m, info) {
        for (h, e) in f.expressions.iter() {
            type_ok(fi[h].ty.inner_with(&m.types)).map_err(|err| format!("rule 3: in `{name}`, {e:?} has a type that is not bool, i32 or u32: {err}"))?;
            if let Expression::Literal(l) = e {
                literal_ok(l).map_err(|err| format!("rule 3: in `{name}`: {err}"))?;
            }
        }
    }
    for (_, e) in m.global_expressions.iter() {
        if let Expression::Literal(l) = e {
            literal_ok(l).map_err(|err| format!("rule 3: at module scope: {err}"))?;
        }
    }
    Ok(())
}

fn literal_ok(l: &Literal) -> Check {
    match l {
        Literal::U32(_) | Literal::I32(_) | Literal::Bool(_) => Ok(()),
        other => Err(format!("the literal {other:?}")),
    }
}

/// The integer functions the semantics suite tests.
fn math_ok(f: MathFunction) -> bool {
    use MathFunction::*;
    matches!(f, Min | Max | Clamp | Abs | Sign | CountLeadingZeros | CountTrailingZeros | CountOneBits | ReverseBits | FirstLeadingBit | FirstTrailingBit | ExtractBits | InsertBits)
}

/// The integer value of a literal, or of a constant initialised with one.
fn literal_value(m: &Module, arena: &naga::Arena<Expression>, h: naga::Handle<Expression>) -> Option<i64> {
    let lit = |l: &Literal| match *l {
        Literal::U32(v) => Some(i64::from(v)),
        Literal::I32(v) => Some(i64::from(v)),
        _ => None,
    };
    match &arena[h] {
        Expression::Literal(l) => lit(l),
        Expression::Constant(c) => match &m.global_expressions[m.constants[*c].init] {
            Expression::Literal(l) => lit(l),
            _ => None,
        },
        _ => None,
    }
}

/// A shift amount the kernels may use: a literal in 0..=31, or `e & k` with `k` a literal
/// in 0..=31 (either side).
fn amount_bounded(m: &Module, arena: &naga::Arena<Expression>, h: naga::Handle<Expression>) -> bool {
    if let Some(v) = literal_value(m, arena, h) {
        return (0..=31).contains(&v);
    }
    match arena[h] {
        Expression::Binary { op: BinaryOperator::And, left, right } => [left, right].iter().any(|&x| literal_value(m, arena, x).is_some_and(|v| (0..=31).contains(&v))),
        _ => false,
    }
}

/// The scalar kind of an expression and whether it is a vector.
fn kind_of(m: &Module, fi: &naga::valid::FunctionInfo, h: naga::Handle<Expression>) -> (Option<ScalarKind>, bool) {
    let t = fi[h].ty.inner_with(&m.types);
    (t.scalar_kind(), matches!(t, TypeInner::Vector { .. }))
}

/// Whether a pointer expression points at an atomic: naga lowers `atomicLoad` to a plain
/// `Load` and `atomicStore` to a plain `Store` through such a pointer.
fn points_at_atomic(m: &Module, fi: &naga::valid::FunctionInfo, p: naga::Handle<Expression>) -> bool {
    match *fi[p].ty.inner_with(&m.types) {
        TypeInner::Pointer { base, .. } => matches!(m.types[base].inner, TypeInner::Atomic(_)),
        _ => false,
    }
}

/// Steps 4, 5 and 7: the closed list of expressions, the kernel rules on shifts and
/// `clamp`, and the semantics operation each integer operation is. Returns the
/// operations used.
fn expressions(m: &Module, info: &ModuleInfo, kernel: bool) -> Check<BTreeSet<Op>> {
    let mut used = BTreeSet::new();
    for (name, f, fi) in functions(m, info) {
        let arena = &f.expressions;
        for (h, e) in arena.iter() {
            let at = |what: String| format!("in `{name}`, {what}");
            match *e {
                Expression::Literal(_) | Expression::Constant(_) | Expression::ZeroValue(_) | Expression::Compose { .. } | Expression::Access { .. } | Expression::AccessIndex { .. } | Expression::Splat { .. } | Expression::Swizzle { .. } | Expression::FunctionArgument(_) | Expression::GlobalVariable(_) | Expression::LocalVariable(_) | Expression::CallResult(_) | Expression::ArrayLength(_) => {}
                // An `atomicLoad`: its value depends on which invocations reached the word first.
                Expression::Load { pointer } => {
                    if points_at_atomic(m, fi, pointer) {
                        return Err(format!("rule 6: {}", at("an atomic word is loaded (atomicLoad)".into())));
                    }
                }
                Expression::Relational { fun, .. } => {
                    if !matches!(fun, naga::RelationalFunction::All | naga::RelationalFunction::Any) {
                        return Err(format!("rule 4: {}", at(format!("the relational function {fun:?}"))));
                    }
                }
                // naga gives every atomic call a result; the call statement does not count
                // as a reference to it, so a count above zero is a read.
                Expression::AtomicResult { .. } => {
                    if fi[h].ref_count > 0 {
                        return Err(format!("rule 6: {}", at("an atomic operation's result is read".into())));
                    }
                }
                Expression::Unary { op, expr } => {
                    let (k, _) = kind_of(m, fi, expr);
                    match (op, k) {
                        (UnaryOperator::Negate, Some(ScalarKind::Sint)) => {
                            used.insert(Op::NegI32);
                        }
                        (UnaryOperator::BitwiseNot, Some(ScalarKind::Sint | ScalarKind::Uint)) => {
                            used.insert(Op::Not);
                        }
                        (UnaryOperator::LogicalNot, Some(ScalarKind::Bool)) | (UnaryOperator::BitwiseNot, Some(ScalarKind::Bool)) => {}
                        (op, k) => return Err(format!("rule 4: {}", at(format!("the unary {op:?} on {k:?}")))),
                    }
                }
                Expression::Binary { op, left, right } => {
                    let (k, vector) = kind_of(m, fi, left);
                    use BinaryOperator as B;
                    let s = k == Some(ScalarKind::Sint);
                    let int = matches!(k, Some(ScalarKind::Sint | ScalarKind::Uint));
                    let v = vector;
                    let op_used = match op {
                        B::Add if int && v && !s => Some(Op::AddVec2U32),
                        B::Multiply if int && v => Some(if s { Op::MulVec2I32 } else { Op::MulVec2U32 }),
                        B::ShiftRight if v => Some(if s { Op::ShrVec2I32 } else { Op::ShrVec2U32 }),
                        B::Add if int && !v => Some(if s { Op::AddI32 } else { Op::AddU32 }),
                        B::Subtract if int && !v => Some(if s { Op::SubI32 } else { Op::SubU32 }),
                        B::Multiply if int && !v => Some(if s { Op::MulI32 } else { Op::MulU32 }),
                        B::Divide if int && !v => Some(if s { Op::DivI32 } else { Op::DivU32 }),
                        B::Modulo if int && !v => Some(if s { Op::RemI32 } else { Op::RemU32 }),
                        B::ShiftLeft if int && !v => Some(if s { Op::ShlI32 } else { Op::ShlU32 }),
                        B::ShiftRight if int && !v => Some(if s { Op::ShrI32 } else { Op::ShrU32 }),
                        B::And if int && !v => Some(Op::And),
                        B::InclusiveOr if int && !v => Some(Op::Or),
                        B::ExclusiveOr if int && !v => Some(Op::Xor),
                        B::Less | B::Greater if int && !v => Some(if s { Op::LtI32 } else { Op::LtU32 }),
                        B::LessEqual | B::GreaterEqual if int && !v => Some(if s { Op::LeI32 } else { Op::LeU32 }),
                        B::Equal if int && !v => Some(Op::Eq),
                        B::NotEqual if int && !v => Some(Op::Ne),
                        B::LogicalAnd | B::LogicalOr | B::And | B::InclusiveOr | B::Equal | B::NotEqual if k == Some(ScalarKind::Bool) => None,
                        _ => return Err(format!("rule 7: {}", at(format!("{op:?} on {k:?} (vector {vector}), which the semantics suite does not test")))),
                    };
                    // MSL leaves a left shift of a negative or overflowing signed value undefined,
                    // and naga passes it through: a kernel shifts a u32 and bitcasts.
                    if kernel && op == B::ShiftLeft && s {
                        return Err(format!("rule 5: {}", at("a left shift of a signed value: shift the u32 and bitcast".into())));
                    }
                    if kernel && matches!(op, B::ShiftLeft | B::ShiftRight) && !amount_bounded(m, arena, right) {
                        return Err(format!("rule 5: {}", at(format!("{op:?} by an amount that is neither a literal in 0..=31 nor masked to it: {:?}", arena[right]))));
                    }
                    used.extend(op_used);
                }
                Expression::Select { accept, .. } => {
                    let (k, vector) = kind_of(m, fi, accept);
                    used.insert(match (k, vector) {
                        (_, true) => Op::SelectVec2U32,
                        (Some(ScalarKind::Sint), false) => Op::SelectI32,
                        _ => Op::SelectU32,
                    });
                }
                Expression::Math { fun, arg, arg1, arg2, .. } => {
                    if !math_ok(fun) {
                        return Err(format!("rule 4: {}", at(format!("the built-in function {fun:?}, not an integer function the suite tests"))));
                    }
                    let (k, _) = kind_of(m, fi, arg);
                    let s = k == Some(ScalarKind::Sint);
                    use MathFunction as F;
                    if kernel && fun == F::Clamp {
                        let lo = arg1.and_then(|x| literal_value(m, arena, x));
                        let hi = arg2.and_then(|x| literal_value(m, arena, x));
                        match (lo, hi) {
                            (Some(lo), Some(hi)) if lo <= hi => {}
                            _ => return Err(format!("rule 5: {}", at("a clamp whose bounds are not literals in order: write min(max(e, low), high)".into()))),
                        }
                    }
                    used.insert(match fun {
                        F::Min => if s { Op::MinI32 } else { Op::MinU32 },
                        F::Max => if s { Op::MaxI32 } else { Op::MaxU32 },
                        F::Clamp => if s { Op::ClampI32 } else { Op::ClampU32 },
                        F::Abs => Op::AbsI32,
                        F::Sign => Op::SignI32,
                        F::CountLeadingZeros => if s { Op::CountLeadingZerosI32 } else { Op::CountLeadingZerosU32 },
                        F::CountTrailingZeros => Op::CountTrailingZerosU32,
                        F::CountOneBits => Op::CountOneBitsU32,
                        F::ReverseBits => Op::ReverseBitsU32,
                        F::FirstLeadingBit => if s { Op::FirstLeadingBitI32 } else { Op::FirstLeadingBitU32 },
                        F::FirstTrailingBit => Op::FirstTrailingBitU32,
                        F::ExtractBits => if s { Op::ExtractBitsI32 } else { Op::ExtractBitsU32 },
                        F::InsertBits => if s { Op::InsertBitsI32 } else { Op::InsertBitsU32 },
                        _ => unreachable!(),
                    });
                }
                Expression::As { expr, kind, convert } => {
                    let (from, _) = kind_of(m, fi, expr);
                    let ok = |k: Option<ScalarKind>| matches!(k, Some(ScalarKind::Sint | ScalarKind::Uint | ScalarKind::Bool));
                    if !ok(Some(kind)) || !ok(from) || convert.is_some_and(|w| w != 4) {
                        return Err(format!("rule 4: {}", at(format!("a conversion from {from:?} to {kind:?} ({convert:?})"))));
                    }
                    if convert.is_some() {
                        used.insert(match (from, kind) {
                            (Some(ScalarKind::Bool), _) => Op::U32OfBool,
                            (Some(ScalarKind::Sint), ScalarKind::Uint) => Op::U32OfI32,
                            (Some(ScalarKind::Uint), ScalarKind::Sint) => Op::I32OfU32,
                            _ => continue,
                        });
                    }
                }
                ref other => return Err(format!("rule 4: {}", at(format!("the expression {other:?}")))),
            }
        }
    }
    Ok(used)
}

/// Step 6, recursively.
fn statements(m: &Module, fi: &naga::valid::FunctionInfo, block: &Block, name: &str) -> Check {
    for s in block.iter() {
        match s {
            // An `atomicStore`: on a word an atomic also reaches, the result is order-dependent.
            Statement::Store { pointer, .. } if points_at_atomic(m, fi, *pointer) => {
                return Err(format!("rule 6: in `{name}`, an atomic word is stored to (atomicStore)"));
            }
            // Whether its result is read is the expression rule's (rule 6 there).
            Statement::Atomic { fun, .. } => {
                if !matches!(fun, AtomicFunction::InclusiveOr) {
                    return Err(format!("rule 6: in `{name}`, the atomic operation {fun:?}"));
                }
            }
            Statement::ControlBarrier(_) | Statement::MemoryBarrier(_) | Statement::WorkGroupUniformLoad { .. } => return Err(format!("rule 6: in `{name}`, a barrier")),
            Statement::Block(b) => statements(m, fi, b, name)?,
            Statement::If { accept, reject, .. } => {
                statements(m, fi, accept, name)?;
                statements(m, fi, reject, name)?;
            }
            Statement::Switch { cases, .. } => {
                for c in cases {
                    statements(m, fi, &c.body, name)?;
                }
            }
            Statement::Loop { body, continuing, .. } => {
                statements(m, fi, body, name)?;
                statements(m, fi, continuing, name)?;
            }
            Statement::Emit(_) | Statement::Break | Statement::Continue | Statement::Return { .. } | Statement::Store { .. } | Statement::Call { .. } => {}
            other => return Err(format!("rule 4: in `{name}`, the statement {other:?}")),
        }
    }
    Ok(())
}

/// What one module was found to use.
struct Found {
    module: Module,
    info: ModuleInfo,
    used: BTreeSet<Op>,
}

/// Rules 1–7 on one module's text; `kernel` is false only for the semantics module.
fn check(text: &str, kernel: bool) -> Check<Found> {
    let (module, info) = compile(text)?;
    interface(&module)?;
    types(&module, &info)?;
    let used = expressions(&module, &info, kernel)?;
    for (name, f, fi) in functions(&module, &info) {
        statements(&module, fi, &f.body, &name)?;
    }
    Ok(Found { module, info, used })
}

fn msl_text(f: &Found, int_div_checks: bool) -> Check<String> {
    let options = msl::Options { lang_version: (2, 4), emit_int_div_checks: int_div_checks, ..Default::default() };
    msl::write_string(&f.module, &f.info, &options, &msl::PipelineOptions::default()).map(|(s, _)| s).map_err(|e| format!("rule 8: MSL: {e}"))
}

fn hlsl_text(f: &Found) -> Check<String> {
    let mut s = String::new();
    hlsl::Writer::new(&mut s, &hlsl::Options::default(), &hlsl::PipelineOptions::default()).write(&f.module, &f.info, None).map_err(|e| format!("rule 8: HLSL: {e}"))?;
    Ok(s)
}

/// Rule 8's signed arithmetic: naga writes a signed add, subtract or multiply through
/// unsigned, `as_type<int>(as_type<uint>(a) + ...)` in MSL and `asint(asuint(a) + ...)` in
/// HLSL. The nesting is what is looked for: a bare bitcast (`bitcast<u32>(i32)`) gives the
/// inner form alone, and is no evidence of the wrapping.
fn signed_guards(name: &str, u: &BTreeSet<Op>, m: &str, h: &str) -> Check {
    let scalar = [Op::AddI32, Op::SubI32, Op::MulI32].iter().any(|o| u.contains(o));
    let vector = u.contains(&Op::MulVec2I32);
    let fail = |lang: &str, what: &str| Err(format!("rule 8: {name}: the {lang} lacks naga's wrapping of {what} signed arithmetic through unsigned"));
    if scalar && !m.contains("as_type<int>(as_type<uint>(") {
        return fail("MSL", "scalar");
    }
    if vector && !["as_type<metal::int2>(as_type<metal::uint2>(", "as_type<int2>(as_type<uint2>("].iter().any(|p| m.contains(p)) {
        return fail("MSL", "vector");
    }
    if (scalar || vector) && !h.contains("asint(asuint(") {
        return fail("HLSL", "");
    }
    Ok(())
}

/// Rule 8 on one module: the translations, and the guards each must carry.
fn translations(name: &str, f: &Found) -> Check {
    let m = msl_text(f, true)?;
    let h = hlsl_text(f)?;
    spv::write_vec(&f.module, &f.info, &spv::Options::default(), None).map_err(|e| format!("rule 8: {name}: SPIR-V: {e}"))?;
    let u = &f.used;
    let need = |cond: bool, text: &str, pat: &str, lang: &str| -> Check {
        if cond && !text.contains(pat) {
            return Err(format!("rule 8: {name}: the {lang} lacks `{pat}`, the guard for an operation the module uses"));
        }
        Ok(())
    };
    signed_guards(name, u, &m, &h)?;
    let div = [Op::DivU32, Op::DivI32].iter().any(|o| u.contains(o));
    let rem = [Op::RemU32, Op::RemI32].iter().any(|o| u.contains(o));
    for (text, lang) in [(&m, "MSL"), (&h, "HLSL")] {
        need(div, text, "naga_div(", lang)?;
        need(rem, text, "naga_mod(", lang)?;
        need(u.contains(&Op::NegI32), text, "naga_neg(", lang)?;
        need(u.contains(&Op::AbsI32), text, "naga_abs(", lang)?;
    }
    if div || rem {
        let raw = msl_text(f, false)?;
        if raw.contains("naga_div(") || raw.contains("naga_mod(") {
            return Err(format!("rule 8: {name}: the MSL keeps its division guards with emit_int_div_checks off, so this check does not see the switch"));
        }
    }
    Ok(())
}

#[test]
fn every_shipped_module_meets_the_rules() {
    let src = Sources::shipped();
    let mut all = BTreeSet::new();
    for (name, text) in src.named() {
        let kernel = name != "semantics";
        let f = check(text, kernel).unwrap_or_else(|e| panic!("{name}: {e}"));
        translations(name, &f).unwrap_or_else(|e| panic!("{e}"));
        let ops: Vec<&str> = f.used.iter().map(|o| o.name()).collect();
        println!("ops-gpu wgsl rules: {name}: rules 1-8 hold; integer operations used: {}", ops.join(" "));
        if kernel {
            all.extend(f.used);
        }
    }
    let ops: Vec<&str> = all.iter().map(|o| o.name()).collect();
    println!("ops-gpu wgsl rules: the kernels use {} of the suite's operations: {}", all.len(), ops.join(" "));
}

/// Rule 7 the other way: the semantics module evaluates every operation of the suite,
/// so a kernel operation the suite names is one the device is held to.
#[test]
fn the_semantics_module_evaluates_every_operation_of_the_suite() {
    let src = Sources::shipped();
    let f = check(&src.semantics, false).unwrap();
    for op in wai_ops_gpu::semantics::ALL {
        // The conversions u32(i32) and i32(u32) are bit-preserving, as bitcast is; the
        // comparisons with > and >= are those with < and <= on swapped operands.
        assert!(f.used.contains(&op), "the semantics module does not evaluate {op:?}");
    }
}

/// The crate creates every module through `create_shader_module`, which keeps wgpu's
/// run-time checks, the division guards among them, on; never through the unchecked
/// form or with checks of its own choosing.
#[test]
fn the_crate_never_turns_the_translators_checks_off() {
    let dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("src");
    let mut seen = 0;
    for entry in std::fs::read_dir(&dir).unwrap() {
        let p = entry.unwrap().path();
        if p.extension().is_some_and(|e| e == "rs") {
            let text = std::fs::read_to_string(&p).unwrap();
            for (n, line) in text.lines().enumerate() {
                let code = line.split("//").next().unwrap_or("");
                for bad in ["create_shader_module_trusted", "ShaderRuntimeChecks", "create_shader_module_passthrough", "create_shader_module_spirv"] {
                    assert!(!code.contains(bad), "{}:{}: {bad}", p.display(), n + 1);
                }
                seen += code.matches("create_shader_module(").count();
            }
        }
    }
    assert!(seen >= 1, "no module is created through create_shader_module");
}

/// Rule 8 sees naga's wrapping of signed arithmetic, not a bitcast: a translation of
/// `ops32` (which adds signed values) with the wrapping taken out, its bitcasts left, is
/// refused, in MSL and in HLSL.
#[test]
fn rule_8_finds_the_wrapping_of_signed_arithmetic() {
    let src = Sources::shipped();
    let f = check(&src.ops32, true).unwrap();
    assert!(f.used.contains(&Op::AddI32), "ops32 adds signed values");
    let (m, h) = (msl_text(&f, true).unwrap(), hlsl_text(&f).unwrap());
    signed_guards("ops32", &f.used, &m, &h).unwrap();
    let unwrapped = m.replace("as_type<int>(as_type<uint>(", "as_type<int>((");
    assert_ne!(unwrapped, m);
    assert!(unwrapped.contains("as_type<uint>("), "the bitcasts alone remain, which the old check took for the wrapping");
    assert!(signed_guards("ops32", &f.used, &unwrapped, &h).unwrap_err().starts_with("rule 8"));
    let unwrapped = h.replace("asint(asuint(", "asint((");
    assert_ne!(unwrapped, h);
    assert!(signed_guards("ops32", &f.used, &m, &unwrapped).unwrap_err().starts_with("rule 8"));
    println!("ops-gpu wgsl rules: rule 8 found the signed wrapping in ops32's MSL and HLSL, and refused each with it taken out");
}

/// Each violation, planted in a shipped module, is refused by the rule it breaks.
#[test]
fn each_planted_violation_is_refused() {
    let src = Sources::shipped();
    let ops32 = &src.ops32;
    let anchor = "    let v = A[t];\n    switch P.mode {";
    assert_eq!(ops32.matches(anchor).count(), 1);
    let plant = |code: &str| ops32.replacen(anchor, &format!("{code}\n{anchor}"), 1);
    let cases: Vec<(&str, String, &str)> = vec![
        ("a floating-point value", plant("    let fl = f32(P.n) * 0.5;\n    O[t] = u32(fl);"), "rule 3"),
        ("an f16 value", format!("enable f16;\n{}", plant("    let h = f16(A[t]);\n    O[t] = u32(h);")), "rule 1"),
        ("a subgroup reduction", format!("enable subgroups;\n{}", plant("    O[t] = subgroupAdd(A[t]);")), "rule 1"),
        ("an atomicAdd", plant("    atomicAdd(&F[P.flag], 1u);"), "rule 6"),
        ("an atomic's result read", plant("    let old = atomicOr(&F[P.flag], 1u);\n    O[t] = old;"), "rule 6"),
        ("an atomicLoad read into the output", plant("    O[t] = atomicLoad(&F[P.flag]);"), "rule 6"),
        ("an atomicStore", plant("    atomicStore(&F[P.flag], 0u);"), "rule 6"),
        ("atomicOr and atomicStore on one word", plant("    atomicOr(&F[P.flag], 1u);\n    atomicStore(&F[P.flag], 0u);"), "rule 6"),
        ("a storage barrier alone", plant("    storageBarrier();"), "rule 6"),
        ("a workgroup variable and a barrier", format!("var<workgroup> wg: array<u32, 64>;\n{}", plant("    wg[t & 63u] = A[t];\n    workgroupBarrier();")), "rule 2"),
        ("an unmasked shift", plant("    O[t] = A[t] << P.f;"), "rule 5"),
        ("a left shift of a signed value", plant("    O[t] = bitcast<u32>(bitcast<i32>(A[t]) << 31u);"), "rule 5"),
        ("a clamp with run-time bounds", plant("    O[t] = clamp(A[t], P.lo_x, P.hi_x);"), "rule 5"),
        ("a floating-point built-in", plant("    O[t] = u32(sqrt(f32(A[t])));"), "rule 3"),
    ];
    for (what, text, rule) in &cases {
        assert_ne!(text, ops32, "{what}: the plant did not change the text");
        match check(text, true) {
            Ok(_) => panic!("{what}: the rules accepted it"),
            Err(e) => {
                assert!(e.starts_with(rule), "{what}: refused, but by `{e}`, not {rule}");
                println!("ops-gpu wgsl rules: planted {what}: refused: {}", e.lines().next().unwrap_or(""));
            }
        }
    }
    // And the shift rule reads the masks the kernels carry: unmask one of arith.wgsl's.
    let unmasked = ops32.replacen("(a.y << ((32u - s) & 31u))", "(a.y << (32u - s))", 1);
    assert_ne!(&unmasked, ops32);
    let e = check(&unmasked, true).err().expect("an unmasked shift in arith.wgsl was accepted");
    assert!(e.starts_with("rule 5"), "{e}");
}