From 7bc03cf7833ca93b76eb4beaf8d43dbb6ddbc6ab Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 19:27:34 +0200 Subject: [PATCH 01/12] test(apr-cli): cover civil_from_days and now_utc_iso8601 in corpus-ingest, falsifier 006 (Refs #5577) Co-Authored-By: Claude Sonnet 5.5 (cherry picked from commit 8626c7c65b15781aaf4f034e52245e9fc6ccda79) --- ...in-apr-cli--aprender-corpus-ingest-v1.yaml | 6 +++++ crates/apr-cli/src/bin/apr-corpus-ingest.rs | 25 +++++++++++++++++++ docs/findings/aprender-w5404.jsonl | 1 + 3 files changed, 32 insertions(+) create mode 100644 docs/findings/aprender-w5404.jsonl diff --git a/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml b/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml index b1be05c385..9806261dd8 100644 --- a/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml +++ b/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml @@ -114,3 +114,9 @@ falsification_tests: if_fails: "GREEN 2026-09-26: 2 rows, set-equal to the 2 commands" mutation: 'delete every aprender-corpus-ingest row; must turn RED naming aprender-corpus-ingest' + - id: FALSIFY-BIN-APR_CORPUS_INGEST-006 + rule: 'civil_from_days and now_utc_iso8601 produce correct civil dates and a fixed-shape stamp' + prediction: 'epoch is 1970-01-01, 2000-02-29 exists, 1900 has no Feb 29, day -1 is 1969-12-31, and the stamp is 20 bytes ending in Z' + test: 'cargo test -p apr-cli --bin aprender-corpus-ingest -- civil_from_days now_utc' + if_fails: 'ingest manifests carry a wrong date or a malformed timestamp' + mutation: 'change the 719_468 epoch offset by one; must turn RED' diff --git a/crates/apr-cli/src/bin/apr-corpus-ingest.rs b/crates/apr-cli/src/bin/apr-corpus-ingest.rs index 5299ecdd29..c729010a08 100644 --- a/crates/apr-cli/src/bin/apr-corpus-ingest.rs +++ b/crates/apr-cli/src/bin/apr-corpus-ingest.rs @@ -524,4 +524,29 @@ mod tests { } assert_eq!(report.present_top_keys.len(), REQUIRED_TOP_KEYS.len()); } + + #[test] + fn civil_from_days_epoch_and_leap_boundaries() { + assert_eq!(civil_from_days(0), (1970, 1, 1)); + assert_eq!(civil_from_days(59), (1970, 3, 1)); + // 2000-02-29 (divisible-by-400 leap day) is day 11_016. + assert_eq!(civil_from_days(11_016), (2000, 2, 29)); + assert_eq!(civil_from_days(11_017), (2000, 3, 1)); + // 1900 is not a leap year; the day before the epoch is 1969-12-31. + assert_eq!(civil_from_days(-1), (1969, 12, 31)); + assert_eq!(civil_from_days(-25_508), (1900, 3, 1)); + assert_eq!(civil_from_days(-25_509), (1900, 2, 28)); + } + + #[test] + fn now_utc_iso8601_has_fixed_shape() { + let s = now_utc_iso8601(); + let b = s.as_bytes(); + assert_eq!(b.len(), 20, "got {s}"); + assert_eq!( + (b[4], b[7], b[10], b[13], b[16], b[19]), + (b'-', b'-', b'T', b':', b':', b'Z') + ); + assert!(s.starts_with("20"), "year after 2000, got {s}"); + } } diff --git a/docs/findings/aprender-w5404.jsonl b/docs/findings/aprender-w5404.jsonl new file mode 100644 index 0000000000..e0a39ef406 --- /dev/null +++ b/docs/findings/aprender-w5404.jsonl @@ -0,0 +1 @@ +{"id":"5577-apr-cli-cov","utc":"2026-10-18T17:27Z","by":"aprender-w5404","base":"0ecee41d04","claim":"civil_from_days and now_utc_iso8601 in crates/apr-cli/src/bin/apr-corpus-ingest.rs had no test; now covered by two unit tests plus FALSIFY-BIN-APR_CORPUS_INGEST-006","method":"pmat query --coverage-gaps has no coverage file here, so ranking is arbitrary; picked a pure uncovered fn reachable from the tests mod"} From a81754f69ff189ed5c2f5345fd9dda491306b698 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 19:18:27 +0200 Subject: [PATCH 02/12] test(aprender-contracts): cover build_diff_info + pv-query-diff-info-v1 contract (Refs #5580) Co-Authored-By: Claude Sonnet 5.5 (cherry picked from commit 7a55cca33eafe8f752e7b19770fa150b51eb852e) --- contracts/pv-query-diff-info-v1.yaml | 43 +++++++++++++++++++ .../src/query/query_enrich_tests.rs | 41 ++++++++++++++++++ 2 files changed, 84 insertions(+) create mode 100644 contracts/pv-query-diff-info-v1.yaml diff --git a/contracts/pv-query-diff-info-v1.yaml b/contracts/pv-query-diff-info-v1.yaml new file mode 100644 index 0000000000..0b5d815a70 --- /dev/null +++ b/contracts/pv-query-diff-info-v1.yaml @@ -0,0 +1,43 @@ +metadata: + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + description: "pv query diff info — build_diff_info reports the last commit that touched a contract file as a full sha plus a date-only string, and reports nothing for a path git has no history for." + kind: pattern + references: + - "aprender#5580 — coverage-gap ticket for aprender-contracts (build_diff_info was at 0.0%)" + - "crates/aprender-contracts/src/query/query_enrich.rs — build_diff_info" + - "crates/aprender-contracts/src/query/query_enrich_tests.rs — the falsifiers" + +equations: + diff_info_is_sha_plus_date_only: + formula: "for a tracked path p: len(commit_hash) == 40 AND len(last_modified) == 10 AND days_ago == parse_iso_days_ago(last_modified, now)" + domain: "a contract path with at least one commit in git" + codomain: "Some(DiffInfo)" + invariants: + - "The time part of the author date is stripped; a date with a time suffix is a defect" + - "A path git has no history for yields None, not an empty DiffInfo" + +proof_obligations: + - id: PVQDI-INV-001 + type: invariant + property: "A tracked file yields a 40-hex sha and a 10-character Y-M-D date" + formal: "cargo test -p aprender-contracts --lib build_diff_info_reports_the_last_commit_of_a_tracked_file exits 0" + applies_to: diff_info_is_sha_plus_date_only + - id: PVQDI-INV-002 + type: invariant + property: "A path with no git history yields None" + formal: "cargo test -p aprender-contracts --lib build_diff_info_is_none_for_a_path_git_has_no_history_for exits 0" + applies_to: diff_info_is_sha_plus_date_only + +falsification_tests: + - id: FALSIFY-PVQDI-001 + rule: "date part keeps the time suffix" + prediction: "mutating date_part to the raw %aI string turns the tracked-file test RED" + test: "cargo test -p aprender-contracts --lib build_diff_info_reports_the_last_commit_of_a_tracked_file" + if_fails: "build_diff_info leaks a time component into last_modified" + - id: FALSIFY-PVQDI-002 + rule: "missing path invents a DiffInfo" + prediction: "a nonexistent path returns None" + test: "cargo test -p aprender-contracts --lib build_diff_info_is_none_for_a_path_git_has_no_history_for" + if_fails: "build_diff_info returns Some for a path without history" diff --git a/crates/aprender-contracts/src/query/query_enrich_tests.rs b/crates/aprender-contracts/src/query/query_enrich_tests.rs index dd6d0f33e8..0d4e7f7f95 100644 --- a/crates/aprender-contracts/src/query/query_enrich_tests.rs +++ b/crates/aprender-contracts/src/query/query_enrich_tests.rs @@ -284,3 +284,44 @@ bindings: assert_eq!(g_binding.status, "unbound"); assert!(g_binding.module_path.is_none()); } + +fn entry_at(path: &str) -> types::ContractEntry { + let mut e = test_entry("diff-info", vec![], 0, 0); + e.path = path.into(); + e +} + +#[test] +fn build_diff_info_reports_the_last_commit_of_a_tracked_file() { + let manifest = concat!(env!("CARGO_MANIFEST_DIR"), "/Cargo.toml"); + let info = build_diff_info(&entry_at(manifest)).expect("Cargo.toml is tracked"); + assert_eq!(info.commit_hash.len(), 40, "full sha: {}", info.commit_hash); + assert!(info.commit_hash.bytes().all(|b| b.is_ascii_hexdigit())); + let parts: Vec<&str> = info.last_modified.split('-').collect(); + assert_eq!(parts.len(), 3, "date part is Y-M-D: {}", info.last_modified); + assert_eq!(parts[0].len(), 4); + assert_eq!(info.last_modified.len(), 10, "time part is stripped"); + assert!(info.days_ago < 36_500, "days_ago is relative to now"); +} + +#[test] +fn build_diff_info_days_ago_matches_parse_iso_days_ago() { + let manifest = concat!(env!("CARGO_MANIFEST_DIR"), "/Cargo.toml"); + let info = build_diff_info(&entry_at(manifest)).expect("tracked"); + let now = std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .unwrap() + .as_secs(); + let expect = parse_iso_days_ago(&info.last_modified, now); + assert!( + info.days_ago.abs_diff(expect) <= 1, + "{} vs {expect}", + info.days_ago + ); +} + +#[test] +fn build_diff_info_is_none_for_a_path_git_has_no_history_for() { + let missing = concat!(env!("CARGO_MANIFEST_DIR"), "/no-such-file-5580.yaml"); + assert!(build_diff_info(&entry_at(missing)).is_none()); +} From 7a0e8741e0532bf8fcfdfa890ee2cde63f527936 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 19:19:47 +0200 Subject: [PATCH 03/12] test(compute): cover relu_inplace and mul_scalar_alloc (Refs #5582) Adds C-BLIS-ELEMENTWISE-INPLACE with two falsifiers; relu max->min mutation turns 2 tests RED. Co-Authored-By: Claude Sonnet 5.5 (cherry picked from commit a2e8060c2ea2e8caa00ba13c27e7d2616fba9526) --- README.md | 4 +- contracts/blis-elementwise-inplace-v1.yaml | 65 +++++++++++++++++++ contracts/contracts.nt | 5 ++ .../aprender-compute/src/blis/elementwise.rs | 41 ++++++++++++ docs/findings/w5382.jsonl | 1 + 5 files changed, 114 insertions(+), 2 deletions(-) create mode 100644 contracts/blis-elementwise-inplace-v1.yaml create mode 100644 docs/findings/w5382.jsonl diff --git a/README.md b/README.md index 0d2356ff40..027a6b2a7d 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 | **1983** 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 | **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`) | | 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 1983 contracts across inference, training, quantization, attention, FFN, +The tree carries 1984 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/blis-elementwise-inplace-v1.yaml b/contracts/blis-elementwise-inplace-v1.yaml new file mode 100644 index 0000000000..60bd64b9a9 --- /dev/null +++ b/contracts/blis-elementwise-inplace-v1.yaml @@ -0,0 +1,65 @@ +metadata: + id: C-BLIS-ELEMENTWISE-INPLACE + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + kind: pattern + status: ACTIVE_ALGORITHM_LEVEL + description: | + Pins relu_inplace and mul_scalar_alloc in aprender-compute's BLIS elementwise + module (#5582): relu_inplace equals the out-of-place relu for every length + (including SIMD tail lengths), and mul_scalar_alloc returns a fresh vector of + the same length with every element scaled and the input untouched. + references: + - 'crates/aprender-compute/src/blis/elementwise.rs (relu_inplace, mul_scalar_alloc)' + +equations: + relu_inplace_equals_relu: + formula: | + relu_inplace(x) == relu(x) elementwise, for any length incl. 0 and non-multiples of the SIMD width + relu(v) = max(v, 0) + domain: f32 slices + invariants: + - 'negatives and -0.0 map to 0.0; zero and positives are unchanged' + mul_scalar_alloc_scales: + formula: 'mul_scalar_alloc(x, s)[i] == x[i] * s; len preserved; x not mutated' + domain: f32 slices, finite scalar + invariants: + - 's == 1.0 is the identity' + +proof_obligations: +- id: BEI-INV-001 + type: invariant + property: in-place ReLU equals out-of-place ReLU + formal: 'relu_inplace(x) == relu(x)' + applies_to: relu_inplace_equals_relu +- id: BEI-INV-002 + type: invariant + property: mul_scalar_alloc scales each element and keeps length + formal: 'out[i] == x[i] * s and len(out) == len(x)' + applies_to: mul_scalar_alloc_scales + +falsification_tests: +- id: FALSIFY-BLIS-ELEMENTWISE-INPLACE-001 + rule: relu_inplace clamps negatives and matches relu across tail lengths + prediction: 'n in {0,1,7,8,9,31,33} match relu; [-2,-0,0,0.5,3,-1e-9,f32::MIN] -> [0,0,0,0.5,3,0,0]' + test: cargo test -p aprender-compute --lib blis::elementwise::tests::relu_inplace + if_fails: in-place ReLU diverges from the out-of-place kernel (negative activations leak through) + ship_blocking: false + mutation: 'replace x.max(0.0) with x.min(0.0) in relu_inplace; must turn RED' +- id: FALSIFY-BLIS-ELEMENTWISE-INPLACE-002 + rule: mul_scalar_alloc scales every element, preserves length, leaves input untouched + prediction: '19-element ramp times 2.5 matches exactly; scalar 1.0 returns the input unchanged' + test: cargo test -p aprender-compute --lib blis::elementwise::tests::mul_scalar_alloc + if_fails: allocating scalar multiply drops, mis-scales or mutates elements + ship_blocking: false + +qa_gate: + id: QA-BLIS-ELEMENTWISE-INPLACE-001 + name: BLIS elementwise in-place/alloc gate + description: relu_inplace and mul_scalar_alloc semantics hold + checks: + - relu_inplace_equals_relu + - mul_scalar_alloc_scales + pass_criteria: FALSIFY-BLIS-ELEMENTWISE-INPLACE-001 and -002 pass + falsification: Any failure fails the gate diff --git a/contracts/contracts.nt b/contracts/contracts.nt index c34b6bfbee..277162579b 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -9386,6 +9386,11 @@ . "contracts/forjar/blake3-state-v1.yaml"^^ . "blake3-state-v1"^^ . + . + . + "contracts/blis-elementwise-inplace-v1.yaml"^^ . + "blis-elementwise-inplace-v1"^^ . + "pattern"^^ . . . . diff --git a/crates/aprender-compute/src/blis/elementwise.rs b/crates/aprender-compute/src/blis/elementwise.rs index 3dbe53da54..5c10bdb49e 100644 --- a/crates/aprender-compute/src/blis/elementwise.rs +++ b/crates/aprender-compute/src/blis/elementwise.rs @@ -993,4 +993,45 @@ mod tests { // 2*x + 1, then relu: [-3,0] [-1,0] [1] [3] [5] assert_eq!(out, vec![0.0, 0.0, 1.0, 3.0, 5.0]); } + + // ── relu_inplace / mul_scalar_alloc (#5582) ─────────────────────────── + + #[test] + fn relu_inplace_clamps_negatives_and_keeps_zero_and_positives() { + let mut data = [-2.0f32, -0.0, 0.0, 0.5, 3.0, -1e-9, f32::MIN]; + relu_inplace(&mut data); + assert_eq!(data, [0.0, 0.0, 0.0, 0.5, 3.0, 0.0, 0.0]); + } + + #[test] + fn relu_inplace_matches_out_of_place_relu_across_tail_lengths() { + for n in [0usize, 1, 7, 8, 9, 31, 33] { + let input: Vec = (0..n).map(|i| ((i * 13 + 5) % 17) as f32 - 8.0).collect(); + let mut expected = vec![0.0f32; n]; + if n > 0 { + relu(&input, &mut expected).unwrap(); + } + let mut actual = input.clone(); + relu_inplace(&mut actual); + assert_eq!(actual, expected, "n={n}"); + } + } + + #[test] + fn mul_scalar_alloc_scales_every_element_and_preserves_length() { + let input: Vec = (0..19).map(|i| i as f32 - 9.0).collect(); + let out = mul_scalar_alloc(&input, 2.5); + assert_eq!(out.len(), input.len()); + for (o, i) in out.iter().zip(&input) { + assert_eq!(*o, i * 2.5); + } + } + + #[test] + fn mul_scalar_alloc_by_one_is_identity_and_input_untouched() { + let input = vec![1.5f32, -2.0, 0.0, 7.25, -0.125, 3.0, 9.0, 11.0, -13.0]; + let before = input.clone(); + assert_eq!(mul_scalar_alloc(&input, 1.0), before); + assert_eq!(input, before); + } } diff --git a/docs/findings/w5382.jsonl b/docs/findings/w5382.jsonl new file mode 100644 index 0000000000..eb49f4774f --- /dev/null +++ b/docs/findings/w5382.jsonl @@ -0,0 +1 @@ +{"id":"FND-20261018-compute-inplace-unreferenced","title":"aprender-compute pub fns with a single reference (their definition): blocking_8x48, packed_a/b_size_v2, with_reserve, get_checksums","evidence":"grep -rw over crates/aprender-compute/{src,tests,benches,examples} finds exactly one hit each; pmat --coverage-gaps timed out without cached llvm-cov","repro":"grep -rwn packed_a_size_v2 crates/aprender-compute","suspected_epic":"unknown","severity":"P3","found_at_sha":"e00034704047bc22f843f7b512f34d3524a0a403"} From bb7d0f97a04ebb0252c1734db8418c3c29e8141e Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 20:13:14 +0200 Subject: [PATCH 04/12] chore(contracts): regen contracts.nt and README contract count for the folded contracts Co-Authored-By: Claude Sonnet 5.5 --- README.md | 4 ++-- contracts/contracts.nt | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) 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 277162579b..ac89048d02 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -13094,6 +13094,11 @@ "contracts/pv-cli-surface-v1.yaml"^^ . "pv-cli-surface-v1"^^ . "pattern"^^ . + . + . + "contracts/pv-query-diff-info-v1.yaml"^^ . + "pv-query-diff-info-v1"^^ . + "pattern"^^ . . . "contracts/pv-version-identity-v1.yaml"^^ . From 7be03853773b2c0b3d1a613c4c2ecf7139799b43 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 20:18:24 +0200 Subject: [PATCH 05/12] =?UTF-8?q?fix(contracts):=20formal:=20lines=20carry?= =?UTF-8?q?=20declared=20=CE=A3=20symbols=20(formal=5Fprose=20baseline=20i?= =?UTF-8?q?s=20shrink-only)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 5.5 --- contracts/blis-elementwise-inplace-v1.yaml | 2 +- contracts/pv-query-diff-info-v1.yaml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/contracts/blis-elementwise-inplace-v1.yaml b/contracts/blis-elementwise-inplace-v1.yaml index 60bd64b9a9..14a92d8545 100644 --- a/contracts/blis-elementwise-inplace-v1.yaml +++ b/contracts/blis-elementwise-inplace-v1.yaml @@ -31,7 +31,7 @@ proof_obligations: - id: BEI-INV-001 type: invariant property: in-place ReLU equals out-of-place ReLU - formal: 'relu_inplace(x) == relu(x)' + formal: '∀ x: relu_inplace(x) ≡ relu(x)' applies_to: relu_inplace_equals_relu - id: BEI-INV-002 type: invariant diff --git a/contracts/pv-query-diff-info-v1.yaml b/contracts/pv-query-diff-info-v1.yaml index 0b5d815a70..16a3c7ef2f 100644 --- a/contracts/pv-query-diff-info-v1.yaml +++ b/contracts/pv-query-diff-info-v1.yaml @@ -22,12 +22,12 @@ proof_obligations: - id: PVQDI-INV-001 type: invariant property: "A tracked file yields a 40-hex sha and a 10-character Y-M-D date" - formal: "cargo test -p aprender-contracts --lib build_diff_info_reports_the_last_commit_of_a_tracked_file exits 0" + formal: "∀ tracked p: len(commit_hash(p)) = 40 ∧ len(last_modified(p)) = 10" applies_to: diff_info_is_sha_plus_date_only - id: PVQDI-INV-002 type: invariant property: "A path with no git history yields None" - formal: "cargo test -p aprender-contracts --lib build_diff_info_is_none_for_a_path_git_has_no_history_for exits 0" + formal: "p ∉ git_history ⇒ build_diff_info(p) ≡ None" applies_to: diff_info_is_sha_plus_date_only falsification_tests: From 62628eaafc45cd697a788ee2a70fb9ea9c8182bd Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 20:20:12 +0200 Subject: [PATCH 06/12] chore(contracts): regen ONT witness (pv-sat) for the folded contract changes Co-Authored-By: Claude Sonnet 5.5 --- ...2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 184d38c1eb..63fba2f6b2 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "021e98642f5a6c17b5389d388a0d4b18df2707f513fda99ae35b661dca0b03c3", + "census_id_set_sha256": "7846d7a3bcda94fa7233d4b1511a1defd702fbbfc6544e36a07e650909659331", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "a56c47b937da11a6c94132b89c28d9420a84f372", + "reasoner_git_sha": "7be03853773b2c0b3d1a613c4c2ecf7139799b43", "checkable_n": 87, "result": { "kind": "model", From 2f2abe0666deb8bbfcdfb899dd86d5d1b57266e0 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 21:57:51 +0200 Subject: [PATCH 07/12] Revert #5577 corpus-ingest test from this fold: touching a cited evidence file needs a surface_audit.csv re-audit (dogfood G2.1) Co-Authored-By: Claude Sonnet 5.5 --- ...in-apr-cli--aprender-corpus-ingest-v1.yaml | 6 ----- crates/apr-cli/src/bin/apr-corpus-ingest.rs | 25 ------------------- docs/findings/aprender-w5404.jsonl | 1 - 3 files changed, 32 deletions(-) delete mode 100644 docs/findings/aprender-w5404.jsonl diff --git a/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml b/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml index 9806261dd8..b1be05c385 100644 --- a/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml +++ b/contracts/bin-apr-cli--aprender-corpus-ingest-v1.yaml @@ -114,9 +114,3 @@ falsification_tests: if_fails: "GREEN 2026-09-26: 2 rows, set-equal to the 2 commands" mutation: 'delete every aprender-corpus-ingest row; must turn RED naming aprender-corpus-ingest' - - id: FALSIFY-BIN-APR_CORPUS_INGEST-006 - rule: 'civil_from_days and now_utc_iso8601 produce correct civil dates and a fixed-shape stamp' - prediction: 'epoch is 1970-01-01, 2000-02-29 exists, 1900 has no Feb 29, day -1 is 1969-12-31, and the stamp is 20 bytes ending in Z' - test: 'cargo test -p apr-cli --bin aprender-corpus-ingest -- civil_from_days now_utc' - if_fails: 'ingest manifests carry a wrong date or a malformed timestamp' - mutation: 'change the 719_468 epoch offset by one; must turn RED' diff --git a/crates/apr-cli/src/bin/apr-corpus-ingest.rs b/crates/apr-cli/src/bin/apr-corpus-ingest.rs index c729010a08..5299ecdd29 100644 --- a/crates/apr-cli/src/bin/apr-corpus-ingest.rs +++ b/crates/apr-cli/src/bin/apr-corpus-ingest.rs @@ -524,29 +524,4 @@ mod tests { } assert_eq!(report.present_top_keys.len(), REQUIRED_TOP_KEYS.len()); } - - #[test] - fn civil_from_days_epoch_and_leap_boundaries() { - assert_eq!(civil_from_days(0), (1970, 1, 1)); - assert_eq!(civil_from_days(59), (1970, 3, 1)); - // 2000-02-29 (divisible-by-400 leap day) is day 11_016. - assert_eq!(civil_from_days(11_016), (2000, 2, 29)); - assert_eq!(civil_from_days(11_017), (2000, 3, 1)); - // 1900 is not a leap year; the day before the epoch is 1969-12-31. - assert_eq!(civil_from_days(-1), (1969, 12, 31)); - assert_eq!(civil_from_days(-25_508), (1900, 3, 1)); - assert_eq!(civil_from_days(-25_509), (1900, 2, 28)); - } - - #[test] - fn now_utc_iso8601_has_fixed_shape() { - let s = now_utc_iso8601(); - let b = s.as_bytes(); - assert_eq!(b.len(), 20, "got {s}"); - assert_eq!( - (b[4], b[7], b[10], b[13], b[16], b[19]), - (b'-', b'-', b'T', b':', b':', b'Z') - ); - assert!(s.starts_with("20"), "year after 2000, got {s}"); - } } diff --git a/docs/findings/aprender-w5404.jsonl b/docs/findings/aprender-w5404.jsonl deleted file mode 100644 index e0a39ef406..0000000000 --- a/docs/findings/aprender-w5404.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"id":"5577-apr-cli-cov","utc":"2026-10-18T17:27Z","by":"aprender-w5404","base":"0ecee41d04","claim":"civil_from_days and now_utc_iso8601 in crates/apr-cli/src/bin/apr-corpus-ingest.rs had no test; now covered by two unit tests plus FALSIFY-BIN-APR_CORPUS_INGEST-006","method":"pmat query --coverage-gaps has no coverage file here, so ranking is arbitrary; picked a pure uncovered fn reachable from the tests mod"} From 9f6792d697320606cf0ac592712feb9f49ad50fb Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 00:18:32 +0200 Subject: [PATCH 08/12] ci: refresh event payload for closing-refs guard Co-Authored-By: Claude Sonnet 5.5 From 6580ab0f1bc6db0d5cd4ca08d222abcfef2c9255 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 02:20:38 +0200 Subject: [PATCH 09/12] ci: refresh event payload for closing-refs guard (keep-open marker) Co-Authored-By: Claude Sonnet 5.5 From 3f7aec73bf8dcee8ddc578c1929d5899426a2e75 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 17:30:51 +0200 Subject: [PATCH 10/12] fix(contracts): regenerate witness after merging main (WitnessStale failed ont5/lint gates) Co-Authored-By: Claude Sonnet 5.5 --- ...09244c59534f015f0be2f90923120a3027c176ad56723d0d850.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 13582518f0..dcb73f6d44 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "063d371c514532fccc38497ed2f0d85711be3c35061de05df561446f16e93d99", + "census_id_set_sha256": "f35a8759558850933e865631184bed94a128e1004b374ffff119dc1d5446cb55", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "56ae1edeaf9f0761d3e0f9bf0754fb735e7c3d05", + "reasoner_git_sha": "e4d4bc4162535ffcf0cd222a0b50ebf4addfdf06", "checkable_n": 87, "result": { "kind": "model", @@ -10,5 +10,5 @@ } }, "pc_reasoner": "fired", - "cpu_ms": 2 + "cpu_ms": 1 } From e1c7f59521e2f1259fbcdb777ab57f4f845c07a5 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 22:25:08 +0200 Subject: [PATCH 11/12] fix(contracts): regenerate shapes.ttl and witness with the in-tree pv (ont4b freshness gate) Co-Authored-By: Claude Sonnet 5.5 --- contracts/shapes.ttl | 68 ++++++++++++++++++++++---------------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/contracts/shapes.ttl b/contracts/shapes.ttl index a718856fa0..bed403e57d 100644 --- a/contracts/shapes.ttl +++ b/contracts/shapes.ttl @@ -1983,11 +1983,11 @@ ] ; sh:property [ sh:path ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:in ( "8.9" "12.1" ) ; @@ -2067,11 +2067,11 @@ sh:maxCount 1 ; sh:class ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2084,11 +2084,11 @@ sh:targetClass ; sh:property [ sh:path ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2103,11 +2103,11 @@ sh:targetClass ; sh:property [ sh:path ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2194,7 +2194,7 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; sh:property [ sh:path ; @@ -2217,7 +2217,7 @@ ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2239,7 +2239,7 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; sh:property [ sh:path ; @@ -2257,7 +2257,7 @@ sh:path ; sh:minCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; sh:property [ sh:path ; @@ -2269,7 +2269,7 @@ ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2283,7 +2283,7 @@ ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2347,11 +2347,11 @@ sh:path ; sh:minCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2392,11 +2392,11 @@ sh:path ; sh:minCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2448,11 +2448,11 @@ sh:path ; sh:minCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2511,11 +2511,11 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2543,11 +2543,11 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2569,11 +2569,11 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2595,11 +2595,11 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2626,11 +2626,11 @@ sh:minCount 1 ; sh:maxCount 1 ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2721,7 +2721,7 @@ sh:minCount 1 ; sh:class ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; sh:property [ sh:path ; @@ -2733,7 +2733,7 @@ ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; @@ -2768,11 +2768,11 @@ sh:maxCount 1 ; sh:class ; sh:nodeKind sh:IRI ; - sh:node ; + sh:node ; ] ; . - a sh:NodeShape ; + a sh:NodeShape ; sh:property [ sh:path ; sh:minCount 1 ; From c84a4e6de50f1b14324301d8112e406a89d6e7aa Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Tue, 20 Oct 2026 01:30:17 +0200 Subject: [PATCH 12/12] chore(readme): readme-sync, CONTRACT_COUNT 1985 -> 1987 after main merge (Refs #5583) Co-Authored-By: Claude Sonnet 5.5 --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 191f91b659..776da6afc1 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 | **1987** 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 1987 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates