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

2026-10-12

Transaction Science

Merge main into wai/d2b-bounds ...

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

a145f5c29a

• View at this point in history

2026-10-12 15:53:48 -04:00

Transaction Science

Merge main into wai/d2b-bounds ...

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

829281c745

• View at this point in history

2026-10-12 09:51:56 -04:00

Transaction Science

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

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

5e6792fd3b

• View at this point in history

2026-10-12 09:50:31 -04:00

2026-10-11

Transaction Science

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

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

8f5e70c800

• View at this point in history

2026-10-11 17:20:05 -04:00

Transaction Science

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

Harnesses whose windows the checker did not finish within their cap (ten or
twenty minutes on an idle 32-core host) are gated by cfg(kani_open): kept in
the source with their statements, compiled and run only on request
(RUSTFLAGS="--cfg kani_open" cargo kani --lib --exact --harness <name>), so
that every harness CI compiles verifies. check_shards.py counts them apart.
wai-verify declares the cfg.

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

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

9006e7aea4

• View at this point in history

2026-10-11 17:16:54 -04:00

Transaction Science

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

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

6bb3f20645

• View at this point in history

2026-10-11 11:05:10 -04:00

Transaction Science

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

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

2419b91403

• View at this point in history

2026-10-11 10:42:52 -04:00

Transaction Science

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

Both timed out at twenty minutes on the wider windows.

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

07a180e518

• View at this point in history

2026-10-11 08:59:58 -04:00

Transaction Science

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

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

25de089ada

• View at this point in history

2026-10-11 08:38:46 -04:00

Transaction Science

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

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

134cefc097

• View at this point in history

2026-10-11 08:37:32 -04:00

Transaction Science

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

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

263e7cf046

• View at this point in history

2026-10-11 06:14:05 -04:00

Transaction Science

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

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

5c73328920

• View at this point in history

2026-10-11 06:03:25 -04:00

Transaction Science

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

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

e24a9e633f

• View at this point in history

2026-10-11 05:31:46 -04:00

Transaction Science

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

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

c1cccd7be8

• View at this point in history

2026-10-11 05:20:51 -04:00

Transaction Science

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

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

7e62f89372

• View at this point in history

2026-10-11 05:20:20 -04:00

Transaction Science

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

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

0264bda1ec

• View at this point in history

2026-10-11 05:08:30 -04:00

Transaction Science

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

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

c37a9b0ea8

• View at this point in history

2026-10-11 04:57:18 -04:00

Transaction Science

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

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

ba8e4be5e7

• View at this point in history

2026-10-11 04:36:14 -04:00

Transaction Science

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

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

b1b860361a

• View at this point in history

2026-10-11 04:35:53 -04:00

Transaction Science

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

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

d1bac5250c

• View at this point in history

2026-10-11 04:23:49 -04:00

Transaction Science

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

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

a508e86809

• View at this point in history

2026-10-11 04:23:40 -04:00

Transaction Science

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

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

2f8c2055d8

• View at this point in history

2026-10-11 04:12:52 -04:00

Transaction Science

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

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

12010ebcbf

• View at this point in history

2026-10-11 04:12:41 -04:00

Transaction Science

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

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

a0c29a4f48

• View at this point in history

2026-10-11 03:59:50 -04:00

Transaction Science

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

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

38f37d8972

• View at this point in history

2026-10-11 03:59:30 -04:00

Transaction Science

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

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

005b3cde74

• View at this point in history

2026-10-11 03:38:12 -04:00

Transaction Science

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

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

5e531c50ac

• View at this point in history

2026-10-11 03:37:44 -04:00

Transaction Science

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

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

faa0419276

• View at this point in history

2026-10-11 03:32:46 -04:00

Transaction Science

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

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

f89fc5ce2c

• View at this point in history

2026-10-11 03:28:16 -04:00

2026-10-10

Transaction Science

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

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

670fff3afe

• View at this point in history

2026-10-10 23:27:46 -04:00

Transaction Science

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

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

147d7c3c15

• View at this point in history

2026-10-10 23:25:51 -04:00

Transaction Science

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

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

dbda332a09

• View at this point in history

2026-10-10 23:23:42 -04:00

Transaction Science

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

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

129cb11bb2

• View at this point in history

2026-10-10 23:16:55 -04:00

Transaction Science

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

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

a11b25dd4b

• View at this point in history

2026-10-10 23:05:34 -04:00

Transaction Science

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

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

74a60a2eaf

• View at this point in history

2026-10-10 22:46:05 -04:00

Transaction Science

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

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

b1bc02ffa0

• View at this point in history

2026-10-10 22:23:38 -04:00

Transaction Science

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

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

66804a58f3

• View at this point in history

2026-10-10 18:19:13 -04:00

Transaction Science

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

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

4e4bd1e2aa

• View at this point in history

2026-10-10 18:19:13 -04:00

Transaction Science

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

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

93e15d74c8

• View at this point in history

2026-10-10 17:19:19 -04:00

Transaction Science

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

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

b52398f4f1

• View at this point in history

2026-10-10 10:26:38 -04:00

Transaction Science

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

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

94710b51cc

• View at this point in history

2026-10-10 10:10:05 -04:00

Transaction Science

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

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

5ad54468bb

• View at this point in history

2026-10-10 09:56:35 -04:00

Transaction Science

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

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

66ebadb097

• View at this point in history

2026-10-10 09:50:57 -04:00

Transaction Science

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

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

cb4bcade44

• View at this point in history

2026-10-10 09:50:09 -04:00

Transaction Science

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

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

0acf8193c1

• View at this point in history

2026-10-10 09:42:31 -04:00

Transaction Science

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

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

357eecdc63

• View at this point in history

2026-10-10 09:38:32 -04:00

Transaction Science

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

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

41bd170c98

• View at this point in history

2026-10-10 09:29:40 -04:00

Transaction Science

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

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

1cdd4a47f0

• View at this point in history

2026-10-10 09:26:27 -04:00