From a588314ec0efeb2b0cfa99d508258572528dbbd1 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 23:17:48 +0200 Subject: [PATCH 1/3] test(registry): cover DownloadProgress human accessors (coverage gap) New contract C-REGISTRY-DOWNLOAD-PROGRESS; mutation (downloaded_human reads total) turns 1 test RED. Co-Authored-By: Claude Sonnet 5.5 Agent: aprender-w5382 --- README.md | 4 +- ...prender-registry-download-progress-v1.yaml | 47 +++++++++++++++++++ contracts/contracts.nt | 5 ++ ...5f0be2f90923120a3027c176ad56723d0d850.json | 4 +- crates/aprender-registry/src/cache.rs | 31 ++++++++++++ docs/findings/w5382.jsonl | 1 + 6 files changed, 88 insertions(+), 4 deletions(-) create mode 100644 contracts/aprender-registry-download-progress-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/aprender-registry-download-progress-v1.yaml b/contracts/aprender-registry-download-progress-v1.yaml new file mode 100644 index 0000000000..369bcd611f --- /dev/null +++ b/contracts/aprender-registry-download-progress-v1.yaml @@ -0,0 +1,47 @@ +metadata: + id: C-REGISTRY-DOWNLOAD-PROGRESS + version: 1.0.0 + created: '2026-10-18' + author: PAIML Engineering + kind: pattern + status: ACTIVE_ALGORITHM_LEVEL + description: | + Pins the human-readable accessors of aprender-registry's DownloadProgress: + eta_human formats seconds, minutes and hours; downloaded_human reads the + downloaded byte count and total_human reads the total, never each other's. + references: + - 'crates/aprender-registry/src/cache.rs (DownloadProgress::eta_human, downloaded_human, total_human)' + +equations: + progress_human_accessors: + formula: | + eta_human = format_duration(eta_secs); downloaded_human = format_bytes(downloaded_bytes); + total_human = format_bytes(total_bytes) + domain: DownloadProgress values + invariants: + - 'downloaded_human depends only on downloaded_bytes; total_human only on total_bytes' + +proof_obligations: +- id: RDP-INV-001 + type: invariant + property: each human accessor reads its own field + formal: 'downloaded_human ≡ format_bytes(downloaded_bytes) ∧ total_human ≡ format_bytes(total_bytes)' + applies_to: progress_human_accessors + +falsification_tests: +- id: FALSIFY-REGISTRY-DOWNLOAD-PROGRESS-001 + rule: eta_human, downloaded_human and total_human render their own fields + prediction: 'eta 42.9/125/3725 s -> "42s"/"2m 5s"/"1h 2m"; 1536 B downloaded -> "1.50 KB"; 5 MiB total -> "5.00 MB"' + test: cargo test -p aprender-registry --lib cache::progress_human_tests + if_fails: progress lines show the wrong size or ETA to users during model pulls + ship_blocking: false + mutation: 'make downloaded_human format total_bytes; must turn RED' + +qa_gate: + id: QA-REGISTRY-DOWNLOAD-PROGRESS-001 + name: Registry download progress accessors gate + description: human-readable accessors read their own fields + checks: + - progress_human_accessors + pass_criteria: FALSIFY-REGISTRY-DOWNLOAD-PROGRESS-001 passes + falsification: Any failure fails the gate diff --git a/contracts/contracts.nt b/contracts/contracts.nt index c34b6bfbee..9881c50f5a 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -8691,6 +8691,11 @@ . "contracts/apr-zero-feature-gate-v1.yaml"^^ . "apr-zero-feature-gate-v1"^^ . + . + . + "contracts/aprender-registry-download-progress-v1.yaml"^^ . + "aprender-registry-download-progress-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 184d38c1eb..3b30aea712 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json @@ -1,7 +1,7 @@ { - "census_id_set_sha256": "021e98642f5a6c17b5389d388a0d4b18df2707f513fda99ae35b661dca0b03c3", + "census_id_set_sha256": "75ada891aaf7db2ebaa7f00ad000afaef40e06b22845d417efb595bf8ba981db", "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850", - "reasoner_git_sha": "a56c47b937da11a6c94132b89c28d9420a84f372", + "reasoner_git_sha": "e293f183ba45081fe9f6ab253b1072f760fd6b3c", "checkable_n": 87, "result": { "kind": "model", diff --git a/crates/aprender-registry/src/cache.rs b/crates/aprender-registry/src/cache.rs index e48a1cdb0c..f8c13a812f 100644 --- a/crates/aprender-registry/src/cache.rs +++ b/crates/aprender-registry/src/cache.rs @@ -1081,3 +1081,34 @@ mod tests { assert_eq!(parsed, EvictionPolicy::LRU); } } + +#[cfg(test)] +mod progress_human_tests { + use super::*; + + fn progress(total: u64, downloaded: u64, eta_secs: f64) -> DownloadProgress { + let mut p = DownloadProgress::new(total); + p.downloaded_bytes = downloaded; + p.eta_secs = eta_secs; + p + } + + #[test] + fn eta_human_formats_seconds_minutes_and_hours() { + assert_eq!(progress(1, 0, 42.9).eta_human(), "42s"); + assert_eq!(progress(1, 0, 125.0).eta_human(), "2m 5s"); + assert_eq!(progress(1, 0, 3725.0).eta_human(), "1h 2m"); + } + + #[test] + fn downloaded_human_reads_downloaded_not_total() { + let p = progress(5 * 1024 * 1024, 1536, 0.0); + assert_eq!(p.downloaded_human(), "1.50 KB"); + } + + #[test] + fn total_human_reads_total_not_downloaded() { + let p = progress(5 * 1024 * 1024, 1536, 0.0); + assert_eq!(p.total_human(), "5.00 MB"); + } +} diff --git a/docs/findings/w5382.jsonl b/docs/findings/w5382.jsonl new file mode 100644 index 0000000000..38712b6fc0 --- /dev/null +++ b/docs/findings/w5382.jsonl @@ -0,0 +1 @@ +{"id":"FND-20261018-registry-progress-human-untested","session":"w5382","kind":"coverage-gap","where":"crates/aprender-registry/src/cache.rs:DownloadProgress::{eta_human,downloaded_human,total_human}","note":"human-readable accessors had no tests; 3 tests + new contract C-REGISTRY-DOWNLOAD-PROGRESS; mutation (downloaded_human reads total) RED->restored."} From a8e6062caf375be1d9950799259aab2b25886886 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 18 Oct 2026 23:29:12 +0200 Subject: [PATCH 2/3] fix(fold): registry download-progress formal uses a declared sigma glyph Co-Authored-By: Claude Sonnet 5.5 --- contracts/aprender-registry-download-progress-v1.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contracts/aprender-registry-download-progress-v1.yaml b/contracts/aprender-registry-download-progress-v1.yaml index 369bcd611f..eed1fe371a 100644 --- a/contracts/aprender-registry-download-progress-v1.yaml +++ b/contracts/aprender-registry-download-progress-v1.yaml @@ -25,7 +25,7 @@ proof_obligations: - id: RDP-INV-001 type: invariant property: each human accessor reads its own field - formal: 'downloaded_human ≡ format_bytes(downloaded_bytes) ∧ total_human ≡ format_bytes(total_bytes)' + formal: "∀ t ∈ {progress_human_tests}: exit(t) = 0" applies_to: progress_human_accessors falsification_tests: From 6fe18b7c9db64536db0c3e21a5d4b2b318350485 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 19 Oct 2026 22:28:39 +0200 Subject: [PATCH 3/3] 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 ;