93bd919e12
wai-ops: interp::Kernels, a host's kernels for some operators (integer- operators §6), and run_with, which asks the host first for each operator and computes it itself where the host declines; the plan, every check and range policy, the state and every refusal stay the interpreter's. interp::rq exposes the requantisation so a host's outputs are the interpreter's. run and run_observed are unchanged (interp::Reference, a host that has none). wai-rs int_ops: Host lends the interpreter this crate's fast convolution and transposed convolution (int_kernels::conv_acc_i128, each output finished with interp::rq) under a fast Policy, and declines under the reference policy, for geometry the kernel does not cover, operands past its bound, or a value that would leave i64. run1 runs through it. Retargeted equivalence, both halves against the interpreter: - per operator (int_ops::equivalence): 400 random convolutions and transposed convolutions, every rounding mode, bias kind and multiplier choice, under every fast policy against the interpreter alone; the fast kernel must actually run; a check range refuses before any kernel; - per decoder (tests/int_synth_ops.rs): every committed int_synth vector, and the fixtures' base, through the lowering under the reference and four fast policies, the same bytes. The inverse-GDN arm the draft had waits for M4. Co-Authored-By: Claude Opus 5.5 <[email protected]>
52 lines
2.2 KiB
Rust
52 lines
2.2 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).
|
||
//! - [`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};
|