`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