wai-ops: the reference crate and conformance vectors for wai-ops/1 (D2a) #206

Merged

dcharlot merged 15 commits from wai/d2a-operators-crate into main 2026-10-10 17:17:02 -04:00

Conversation 0 Commits 15 Files changed 131 +14806

dcharlot commented 2026-10-09 19:35:01 -04:00

Owner

Copy link

Adds wai/wai-ops, the reference crate for wai-ops/1, together with its conformance corpus wai/ops-conformance/, an independent checker wai/tools/wai_ops_check.py, and the wai-ops.yml workflow. This is phase D2a of the integer operator set.

Stacked on #202. The branch starts at #202's head, so until #202 merges this diff also shows the integer-operators.md text. Merge #202 first.

What lands

• wai/wai-ops is no_std with alloc and has no dependencies. It contains:

  • xint, a 512-bit integer that saturates as §8.1 requires;
  • json, with the canonical writer of §8.5;
  • graph, which parses and writes WHG1 (load steps 1–6), plus Loaded;
  • plan, the load-time and run-time plans;
  • interp, every graph operator of §5;
  • stage, E1–E13;
  • lower, the six lowerings of §13.

• Load step 8 (the bounds pass and verdict) is not built yet; it comes with the certifier. In the default build, step 8 refuses every graph. The interpreter runs only a Loaded graph, and only graph::load makes one, so the default build decodes nothing. The uncertified switch skips step 8 and is enabled only by the tests, the conformance tool and its browser-engine build.

• wai/ops-conformance/, written by wai-ops vectors gen, contains:

  • per-operator vectors and stage vectors;
  • graph vectors: the phase form, state, the load and run refusals, and the lowering vectors;
  • the lowered graphs of every committed set and of the small sets, with certificates/index.json.

  The README now points to §14.1 for every field. It also lists what waits for step 8.

• wai/tools/wai_ops_check.py uses the Python standard library only and shares no code with wai-ops. It:

  • recomputes every vector file, including load (steps 1–8) and profiles, from its own bounds pass and verdict;
  • re-lowers every set;
  • checks that each lowering vector's graph is the role its id names.

• wai-ops.yml runs these legs:

  • linux, linux-arm64 and macos, natively: tests in both builds, and vectors verify;
  • wasm32-wasip2 under wasmtime: tests in both builds, and vectors verify;
  • wasm32-unknown-unknown under Node;
  • the checker;
  • the concurrency gate.

Review findings and what changed

Fourteen findings. Thirteen are fixed in full. The fourteenth (the checker, #6) is fixed except for its step-8 vectors, which wait for step 8 (see "Not in this PR"). Text fixes are on #202, and code fixes are here.

1. The at of an E8 refusal named the wrong position. Only the in step set the position, so a refusal in a position's out step (in sgm, the flush after an escape) named the last in of its group. The out step now sets the position too, in the crate and in the checker. mans_decode/sgm/40 goes from at=11 to at=10. §14.1 now defines at for a flush that belongs to no single position. The review's E8 fuzz, rerun on this binary, shows 0 at mismatches in 12,000 cases. With the fix reverted, one seed alone shows 45.

2. E9's 32-bit form overflowed near the i32 limits. The text now states the condition under which it fits. In the code, residual_step_i32 checks that condition in debug builds, and two tests cover the limits. There are also 32 new residual_step vectors at the i32 limits.

3. E12's widths were wrong. The text now says every value fits i50; the earlier claim was 47 bits. Three new rate_predict vectors sit at the i16 extremes with rates near 2^32.

4. Exactness-boundary vectors were missing. Those that depend on load step 8 cannot be written until step 8 exists. The README now lists them as deferred, so the corpus no longer appears to cover them (see "Not in this PR").

5. §13.2 and ReLU inputs. The crate and the checker now follow the text: a tensor that a ReLU reads, other than the network's input, is derived. The checker's x_record was rewritten from the §13.2 wording. This regenerated:

   • the h_s graphs of the int_hyper set 7aceaa1a… and of the int_mlicpp sets 07e1835d… and 7ef44f3b…;
   • the lower_whm1 and lower_wmb1 vectors.

   No output changes. With the old rule restored, the checker fails all three graphs.

6. The checker did not check profiles, step 8 or the lowering vectors. It now has a bounds pass and verdict written from §8.1–§8.5, with saturation at every primitive. It runs step 8 and recomputes profiles, which agree with all 1,599 tags and with Appendix C for every committed set. Each lowering vector's graph must now equal its re-lowered role. §14.1 (#202) now states the rule that a refused load lists both profiles.

7. at was defined only in the README. It is now normative in §14.1, and the corpus follows it (see 1).

8. Some refusal codes were unstated. §5E now states that a broken condition is refused with model_mismatch before any symbol, and lists the exceptions. E8 is reworded. No vector changes, because the corpus already gave these codes.

9. Input value checks had no stated place. §4 step 4 now applies each input's policy first. The existing run/order/10 pins this: with the check moved into step 1, that vector fails.

10. Some vector fields were defined only in the README. The operand, mode and layout table is now normative in §14.1, including the predictors' fields and their CHW layouts.

11. Gaps that only the crate settled. Each is now in the text and has a vector that a different reading fails:

    • a refused decode changes no state;
    • the uncropped output of cout·uh·uw elements is capped;
    • the order is caps, then the shape rule, then max_elems;
    • crop starts are at least 0, and a scalar start is planned at 0 at load;
    • step 1 runs input by input;
    • m_bytes and g_bytes are 4 or 8.

    Eleven checker mutations, one for each reading, each fail on exactly one new line. subpos_merge now caps its sides before its shape rule, as §4 says. No input within the caps can tell the two orders apart.

12. Step 8 could be bypassed. run now takes &Loaded.

    • A compile_fail (E0308) doc test shows that an unloaded lowered graph does not compile as an argument to run. The review's bypass now fails to compile, and graph::load of the same bytes returns Load(8).
    • The goldens load every graph.
    • tests/step8.rs runs in every build.

13. The paths: filter missed the goldens' digest file. Both filter lists now take wai/neural-conformance/**. The repo's matcher now says True for sha256.json.

14. The tests never ran on a 32-bit target. The wasip2 leg now runs cargo test under wasmtime in both builds. The native default build runs cargo test, so the step-8 and doc tests run.

Not in this PR

• The vectors that need load step 8:

  • sigmoid and elu at −2^63;
  • an rq whose q passes 64 bits while y fits;
  • a lut16 or a check range refused by the bounds pass;
  • a step-8 refusal in graphs/load.jsonl.

  The plan places them in D2b with the certifier. The checker already runs step 8, so they are checked as soon as they land.

• A checker written by a session that has read only the text. The original checker was written after the crate, in the same session. The review found two places where it copied the crate: E8's positions and the ReLU rule. Both are now rewritten from the text. The bounds pass was written from §8, starting from a pass the review wrote from §8 alone. The session that made these fixes had read the crate, so the text-only checker the plan calls for is still owed before D2a closes.

Exit tests

All of these ran at this head:

• macOS arm64, natively. All passed:
  • cargo test --locked (default build): 13 unit tests, the step-8 test, and 2 doc tests;
  • cargo test --locked --features uncertified, in debug and release: 13 unit tests, 6 goldens (3 ignored), the step-8 test, and 2 doc tests;
  • wai-ops vectors verify ..: 53 vector files, 2,794 vectors, 17 sets re-lowered, 93 files regenerated, every byte equal.
• wasm32-wasip2 under wasmtime. Both cargo test builds pass, and vectors verify passes.
• wasm32-unknown-unknown under Node. Every vector file recomputes.
• The checker, under Python 3.11 and 3.14. It rewrites every vector file and lowered graph byte for byte, and matches all 11 lowered roles.
• Linux x86_64 and arm64 run in CI.

Falsification

Each fix was committed before it was falsified.

• E8 position (1). With the fix reverted, vectors verify fails on mans_decode.jsonl line 41, and the checker fails without its out position.
• E9 condition (2). With the condition weakened to the old claim, residual_form_condition_is_tight fails.
• ReLU rule (5). With the old rule, the checker fails on 3 lowered graphs.
• Checker (6). Each of these fails the checker:
  • a changed profiles tag;
  • a lowering vector whose graph was swapped;
  • removing the acc32 parameter conditions;
  • the all-taps transposed-convolution rule;
  • not counting check policies against acc32;
  • flooring igdn once;
  • classing rq.p as acc.
• The eleven readings (11). Each fails one new line.
• run taking a Graph (12). The compile_fail doc test fails ("compiled successfully").

Checks run

• check-public-names.sh and check-comparative-prose.sh were run one file at a time on every changed text-bearing file and on this body. All were clean.
• check-no-vanity-metrics.sh, check-wai-section-refs.py and check-workflow-concurrency.sh were clean.
• Open PRs were checked first. None touches wai-ops, ops-conformance, wai_ops_check.py or wai-ops.yml.

🤖 Generated with Claude Code

Adds `wai/wai-ops`, the reference crate for `wai-ops/1`, together with its conformance corpus `wai/ops-conformance/`, an independent checker `wai/tools/wai_ops_check.py`, and the `wai-ops.yml` workflow. This is phase D2a of the integer operator set. **Stacked on #202.** The branch starts at #202's head, so until #202 merges this diff also shows the `integer-operators.md` text. Merge #202 first. ## What lands - **`wai/wai-ops`** is `no_std` with `alloc` and has no dependencies. It contains: - `xint`, a 512-bit integer that saturates as §8.1 requires; - `json`, with the canonical writer of §8.5; - `graph`, which parses and writes `WHG1` (load steps 1–6), plus `Loaded`; - `plan`, the load-time and run-time plans; - `interp`, every graph operator of §5; - `stage`, E1–E13; - `lower`, the six lowerings of §13. - **Load step 8 (the bounds pass and verdict)** is not built yet; it comes with the certifier. In the default build, step 8 refuses every graph. The interpreter runs only a `Loaded` graph, and only `graph::load` makes one, so the default build decodes nothing. The `uncertified` switch skips step 8 and is enabled only by the tests, the conformance tool and its browser-engine build. - **`wai/ops-conformance/`**, written by `wai-ops vectors gen`, contains: - per-operator vectors and stage vectors; - graph vectors: the phase form, state, the load and run refusals, and the lowering vectors; - the lowered graphs of every committed set and of the small sets, with `certificates/index.json`. The README now points to §14.1 for every field. It also lists what waits for step 8. - **`wai/tools/wai_ops_check.py`** uses the Python standard library only and shares no code with `wai-ops`. It: - recomputes every vector file, including `load` (steps 1–8) and `profiles`, from its own bounds pass and verdict; - re-lowers every set; - checks that each lowering vector's graph is the role its id names. - **`wai-ops.yml`** runs these legs: - linux, linux-arm64 and macos, natively: tests in both builds, and `vectors verify`; - wasm32-wasip2 under wasmtime: tests in both builds, and `vectors verify`; - wasm32-unknown-unknown under Node; - the checker; - the concurrency gate. ## Review findings and what changed Fourteen findings. Thirteen are fixed in full. The fourteenth (the checker, #6) is fixed except for its step-8 vectors, which wait for step 8 (see "Not in this PR"). Text fixes are on #202, and code fixes are here. 1. **The `at` of an E8 refusal named the wrong position.** Only the `in` step set the position, so a refusal in a position's `out` step (in `sgm`, the flush after an escape) named the last `in` of its group. The `out` step now sets the position too, in the crate and in the checker. `mans_decode/sgm/40` goes from `at=11` to `at=10`. §14.1 now defines `at` for a flush that belongs to no single position. The review's E8 fuzz, rerun on this binary, shows 0 `at` mismatches in 12,000 cases. With the fix reverted, one seed alone shows 45. 2. **E9's 32-bit form overflowed near the i32 limits.** The text now states the condition under which it fits. In the code, `residual_step_i32` checks that condition in debug builds, and two tests cover the limits. There are also 32 new `residual_step` vectors at the i32 limits. 3. **E12's widths were wrong.** The text now says every value fits i50; the earlier claim was 47 bits. Three new `rate_predict` vectors sit at the i16 extremes with rates near 2^32. 4. **Exactness-boundary vectors were missing.** Those that depend on load step 8 cannot be written until step 8 exists. The README now lists them as deferred, so the corpus no longer appears to cover them (see "Not in this PR"). 5. **§13.2 and ReLU inputs.** The crate and the checker now follow the text: a tensor that a ReLU reads, other than the network's input, is `derived`. The checker's `x_record` was rewritten from the §13.2 wording. This regenerated: - the `h_s` graphs of the int_hyper set `7aceaa1a…` and of the int_mlicpp sets `07e1835d…` and `7ef44f3b…`; - the `lower_whm1` and `lower_wmb1` vectors. No output changes. With the old rule restored, the checker fails all three graphs. 6. **The checker did not check `profiles`, step 8 or the lowering vectors.** It now has a bounds pass and verdict written from §8.1–§8.5, with saturation at every primitive. It runs step 8 and recomputes `profiles`, which agree with all 1,599 tags and with Appendix C for every committed set. Each lowering vector's graph must now equal its re-lowered role. §14.1 (#202) now states the rule that a refused load lists both profiles. 7. **`at` was defined only in the README.** It is now normative in §14.1, and the corpus follows it (see 1). 8. **Some refusal codes were unstated.** §5E now states that a broken condition is refused with `model_mismatch` before any symbol, and lists the exceptions. E8 is reworded. No vector changes, because the corpus already gave these codes. 9. **Input value checks had no stated place.** §4 step 4 now applies each input's policy first. The existing `run/order/10` pins this: with the check moved into step 1, that vector fails. 10. **Some vector fields were defined only in the README.** The operand, mode and layout table is now normative in §14.1, including the predictors' fields and their CHW layouts. 11. **Gaps that only the crate settled.** Each is now in the text and has a vector that a different reading fails: - a refused decode changes no state; - the uncropped output of `cout·uh·uw` elements is capped; - the order is caps, then the shape rule, then `max_elems`; - crop starts are at least 0, and a scalar start is planned at 0 at load; - step 1 runs input by input; - `m_bytes` and `g_bytes` are 4 or 8. Eleven checker mutations, one for each reading, each fail on exactly one new line. `subpos_merge` now caps its sides before its shape rule, as §4 says. No input within the caps can tell the two orders apart. 12. **Step 8 could be bypassed.** `run` now takes `&Loaded`. - A `compile_fail` (E0308) doc test shows that an unloaded lowered graph does not compile as an argument to `run`. The review's bypass now fails to compile, and `graph::load` of the same bytes returns `Load(8)`. - The goldens load every graph. - `tests/step8.rs` runs in every build. 13. **The `paths:` filter missed the goldens' digest file.** Both filter lists now take `wai/neural-conformance/**`. The repo's matcher now says True for `sha256.json`. 14. **The tests never ran on a 32-bit target.** The wasip2 leg now runs `cargo test` under wasmtime in both builds. The native default build runs `cargo test`, so the step-8 and doc tests run. ## Not in this PR - **The vectors that need load step 8:** - `sigmoid` and `elu` at −2^63; - an `rq` whose `q` passes 64 bits while `y` fits; - a `lut16` or a `check` range refused by the bounds pass; - a step-8 refusal in `graphs/load.jsonl`. The plan places them in D2b with the certifier. The checker already runs step 8, so they are checked as soon as they land. - **A checker written by a session that has read only the text.** The original checker was written after the crate, in the same session. The review found two places where it copied the crate: E8's positions and the ReLU rule. Both are now rewritten from the text. The bounds pass was written from §8, starting from a pass the review wrote from §8 alone. The session that made these fixes had read the crate, so the text-only checker the plan calls for is still owed before D2a closes. ## Exit tests All of these ran at this head: - **macOS arm64, natively.** All passed: - `cargo test --locked` (default build): 13 unit tests, the step-8 test, and 2 doc tests; - `cargo test --locked --features uncertified`, in debug and release: 13 unit tests, 6 goldens (3 ignored), the step-8 test, and 2 doc tests; - `wai-ops vectors verify ..`: 53 vector files, 2,794 vectors, 17 sets re-lowered, 93 files regenerated, every byte equal. - **wasm32-wasip2 under wasmtime.** Both `cargo test` builds pass, and `vectors verify` passes. - **wasm32-unknown-unknown under Node.** Every vector file recomputes. - **The checker, under Python 3.11 and 3.14.** It rewrites every vector file and lowered graph byte for byte, and matches all 11 lowered roles. - **Linux x86_64 and arm64** run in CI. ## Falsification Each fix was committed before it was falsified. - **E8 position (1).** With the fix reverted, `vectors verify` fails on `mans_decode.jsonl` line 41, and the checker fails without its `out` position. - **E9 condition (2).** With the condition weakened to the old claim, `residual_form_condition_is_tight` fails. - **ReLU rule (5).** With the old rule, the checker fails on 3 lowered graphs. - **Checker (6).** Each of these fails the checker: - a changed `profiles` tag; - a lowering vector whose graph was swapped; - removing the `acc32` parameter conditions; - the all-taps transposed-convolution rule; - not counting `check` policies against `acc32`; - flooring `igdn` once; - classing `rq.p` as `acc`. - **The eleven readings (11).** Each fails one new line. - **`run` taking a `Graph` (12).** The `compile_fail` doc test fails ("compiled successfully"). ## Checks run - `check-public-names.sh` and `check-comparative-prose.sh` were run one file at a time on every changed text-bearing file and on this body. All were clean. - `check-no-vanity-metrics.sh`, `check-wai-section-refs.py` and `check-workflow-concurrency.sh` were clean. - Open PRs were checked first. None touches `wai-ops`, `ops-conformance`, `wai_ops_check.py` or `wai-ops.yml`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 18 commits 2026-10-09 19:35:01 -04:00

wai: integer-operators, the integer operator set wai-ops/1 (Draft text) ... 1f6834e98d

The proposed extension text as drafted: the operators and their exact
integer arithmetic, the tensor range policies, the acc64 and acc32
profiles, the static bounds rules and the bounds certificate, the
accelerator subset, the WHG1 graph form, profile declaration, the
relation to the determinism tiers, the canonical lowerings of the
existing integer network forms, and conformance.

This commit is the text as drafted, unedited; the next commits
reconcile it with what lands beside it.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai: integer-operators lands beside its payload text ... 116fcb520f

integer-payloads gains the text the operator set depends on:
- §9: the members and checks of entropy.json, and the layers'
  arithmetic is now integer-operators §13.2 (WHM1) and §13.3 (WAM1);
- §13: the wai.neural.int_synth payload and its set, int_synth.json,
  with the checks the reference decoder makes only once it decodes
  through its lowering listed as such;
- §14: WIM1 and the WMB1 bundle of wai.neural.int_mlicpp, including
  that the entropy network reads every element of y not yet decoded
  as 0, and the one afrac in 1..=30 its networks and tables share.

integer-operators is reconciled with that:
- §15.2 points at those sections instead of carrying a second copy,
  and the §13.5 payload column cites them (WIA1 and WIS1 now name
  integer-payloads, not this text's own §5 and §6);
- §15.1 separates what changes now from what lands with each
  capability's lowering, and §15.3 says each change takes effect then;
- §13.6.1: the hyper-scale shift members are [1, C, 1, 1] in the
  bundle, not [C]; a segment's payload is defined (after the marker
  and length field), and each is one entropy substream within the
  configuration determinism-tiers §5 scopes;
- §8.1: a product or sum of more than two operands written without
  Σ is a left fold as written, which keeps the saturated flag
  independent of evaluation order, and the 512-bit width is shown to
  be needed (igdn.x2 at ±2^255 forms 2^510);
- the status block says the reference crate, tool and corpus follow
  this Draft, and names the decoders that are the reference until then.

The README names the extension and the CHANGELOG records it.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai: integer-operators, the rules the corpus relied on, written into the text ... 64e37d8ebf

A review of the D2a corpus found rules that only the crate and the corpus README
stated, and two width claims that do not hold. This writes each into the text.

- §5E: a condition an operator states is refused before any symbol, with
  model_mismatch (field_range for E2, geometry_mismatch for the shapes E11 and
  E12 read). E8's table and bound checks are model_mismatch; only its window
  refusals are stream_exhausted. E5, E6, E7 and E10 state their conditions.
- E9: the 32-bit form fits i32 only when lo − 131070 and hi + 131070 also do;
  near the i32 limits it does not.
- E12 and §7.4: rate_predict's product (b − a)·ρ reaches 2^48 and rdiv's
  2|n| + d passes it; every value fits i50, not 47 bits.
- §4: step 1 runs input by input; step 3 checks the sizes an operator forms
  against 2^26, then the shape rule, then max_elems; step 4 applies the inputs'
  policies first.
- §5.3: the cap is on the uncropped output, cout·uh·uw. §5.10: crop starts are
  at least 0, and at load a scalar start is planned at 0.
- §10.3: a refused decode changes no state. §10.4: chscale's m_bytes and
  layernorm_c's g_bytes are 4 or 8.
- §13.2: a tensor read by a ReLU, other than the network's input, is derived.
- §14.1: decode inputs are data inputs only; a refused load lists both
  profiles; stage modes, the predictors' fields and layouts, and coding_order's
  indices are normative; and `at`, mans_decode's position rule included.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai: integer-operators §8.3, the interval of subpos_merge and crop_to ... 7600816a40

The movement row gave "the input's interval" and the hull only for concat.
subpos_merge reads four inputs and crop_to two; the row now says that
subpos_merge, like concat, takes the hull of its inputs' intervals, and that
crop_to takes its first input's, which a bounds pass written from the text
needs in order to agree with the certified tags.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai: integer-operators §14.1, the checker recomputes profiles too ... fee4516886

`profiles` decides which implementations must reproduce a vector, so an
independent checker that copies it checks nothing about it. The checker now
recomputes it from its own bounds pass (§8), as it does `load` and `expect`.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: the reference crate for wai-ops/1 (WHG1, plans, interpreter, stage operators, lowerings) ... 41737afb22

A new crate, wai/wai-ops: no_std with alloc, no dependencies.

- xint: a 512-bit signed integer with the saturation of integer-operators §8.1.
- json: a reader that keeps numbers as written, and the canonical writer of §8.5.
- graph: WHG1 parse and write, load steps 1–6 of §10.5.
- plan: the load-time plan (step 7) and the run-time plan (§4).
- interp: every graph operator of §5, exact in i128, with the policies and the
  sequence state of §10.3.
- stage: E1–E13; E1 with both escapes, both end rules and both table rules, E8
  total with every refusal stream_exhausted.
- lower: int_synth/1, whm1/1, wam1/1, wmb1/1, world/1 and jpegai-int/1 (§13.6.1),
  each writing §13.0's canonical bytes.

Load step 8 (the bounds pass and the verdict) is not built: without the
`uncertified` feature every graph is refused at step 8; with it, step 8 is skipped.

tests/goldens.rs lowers every committed set and decodes its committed payload
through the interpreter and the stage operators, and every output digest
reproduces: the four int_synth sets, both world clips frame by frame, the
int_hyper tiny set, splat, audio and int_mlicpp. Opt-in, against data that is not
committed: the jpegai scale path and both mANS decodes equal the legacy decoder's
every intermediate on a real codestream, and E8 equals the reference encoder's
streams and tables.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: the conformance corpus, its generator, and the WASI and browser-engine legs ... 608a1bea8d

wai/ops-conformance/, in integer-operators §14.1's format, written by
`wai-ops vectors gen`:

- vectors/<operator>.jsonl: one-operator graph vectors for every graph operator:
  random cases over several magnitudes, and the coverage classes of §14.1:
  bound-attaining inputs, rounding ties at every mode and the shifts the class
  names, geometry, the i32 limits and one past them, check and scalar ranges at
  their ends and one past, every run-time shape refusal, and the distinguishing
  cases (per-term igdn floors, leaky floors, softmax rows, elu(0), a half mean in
  layernorm_c, ε = 2^64 − 1, exp at n = 62 and 63).
- stage/<operator>.jsonl: E1–E13. E1 under every mode, with each strict refusal
  alone and in each pair one symbol can give, under both end rules; E8 with zero
  tails, short streams, and escapes at bounds of 128 and 255.
- graphs/: the phase form against conv_transpose (the generator checks the two
  outputs agree), a state carried across three decodes, a refusal at each load
  check (steps 1–7) and at each run step, and every lowering on a small set.
- certificates/<capability>/<set digest>/<role>.whg1: the lowered graphs of every
  committed set and of the small sets, with certificates/index.json.

Every vector's `profiles` is the profiles its graph meets under §7 and §8.3, from
the generator's own tagger; a case that meets neither is not written (its load
refusal is a D2b vector). The certifier must agree with every tag.

`wai-ops vectors verify` recomputes every vector file, re-lowers every set and
regenerates the corpus, and requires every byte to match. It passes natively, as
the same binary built for wasm32-wasip2 under wasmtime, and through wai-ops/node,
the recomputation as a wasm32-unknown-unknown module run by Node.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: an independent checker, wai_ops_check.py, for the vectors and the lowerings ... 0ca38c3917

wai/tools/wai_ops_check.py, Python standard library only, sharing no code with
wai-ops. From integer-operators (and integer-payloads for the source forms), it
recomputes every vector file of ops-conformance: each graph vector's `load` (WHG1
and load steps 1–7) and every decode's `expect` (§4, every operator of §5, the
transposed convolution in its gather form), and each stage vector's `expect` (§5E);
writes each file canonically and requires the committed bytes. It re-lowers every
set the index lists by §13 and requires each lowered graph's bytes and each set's
digest. On the committed corpus it rewrites all 53 vector files and all 28 lowered
graphs byte for byte; a changed output, a changed symbol and a changed byte of a
lowered graph each fail it.

Independence: written in the same session as wai-ops, after it, from the text, with
the text open and the Rust closed, and structured differently where the text allows.
It is not the separate text-only session the plan asks for; that session is still
owed before D2a merges.

graph.rs gains tests that a graph round-trips, that the default build refuses every
graph at load step 8, and that the `uncertified` switch skips it.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: CI on every leg the corpus runs on, and the corpus README ... 06cfd42db4

.github/workflows/wai-ops.yml, with a concurrency group per ref:

- linux, linux-arm64, macos: the unit tests in the default build (load step 8
  refuses every graph) and with the `uncertified` switch, the goldens in debug and
  release, and `wai-ops vectors verify`;
- wasm32-wasip2 under wasmtime 38.0.3: `wai-ops vectors verify`;
- wasm32-unknown-unknown under Node: every vector file recomputed;
- tools/wai_ops_check.py, the independent checker, and the concurrency gate.

ops-conformance/README.md names the layout, the conventions both recomputations
follow where §14.1 leaves a choice (data inputs only in `inputs`, a refused decode
leaves the state, each stage operator's `in`, `modes` and `expect`, and what `at`
reads for each), the lowered sets' digests, and how to regenerate and verify.

The three goldens that need data this repository does not commit (a jpegai bundle,
a legacy decoder's intermediates on one codestream, the reference encoder's mANS
streams) are now `#[ignore]` with the reason, so CI reports them ignored rather than
passed; locally, with the data, all three pass. The tagger now applies §8.5's fit
rule as written; the corpus is unchanged by it.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: the strict run-out case alone, not paired with a non-minimal count ... b0fd9f0d78

Its stream's groups were 2, 6, 0: a zero last group, so under final_only it showed
the non-minimal refusal, which has its own paired case. Now 1, 6: under canonical it
is refused at the symbol (stream_exhausted), under final_only the symbol decodes and
the end refuses (stream_exhausted at 1).

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: mans_decode reports a refusal at the position whose step refuses ... 6aa29469af

Only the `in` step set the reported position, so a refusal in a position's
`out` step (in sgm, the flush after an escape) named the last `in` of its
group. mans_decode/sgm/40 said at=11; symbol 10's escape flush refuses, and it
now says at=10. A flush that belongs to no single position reports the last
position whose `in` step ran, as integer-operators §14.1 now states.

The checker sets the position at each `in` and `out` step and names the
group, remainder and row-end flushes as such, following §14.1's wording.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: residual_step's 32-bit form, with the conditions under which it fits i32 ... 891dc08dfd

E9's 32-bit form fits i32 only when hi − lo ≤ 65535 and lo − 131070 and
hi + 131070 also fit. At lo = 2^31 − 65536, hi = 2^31 − 1, q = 65535,
pred = hi, r = 2, it formed hi + 131070 and the function overflowed.

- `residual_step_i32` asserts its conditions (`i32_form_fits`) in debug builds.
- `residual_identity_holds` covers the ranges nearest the i32 limits on which
  the form still fits, and `residual_form_condition_is_tight` shows that one
  step past them it does not, while the exact form gives the clamped value.
- stage/residual_step.jsonl gains 32 vectors at the i32 limits, at r = ±R and
  ±(R + 1), with q = 1 and q = 65535, as §14.1 item 7 asks.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: rate_predict vectors at the i16 extremes with rates near 2^32 ... f6e872a35c

With prev = [−32768, 32767], rate_num = 2^32 − 1 and rate_den = 2^32 − 2,
(b − a)·ρ is 65535·(2^32 − 2), just under 2^48, and rdiv's 2|n| + d passes
2^48 (§5E E12 now states the widths). Three vectors pin the results: both
orders of the extremes, and two channels at rate_den = 2^31.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: a tensor a ReLU reads inside a WHM1 network is derived, as §13.2 says ... 603a0b803d

§13.2 gives `check` only to an x_ℓ that a layer of tag 0, 1, 2 or 4 reads,
and `check [−2^63, I64]` to a network input that no such layer reads; every
other tensor is `derived`. The lowering and the checker both gave every x_ℓ a
ReLU reads `check [−2^63, I64]`, so a reader of the text could not reproduce
three committed graphs.

Both now follow the text. The checker's `x_record` is rewritten from the
§13.2 wording, not from the crate. Regenerated: the h_s graph of the int_hyper
set 7aceaa1a… and of the int_mlicpp sets 07e1835d… and 7ef44f3b…, and the
lower_whm1 and lower_wmb1 vectors that embed them. No output changes: the
range they drop held every i64.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai_ops_check.py: load step 8, profiles recomputed, lowering vectors tied to their roles ... 8aff0cb5d6

The checker copied each vector's `profiles` from the committed line, never ran
load step 8, and took the graph bytes of graphs/lower_*.jsonl as given. So a
regression in the generator's tagger, or a lowering vector whose graph was not
its role as lowered, would have passed.

- A bounds pass and verdict written from integer-operators §8.1–§8.5: every
  +, −, × and floor division saturated at ±2^255 with the node's saturated flag
  (§8.1), the term and partial-sum intervals (§8.2), each operator's rule
  (§8.3), the classes and parameter conditions of §7, and what a node fits and
  the verdict (§8.5). It writes no certificate.
- Load step 8: an empty `check` interval, a lut16 input range past ±32767, or
  a verdict that meets neither profile refuses the graph (model_mismatch).
- `profiles` is recomputed: both profiles for a refused load, else exactly
  those the verdict meets (§14.1). It agrees with all 1,599 committed tags, and
  with Appendix C's predictions for every committed set (int_synth gradient,
  bloom and facade acc32; photo and every WHM1, WAM1 and WMB1 set acc64).
- Each lowering vector's id names <file>/<set>/<role>; its graph must be that
  role as re-lowered, and every role must have one.

The README now points to §14.1 for every field, and lists the coverage classes
of §14.1 item 6 that wait for step 8 in wai-ops: sigmoid and elu at −2^63, and
an rq whose q passes 64 bits while y fits.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: a vector for each run and load rule the text now states ... bef055304b

A review found rules that only the crate and the README settled, and that no
vector pinned: changing the checker to another reading of each changed no
committed byte. integer-operators now states each one, and each now has a
vector that a different reading fails:

- state: a refused decode changes no state; until a decode completes, a state
  input is `init`, sized by input 0 of the decode being made (§10.3).
- run step 1 runs input by input; an input with a dimension of 0 is
  model_mismatch (§4).
- run step 3: conv_transpose's uncropped output of cout planes is capped, not
  one plane; the caps come before the shape rule, both for that output and for
  an uncropped side; the shape rule comes before max_elems (crop_to) (§4, §5.3).
- crop: a scalar start of −1 is refused though −1 + h ≤ H, and at load a
  scalar start is planned at 0, not at its range's low end (§5.10).
- load step 5: chscale's m_bytes and layernorm_c's g_bytes of 2 are refused,
  and 4 loads (§10.4).

subpos_merge now caps its output sides before its shape rule, in the crate
and the checker, as §4 states for every operator. No input within the caps
can tell the two orders apart.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops: the interpreter runs only a loaded graph, so step 8 cannot be bypassed ... 5e43805620

Load step 8 was enforced at `graph::load` only. `interp::run` took any
`&Graph`, and a lowering's graph, a parsed one or a struct literal reached it
without step 8: in the default build, `lower::int_synth` then `run` decoded the
gradient set to its committed digest while `graph::load` of the same bytes
refused it at Load(8).

- `graph::Loaded` holds a graph that passed every load step; its field is
  private and only `graph::load` makes one. `run` takes `&Loaded`.
- A `Graph`, parsed, lowered or built in place, is data. A compile_fail
  example (E0308) on `Loaded` shows a lowered graph cannot be passed to `run`.
- The goldens load every lowered graph from its bytes before running it, so
  their `uncertified` gate now guards something.
- tests/step8.rs, in every build: each lowered int_synth graph is refused at
  Load(8) without the switch and loads with it.
- Cargo.toml says who enables the switch, and that no decoder may.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

wai-ops.yml: the goldens' digest file in the filter; every test on the 32-bit leg ... 98b5088dfe

- The goldens compare against wai/neural-conformance/sha256.json, which the
  `paths:` filters did not match (the repo's own matcher said False). Both
  lists now take wai/neural-conformance/**, so a re-pinned digest runs wai-ops.
- The wasip2 leg ran only `vectors verify`, so the unit tests and the goldens
  never ran on a 32-bit target. It now runs `cargo test` under wasmtime in the
  default build (unit and step-8 tests) and with `uncertified` (unit tests,
  goldens, step-8 test), with the wai directory preopened at its own absolute
  path for the files the tests read. Both pass locally under wasmtime.
- The native default-build step runs `cargo test`, not `--lib`, so the step-8
  test and the doc tests that keep an unloaded graph from running are run.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot added 1 commit 2026-10-10 02:11:50 -04:00

int_kernels_vectors: ops-conformance states no digest of decoded output ... f81f28d43c

every_decoded_output_states_a_sha256 enumerates every wai/*-conformance/
directory, and the new ops-conformance had neither a sha256.json sidecar nor an
exclusion, so the cargo-class corpora job failed reading the sidecar.

It takes an exclusion, because SPEC §7 *Digests* does not reach it: the rule
binds a vector that states a digest of a parameter-set decode's output, and no
file there states one. Every operator, stage and graph vector, the lower_*
decodes of the sets under sets/ included, states its output integers in full or
its refusal code; certificates/index.json states only each set's SHA-256 (a
parameter-set identity), and the lowered graphs are held as bytes and compared
byte for byte. The output digests a capability decoded through its lowering
must reproduce (integer-operators §14.4) stay in that capability's own corpus,
whose sidecars wai-ops's goldens already read.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot added 1 commit 2026-10-10 02:13:07 -04:00

ops-conformance: say why the corpus carries no sha256.json ... 9b748c97bd

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot merged commit 5be238af32 into main 2026-10-10 17:17:02 -04:00

dcharlot referenced this pull request from a commit 2026-10-10 17:17:04 -04:00

Merge pull request 'wai-ops: the reference crate and conformance vectors for wai-ops/1 (D2a)' (#206) from wai/d2a-operators-crate into main

dcharlot referenced this pull request from a commit 2026-10-10 17:23:08 -04:00

Merge origin/main into wai/generate-score-cli

dcharlot referenced this pull request from a commit 2026-10-10 17:26:53 -04:00

Merge wai/generate-score-cli (with main) into wai/reach-builds

dcharlot referenced this pull request from a commit 2026-10-10 22:23:54 -04:00

Merge wai/reach-builds (with #197 and main) into wai/d1-record-true

dcharlot referenced this pull request from a commit 2026-10-10 22:24:07 -04:00

Merge wai/d1-record-true (with #205, #197 and main) into wai/w4-4-staged-packages

dcharlot referenced this pull request 2026-10-11 22:25:20 -04:00

wai-ops: the bounds pass, certificates from two certifiers, and the operator set's Kani harnesses (D2b) #221

dcharlot referenced this pull request from a commit 2026-10-13 00:53:47 -04:00

Merge main (at 5be238af, with D2a #206) into wai/d2b-bounds

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!206

No description provided.