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]>
32 lines
1.1 KiB
TOML
32 lines
1.1 KiB
TOML
# The reference implementation of `wai-ops/1`, the integer operator set
|
|
# (`extensions/integer-operators.md`): the `WHG1` graph form, the load and run-time
|
|
# plans, the interpreter, the stage operators, the canonical lowerings of the
|
|
# registered integer network forms, the bounds pass with its certificate (load step
|
|
# 8), and the conformance vectors of `../ops-conformance/`.
|
|
#
|
|
# `no_std` with `alloc`, and no dependencies, so that a model checker can include
|
|
# its sources by `#[path]` the way `wai-verify` includes the other integer sources.
|
|
[package]
|
|
name = "wai-ops"
|
|
version = "0.1.0"
|
|
edition = "2024"
|
|
rust-version = "1.97"
|
|
license = "Apache-2.0"
|
|
publish = false
|
|
description = "WAI integer operator set wai-ops/1: WHG1 graphs, plans, interpreter, stage operators, lowerings, bounds certificates and conformance vectors"
|
|
|
|
[lib]
|
|
name = "wai_ops"
|
|
path = "src/lib.rs"
|
|
|
|
# The tool that drives this library (the certifier, the lowerings and the corpus) is
|
|
# `wai-verify`, a binary of `../wai-verify` behind its `cli` feature.
|
|
|
|
[lints.rust]
|
|
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] }
|
|
|
|
[dependencies]
|
|
# none
|
|
|
|
[profile.release]
|
|
debug = false
|