`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