5bd1cb9470
The cargo-class build and the library tests add staged and the integer media features; the fast-kernel steps (overflow checks on and off) add staged and run the wai stage tests; staged is checked alone and for wasm32; the corpus loop verifies staged-conformance on every leg; staged_verify.py runs beside the other independent verifiers. The byte-equality job fires on the staged sources it includes and on the corpus, and the proof job on the two staged sources its harnesses cover. Co-Authored-By: Claude Opus 5.5 <[email protected]>
101 lines
4 KiB
YAML
101 lines
4 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'
|
|
- 'wai/wai-rs/src/staged/predict.rs'
|
|
- 'wai/wai-rs/src/staged/wir1_arith.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/staged/predict.rs'
|
|
- 'wai/wai-rs/src/staged/wir1_arith.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
|