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]>
157 lines
9.3 KiB
Markdown
157 lines
9.3 KiB
Markdown
# ops-conformance — the integer operator set
|
||
|
||
Vectors for `wai-ops/1`, the integer operator set
|
||
([`extensions/integer-operators.md`](../extensions/integer-operators.md)): its graph
|
||
operators (§5), its stage operators (§5E), the `WHG1` graph form (§10), and the
|
||
canonical lowerings of the registered integer network forms (§13).
|
||
|
||
**Provenance.** Generated here by `wai-verify vectors gen` from fixed SplitMix64
|
||
sequences: every graph, parameter, input and stream under `vectors/`, `stage/`,
|
||
`graphs/` and `sets/` is generated integers, with no media. The lowered graphs under
|
||
`certificates/` are those of the sets this corpus generates and of the parameter sets
|
||
other corpora commit, which keep their own provenance (`certificates/index.json`
|
||
names each one's corpus).
|
||
|
||
**Equivalence.** An operator implementation of a profile (§7) conforms when it
|
||
reproduces every vector tagged with that profile, refusals included: the same `load`
|
||
outcome, and for every decode the same output integers or the same refusal code. A
|
||
lowering conforms when it writes every lowered graph byte for byte.
|
||
|
||
## Layout
|
||
|
||
- `vectors/<operator>.jsonl` — graph vectors whose graph has one operator (§14.1).
|
||
- `stage/<operator>.jsonl` — stage-operator vectors (§14.1).
|
||
- `graphs/<name>.jsonl` — graph vectors whose graph has several operators (§14.2):
|
||
- `phase` — a transposed convolution and the same computed as phase convolutions,
|
||
interleaved by `pixel_shuffle` and cropped (§9.3), as the graph's two outputs;
|
||
- `state` — state inputs carried across decodes (§10.3), a refused decode among
|
||
them;
|
||
- `load` — a graph refused at each load check of §10.5, steps 1–7, and a `crop`
|
||
planned at load (§5.10);
|
||
- `run` — a decode refused at each step of §4's run, and the order between them
|
||
and within step 3 (the caps, then the shape rule, then `max_elems`);
|
||
- `lower_<form>` — each lowering of §13 on a small set from `sets/`.
|
||
- `sets/<name>/` — the small parameter sets the `lower_*` vectors lower, one per
|
||
lowering, in their registered forms.
|
||
- `certificates/<capability>/<set digest>.json` — each set's bounds certificate
|
||
(§8.5, §14.3), and beside it `certificates/<capability>/<set digest>/<role>.whg1`,
|
||
each lowered graph.
|
||
- `certificates/index.json` — every set lowered here: its capability, its lowering,
|
||
its members (the name in the set and the file, relative to `wai/`, that holds it),
|
||
its digest, and the path of each lowered graph, in §13.0's role order.
|
||
- `certificates/falsification.json` — the two sets of §14.3 that a certifier must
|
||
reject, in the same form, each with `claim`, the profile it is checked against:
|
||
`overflow_acc64`, whose accumulator passes i64 by one unit, and `claim_acc32`,
|
||
whose pin claims `acc32` and whose accumulator passes i32 by one unit, one weight
|
||
past a set that meets it. Their members are under `sets/`. A sink refuses both
|
||
under the profile they are checked against (§8.6).
|
||
- `certificates/external.json` — the sets whose certificates are here although the
|
||
sets are not: the CI-regenerated `wai.neural.int_hyper` set and the `jpegai/v1`
|
||
bundle of the models root. Each entry gives the set's members (the name in the set,
|
||
then the file the job that holds it reads), its digest, the profile its verdict
|
||
meets, and that job's workflow, which certifies the set and requires these bytes.
|
||
Here, `vectors verify` and the independent checker check only what they can
|
||
without the set: that each such certificate is canonical, names its set, and meets
|
||
its profile. The job that holds the set certifies it with both certifiers.
|
||
|
||
Files are compared as bytes; `.gitattributes` turns off line-ending conversion.
|
||
|
||
This corpus has no `sha256.json` sidecar (SPEC §7 *Digests*). Every vector states its
|
||
output integers in full, or its refusal code, and never a digest of them. The only
|
||
digest in `certificates/` is each set's SHA-256, which identifies a parameter set. The
|
||
output digests that a capability reproduces through its lowering (integer-operators §14.4)
|
||
stay in that capability's own corpus.
|
||
|
||
## The vector files
|
||
|
||
Every file follows integer-operators §14.1, which is normative for every field: the
|
||
graph vector and its decodes, the stage vector with its `modes`, each operator's
|
||
`in` and `expect` (the predictors' layouts included), and the refusal index `at`.
|
||
In short:
|
||
|
||
- Every file is JSON Lines: one canonical JSON value per line (§8.5's rules), each
|
||
line ending with one line feed.
|
||
- A graph vector's decodes list the graph's **data** inputs only; the decodes of one
|
||
vector are one sequence, and a refused decode changes no state (§10.3).
|
||
- `load` is the outcome of load steps 1–8 (§10.5), under every profile the vector
|
||
lists. A vector whose load is refused, at any step, has no decodes and lists both
|
||
profiles; one that loads lists exactly the profiles its verdict meets.
|
||
- `at` is −1 for a refusal before any symbol or element, the symbol's index for
|
||
`rans64_decode` (the number of symbols for a refusal after the last one), and, for
|
||
`mans_decode`, the position whose step refuses, or, for a flush that belongs to no
|
||
single position, the last position whose `in` step ran.
|
||
- A vector of `graphs/lower_<form>.jsonl` has the id `<file>/<set>/<role>/…`: its
|
||
graph is that role of the set `sets/<set>/` as lowered.
|
||
|
||
## The vectors load step 8 decides
|
||
|
||
Whether a graph loads, and under which profiles, is the verdict of its bounds pass
|
||
(§8). Besides every other vector's `profiles`, these depend on it alone (§14.1 item
|
||
6), each in its operator's file, with an id that names the class:
|
||
|
||
- `sigmoid/step8/…`, `elu/step8/…`: an input range that reaches `−2^63`, refused at
|
||
load (`exp.negx` passes i64); the ranges that stop at `−(2^63 − 1)` decode;
|
||
- `<op>/step8_q/…`: an `rq` whose `q` passes 64 bits, refused under `acc64`; with a
|
||
`post` bias (`conv`, `conv_transpose`, `rescale`) `y` fits while `q` does not, and
|
||
beside each, the same graph one unit inside, which decodes;
|
||
- `l2norm/eps/…` and `layernorm_c`'s cases with `ε = 2^64 − 1`, which load under
|
||
`acc64` only;
|
||
- `<op>/acc32_param/…`: a graph that fails `acc32` by one parameter condition of
|
||
§7.2 alone (`rq.mult`, `rq.shift`, `rq.post_bias`, `weights`, `chscale.m`,
|
||
`chscale.s`, `igdn.gamma`, `igdn.shift`, `leaky.a`), every interval within i32;
|
||
- `lut16/step8/…`: an input range that reaches `±32768` (§5.6);
|
||
- `graphs/load.jsonl`, `load/step8/…`: a `check` range its producer cannot meet, one
|
||
that its producer meets at one value (loads, under `acc64` only), and an
|
||
accumulator past i64.
|
||
|
||
## The lowered sets
|
||
|
||
`certificates/index.json` lists every set. A set of one file is identified by its
|
||
file's SHA-256, and a set of several files by the SHA-256 of its `wai.prior.set`
|
||
listing over the member names the index gives (SPEC §3.1). `wai.world.model` has no
|
||
registered set yet: its two networks are named `T.whm` and `g_s.whm` here, and its
|
||
lowering's latent channel count, which the initial latent fixes, is the entry's `c`.
|
||
|
||
## Generation and verification
|
||
|
||
cd wai/wai-verify
|
||
cargo run --release --features cli --bin wai-verify -- vectors gen ..
|
||
|
||
writes every file here but this README, `.gitattributes`, and `external.json` with
|
||
the certificates it lists.
|
||
|
||
cargo run --release --features cli --bin wai-verify -- vectors verify ..
|
||
|
||
recomputes every vector file from its inputs, re-lowers every set and recomputes its
|
||
certificate from the committed lowered graphs, checks that each falsification set
|
||
fails the profile it claims, and regenerates the corpus, and requires every byte to
|
||
equal the committed one. The same check runs built for `wasm32-wasip2` under a WASI
|
||
runtime, and, for the vector files, `wai-ops/node/verify.mjs` runs the recomputation
|
||
as a `wasm32-unknown-unknown` module under a browser's engine.
|
||
|
||
wai-verify bounds <set> --capability <name> [--profile acc32|acc64] [--check <cert>]
|
||
|
||
certifies one set (or `WHG1` graphs on their own), and exits 0 when its verdict meets
|
||
the profile, 1 when it does not, and 3 when `--check` finds a difference.
|
||
|
||
python3 -I tools/wai_ops_check.py ops-conformance
|
||
|
||
is the independent checker: Python standard library only, sharing no code with
|
||
`wai-ops`, and held to the extension's text: where the two disagree, the text
|
||
decides, and the disagreement is a bug in one of them. It rewrites every vector file
|
||
from its inputs, `load` (steps 1–8) and `profiles` from its own bounds pass and
|
||
verdict (§8.1–§8.5) included; re-lowers every set and requires each lowered graph,
|
||
and that each loads; and requires each lowering vector's graph to be the role its id
|
||
names. It is also a second certifier (§1): from each set's lowered graphs it writes
|
||
the set's certificate (§8.5) and requires the committed bytes, for every set of
|
||
`index.json` and both falsification sets, each of which must fail the profile it
|
||
claims. Every byte must equal the committed one.
|
||
|
||
python3 -I tools/wai_ops_check.py ops-conformance --external <name>=<dir>
|
||
python3 -I tools/wai_ops_check.py certify --capability <name> --lowering <id> \
|
||
--member <name>=<path>... [--profile acc32|acc64] [--out <cert>] [--check <cert>]
|
||
|
||
certify an external set from the directory that holds its files, and one set (or
|
||
`WHG1` graphs on their own, with `--whg1 <role>=<path>`), with the exit statuses of
|
||
`wai-verify bounds`: 0, 1, 3 as above; 2 when a graph is malformed or refused at load;
|
||
4 when the lowering refuses the set; 5 for usage.
|