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.

# 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'
      # 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