open-standards/wai/wai-ops
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Transaction Science 9006e7aea4 wai-ops proofs: harnesses that did not close are gated; CI in seven shards by measured time
Harnesses whose windows the checker did not finish within their cap (ten or
twenty minutes on an idle 32-core host) are gated by cfg(kani_open): kept in
the source with their statements, compiled and run only on request
(RUSTFLAGS="--cfg kani_open" cargo kani --lib --exact --harness <name>), so
that every harness CI compiles verifies. check_shards.py counts them apart.
wai-verify declares the cfg.

The shards, from the measured times: the wai-rs harnesses; arith and limb;
the two 512-bit isqrt harnesses; the stage harnesses; the two longest stage
harnesses (K26, and K29 over every range, renamed so a filter names it alone);
sound; plan.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-10-11 17:16:54 -04:00
..
node wai-verify: the bounds certifier, the lowerings and the corpus tool 2026-10-10 09:38:32 -04:00
src wai-ops proofs: harnesses that did not close are gated; CI in seven shards by measured time 2026-10-11 17:16:54 -04:00
tests wai-ops: a run can be observed, and every golden decode is held to its certificate 2026-10-10 23:16:55 -04:00
Cargo.lock wai-ops: the reference crate for wai-ops/1 (WHG1, plans, interpreter, stage operators, lowerings) 2026-10-09 19:31:38 -04:00
Cargo.toml wai-verify: the bounds certifier, the lowerings and the corpus tool 2026-10-10 09:38:32 -04:00