### Integer operators: the reference crate, the bounds pass and its certificates

The crate, the tool and the corpus that
[integer-operators](extensions/integer-operators.md) (Draft) names exist. No capability
decodes through them yet: each capability's reference decoder is still the one its
payload extension names.

- **`wai-ops`**, the reference crate, `no_std` with `alloc` and no dependencies: the
  512-bit saturating integer of §8.1, the canonical JSON writer of §8.5, the `WHG1`
  parser and writer, the load-time and run-time plans, every graph operator of §5, the
  stage operators E1–E13, and the lowerings of §13.
- **Load step 8.** `wai_ops::bounds` runs the bounds pass of §8.1–§8.5 and writes the
  canonical certificate. The interpreter runs only a loaded graph, so nothing decodes a
  parameter set its certificate does not admit. `interp::run_observed` reports every
  value a run forms; `bounds::Within` holds a run to its certificate, and every golden
  decode runs that way.
- **`wai-verify`**: `bounds`, `lower` and `vectors`, with `--check`, `--witness` and
  `--advise`.
- **`wai/ops-conformance/`**: per-operator, stage, graph, load and lowering vectors, the
  lowered graph of every committed parameter set, and each set's certificate.
- **Two certifiers.** `tools/wai_ops_check.py`, written from the extension text and
  sharing no code with the crate, recomputes every vector and every certificate byte
  for byte.
- **`wai_ops::limb32`**, a reference model of the 32-bit arithmetic the `acc32` profile's
  two products need, checked against 64-bit arithmetic.
- **Model checking.** The operator set's harnesses are in `wai-ops/src/proofs/`, hosted
  by `wai-verify` and run by `wai-formal-verification.yml`. A harness that does not yet
  verify within the job's budget is kept, behind `cfg(kani_open)`, and is not run or
  counted as proved.
- **`wai-ops.yml`** runs the crate's tests and `vectors verify` natively, under
  wasm32-wasip2 and under wasm32 in Node, and runs the checker.

