8356268251
Each convolution's term hull and partial-sum interval come from four sums per output channel (least and greatest weight, sum of the positive and of the negative weights; per residue for conv_transpose), and each igdn row folds in i128, wherever no operation of the rule's fold can saturate; elsewhere the rule folds tap by tap as before. The pass before this change is kept, test-only (feature `oracle` for other crates), as bounds_oracle, with a differential over the committed graphs, the pretrained set when present, and random and adversarial operators and graphs. Co-Authored-By: Claude Opus 5.5 <[email protected]>
56 lines
2.5 KiB
Rust
56 lines
2.5 KiB
Rust
//! `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).
|
||
//! - `bounds_oracle` (test-only, or the `oracle` feature): the bounds pass as it stood
|
||
//! before its closed forms, every term folded in 512 bits, which [`bounds`] is held to.
|
||
//! - [`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;
|
||
#[cfg(any(test, feature = "oracle"))]
|
||
pub mod bounds_oracle;
|
||
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};
|