1cdd4a47f0
`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]>
61 lines
2.7 KiB
Rust
61 lines
2.7 KiB
Rust
//! Load step 8 (§10.5): every graph loads under a profile, and loads only when its
|
|
//! verdict meets that profile (§8.6). The interpreter takes only a `Loaded` graph,
|
|
//! which only `graph::load` makes, so a lowered set's graphs cannot be run around
|
|
//! the verdict. (That `run` rejects a `Graph` at compile time is the `compile_fail`
|
|
//! example on `Loaded`.)
|
|
|
|
use std::path::PathBuf;
|
|
|
|
use wai_ops::code::{Code, Refusal, Site};
|
|
use wai_ops::{Profile, graph, lower};
|
|
|
|
fn read(p: &str) -> Vec<u8> {
|
|
let path = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("..").join(p);
|
|
std::fs::read(&path).unwrap_or_else(|e| panic!("{p}: {e}"))
|
|
}
|
|
|
|
fn step8() -> Refusal {
|
|
Refusal::new(Code::ModelMismatch, Site::Load(8))
|
|
}
|
|
|
|
/// Every lowered graph of the committed int_synth sets loads under `acc64`. The
|
|
/// facade, gradient and bloom sets also load under `acc32`; photo does not, and its
|
|
/// `acc32` load is refused at step 8.
|
|
#[test]
|
|
fn a_lowered_set_loads_only_under_a_profile_its_verdict_meets() {
|
|
for (name, acc32) in [("gradient", true), ("bloom", true), ("facade", true), ("photo", false)] {
|
|
let set = lower::int_synth(&read(&format!("neural-conformance/vectors/{name}/int_synth.json"))).unwrap();
|
|
for (role, g) in &set.roles {
|
|
let b = g.to_bytes();
|
|
let l = graph::load(&b, Profile::Acc64).unwrap_or_else(|e| panic!("{name}/{role}: {e:?}"));
|
|
assert_eq!(l.meets(Profile::Acc32), acc32, "{name}/{role}");
|
|
match graph::load(&b, Profile::Acc32) {
|
|
Ok(_) => assert!(acc32, "{name}/{role} loads under acc32"),
|
|
Err(e) => {
|
|
assert!(!acc32, "{name}/{role} is refused under acc32");
|
|
assert_eq!(e, step8(), "{name}/{role}");
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/// The overflow set of §14.3, whose accumulator passes i64 by one unit, is refused at
|
|
/// step 8 under both profiles, and so is the same set one unit inside.
|
|
#[test]
|
|
fn the_overflow_set_is_refused_at_step_8() {
|
|
let set = lower::int_synth(&read("ops-conformance/sets/overflow_acc64/int_synth.json")).unwrap();
|
|
let b = set.get("synth").unwrap().to_bytes();
|
|
for p in Profile::ALL {
|
|
assert_eq!(graph::load(&b, p).unwrap_err(), step8(), "{p:?}");
|
|
}
|
|
}
|
|
|
|
/// The set of §14.3 whose pin claims `acc32` meets `acc64` and fails `acc32`.
|
|
#[test]
|
|
fn the_acc32_claim_set_loads_under_acc64_only() {
|
|
let set = lower::int_synth(&read("ops-conformance/sets/claim_acc32/int_synth.json")).unwrap();
|
|
let b = set.get("synth").unwrap().to_bytes();
|
|
assert!(!graph::load(&b, Profile::Acc64).unwrap().meets(Profile::Acc32));
|
|
assert_eq!(graph::load(&b, Profile::Acc32).unwrap_err(), step8());
|
|
}
|