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

Merged

dcharlot merged 48 commits from wai/d2b-bounds into main 2026-10-13 00:53:47 -04:00

Conversation 0 Commits 48 Files changed 85 +7654 -1488

dcharlot commented 2026-10-11 22:25:20 -04:00

Owner

Copy link

D2b of the integer operator set wai-ops/1 (extensions/integer-operators.md, Draft): load step 8, the bounds pass and its certificate, the wai-verify tool, certificates of every committed set from two certifiers, and the operator set's model-checker harnesses. Follows #206 (D2a).

What is in it

• wai_ops::bounds. §8.1–§8.5: 512-bit intervals with saturation per operation, each rule of §8.3, admissible ranges (§8.4), and the canonical certificate writer. Load step 8 is on, and the uncertified switch is gone: the interpreter runs only a loaded graph, so nothing decodes a set its certificate does not admit.
• wai-verify (bounds, lower, vectors), folded from wai-ops' old binary, with --check, --witness and --advise. The witness for photo's node 6 is a node-local graph whose input attains convT.acc's upper end.
• Certificates for every committed set, both falsification sets, and the two sets held outside the tree, by digest (table below). There are also 28 vectors whose outcome only step 8 decides.
• The independent certifier (tools/wai_ops_check.py), written from the text alone, recomputes every certificate byte for byte.
• wai_ops::limb32. A reference model of the 32-bit fabric arithmetic for acc32's two products: the 16-bit-limb product, and the epilogue on two words with shifts that take their amount mod 32. Unit tests compare it with i64 arithmetic, and K2 and K2b prove it.
• A run can be observed. interp::run_observed reports every value under every key of Table 8.5-A; run is the same with an observer that compiles to nothing. bounds::Within holds a run to its certificate. Every golden decode now runs observed and must stay inside its certified intervals. tests/trace.rs does the same for hand-built graphs at the edge of acc64.
• Kernels. The interpreter is one function per operator, which eval dispatches to. The plan's shape rules are functions op_sizes applies. mans_decode checks its bounds before it builds its tables; both are load checks with one refusal, so the order is not observable. The latent table build visits slots by index. The parser's zero check loops to a constant count. Every vector file, lowered graph and certificate is unchanged.
• Kani. The test plan's harnesses are in wai-ops/src/proofs/, hosted by wai-verify, which includes wai-ops' modules at its root under cfg(kani) (results below).

Certificates

capability	set	digest	lowering	acc64	acc32	first failure under acc32 / acc64
wai.audio.int_codec	audio	132958122b25…	wam1/1	yes	no	g_s input 0, range, 47 bits
wai.audio.int_codec	audio	8eca5bfdc1d8…	wam1/1	yes	no	g_s input 0, range, 53 bits
wai.image.jpegai	jpegai/v1 (external, by digest)	3e243dc11566…	jpegai-int/1	yes	yes	—
wai.image.jpegai	jpegai	60020d0657c4…	jpegai-int/1	yes	yes	—
wai.neural.int_hyper	tiny	13e8b0d18e00…	whm1/1	yes	no	h_s input 0, range, 53 bits
wai.neural.int_hyper	hyper	7aceaa1aad14…	whm1/1	yes	no	h_s input 0, range, 52 bits
wai.neural.int_hyper	sota (external, by digest)	f16fd09cd79b…	whm1/1	yes	no	h_s input 0, range, 41 bits
wai.neural.int_mlicpp	mlicpp	07e1835da603…	wmb1/1	yes	no	h_s input 0, range, 54 bits
wai.neural.int_mlicpp	int_mlicpp	7ef44f3b1fc4…	wmb1/1	yes	no	h_s input 0, range, 47 bits
wai.neural.int_synth	synth	00c2274be6b4…	int_synth/1	yes	yes	—
wai.neural.int_synth	gradient	1c4705d17c01…	int_synth/1	yes	yes	—
wai.neural.int_synth	bloom	21f092964e13…	int_synth/1	yes	yes	—
wai.neural.int_synth	photo	50868e72f5f1…	int_synth/1	yes	no	synth node 6, convT.acc, 36 bits
wai.neural.int_synth	claim_acc32 (falsification set)	76916c8f85da…	int_synth/1	yes	no	synth node 1, convT.acc, 33 bits
wai.neural.int_synth	overflow_acc64 (falsification set)	b35460f39f31…	int_synth/1	no	no	synth node 0, convT.acc, 37 bits / synth node 2, convT.acc, 65 bits
wai.neural.int_synth	facade	c6a362696d61…	int_synth/1	yes	yes	—
wai.splat.int_codec	splat	033a37c9d29d…	whm1/1	yes	no	g_s input 0, range, 44 bits
wai.video.int_hyper	tiny	13e8b0d18e00…	whm1/1	yes	no	h_s input 0, range, 53 bits
wai.world.model	world2	34986fa89648…	world/1	yes	no	T input 0, range, 64 bits
wai.world.model	world	5291a52bdbf2…	world/1	yes	no	T input 0, range, 64 bits
wai.world.model	world	da046216ff94…	world/1	yes	no	T input 0, range, 64 bits

The verdicts match Appendix C. Photo first fails acc32 at node 6, with convT.acc = [−25165614250, 26172239136] (36 bits). Every WHM1/WAM1/world set fails acc32 at its input range, which by construction is the legacy guard (O1, O2).

Independence

• wai_ops_check.py (Python standard library only) shares no code with wai-ops. Its session read only Part 1. It rewrites every vector file and every lowered graph, and recomputes all 21 certificates byte for byte. The two external sets are recomputed with their files supplied: in this session locally, and in CI in wai-sota-vectors.yml and wai-jpegai-e2e.yml.
• It also agrees with wai-ops on every graph-vector graph and every saturating graph.
• Its certifier half was written before any comparison with the Rust output. Each disagreement found then was settled against the text.
• Lowered graphs and certificates are byte-identical on every leg of wai-ops.yml: Linux x86_64, Linux arm64, macOS arm64, and wasm32-wasip2 under wasmtime.

Kani

Every harness was run alone, one at a time, with CARGO_BUILD_JOBS=8. Most runs were on an idle 32-core host; a few early runs were on the dev Mac, then heavily loaded by other work. Times are Kani's verification time.

Where a harness would have proved two multiplier, divider or isqrt circuits equal, or executed 512-bit arithmetic on symbolic operands, it does not close in bounded time. Those harnesses were restated:

• The soundness harnesses check §8.3's rules restated in i128/i64 (proofs/rules.rs). That the bounds pass computes those same rules is what the independent certifier shows, on every certificate.
• Harnesses read the interpreter's own intermediates through an observer instead of recomputing them.
• Some statements are split into lemmas that together are the property.

A harness whose window still did not close within its cap is gated by cfg(kani_open). It is kept, with its statement, and runs only on request: RUSTFLAGS="--cfg kani_open" cargo kani --lib --exact --harness <name>. CI compiles only harnesses that verified.

Verified (in CI):

row	harness	window	time
K1	k01_rq_is_its_definition	v, m, bias any i64; s ≤ 127; every rounding and bias placement	149 s
K2	k02_limb_combination_is_exact, …_partials_do_not_wrap, …_signs	every partial product; every u32, i32, i64	0.4 s, 0.05 s, 0.03 s
K2b	k02b_limb_epilogue	every product acc32 allows, s ≤ 63, every rounding, post in i32	6.4 s
K3	k03_rounding_is_its_definition, …_is_monotone	every i128 p, s ≤ 127	80 s, 7.4 s
K4	k04_term_lies_in_its_interval; k04_partial_sums_lie_in_a (induction: base, and one step over every value, so any number of terms)	i8 terms; every i32	26 s, 0.2 s
K5	k05_chunked_i32_sums	≤ 8 terms, every partition, every term interval in i32	27 s
K6	k06_dot_lane_never_wraps	n = 2 and 4, ≤ 8 products	46 s
K9	k09_conv_transpose_residues (one position reads one residue; with K4's lemma)	y ≤ 64, ph ≤ 2, sh ≤ 3	0.07 s
K11	k11_isqrt_is_monotone, k11_corner_hull_holds_products (with K3 and the first part, gated)	u32; i8	118 s, 106 s
K12	k12_largest_returns_the_maximum (every threshold); k12_p_leaky_is_monotone, k12_p_conv_is_monotone	X in u32, parameters in u8/u16	248 s, 0.5 s, 16 s
K13	k13_isqrt_u128_is_floor_sqrt; k13_isqrt_i512_is_floor_sqrt; k13_isqrt_ceil_i512_is_ceil_sqrt	n < 2^32	104 s, 672 s, 1079 s
K14	k14_leaky_bounds_sound_i8	interval, value and a in i8, f ≤ 63	123 s
K15	k15_lut16_index_is_total	every range in [−32767, 32767]; both one-past ends refused	18.5 s
K16	k16_pixel_shuffle_is_a_bijection, k16_pixel_unshuffle_is_a_bijection	four shapes each, planes ≤ 4×4	9.9 s, 13 s
K17	k17_exp_neg_q16_ranges_i32	x ∈ [−(2^31 − 1), 0]	22 s
K19	k19_sigmoid_ranges; k19_elu_ranges (certified α)	every i64 v > −2^63; every interval and α	8.4 s, 621 s
K23	k23_bucket_ceil_…, k23_bucket_floor_…	≤ 4 edges, every σ pair	0.8 s, 3.4 s
K26	k26_rans64_t2_is_total	32-byte streams, ≤ 3 symbols, both escapes and end rules	876 s
K27	k27_mans_bounds_are_unsigned	every bound outside [0, 255]	0.7 s
K28	k28_mans_entry_fields	every next ∈ [1, 511], every symbol	0.1 s
K29	k29_residual_step_32bit_identity_every_range; …_registered_ranges	every range of the form; U8 and I16	1080 s, 87 s
K30	k30_scale_index_in_range, k30_block_stat_in_range, k30_band_lookup_in_range	as stated in each	0.06 s, 120 s, 1.3 s
K32	k32_sat_is_a_monotone_clamp; k32_xint_add_sub_neg_exact_at_the_saturation_edges	every pair of 512-bit values; edges ±(2^255 − d), d < 2^16	7.2 s, 29 s

Did not close; gated by cfg(kani_open) (cap 10 or 20 minutes, after the restatements above). The windows are the designed ones, and where a narrower one was also tried, that one too:

• K7, K8 (conv_transpose gather and phase forms against the kernel, four concrete shapes, a symbolic position) and K10 (igdn against the reference and the fast kernel; also one channel, one position). Covered by the graphs/phase vectors, the igdn equivalence tests in wai-rs and the trace tests.
• K4 and K9 at the kernel; K11's first part; K22 (gram, apply); K18 (softmax, W ≤ 4 and W ≤ 2); K20 (L1, ε below 2^31); K21 (L2, ε ≤ 2^20); K14 at i32 and i16. For these, Kani proves the rules' lemmas (K4, K9, K11 above). The trace tests hold every value the interpreter forms, in every golden decode and on the extreme graphs, to its certified interval.
• K12 p_igdn (512-bit isqrt on symbolic operands), K17 at its full window (i64), K32's product at the edges.
• K16 subpos and pad/crop; K31 (WHG1 parse, ≤ 96 bytes); K33 (run-time plan: conv, conv_transpose, multi-input).
• K24, K25 (strict escape and canonical end against the text's decoder, 64- and 32-byte streams), K27 (span decodes at fixed tables, 16-byte streams), K28's every-slot harness. The stage vectors cover these, with refusals and their order.

Retiring int_transform's three harnesses (O14). Not done. O14 retires them once K18 and K20 pass, and neither closed at its window. They stay, as does SPEC's text about them.

Harness defects found and fixed, not property failures:

• unwinding bounds on byte comparisons and limb loops;
• an overflow in K6's own assumption;
• K19's α = −2^63, which the certificate refuses;
• K26's refusal of an empty range.

No harness found a defect in wai-ops.

Falsification

Each fault went into a copy of the committed tree, with the harness run alone; each harness verified green on the unmodified tree at the same commit first.

fault	harness	result
limb32::combine drops its second carry	K2 k02_limb_combination_is_exact	FAILED, "the carries are exact" (2 s)
round breaks a half_even tie toward odd	K3 k03_rounding_is_its_definition	FAILED, "R_half_even(p, s) as §2 defines it" (37 s)
rq_apply narrows q to i64 before the post bias	K1 k01_rq_is_its_definition	FAILED, "rq.y = q + post" (152 s)

For the certificate rows of Part 3.5, wai-ops.yml runs the two falsification sets on every leg: the overflow set must fail acc64 at load, and the set claiming acc32 must fail it.

Self-review

• Bound soundness. The photo witness runs observed: every value lies in node 6's certified intervals, and the accumulator with its bias attains convT.acc's upper end. The extreme graphs (tests/trace.rs) and every golden decode run observed too, with no value outside its interval and no key the certificate does not record. Building them, two graphs I expected to certify were refused at load. The refusals were correct: a softmax spread of 2^63, and an elu α of −2^63. The tests now assert both refusals.
• CI reachability.
  • wai-formal-verification.yml is now seven shards by measured time. A first job (check_shards.py) holds the shards to covering every compiled harness exactly once. The path filter includes wai/wai-ops/src/**.
  • Three wai-ops goldens are ignored for want of uncommitted inputs, and were run here and pass. The scale-path one now also runs in wai-jpegai-e2e.yml, which fetches the bundle. The other two need assets that are not redistributable.
  • limb32's unit tests and tests/trace.rs run on every wai-ops.yml leg, wasm32-wasip2 included. The witness test runs on the three native legs.
• Goldens. No file under wai-rs, nor any other conformance corpus, changes. The gate (build, lib tests, carriage, every corpus, fast kernels, byte-exact, wasm32, neural gates) is GREEN on this head.
• Public text. The name and comparative-prose checks pass on every changed text file, and the workflow-concurrency check passes.

Checked on this head (8f5e70c8, main at 4ab66d24 merged):

• wai-ops tests, debug and release; wai-verify tests and vectors verify;
• the gate, GREEN;
• the seven shards, each run as CI runs it (cargo kani --lib with the shard's filters), on the idle host:

shard	harnesses	time
integer-core (wai-rs' own)	17	244 s
arith	13	487 s
isqrt512	2	1619 s
stage	8	111 s
stage-long	2	1977 s
sound	8	470 s
plan	6	361 s

check_shards.py reports 56 harnesses in 7 shards, with 31 gated by cfg(kani_open) and in none.

The wasm32-wasip2 run and wai_ops_check.py with both external sets ran at 2419b914. Since then, the only wai-ops changes are under src/proofs/, compiled only under cfg(kani). The checker is unchanged.

Main has since moved to fe0282d6 (#220). That change touches only wai-web and its wasm workflow, none of this branch's files, and merges without conflict.

The forge CI runs on this pull request.

🤖 Generated with Claude Code

D2b of the integer operator set `wai-ops/1` (`extensions/integer-operators.md`, Draft): load step 8, the bounds pass and its certificate, the `wai-verify` tool, certificates of every committed set from two certifiers, and the operator set's model-checker harnesses. Follows #206 (D2a). ## What is in it - **`wai_ops::bounds`.** §8.1–§8.5: 512-bit intervals with saturation per operation, each rule of §8.3, admissible ranges (§8.4), and the canonical certificate writer. Load step 8 is on, and the `uncertified` switch is gone: the interpreter runs only a loaded graph, so nothing decodes a set its certificate does not admit. - **`wai-verify`** (`bounds`, `lower`, `vectors`), folded from wai-ops' old binary, with `--check`, `--witness` and `--advise`. The witness for photo's node 6 is a node-local graph whose input attains `convT.acc`'s upper end. - **Certificates** for every committed set, both falsification sets, and the two sets held outside the tree, by digest (table below). There are also 28 vectors whose outcome only step 8 decides. - **The independent certifier** (`tools/wai_ops_check.py`), written from the text alone, recomputes every certificate byte for byte. - **`wai_ops::limb32`.** A reference model of the 32-bit fabric arithmetic for `acc32`'s two products: the 16-bit-limb product, and the epilogue on two words with shifts that take their amount mod 32. Unit tests compare it with `i64` arithmetic, and K2 and K2b prove it. - **A run can be observed.** `interp::run_observed` reports every value under every key of Table 8.5-A; `run` is the same with an observer that compiles to nothing. `bounds::Within` holds a run to its certificate. Every golden decode now runs observed and must stay inside its certified intervals. `tests/trace.rs` does the same for hand-built graphs at the edge of `acc64`. - **Kernels.** The interpreter is one function per operator, which `eval` dispatches to. The plan's shape rules are functions `op_sizes` applies. `mans_decode` checks its bounds before it builds its tables; both are load checks with one refusal, so the order is not observable. The latent table build visits slots by index. The parser's zero check loops to a constant count. Every vector file, lowered graph and certificate is unchanged. - **Kani.** The test plan's harnesses are in `wai-ops/src/proofs/`, hosted by `wai-verify`, which includes wai-ops' modules at its root under `cfg(kani)` (results below). ## Certificates | capability | set | digest | lowering | acc64 | acc32 | first failure under acc32 / acc64 | |---|---|---|---|---|---|---| | `wai.audio.int_codec` | audio | `132958122b25…` | `wam1/1` | yes | no | g_s input 0, `range`, 47 bits | | `wai.audio.int_codec` | audio | `8eca5bfdc1d8…` | `wam1/1` | yes | no | g_s input 0, `range`, 53 bits | | `wai.image.jpegai` | jpegai/v1 (external, by digest) | `3e243dc11566…` | `jpegai-int/1` | yes | yes | — | | `wai.image.jpegai` | jpegai | `60020d0657c4…` | `jpegai-int/1` | yes | yes | — | | `wai.neural.int_hyper` | tiny | `13e8b0d18e00…` | `whm1/1` | yes | no | h_s input 0, `range`, 53 bits | | `wai.neural.int_hyper` | hyper | `7aceaa1aad14…` | `whm1/1` | yes | no | h_s input 0, `range`, 52 bits | | `wai.neural.int_hyper` | sota (external, by digest) | `f16fd09cd79b…` | `whm1/1` | yes | no | h_s input 0, `range`, 41 bits | | `wai.neural.int_mlicpp` | mlicpp | `07e1835da603…` | `wmb1/1` | yes | no | h_s input 0, `range`, 54 bits | | `wai.neural.int_mlicpp` | int_mlicpp | `7ef44f3b1fc4…` | `wmb1/1` | yes | no | h_s input 0, `range`, 47 bits | | `wai.neural.int_synth` | synth | `00c2274be6b4…` | `int_synth/1` | yes | yes | — | | `wai.neural.int_synth` | gradient | `1c4705d17c01…` | `int_synth/1` | yes | yes | — | | `wai.neural.int_synth` | bloom | `21f092964e13…` | `int_synth/1` | yes | yes | — | | `wai.neural.int_synth` | photo | `50868e72f5f1…` | `int_synth/1` | yes | no | synth node 6, `convT.acc`, 36 bits | | `wai.neural.int_synth` | claim_acc32 (falsification set) | `76916c8f85da…` | `int_synth/1` | yes | no | synth node 1, `convT.acc`, 33 bits | | `wai.neural.int_synth` | overflow_acc64 (falsification set) | `b35460f39f31…` | `int_synth/1` | no | no | synth node 0, `convT.acc`, 37 bits / synth node 2, `convT.acc`, 65 bits | | `wai.neural.int_synth` | facade | `c6a362696d61…` | `int_synth/1` | yes | yes | — | | `wai.splat.int_codec` | splat | `033a37c9d29d…` | `whm1/1` | yes | no | g_s input 0, `range`, 44 bits | | `wai.video.int_hyper` | tiny | `13e8b0d18e00…` | `whm1/1` | yes | no | h_s input 0, `range`, 53 bits | | `wai.world.model` | world2 | `34986fa89648…` | `world/1` | yes | no | T input 0, `range`, 64 bits | | `wai.world.model` | world | `5291a52bdbf2…` | `world/1` | yes | no | T input 0, `range`, 64 bits | | `wai.world.model` | world | `da046216ff94…` | `world/1` | yes | no | T input 0, `range`, 64 bits | The verdicts match Appendix C. Photo first fails `acc32` at node 6, with `convT.acc = [−25165614250, 26172239136]` (36 bits). Every `WHM1`/`WAM1`/world set fails `acc32` at its input range, which by construction is the legacy guard (O1, O2). ## Independence - `wai_ops_check.py` (Python standard library only) shares no code with wai-ops. Its session read only Part 1. It rewrites every vector file and every lowered graph, and recomputes all 21 certificates byte for byte. The two external sets are recomputed with their files supplied: in this session locally, and in CI in `wai-sota-vectors.yml` and `wai-jpegai-e2e.yml`. - It also agrees with wai-ops on every graph-vector graph and every saturating graph. - Its certifier half was written before any comparison with the Rust output. Each disagreement found then was settled against the text. - Lowered graphs and certificates are byte-identical on every leg of `wai-ops.yml`: Linux x86_64, Linux arm64, macOS arm64, and wasm32-wasip2 under wasmtime. ## Kani Every harness was run alone, one at a time, with `CARGO_BUILD_JOBS=8`. Most runs were on an idle 32-core host; a few early runs were on the dev Mac, then heavily loaded by other work. Times are Kani's verification time. Where a harness would have proved two multiplier, divider or `isqrt` circuits equal, or executed 512-bit arithmetic on symbolic operands, it does not close in bounded time. Those harnesses were restated: - The soundness harnesses check §8.3's rules restated in `i128`/`i64` (`proofs/rules.rs`). That the bounds pass computes those same rules is what the independent certifier shows, on every certificate. - Harnesses read the interpreter's own intermediates through an observer instead of recomputing them. - Some statements are split into lemmas that together are the property. A harness whose window still did not close within its cap is gated by `cfg(kani_open)`. It is kept, with its statement, and runs only on request: `RUSTFLAGS="--cfg kani_open" cargo kani --lib --exact --harness <name>`. CI compiles only harnesses that verified. **Verified (in CI):** | row | harness | window | time | |---|---|---|---| | K1 | `k01_rq_is_its_definition` | `v`, `m`, bias any `i64`; `s` ≤ 127; every rounding and bias placement | 149 s | | K2 | `k02_limb_combination_is_exact`, `…_partials_do_not_wrap`, `…_signs` | every partial product; every `u32`, `i32`, `i64` | 0.4 s, 0.05 s, 0.03 s | | K2b | `k02b_limb_epilogue` | every product `acc32` allows, `s` ≤ 63, every rounding, `post` in `i32` | 6.4 s | | K3 | `k03_rounding_is_its_definition`, `…_is_monotone` | every `i128` `p`, `s` ≤ 127 | 80 s, 7.4 s | | K4 | `k04_term_lies_in_its_interval`; `k04_partial_sums_lie_in_a` (induction: base, and one step over every value, so any number of terms) | `i8` terms; every `i32` | 26 s, 0.2 s | | K5 | `k05_chunked_i32_sums` | ≤ 8 terms, every partition, every term interval in `i32` | 27 s | | K6 | `k06_dot_lane_never_wraps` | n = 2 and 4, ≤ 8 products | 46 s | | K9 | `k09_conv_transpose_residues` (one position reads one residue; with K4's lemma) | `y` ≤ 64, `ph` ≤ 2, `sh` ≤ 3 | 0.07 s | | K11 | `k11_isqrt_is_monotone`, `k11_corner_hull_holds_products` (with K3 and the first part, gated) | `u32`; `i8` | 118 s, 106 s | | K12 | `k12_largest_returns_the_maximum` (every threshold); `k12_p_leaky_is_monotone`, `k12_p_conv_is_monotone` | X in `u32`, parameters in `u8`/`u16` | 248 s, 0.5 s, 16 s | | K13 | `k13_isqrt_u128_is_floor_sqrt`; `k13_isqrt_i512_is_floor_sqrt`; `k13_isqrt_ceil_i512_is_ceil_sqrt` | `n` < 2^32 | 104 s, 672 s, 1079 s | | K14 | `k14_leaky_bounds_sound_i8` | interval, value and `a` in `i8`, `f` ≤ 63 | 123 s | | K15 | `k15_lut16_index_is_total` | every range in `[−32767, 32767]`; both one-past ends refused | 18.5 s | | K16 | `k16_pixel_shuffle_is_a_bijection`, `k16_pixel_unshuffle_is_a_bijection` | four shapes each, planes ≤ 4×4 | 9.9 s, 13 s | | K17 | `k17_exp_neg_q16_ranges_i32` | `x` ∈ [−(2^31 − 1), 0] | 22 s | | K19 | `k19_sigmoid_ranges`; `k19_elu_ranges` (certified α) | every `i64` `v` > −2^63; every interval and α | 8.4 s, 621 s | | K23 | `k23_bucket_ceil_…`, `k23_bucket_floor_…` | ≤ 4 edges, every σ pair | 0.8 s, 3.4 s | | K26 | `k26_rans64_t2_is_total` | 32-byte streams, ≤ 3 symbols, both escapes and end rules | 876 s | | K27 | `k27_mans_bounds_are_unsigned` | every bound outside [0, 255] | 0.7 s | | K28 | `k28_mans_entry_fields` | every `next` ∈ [1, 511], every symbol | 0.1 s | | K29 | `k29_residual_step_32bit_identity_every_range`; `…_registered_ranges` | every range of the form; `U8` and `I16` | 1080 s, 87 s | | K30 | `k30_scale_index_in_range`, `k30_block_stat_in_range`, `k30_band_lookup_in_range` | as stated in each | 0.06 s, 120 s, 1.3 s | | K32 | `k32_sat_is_a_monotone_clamp`; `k32_xint_add_sub_neg_exact_at_the_saturation_edges` | every pair of 512-bit values; edges `±(2^255 − d)`, `d` < 2^16 | 7.2 s, 29 s | **Did not close; gated by `cfg(kani_open)` (cap 10 or 20 minutes, after the restatements above).** The windows are the designed ones, and where a narrower one was also tried, that one too: - **K7, K8** (`conv_transpose` gather and phase forms against the kernel, four concrete shapes, a symbolic position) and **K10** (`igdn` against the reference and the fast kernel; also one channel, one position). Covered by the `graphs/phase` vectors, the igdn equivalence tests in wai-rs and the trace tests. - **K4 and K9 at the kernel; K11's first part; K22** (`gram`, `apply`); **K18** (softmax, W ≤ 4 and W ≤ 2); **K20** (L1, ε below 2^31); **K21** (L2, ε ≤ 2^20); **K14** at `i32` and `i16`. For these, Kani proves the rules' lemmas (K4, K9, K11 above). The trace tests hold every value the interpreter forms, in every golden decode and on the extreme graphs, to its certified interval. - **K12** `p_igdn` (512-bit `isqrt` on symbolic operands), **K17** at its full window (`i64`), **K32**'s product at the edges. - **K16** `subpos` and pad/crop; **K31** (`WHG1` parse, ≤ 96 bytes); **K33** (run-time plan: conv, conv_transpose, multi-input). - **K24, K25** (strict escape and canonical end against the text's decoder, 64- and 32-byte streams), **K27** (span decodes at fixed tables, 16-byte streams), **K28**'s every-slot harness. The stage vectors cover these, with refusals and their order. **Retiring `int_transform`'s three harnesses (O14).** Not done. O14 retires them once K18 and K20 pass, and neither closed at its window. They stay, as does SPEC's text about them. **Harness defects found and fixed, not property failures:** - unwinding bounds on byte comparisons and limb loops; - an overflow in K6's own assumption; - K19's α = −2^63, which the certificate refuses; - K26's refusal of an empty range. No harness found a defect in wai-ops. ## Falsification Each fault went into a copy of the committed tree, with the harness run alone; each harness verified green on the unmodified tree at the same commit first. | fault | harness | result | |---|---|---| | `limb32::combine` drops its second carry | K2 `k02_limb_combination_is_exact` | FAILED, "the carries are exact" (2 s) | | `round` breaks a `half_even` tie toward odd | K3 `k03_rounding_is_its_definition` | FAILED, "R_half_even(p, s) as §2 defines it" (37 s) | | `rq_apply` narrows `q` to `i64` before the `post` bias | K1 `k01_rq_is_its_definition` | FAILED, "rq.y = q + post" (152 s) | For the certificate rows of Part 3.5, `wai-ops.yml` runs the two falsification sets on every leg: the overflow set must fail `acc64` at load, and the set claiming `acc32` must fail it. ## Self-review - **Bound soundness.** The photo witness runs observed: every value lies in node 6's certified intervals, and the accumulator with its bias attains `convT.acc`'s upper end. The extreme graphs (`tests/trace.rs`) and every golden decode run observed too, with no value outside its interval and no key the certificate does not record. Building them, two graphs I expected to certify were refused at load. The refusals were correct: a softmax spread of 2^63, and an elu α of −2^63. The tests now assert both refusals. - **CI reachability.** - `wai-formal-verification.yml` is now seven shards by measured time. A first job (`check_shards.py`) holds the shards to covering every compiled harness exactly once. The path filter includes `wai/wai-ops/src/**`. - Three wai-ops goldens are ignored for want of uncommitted inputs, and were run here and pass. The scale-path one now also runs in `wai-jpegai-e2e.yml`, which fetches the bundle. The other two need assets that are not redistributable. - `limb32`'s unit tests and `tests/trace.rs` run on every `wai-ops.yml` leg, wasm32-wasip2 included. The witness test runs on the three native legs. - **Goldens.** No file under `wai-rs`, nor any other conformance corpus, changes. The gate (build, lib tests, carriage, every corpus, fast kernels, byte-exact, wasm32, neural gates) is GREEN on this head. - **Public text.** The name and comparative-prose checks pass on every changed text file, and the workflow-concurrency check passes. **Checked on this head** (`8f5e70c8`, main at `4ab66d24` merged): - wai-ops tests, debug and release; `wai-verify` tests and `vectors verify`; - the gate, GREEN; - the seven shards, each run as CI runs it (`cargo kani --lib` with the shard's filters), on the idle host: | shard | harnesses | time | |---|---|---| | integer-core (wai-rs' own) | 17 | 244 s | | arith | 13 | 487 s | | isqrt512 | 2 | 1619 s | | stage | 8 | 111 s | | stage-long | 2 | 1977 s | | sound | 8 | 470 s | | plan | 6 | 361 s | `check_shards.py` reports 56 harnesses in 7 shards, with 31 gated by `cfg(kani_open)` and in none. The wasm32-wasip2 run and `wai_ops_check.py` with both external sets ran at `2419b914`. Since then, the only wai-ops changes are under `src/proofs/`, compiled only under `cfg(kani)`. The checker is unchanged. Main has since moved to `fe0282d6` (#220). That change touches only `wai-web` and its wasm workflow, none of this branch's files, and merges without conflict. The forge CI runs on this pull request. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 45 commits 2026-10-11 22:25:20 -04:00

wai-ops: load step 8, the bounds pass and the certificate (D2b) ... 1cdd4a47f0

`wai_ops::bounds` applies §8.1–§8.3 rule by rule in 512-bit arithmetic,
saturating after every primitive operation and marking the node; classes each
intermediate and producer result (§7.1), checks the parameter conditions
(§7.2), finds the first failure and the accelerator verdict, and writes the
certificate canonically (§8.5). Admissible ranges (§8.4) and the clamps they
propose are there for `--advise`.

`graph::load` now takes the implementation's profile and runs step 8: the
pass, `lut16`'s range check, an empty `check` intersection, and the profile
against the verdict. The `uncertified` switch is gone, with the generator's
own tagger: the generator and the vector recomputation take `load` and
`profiles` from the certifier, and reproduce every committed vector.

Every set the corpus lowers now has its certificate beside its lowered
graphs, and the two falsification sets of §14.3 (an int_synth set one unit
past i64, and one whose pin claims acc32 and that is one weight past it) are
generated, lowered and certified, listed in certificates/falsification.json.

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

ops-conformance: the vectors whose outcome only load step 8 decides ... 41bd170c98

sigmoid and elu on a range that reaches -2^63; an rq whose q passes 64 bits
(with y back in range where a post bias allows); l2norm at eps = 2^64 - 1; a
graph that fails acc32 by each parameter key of section 7.2 alone; lut16 at
+-32768; and in graphs/load.jsonl, a graph refused at step 8 for an empty
check intersection and for an accumulator past i64. The independent checker
recomputes every one of them from its own bounds pass.

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

wai-verify: the bounds certifier, the lowerings and the corpus tool ... 357eecdc63

`wai-verify bounds` certifies a legacy set (a file, a directory, or members
named one by one) through its capability's lowering, or WHG1 graphs on their
own, and writes the certificate; it exits 0 when the verdict meets the
profile, 1 when it fails it (with the first failure, and a node-local witness
for each failing node under --witness), 2 on malformed input, 3 when --check
finds a difference (with the first differing JSON path), 4 when the lowering
refuses, 5 on usage. --advise prints each tensor's admissible range and the
clamps that would make the graph meet the profile.

`wai-verify lower` writes a set's lowered graphs, and `wai-verify vectors`
is the D2a tool folded in: it now also recomputes every set's certificate
from the committed lowered graphs and checks that each falsification set
fails the profile it claims. The tool needs the `cli` feature, so the Kani
host keeps no dependency, and Kani runs on the library target.

wai-ops.yml builds the tool on every leg, wasip2 included, drops the
`uncertified` steps, and checks the exit status on the falsification sets and
on committed sets.

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

ops-conformance: certificates of the sets held outside the tree, by digest ... 0acf8193c1

The CI-regenerated wai.neural.int_hyper set and the jpegai/v1 bundle are not
committed, so their bounds certificates are, under each set's digest, listed
in certificates/external.json. wai-sota-vectors.yml certifies the set it
regenerates and wai-jpegai-e2e.yml the bundle it fetches, and each requires
the committed bytes (--check) and its profile: acc64 for the int_hyper set,
whose three files had the same digests in every logged run and here, and acc32
for the bundle's scale path, whose set digest is the listing digest its
set-form pin already covers. `vectors verify` checks what it can without the
sets: each such certificate is canonical, names its set and meets its profile.

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

wai-ops bounds: the contraction, elementwise and movement rules by hand ... cb4bcade44

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

wai-ops.yml: exercise --witness and --advise on every leg ... 66ebadb097

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

wai-verify: the witness names its position; its tests run in CI ... 5ad54468bb

A convolution witness records the output channel and position its input
drives to the bound. A test runs the photo set's node-6 witness through the
interpreter and finds the rounded accumulator there, the accumulator being
convT.acc's upper end; another checks the path --check reports.

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

wai_ops_check.py: the certifier half, written from the text before any comparison ... 94710b51cc

The bounds pass now keeps, per node, what section 8.5 records: the hulled
intermediates of Table 8.5-A, the saturated flag, each output's producer
result and its interval after the policy, the acc32 parameter keys of 7.2,
the flags and reasons of 9.2, k_c and mac. The verdict, the first failures
and the canonical writer follow 8.5; load step 8 and `profiles` use the same
pass. check() recomputes the certificate of every set of index.json and of
the two falsification sets, and checks external.json's certificates (in
full when --external gives a set's files). `certify` certifies one set with
the bounds tool's exit status.

Written from integer-operators.md sections 7, 8, 9.2 and 14 and the
checker's own D2a code, without reading wai-ops or any committed
certificate; this commit precedes the first comparison.

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

wai-ops CI: the external sets' certificates from both certifiers ... b52398f4f1

The jobs that hold the CI-regenerated int_hyper set and the jpegai/v1 bundle
now also run tools/wai_ops_check.py certify on the same files, with --check
against the certificate committed by digest; the checker joins both path
filters. wai-ops.yml's checker step already runs the Python certifier on
every committed set and both falsification sets; its name and the header
say so. The ops-conformance README describes the certifier half, the
--external option and the certify exit statuses.

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

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

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

wai-ops: limb32, the 32-bit fabric's acc32 product and epilogue ... 4e4bd1e2aa

A reference model of the arithmetic a 32-bit integer shading language uses
for acc32's two product intermediates (integer-operators §7.1, §7.3): the
signed 32 × 32-bit product from 16-bit halves in u32 arithmetic that wraps,
then the rounding shift on the two-word value with shifts that take their
amount mod 32, the post bias, and the narrowing to i32. Unit tests compare it
with i64 multiplication and with the interpreter's roundings, at the edges
and on samples; Kani's K2 and K2b prove it.

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

wai-ops: the seams the model checker needs, with no change in behaviour ... 66804a58f3

- interp: rq_apply and eval are crate-visible, so a harness runs one operator;
- bounds: the rule evaluation (eval, Eval) and k_c are crate-visible, so a
  harness applies one operator's rule to a symbolic interval;
- lower/whm: the three P_ℓ predicates of §13.2 are named functions, which
  x_of searches as before;
- stage/mans: a row's slots (latent_slots) and a slot's entry (latent_entry)
  are functions the table build calls, so the slots can be inspected; the
  window and the span decoders are crate-visible;
- xint: I512 equality compares the eight limbs written out. The derived
  comparison of the array is a 64-byte loop, which a model checker unwinds at
  every use. A from_limbs constructor exists under cfg(kani).

Every vector file, lowered graph and certificate is unchanged (wai-verify
vectors verify; the unit, golden, step-8 and verdict tests).

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

wai-verify: host the operator set's harnesses (work in progress) ... b1bc02ffa0

wai-verify includes wai-ops' modules at its root under cfg(kani), and the
harnesses of the test plan's K1–K33 in wai-ops/src/proofs/. check_shards.py
will hold the CI shards to covering every harness exactly once. The
formal-verification workflow's path filter now includes wai-ops' sources.
Harnesses are being run one at a time; results land with the commits that
follow.

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

wai-ops proofs: K13 on the u32 window; K26 allows the refusal of an empty range ... 74a60a2eaf

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

wai-ops proofs: the soundness harnesses check §8.3's rules restated in i128 ... a11b25dd4b

The bounds pass forms its intervals in 512-bit arithmetic with saturation,
which the model checker cannot execute on symbolic operands in bounded time:
with an I512 reference, K3 spent 1,047 s in the solver, and the 512-bit isqrt
had not left symbolic execution after 21 minutes. proofs/rules.rs restates
each rule from the text in i128, on windows where no value leaves it, and
K4, K9, K11, K14, K19, K20 and K22 check the interpreter against those. That
the bounds pass computes the same rules is what the independent certifier
shows, recomputing every certificate byte for byte.

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

wai-ops: a run can be observed, and every golden decode is held to its certificate ... 129cb11bb2

interp::run_observed reports to an Observe every value an operator forms under
one of §5's named intermediates (the keys of §8.5, Table 8.5-A), and every
producer-result element before its policy. run is run_observed with Quiet,
which compiles to nothing. gram and apply now form their epilogue through
rq_apply: their rq has no multiplier and no bias (a parse rule), so the
integers are the same.

bounds::Within is an observer that holds a run to a pass: every value must lie
in the interval the pass records for it, and every key must be one the node
records.

- Every golden decode (tests/goldens.rs) runs observed: every committed set's
  decode stays inside its certified intervals.
- tests/trace.rs: hand-built graphs at the edge of acc64, one per operator
  family, loaded through step 8 and run on inputs at their range ends and on
  samples; softmax one past its widest spread, and elu with α = −2^63, are
  refused at load.
- The photo witness, run observed, stays inside node 6's intervals, and its
  accumulator with the bias attains convT.acc's upper end.

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

wai-ops proofs: harnesses read the interpreter's own intermediates ... dbda332a09

A harness that recomputes a value the interpreter also computes, and compares,
asks the solver to show two multiplier, divider or isqrt circuits equal, which
it does not decide in bounded time: K17, which compared an i64 division by
45426 with the interpreter's i128 one, had one property unsolved after eleven
minutes (stopped; no verdict). K1, K11, K14, K17, K18, K19, K20 and K21 now read
the values the interpreter forms through an observer (proofs::Rec, by
position, in the order each operator reports them) and check those against
the definitions and the rules. exp_observed is crate-visible for K17.

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

wai-ops: the latent table build visits slots by index; K28 at width 8 ... 147d7c3c15

latent_slots wrote each column's slot ranges with loops over symbolic bounds,
which the model checker unrolls to its limit at every iteration (K28 had not
left symbolic execution after six minutes; stopped). Each column now visits the
256 slots by index and writes those its two ranges hold: the same table, with
every loop bound fixed. Every vector file, lowered graph and certificate is
unchanged (wai-verify vectors verify; tools/wai_ops_check.py).

K28's row is of width 8: a narrower row builds the table of its
zero-extension, so this covers every width up to 8.

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

CI: the formal-verification job in shards; the scale-path golden runs where its bundle is ... 670fff3afe

wai-formal-verification.yml runs the harnesses in a matrix of shards, each a
list of --harness filters, with a job that holds the shards to covering every
harness exactly once (wai-verify/check_shards.py). Its header describes the
operator set's harnesses.

wai-jpegai-e2e.yml already fetches the jpegai/v1 bundle and certifies its
scale path; it now also runs wai-ops' scale-path golden on it (ignored
elsewhere, as the bundle is not committed), with every value held to its
certified interval.

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

wai-verify: the module docs name wai-ops' harnesses and K10's use of the fast IGDN ... f89fc5ce2c

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

wai-ops interp: one function per operator, which eval dispatches to ... faa0419276

The model checker does not carry an operator's code and parameters as
constants when they sit in a graph on the heap: planning a leaky graph, it
explored subpos_merge's arm of the plan, and running a conv graph, apply's arm
of the interpreter, each with loop bounds it could not see, and none of the
graph-based harnesses left symbolic execution in twenty minutes. Each
operator's computation is now a function (k_conv, k_conv_t, …, k_apply) on its
input tensors, its parameters and its output sizes; eval extracts those from
the graph and calls it, and a harness calls it directly. The integers are the
same: every vector file, lowered graph and certificate is unchanged
(wai-verify vectors verify; tools/wai_ops_check.py), and the tests pass.

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

wai-ops: the plan's shape rules as functions; the graph harnesses call kernels ... 5e531c50ac

plan: conv_sides, conv_t_sides, shuffle_sides, unshuffle_sides,
pad_rep_sides and crop_side are the shape rules op_sizes applies, as
functions; the sizes are the same.

The harnesses that built a one-operator graph now call the operator's kernel
with sizes and parameters the checker can see:
- K4 and K9: every partial sum of the terms one output position can hold (any
  set of up to 18 taps, or of one residue class) lies in A(K, b), with the
  residue lemma for conv_transpose; and the kernel at concrete shapes, with a
  keyed observer holding every value it forms to its rule interval;
- K7 and K8: the kernel at six concrete shapes, each its own call site,
  against the gather and the phase forms at every output position;
- K10, K11, K14 and K18–K22: the kernels directly;
- K15, K16 and K33: the kernels and the plan's shape rules.

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

wai-ops proofs: K2's partial products, without a second multiplier ... 005b3cde74

The harness multiplied the halves again in u64 to compare: four multiplier
circuits to prove equal, unfinished after six minutes. Its content is that the
u32 multiplications never overflow, which the checker's overflow check on each
proves, and that the halves recompose the operands.

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

wai-ops proofs: K2 without the composition harness ... 38f37d8972

It ran the partial products a second time to compare with the function under
test, two identical multiplier circuits; its statement is mul_i32's three
lines. K2 is the combination, the overflow check on the partial products and
the signs; the unit tests compare the whole product with i64 multiplication.

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

wai-ops proofs: K5 and K6 take K_c from §6's formula ... a0c29a4f48

k_c is a 512-bit long division by a symbolic divisor, compared with an i64
division: two dividers to prove equal. K_c = ⌊(2^31 − 1)/P⌋ is §6's formula;
the independent certifier recomputes each certificate's k_c.

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

wai-ops proofs: unwinding bounds that cover each harness's loops; narrower-window variants ... 12010ebcbf

- K4's kernel harness and the K16 harnesses unwind past the lengths of their
  operands; K14, K15 and K19 have bounds; K16's merge check compares one
  element at a symbolic position instead of whole vectors; K28 builds its row as
  an array, so its column loop has a constant bound; K33's multi-input window
  is planes up to 2×2.
- K17 on i32 inputs, K20 with ε below 2^31 and K21 with ε up to 2^20 and values
  within ±2^10, beside the designed windows: where a designed window does not
  close, the narrower one is what is verified, and the report says so.
- K32: the linear operations and the product in separate harnesses.

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

wai-ops proofs: K29 on the registered ranges, beside every range of the form ... 2f8c2055d8

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

wai-ops proofs: K6 bounds the instruction count before multiplying by it ... a508e86809

The harness formed n·j for an unbounded symbolic j before assuming its range,
and the checker reported the overflow: a harness defect, not the property's.

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

wai-ops proofs: K14 on an i16 window beside its i32 one ... d1bac5250c

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

wai-ops proofs: K19's elu holds certified graphs only; K15 unwinds the 512-bit compare ... b1b860361a

K19: with α = −2^63, ⌊α·(−2^16)/2^16⌋ = 2^63 does not fit i64; the interpreter
refuses rather than wrap, and load step 8 refuses the graph (tests/trace.rs
shows it). The harness now assumes the rule's producer result fits i64, as a
certified graph's does. K15: the bound covers I512::cmp's loop over its limbs.
Both were harness defects.

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

wai-ops proofs: K30's block_stat at concrete shapes ... ba8e4be5e7

With symbolic sides and block size, the strided loops had not finished in
seventeen minutes; four shapes, each its own call site, cover full and partial
blocks in both directions and blocks of 1.

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

wai-ops proofs: K4's and K9's shape-free sums in i32 ... c37a9b0ea8

CBMC ran out of memory on K4: it formed every product of two i8 values as a
128-bit multiplication. Every value of these two harnesses is at most 18·2^14
in magnitude, so they form §8.2's term interval and A(K, b) in i32.

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

wai-ops: mans_decode checks its bounds before it builds its tables ... 0264bda1ec

Both are load checks with one refusal (model_mismatch, before any symbol), so
the order is not observable; checking the bounds first lets K27 reach the
refusal of a signed bound without building a table, which it had not done in
twenty minutes. K27's bounds harness takes only bounds outside [0, 255].
Every vector file, lowered graph and certificate is unchanged.

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

wai-ops proofs: K27 at fixed tables; K4 and K9 as two lemmas each ... 7e62f89372

K27's span harnesses ran CBMC out of memory with fully symbolic 256-entry
tables. The design's window is fixed tables: two whose entries take every nb
from 0 to 8, every base and low bits that reach both escapes, with the stream,
the bounds, the masks and the distributions symbolic.

K4's shape-free harness timed out chaining eighteen multiplication facts
through the sums. It is two lemmas, each over every value: a term lies in its
term interval; terms within their intervals have every subset sum in A(K, b).
K9's residue lemma stands alone and uses the second.

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

wai-ops proofs: K27's fixed tables are constants ... c1cccd7be8

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

wai-ops proofs: K25's bound covers the comparison of its two results ... e24a9e633f

Comparing the decoded symbols (two i64, sixteen bytes) is a memcmp loop of
seventeen iterations; the harness allowed ten, and the checker reported the
unwinding assertion. A harness defect.

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

wai-ops proofs: K11 at a concrete channel count per call site ... 5c73328920

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

wai-ops proofs: K12's conv and leaky predicates on X in u32 ... 263e7cf046

At X in u64 the leaky predicate's monotonicity, a 64 × 16-bit product, had not
closed in twenty minutes.

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

wai-ops: the parser's zero check loops to its count; harnesses the checker can finish ... 134cefc097

graph: R::zero checks its n bytes by index, n a constant at every call site;
the same check. Every vector file, lowered graph and certificate is unchanged.

Harnesses, from where each spent its time:
- the keyed observer tells keys apart by their length and two bytes, where a
  string comparison was a byte loop unrolled at every call (K4's and K9's
  kernel harnesses, K22);
- K7 and K8 compare at a symbolic output position, at four shapes;
- K4's sum lemma is proved by induction: a base, and one step over every
  value, which covers any number of terms;
- K24 and K25 compare outcomes element by element;
- K27 on 16-byte streams;
- K18 also on rows of up to 2 values; K12's igdn predicate on X in u8.

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

wai-ops proofs: K11 as its first part and three lemmas; K10 also at one channel ... 25de089ada

K11 timed out with three isqrt circuits and their products in one formula. Its
statement splits: the values up to the final norm lie in the rule's intervals,
the final norm in Nf; isqrt is non-decreasing; the corner hull holds every
product of two intervals' values; and R_floor is non-decreasing (K3). Together
they are the rule's soundness.

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

wai-ops proofs: K11's corner lemma on i8 values; K16's subpos at one shape ... 07a180e518

Both timed out at twenty minutes on the wider windows.

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

Merge main (at 3af82118, with #215–#217) into wai/d2b-bounds ... 2419b91403

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

wai-ops proofs: K14's rule in i64, and an i8 window ... 6bb3f20645

The rule's products were formed as 128-bit multiplications; every product of
two i32 values fits i64. At i16 the harness had not closed in ten minutes.

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

wai-ops proofs: harnesses that did not close are gated; CI in seven shards by measured time ... 9006e7aea4

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]>

Merge main (at 4ab66d24, with #199, #201 and #219) into wai/d2b-bounds ... 8f5e70c800

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

dcharlot referenced this pull request 2026-10-11 22:59:51 -04:00

wai-vector: the default stroke set and the test repertoire, as WSF1 sources expanded by Annex A, and the text vectors (D7-5) #224

dcharlot added 1 commit 2026-10-12 09:50:33 -04:00

wai-ops proofs: the rans64 totality proof runs where its memory fits ... 5e6792fd3b

k26 peaks at about 28 GiB of resident memory (688 s, measured); the linux runner has
15 GiB shared by two jobs and CBMC ran out of memory there. It gets a shard of its own
on the macos runner. The Kani install step no longer rewrites a host's live install,
and check_shards reads a matrix line that names its runner and refuses one it cannot
read.

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

dcharlot added 1 commit 2026-10-12 15:25:39 -04:00

Merge main into wai/d2b-bounds ... 829281c745

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

dcharlot added 1 commit 2026-10-12 19:58:42 -04:00

Merge main into wai/d2b-bounds ... a145f5c29a

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

dcharlot merged commit 0d82816fbe into main 2026-10-13 00:53:47 -04:00

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

Merge pull request 'wai-ops: the bounds pass, certificates from two certifiers, and the operator set's Kani harnesses (D2b)' (#221) from wai/d2b-bounds into main

dcharlot referenced this pull request from a commit 2026-10-14 02:13:13 -04:00

Merge origin/main (at 1fa13396, with D2b #221, #227 and #228) into wai/d2c-decoders-on-ops

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!221

No description provided.