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]>
97 lines
3.8 KiB
YAML
97 lines
3.8 KiB
YAML
name: wai formal verification (integer core)
|
|
|
|
# The other half of the determinism contract.
|
|
#
|
|
# `wai-byte-equality` establishes byte-exactness by SAMPLING: it decodes fixed
|
|
# vectors on five real OS/arch combinations and asserts identical bytes. That
|
|
# proves the paths agree on the inputs someone thought to write down.
|
|
#
|
|
# This job REASONS instead. It runs a model checker (Kani/CBMC) over the same
|
|
# sources, for every input in a bounded window, and discharges the property the
|
|
# byte-exactness claim actually rests on: arithmetic totality. Rust integer
|
|
# overflow panics in debug and wraps in release, so an overflowing decoder is
|
|
# not one implementation but two, and which one a sink runs depends on how it
|
|
# was compiled. A decoder proved free of overflow, out-of-bounds access and
|
|
# non-termination is a decoder whose bitstream means exactly one thing.
|
|
#
|
|
# This is not redundant with the matrix: the matrix decodes WELL-FORMED vectors,
|
|
# so it cannot see defects that only a malformed or adversarial stream reaches.
|
|
# Four such defects in the bypass escape were found here and fixed, and the
|
|
# harnesses stand so they cannot come back.
|
|
#
|
|
# The proofs are bounded (small symbolic CDFs, fixed-length symbolic streams,
|
|
# explicit unwind limits). Bounded is not universal, and the job claims only
|
|
# what it checks.
|
|
|
|
on:
|
|
pull_request:
|
|
paths:
|
|
- 'wai/wai-verify/**'
|
|
# The verified source itself must be able to fire this job, or a change
|
|
# can regress totality and merge green.
|
|
- 'wai/wai-rs/src/rans.rs'
|
|
- 'wai/wai-rs/src/int_entropy.rs'
|
|
- 'wai/wai-rs/src/int_transform.rs'
|
|
- 'wai/wai-rs/src/wai_video_policy.rs'
|
|
# Not verified by any harness, but #[path]-included because int_transform's
|
|
# IGDN dispatches to it, so it must still compile under the model checker
|
|
# (its cfg(kani) branches are compiled nowhere else).
|
|
- 'wai/wai-rs/src/int_kernels.rs'
|
|
- '.github/workflows/wai-formal-verification.yml'
|
|
push:
|
|
branches:
|
|
- main
|
|
paths:
|
|
- 'wai/wai-verify/**'
|
|
- 'wai/wai-rs/src/rans.rs'
|
|
- 'wai/wai-rs/src/int_entropy.rs'
|
|
- 'wai/wai-rs/src/int_transform.rs'
|
|
- 'wai/wai-rs/src/wai_video_policy.rs'
|
|
- 'wai/wai-rs/src/int_kernels.rs'
|
|
- '.github/workflows/wai-formal-verification.yml'
|
|
|
|
jobs:
|
|
kani:
|
|
runs-on: linux
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
|
|
# dtolnay/rust-toolchain cannot help — it calls `rustup`, which is absent
|
|
# on this runner image.
|
|
- name: Install rustup + toolchain
|
|
run: |
|
|
set -euo pipefail
|
|
if ! command -v rustup >/dev/null; then
|
|
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \
|
|
| sh -s -- -y --profile minimal --default-toolchain 1.98.0
|
|
fi
|
|
echo "$HOME/.cargo/bin" >> "$GITHUB_PATH"
|
|
|
|
# Kani ships its own pinned nightly and a CBMC build; both are slow to
|
|
# fetch, so they are cached on the verifier version.
|
|
- name: Cache Kani toolchain
|
|
uses: actions/cache@v4
|
|
with:
|
|
path: |
|
|
~/.cargo/bin/kani
|
|
~/.cargo/bin/cargo-kani
|
|
~/.kani
|
|
key: kani-0.67.0-${{ runner.os }}
|
|
|
|
- name: Install Kani
|
|
run: |
|
|
set -euo pipefail
|
|
export PATH="$HOME/.cargo/bin:$PATH"
|
|
command -v cargo-kani >/dev/null || cargo install --locked kani-verifier --version 0.67.0
|
|
# Idempotent; fetches the pinned nightly + CBMC on a cold cache.
|
|
cargo kani setup
|
|
|
|
- name: Verify the integer core
|
|
working-directory: wai/wai-verify
|
|
run: |
|
|
set -euo pipefail
|
|
export PATH="$HOME/.cargo/bin:$PATH"
|
|
# Every harness must verify. A failing harness is a real finding
|
|
# about the decoder, so this job is allowed to be the thing that
|
|
# blocks the merge.
|
|
cargo kani
|