f27109f4d8
WAI's integer decoders ran scalar, single-threaded loops, and no throughput figure existed for them. Integer arithmetic is exact, so the work can be re-partitioned across lanes and threads without changing any result, as long as each output element's arithmetic and overflow behaviour are unchanged. - src/int_kernels.rs holds the fast convolution, transposed-convolution, matmul and elementwise kernels. Each gives the same integer as the scalar reference for every output element. Threading uses std:🧵:scope and is not used on wasm32. - A fast kernel runs only where its own arithmetic cannot overflow and the reference can size its output; operands outside that bound, and geometries where the padded input outgrows the reference's proportion, are handed to the reference kernel. With overflow checks on, the fast path panics where the reference panics; with them off, it returns the same integers. - Equivalence is tested, not argued: every committed integer-decoder vector is decoded under the reference and under each fast policy against its frozen hash (tests/int_kernels_vectors.rs), edge geometry runs through the public decoders (tests/int_kernels_geometry.rs), and wai-conformance runs both in dev and release profiles on every leg. The Kani harnesses are unchanged and still verify. - wai_decode_bench times reference and fast decodes interleaved in one process, best of N. research/decode-throughput.md records the measured figures, the machine and the method, and which benchmarked vectors are trained models; the largest gain is on the int_hyper synthesis topology (synthetic weights). Co-Authored-By: Claude Opus 5.5 <[email protected]>
23 lines
895 B
TOML
23 lines
895 B
TOML
# Formal verification host for WAI's integer core.
|
|
#
|
|
# Deliberately a SEPARATE tiny crate, mirroring `byte-exact-conformance`: it
|
|
# `#[path]`-includes the pure-integer sources from wai-rs (single source of
|
|
# truth, no copy) so the model checker sees a minimal dependency closure —
|
|
# which is what makes the proofs tractable.
|
|
#
|
|
# NOTE: no `rust-version` on purpose. The verifier ships its own pinned nightly
|
|
# toolchain; an MSRV above it makes cargo refuse to build the proof harnesses.
|
|
[package]
|
|
name = "wai-verify"
|
|
version = "0.1.0"
|
|
edition = "2024"
|
|
license = "Apache-2.0"
|
|
publish = false
|
|
|
|
# `cfg(kani)` is set by the model checker on the included sources. Declared so an
|
|
# ordinary build or clippy run of this crate does not warn on it.
|
|
[lints.rust]
|
|
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
|
|
|
|
[dependencies]
|
|
# none — the integer core this crate verifies is pure std.
|