446865697c
A stage-only decode has no fast kernel behind an interpreter. What a faster
fabric runs instead is E9's 32-bit form (§5E E9, Width): the form D3b's
integer GPU legs take. Gate 5 holds it to the exact form.
- wai-ops: residual_step_i32 and i32_form_fits behind the new i32_forms
feature (and cfg(test), cfg(kani), so the unit tests and K29 keep them);
residual_step_by_i32, E9 through its 32-bit form for a driver whose
operands are i64. wai-verify declares the feature name its included
sources test.
- wai-rs i32_forms: int_video::ops::{decode_typed_i32,
decode_pframes_typed_i32} and staged::wir1::ops::apply_unit_i32, the
drivers with E9 as a parameter.
- Parity: every committed clip and layer through the 32-bit form as through
the exact form (tests/int_video_ops.rs, tests/wir1_ops.rs), changed
streams too; the differential compares the 32-bit form on every random
case; byte-exact-conformance (i32_forms on by default) decodes WIV1 and the
staged sets through it to the pinned digests on every leg.
- CI: the fast-kernel steps carry i32_forms, appended so gate.sh's grep
still finds them.
Gate 4's falsification, for the record: ops::frame's block grid taken as
w / block, which only a grid with a partial last column reaches (every
committed clip's sides are multiples of its block). Gates 1 to 3 stayed
green (int_video_ops 5, wir1_ops 5); int_video_random_clips_decode_alike
failed at seed 3372 (h 5, w 3, block 4). Timed 300 s, seed 20261017: debug
2,402,935 clips and 408,439 layers, release 11,948,953 and 3,322,036,
alike.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
44 lines
1.8 KiB
TOML
44 lines
1.8 KiB
TOML
# The reference implementation of `wai-ops/1`, the integer operator set
|
|
# (`extensions/integer-operators.md`): the `WHG1` graph form, the load and run-time
|
|
# plans, the interpreter, the stage operators, the canonical lowerings of the
|
|
# registered integer network forms, the bounds pass with its certificate (load step
|
|
# 8), and the conformance vectors of `../ops-conformance/`.
|
|
#
|
|
# `no_std` with `alloc`, and no dependencies, so that a model checker can include
|
|
# its sources by `#[path]` the way `wai-verify` includes the other integer sources.
|
|
[package]
|
|
name = "wai-ops"
|
|
version = "0.1.0"
|
|
edition = "2024"
|
|
rust-version = "1.97"
|
|
license = "Apache-2.0"
|
|
publish = false
|
|
description = "WAI integer operator set wai-ops/1: WHG1 graphs, plans, interpreter, stage operators, lowerings, bounds certificates and conformance vectors"
|
|
|
|
[lib]
|
|
name = "wai_ops"
|
|
path = "src/lib.rs"
|
|
|
|
# The tool that drives this library (the certifier, the lowerings and the corpus) is
|
|
# `wai-verify`, a binary of `../wai-verify` behind its `cli` feature.
|
|
|
|
[lints.rust]
|
|
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
|
|
|
|
[dependencies]
|
|
# none
|
|
|
|
[features]
|
|
# `i32_forms`: the 32-bit forms of the stage operators that have one by identity, E9's
|
|
# (`stage::residual_step_i32`, `stage::i32_form_fits`, §5E E9 *Width*), the arithmetic a
|
|
# 32-bit fabric runs. For the integer GPU legs and the parity tests that hold those
|
|
# forms to the exact ones; this crate's tests and the model checker compile them
|
|
# without it. Never on a decode's default path.
|
|
i32_forms = []
|
|
# `bounds_oracle`: the bounds pass as it stood before its closed forms, for another
|
|
# crate's tests to hold `bounds::pass` to (wai-rs's random-set differential). This
|
|
# crate's own tests see it without the feature. Never on a decode's path.
|
|
oracle = []
|
|
|
|
[profile.release]
|
|
debug = false
|