f2513980d8
The arithmetic guards of the direct decodes (their own predictors, and the
saturating step of wir1_arith) no longer run outside the test-only decode;
the stage operators carry them now.
- int_video::predict is E10 on an RGB8 frame (the encoder predicts with it,
as the decode does); the direct predictor, verbatim, is
int_video::legacy::predict, test-only.
- staged::wir1: the direct decode's pred_at and step are legacy's. The
encoder predicts with the decode's E11, E12 or the element below
(ops::prediction) and steps with E9; it refuses a stage below of the wrong
shape or element type up front. ops::{up2_prediction, rate_prediction} are
E11 and E12 on the interleaved layouts, which the staged-measurement and
staged-corpus tools now call.
- staged::predict's up2_at, rate_at, rate_index and rdiv, and the
wir1_arith module, are test-only (legacy_int; and cfg(kani), for the
harnesses that still prove them); rate_len, the rate predictor's geometry,
stays. wai-verify declares legacy_int.
- The predictors' proofs move to the operators a decode runs: wai-ops'
e11_up2_between_its_neighbours, e12_rdiv_matches_its_definition and
e12_rate_at_reads_only_source_samples, in the stage shard.
Gate 6's results, for the record (the switch at 9a377f9b): gate.sh GREEN;
the release fast-kernel step; staged_verify.py and int_payload_verify.py;
wai-web native 32 and wasm32, verify_int_payload_wasm and verify_staged_wasm
(69 of 69 cases, 146 unit stage hashes equal the native ones); include/wai.h
unchanged. Falsified with the switch live: E10's half-pel rounding without
its +1 and E12's rdiv halves toward zero turn the file-based goldens red
(byte-exact wiv1_keyframe_0_payloads_are_byte_identical, video_real frame 2;
int_video_real_footage_exercises_the_half_pel_predictor;
staged_audio_rate_ladder_is_byte_exact; wai-rs int_video_halfpel), and the
corpora (wai_int_payload_vectors verify, FAIL video_real; wai_staged_vectors
verify, the encoder's reconstruction differs from the decode); the Python
verifiers stay green. The decode cloning the previous frame for E10 turns
int_payload_cost red: int_video held 42524 bytes against 35612 declared.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
231 lines
11 KiB
YAML
231 lines
11 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.
|
||
#
|
||
# It also checks the integer operator set (wai/extensions/integer-operators.md):
|
||
# the harnesses of its test plan, in wai/wai-ops/src/proofs/, which the host
|
||
# includes beside the operator set's sources. They prove the roundings, the
|
||
# requantisation, a 32-bit fabric's limb product and epilogue, the soundness of
|
||
# the bound rules against the interpreter, the stage operators' totality and
|
||
# refusal order, the plans, and the graph form's parse. Each harness states its
|
||
# window. The harnesses run in shards; the first job holds the shards to
|
||
# covering every harness exactly once.
|
||
|
||
# One run per branch at a time. A push supersedes the run before it.
|
||
#
|
||
# There is one `macos` runner and it is the dev Mac, so every macOS job in this
|
||
# repo queues on it. With no concurrency group, a session pushing four versions
|
||
# of a branch queued four complete sets of runs and every one of them had to
|
||
# drain: on 2026-10-05 a PR's 21 contexts settled none in 70 minutes behind a
|
||
# backlog of 25 runs, and the queue grew faster than it cleared. Only the newest
|
||
# commit's verdict is wanted, so the older runs are cancelled.
|
||
#
|
||
# Verified on this forge (Forgejo 16.0.5) in `ci-test` before being added here:
|
||
# the key parses, and a newer push moves an older run to `cancelled` even while
|
||
# it is still queued, which is the case that matters.
|
||
#
|
||
# `cancel-in-progress: true` also applies to `main`. That is deliberate and
|
||
# safe here: main advances by merge commits whose tree contains the commits
|
||
# before them, so the newer run covers the older one's changes.
|
||
concurrency:
|
||
group: ${{ github.workflow }}-${{ github.ref }}
|
||
cancel-in-progress: true
|
||
|
||
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'
|
||
# Verified by K10 as the fast path of the reference IGDN, and #[path]-included
|
||
# because int_transform's IGDN dispatches to it, so it must also compile under
|
||
# the model checker (its cfg(kani) branches are compiled nowhere else).
|
||
- 'wai/wai-rs/src/int_kernels.rs'
|
||
# The integer operator set: its sources, which the host includes module by
|
||
# module, and its harnesses (src/proofs/).
|
||
- 'wai/wai-ops/src/**'
|
||
- '.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'
|
||
- 'wai/wai-ops/src/**'
|
||
- '.github/workflows/wai-formal-verification.yml'
|
||
|
||
jobs:
|
||
# Does this pull request's own diff touch the paths below? This forge matches a
|
||
# workflow's `paths:` against the push, so a merge of main into a branch fires the
|
||
# workflow whatever the pull request changes; every job here waits on this answer.
|
||
# A push to main, a schedule, or anything the script cannot determine answers
|
||
# `true` (scripts/pr-touches-paths.py).
|
||
relevant:
|
||
name: does this change touch it
|
||
runs-on: linux-arm64
|
||
outputs:
|
||
run: ${{ steps.gate.outputs.run }}
|
||
steps:
|
||
- uses: actions/checkout@v5
|
||
with:
|
||
fetch-depth: 0
|
||
- id: gate
|
||
run: |
|
||
set -euo pipefail
|
||
r=$(python3 scripts/pr-touches-paths.py .github/workflows/wai-formal-verification.yml \
|
||
"${{ github.event.pull_request.base.sha }}" \
|
||
"${{ github.event.pull_request.head.sha }}")
|
||
echo "this change touches wai-formal-verification: $r"
|
||
echo "run=$r" >> "$GITHUB_OUTPUT"
|
||
|
||
# Every harness the host compiles runs in exactly one shard of the matrix below:
|
||
# one no shard runs would be compiled and never checked. No toolchain is needed;
|
||
# the script reads the included sources and this file.
|
||
shards:
|
||
needs: relevant
|
||
if: needs.relevant.outputs.run == 'true'
|
||
name: every harness in one shard
|
||
runs-on: linux
|
||
timeout-minutes: 10
|
||
steps:
|
||
- uses: actions/checkout@v4
|
||
|
||
- uses: actions/setup-python@v5
|
||
with:
|
||
python-version: '3.11'
|
||
|
||
- name: Every harness runs in exactly one shard
|
||
run: python3 -I wai/wai-verify/check_shards.py .
|
||
|
||
kani:
|
||
needs: relevant
|
||
if: needs.relevant.outputs.run == 'true'
|
||
name: kani (${{ matrix.shard }})
|
||
runs-on: ${{ matrix.os }}
|
||
timeout-minutes: 120
|
||
strategy:
|
||
fail-fast: false
|
||
# Each shard is a list of `--harness` filters: a harness runs when its full name
|
||
# contains one. The integer operator set's harnesses (K1–K33 of its test plan)
|
||
# are in proofs::, split so that no shard runs much past an hour; the two 512-bit
|
||
# isqrt harnesses and the longest stage harnesses have shards of their own.
|
||
# Harnesses gated by cfg(kani_open) are not compiled here.
|
||
#
|
||
# Each shard runs where its memory fits. The rans64 totality proof (k26) peaks at
|
||
# about 28 GiB of resident memory and takes about 690 s of verification (measured
|
||
# with /usr/bin/time -l on a 256 GB host); the linux runner has 15 GiB, shared by
|
||
# two jobs, and CBMC ran out of memory there. It has a shard of its own on the
|
||
# macos runner. Every other shard has run to completion on the linux runner.
|
||
matrix:
|
||
include:
|
||
- { shard: integer-core, os: linux, harness: "rans:: int_entropy:: int_transform:: wai_video_policy:: staged_predict:: staged_wir1_arith::" }
|
||
- { shard: arith, os: linux, harness: "proofs::arith::k01 proofs::arith::k03 proofs::arith::k13_isqrt_u128 proofs::arith::k17 proofs::arith::k32 proofs::limb::" }
|
||
- { shard: isqrt512, os: linux, harness: "proofs::arith::k13_isqrt_i512 proofs::arith::k13_isqrt_ceil_i512" }
|
||
- { shard: stage, os: linux, harness: "proofs::stage::k23 proofs::stage::k27 proofs::stage::k28 proofs::stage::k29_residual_step_32bit_identity_registered proofs::stage::k30 proofs::stage::e11 proofs::stage::e12" }
|
||
- { shard: stage-long, os: linux, harness: "proofs::stage::k29_residual_step_32bit_identity_every_range" }
|
||
- { shard: rans64-t2, os: macos, harness: "proofs::stage::k26" }
|
||
- { shard: sound, os: linux, harness: "proofs::sound::" }
|
||
- { shard: plan, os: linux, harness: "proofs::plan::" }
|
||
steps:
|
||
- uses: actions/checkout@v4
|
||
|
||
# dtolnay/rust-toolchain cannot help — it calls `rustup`, which is absent
|
||
# on the linux runner's image. The macOS runner executes on the host, which
|
||
# has rustup in ~/.cargo/bin, but launchd's PATH omits that directory: it
|
||
# is put first, so the host's install is found and left as it is.
|
||
- name: Install rustup + toolchain
|
||
shell: bash
|
||
run: |
|
||
set -euo pipefail
|
||
export PATH="$HOME/.cargo/bin:$PATH"
|
||
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. Not on macOS: that
|
||
# runner's home is the host's own, where Kani is installed, and a restore
|
||
# would write over a live install.
|
||
- name: Cache Kani toolchain
|
||
if: matrix.os != 'macos'
|
||
uses: actions/cache@v4
|
||
with:
|
||
path: |
|
||
~/.cargo/bin/kani
|
||
~/.cargo/bin/cargo-kani
|
||
~/.kani
|
||
key: kani-0.67.0-${{ runner.os }}
|
||
|
||
# The same steps on every runner: Kani 0.67.0 unless that version is installed,
|
||
# then its setup unless it is set up. Setup fetches the release bundle (CBMC and
|
||
# the driver) and installs the pinned nightly, which the bundle's `toolchain`
|
||
# links to in ~/.rustup. Run again, it fetches and installs both again, so it is
|
||
# skipped when the bundle and its toolchain are both in place: on the macOS
|
||
# host, which is set up, it would rewrite a live install. The cache holds the
|
||
# bundle but not ~/.rustup, so a container sets up every time.
|
||
- name: Install Kani
|
||
shell: bash
|
||
run: |
|
||
set -euo pipefail
|
||
export PATH="$HOME/.cargo/bin:$PATH"
|
||
if [ "$(cargo kani --version 2>/dev/null || true)" != "cargo-kani 0.67.0" ]; then
|
||
cargo install --locked kani-verifier --version 0.67.0
|
||
fi
|
||
k="$HOME/.kani/kani-0.67.0"
|
||
if [ ! -x "$k/bin/kani-driver" ] || [ ! -x "$k/bin/cbmc" ] || [ ! -e "$k/toolchain/bin/rustc" ]; then
|
||
cargo kani setup
|
||
fi
|
||
cargo kani --version
|
||
|
||
- name: Verify the shard's harnesses
|
||
working-directory: wai/wai-verify
|
||
shell: bash
|
||
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.
|
||
#
|
||
# The harnesses are in the library. The crate's one binary, the
|
||
# `wai-verify` tool, needs the `cli` feature, and a target whose
|
||
# required features are off stops `cargo kani` from building any;
|
||
# `--lib` selects the library alone.
|
||
args=()
|
||
for f in ${{ matrix.harness }}; do args+=(--harness "$f"); done
|
||
cargo kani --lib "${args[@]}"
|