diff --git a/ci/explicit-test-commands.d/817-contracts-cli-certify-analyze-config.cmd b/ci/explicit-test-commands.d/817-contracts-cli-certify-analyze-config.cmd new file mode 100644 index 0000000000..6460edb736 --- /dev/null +++ b/ci/explicit-test-commands.d/817-contracts-cli-certify-analyze-config.cmd @@ -0,0 +1 @@ +cargo test -p aprender-contracts-cli --test certify_analyze_config_5622 diff --git a/contracts/bin-aprender-contracts-cli--pv-v1.yaml b/contracts/bin-aprender-contracts-cli--pv-v1.yaml index c4358221b9..f2e048b2a9 100644 --- a/contracts/bin-aprender-contracts-cli--pv-v1.yaml +++ b/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' diff --git a/contracts/contracts.nt b/contracts/contracts.nt index 87447a2049..a0b20c44eb 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -13961,6 +13961,11 @@ . "contracts/tensor-transpose-roundtrip-v1.yaml"^^ . "tensor-transpose-roundtrip-v1"^^ . + . + . + "contracts/test-lib-loadtest-run-phase-max-v1.yaml"^^ . + "test-lib-loadtest-run-phase-max-v1"^^ . + "pattern"^^ . . . . diff --git a/contracts/test-lib-loadtest-run-phase-max-v1.yaml b/contracts/test-lib-loadtest-run-phase-max-v1.yaml new file mode 100644 index 0000000000..5ecdbb320d --- /dev/null +++ b/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" + 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" diff --git a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json b/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json index 5ca9abb1de..cd088777f2 100644 --- a/contracts/witness/811c78184eb2609244c59534f015f0be2f90923120a3027c176ad56723d0d850.json +++ b/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": { diff --git a/crates/aprender-contracts-cli/tests/certify_analyze_config_5622.rs b/crates/aprender-contracts-cli/tests/certify_analyze_config_5622.rs new file mode 100644 index 0000000000..0a7f11c803 --- /dev/null +++ b/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 { + 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()); +} diff --git a/crates/aprender-sparse/src/bsr_new_5632_tests.rs b/crates/aprender-sparse/src/bsr_new_5632_tests.rs new file mode 100644 index 0000000000..b42f13bb61 --- /dev/null +++ b/crates/aprender-sparse/src/bsr_new_5632_tests.rs @@ -0,0 +1,91 @@ +//! Coverage for `BsrMatrix::new` validation (#5632). + +use crate::{BsrMatrix, SparseError}; + +#[test] +fn accepts_consistent_structure_and_reports_shape() { + // 2x3 block grid, block_size 2, two stored blocks. + let m = BsrMatrix::new(2, 3, 2, vec![0, 1, 2], vec![0, 2], vec![1.0; 8]).expect("valid"); + assert_eq!(m.rows(), 4); + assert_eq!(m.cols(), 6); + assert_eq!(m.block_size(), 2); + assert_eq!(m.nnz_blocks(), 2); +} + +#[test] +fn accepts_empty_matrix() { + let m = BsrMatrix::new(1, 1, 4, vec![0, 0], vec![], vec![]).expect("empty is valid"); + assert_eq!(m.nnz_blocks(), 0); + assert_eq!(m.rows(), 4); +} + +#[test] +fn rejects_offsets_of_wrong_length() { + let err = BsrMatrix::new(2, 2, 1, vec![0, 1], vec![0], vec![1.0]).expect_err("short offsets"); + assert!( + matches!( + err, + SparseError::InvalidOffsetsLength { + actual: 2, + expected: 3 + } + ), + "{err}" + ); + let err = BsrMatrix::new(1, 1, 1, vec![0, 0, 0], vec![], vec![]).expect_err("long offsets"); + assert!( + matches!( + err, + SparseError::InvalidOffsetsLength { + actual: 3, + expected: 2 + } + ), + "{err}" + ); +} + +#[test] +fn rejects_values_not_matching_block_count_times_block_area() { + // 1 block of 2x2 needs 4 values. + let err = BsrMatrix::new(1, 1, 2, vec![0, 1], vec![0], vec![1.0; 3]).expect_err("short"); + assert!( + matches!( + err, + SparseError::LengthMismatch { + col_len: 4, + val_len: 3 + } + ), + "{err}" + ); + let err = BsrMatrix::new(1, 1, 2, vec![0, 1], vec![0], vec![1.0; 5]).expect_err("long"); + assert!( + matches!( + err, + SparseError::LengthMismatch { + col_len: 4, + val_len: 5 + } + ), + "{err}" + ); +} + +#[test] +fn offsets_length_is_checked_before_values_length() { + let err = BsrMatrix::new(2, 2, 2, vec![0], vec![0], vec![]).expect_err("both wrong"); + assert!( + matches!(err, SparseError::InvalidOffsetsLength { .. }), + "{err}" + ); +} + +#[test] +fn new_matrix_round_trips_through_to_csr() { + // One 2x2 block [[1,2],[3,4]] at block (0,1) of a 1x2 block grid. + let m = BsrMatrix::new(1, 2, 2, vec![0, 1], vec![1], vec![1.0, 2.0, 3.0, 4.0]).expect("valid"); + let csr = m.to_csr().expect("csr"); + assert_eq!((csr.rows(), csr.cols()), (2, 4)); + assert_eq!(csr.nnz(), 4); +} diff --git a/crates/aprender-sparse/src/lib.rs b/crates/aprender-sparse/src/lib.rs index bedd6b75a5..41a444f1a8 100644 --- a/crates/aprender-sparse/src/lib.rs +++ b/crates/aprender-sparse/src/lib.rs @@ -69,3 +69,6 @@ pub use validate::validate_csr_invariants; #[cfg(test)] mod tests; + +#[cfg(test)] +mod bsr_new_5632_tests; diff --git a/crates/aprender-test-lib/src/llm/loadtest.rs b/crates/aprender-test-lib/src/llm/loadtest.rs index a80361e12f..f2c2348f2b 100644 --- a/crates/aprender-test-lib/src/llm/loadtest.rs +++ b/crates/aprender-test-lib/src/llm/loadtest.rs @@ -2378,4 +2378,79 @@ mod tests { assert_eq!(tail.jitter.spike_count, 0); assert!(!tail.drift.degradation_detected); } + + // ===== run_phase_max (FALSIFY-LOADTEST-MAX-001..003) ===== + + /// Serve `body` to every connection until the returned handle is aborted. + async fn spawn_json_server(body: &'static str) -> (String, tokio::task::JoinHandle<()>) { + use tokio::io::{AsyncReadExt, AsyncWriteExt}; + let listener = tokio::net::TcpListener::bind("127.0.0.1:0").await.unwrap(); + let url = format!("http://{}", listener.local_addr().unwrap()); + let handle = tokio::spawn(async move { + loop { + let Ok((mut sock, _)) = listener.accept().await else { + return; + }; + tokio::spawn(async move { + let mut buf = vec![0u8; 8192]; + let _ = sock.read(&mut buf).await; + let resp = format!( + "HTTP/1.1 200 OK\r\nContent-Type: application/json\r\nContent-Length: {}\r\nConnection: close\r\n\r\n{body}", + body.len() + ); + let _ = sock.write_all(resp.as_bytes()).await; + }); + } + }); + (url, handle) + } + + const CANNED: &str = r#"{"id":"x","object":"chat.completion","created":1,"model":"m","choices":[{"index":0,"message":{"role":"assistant","content":"4"},"finish_reason":"stop"}],"usage":{"prompt_tokens":7,"completion_tokens":3,"total_tokens":10}}"#; + + fn max_config(concurrency: usize) -> LoadTestConfig { + LoadTestConfig { + concurrency, + ..LoadTestConfig::default() + } + } + + #[tokio::test] + async fn test_run_phase_max_records_server_token_counts() { + let (url, server) = spawn_json_server(CANNED).await; + let lt = LoadTest::new(LlmClient::new(url, "m"), max_config(2)); + let records = lt.run_phase_max(Duration::from_millis(200)).await.unwrap(); + server.abort(); + assert!(records.len() >= 2, "each worker sends at least once"); + for r in &records { + assert!(r.success); + assert_eq!(r.tokens, 3); + assert_eq!(r.prompt_tokens, 7); + assert_eq!(r.finish_reason.as_deref(), Some("stop")); + assert!( + r.response_content.is_none(), + "content not captured by default" + ); + } + } + + #[tokio::test] + async fn test_run_phase_max_unreachable_server_yields_failed_records() { + // Bind then drop so the port is closed. + let l = tokio::net::TcpListener::bind("127.0.0.1:0").await.unwrap(); + let url = format!("http://{}", l.local_addr().unwrap()); + drop(l); + let lt = LoadTest::new(LlmClient::new(url, "m"), max_config(1)); + let records = lt.run_phase_max(Duration::from_millis(100)).await.unwrap(); + assert!(!records.is_empty()); + assert!(records.iter().all(|r| !r.success && r.tokens == 0)); + } + + #[tokio::test] + async fn test_run_phase_max_zero_duration_sends_nothing() { + let (url, server) = spawn_json_server(CANNED).await; + let lt = LoadTest::new(LlmClient::new(url, "m"), max_config(3)); + let records = lt.run_phase_max(Duration::ZERO).await.unwrap(); + server.abort(); + assert!(records.is_empty()); + } }