//! 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 bound globals are exactly the six
//!    bindings of `wgsl/common.wgsl`; there is no private memory; and every workgroup
//!    variable is an array of a fixed number of `i32` or `u32` words (no atomic).
//! 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`, on a word of the flag binding, 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. The one barrier is `workgroupBarrier`, in an entry point:
//!    no storage or texture barrier, no `workgroupUniformLoad`.
//! 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. A module with a `workgroupBarrier` carries
//!    it as MSL's `threadgroup_barrier(mem_threadgroup)` and HLSL's
//!    `GroupMemoryBarrierWithGroupSync()`.
//! 9. Workgroup memory is used only in the form determinism-tiers item 3 admits (decision
//!    D76), so that every read of it has one possible value:
//!    - **uniformity**: every `workgroupBarrier` is reached in uniform control flow over
//!      the workgroup, by an analysis of this test's own that is stricter than WGSL's
//!      (§15.2): a value is uniform only when built from literals, constants, the record,
//!      the read-only bindings at uniform indices, `workgroup_id`, `num_workgroups`, and
//!      local variables every store to which is of a uniform value in uniform control
//!      flow; control flow is non-uniform inside a branch or a loop whose condition is not
//!      uniform, for the rest of a loop's body and its later iterations after a `break` or
//!      `continue` in non-uniform control flow, and for the rest of the entry point after
//!      a `return` in it. (naga's own analysis, which rule 1 runs, does not refuse a
//!      barrier in non-uniform control flow: this one does.)
//!    - **one writer a word**: every write to a workgroup array is at the invocation's
//!      `local_invocation_index` (the array at least the workgroup's size), or at a
//!      counter that starts there, steps by the workgroup's size and nothing else, and is
//!      below a literal no greater than the array's length by the guard of the loop it
//!      steps in (`for (var k = li; k < L; k += WG)`, or `k < min(e, L)`): so a word is written only by the
//!      invocation whose index is its own modulo the workgroup's size, and every write is
//!      in bounds. Only entry points write workgroup memory; a function may read it.
//!    - **a barrier between a write and a read**: no stretch of an entry point that a path
//!      can run without passing a `workgroupBarrier` (through branches, around loops, into
//!      the functions it calls) both writes and reads the same workgroup array.
//!
//! 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 storage barrier alone, an unmasked shift, a signed left
//! shift, a run-time `clamp`, and, in workgroup memory, a missing barrier on either side of
//! a tile's read, a barrier in non-uniform control flow, a barrier after a non-uniform
//! return, a loop of barriers bounded by a non-uniform count, a write at a fixed index, a
//! counter guarded past its array, a counter stepping by less than the workgroup, a counter
//! that does not start at the invocation's index, a write in a function, an atomic in
//! workgroup memory, a `workgroupUniformLoad`, a non-uniform store into a loop's count) is
//! shown to be refused, by the rule it breaks; and a tiled kernel in the admitted form is
//! shown to pass.

use std::collections::{BTreeMap, BTreeSet};

use naga::back::{hlsl, msl, spv};
use naga::valid::{Capabilities, ModuleInfo, ValidationFlags, Validator};
use naga::{AddressSpace, AtomicFunction, Barrier, BinaryOperator, Binding, Block, BuiltIn, Expression, Function, GlobalVariable, Handle, Literal, LocalVariable, 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();
        if v.space == AddressSpace::WorkGroup {
            words(m, v.ty).ok_or(format!("rule 2: workgroup variable `{name}` is not an array of a fixed number of i32 or u32 words"))?;
            if v.binding.is_some() {
                return Err(format!("rule 2: workgroup variable `{name}` has a binding"));
            }
            continue;
        }
        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(())
}

/// The length in words of a workgroup array of `i32` or `u32` of a fixed length; `None` for
/// any other type (an atomic, a vector, a structure, an array of run-time length).
fn words(m: &Module, ty: Handle<naga::Type>) -> Option<u32> {
    match m.types[ty].inner {
        TypeInner::Array { base, size: naga::ArraySize::Constant(n), .. } => match m.types[base].inner {
            TypeInner::Scalar(s) if matches!(s.kind, ScalarKind::Sint | ScalarKind::Uint) && s.width == 4 => Some(n.get()),
            _ => None,
        },
        _ => None,
    }
}

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. `f` is the function the block is in; `entry` whether it is an entry
/// point.
fn statements(m: &Module, f: &Function, fi: &naga::valid::FunctionInfo, block: &Block, name: &str, entry: bool) -> 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, pointer, .. } => {
                if !matches!(fun, AtomicFunction::InclusiveOr) {
                    return Err(format!("rule 6: in `{name}`, the atomic operation {fun:?}"));
                }
                let on_flags = matches!(root(&f.expressions, *pointer), Root::Global(g) if matches!(m.global_variables[g].space, AddressSpace::Storage { .. }));
                if !on_flags {
                    return Err(format!("rule 6: in `{name}`, an atomic operation on a word outside the flag binding"));
                }
            }
            Statement::ControlBarrier(b) if *b == Barrier::WORK_GROUP && entry => {}
            Statement::ControlBarrier(b) if *b == Barrier::WORK_GROUP => return Err(format!("rule 6: in `{name}`, a workgroupBarrier outside an entry point")),
            Statement::ControlBarrier(b) | Statement::MemoryBarrier(b) => return Err(format!("rule 6: in `{name}`, a barrier other than workgroupBarrier ({b:?})")),
            Statement::WorkGroupUniformLoad { .. } => return Err(format!("rule 6: in `{name}`, a workgroupUniformLoad")),
            Statement::Block(b) => statements(m, f, fi, b, name, entry)?,
            Statement::If { accept, reject, .. } => {
                statements(m, f, fi, accept, name, entry)?;
                statements(m, f, fi, reject, name, entry)?;
            }
            Statement::Switch { cases, .. } => {
                for c in cases {
                    statements(m, f, fi, &c.body, name, entry)?;
                }
            }
            Statement::Loop { body, continuing, .. } => {
                statements(m, f, fi, body, name, entry)?;
                statements(m, f, fi, continuing, name, entry)?;
            }
            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 and 9 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)?;
    let n_fn = module.functions.len();
    for (k, (name, f, fi)) in functions(&module, &info).into_iter().enumerate() {
        statements(&module, f, fi, &f.body, &name, k >= n_fn)?;
    }
    workgroup_form(&module)?;
    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"));
        }
    }
    if has_barrier(&f.module) {
        need(true, &m, "threadgroup_barrier(metal::mem_flags::mem_threadgroup)", "MSL")?;
        need(true, &h, "GroupMemoryBarrierWithGroupSync()", "HLSL")?;
    }
    Ok(())
}

/// Whether any entry point of the module has a `workgroupBarrier`.
fn has_barrier(m: &Module) -> bool {
    fn any(b: &Block) -> bool {
        b.iter().any(|s| match s {
            Statement::ControlBarrier(_) => true,
            Statement::Block(b) => any(b),
            Statement::If { accept, reject, .. } => any(accept) || any(reject),
            Statement::Switch { cases, .. } => cases.iter().any(|c| any(&c.body)),
            Statement::Loop { body, continuing, .. } => any(body) || any(continuing),
            _ => false,
        })
    }
    m.entry_points.iter().any(|e| any(&e.function.body))
}

// ---------------------------------------------------------------------------------------
// Rule 9: workgroup memory in the one form determinism-tiers item 3 admits (decision D76).
// ---------------------------------------------------------------------------------------

/// The memory a pointer expression reaches: the variable at the root of its access chain.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
enum Root {
    Global(Handle<GlobalVariable>),
    Local(Handle<LocalVariable>),
    Other,
}

fn root(arena: &naga::Arena<Expression>, mut p: Handle<Expression>) -> Root {
    loop {
        match arena[p] {
            Expression::Access { base, .. } | Expression::AccessIndex { base, .. } => p = base,
            Expression::GlobalVariable(g) => return Root::Global(g),
            Expression::LocalVariable(l) => return Root::Local(l),
            _ => return Root::Other,
        }
    }
}

/// Every statement of a block, depth first, with the loops that enclose it (innermost
/// last) as `(the loop's body, its continuing block)`.
fn each_statement<'a>(b: &'a Block, f: &mut dyn FnMut(&'a Statement)) {
    for s in b.iter() {
        f(s);
        match s {
            Statement::Block(b) => each_statement(b, f),
            Statement::If { accept, reject, .. } => {
                each_statement(accept, f);
                each_statement(reject, f);
            }
            Statement::Switch { cases, .. } => {
                for c in cases {
                    each_statement(&c.body, f);
                }
            }
            Statement::Loop { body, continuing, .. } => {
                each_statement(body, f);
                each_statement(continuing, f);
            }
            _ => {}
        }
    }
}

/// What a function (not an entry point) does with workgroup memory and with values that are
/// not uniform: the workgroup arrays it reads, itself or through the functions it calls, and
/// whether its result can differ between invocations given uniform arguments.
#[derive(Clone, Default)]
struct Summary {
    reads: BTreeSet<Handle<GlobalVariable>>,
    nonuniform: bool,
}

/// Whether loads through a global are the same in every invocation: the record (uniform) and
/// the read-only bindings, which no invocation of the dispatch writes (WGSL §15.2.8: a
/// read-only module-scope variable).
fn global_uniform(m: &Module, g: Handle<GlobalVariable>) -> bool {
    match m.global_variables[g].space {
        AddressSpace::Uniform => true,
        AddressSpace::Storage { access } => !access.contains(StorageAccess::STORE),
        _ => false,
    }
}

fn summaries(m: &Module) -> Check<Vec<Summary>> {
    let mut out: Vec<Summary> = Vec::with_capacity(m.functions.len());
    for (_, f) in m.functions.iter() {
        let name = f.name.clone().unwrap_or_default();
        let mut s = Summary::default();
        let arena = &f.expressions;
        for (_, e) in arena.iter() {
            match *e {
                Expression::Load { pointer } => match root(arena, pointer) {
                    Root::Global(g) if m.global_variables[g].space == AddressSpace::WorkGroup => {
                        s.reads.insert(g);
                        s.nonuniform = true;
                    }
                    Root::Global(g) if !global_uniform(m, g) => s.nonuniform = true,
                    Root::Global(_) | Root::Local(_) => {}
                    // A pointer argument: its memory is the caller's.
                    Root::Other => s.nonuniform = true,
                },
                Expression::AtomicResult { .. } | Expression::WorkGroupUniformLoadResult { .. } => s.nonuniform = true,
                _ => {}
            }
        }
        let mut err = None;
        each_statement(&f.body, &mut |st| match st {
            Statement::Store { pointer, .. } => {
                if let Root::Global(g) = root(arena, *pointer)
                    && m.global_variables[g].space == AddressSpace::WorkGroup
                {
                    err.get_or_insert(format!("rule 9: the function `{name}` writes workgroup memory; only an entry point may"));
                }
            }
            Statement::Call { function, .. } => {
                let c: &Summary = &out[function.index()];
                s.reads.extend(c.reads.iter().copied());
                s.nonuniform |= c.nonuniform;
            }
            _ => {}
        });
        if let Some(e) = err {
            return Err(e);
        }
        out.push(s);
    }
    Ok(out)
}

/// The uniformity analysis of one entry point (module docs, rule 9).
struct Uniformity<'a> {
    m: &'a Module,
    f: &'a Function,
    sums: &'a [Summary],
    /// The entry point's arguments that are uniform built-ins.
    arg_uniform: Vec<bool>,
    /// Local variables shown not to be uniform: a store of a value that is not, or a store
    /// in non-uniform control flow.
    var_bad: Vec<bool>,
    /// Each expression's uniformity, for the current `var_bad`.
    u: Vec<bool>,
    /// A `return` was reached in non-uniform control flow: the rest of the entry point is.
    diverged: bool,
    errors: BTreeSet<String>,
}

impl<'a> Uniformity<'a> {
    fn exprs(&mut self) {
        let arena = &self.f.expressions;
        // Each call's result, and the arguments it was called with.
        let mut calls: BTreeMap<Handle<Expression>, Vec<Handle<Expression>>> = BTreeMap::new();
        each_statement(&self.f.body, &mut |st| {
            if let Statement::Call { arguments, result: Some(r), .. } = st {
                calls.insert(*r, arguments.clone());
            }
        });
        let mut u = vec![false; arena.len()];
        for (h, e) in arena.iter() {
            let g = |x: Handle<Expression>| x.index() < h.index() && u[x.index()];
            let v = match *e {
                Expression::Literal(_) | Expression::Constant(_) | Expression::Override(_) | Expression::ZeroValue(_) => true,
                Expression::FunctionArgument(i) => self.arg_uniform.get(i as usize).copied().unwrap_or(false),
                // An address: the same in every invocation. Whether what is loaded through it
                // is, is the load's.
                Expression::GlobalVariable(_) | Expression::LocalVariable(_) => true,
                Expression::Access { base, index } => g(base) && g(index),
                Expression::AccessIndex { base, .. } => g(base),
                Expression::Load { pointer } => {
                    g(pointer)
                        && match root(arena, pointer) {
                            Root::Global(v) => global_uniform(self.m, v),
                            Root::Local(l) => !self.var_bad[l.index()],
                            Root::Other => false,
                        }
                }
                Expression::Unary { expr, .. } | Expression::As { expr, .. } | Expression::ArrayLength(expr) => g(expr),
                Expression::Splat { value, .. } => g(value),
                Expression::Swizzle { vector, .. } => g(vector),
                Expression::Relational { argument, .. } => g(argument),
                Expression::Binary { left, right, .. } => g(left) && g(right),
                Expression::Select { condition, accept, reject } => g(condition) && g(accept) && g(reject),
                Expression::Math { arg, arg1, arg2, arg3, .. } => g(arg) && [arg1, arg2, arg3].into_iter().flatten().all(g),
                Expression::Compose { ref components, .. } => components.iter().all(|&x| g(x)),
                Expression::CallResult(fun) => !self.sums[fun.index()].nonuniform && calls.get(&h).is_some_and(|args| args.iter().all(|&x| g(x))),
                _ => false,
            };
            u[h.index()] = v;
        }
        self.u = u;
    }

    /// Walk a block entered in uniform control flow where `cf_in` holds; whether it can leave
    /// its loop (`break`, `continue`) or the entry point (`return`) in control flow that is
    /// not uniform.
    fn block(&mut self, blk: &Block, cf_in: bool) -> bool {
        let mut cf = cf_in;
        let mut exits = false;
        for s in blk.iter() {
            let now = cf && !self.diverged;
            match s {
                Statement::Store { pointer, value } => {
                    if let Root::Local(l) = root(&self.f.expressions, *pointer)
                        && !(now && self.u[value.index()] && self.u[pointer.index()])
                    {
                        self.var_bad[l.index()] = true;
                    }
                }
                Statement::ControlBarrier(_) => {
                    if !now {
                        self.errors.insert("rule 9: a workgroupBarrier in control flow that is not uniform over the workgroup".into());
                    }
                }
                Statement::Return { .. } => {
                    if !now {
                        self.diverged = true;
                    }
                    return exits || !now;
                }
                Statement::Break | Statement::Continue => return exits || !now,
                Statement::Block(inner) => {
                    if self.block(inner, now) {
                        exits = true;
                        cf = false;
                    }
                }
                Statement::If { condition, accept, reject } => {
                    let c = now && self.u[condition.index()];
                    let a = self.block(accept, c);
                    let r = self.block(reject, c);
                    if a || r {
                        exits = true;
                        cf = false;
                    }
                }
                Statement::Switch { selector, cases } => {
                    let c = now && self.u[selector.index()];
                    for case in cases {
                        if self.block(&case.body, c) {
                            exits = true;
                            cf = false;
                        }
                    }
                }
                Statement::Loop { body, continuing, break_if } => {
                    let mut start = now;
                    loop {
                        let was = self.diverged;
                        let body_exits = self.block(body, start);
                        let cont_exits = self.block(continuing, start && !body_exits);
                        let bi = break_if.is_none_or(|e| self.u[e.index()]);
                        let nonuniform = body_exits || cont_exits || !bi || (self.diverged && !was);
                        if nonuniform && start {
                            start = false;
                            continue;
                        }
                        break;
                    }
                    // A loop that does not return reconverges (WGSL §15.2.6, a loop of
                    // behaviour {Next}); after a non-uniform return the entry point has not.
                }
                _ => {}
            }
        }
        exits
    }
}

/// One entry point's phases: the workgroup arrays read and written since the last barrier
/// on some path, and the write form (module docs, rule 9).
struct Phases<'a> {
    m: &'a Module,
    f: &'a Function,
    sums: &'a [Summary],
    name: String,
    /// The workgroup arrays and their lengths in words.
    arrays: &'a BTreeMap<Handle<GlobalVariable>, u32>,
    /// The workgroup's size, and the argument that is `local_invocation_index`.
    wg: u32,
    li: Option<u32>,
    /// The local variables that are counters: every store to them is of `li` or of
    /// themselves plus the workgroup's size.
    counters: BTreeSet<Handle<LocalVariable>>,
    /// The guards of the loops enclosing the current statement: `(counter, bound)` where
    /// the loop's body begins `if (counter < bound) {} else { break; }` and does not store
    /// to the counter.
    guards: Vec<Option<(Handle<LocalVariable>, u32)>>,
    error: Option<String>,
}

type Open = BTreeSet<(Handle<GlobalVariable>, bool)>;

struct PhOut {
    fall: Option<Open>,
    brk: Open,
    cont: Open,
}

impl<'a> Phases<'a> {
    fn access(&mut self, open: &mut Open, g: Handle<GlobalVariable>, write: bool) {
        if open.contains(&(g, !write)) && self.error.is_none() {
            let var = self.m.global_variables[g].name.clone().unwrap_or_default();
            let (now, then) = if write { ("written", "read") } else { ("read", "written") };
            self.error = Some(format!("rule 9: in `{}`, the workgroup array `{var}` is {now} where a path from a place it is {then} passes no workgroupBarrier", self.name));
        }
        open.insert((g, write));
    }

    /// The literal or constant value of an expression.
    fn literal(&self, h: Handle<Expression>) -> Option<i64> {
        literal_value(self.m, &self.f.expressions, h)
    }

    /// The local variable an expression loads, if it is a plain load of one.
    fn loads_local(&self, h: Handle<Expression>) -> Option<Handle<LocalVariable>> {
        match self.f.expressions[h] {
            Expression::Load { pointer } => match self.f.expressions[pointer] {
                Expression::LocalVariable(l) => Some(l),
                _ => None,
            },
            _ => None,
        }
    }

    /// A loop's guard (see `guards`).
    fn guard(&self, body: &Block) -> Option<(Handle<LocalVariable>, u32)> {
        let first = body.iter().find(|s| !matches!(s, Statement::Emit(_)))?;
        let Statement::If { condition, accept, reject } = first else { return None };
        if !accept.is_empty() || reject.len() != 1 || !matches!(reject.iter().next(), Some(Statement::Break)) {
            return None;
        }
        let Expression::Binary { op: BinaryOperator::Less, left, right } = self.f.expressions[*condition] else { return None };
        let k = self.loads_local(left)?;
        // `k < L`, or `k < min(e, L)` (either way round), L a literal.
        let bound = match self.f.expressions[right] {
            Expression::Math { fun: MathFunction::Min, arg, arg1: Some(arg1), .. } => self.literal(arg1).or_else(|| self.literal(arg))?,
            _ => self.literal(right)?,
        };
        let bound = u32::try_from(bound).ok()?;
        let mut stored = false;
        each_statement(body, &mut |s| {
            if let Statement::Store { pointer, .. } = s
                && root(&self.f.expressions, *pointer) == Root::Local(k)
            {
                stored = true;
            }
        });
        (!stored).then_some((k, bound))
    }

    fn write_form(&mut self, pointer: Handle<Expression>, g: Handle<GlobalVariable>) {
        let arena = &self.f.expressions;
        let len = self.arrays[&g];
        let var = self.m.global_variables[g].name.clone().unwrap_or_default();
        let ok = match arena[pointer] {
            Expression::Access { base, index } if matches!(arena[base], Expression::GlobalVariable(_)) => match arena[index] {
                Expression::FunctionArgument(i) if Some(i) == self.li => self.wg <= len,
                _ => match self.loads_local(index) {
                    Some(k) => self.counters.contains(&k) && self.guards.iter().flatten().any(|&(gk, bound)| gk == k && bound <= len),
                    None => false,
                },
            },
            _ => false,
        };
        if !ok && self.error.is_none() {
            self.error = Some(format!(
                "rule 9: in `{}`, a write to the workgroup array `{var}` is not at the invocation's index, nor at a counter from it stepping by the workgroup's size and guarded below the array's length",
                self.name
            ));
        }
    }

    fn block(&mut self, b: &Block, mut open: Open) -> PhOut {
        let mut out = PhOut { fall: None, brk: Open::new(), cont: Open::new() };
        for s in b.iter() {
            match s {
                Statement::Emit(range) => {
                    for h in range.clone() {
                        if let Expression::Load { pointer } = self.f.expressions[h]
                            && let Root::Global(g) = root(&self.f.expressions, pointer)
                            && self.arrays.contains_key(&g)
                        {
                            self.access(&mut open, g, false);
                        }
                    }
                }
                Statement::Store { pointer, .. } => {
                    if let Root::Global(g) = root(&self.f.expressions, *pointer)
                        && self.arrays.contains_key(&g)
                    {
                        self.write_form(*pointer, g);
                        self.access(&mut open, g, true);
                    }
                }
                Statement::Call { function, .. } => {
                    let reads: Vec<Handle<GlobalVariable>> = self.sums[function.index()].reads.iter().copied().collect();
                    for g in reads {
                        self.access(&mut open, g, false);
                    }
                }
                Statement::ControlBarrier(_) => open.clear(),
                Statement::Return { .. } => return out,
                Statement::Break => {
                    out.brk.extend(open);
                    return out;
                }
                Statement::Continue => {
                    out.cont.extend(open);
                    return out;
                }
                Statement::Block(inner) => {
                    let r = self.block(inner, open);
                    out.brk.extend(r.brk);
                    out.cont.extend(r.cont);
                    match r.fall {
                        Some(o) => open = o,
                        None => return out,
                    }
                }
                Statement::If { accept, reject, .. } => {
                    let a = self.block(accept, open.clone());
                    let r = self.block(reject, open);
                    out.brk.extend(a.brk.into_iter().chain(r.brk));
                    out.cont.extend(a.cont.into_iter().chain(r.cont));
                    match (a.fall, r.fall) {
                        (None, None) => return out,
                        (x, y) => open = x.into_iter().chain(y).flatten().collect(),
                    }
                }
                Statement::Switch { cases, .. } => {
                    let mut after: Option<Open> = None;
                    let mut carried: Option<Open> = None;
                    for case in cases {
                        let input: Open = open.iter().copied().chain(carried.take().into_iter().flatten()).collect();
                        let r = self.block(&case.body, input);
                        out.brk.extend(r.brk.iter().copied());
                        out.cont.extend(r.cont);
                        // A `break` in a switch leaves the switch.
                        let leaving: Option<Open> = match r.fall {
                            Some(f) if case.fall_through => {
                                carried = Some(f);
                                None
                            }
                            f => Some(f.into_iter().flatten().chain(r.brk).collect()),
                        };
                        if let Some(l) = leaving {
                            after = Some(after.into_iter().flatten().chain(l).collect());
                        }
                    }
                    match after {
                        Some(a) => open = a,
                        None => return out,
                    }
                }
                Statement::Loop { body, continuing, break_if } => {
                    let gd = self.guard(body);
                    self.guards.push(gd);
                    let entry = open.clone();
                    let mut head = open;
                    let leave = loop {
                        let b = self.block(body, head.clone());
                        let cont_in: Open = b.fall.into_iter().flatten().chain(b.cont).collect();
                        let c = self.block(continuing, cont_in);
                        let c_fall = c.fall.unwrap_or_default();
                        let next: Open = entry.iter().copied().chain(c_fall.iter().copied()).collect();
                        if next == head || self.error.is_some() {
                            let mut leave: Open = b.brk;
                            if break_if.is_some() {
                                leave.extend(c_fall);
                            }
                            break leave;
                        }
                        head = next;
                    };
                    self.guards.pop();
                    open = leave;
                }
                _ => {}
            }
        }
        out.fall = Some(open);
        out
    }
}

/// Rule 9 on one module.
fn workgroup_form(m: &Module) -> Check {
    let arrays: BTreeMap<Handle<GlobalVariable>, u32> = m.global_variables.iter().filter(|(_, v)| v.space == AddressSpace::WorkGroup).filter_map(|(h, v)| words(m, v.ty).map(|n| (h, n))).collect();
    let sums = summaries(m)?;
    for (i, e) in m.entry_points.iter().enumerate() {
        let f = &e.function;
        let builtin = |a: &naga::FunctionArgument| match a.binding {
            Some(Binding::BuiltIn(b)) => Some(b),
            _ => None,
        };
        let arg_uniform: Vec<bool> = f.arguments.iter().map(|a| matches!(builtin(a), Some(BuiltIn::WorkGroupId | BuiltIn::NumWorkGroups))).collect();
        let li = f.arguments.iter().position(|a| builtin(a) == Some(BuiltIn::LocalInvocationIndex)).map(|p| p as u32);
        // Uniformity: a fixed point over the local variables shown not to be uniform.
        let mut un = Uniformity { m, f, sums: &sums, arg_uniform, var_bad: vec![false; f.local_variables.len()], u: Vec::new(), diverged: false, errors: BTreeSet::new() };
        loop {
            let before = un.var_bad.clone();
            un.exprs();
            un.diverged = false;
            un.errors.clear();
            un.block(&f.body, true);
            if un.var_bad == before {
                break;
            }
        }
        if let Some(e) = un.errors.into_iter().next() {
            return Err(format!("{e} (in `{}`)", e_name(m, i)));
        }
        if arrays.is_empty() {
            continue;
        }
        // The counters: every store to them is of `li`, or of themselves plus the size.
        let wg = e.workgroup_size[0];
        let arena = &f.expressions;
        let mut verdict: BTreeMap<Handle<LocalVariable>, bool> = BTreeMap::new();
        each_statement(&f.body, &mut |s| {
            if let Statement::Store { pointer, value } = s
                && let Expression::LocalVariable(k) = arena[*pointer]
            {
                let is_li = matches!(arena[*value], Expression::FunctionArgument(a) if Some(a) == li);
                let is_step = match arena[*value] {
                    Expression::Binary { op: BinaryOperator::Add, left, right } => {
                        let me = |x: Handle<Expression>| matches!(arena[x], Expression::Load { pointer } if arena[pointer] == Expression::LocalVariable(k));
                        let size = |x: Handle<Expression>| literal_value(m, arena, x) == Some(i64::from(wg));
                        (me(left) && size(right)) || (size(left) && me(right))
                    }
                    _ => false,
                };
                let ok = (is_li || is_step) && f.local_variables[k].init.is_none();
                *verdict.entry(k).or_insert(true) &= ok;
            }
        });
        let counters = verdict.into_iter().filter(|&(_, ok)| ok).map(|(k, _)| k).collect();
        let mut ph = Phases { m, f, sums: &sums, name: e_name(m, i), arrays: &arrays, wg, li, counters, guards: Vec::new(), error: None };
        ph.block(&f.body, Open::new());
        if let Some(err) = ph.error {
            return Err(err);
        }
    }
    Ok(())
}

fn e_name(m: &Module, i: usize) -> String {
    m.entry_points[i].name.clone()
}

#[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-9 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; and it never sets a pipeline's
/// `zero_initialize_workgroup_memory`, which is on unless a host turns it off (rule 9's form
/// leans on WGSL's zero initial value of workgroup memory, WGSL §7.3).
#[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", "zero_initialize_workgroup_memory"] {
                    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 written at an index of the global grid, then a barrier after a non-uniform return", format!("var<workgroup> wg: array<u32, 64>;\n{}", plant("    wg[t & 63u] = A[t];\n    workgroupBarrier();")), "rule 9"),
        ("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}");
}

/// A tiled kernel in the form rule 9 admits: each pass loads a tile of `A` into workgroup
/// memory, a word an invocation at a counter's stride, between two barriers, and every
/// invocation reads it, its own words and a neighbour's, after the second.
const TILED: &str = "
var<workgroup> tile: array<u32, 512>;

@compute @workgroup_size(256)
fn tiled(@builtin(local_invocation_index) li: u32, @builtin(workgroup_id) wid: vec3<u32>) {
    let base = wid.x * 256u;
    var acc = 0u;
    for (var c = 0u; c < P.c; c++) {
        workgroupBarrier();
        for (var k = li; k < 512u; k += 256u) {
            tile[k] = A[(c * 512u + k) % max(P.n, 1u)];
        }
        workgroupBarrier();
        acc = acc + tile[li] * tile[(li + 1u) & 511u];
    }
    let t = base + li;
    if (t < P.n) {
        O[t] = acc;
    }
}
";

/// The admitted form passes every rule, its translations carry the barrier, and each way of
/// leaving the form is refused by the rule it breaks.
#[test]
fn rule_9_admits_the_tiled_form_and_refuses_each_way_out_of_it() {
    let src = Sources::shipped();
    let base = format!("{}\n{TILED}", src.ops32);
    let f = check(&base, true).unwrap_or_else(|e| panic!("the admitted form: {e}"));
    translations("tiled", &f).unwrap_or_else(|e| panic!("{e}"));
    assert!(has_barrier(&f.module));
    println!("ops-gpu wgsl rules: rule 9: the tiled form passes rules 1-9, and its MSL and HLSL carry the workgroup barrier");
    let second = "        }\n        workgroupBarrier();\n        acc =";
    let first = "        workgroupBarrier();\n        for (var k";
    assert_eq!(base.matches(second).count(), 1);
    assert_eq!(base.matches(first).count(), 1);
    let edit = |from: &str, to: &str| {
        assert_eq!(base.matches(from).count(), 1, "{from:?} is not once in the base");
        base.replacen(from, to, 1)
    };
    let cases: Vec<(&str, String, &str)> = vec![
        ("a tile read with no barrier after its write", edit(second, "        }\n        acc ="), "rule 9: in `tiled`, the workgroup array `tile` is read"),
        ("a tile written with no barrier after the last pass's read", edit(first, "        for (var k"), "rule 9: in `tiled`, the workgroup array `tile` is written"),
        ("a barrier in non-uniform control flow", edit(second, "        }\n        if (li < 128u) {\n            workgroupBarrier();\n        }\n        acc ="), "rule 9: a workgroupBarrier in control flow"),
        ("a barrier after a non-uniform return", edit("    let base = wid.x * 256u;\n", "    let base = wid.x * 256u;\n    if (base + li >= P.n) {\n        return;\n    }\n"), "rule 9: a workgroupBarrier in control flow"),
        ("a loop of barriers bounded by a non-uniform count", edit("c < P.c;", "c < P.c + (li & 1u);"), "rule 9: a workgroupBarrier in control flow"),
        ("a non-uniform store into a loop's count", edit("    var acc = 0u;\n    for (var c = 0u; c < P.c; c++) {", "    var acc = 0u;\n    var n = P.c;\n    if (li == 0u) {\n        n = 1u;\n    }\n    for (var c = 0u; c < n; c++) {"), "rule 9: a workgroupBarrier in control flow"),
        ("a tile written at an index other than the counter", edit("tile[k] = ", "tile[k & 7u] = "), "rule 9: in `tiled`, a write to the workgroup array `tile` is not"),
        ("a counter guarded past its array", edit("k < 512u;", "k < 513u;"), "rule 9: in `tiled`, a write to the workgroup array `tile` is not"),
        ("a counter stepping by less than the workgroup", edit("k += 256u", "k += 128u"), "rule 9: in `tiled`, a write to the workgroup array `tile` is not"),
        ("a counter that does not start at the invocation's index", edit("var k = li;", "var k = li + 1u;"), "rule 9: in `tiled`, a write to the workgroup array `tile` is not"),
        ("a tile written by a function", format!("{}\nfn put(i: u32, v: u32) {{\n    tile[i] = v;\n}}\n", edit("tile[k] = A[(c * 512u + k) % max(P.n, 1u)];", "put(k, A[(c * 512u + k) % max(P.n, 1u)]);")), "rule 9: the function `put` writes workgroup memory"),
        ("a tile read through a function with no barrier after its write", format!("{}\nfn tile_at(i: u32) -> u32 {{\n    return tile[i];\n}}\n", edit(&format!("{second} acc + tile[li] * tile[(li + 1u) & 511u];"), "        }\n        acc = acc + tile_at(li) * tile_at((li + 1u) & 511u);")), "rule 9: in `tiled`, the workgroup array `tile` is read"),
        ("an atomic in workgroup memory", format!("var<workgroup> wa: atomic<u32>;\n{}", edit("        acc = acc + tile[li]", "        atomicOr(&wa, 1u);\n        acc = acc + tile[li]")), "rule 2: workgroup variable `wa`"),
        ("a storage barrier in place of the workgroup barrier", edit(second, "        }\n        storageBarrier();\n        acc ="), "rule 6"),
        ("a workgroupUniformLoad", format!("var<workgroup> wn: array<u32, 4>;\n{}", edit("        acc = acc + tile[li]", "        acc = acc + workgroupUniformLoad(&wn)[0];\n        acc = acc + tile[li]")), "rule "),
    ];
    for (what, text, want) in &cases {
        assert_ne!(text, &base, "{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(want), "{what}: refused, but by `{e}`, not `{want}`");
                println!("ops-gpu wgsl rules: planted {what}: refused: {}", e.lines().next().unwrap_or(""));
            }
        }
    }
    println!("ops-gpu wgsl rules: rule 9: {} planted ways out of the tiled form, each refused by the rule it breaks", cases.len());
}

/// Each barrier of the shipped tiled kernels (`conv_tile` and `igdn_tile` of `wgsl/tile.wgsl`)
/// taken out in turn leaves a stretch that writes and reads their workgroup array, and rule 9
/// refuses it: the planted fault "a missing barrier" in the tiled kernels is the rules check's to
/// catch.
#[test]
fn a_barrier_taken_out_of_the_tiled_kernel_is_refused() {
    let src = Sources::shipped();
    let start = src.ops64.find("fn conv_tile(").expect("ops64 has the tiled kernel");
    let at: Vec<usize> = src.ops64[start..].match_indices("workgroupBarrier();").map(|(i, _)| i + start).collect();
    assert!(at.len() >= 10, "the tiled kernels have {} barriers", at.len());
    for (k, &i) in at.iter().enumerate() {
        let text = format!("{}{}", &src.ops64[..i], &src.ops64[i + "workgroupBarrier();".len()..]);
        let e = check(&text, true).err().unwrap_or_else(|| panic!("barrier {k} of conv_tile taken out: the rules accepted it"));
        assert!(e.starts_with("rule 9: in `conv_tile`") || e.starts_with("rule 9: in `igdn_tile`"), "barrier {k} taken out: refused, but by `{e}`");
        println!("ops-gpu wgsl rules: the tiled kernels without barrier {k}: refused: {e}");
    }
    println!("ops-gpu wgsl rules: each of the tiled kernels' {} barriers taken out is refused by rule 9", at.len());
}