//! `wai-ops/1`, the WAI integer operator set (`extensions/integer-operators.md`).
//!
//! - [`xint`]: a 512-bit signed integer with the saturation of §8.1.
//! - [`json`]: a JSON reader (integers of any size, numbers kept as written) and the
//!   canonical writer of §8.5.
//! - [`graph`]: `WHG1` (§10), parsed and written, with load steps 1–6 of §10.5.
//! - [`plan`]: the load-time plan (§10.5 step 7) and the run-time plan (§4).
//! - [`interp`]: the reference interpreter of the graph operators (§5).
//! - [`stage`]: the stage operators E1–E13 (§5E).
//! - [`lower`]: the canonical lowerings of §13.
//! - [`limb32`]: a reference model of a 32-bit fabric's `acc32` products and epilogue.
//! - [`bounds`]: load step 8, the bounds pass (§8.1–§8.3), the verdict and the bounds
//!   certificate (§8.5), and admissible ranges (§8.4).
//! - [`vectors`]: the conformance vector files of §14.1, recomputed from their inputs.
//! - [`generate`]: the generator of `../ops-conformance/`, which writes those files.
//!
//! Every value is an exact integer. Nothing here uses floating point or depends on the
//! target's word size, and nothing wraps except in [`limb32`], whose wrapping 32-bit
//! adds are the fabric's it models, and are proved to give the exact values.
//!
//! A graph loads under a profile ([`graph::load`]): load step 8 runs the bounds pass
//! and refuses a graph whose verdict does not meet that profile (§8.6). The
//! interpreter runs only a [`Loaded`] graph, which only `load` makes, so no entry
//! point decodes a graph its certificate does not admit.
#![no_std]
#![forbid(unsafe_code)]

extern crate alloc;

pub mod bounds;
pub mod code;
pub mod generate;
pub mod graph;
pub mod interp;
pub mod json;
pub mod limb32;
pub mod lower;
pub mod plan;
pub mod sha256;
pub mod stage;
pub mod vectors;
pub mod xint;

// The model checker's harnesses (K1–K33 of the test plan) are in `src/proofs/`, behind
// `#[cfg(kani)]`. `wai-verify` hosts them: it includes this crate's modules by
// `#[path]`, beside the `wai-rs` sources one of them is checked against, so they are
// compiled there and not here.

pub use bounds::Profile;
pub use code::{Code, Refusal, Site};
pub use graph::{Graph, Loaded};
pub use interp::{Kernels, Sequence, Tensor, run, run_with};