diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index 79285a0c2..8b4c92936 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -22,6 +22,15 @@ name: wai formal verification (integer core) # 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. # @@ -55,10 +64,13 @@ on: - '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). + # 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: @@ -72,19 +84,66 @@ on: - '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: - kani: + # 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: + 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: + 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" } + - { 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 this runner image. + # 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 @@ -92,8 +151,11 @@ jobs: 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. + # 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: | @@ -102,20 +164,41 @@ jobs: ~/.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" - 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 + 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 integer core + - 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. - cargo kani + # + # 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[@]}" diff --git a/.github/workflows/wai-jpegai-e2e.yml b/.github/workflows/wai-jpegai-e2e.yml index 8422b35e7..1890a3c91 100644 --- a/.github/workflows/wai-jpegai-e2e.yml +++ b/.github/workflows/wai-jpegai-e2e.yml @@ -23,6 +23,11 @@ name: WAI JPEG-AI whole decode (pinned inputs, required) # of samples differ from it at all (the test's bar); # - two decodes in one process are byte-identical and the reconstruction binding # verifies the second and rejects a one-byte change; +# - the bundle's bounds certificate (wai/extensions/integer-operators.md §8.5, +# §13.6.1: the two scale graphs) is byte for byte the one committed under the +# set's digest in wai/ops-conformance/certificates/, which is the listing digest +# the set-form pin below covers, from both certifiers (wai-verify and the +# independent tools/wai_ops_check.py), and its verdict meets acc32; # - the decoded pixels hash to WAI_JPEGAI_EXPECT_SHA256 below: the value measured # from these inputs on an Apple Silicon Mac (aarch64 macOS, native) and # reproduced by an x86_64 Linux build (glibc, run under QEMU user-mode @@ -108,6 +113,16 @@ on: - 'wai/wai-rs/tests/support/**' - 'wai/tools/wai_jpegai_fetch_e2e_inputs.sh' - 'wai/tools/jpegai-e2e-v1.sha256' + # The bounds certificate of the bundle's scale path (the step after the fetch): + # the certifier, and the certificate committed by digest. + - 'wai/wai-ops/src/**' + - 'wai/wai-ops/tests/goldens.rs' + - 'wai/wai-verify/Cargo.toml' + - 'wai/wai-verify/Cargo.lock' + - 'wai/wai-verify/src/bin/**' + - 'wai/ops-conformance/certificates/external.json' + - 'wai/ops-conformance/certificates/wai.image.jpegai/3e243dc11566922f5cb7f4c628afd440b18d56a08b99b07cc33d5c8522aeec37.json' + - 'wai/tools/wai_ops_check.py' - '.github/workflows/wai-jpegai-e2e.yml' pull_request: paths: @@ -133,6 +148,16 @@ on: - 'wai/wai-rs/tests/support/**' - 'wai/tools/wai_jpegai_fetch_e2e_inputs.sh' - 'wai/tools/jpegai-e2e-v1.sha256' + # The bounds certificate of the bundle's scale path (the step after the fetch): + # the certifier, and the certificate committed by digest. + - 'wai/wai-ops/src/**' + - 'wai/wai-ops/tests/goldens.rs' + - 'wai/wai-verify/Cargo.toml' + - 'wai/wai-verify/Cargo.lock' + - 'wai/wai-verify/src/bin/**' + - 'wai/ops-conformance/certificates/external.json' + - 'wai/ops-conformance/certificates/wai.image.jpegai/3e243dc11566922f5cb7f4c628afd440b18d56a08b99b07cc33d5c8522aeec37.json' + - 'wai/tools/wai_ops_check.py' - '.github/workflows/wai-jpegai-e2e.yml' # Weekly, independent of changes: the inputs live outside the repository, and # their disappearing should surface here, not at the next unrelated PR. @@ -165,6 +190,53 @@ jobs: shell: bash working-directory: wai run: tools/wai_jpegai_fetch_e2e_inputs.sh "$WAI_JPEGAI_DIR" + # The scale path's bounds certificate (integer-operators §8.5, §13.6.1). The + # bundle is not committed, so its certificate is, under the set's digest (the + # listing of norm.json and weights/*, as the set-form pin covers it), and + # listed in wai/ops-conformance/certificates/external.json. + - name: The bundle's bounds certificate is the committed one, and meets acc32 + shell: bash + working-directory: wai + run: | + set -euo pipefail + (cd wai-verify && cargo build --locked --release --features cli --bin wai-verify) + D="$WAI_JPEGAI_DIR" + M=(--member "norm.json=$D/norm.json") + for n in hs_y hs_uv hyp_y hyp_uv synth_y synth_uv mcm0_y mcm1_y mcm2_y mcm3_y icci; do + M+=(--member "weights/$n.json=$D/$n.json") + done + wai-verify/target/release/wai-verify bounds --capability wai.image.jpegai "${M[@]}" --profile acc32 \ + --out "${RUNNER_TEMP:-/tmp}/jpegai-bounds.json" \ + --check ops-conformance/certificates/wai.image.jpegai/3e243dc11566922f5cb7f4c628afd440b18d56a08b99b07cc33d5c8522aeec37.json + # The same certificate from the independent certifier (Python standard library + # only, sharing no code with wai-ops). + - uses: actions/setup-python@v5 + with: + python-version: '3.11' + - name: The independent certifier writes the same certificate, and it meets acc32 + shell: bash + working-directory: wai + run: | + set -euo pipefail + D="$WAI_JPEGAI_DIR" + M=(--member "norm.json=$D/norm.json") + for n in hs_y hs_uv hyp_y hyp_uv synth_y synth_uv mcm0_y mcm1_y mcm2_y mcm3_y icci; do + M+=(--member "weights/$n.json=$D/$n.json") + done + python3 -I tools/wai_ops_check.py certify --capability wai.image.jpegai --lowering jpegai-int/1 "${M[@]}" \ + --profile acc32 --out "${RUNNER_TEMP:-/tmp}/jpegai-bounds-py.json" \ + --check ops-conformance/certificates/wai.image.jpegai/3e243dc11566922f5cb7f4c628afd440b18d56a08b99b07cc33d5c8522aeec37.json + # The operator set's lowering of the bundle's scale path (integer-operators + # §13.6.1), run through the interpreter with every value held to its certified + # interval, against the legacy decoder's arithmetic on the same bundle. + - name: The scale path's lowering decodes as the legacy arithmetic does + shell: bash + working-directory: wai/wai-ops + run: | + set -euo pipefail + WAI_OPS_JPEGAI_BUNDLE="$WAI_JPEGAI_DIR" \ + cargo test --locked --release --test goldens -- --ignored --exact jpegai_scale_path_on_a_supplied_bundle + - name: Whole decode vs the reference, determinism, pinned pixel hash (missing input = failure) shell: bash working-directory: wai/wai-rs diff --git a/.github/workflows/wai-ops.yml b/.github/workflows/wai-ops.yml index 712fae639..9dc7da721 100644 --- a/.github/workflows/wai-ops.yml +++ b/.github/workflows/wai-ops.yml @@ -5,17 +5,23 @@ name: wai-ops integer operators # wai/ops-conformance/ from its inputs and requires the committed bytes: # # - Linux x86_64, Linux arm64 and macOS arm64, natively, debug and release: the -# unit tests, the goldens (every committed parameter set lowered, loaded and +# unit tests (the bound rules against hand-computed values among them), the +# goldens (every committed parameter set lowered, loaded through load step 8 and # decoded through the interpreter to its committed output digest), the step-8 -# test and the doc tests, each in the default build and with the `uncertified` -# switch, and `wai-ops vectors verify`, which also re-lowers every set and -# regenerates the whole corpus; -# - WASI (wasm32-wasip2) under wasmtime, a 32-bit target: the same unit tests, -# goldens and step-8 test in both builds, and the same `vectors verify`; +# and verdict tests and the doc tests; `wai-verify vectors verify`, which also +# re-lowers every set, recomputes its bounds certificate from the committed +# lowered graphs and regenerates the whole corpus, so every certificate is +# byte-identical on every leg; and `wai-verify bounds` on the falsification sets +# of integer-operators §14.3, which must exit 1, and on committed sets, which +# must exit 0 under their profile; +# - WASI (wasm32-wasip2) under wasmtime, a 32-bit target: the same tests, and the +# same `vectors verify`; # - a browser's engine (wasm32-unknown-unknown) under Node: the recomputation of # every vector file; # - the independent checker, tools/wai_ops_check.py: Python standard library only, -# sharing no code with wai-ops, rewrites every vector file and every lowered graph. +# sharing no code with wai-ops, rewrites every vector file and every lowered graph, +# and, as a second certifier, every certificate, the falsification sets' included +# (each must fail the profile it claims). # # There is no Windows leg: the Windows runner has been offline since 2026-08-28. @@ -33,6 +39,8 @@ on: pull_request: paths: - 'wai/wai-ops/**' + # The certifier, the lowerings and the corpus tool, and the Kani host they share. + - 'wai/wai-verify/**' - 'wai/ops-conformance/**' - 'wai/tools/wai_ops_*.py' # The text the checker is held to. @@ -52,6 +60,8 @@ on: - main paths: - 'wai/wai-ops/**' + # The certifier, the lowerings and the corpus tool, and the Kani host they share. + - 'wai/wai-verify/**' - 'wai/ops-conformance/**' - 'wai/tools/wai_ops_*.py' - 'wai/extensions/integer-operators.md' @@ -91,28 +101,66 @@ jobs: rustup default 1.98.0 echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" - # Without the `uncertified` switch, load step 8 refuses every graph: the default - # build is what a decoder would link before the certifier exists. Its tests show - # that, and the doc tests that a graph runs only once loaded. - - name: Unit, step-8 and doc tests, default build + - name: Unit, goldens, step-8, verdict and doc tests, debug working-directory: wai/wai-ops shell: bash run: cargo test --locked - - name: Unit tests and goldens, debug + - name: Unit, goldens, step-8 and verdict tests, release working-directory: wai/wai-ops shell: bash - run: cargo test --locked --features uncertified + run: cargo test --locked --release - - name: Unit tests and goldens, release - working-directory: wai/wai-ops + - name: Build wai-verify, and its own tests (the witness through the interpreter; --check's path) + working-directory: wai/wai-verify shell: bash - run: cargo test --locked --release --features uncertified + run: | + set -euo pipefail + cargo build --locked --release --features cli --bin wai-verify + cargo test --locked --release --features cli --bin wai-verify - - name: Every vector file recomputed, every set re-lowered, the corpus regenerated - working-directory: wai/wai-ops + - name: Every vector file recomputed, every set re-lowered and certified, the corpus regenerated + working-directory: wai shell: bash - run: cargo run --locked --release --features uncertified --bin wai-ops -- vectors verify .. + run: wai-verify/target/release/wai-verify vectors verify . + + # The exit status of `wai-verify bounds` (0: the verdict meets the profile, 1: it + # fails it, 3: a difference from the committed certificate), on the sets whose + # verdict integer-operators §14.3 and the design's predictions fix. + - name: The falsification sets fail their profile; committed sets meet theirs + working-directory: wai + shell: bash + run: | + set -euo pipefail + V=wai-verify/target/release/wai-verify + C=ops-conformance/certificates/wai.neural.int_synth + T="${RUNNER_TEMP:-/tmp}" + bounds() { + local want=$1; shift + set +e; "$V" bounds "$@" --out "$T/cert.json"; local got=$?; set -e + [ "$got" = "$want" ] || { echo "::error::wai-verify bounds $* exited $got, not $want"; exit 1; } + } + # One unit past i64 under acc64, and a claim of acc32 one weight past it. + bounds 1 ops-conformance/sets/overflow_acc64/int_synth.json --capability wai.neural.int_synth --profile acc64 \ + --check $C/b35460f39f31a559e97e66b8dde4597a309cbc44199c40097f935dd8e6e7305a.json + bounds 1 ops-conformance/sets/claim_acc32/int_synth.json --capability wai.neural.int_synth --profile acc32 \ + --check $C/76916c8f85da7663c09fba8cb091d628ed38328b680563285b8056cec82fd1ac.json + # facade meets acc32; photo meets acc64 and fails acc32 (at node 6, convT.acc). + bounds 0 neural-conformance/vectors/facade/int_synth.json --capability wai.neural.int_synth --profile acc32 \ + --check $C/c6a362696d61605931ef4da98ae630362dcd73ea6be7864db6e61d6c5abbcd24.json + bounds 0 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth --profile acc64 \ + --check $C/50868e72f5f1599569c413ed1f67ab8610fa0b3c17919162cbf370f49275125c.json + # With --witness, a node-local graph for each failing node: photo's node 6, whose + # input attains convT.acc's upper end. With --advise, the clamps that would let + # the overflow set meet acc64. + bounds 1 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth --profile acc32 \ + --witness "$T/witness" + test -s "$T/witness/synth-6.json" + grep -q '"acc":"26172239136"' "$T/witness/synth-6.json" + bounds 1 ops-conformance/sets/overflow_acc64/int_synth.json --capability wai.neural.int_synth --advise acc64 + # A certificate that is not the committed one is exit 3. + bounds 3 neural-conformance/vectors/photo/int_synth.json --capability wai.neural.int_synth \ + --check $C/c6a362696d61605931ef4da98ae630362dcd73ea6be7864db6e61d6c5abbcd24.json wasip2: name: wasm32-wasip2 (wasmtime) @@ -144,7 +192,7 @@ jobs: # The tests read committed files through CARGO_MANIFEST_DIR/.., so the wai # directory is preopened at its own absolute path. - - name: Unit and step-8 tests, default build, under WASI + - name: Unit, goldens, step-8 and verdict tests, under WASI working-directory: wai/wai-ops shell: bash run: | @@ -153,27 +201,18 @@ jobs: CARGO_TARGET_WASM32_WASIP2_RUNNER="wasmtime run --dir $W::$W" \ cargo test --locked --release --target wasm32-wasip2 - - name: Unit tests, goldens and step-8 test, under WASI - working-directory: wai/wai-ops + - name: Build wai-verify for wasm32-wasip2 + working-directory: wai/wai-verify shell: bash - run: | - set -euo pipefail - W=$(cd .. && pwd) - CARGO_TARGET_WASM32_WASIP2_RUNNER="wasmtime run --dir $W::$W" \ - cargo test --locked --release --features uncertified --target wasm32-wasip2 + run: cargo build --locked --release --features cli --target wasm32-wasip2 --bin wai-verify - - name: Build the tool for wasm32-wasip2 - working-directory: wai/wai-ops - shell: bash - run: cargo build --locked --release --features uncertified --target wasm32-wasip2 --bin wai-ops - - - name: Every vector file recomputed, every set re-lowered, the corpus regenerated, under WASI + - name: Every vector file recomputed, every set re-lowered and certified, the corpus regenerated, under WASI working-directory: wai shell: bash run: | set -euo pipefail wasmtime --version - wasmtime run --dir .::/wai wai-ops/target/wasm32-wasip2/release/wai-ops.wasm vectors verify /wai + wasmtime run --dir .::/wai wai-verify/target/wasm32-wasip2/release/wai-verify.wasm vectors verify /wai node: name: wasm32 under Node @@ -219,7 +258,7 @@ jobs: python-version: '3.11' # Standard library only, so it needs nothing installed. - - name: wai_ops_check.py rewrites every vector file and every lowered graph + - name: wai_ops_check.py rewrites every vector file, every lowered graph and every certificate working-directory: wai shell: bash run: python3 -I tools/wai_ops_check.py ops-conformance diff --git a/.github/workflows/wai-sota-vectors.yml b/.github/workflows/wai-sota-vectors.yml index cd6b59da4..eaa3b589a 100644 --- a/.github/workflows/wai-sota-vectors.yml +++ b/.github/workflows/wai-sota-vectors.yml @@ -22,6 +22,12 @@ name: WAI mbt2018_mean integer decode (regenerated vectors) # - the Rust integer decode reproduces the export tool's integer reference # byte-for-byte (synthesis, hyper-decoder, the whole conditional bitstream, the # compact binary model, the eight-frame clip); +# - the regenerated set's bounds certificate (wai/extensions/integer-operators.md +# §8.5) is byte for byte the one committed under its set digest in +# wai/ops-conformance/certificates/, from both certifiers (wai-verify and the +# independent tools/wai_ops_check.py), and its verdict meets acc64. The set is +# not committed, so this job is where its certificate is checked; the set's +# three files have had the same digests on every run and machine recorded; # - on the pinned photograph, the integer decode costs at most 1 dB against the # same model's float decode (the bar CI enforces), measured by the Rust decoder # on its own output. Measured on an Apple Silicon Mac: 35.985 dB for the integer @@ -129,6 +135,15 @@ on: - 'wai/tools/requirements-sota-int.txt' # The wasm32 decode of the same vectors (the last steps below). - 'wai/wai-web/**' + # The bounds certificate of the regenerated set (the step after the + # regeneration): the certifier, and the certificate committed by digest. + - 'wai/wai-ops/src/**' + - 'wai/wai-verify/Cargo.toml' + - 'wai/wai-verify/Cargo.lock' + - 'wai/wai-verify/src/bin/**' + - 'wai/ops-conformance/certificates/external.json' + - 'wai/ops-conformance/certificates/wai.neural.int_hyper/f16fd09cd79b831d7d821e030c05e99e9fb5ea216574e699944ea4e55ac0a404.json' + - 'wai/tools/wai_ops_check.py' - '.github/workflows/wai-sota-vectors.yml' pull_request: paths: @@ -151,6 +166,15 @@ on: - 'wai/tools/requirements-sota-int.txt' # The wasm32 decode of the same vectors (the last steps below). - 'wai/wai-web/**' + # The bounds certificate of the regenerated set (the step after the + # regeneration): the certifier, and the certificate committed by digest. + - 'wai/wai-ops/src/**' + - 'wai/wai-verify/Cargo.toml' + - 'wai/wai-verify/Cargo.lock' + - 'wai/wai-verify/src/bin/**' + - 'wai/ops-conformance/certificates/external.json' + - 'wai/ops-conformance/certificates/wai.neural.int_hyper/f16fd09cd79b831d7d821e030c05e99e9fb5ea216574e699944ea4e55ac0a404.json' + - 'wai/tools/wai_ops_check.py' - '.github/workflows/wai-sota-vectors.yml' # Weekly, independent of changes: the job depends on artifacts fetched from # outside the repository (the checkpoint, the pinned wheels), and their @@ -228,6 +252,35 @@ jobs: # files differ between machines (see the header). It is not a list any # other run must reproduce, here or elsewhere. (cd "$WAI_SOTA_INT_DIR" && sha256sum *) + # The set's bounds certificate (integer-operators §8.5). The set is not + # committed, so its certificate is, under the set's digest, and listed in + # wai/ops-conformance/certificates/external.json. A regenerated set with other + # bytes has another digest, and --check fails on set_sha256 first. + - name: The regenerated set's bounds certificate is the committed one, and meets acc64 + shell: bash + working-directory: wai + run: | + set -euo pipefail + (cd wai-verify && cargo build --locked --release --features cli --bin wai-verify) + D="$WAI_SOTA_INT_DIR" + wai-verify/target/release/wai-verify bounds --capability wai.neural.int_hyper \ + --member h_s.whm="$D/int_hs_model.bin" --member g_s.whm="$D/int_synth_sota_model.bin" \ + --member entropy.json="$D/cond_entropy.json" --profile acc64 \ + --out "${RUNNER_TEMP:-/tmp}/int-hyper-bounds.json" \ + --check ops-conformance/certificates/wai.neural.int_hyper/f16fd09cd79b831d7d821e030c05e99e9fb5ea216574e699944ea4e55ac0a404.json + # The same certificate from the independent certifier (Python standard library + # only, sharing no code with wai-ops), which needs only the Python set up above. + - name: The independent certifier writes the same certificate, and it meets acc64 + shell: bash + working-directory: wai + run: | + set -euo pipefail + D="$WAI_SOTA_INT_DIR" + python3 -I tools/wai_ops_check.py certify --capability wai.neural.int_hyper --lowering whm1/1 \ + --member h_s.whm="$D/int_hs_model.bin" --member g_s.whm="$D/int_synth_sota_model.bin" \ + --member entropy.json="$D/cond_entropy.json" --profile acc64 \ + --out "${RUNNER_TEMP:-/tmp}/int-hyper-bounds-py.json" \ + --check ops-conformance/certificates/wai.neural.int_hyper/f16fd09cd79b831d7d821e030c05e99e9fb5ea216574e699944ea4e55ac0a404.json - name: Rust decodes every int_hyper vector byte-for-byte (missing input = failure), and the missing-input rule holds shell: bash working-directory: wai/wai-rs diff --git a/wai/ops-conformance/README.md b/wai/ops-conformance/README.md index 44fe269a3..4f68e4f95 100644 --- a/wai/ops-conformance/README.md +++ b/wai/ops-conformance/README.md @@ -5,7 +5,7 @@ Vectors for `wai-ops/1`, the integer operator set operators (§5), its stage operators (§5E), the `WHG1` graph form (§10), and the canonical lowerings of the registered integer network forms (§13). -**Provenance.** Generated here by `wai-ops vectors gen` from fixed SplitMix64 +**Provenance.** Generated here by `wai-verify vectors gen` from fixed SplitMix64 sequences: every graph, parameter, input and stream under `vectors/`, `stage/`, `graphs/` and `sets/` is generated integers, with no media. The lowered graphs under `certificates/` are those of the sets this corpus generates and of the parameter sets @@ -33,10 +33,26 @@ lowering conforms when it writes every lowered graph byte for byte. - `lower_