batch: lane A 1 - fold #5784 #5781 #5728 #5827 (coverage; sub-PRs #5784 #5781 #5728 #5827)

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 | **<!-- CONTRACT_COUNT_START -->1996<!-- CONTRACT_COUNT_END -->** 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 | **<!-- CONTRACT_COUNT_START -->1997<!-- CONTRACT_COUNT_END -->** 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 <!-- CONTRACT_COUNT_START -->1996<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
+The tree carries <!-- CONTRACT_COUNT_START -->1997<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
 tokenization, model formats, CLI safety — and this README itself.
 
 ## Migration from old crates

ci/explicit-test-commands.d/826-contracts-cli-certify-analyze-config.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test certify_analyze_config_5622

contracts/bin-aprender-contracts-cli--pv-v1.yaml

@@ -174,3 +174,9 @@ falsification_tests:
     test: 'cargo test -p aprender-contracts-cli --test coverage_report_render'
     if_fails: 'the coverage report renderer drifts without a test noticing'
     mutation: 'print binding_partial in the Binding implemented line; coverage_with_binding_adds_binding_totals must turn RED (MEASURED 2026-10-19)'
+  - id: FALSIFY-BIN-PV-007
+    rule: '`certify` config analysis flags the algebraic constraints a transformer needs'
+    prediction: 'analyze_config derives head_dim = hidden/heads, defaults kv heads to heads, and names each failing check (positivity, hidden%heads, heads%kv, even head_dim) without dividing by zero'
+    test: 'cargo test -p aprender-contracts-cli --test certify_analyze_config_5622'
+    if_fails: 'a malformed config.json is certified, or the report names the wrong constraint'
+    mutation: 'change `head_dim % 2 == 0` to `head_dim % 2 == 1`; odd_head_dim_fails_only_the_rope_check must turn RED'

contracts/bin-aprender-qa-cli--apr-qa-v1.yaml

@@ -135,3 +135,9 @@ falsification_tests:
     test: 'cargo test -p aprender-qa-cli --test cli_surface_gate unusable_input_is_rejected'
     if_fails: 'MEASURED 2026-09-26 (aprender-01): GREEN on an unmutated tree; no source mutation was run for this binary'
     mutation: 'make a rejection path return Ok(()) or unwrap the read; must turn RED on that row'
+  - id: FALSIFY-BIN-APR-QA-007
+    rule: 'profile throughput minimums resolve per backend, then legacy, then 5 (cpu) / 50 (gpu)'
+    prediction: 'check_profiling_assertions records a failed assertion exactly when a measured tok/s is below the resolved minimum, and records nothing when profile_ci is absent'
+    test: 'cargo test -p aprender-qa-cli --lib profiling_assertion_tests'
+    if_fails: 'a throughput regression passes certification, or a legacy min_throughput stops applying'
+    mutation: 'change unwrap_or(5.0) to unwrap_or(6.0) in check_profiling_assertions; defaults_are_5_cpu_and_50_gpu must turn RED (run 2026-10-21T10:15Z on lambda-labs: mutant rc=101, 2 of 5 RED incl. defaults_are_5_cpu_and_50_gpu; restored rc=0, 5 passed)'

contracts/contracts.nt

@@ -13961,6 +13961,11 @@
 <https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .
 <https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/tensor-transpose-roundtrip-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
 <https://ont.paiml.dev/v1alpha1/contract/tensor-transpose-roundtrip-v1> <https://ont.paiml.dev/v1alpha1/id> "tensor-transpose-roundtrip-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
+<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/ns/prov#Entity> .
+<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
+<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/file> "contracts/test-lib-loadtest-run-phase-max-v1.yaml"^^<http://www.w3.org/2001/XMLSchema#string> .
+<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/id> "test-lib-loadtest-run-phase-max-v1"^^<http://www.w3.org/2001/XMLSchema#string> .
+<https://ont.paiml.dev/v1alpha1/contract/test-lib-loadtest-run-phase-max-v1> <https://ont.paiml.dev/v1alpha1/kind> "pattern"^^<http://www.w3.org/2001/XMLSchema#string> .
 <https://ont.paiml.dev/v1alpha1/contract/tfidf-l2-norm-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://www.w3.org/ns/prov#Entity> .
 <https://ont.paiml.dev/v1alpha1/contract/tfidf-l2-norm-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Contract> .
 <https://ont.paiml.dev/v1alpha1/contract/tfidf-l2-norm-v1> <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <https://ont.paiml.dev/v1alpha1/Kernel> .

contracts/distributed-training-v1.yaml

@@ -33,3 +33,8 @@ falsification:
     description: "loss(distributed, N) ≈ loss(single, N) within ε"
     test: "Related tests in crates/aprender-distribute/src/"
     evidence: "cargo test --lib"
+
+  - id: FALSIFY-DISTRIBUTED_TRAINING_V1_003
+    description: "run_worker clamps an out-of-range shard to the training split and fails closed on a bad coordinator (Shutdown mid-AllReduce, non-shard message, refused connect)"
+    test: "crates/aprender-train/src/finetune/classify_trainer_tests.rs::run_worker_tests"
+    evidence: "cargo test -p aprender-train --lib run_worker_tests"

contracts/test-lib-loadtest-run-phase-max-v1.yaml

@@ -0,0 +1,47 @@
+metadata:
+  version: 1.0.0
+  created: '2026-10-19'
+  author: PAIML Engineering
+  description: "aprender-test-lib LoadTest::run_phase_max (#5626) — closed-loop phase: every worker sends back-to-back requests until the deadline and the records carry the server's token counts; a dead server yields failed records, a zero-length phase sends nothing."
+  kind: pattern
+  references:
+    - "crates/aprender-test-lib/src/llm/loadtest.rs — run_phase_max"
+    - "aprender#5626 — coverage ticket"
+
+equations:
+  closed_loop_phase:
+    formula: "records(run_phase_max(d)) = [] when d = 0; otherwise >= concurrency records; success iff the server answered 2xx with a parseable body; tokens = usage.completion_tokens"
+    domain: "LoadTest with Max rate, a duration, and an HTTP endpoint"
+    codomain: "Vec<RequestRecord>"
+    invariants:
+      - "response content is not captured unless validation needs it"
+      - "an unreachable server never yields a successful record"
+
+proof_obligations:
+  - id: LOADTEST-MAX-INV-001
+    type: invariant
+    property: "Records carry the server's token counts and finish reason"
+    formal: "∀ run: cargo test -p aprender-test-lib --features llm --lib test_run_phase_max_records_server_token_counts exits 0"
+    applies_to: closed_loop_phase
+  - id: LOADTEST-MAX-INV-002
+    type: invariant
+    property: "Zero-length phase sends nothing"
+    formal: "∀ run: cargo test -p aprender-test-lib --features llm --lib test_run_phase_max_zero_duration_sends_nothing exits 0"
+    applies_to: closed_loop_phase
+
+falsification_tests:
+  - id: FALSIFY-LOADTEST-MAX-001
+    rule: "deadline loop disabled"
+    prediction: "replacing the while condition with false turns test_run_phase_max_records_server_token_counts RED"
+    test: "cargo test -p aprender-test-lib --features llm --lib test_run_phase_max_records_server_token_counts"
+    if_fails: "worker loop is unguarded"
+  - id: FALSIFY-LOADTEST-MAX-002
+    rule: "workers not spawned"
+    prediction: "spawning 0 workers turns test_run_phase_max_unreachable_server_yields_failed_records RED"
+    test: "cargo test -p aprender-test-lib --features llm --lib test_run_phase_max_unreachable_server_yields_failed_records"
+    if_fails: "worker spawn count is unguarded"
+  - id: FALSIFY-LOADTEST-MAX-003
+    rule: "content capture forced on"
+    prediction: "capture_content = true turns test_run_phase_max_records_server_token_counts RED"
+    test: "cargo test -p aprender-test-lib --features llm --lib test_run_phase_max_records_server_token_counts"
+    if_fails: "content capture gating is unguarded"

contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json

@@ -1,5 +1,5 @@
 {
-  "census_id_set_sha256": "db20faa02774eeffec52d05d3e579c0ec7047e2f0bed655de26b7e3eeff34151",
+  "census_id_set_sha256": "a3ed7f39b829b351f611f40bcdd1f5d2193f087021ff4941712d41f762526b6e",
   "relations_sha256": "811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850",
   "checkable_n": 87,
   "result": {

crates/aprender-contracts-cli/tests/certify_analyze_config_5622.rs

@@ -0,0 +1,101 @@
+//! `certify::analyze_config` derives geometry from a HF `config.json` and flags
+//! the algebraic constraints a transformer needs (#5622).
+
+use aprender_contracts_cli::commands::certify::analyze_config;
+
+fn analyze(json: &str) -> serde_json::Value {
+    let dir = tempfile::tempdir().expect("tempdir");
+    let p = dir.path().join("config.json");
+    std::fs::write(&p, json).expect("write");
+    analyze_config(&p).expect("analyze")
+}
+
+fn failed_checks(v: &serde_json::Value) -> Vec<String> {
+    v["algebra_checks"]
+        .as_array()
+        .expect("array")
+        .iter()
+        .filter(|c| c["passed"] == false)
+        .map(|c| c["check"].as_str().expect("name").to_string())
+        .collect()
+}
+
+#[test]
+fn valid_config_derives_geometry_and_passes_every_check() {
+    let v = analyze(
+        r#"{"hidden_size":64,"num_hidden_layers":2,"num_attention_heads":8,
+            "num_key_value_heads":2,"vocab_size":100}"#,
+    );
+    assert_eq!(v["head_dim"], 8);
+    assert_eq!(v["num_kv_heads"], 2);
+    // embed + 9 tensors per layer + final norm + lm_head
+    assert_eq!(v["expected_tensors"], 1 + 2 * 9 + 2);
+    assert_eq!(v["algebra_checks"].as_array().expect("array").len(), 7);
+    assert_eq!(v["all_checks_pass"], true);
+    assert!(failed_checks(&v).is_empty());
+}
+
+#[test]
+fn kv_heads_default_to_attention_heads() {
+    let v = analyze(
+        r#"{"hidden_size":32,"num_hidden_layers":1,"num_attention_heads":4,"vocab_size":10}"#,
+    );
+    assert_eq!(v["num_kv_heads"], 4);
+    assert_eq!(v["all_checks_pass"], true);
+}
+
+#[test]
+fn empty_config_fails_the_positivity_checks_without_dividing_by_zero() {
+    let v = analyze("{}");
+    assert_eq!(v["all_checks_pass"], false);
+    assert_eq!(v["head_dim"], 0);
+    assert_eq!(v["expected_tensors"], 0);
+    let failed = failed_checks(&v);
+    for name in [
+        "hidden_size > 0",
+        "num_layers > 0",
+        "num_heads > 0",
+        "vocab_size > 0",
+    ] {
+        assert!(
+            failed.iter().any(|f| f == name),
+            "{name} should fail: {failed:?}"
+        );
+    }
+}
+
+#[test]
+fn indivisible_heads_are_named() {
+    let v = analyze(
+        r#"{"hidden_size":30,"num_hidden_layers":1,"num_attention_heads":4,
+            "num_key_value_heads":3,"vocab_size":10}"#,
+    );
+    assert_eq!(v["all_checks_pass"], false);
+    let failed = failed_checks(&v);
+    assert!(
+        failed.contains(&"hidden_size % num_heads == 0".to_string()),
+        "{failed:?}"
+    );
+    assert!(
+        failed.contains(&"num_heads % num_kv_heads == 0".to_string()),
+        "{failed:?}"
+    );
+}
+
+#[test]
+fn odd_head_dim_fails_only_the_rope_check() {
+    let v = analyze(
+        r#"{"hidden_size":12,"num_hidden_layers":1,"num_attention_heads":4,"vocab_size":10}"#,
+    );
+    assert_eq!(v["head_dim"], 3);
+    assert_eq!(failed_checks(&v), vec!["head_dim % 2 == 0".to_string()]);
+}
+
+#[test]
+fn missing_file_and_bad_json_are_errors() {
+    let dir = tempfile::tempdir().expect("tempdir");
+    assert!(analyze_config(&dir.path().join("absent.json")).is_err());
+    let p = dir.path().join("bad.json");
+    std::fs::write(&p, "{not json").expect("write");
+    assert!(analyze_config(&p).is_err());
+}

crates/aprender-explain/src/tui/mod.rs

@@ -431,3 +431,6 @@ fn render_status_bar(canvas: &mut DirectTerminalCanvas<'_>, width: u16, height:
 mod scrollbar_tests;
 #[cfg(test)]
 mod tests;
+
+#[cfg(test)]
+mod source_pane_tests;

crates/aprender-explain/src/tui/source_pane_tests.rs

@@ -0,0 +1,107 @@
+//! `render_source_pane` (#5601): title, line numbers, scroll offset, truncation, borders.
+
+use super::*;
+use crate::analyzer::AnalysisReport;
+
+const W: u16 = 30;
+
+fn app_with(src: &str, scroll: u16) -> TuiApp {
+    let report = AnalysisReport {
+        name: "k".to_string(),
+        ..Default::default()
+    };
+    let mut app = TuiApp::new(src.to_string(), report);
+    app.source_scroll = scroll;
+    app
+}
+
+/// Render the pane at (0,0) with the given height into a W x 12 buffer.
+fn rendered(app: &TuiApp, width: u16, height: u16) -> CellBuffer {
+    let mut buf = CellBuffer::new(W, 12);
+    {
+        let mut canvas = DirectTerminalCanvas::new(&mut buf);
+        render_source_pane(&mut canvas, app, 0.0, 0.0, width, height);
+    }
+    buf
+}
+
+fn cell(buf: &CellBuffer, x: u16, y: u16) -> String {
+    buf.get(x, y).expect("cell").symbol.to_string()
+}
+
+fn row(buf: &CellBuffer, y: u16) -> String {
+    (0..W)
+        .map(|x| buf.get(x, y).expect("cell").symbol.to_string())
+        .collect::<String>()
+        .trim_end()
+        .to_string()
+}
+
+#[test]
+fn title_carries_the_report_name_and_corners() {
+    let buf = rendered(&app_with("ret;", 0), 20, 5);
+    let top = row(&buf, 0);
+    assert!(top.starts_with("┌ PTX: k "), "{top}");
+    assert!(top.ends_with('┐'), "{top}");
+    assert_eq!(top.chars().count(), 20, "{top}");
+    let bottom = row(&buf, 4);
+    assert_eq!(bottom, format!("└{}┘", "─".repeat(18)));
+}
+
+#[test]
+fn rows_show_one_based_line_numbers_and_text_between_borders() {
+    let buf = rendered(&app_with("a\nb\nc", 0), 20, 5);
+    let r1 = row(&buf, 1);
+    assert!(r1.starts_with("│   1 a"), "{r1}");
+    assert_eq!(cell(&buf, 19, 1), "│", "right border");
+    assert!(row(&buf, 2).starts_with("│   2 b"), "{}", row(&buf, 2));
+    assert!(row(&buf, 3).starts_with("│   3 c"), "{}", row(&buf, 3));
+}
+
+#[test]
+fn scroll_offsets_the_first_visible_line() {
+    let src = "l1\nl2\nl3\nl4\nl5";
+    let buf = rendered(&app_with(src, 2), 20, 5);
+    assert!(row(&buf, 1).starts_with("│   3 l3"), "{}", row(&buf, 1));
+    assert!(row(&buf, 2).starts_with("│   4 l4"), "{}", row(&buf, 2));
+    assert!(row(&buf, 3).starts_with("│   5 l5"), "{}", row(&buf, 3));
+}
+
+#[test]
+fn rows_past_the_end_keep_borders_but_have_no_line_number() {
+    let buf = rendered(&app_with("only", 0), 20, 5);
+    let r = row(&buf, 2);
+    assert!(r.starts_with('│'), "{r}");
+    assert!(!r.chars().any(|c| c.is_ascii_digit()), "{r}");
+    assert_eq!(cell(&buf, 19, 2), "│", "right border");
+}
+
+#[test]
+fn long_lines_are_truncated_to_the_inner_width() {
+    // width 20 -> inner 18 -> text budget 18 - 6 = 12 chars
+    let buf = rendered(&app_with("ABCDEFGHIJKLMNOPQRST", 0), 20, 4);
+    let r = row(&buf, 1);
+    // text occupies cols 6..=17; col 18 is the scrollbar, col 19 the border
+    assert_eq!(cell(&buf, 6, 1), "A");
+    assert_eq!(cell(&buf, 17, 1), "L");
+    assert_eq!(cell(&buf, 19, 1), "│");
+    assert!((20..W).all(|x| cell(&buf, x, 1) == " "), "{r}");
+}
+
+#[test]
+fn offset_origin_moves_the_whole_pane() {
+    let app = app_with("a", 0);
+    let mut buf = CellBuffer::new(W, 12);
+    {
+        let mut canvas = DirectTerminalCanvas::new(&mut buf);
+        render_source_pane(&mut canvas, &app, 2.0, 3.0, 20, 4);
+    }
+    assert_eq!(cell(&buf, 2, 3), "┌");
+    assert_eq!(cell(&buf, 2, 6), "└");
+    assert_eq!(cell(&buf, 0, 3), " ");
+    // content row 4: left border at x, number at x+1, text at x+6, right border at x+width-1
+    assert_eq!(cell(&buf, 2, 4), "│");
+    assert_eq!(cell(&buf, 6, 4), "1");
+    assert_eq!(cell(&buf, 8, 4), "a");
+    assert_eq!(cell(&buf, 21, 4), "│");
+}