From 59a988e0d8d9e79c1a752d24ae36063958b42436 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 08:45:02 +0200 Subject: [PATCH 1/2] test(aprender-simulate): cover validate_verification_tests (EDD-07) + contract Co-Authored-By: Claude Sonnet 5.5 --- README.md | 4 +- contracts/contracts.nt | 5 ++ .../simulate-edd-verification-tests-v1.yaml | 38 ++++++++++++++ ...5f0be2f90923120a3027c176ad56723d0d850.json | 4 +- .../aprender-simulate/src/edd/validation.rs | 50 +++++++++++++++++++ 5 files changed, 97 insertions(+), 4 deletions(-) create mode 100644 contracts/simulate-edd-verification-tests-v1.yaml diff --git a/README.md b/README.md index 027a6b2a7d..191f91b659 100644 --- a/README.md +++ b/README.md @@ -114,7 +114,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **81** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1984** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1985** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **113** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` also lists `help` itself, and `grep -c '^ - name:'` gives 119 — other same-indent `name:` keys exist in the file) | | Book CLI chapters | **114** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **73** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -403,7 +403,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1984 contracts across inference, training, quantization, attention, FFN, +The tree carries 1985 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/contracts.nt b/contracts/contracts.nt index f0d8c3a042..646ee9e8da 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -13721,6 +13721,11 @@ "simd-scalar-parity-v1"^^ . "simd-scalar-parity"^^ . "1.0.0"^^ . + . + . + "contracts/simulate-edd-verification-tests-v1.yaml"^^ . + "simulate-edd-verification-tests-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/simulate-edd-verification-tests-v1.yaml b/contracts/simulate-edd-verification-tests-v1.yaml new file mode 100644 index 0000000000..a264bc7cf7 --- /dev/null +++ b/contracts/simulate-edd-verification-tests-v1.yaml @@ -0,0 +1,38 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "EDD-07 — EddValidator::validate_verification_tests reports each failing EMC verification test as a critical EDD-07 violation, passes silently when all hold, and records failures in the validator." + kind: pattern + references: + - "crates/aprender-simulate/src/edd/validation.rs — validate_verification_tests and its tests" + - "docs/findings/aprender-w5032.jsonl — coverage-gaps ranking that selected this function" + +equations: + edd07_reports_exactly_the_failing_tests: + formula: "errors == { t in emc.tests : |eval(t.inputs) - t.expected| > t.tolerance }, each code EDD-07 and severity Critical; validator.violations grows by |errors|" + domain: "an EquationModelCard with >= 1 verification test and an evaluator closure" + codomain: "Result<(), Vec>" + invariants: + - "A passing run leaves the validator's violations untouched" + - "A failing run appends to, never replaces, earlier violations" + - "The violation context carries the FAIL line with expected, actual and tolerance" + +proof_obligations: + - id: SEV-INV-001 + type: invariant + property: "Only failing tests are reported, as EDD-07 Critical with FAIL context" + formal: "∀ t ∈ {test_validate_verification_tests_failure_is_edd07_critical_with_context}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + - id: SEV-INV-002 + type: invariant + property: "Failures accumulate in the validator across runs" + formal: "∀ t ∈ {test_validate_verification_tests_failures_accumulate_in_validator}: exit(t) = 0" + applies_to: edd07_reports_exactly_the_failing_tests + +falsification_tests: + - id: FALSIFY-SEV-001 + rule: "failures not recorded" + prediction: "deleting the self.violations.extend call turns the accumulate test RED" + test: "cargo test -p aprender-simulate --lib test_validate_verification_tests_failures_accumulate_in_validator" + if_fails: "a failed verification leaves no trace in the validator" diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 6bb276cb32..d45d145b96 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "7597b4ad189f534dd58cda55c9b1fe29e6339ddb77fd5f40969b4a028eed8f88", + "census_id_set_sha256": "baac627e81511256895c61f340bd3c03eda199ac25c1e6fa5e1f9c380dea159f", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "461bf9ef1921a8fbea4bc338f21b566ec342a95e", + "reasoner_git_sha": "2ab028214900e252b59d1e5c5c5fcd15fe3c43a6", "checkable_n": 87, "result": { "kind": "model", diff --git a/crates/aprender-simulate/src/edd/validation.rs b/crates/aprender-simulate/src/edd/validation.rs index b07d563e75..75ccb103d5 100644 --- a/crates/aprender-simulate/src/edd/validation.rs +++ b/crates/aprender-simulate/src/edd/validation.rs @@ -1559,4 +1559,54 @@ mod tests { let result_loose = richardson_extrapolation(&values, 2.0, 2.5, 1.0); assert!(result_loose.order_matches); } + + fn emc_with_tests(tests: &[(&str, f64, f64)]) -> EquationModelCard { + let mut b = EmcBuilder::new() + .name("Test") + .equation("x = y") + .citation(Citation::new(&["Test"], "Test", 2024)); + for (d, e, t) in tests { + b = b.add_verification_test(*d, *e, *t); + } + b.build().ok().unwrap() + } + + #[test] + fn test_validate_verification_tests_all_pass_records_nothing() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("a", 1.0, 0.1), ("b", 1.0, 0.5)]); + assert!(v.validate_verification_tests(&emc, |_| 1.05).is_ok()); + assert!(v.violations().is_empty()); + } + + #[test] + fn test_validate_verification_tests_failure_is_edd07_critical_with_context() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("good", 1.0, 0.1), ("bad", 5.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 1.0).err().unwrap(); + assert_eq!(errs.len(), 1, "only the failing test is reported"); + assert_eq!(errs[0].code, "EDD-07"); + assert_eq!(errs[0].severity, ViolationSeverity::Critical); + assert!(errs[0].message.contains("Verification test failed: bad")); + assert!(errs[0] + .context + .as_deref() + .unwrap_or("") + .contains("FAIL: bad")); + } + + #[test] + fn test_validate_verification_tests_failures_accumulate_in_validator() { + let mut v = EddValidator::new(); + let emc = emc_with_tests(&[("x", 9.0, 0.1), ("y", 8.0, 0.1)]); + let errs = v.validate_verification_tests(&emc, |_| 0.0).err().unwrap(); + assert_eq!(errs.len(), 2); + assert_eq!(v.violations().len(), 2); + let _ = v.validate_verification_tests(&emc, |_| 0.0); + assert_eq!( + v.violations().len(), + 4, + "a second run appends, not replaces" + ); + } } From c93bd4a7ededc7cb8fdaf9db3192f244a8d99b2c Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 20:33:17 +0200 Subject: [PATCH 2/2] chore(contracts): regenerate README count and pv-sat witness after merging main Co-Authored-By: Claude Sonnet 5.5 --- README.md | 4 ++-- ...2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 191f91b659..f14aaebaff 100644 --- a/README.md +++ b/README.md @@ -114,7 +114,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **81** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1985** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1986** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **113** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` also lists `help` itself, and `grep -c '^ - name:'` gives 119 — other same-indent `name:` keys exist in the file) | | Book CLI chapters | **114** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **73** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -403,7 +403,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1985 contracts across inference, training, quantization, attention, FFN, +The tree carries 1986 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index a5088c39a3..ab7a788cda 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,5 +1,5 @@ { - "census_id_set_sha256": "063d371c514532fccc38497ed2f0d85711be3c35061de05df561446f16e93d99", + "census_id_set_sha256": "2714efdf4e5b92782260d970b5de68f7c57a417bd123e18cab2c662b8a311cb4", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", "checkable_n": 87, "result": {