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: gate
    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, and two of them no longer fit the
      # general runners.
      #
      # 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` runners have 15 GiB shared by two jobs, and CBMC ran out of
      # memory there, so it was moved to `macos` -- which is a host carrying two CI
      # labels, an inference server and a simulation sweep, and was measured at load
      # 185 on 32 cores.
      #
      # `isqrt512` then began failing on `linux` the same way, but as a timeout rather
      # than an allocation error: 1 h 59 m 46 s against this job's 120-minute budget. A
      # model checker that runs out of time has refuted nothing and proved nothing, so
      # it is the one failure mode a proof gate must not reach by accident.
      #
      # Both now run on `macos-proofs`: a 28-core, 96 GB Mac Studio at load ~6, with a
      # runner of capacity 1 so a harness never shares the box with another. The label
      # is deliberately narrow -- that host has the Command Line Tools but no full
      # Xcode, Metal, node, browsers or Java, so it must not answer the general `macos`
      # label, where a missing tool reads as a code failure. It has rustup, and these
      # shards install their own prover.
      #
      # Every other shard has run to completion on the linux runners.
      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: macos-proofs, 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-proofs, 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.99.1
          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 either macOS
      # label: those runners execute on the host, so `~` is the host's own home,
      # where Kani is installed, and a restore would write over a live install.
      # The test is a prefix, not `!= 'macos'`, because `macos-proofs` is a second
      # such host -- and `runner.os` is `macOS` for both, so one key would also
      # have them overwriting each other's.
      - name: Cache Kani toolchain
        if: ${{ !startsWith(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[@]}"