diff --git a/crates/aprender-compute/src/verification_specs.rs b/crates/aprender-compute/src/verification_specs.rs deleted file mode 100644 index 69114cbdb..000000000 --- a/crates/aprender-compute/src/verification_specs.rs +++ /dev/null @@ -1,317 +0,0 @@ -//! Formal Verification Specifications for trueno -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. -//! -//! When Verus is available, these can be mechanically verified. -//! Without Verus, they serve as checked documentation via debug_assert!(). - -/// Configuration validation invariants -/// -/// # Verification Specifications -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate that a size parameter is within acceptable bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate that an index is within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice invariant - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric invariants for computation safety -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition that checks for overflow - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate that a float value is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize a value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -// ─── Verus Formal Verification Specs ───────────────────────────── -// Domain: trueno - SIMD operations, tensor dimensions, memory alignment -// Machine-checkable pre/postconditions for tensor computation safety. - -#[cfg(verus)] -mod verus_specs { - use builtin::*; - use builtin_macros::*; - - verus! { - // ── Tensor dimension verification ── - - #[requires(rows > 0 && cols > 0)] - #[ensures(result == rows * cols)] - fn verify_tensor_size(rows: u64, cols: u64) -> u64 { - rows * cols - } - - #[requires(dim_a > 0 && dim_b > 0)] - #[ensures(result == (dim_a == dim_b))] - fn verify_dimension_match(dim_a: u64, dim_b: u64) -> bool { - dim_a == dim_b - } - - #[requires(a_cols == b_rows)] - #[ensures(result == a_rows * b_cols)] - #[recommends(a_rows * b_cols <= 1024 * 1024 * 1024)] - fn verify_matmul_output_size(a_rows: u64, a_cols: u64, b_rows: u64, b_cols: u64) -> u64 { - a_rows * b_cols - } - - #[requires(ndim > 0 && ndim <= 8)] - #[ensures(result == ndim)] - #[invariant(ndim <= 8)] - fn verify_tensor_rank(ndim: u64) -> u64 { ndim } - - // ── SIMD alignment verification ── - - #[requires(alignment > 0)] - #[ensures(result == (addr % alignment == 0))] - #[recommends(alignment == 32)] - fn verify_simd_alignment(addr: u64, alignment: u64) -> bool { - addr % alignment == 0 - } - - #[requires(size > 0)] - #[ensures(result >= size)] - #[ensures(result % 32 == 0)] - fn verify_aligned_alloc_size(size: u64) -> u64 { - ((size + 31) / 32) * 32 - } - - #[requires(lane_width > 0)] - #[ensures(result == (len % lane_width == 0))] - #[recommends(lane_width == 8)] - fn verify_simd_lane_alignment(len: u64, lane_width: u64) -> bool { - len % lane_width == 0 - } - - // ── Quantization verification ── - - #[requires(block_size > 0)] - #[ensures(result == (num_elements % block_size == 0))] - #[recommends(block_size == 32)] - fn verify_quant_block_alignment(num_elements: u64, block_size: u64) -> bool { - num_elements % block_size == 0 - } - - #[requires(bits > 0 && bits <= 8)] - #[ensures(result == (1u64 << bits) - 1)] - fn verify_quant_max_value(bits: u64) -> u64 { - (1u64 << bits) - 1 - } - - #[requires(num_blocks > 0)] - #[ensures(result == num_blocks * bytes_per_block)] - #[invariant(bytes_per_block > 0)] - fn verify_quantized_buffer_size(num_blocks: u64, bytes_per_block: u64) -> u64 { - num_blocks * bytes_per_block - } - - // ── Stride verification ── - - #[requires(ndim > 0)] - #[ensures(result > 0)] - #[decreases(ndim)] - fn verify_contiguous_stride(shape_product: u64, ndim: u64) -> u64 { - if ndim == 0 { 1 } else { shape_product } - } - - #[requires(offset < total_elements)] - #[ensures(result < total_elements)] - fn verify_element_offset(offset: u64, total_elements: u64) -> u64 { offset } - - // ── Memory pool verification ── - - #[requires(pool_capacity > 0)] - #[ensures(result <= pool_capacity)] - #[invariant(allocated <= pool_capacity)] - fn verify_pool_allocation(allocated: u64, pool_capacity: u64) -> u64 { allocated } - - #[requires(requested > 0)] - #[ensures(result == (available >= requested))] - #[recommends(available >= requested)] - fn verify_pool_has_space(available: u64, requested: u64) -> bool { - available >= requested - } - - // ── Broadcast verification ── - - #[requires(dim_a > 0 && dim_b > 0)] - #[ensures(result == (dim_a == dim_b || dim_a == 1 || dim_b == 1))] - fn verify_broadcast_compatible(dim_a: u64, dim_b: u64) -> bool { - dim_a == dim_b || dim_a == 1 || dim_b == 1 - } - - #[requires(dim_a > 0 && dim_b > 0)] - #[ensures(result >= dim_a && result >= dim_b)] - fn verify_broadcast_output_dim(dim_a: u64, dim_b: u64) -> u64 { - if dim_a > dim_b { dim_a } else { dim_b } - } - - // ── Transpose verification ── - - #[requires(rows > 0 && cols > 0)] - #[ensures(result == rows * cols)] - #[invariant(rows * cols == cols * rows)] - fn verify_transpose_element_count(rows: u64, cols: u64) -> u64 { - rows * cols - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - assert_eq!(config_contracts::validated_len(&[0]), 1); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - assert!((numeric_contracts::normalize(5.0, 0.0, 10.0) - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-core/src/format/bpe_inv_005.rs b/crates/aprender-core/src/format/bpe_inv_005.rs deleted file mode 100644 index e8c687f7f..000000000 --- a/crates/aprender-core/src/format/bpe_inv_005.rs +++ /dev/null @@ -1,315 +0,0 @@ -// SHIP-TWO-001 MODEL-2 — `tokenizer-bpe-v1` (C-TOK-BPE-001) -// algorithm-level PARTIAL discharge for INV-BPE-005. -// -// Contract: `contracts/tokenizer-bpe-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// MODEL-2 tokenizer pipeline (§26.3), AC-SHIP2-003. -// -// ## What INV-BPE-005 says -// -// description: Unicode normalization is NFC and is applied BEFORE -// BPE encoding. Running nfc(nfc(text)) yields the -// same bytes as nfc(text) (NFC is idempotent — this -// catches double-normalization bugs). -// falsifier: For a test string containing composable sequences -// (e.g. "café" composed vs "café" decomposed), -// tokenizer.encode() must produce identical token -// IDs for both. If they differ, the tokenizer is -// NOT applying NFC pre-encode. -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two byte slices (one from the composed -// input, one from the decomposed input) representing the -// post-NFC-pre-BPE form, AND optionally the result of -// nfc(nfc(text)) for double-application idempotence, Pass iff: -// -// composed_nfc == decomposed_nfc (composable equivalence) AND -// composed_nfc == double_nfc (NFC idempotence) -// -// Both equalities are byte-level. Catches three regression classes: -// - Tokenizer not applying NFC at all (composed != decomposed). -// - Tokenizer applying NFD instead of NFC (different canonical -// form; also caught by composed != decomposed). -// - Double-NFC drift (NFC implementation has a non-idempotent bug). - -/// Binary verdict for `INV-BPE-005`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum BpeInv005Verdict { - /// Composed-input NFC == decomposed-input NFC (composable - /// equivalence) AND nfc(nfc(text)) == nfc(text) (idempotence). - Pass, - /// One or more of: - /// - Either input is empty (caller error — degenerate). - /// - `composed_nfc != decomposed_nfc` (NFC not applied or - /// inconsistent canonical form). - /// - `composed_nfc != double_nfc` (NFC implementation is not - /// idempotent). - Fail, -} - -/// Pure verdict function for `INV-BPE-005`. -/// -/// Inputs: -/// - `composed_nfc`: result of `nfc(text)` where `text` was provided -/// in NFC-composed form (e.g., "café" with U+00E9). -/// - `decomposed_nfc`: result of `nfc(text)` where `text` was -/// provided in NFD-decomposed form (e.g., "café" with -/// U+0065 U+0301). -/// - `double_nfc`: result of `nfc(nfc(text))` where the inner `nfc` -/// was already applied (idempotence probe). -/// -/// Pass iff: -/// 1. All three slices are non-empty (rules out vacuous Pass on -/// empty input), -/// 2. `composed_nfc == decomposed_nfc` (composable equivalence), -/// 3. `composed_nfc == double_nfc` (idempotence on the composed -/// branch — implies idempotence on decomposed too via -/// transitivity since composed_nfc == decomposed_nfc). -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// All three NFC-equivalent — `Pass`: -/// ``` -/// use aprender::format::bpe_inv_005::{ -/// verdict_from_nfc_idempotence, BpeInv005Verdict, -/// }; -/// // "café" composed (4 bytes UTF-8 for café in NFC). -/// let nfc_form: &[u8] = "café".as_bytes(); -/// let v = verdict_from_nfc_idempotence(nfc_form, nfc_form, nfc_form); -/// assert_eq!(v, BpeInv005Verdict::Pass); -/// ``` -/// -/// Composed != decomposed (NFC not applied) — `Fail`: -/// ``` -/// use aprender::format::bpe_inv_005::{ -/// verdict_from_nfc_idempotence, BpeInv005Verdict, -/// }; -/// let composed: &[u8] = "café".as_bytes(); // U+00E9 -/// let decomposed: &[u8] = "cafe\u{0301}".as_bytes(); // 'e' + combining acute -/// let v = verdict_from_nfc_idempotence(composed, decomposed, composed); -/// assert_eq!(v, BpeInv005Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_nfc_idempotence( - composed_nfc: &[u8], - decomposed_nfc: &[u8], - double_nfc: &[u8], -) -> BpeInv005Verdict { - if composed_nfc.is_empty() || decomposed_nfc.is_empty() || double_nfc.is_empty() { - return BpeInv005Verdict::Fail; - } - if composed_nfc != decomposed_nfc { - return BpeInv005Verdict::Fail; - } - if composed_nfc != double_nfc { - return BpeInv005Verdict::Fail; - } - BpeInv005Verdict::Pass -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — all three byte slices identical. - // ------------------------------------------------------------------------- - #[test] - fn pass_all_three_identical_ascii() { - let nfc = b"hello"; - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - #[test] - fn pass_all_three_identical_cafe_composed() { - // "café" with composed é (U+00E9). 5 bytes UTF-8: c-a-f-é-(implicit). - let nfc: &[u8] = "café".as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - #[test] - fn pass_all_three_identical_cjk() { - let nfc = "中文测试".as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - #[test] - fn pass_all_three_identical_emoji() { - // Single-codepoint emoji. - let nfc = "🎉".as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - #[test] - fn pass_all_three_identical_mathematical_symbols() { - let nfc = "∑∫π√".as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — composed != decomposed (NFC not applied). - // ------------------------------------------------------------------------- - #[test] - fn fail_cafe_composed_vs_decomposed() { - // The classic regression: "café" U+00E9 vs "café" e+combining acute. - let composed: &[u8] = "café".as_bytes(); - let decomposed: &[u8] = "cafe\u{0301}".as_bytes(); - // double_nfc matches composed (the post-NFC form). - let v = verdict_from_nfc_idempotence(composed, decomposed, composed); - assert_eq!( - v, - BpeInv005Verdict::Fail, - "composed != decomposed must Fail (NFC not applied)" - ); - } - - #[test] - fn fail_completely_different_strings() { - let a = b"hello"; - let b = b"world"; - let v = verdict_from_nfc_idempotence(a, b, a); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - #[test] - fn fail_single_byte_difference() { - let a = b"hello"; - let b = b"hellp"; - let v = verdict_from_nfc_idempotence(a, b, a); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — idempotence violation (double_nfc drift). - // ------------------------------------------------------------------------- - #[test] - fn fail_double_nfc_differs() { - // composed == decomposed, but nfc(nfc) != nfc — non-idempotent - // NFC implementation. - let nfc: &[u8] = "café".as_bytes(); - let drifted: &[u8] = "cafe".as_bytes(); // dropped the é - let v = verdict_from_nfc_idempotence(nfc, nfc, drifted); - assert_eq!( - v, - BpeInv005Verdict::Fail, - "double-NFC drift must Fail (non-idempotent)" - ); - } - - #[test] - fn fail_double_nfc_off_by_one_byte() { - let nfc = b"hello"; - let drifted = b"hellp"; // last byte differs - let v = verdict_from_nfc_idempotence(nfc, nfc, drifted); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — both NFC violations and idempotence violation. - // ------------------------------------------------------------------------- - #[test] - fn fail_both_violations_combined() { - let composed: &[u8] = "café".as_bytes(); - let decomposed: &[u8] = "cafe\u{0301}".as_bytes(); - let double = b"foo"; // Completely different from composed - let v = verdict_from_nfc_idempotence(composed, decomposed, double); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — caller errors (empty inputs). - // ------------------------------------------------------------------------- - #[test] - fn fail_all_empty() { - let v = verdict_from_nfc_idempotence(&[], &[], &[]); - assert_eq!( - v, - BpeInv005Verdict::Fail, - "all-empty inputs must Fail (vacuous Pass refused)" - ); - } - - #[test] - fn fail_composed_empty() { - let v = verdict_from_nfc_idempotence(&[], b"abc", b"abc"); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - #[test] - fn fail_decomposed_empty() { - let v = verdict_from_nfc_idempotence(b"abc", &[], b"abc"); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - #[test] - fn fail_double_empty() { - let v = verdict_from_nfc_idempotence(b"abc", b"abc", &[]); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Symmetry / transitivity properties. - // ------------------------------------------------------------------------- - #[test] - fn pass_with_a_b_swapped_when_equal() { - // If composed == decomposed == double, swapping a and b - // doesn't change verdict. - let nfc = b"hello"; - let v_ab = verdict_from_nfc_idempotence(nfc, nfc, nfc); - let v_ba = verdict_from_nfc_idempotence(nfc, nfc, nfc); // Same in this trivial case - assert_eq!(v_ab, v_ba); - assert_eq!(v_ab, BpeInv005Verdict::Pass); - } - - #[test] - fn fail_three_way_distinct() { - // a != b != c, all distinct. Catches a regression that - // somehow mismatches all three. - let a = b"abc"; - let b = b"def"; - let c = b"ghi"; - let v = verdict_from_nfc_idempotence(a, b, c); - assert_eq!(v, BpeInv005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — multi-codepoint composables (e.g., Hangul). - // ------------------------------------------------------------------------- - #[test] - fn pass_hangul_precomposed_form() { - // "한" precomposed Hangul syllable U+D55C. - let nfc = "한".as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } - - #[test] - fn fail_hangul_precomposed_vs_decomposed() { - // Precomposed U+D55C vs decomposed jamo U+1112 + U+1161 + U+11AB. - let composed = "한".as_bytes(); - let decomposed = "\u{1112}\u{1161}\u{11AB}".as_bytes(); - let v = verdict_from_nfc_idempotence(composed, decomposed, composed); - assert_eq!( - v, - BpeInv005Verdict::Fail, - "Hangul precomposed != decomposed must Fail" - ); - } - - #[test] - fn pass_long_well_formed_text() { - let text = "The quick brown fox jumps over the lazy dog. \ - Café au lait. 中文测试 🎉. ∑∫π. 한국어. 1234567890"; - let nfc = text.as_bytes(); - let v = verdict_from_nfc_idempotence(nfc, nfc, nfc); - assert_eq!(v, BpeInv005Verdict::Pass); - } -} diff --git a/crates/aprender-core/src/format/cmd_safety.rs b/crates/aprender-core/src/format/cmd_safety.rs deleted file mode 100644 index ccdc24801..000000000 --- a/crates/aprender-core/src/format/cmd_safety.rs +++ /dev/null @@ -1,324 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-command-safety-v1` algorithm-level -// PARTIAL discharge for FALSIFY-CMD-SAFETY-001..004 (closes 4/4). -// -// Contract: `contracts/apr-cli-command-safety-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// All four cmd-safety verdicts share this module because they -// each have a small, simple algorithm-level reduction. Bundling -// them together (analogous to `pub_cli_002_004`, `qa_002_006`) -// avoids muda while keeping each verdict's contract ID distinct. - -// =========================================================================== -// CMD-SAFETY-001 — read-only commands do not write -// =========================================================================== - -/// Binary verdict for `FALSIFY-CMD-SAFETY-001` (read-only commands -/// create no new files in /tmp). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum CmdSafety001Verdict { - /// `files_after - files_before == 0` (no new files created). - Pass, - /// New files were created OR `files_after < files_before` - /// (counter corruption). - Fail, -} - -/// Pure verdict function for `FALSIFY-CMD-SAFETY-001`. -/// -/// Pass iff `files_after == files_before`. -#[must_use] -pub fn verdict_from_file_count_delta( - files_before: u64, - files_after: u64, -) -> CmdSafety001Verdict { - if files_before == files_after { - CmdSafety001Verdict::Pass - } else { - CmdSafety001Verdict::Fail - } -} - -// =========================================================================== -// CMD-SAFETY-002 — mutating commands need --output -// =========================================================================== - -/// Binary verdict for `FALSIFY-CMD-SAFETY-002` (apr convert without -/// -o fails with usage error containing "output" or "required"). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum CmdSafety002Verdict { - /// Stderr is non-empty AND contains `output` OR `required` - /// (case-insensitive ASCII). - Pass, - /// Empty stderr OR neither substring present (mutating cmd - /// silently accepted no output path). - Fail, -} - -/// Pure verdict function for `FALSIFY-CMD-SAFETY-002`. -/// -/// Pass iff `stderr` (lowercase) contains `output` OR `required`. -#[must_use] -pub fn verdict_from_mutating_cmd_usage_error(stderr: &[u8]) -> CmdSafety002Verdict { - if stderr.is_empty() { - return CmdSafety002Verdict::Fail; - } - let lower: Vec = stderr.iter().map(|b| b.to_ascii_lowercase()).collect(); - if contains_subseq(&lower, b"output") || contains_subseq(&lower, b"required") { - CmdSafety002Verdict::Pass - } else { - CmdSafety002Verdict::Fail - } -} - -// =========================================================================== -// CMD-SAFETY-003 — long-running commands handle SIGINT -// =========================================================================== - -/// Maximum exit code for a SIGINT-handled long-running command. -/// 130 = 128 + 2 (SIGINT signal number); the contract test -/// requires `[ $? -le 130 ]`. -pub const AC_CMD_SAFETY_003_MAX_EXIT: i32 = 130; - -/// Binary verdict for `FALSIFY-CMD-SAFETY-003` (apr tui exits -/// cleanly on SIGINT — exit code <= 130). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum CmdSafety003Verdict { - /// `0 <= exit_code <= 130` (clean exit OR SIGINT-derived). - Pass, - /// `exit_code > 130` (panic / unhandled exception) - /// OR `exit_code < 0` (out-of-domain). - Fail, -} - -/// Pure verdict function for `FALSIFY-CMD-SAFETY-003`. -/// -/// Pass iff `0 <= exit_code <= 130`. -#[must_use] -pub fn verdict_from_sigint_exit_code(exit_code: i32) -> CmdSafety003Verdict { - if (0..=AC_CMD_SAFETY_003_MAX_EXIT).contains(&exit_code) { - CmdSafety003Verdict::Pass - } else { - CmdSafety003Verdict::Fail - } -} - -// =========================================================================== -// CMD-SAFETY-004 — command classification complete -// =========================================================================== - -/// Binary verdict for `FALSIFY-CMD-SAFETY-004` (every command in -/// apr --help is classified as read_only/mutating/long_running). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum CmdSafety004Verdict { - /// Total commands > 0 AND classified count == total commands. - Pass, - /// Total == 0, classified > total (corruption), or classified - /// < total (incomplete classification). - Fail, -} - -/// Pure verdict function for `FALSIFY-CMD-SAFETY-004`. -/// -/// Pass iff `total_commands > 0 AND classified_count == total_commands`. -#[must_use] -pub fn verdict_from_command_classification( - total_commands: u64, - classified_count: u64, -) -> CmdSafety004Verdict { - if total_commands == 0 { - return CmdSafety004Verdict::Fail; - } - if classified_count == total_commands { - CmdSafety004Verdict::Pass - } else { - CmdSafety004Verdict::Fail - } -} - -// =========================================================================== -// Shared primitive -// =========================================================================== - -#[must_use] -fn contains_subseq(haystack: &[u8], needle: &[u8]) -> bool { - if needle.len() > haystack.len() { - return false; - } - haystack.windows(needle.len()).any(|w| w == needle) -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // CMD-SAFETY-001 — read-only no new files - // ------------------------------------------------------------------------- - #[test] - fn s001_pass_no_new_files() { - let v = verdict_from_file_count_delta(42, 42); - assert_eq!(v, CmdSafety001Verdict::Pass); - } - - #[test] - fn s001_pass_zero_files() { - let v = verdict_from_file_count_delta(0, 0); - assert_eq!(v, CmdSafety001Verdict::Pass); - } - - #[test] - fn s001_fail_one_new_file() { - let v = verdict_from_file_count_delta(42, 43); - assert_eq!(v, CmdSafety001Verdict::Fail); - } - - #[test] - fn s001_fail_files_decreased() { - // Counter corruption: read-only command shouldn't decrease - // file count either (cleanup of someone else's files). - let v = verdict_from_file_count_delta(42, 41); - assert_eq!(v, CmdSafety001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // CMD-SAFETY-002 — usage error contains output/required - // ------------------------------------------------------------------------- - #[test] - fn s002_pass_contains_output_lowercase() { - let v = verdict_from_mutating_cmd_usage_error(b"error: --output is required"); - assert_eq!(v, CmdSafety002Verdict::Pass); - } - - #[test] - fn s002_pass_contains_output_uppercase() { - let v = verdict_from_mutating_cmd_usage_error(b"ERROR: --OUTPUT IS REQUIRED"); - assert_eq!(v, CmdSafety002Verdict::Pass); - } - - #[test] - fn s002_pass_contains_required_only() { - let v = verdict_from_mutating_cmd_usage_error(b"missing required argument"); - assert_eq!(v, CmdSafety002Verdict::Pass); - } - - #[test] - fn s002_fail_neither_substring() { - let v = verdict_from_mutating_cmd_usage_error(b"some unrelated error"); - assert_eq!(v, CmdSafety002Verdict::Fail); - } - - #[test] - fn s002_fail_empty_stderr() { - let v = verdict_from_mutating_cmd_usage_error(&[]); - assert_eq!(v, CmdSafety002Verdict::Fail); - } - - #[test] - fn s002_pass_realistic_clap_error() { - let v = verdict_from_mutating_cmd_usage_error( - b"error: the following required arguments were not provided:\n --output ", - ); - assert_eq!(v, CmdSafety002Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // CMD-SAFETY-003 — SIGINT exit code <= 130 - // ------------------------------------------------------------------------- - #[test] - fn s003_provenance_max_exit_is_130() { - assert_eq!(AC_CMD_SAFETY_003_MAX_EXIT, 130); - } - - #[test] - fn s003_pass_clean_exit_zero() { - let v = verdict_from_sigint_exit_code(0); - assert_eq!(v, CmdSafety003Verdict::Pass); - } - - #[test] - fn s003_pass_sigint_130() { - let v = verdict_from_sigint_exit_code(130); - assert_eq!(v, CmdSafety003Verdict::Pass); - } - - #[test] - fn s003_pass_clean_error_exit_1() { - let v = verdict_from_sigint_exit_code(1); - assert_eq!(v, CmdSafety003Verdict::Pass); - } - - #[test] - fn s003_fail_panic_101_above_130() { - // Wait — 101 < 130, so this would actually Pass per - // contract `<= 130`. Document the contract semantics: - // panic exit 101 IS within the "clean" range per contract. - let v = verdict_from_sigint_exit_code(101); - assert_eq!(v, CmdSafety003Verdict::Pass); - } - - #[test] - fn s003_fail_137_sigkill() { - // SIGKILL (128 + 9 = 137) > 130 → Fail (uncatchable signal, - // means TUI didn't release resources cleanly). - let v = verdict_from_sigint_exit_code(137); - assert_eq!(v, CmdSafety003Verdict::Fail); - } - - #[test] - fn s003_fail_negative_exit() { - let v = verdict_from_sigint_exit_code(-1); - assert_eq!(v, CmdSafety003Verdict::Fail); - } - - #[test] - fn s003_fail_exit_above_255() { - let v = verdict_from_sigint_exit_code(256); - assert_eq!(v, CmdSafety003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // CMD-SAFETY-004 — every command classified - // ------------------------------------------------------------------------- - #[test] - fn s004_pass_all_58_classified() { - // Canonical 58-command apr CLI, all classified. - let v = verdict_from_command_classification(58, 58); - assert_eq!(v, CmdSafety004Verdict::Pass); - } - - #[test] - fn s004_fail_one_unclassified() { - let v = verdict_from_command_classification(58, 57); - assert_eq!(v, CmdSafety004Verdict::Fail); - } - - #[test] - fn s004_fail_zero_total() { - let v = verdict_from_command_classification(0, 0); - assert_eq!(v, CmdSafety004Verdict::Fail); - } - - #[test] - fn s004_fail_classified_exceeds_total() { - // Counter corruption. - let v = verdict_from_command_classification(58, 100); - assert_eq!(v, CmdSafety004Verdict::Fail); - } - - #[test] - fn s004_pass_smaller_cli() { - let v = verdict_from_command_classification(20, 20); - assert_eq!(v, CmdSafety004Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Shared primitive - // ------------------------------------------------------------------------- - #[test] - fn contains_subseq_basic() { - assert!(contains_subseq(b"hello world", b"world")); - assert!(!contains_subseq(b"hello world", b"xyz")); - assert!(!contains_subseq(b"short", b"longer")); - } -} diff --git a/crates/aprender-core/src/format/cov_001.rs b/crates/aprender-core/src/format/cov_001.rs deleted file mode 100644 index 646aaddaa..000000000 --- a/crates/aprender-core/src/format/cov_001.rs +++ /dev/null @@ -1,269 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-coverage-v1` algorithm-level PARTIAL -// discharge for FALSIFY-COV-001. -// -// Contract: `contracts/apr-cli-coverage-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI coverage gate). -// -// ## What FALSIFY-COV-001 says -// -// rule: coverage above 95% -// prediction: "cargo llvm-cov line coverage >= 95%" -// if_fails: "apr-cli coverage below 95%" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given a measured `line_coverage_percent` (an -// f64 in [0.0, 100.0]), Pass iff: -// -// line_coverage_percent.is_finite() AND -// 0.0 <= line_coverage_percent <= 100.0 AND -// line_coverage_percent >= AC_COV_001_MIN_PERCENT (95.0) -// -// Inclusive `>=` matches the contract's `>= 95.0` test wording. -// Domain checks (NaN, ±∞, > 100) catch coverage-tool corruption. - -/// Minimum required line coverage percentage. -/// -/// Per CLAUDE.md "Quality Standards" + spec §11: 95% line -/// coverage is the published threshold. The original 85% was -/// upgraded to 95% (per CLAUDE.md note "upgraded from 85%"). -/// Drift to 80% would silently degrade quality; drift to 99% -/// would over-tighten beyond contract. -pub const AC_COV_001_MIN_PERCENT: f64 = 95.0; - -/// Binary verdict for `FALSIFY-COV-001`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Cov001Verdict { - /// `line_coverage_percent` is in [95.0, 100.0] (inclusive). - Pass, - /// One or more of: - /// - `line_coverage_percent` is NaN or ±∞. - /// - `line_coverage_percent < 0.0` or `> 100.0` (out-of-domain). - /// - `line_coverage_percent < 95.0` (below contract floor). - Fail, -} - -/// Pure verdict function for `FALSIFY-COV-001`. -/// -/// Inputs: -/// - `line_coverage_percent`: parsed from `cargo llvm-cov report -/// --summary-only | grep TOTAL | awk '{print $10}'`. Expected -/// to be an f64 in `[0.0, 100.0]`. -/// -/// Pass iff: -/// 1. `line_coverage_percent.is_finite()`, -/// 2. `0.0 <= line_coverage_percent <= 100.0`, -/// 3. `line_coverage_percent >= 95.0`. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// 96.5% line coverage — `Pass`: -/// ``` -/// use aprender::format::cov_001::{ -/// verdict_from_line_coverage_percent, Cov001Verdict, -/// }; -/// let v = verdict_from_line_coverage_percent(96.5); -/// assert_eq!(v, Cov001Verdict::Pass); -/// ``` -/// -/// 94.99% (just below floor) — `Fail`: -/// ``` -/// use aprender::format::cov_001::{ -/// verdict_from_line_coverage_percent, Cov001Verdict, -/// }; -/// let v = verdict_from_line_coverage_percent(94.99); -/// assert_eq!(v, Cov001Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_line_coverage_percent(line_coverage_percent: f64) -> Cov001Verdict { - if !line_coverage_percent.is_finite() { - return Cov001Verdict::Fail; - } - if !(0.0..=100.0).contains(&line_coverage_percent) { - return Cov001Verdict::Fail; - } - if line_coverage_percent >= AC_COV_001_MIN_PERCENT { - Cov001Verdict::Pass - } else { - Cov001Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — 95.0 floor. - // ------------------------------------------------------------------------- - #[test] - fn provenance_min_percent_is_95() { - assert!((AC_COV_001_MIN_PERCENT - 95.0).abs() < 1e-12); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — at and above floor. - // ------------------------------------------------------------------------- - #[test] - fn pass_at_exact_floor_95_0() { - // Inclusive floor: 95.0 itself passes. - let v = verdict_from_line_coverage_percent(95.0); - assert_eq!(v, Cov001Verdict::Pass); - } - - #[test] - fn pass_at_canonical_96_35_per_claude_md() { - // CLAUDE.md says "Coverage 96.35%" — that's the canonical claim. - let v = verdict_from_line_coverage_percent(96.35); - assert_eq!(v, Cov001Verdict::Pass); - } - - #[test] - fn pass_at_perfect_100() { - let v = verdict_from_line_coverage_percent(100.0); - assert_eq!(v, Cov001Verdict::Pass); - } - - #[test] - fn pass_at_99_99() { - let v = verdict_from_line_coverage_percent(99.99); - assert_eq!(v, Cov001Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — below floor. - // ------------------------------------------------------------------------- - #[test] - fn fail_just_below_95_at_94_99() { - let v = verdict_from_line_coverage_percent(94.99); - assert_eq!( - v, - Cov001Verdict::Fail, - "94.99% must Fail (below 95% contract floor)" - ); - } - - #[test] - fn fail_at_85_old_threshold() { - // The pre-CLAUDE.md threshold; must Fail under current contract. - let v = verdict_from_line_coverage_percent(85.0); - assert_eq!( - v, - Cov001Verdict::Fail, - "85% (old threshold) must Fail under upgraded 95% contract" - ); - } - - #[test] - fn fail_at_zero() { - let v = verdict_from_line_coverage_percent(0.0); - assert_eq!(v, Cov001Verdict::Fail); - } - - #[test] - fn fail_at_50() { - let v = verdict_from_line_coverage_percent(50.0); - assert_eq!(v, Cov001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — domain violations (NaN, ±∞). - // ------------------------------------------------------------------------- - #[test] - fn fail_nan() { - let v = verdict_from_line_coverage_percent(f64::NAN); - assert_eq!(v, Cov001Verdict::Fail); - } - - #[test] - fn fail_positive_infinity() { - let v = verdict_from_line_coverage_percent(f64::INFINITY); - assert_eq!(v, Cov001Verdict::Fail); - } - - #[test] - fn fail_negative_infinity() { - let v = verdict_from_line_coverage_percent(f64::NEG_INFINITY); - assert_eq!(v, Cov001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — out-of-domain percentages. - // ------------------------------------------------------------------------- - #[test] - fn fail_negative_percent() { - let v = verdict_from_line_coverage_percent(-1.0); - assert_eq!(v, Cov001Verdict::Fail); - } - - #[test] - fn fail_above_100() { - // Coverage cannot exceed 100% by definition. - let v = verdict_from_line_coverage_percent(100.001); - assert_eq!(v, Cov001Verdict::Fail); - } - - #[test] - fn fail_huge_value() { - let v = verdict_from_line_coverage_percent(1e10); - assert_eq!(v, Cov001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Boundary sweep around 95.0 floor. - // ------------------------------------------------------------------------- - #[test] - fn coverage_sweep_around_floor() { - let probes: Vec<(f64, Cov001Verdict)> = vec![ - (0.0, Cov001Verdict::Fail), - (50.0, Cov001Verdict::Fail), - (90.0, Cov001Verdict::Fail), - (94.0, Cov001Verdict::Fail), - (94.99, Cov001Verdict::Fail), - (95.0, Cov001Verdict::Pass), // inclusive floor - (95.01, Cov001Verdict::Pass), - (96.35, Cov001Verdict::Pass), // CLAUDE.md canonical - (99.0, Cov001Verdict::Pass), - (100.0, Cov001Verdict::Pass), // inclusive ceiling - (100.001, Cov001Verdict::Fail), // domain - ]; - for (pct, expected) in probes { - let v = verdict_from_line_coverage_percent(pct); - assert_eq!(v, expected, "pct={pct} expected {expected:?}"); - } - } - - #[test] - fn fail_just_below_floor_via_ulp() { - // ULP just below 95.0 must Fail. - let just_below = f64::from_bits(95.0_f64.to_bits() - 1); - assert!(just_below < 95.0); - let v = verdict_from_line_coverage_percent(just_below); - assert_eq!( - v, - Cov001Verdict::Fail, - "ULP-below floor must Fail (strict < 95)" - ); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr-cli historical coverage values. - // ------------------------------------------------------------------------- - #[test] - fn pass_at_canonical_apr_cli_96_35_percent() { - // Per CLAUDE.md: 96.35% is the published apr-cli line coverage. - let v = verdict_from_line_coverage_percent(96.35); - assert_eq!(v, Cov001Verdict::Pass); - } - - #[test] - fn fail_when_dropped_below_floor() { - // Hypothetical regression: refactor without tests; coverage - // drops to 92%. - let v = verdict_from_line_coverage_percent(92.0); - assert_eq!(v, Cov001Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/ops_001.rs b/crates/aprender-core/src/format/ops_001.rs deleted file mode 100644 index 96bb94d72..000000000 --- a/crates/aprender-core/src/format/ops_001.rs +++ /dev/null @@ -1,241 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-001. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-001 says -// -// rule: ReadOnly commands have no side effects -// prediction: apr check does not modify any file (before/after -// hash identical) -// test: Snapshot filesystem, run apr check, diff snapshot -// if_fails: Read-only command has hidden file mutation -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two filesystem-snapshot SHA-256 digests -// (before / after running a "read-only" command), Pass iff: -// -// before is 32 bytes long AND -// after is 32 bytes long AND -// before == after (byte-identical) -// -// Mirrors `data_inv_005`'s shape (corpus_sha256 reproducibility), -// applied to filesystem snapshots. The 32-byte SHA-256 length -// pin catches hash-function drift. Byte-identical match catches -// any file mutation (mtime/size/content) that a read-only -// command should not introduce. - -/// SHA-256 digest length in bytes. -pub const AC_OPS_001_SHA256_BYTES: usize = 32; - -/// Binary verdict for `FALSIFY-OPS-001`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops001Verdict { - /// Both digests are 32 bytes long AND byte-identical. - Pass, - /// One or more of: - /// - Either digest is not 32 bytes (caller error — wrong - /// hash function, truncation, padding bug). - /// - Digests differ in any byte (read-only command mutated - /// the filesystem). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-001`. -/// -/// Inputs: -/// - `before_snapshot`: SHA-256 of the filesystem state before -/// running the command. -/// - `after_snapshot`: SHA-256 of the filesystem state after the -/// command exited. -/// -/// Pass iff: -/// 1. `before_snapshot.len() == 32`, -/// 2. `after_snapshot.len() == 32`, -/// 3. `before_snapshot == after_snapshot` (byte-identical). -/// -/// Otherwise `Fail`. -#[must_use] -pub fn verdict_from_filesystem_snapshot_pair( - before_snapshot: &[u8], - after_snapshot: &[u8], -) -> Ops001Verdict { - if before_snapshot.len() != AC_OPS_001_SHA256_BYTES { - return Ops001Verdict::Fail; - } - if after_snapshot.len() != AC_OPS_001_SHA256_BYTES { - return Ops001Verdict::Fail; - } - if before_snapshot == after_snapshot { - Ops001Verdict::Pass - } else { - Ops001Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — SHA-256 32-byte length. - // ------------------------------------------------------------------------- - #[test] - fn provenance_sha256_byte_length_is_32() { - assert_eq!(AC_OPS_001_SHA256_BYTES, 32); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — read-only commands leave filesystem unchanged. - // ------------------------------------------------------------------------- - #[test] - fn pass_identical_digests_all_zeros() { - let snapshot = [0u8; 32]; - let v = verdict_from_filesystem_snapshot_pair(&snapshot, &snapshot); - assert_eq!(v, Ops001Verdict::Pass); - } - - #[test] - fn pass_realistic_sha256_digest() { - let digest = [ - 0xe3, 0xb0, 0xc4, 0x42, 0x98, 0xfc, 0x1c, 0x14, 0x9a, 0xfb, 0xf4, 0xc8, 0x99, 0x6f, - 0xb9, 0x24, 0x27, 0xae, 0x41, 0xe4, 0x64, 0x9b, 0x93, 0x4c, 0xa4, 0x95, 0x99, 0x1b, - 0x78, 0x52, 0xb8, 0x55, - ]; - let v = verdict_from_filesystem_snapshot_pair(&digest, &digest); - assert_eq!(v, Ops001Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — single-byte mutation (read-only contract violated). - // ------------------------------------------------------------------------- - #[test] - fn fail_first_byte_differs() { - let before = [0xab_u8; 32]; - let mut after = [0xab_u8; 32]; - after[0] = 0xac; - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!( - v, - Ops001Verdict::Fail, - "single-byte mutation must Fail" - ); - } - - #[test] - fn fail_last_byte_differs() { - let before = [0xab_u8; 32]; - let mut after = [0xab_u8; 32]; - after[31] = 0xac; - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!(v, Ops001Verdict::Fail); - } - - #[test] - fn fail_one_bit_differs() { - let before = [0u8; 32]; - let mut after = [0u8; 32]; - after[0] = 0x01; - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!(v, Ops001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — wrong digest length (caller error). - // ------------------------------------------------------------------------- - #[test] - fn fail_before_too_short() { - let v = verdict_from_filesystem_snapshot_pair(&[0u8; 31], &[0u8; 32]); - assert_eq!(v, Ops001Verdict::Fail); - } - - #[test] - fn fail_after_too_short() { - let v = verdict_from_filesystem_snapshot_pair(&[0u8; 32], &[0u8; 16]); - assert_eq!(v, Ops001Verdict::Fail); - } - - #[test] - fn fail_both_empty() { - let v = verdict_from_filesystem_snapshot_pair(&[], &[]); - assert_eq!(v, Ops001Verdict::Fail); - } - - #[test] - fn fail_wrong_length_but_equal() { - // 16-byte arrays that match — must still Fail (wrong hash - // function, e.g., MD5 substituted). - let v = verdict_from_filesystem_snapshot_pair(&[0xab_u8; 16], &[0xab_u8; 16]); - assert_eq!( - v, - Ops001Verdict::Fail, - "matching but wrong-length must Fail" - ); - } - - // ------------------------------------------------------------------------- - // Section 5: Boundary sweep — every byte position differing. - // ------------------------------------------------------------------------- - #[test] - fn fail_at_every_byte_position() { - for pos in 0..32 { - let before = [0xab_u8; 32]; - let mut after = [0xab_u8; 32]; - after[pos] ^= 0x01; - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!( - v, - Ops001Verdict::Fail, - "byte position {pos} flip must Fail" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 6: Symmetry property. - // ------------------------------------------------------------------------- - #[test] - fn verdict_is_symmetric() { - let a = [0u8; 32]; - let mut b = [0u8; 32]; - b[7] = 0xff; - let ab = verdict_from_filesystem_snapshot_pair(&a, &b); - let ba = verdict_from_filesystem_snapshot_pair(&b, &a); - assert_eq!(ab, ba); - assert_eq!(ab, Ops001Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr check / inspect read-only scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_check_clean_run() { - // `apr check model.gguf` exits without mutating filesystem. - let snapshot = [0xa5_u8; 32]; - let v = verdict_from_filesystem_snapshot_pair(&snapshot, &snapshot); - assert_eq!(v, Ops001Verdict::Pass); - } - - #[test] - fn fail_apr_check_wrote_lock_file() { - // Regression: apr check accidentally wrote a .lock file or - // updated mtime on the model — filesystem hash differs. - let before = [0xa5_u8; 32]; - let mut after = [0xa5_u8; 32]; - after[15] = 0xb6; // mid-digest mutation - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!(v, Ops001Verdict::Fail); - } - - #[test] - fn fail_apr_inspect_cached_metadata_write() { - // Regression: `apr inspect` writes a metadata cache as a - // side effect — filesystem mutated. - let before = [0xa5_u8; 32]; - let after = [0xb6_u8; 32]; // completely different - let v = verdict_from_filesystem_snapshot_pair(&before, &after); - assert_eq!(v, Ops001Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/ops_002.rs b/crates/aprender-core/src/format/ops_002.rs deleted file mode 100644 index fbcfc3be5..000000000 --- a/crates/aprender-core/src/format/ops_002.rs +++ /dev/null @@ -1,323 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-002. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-002 says -// -// rule: No resource leaks after command exit -// prediction: GPU memory returns to baseline after inference error -// test: Force inference OOM, measure GPU memory after, compare -// to baseline -// if_fails: GPU memory leak on error path -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`baseline_bytes`, `post_error_bytes`, -// `tolerance_bytes`), Pass iff: -// -// baseline_bytes is in [0, AC_OPS_002_MAX_PLAUSIBLE_GPU_BYTES] AND -// post_error_bytes is in same range AND -// |post_error_bytes - baseline_bytes| <= tolerance_bytes AND -// tolerance_bytes <= AC_OPS_002_MAX_TOLERANCE_BYTES (256 MiB) -// -// Bounded-delta verdict — different from byte-equality (which -// would be too strict; CUDA driver retains some metadata pages). -// Tolerance must itself be bounded — otherwise a contributor -// could pass `tolerance = u64::MAX` and silently disable the gate. - -/// Maximum plausible GPU memory in bytes (1 TiB). -/// -/// Catches counter corruption / unsigned-overflow regressions. -/// 1 TiB exceeds any consumer or datacenter GPU. -pub const AC_OPS_002_MAX_PLAUSIBLE_GPU_BYTES: u64 = 1_024 * 1_024 * 1_024 * 1_024; // 1 TiB - -/// Maximum legal tolerance band, in bytes (256 MiB). -/// -/// CUDA driver typically retains tens of MiB of metadata after -/// freeing user allocations. 256 MiB gives generous slack while -/// still rejecting tolerance values that would mask real leaks -/// (e.g., tolerance = 8 GiB would silently accept a per-error -/// leak of an entire 7B model's weights). -pub const AC_OPS_002_MAX_TOLERANCE_BYTES: u64 = 256 * 1_024 * 1_024; // 256 MiB - -/// Binary verdict for `FALSIFY-OPS-002`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops002Verdict { - /// `|post_error - baseline| <= tolerance` AND all values are - /// within their domain bounds. - Pass, - /// One or more of: - /// - Either memory reading exceeds 1 TiB (corruption). - /// - `tolerance > 256 MiB` (caller error — would mask leaks). - /// - `|post_error - baseline| > tolerance` (memory leak). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-002`. -/// -/// Inputs: -/// - `baseline_bytes`: GPU memory occupied before the inference -/// error (typically the model's working set). -/// - `post_error_bytes`: GPU memory occupied after the failing -/// inference returned (should be back to baseline). -/// - `tolerance_bytes`: allowable absolute delta. Capped at -/// 256 MiB. -/// -/// Pass iff: -/// 1. `baseline_bytes <= 1 TiB`, -/// 2. `post_error_bytes <= 1 TiB`, -/// 3. `tolerance_bytes <= 256 MiB`, -/// 4. `|post_error_bytes - baseline_bytes| <= tolerance_bytes`. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// 6 GiB baseline, 6 GiB after error, 64 MiB tolerance — `Pass`: -/// ``` -/// use aprender::format::ops_002::{ -/// verdict_from_gpu_memory_leak_delta, Ops002Verdict, -/// }; -/// const GIB: u64 = 1_073_741_824; -/// const MIB: u64 = 1_048_576; -/// let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB, 64 * MIB); -/// assert_eq!(v, Ops002Verdict::Pass); -/// ``` -/// -/// 6 GiB baseline, 8 GiB after error (2 GiB leak), 64 MiB tolerance — -/// `Fail`: -/// ``` -/// use aprender::format::ops_002::{ -/// verdict_from_gpu_memory_leak_delta, Ops002Verdict, -/// }; -/// const GIB: u64 = 1_073_741_824; -/// const MIB: u64 = 1_048_576; -/// let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 8 * GIB, 64 * MIB); -/// assert_eq!(v, Ops002Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_gpu_memory_leak_delta( - baseline_bytes: u64, - post_error_bytes: u64, - tolerance_bytes: u64, -) -> Ops002Verdict { - if baseline_bytes > AC_OPS_002_MAX_PLAUSIBLE_GPU_BYTES { - return Ops002Verdict::Fail; - } - if post_error_bytes > AC_OPS_002_MAX_PLAUSIBLE_GPU_BYTES { - return Ops002Verdict::Fail; - } - if tolerance_bytes > AC_OPS_002_MAX_TOLERANCE_BYTES { - return Ops002Verdict::Fail; - } - let delta = post_error_bytes.abs_diff(baseline_bytes); - if delta <= tolerance_bytes { - Ops002Verdict::Pass - } else { - Ops002Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - const KIB: u64 = 1_024; - const MIB: u64 = 1_024 * KIB; - const GIB: u64 = 1_024 * MIB; - const TIB: u64 = 1_024 * GIB; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — domain caps. - // ------------------------------------------------------------------------- - #[test] - fn provenance_max_gpu_bytes_is_1_tib() { - assert_eq!(AC_OPS_002_MAX_PLAUSIBLE_GPU_BYTES, TIB); - } - - #[test] - fn provenance_max_tolerance_is_256_mib() { - assert_eq!(AC_OPS_002_MAX_TOLERANCE_BYTES, 256 * MIB); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — clean memory return at canonical scales. - // ------------------------------------------------------------------------- - #[test] - fn pass_exact_baseline_match() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_within_tolerance_above() { - // 6 GiB → 6 GiB + 32 MiB; within 64 MiB tolerance. - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB + 32 * MIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_within_tolerance_below() { - // 6 GiB → 6 GiB - 32 MiB; within 64 MiB tolerance. - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB - 32 * MIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_at_exact_tolerance_boundary() { - // delta = tolerance (inclusive). - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB + 64 * MIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_zero_baseline_zero_after() { - let v = verdict_from_gpu_memory_leak_delta(0, 0, MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_at_max_tolerance_256_mib() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB + 200 * MIB, 256 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — leak above tolerance. - // ------------------------------------------------------------------------- - #[test] - fn fail_just_above_tolerance() { - // delta = 64 MiB + 1 byte; tolerance = 64 MiB. - let v = - verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB + 64 * MIB + 1, 64 * MIB); - assert_eq!( - v, - Ops002Verdict::Fail, - "1-byte over tolerance must Fail" - ); - } - - #[test] - fn fail_2_gib_leak() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 8 * GIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Fail); - } - - #[test] - fn fail_full_model_leak() { - // Per-error leak of an entire 7B model's working set: 4 GiB. - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 10 * GIB, 64 * MIB); - assert_eq!( - v, - Ops002Verdict::Fail, - "model-sized leak must Fail (catastrophic)" - ); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — domain violations (memory readings). - // ------------------------------------------------------------------------- - #[test] - fn fail_baseline_above_1_tib() { - let v = verdict_from_gpu_memory_leak_delta(TIB + 1, 6 * GIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Fail); - } - - #[test] - fn fail_post_error_above_1_tib() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, TIB + 1, 64 * MIB); - assert_eq!(v, Ops002Verdict::Fail); - } - - #[test] - fn fail_baseline_at_u64_max() { - let v = verdict_from_gpu_memory_leak_delta(u64::MAX, 6 * GIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — caller error (tolerance too large). - // ------------------------------------------------------------------------- - #[test] - fn fail_tolerance_just_above_256_mib() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB, 256 * MIB + 1); - assert_eq!( - v, - Ops002Verdict::Fail, - "tolerance > 256 MiB must Fail (would mask leaks)" - ); - } - - #[test] - fn fail_tolerance_8_gib_would_mask_model_leak() { - // Adversarial: tolerance = 8 GiB would silently accept a - // 7B-model-sized leak. - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB, 8 * GIB); - assert_eq!(v, Ops002Verdict::Fail); - } - - #[test] - fn fail_tolerance_at_u64_max() { - let v = verdict_from_gpu_memory_leak_delta(6 * GIB, 6 * GIB, u64::MAX); - assert_eq!(v, Ops002Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Boundary sweep — delta around tolerance band. - // ------------------------------------------------------------------------- - #[test] - fn delta_sweep_around_64_mib_tolerance() { - let baseline = 6 * GIB; - let tolerance = 64 * MIB; - let probes: Vec<(u64, Ops002Verdict)> = vec![ - (baseline, Ops002Verdict::Pass), - (baseline + MIB, Ops002Verdict::Pass), - (baseline + 32 * MIB, Ops002Verdict::Pass), - (baseline + tolerance - 1, Ops002Verdict::Pass), - (baseline + tolerance, Ops002Verdict::Pass), // inclusive - (baseline + tolerance + 1, Ops002Verdict::Fail), - (baseline + 100 * MIB, Ops002Verdict::Fail), - (baseline + 1 * GIB, Ops002Verdict::Fail), - ]; - for (post, expected) in probes { - let v = verdict_from_gpu_memory_leak_delta(baseline, post, tolerance); - assert_eq!( - v, expected, - "post={post} expected {expected:?} (baseline=6 GiB, tol=64 MiB)" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — typical RTX 4090 / A100 baselines. - // ------------------------------------------------------------------------- - #[test] - fn pass_rtx_4090_clean_inference_error() { - // RTX 4090 24 GiB; Qwen2.5-7B Q4_K = ~5 GiB; 64 MiB tolerance - // covers driver metadata. - let v = verdict_from_gpu_memory_leak_delta(5 * GIB, 5 * GIB + 12 * MIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn pass_a100_80gb_clean_inference_error() { - // A100 80 GiB; Qwen2.5-72B Q4_K = ~38 GiB. - let v = verdict_from_gpu_memory_leak_delta(38 * GIB, 38 * GIB + 8 * MIB, 64 * MIB); - assert_eq!(v, Ops002Verdict::Pass); - } - - #[test] - fn fail_per_request_kv_cache_leak() { - // Realistic regression: KV cache for a failed request not - // freed; each failure adds ~256 MiB. - let v = - verdict_from_gpu_memory_leak_delta(5 * GIB, 5 * GIB + 256 * MIB + MIB, 64 * MIB); - assert_eq!( - v, - Ops002Verdict::Fail, - "KV cache leak must Fail" - ); - } -} diff --git a/crates/aprender-core/src/format/ops_003.rs b/crates/aprender-core/src/format/ops_003.rs deleted file mode 100644 index 8972943f0..000000000 --- a/crates/aprender-core/src/format/ops_003.rs +++ /dev/null @@ -1,258 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-003. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-003 says -// -// rule: Greedy decoding is deterministic -// prediction: Two runs with temperature=0 produce identical output -// test: Run same prompt twice with temperature=0, assert output equality -// if_fails: Non-deterministic codepath in greedy sampling -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two stdout byte slices from -// `apr run --temperature 0 ...` invoked twice with the same -// prompt, Pass iff: -// -// run_a is non-empty AND -// run_b is non-empty AND -// run_a == run_b (byte-identical) -// -// Same shape as `bpe_inv_006` (encode determinism), applied to -// the inference output instead of token IDs. Catches: -// - HashMap iteration order in argmax-tiebreak. -// - Race condition in multi-threaded sampling. -// - Stochastic codepath that ignores temperature=0. - -/// Binary verdict for `FALSIFY-OPS-003`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops003Verdict { - /// Both outputs are non-empty AND byte-identical. - Pass, - /// One or more of: - /// - Either output is empty (caller error — `apr run` silent - /// regression). - /// - Outputs differ in any byte (non-deterministic codepath - /// in greedy sampling). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-003`. -/// -/// Inputs: -/// - `run_a`: stdout bytes from first `apr run --temperature 0` -/// invocation. -/// - `run_b`: stdout bytes from second `apr run --temperature 0` -/// invocation with the same prompt. -/// -/// Pass iff: -/// 1. `!run_a.is_empty()`, -/// 2. `!run_b.is_empty()`, -/// 3. `run_a == run_b` (byte-identical). -/// -/// Otherwise `Fail`. -#[must_use] -pub fn verdict_from_greedy_decoding_pair( - run_a: &[u8], - run_b: &[u8], -) -> Ops003Verdict { - if run_a.is_empty() || run_b.is_empty() { - return Ops003Verdict::Fail; - } - if run_a == run_b { - Ops003Verdict::Pass - } else { - Ops003Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — identical greedy outputs. - // ------------------------------------------------------------------------- - #[test] - fn pass_short_identical_output() { - let a = b"4\n"; - let b = b"4\n"; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!(v, Ops003Verdict::Pass); - } - - #[test] - fn pass_realistic_2_plus_2_response() { - // Canonical apr run --temperature 0 'What is 2+2?' output. - let response = b"4"; - let v = verdict_from_greedy_decoding_pair(response, response); - assert_eq!(v, Ops003Verdict::Pass); - } - - #[test] - fn pass_long_identical_response() { - let long = vec![b'x'; 10_000]; - let v = verdict_from_greedy_decoding_pair(&long, &long); - assert_eq!(v, Ops003Verdict::Pass); - } - - #[test] - fn pass_with_special_chars() { - let a = b"```python\nprint('hello')\n```"; - let v = verdict_from_greedy_decoding_pair(a, a); - assert_eq!(v, Ops003Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — single-byte drift (non-determinism). - // ------------------------------------------------------------------------- - #[test] - fn fail_first_byte_differs() { - let a = b"4\n"; - let b = b"5\n"; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!( - v, - Ops003Verdict::Fail, - "single-byte drift must Fail (non-determinism)" - ); - } - - #[test] - fn fail_last_byte_differs() { - let a = b"def foo():\n pass\n"; - let b = b"def foo():\n pass "; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!(v, Ops003Verdict::Fail); - } - - #[test] - fn fail_middle_byte_differs() { - let a = b"hello world"; - let b = b"hellp world"; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!(v, Ops003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — length mismatch. - // ------------------------------------------------------------------------- - #[test] - fn fail_a_longer() { - let a = b"hello world"; - let b = b"hello"; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!(v, Ops003Verdict::Fail); - } - - #[test] - fn fail_b_longer() { - let a = b"hello"; - let b = b"hello world"; - let v = verdict_from_greedy_decoding_pair(a, b); - assert_eq!(v, Ops003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — empty inputs. - // ------------------------------------------------------------------------- - #[test] - fn fail_a_empty() { - let v = verdict_from_greedy_decoding_pair(&[], b"output"); - assert_eq!(v, Ops003Verdict::Fail); - } - - #[test] - fn fail_b_empty() { - let v = verdict_from_greedy_decoding_pair(b"output", &[]); - assert_eq!(v, Ops003Verdict::Fail); - } - - #[test] - fn fail_both_empty() { - let v = verdict_from_greedy_decoding_pair(&[], &[]); - assert_eq!( - v, - Ops003Verdict::Fail, - "both empty must Fail (vacuous Pass refused)" - ); - } - - // ------------------------------------------------------------------------- - // Section 5: Symmetry property. - // ------------------------------------------------------------------------- - #[test] - fn verdict_is_symmetric_pass() { - let same = b"identical"; - let v_ab = verdict_from_greedy_decoding_pair(same, same); - let v_ba = verdict_from_greedy_decoding_pair(same, same); - assert_eq!(v_ab, v_ba); - assert_eq!(v_ab, Ops003Verdict::Pass); - } - - #[test] - fn verdict_is_symmetric_fail() { - let a = b"foo"; - let b = b"bar"; - let v_ab = verdict_from_greedy_decoding_pair(a, b); - let v_ba = verdict_from_greedy_decoding_pair(b, a); - assert_eq!(v_ab, v_ba); - assert_eq!(v_ab, Ops003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Position sweep — drift at every position must Fail. - // ------------------------------------------------------------------------- - #[test] - fn fail_at_every_drift_position() { - let baseline = b"the quick brown fox jumps over the lazy dog"; - for pos in 0..baseline.len() { - let mut drift = baseline.to_vec(); - drift[pos] ^= 0x01; - let v = verdict_from_greedy_decoding_pair(baseline, &drift); - assert_eq!( - v, - Ops003Verdict::Fail, - "drift at position {pos} must Fail" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr run scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_run_arithmetic_same_answer() { - // Run twice with --temperature 0; both produce "4". - let response = b"4"; - let v = verdict_from_greedy_decoding_pair(response, response); - assert_eq!(v, Ops003Verdict::Pass); - } - - #[test] - fn fail_apr_run_hashmap_tiebreak_drift() { - // Realistic regression: argmax tiebreak picks different - // token id between runs due to HashMap iteration order. - let run_a = b"The answer is 4"; - let run_b = b"The answer is 5"; // tiebreak chose differently - let v = verdict_from_greedy_decoding_pair(run_a, run_b); - assert_eq!( - v, - Ops003Verdict::Fail, - "argmax tiebreak drift must Fail" - ); - } - - #[test] - fn fail_apr_run_floating_point_associativity() { - // Realistic regression: parallel logit reduction order - // varies between runs, producing different argmax. - let run_a = b"def factorial(n):\n return 1 if n == 0 else n * factorial(n - 1)"; - let run_b = b"def factorial(n):\n return 1 if n <= 0 else n * factorial(n - 1)"; - let v = verdict_from_greedy_decoding_pair(run_a, run_b); - assert_eq!(v, Ops003Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/ops_004.rs b/crates/aprender-core/src/format/ops_004.rs deleted file mode 100644 index 050b5a55a..000000000 --- a/crates/aprender-core/src/format/ops_004.rs +++ /dev/null @@ -1,286 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-004. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-004 says -// -// rule: Progress percentage monotonically increasing -// prediction: Progress never decreases during model loading -// test: Capture all progress events during pull, verify monotonicity -// if_fails: Progress percentage regression (confuses users) -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given a sequence of progress percentages observed -// during a model pull/load operation, Pass iff: -// -// sequence is non-empty AND -// every value is finite AND in [0.0, 100.0] AND -// for every adjacent pair (a, b): a <= b (monotonically -// non-decreasing) -// -// Non-strict `<=` allows the same value to be emitted twice in a -// row (typical with throttled progress reporting). Strict `<` would -// reject normal progress streams. - -/// Binary verdict for `FALSIFY-OPS-004`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops004Verdict { - /// Sequence is non-empty, all values are finite + in - /// `[0.0, 100.0]`, AND every adjacent pair is non-decreasing. - Pass, - /// One or more of: - /// - `progress_sequence.is_empty()` (caller error — no - /// progress events captured). - /// - Any value is NaN, ±∞, or outside `[0.0, 100.0]`. - /// - Any adjacent pair `(a, b)` has `a > b` (progress - /// regressed). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-004`. -/// -/// Inputs: -/// - `progress_sequence`: percentages (in [0, 100]) emitted by -/// the apr puller in chronological order. -/// -/// Pass iff: -/// 1. `!progress_sequence.is_empty()`, -/// 2. Every value is finite, -/// 3. Every value is in `[0.0, 100.0]`, -/// 4. For every `i > 0`: `progress_sequence[i-1] <= -/// progress_sequence[i]`. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// Strictly increasing — `Pass`: -/// ``` -/// use aprender::format::ops_004::{ -/// verdict_from_progress_monotonicity, Ops004Verdict, -/// }; -/// let v = verdict_from_progress_monotonicity(&[0.0, 25.0, 50.0, 75.0, 100.0]); -/// assert_eq!(v, Ops004Verdict::Pass); -/// ``` -/// -/// Regression at index 2 — `Fail`: -/// ``` -/// use aprender::format::ops_004::{ -/// verdict_from_progress_monotonicity, Ops004Verdict, -/// }; -/// let v = verdict_from_progress_monotonicity(&[0.0, 50.0, 30.0, 100.0]); -/// assert_eq!(v, Ops004Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_progress_monotonicity(progress_sequence: &[f64]) -> Ops004Verdict { - if progress_sequence.is_empty() { - return Ops004Verdict::Fail; - } - for &p in progress_sequence { - if !p.is_finite() { - return Ops004Verdict::Fail; - } - if !(0.0..=100.0).contains(&p) { - return Ops004Verdict::Fail; - } - } - for w in progress_sequence.windows(2) { - if w[0] > w[1] { - return Ops004Verdict::Fail; - } - } - Ops004Verdict::Pass -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — typical clean progress sequences. - // ------------------------------------------------------------------------- - #[test] - fn pass_strictly_increasing() { - let v = verdict_from_progress_monotonicity(&[0.0, 25.0, 50.0, 75.0, 100.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_with_repeats() { - // Throttled emission: 25.0 → 25.0 → 50.0 (same-value adjacent - // pairs are allowed under non-strict <=). - let v = verdict_from_progress_monotonicity(&[0.0, 25.0, 25.0, 50.0, 100.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_single_event() { - // Single 0.0 (or 100.0) sequence is trivially monotonic. - let v = verdict_from_progress_monotonicity(&[0.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_starts_at_nonzero() { - // Resume scenario: progress starts at 50% (cached prefix). - let v = verdict_from_progress_monotonicity(&[50.0, 75.0, 100.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_realistic_dense_progress() { - // Realistic 1% emission cadence. - let dense: Vec = (0..=100).map(f64::from).collect(); - let v = verdict_from_progress_monotonicity(&dense); - assert_eq!(v, Ops004Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — progress regression. - // ------------------------------------------------------------------------- - #[test] - fn fail_simple_regression() { - let v = verdict_from_progress_monotonicity(&[0.0, 50.0, 30.0, 100.0]); - assert_eq!( - v, - Ops004Verdict::Fail, - "regression at index 2 must Fail" - ); - } - - #[test] - fn fail_drop_to_zero() { - // Progress reset mid-stream. - let v = verdict_from_progress_monotonicity(&[0.0, 50.0, 0.0, 100.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_one_ulp_regression() { - let v = verdict_from_progress_monotonicity(&[ - 50.0, - f64::from_bits(50.0_f64.to_bits() - 1), - ]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_regression_at_end() { - // 99 → 50 at the last pair. - let v = verdict_from_progress_monotonicity(&[0.0, 25.0, 50.0, 99.0, 50.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — empty sequence (caller error). - // ------------------------------------------------------------------------- - #[test] - fn fail_empty_sequence() { - let v = verdict_from_progress_monotonicity(&[]); - assert_eq!( - v, - Ops004Verdict::Fail, - "empty sequence must Fail (no progress observed)" - ); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — domain violations (NaN, ±∞). - // ------------------------------------------------------------------------- - #[test] - fn fail_nan_in_sequence() { - let v = verdict_from_progress_monotonicity(&[0.0, 25.0, f64::NAN, 50.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_positive_infinity() { - let v = verdict_from_progress_monotonicity(&[0.0, f64::INFINITY, 100.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_negative_infinity() { - let v = verdict_from_progress_monotonicity(&[f64::NEG_INFINITY, 50.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — out-of-range values. - // ------------------------------------------------------------------------- - #[test] - fn fail_negative_percentage() { - let v = verdict_from_progress_monotonicity(&[-1.0, 50.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_above_100_percent() { - let v = verdict_from_progress_monotonicity(&[0.0, 50.0, 101.0]); - assert_eq!(v, Ops004Verdict::Fail); - } - - #[test] - fn fail_huge_value() { - let v = verdict_from_progress_monotonicity(&[0.0, 1e10]); - assert_eq!(v, Ops004Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Boundary cases — at exactly 0.0 and 100.0. - // ------------------------------------------------------------------------- - #[test] - fn pass_at_floor_0_percent() { - let v = verdict_from_progress_monotonicity(&[0.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_at_ceiling_100_percent() { - let v = verdict_from_progress_monotonicity(&[100.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn pass_full_range_two_events() { - let v = verdict_from_progress_monotonicity(&[0.0, 100.0]); - assert_eq!(v, Ops004Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr pull dataset progress scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_pull_clean_stream() { - // 1KB granularity progress on 1MB file. - let mut events = Vec::new(); - for i in 0..=1024 { - events.push(f64::from(i) * 100.0 / 1024.0); - } - let v = verdict_from_progress_monotonicity(&events); - assert_eq!(v, Ops004Verdict::Pass); - } - - #[test] - fn fail_apr_pull_retry_resets_progress() { - // Realistic regression: HF endpoint 503; puller retries - // and emits progress=0 mid-stream. - let v = verdict_from_progress_monotonicity(&[0.0, 30.0, 60.0, 0.0, 30.0, 100.0]); - assert_eq!( - v, - Ops004Verdict::Fail, - "retry reset must Fail (confuses users)" - ); - } - - #[test] - fn fail_apr_pull_concurrent_writer_overlap() { - // Multi-thread regression: progress events arrive out of - // order due to lockless emission. - let v = verdict_from_progress_monotonicity(&[0.0, 25.0, 50.0, 40.0, 75.0]); - assert_eq!(v, Ops004Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/ops_005.rs b/crates/aprender-core/src/format/ops_005.rs deleted file mode 100644 index 2321ef13a..000000000 --- a/crates/aprender-core/src/format/ops_005.rs +++ /dev/null @@ -1,199 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-005. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-005 says -// -// rule: Concurrent inference results independent -// prediction: Result of request A is identical whether B runs -// concurrently or not -// test: Run request A alone, then with concurrent B, diff results -// if_fails: KV cache contamination between concurrent requests -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two stdout byte slices for the same prompt -// — one captured running alone, one captured with a concurrent -// peer — Pass iff: -// -// alone_output is non-empty AND -// concurrent_output is non-empty AND -// alone_output == concurrent_output (byte-identical) -// -// Same shape as `bpe_inv_006` (encode determinism) and `ops_003` -// (greedy determinism), applied to concurrent-vs-isolated -// inference. Catches KV cache contamination, batch-id leakage, -// global-mutex-violation regressions. - -/// Binary verdict for `FALSIFY-OPS-005`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops005Verdict { - /// Both outputs are non-empty AND byte-identical. - Pass, - /// One or more of: - /// - Either output is empty (caller error — `apr run` silent - /// regression). - /// - Outputs differ in any byte (KV cache contamination, - /// batch-id leakage, or other concurrent-state corruption). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-005`. -/// -/// Inputs: -/// - `alone_output`: stdout from `apr run` invoked alone. -/// - `concurrent_output`: stdout from `apr run` invoked with the -/// same prompt while a peer request is in flight. -/// -/// Pass iff both non-empty AND byte-identical. -#[must_use] -pub fn verdict_from_concurrent_isolation( - alone_output: &[u8], - concurrent_output: &[u8], -) -> Ops005Verdict { - if alone_output.is_empty() || concurrent_output.is_empty() { - return Ops005Verdict::Fail; - } - if alone_output == concurrent_output { - Ops005Verdict::Pass - } else { - Ops005Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — concurrent-isolated agreement. - // ------------------------------------------------------------------------- - #[test] - fn pass_identical_outputs() { - let same = b"4"; - let v = verdict_from_concurrent_isolation(same, same); - assert_eq!(v, Ops005Verdict::Pass); - } - - #[test] - fn pass_long_identical_response() { - let long = vec![b'x'; 5000]; - let v = verdict_from_concurrent_isolation(&long, &long); - assert_eq!(v, Ops005Verdict::Pass); - } - - #[test] - fn pass_realistic_apr_run_arithmetic() { - let response = b"The answer is 4."; - let v = verdict_from_concurrent_isolation(response, response); - assert_eq!(v, Ops005Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — contamination (single-byte drift). - // ------------------------------------------------------------------------- - #[test] - fn fail_first_byte_differs() { - let alone = b"4"; - let concurrent = b"5"; - let v = verdict_from_concurrent_isolation(alone, concurrent); - assert_eq!( - v, - Ops005Verdict::Fail, - "concurrent contamination must Fail" - ); - } - - #[test] - fn fail_kv_cache_leakage_drift() { - // Realistic regression: KV cache from peer request leaked - // into A's tail tokens. - let alone = b"def factorial(n):\n return 1 if n == 0 else n * factorial(n - 1)"; - let concurrent = b"def factorial(n):\n return 1 if n <= 0 else n * factorial(n - 1)"; - let v = verdict_from_concurrent_isolation(alone, concurrent); - assert_eq!(v, Ops005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — empty inputs. - // ------------------------------------------------------------------------- - #[test] - fn fail_alone_empty() { - let v = verdict_from_concurrent_isolation(&[], b"output"); - assert_eq!(v, Ops005Verdict::Fail); - } - - #[test] - fn fail_concurrent_empty() { - let v = verdict_from_concurrent_isolation(b"output", &[]); - assert_eq!(v, Ops005Verdict::Fail); - } - - #[test] - fn fail_both_empty() { - let v = verdict_from_concurrent_isolation(&[], &[]); - assert_eq!(v, Ops005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Symmetry property. - // ------------------------------------------------------------------------- - #[test] - fn verdict_is_symmetric_pass() { - let same = b"identical"; - let v_ab = verdict_from_concurrent_isolation(same, same); - let v_ba = verdict_from_concurrent_isolation(same, same); - assert_eq!(v_ab, v_ba); - assert_eq!(v_ab, Ops005Verdict::Pass); - } - - #[test] - fn verdict_is_symmetric_fail() { - let a = b"foo"; - let b = b"bar"; - let v_ab = verdict_from_concurrent_isolation(a, b); - let v_ba = verdict_from_concurrent_isolation(b, a); - assert_eq!(v_ab, v_ba); - assert_eq!(v_ab, Ops005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Length mismatch. - // ------------------------------------------------------------------------- - #[test] - fn fail_alone_longer() { - let v = verdict_from_concurrent_isolation(b"longer text", b"short"); - assert_eq!(v, Ops005Verdict::Fail); - } - - #[test] - fn fail_concurrent_longer() { - let v = verdict_from_concurrent_isolation(b"short", b"longer text"); - assert_eq!(v, Ops005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Realistic — concurrent-inference regression classes. - // ------------------------------------------------------------------------- - #[test] - fn fail_batch_id_leakage() { - // Realistic: batch_id confusion causes A's tokens to come - // from B's logits. - let alone = b"hello world"; - let concurrent = b"hello WORLD"; - let v = verdict_from_concurrent_isolation(alone, concurrent); - assert_eq!(v, Ops005Verdict::Fail); - } - - #[test] - fn fail_global_mutex_release_during_softmax() { - // Realistic: mutex released mid-softmax allows peer to - // overwrite logits buffer. - let alone = b"output A"; - let concurrent = b"output X"; - let v = verdict_from_concurrent_isolation(alone, concurrent); - assert_eq!(v, Ops005Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/ops_006.rs b/crates/aprender-core/src/format/ops_006.rs deleted file mode 100644 index e263facd0..000000000 --- a/crates/aprender-core/src/format/ops_006.rs +++ /dev/null @@ -1,217 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-006. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-006 says -// -// rule: Tokenizer encode/decode roundtrip -// prediction: Random UTF-8 strings survive tokenize/detokenize -// roundtrip -// test: Generate 1000 random UTF-8 strings, encode then decode, -// assert equality -// if_fails: Tokenizer drops or corrupts characters -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`docs_scanned`, `roundtrip_failures`), -// Pass iff: -// -// docs_scanned >= AC_OPS_006_REQUIRED_DOCS (1000) AND -// roundtrip_failures == 0 AND -// roundtrip_failures <= docs_scanned -// -// Same shape as `bpe_inv_003` (BPE round-trip) but with a smaller -// (1000-doc) sample size and broader scope (any UTF-8 input, -// not just held-out corpus). - -/// Required minimum number of random UTF-8 strings to scan. -/// -/// Per contract `OPS-006`: "Generate 1000 random UTF-8 strings". -/// Drift to 100 would lose statistical power for rare-codepoint -/// regressions; drift to 10000 would over-tax smoke runs. -pub const AC_OPS_006_REQUIRED_DOCS: u64 = 1_000; - -/// Binary verdict for `FALSIFY-OPS-006`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops006Verdict { - /// Sample-scan visited >= 1000 random UTF-8 strings AND zero - /// round-trip failures observed. - Pass, - /// One or more of: - /// - `docs_scanned < 1000` (insufficient sample size). - /// - `roundtrip_failures > 0` (tokenizer dropped or corrupted - /// characters; one is enough). - /// - `roundtrip_failures > docs_scanned` (counter corruption). - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-006`. -/// -/// Inputs: -/// - `docs_scanned`: number of random UTF-8 strings the -/// roundtrip-test harness evaluated. -/// - `roundtrip_failures`: number of those where -/// `decode(encode(s)) != s`. -/// -/// Pass iff: -/// 1. `docs_scanned >= 1000`, -/// 2. `roundtrip_failures == 0`, -/// 3. `roundtrip_failures <= docs_scanned`. -/// -/// Otherwise `Fail`. -#[must_use] -pub fn verdict_from_random_roundtrip_scan( - docs_scanned: u64, - roundtrip_failures: u64, -) -> Ops006Verdict { - if docs_scanned < AC_OPS_006_REQUIRED_DOCS { - return Ops006Verdict::Fail; - } - if roundtrip_failures > docs_scanned { - return Ops006Verdict::Fail; - } - if roundtrip_failures == 0 { - Ops006Verdict::Pass - } else { - Ops006Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — 1000-doc sample floor. - // ------------------------------------------------------------------------- - #[test] - fn provenance_required_docs_is_1000() { - assert_eq!(AC_OPS_006_REQUIRED_DOCS, 1_000); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — clean tokenizer, sufficient sample. - // ------------------------------------------------------------------------- - #[test] - fn pass_at_exact_floor() { - let v = verdict_from_random_roundtrip_scan(1_000, 0); - assert_eq!(v, Ops006Verdict::Pass); - } - - #[test] - fn pass_above_floor() { - let v = verdict_from_random_roundtrip_scan(10_000, 0); - assert_eq!(v, Ops006Verdict::Pass); - } - - #[test] - fn pass_at_huge_sample() { - let v = verdict_from_random_roundtrip_scan(1_000_000, 0); - assert_eq!(v, Ops006Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — roundtrip failures (zero-tolerance). - // ------------------------------------------------------------------------- - #[test] - fn fail_one_failure_in_1000() { - let v = verdict_from_random_roundtrip_scan(1_000, 1); - assert_eq!( - v, - Ops006Verdict::Fail, - "one roundtrip failure must Fail (no tolerance)" - ); - } - - #[test] - fn fail_handful_of_failures() { - let v = verdict_from_random_roundtrip_scan(1_000, 7); - assert_eq!(v, Ops006Verdict::Fail); - } - - #[test] - fn fail_one_in_million() { - let v = verdict_from_random_roundtrip_scan(1_000_000, 1); - assert_eq!(v, Ops006Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — sample size too small. - // ------------------------------------------------------------------------- - #[test] - fn fail_zero_docs() { - let v = verdict_from_random_roundtrip_scan(0, 0); - assert_eq!(v, Ops006Verdict::Fail); - } - - #[test] - fn fail_just_below_floor() { - let v = verdict_from_random_roundtrip_scan(999, 0); - assert_eq!(v, Ops006Verdict::Fail); - } - - #[test] - fn fail_one_doc() { - let v = verdict_from_random_roundtrip_scan(1, 0); - assert_eq!(v, Ops006Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Counter / partition violations. - // ------------------------------------------------------------------------- - #[test] - fn fail_failures_exceed_docs() { - let v = verdict_from_random_roundtrip_scan(1_000, 1_001); - assert_eq!(v, Ops006Verdict::Fail); - } - - #[test] - fn fail_huge_failures_with_smaller_scan() { - let v = verdict_from_random_roundtrip_scan(1_000, u64::MAX); - assert_eq!(v, Ops006Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Boundary sweep. - // ------------------------------------------------------------------------- - #[test] - fn failure_count_sweep_at_1000_scan() { - let scanned = 1_000_u64; - let probes: Vec<(u64, Ops006Verdict)> = vec![ - (0, Ops006Verdict::Pass), - (1, Ops006Verdict::Fail), - (10, Ops006Verdict::Fail), - (500, Ops006Verdict::Fail), - (999, Ops006Verdict::Fail), - (1_000, Ops006Verdict::Fail), - (1_001, Ops006Verdict::Fail), // partition - ]; - for (failures, expected) in probes { - let v = verdict_from_random_roundtrip_scan(scanned, failures); - assert_eq!( - v, expected, - "scanned={scanned} failures={failures} expected {expected:?}" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Domain — zero-tolerance property. - // ------------------------------------------------------------------------- - #[test] - fn pass_iff_failures_is_exactly_zero() { - for scanned in [1_000_u64, 5_000, 10_000, 100_000] { - let v_pass = verdict_from_random_roundtrip_scan(scanned, 0); - assert_eq!(v_pass, Ops006Verdict::Pass, "scanned={scanned}"); - - let v_fail = verdict_from_random_roundtrip_scan(scanned, 1); - assert_eq!( - v_fail, - Ops006Verdict::Fail, - "scanned={scanned} with one failure" - ); - } - } -} diff --git a/crates/aprender-core/src/format/ops_007.rs b/crates/aprender-core/src/format/ops_007.rs deleted file mode 100644 index 70f45befd..000000000 --- a/crates/aprender-core/src/format/ops_007.rs +++ /dev/null @@ -1,283 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-operations-v1` algorithm-level PARTIAL -// discharge for FALSIFY-OPS-007. -// -// Contract: `contracts/apr-cli-operations-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md`. -// -// ## What FALSIFY-OPS-007 says -// -// rule: Token count bounded by input length -// prediction: No input produces more than 4x tokens (BPE worst case) -// test: Encode adversarial strings (single-byte tokens), verify -// count <= 4 * len -// if_fails: Token explosion — unbounded memory usage -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`input_byte_len`, `token_count`), Pass iff: -// -// input_byte_len > 0 AND -// token_count <= AC_OPS_007_MAX_RATIO (4) * input_byte_len -// -// Linear-bound verdict via `checked_mul` to prevent overflow at -// adversarial input sizes near `u64::MAX`. Inclusive `<=` matches -// the contract's `<= 4 * len` test wording. - -/// Maximum tokens-per-input-byte ratio for BPE worst case. -/// -/// Per contract: BPE byte-level fallback emits at most ~4 tokens -/// per input byte in the worst case (UTF-8 4-byte sequences split -/// into 4 byte-fallback tokens). 4× cap is the published BPE -/// worst-case bound. -/// -/// Drift to 8× would mask token-explosion bugs (unbounded merge -/// expansion); drift to 2× would over-tighten and reject -/// pathological-but-valid CJK / emoji inputs. -pub const AC_OPS_007_MAX_RATIO: u64 = 4; - -/// Binary verdict for `FALSIFY-OPS-007`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Ops007Verdict { - /// `input_byte_len > 0` AND `token_count <= 4 * input_byte_len`. - Pass, - /// One or more of: - /// - `input_byte_len == 0` (caller error — empty input). - /// - `token_count > 4 * input_byte_len` (token explosion). - /// - Multiplication overflow on `4 * input_byte_len`. - Fail, -} - -/// Pure verdict function for `FALSIFY-OPS-007`. -/// -/// Inputs: -/// - `input_byte_len`: length of the input string in bytes (UTF-8). -/// - `token_count`: number of tokens produced by tokenizing the -/// input. -/// -/// Pass iff: -/// 1. `input_byte_len > 0`, -/// 2. `token_count <= input_byte_len.checked_mul(4)` (overflow → Fail). -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// 100-byte input → 50 tokens (well within 4× cap) — `Pass`: -/// ``` -/// use aprender::format::ops_007::{ -/// verdict_from_token_count_bound, Ops007Verdict, -/// }; -/// let v = verdict_from_token_count_bound(100, 50); -/// assert_eq!(v, Ops007Verdict::Pass); -/// ``` -/// -/// 100-byte input → 401 tokens (exceeds 4× cap = 400) — `Fail`: -/// ``` -/// use aprender::format::ops_007::{ -/// verdict_from_token_count_bound, Ops007Verdict, -/// }; -/// let v = verdict_from_token_count_bound(100, 401); -/// assert_eq!(v, Ops007Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_token_count_bound( - input_byte_len: u64, - token_count: u64, -) -> Ops007Verdict { - if input_byte_len == 0 { - return Ops007Verdict::Fail; - } - let max_tokens = match input_byte_len.checked_mul(AC_OPS_007_MAX_RATIO) { - Some(v) => v, - None => return Ops007Verdict::Fail, - }; - if token_count <= max_tokens { - Ops007Verdict::Pass - } else { - Ops007Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — 4× ratio. - // ------------------------------------------------------------------------- - #[test] - fn provenance_max_ratio_is_4() { - assert_eq!(AC_OPS_007_MAX_RATIO, 4); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — typical compression ratios. - // ------------------------------------------------------------------------- - #[test] - fn pass_typical_compression_ratio() { - // BPE typically compresses ~3:1 on English text — 100 bytes → ~30 tokens. - let v = verdict_from_token_count_bound(100, 30); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn pass_at_exact_4x_cap() { - // Worst case: every byte → 4 tokens. - let v = verdict_from_token_count_bound(100, 400); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn pass_one_byte_one_token() { - let v = verdict_from_token_count_bound(1, 1); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn pass_realistic_apr_run_input() { - // 50-byte prompt → 12 tokens (typical English compression). - let v = verdict_from_token_count_bound(50, 12); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn pass_huge_clean_input() { - let v = verdict_from_token_count_bound(1_000_000, 100_000); - assert_eq!(v, Ops007Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — token explosion. - // ------------------------------------------------------------------------- - #[test] - fn fail_just_above_4x_cap() { - let v = verdict_from_token_count_bound(100, 401); - assert_eq!( - v, - Ops007Verdict::Fail, - "+1 token over cap must Fail" - ); - } - - #[test] - fn fail_5x_token_explosion() { - let v = verdict_from_token_count_bound(100, 500); - assert_eq!(v, Ops007Verdict::Fail); - } - - #[test] - fn fail_10x_token_explosion() { - let v = verdict_from_token_count_bound(100, 1_000); - assert_eq!(v, Ops007Verdict::Fail); - } - - #[test] - fn fail_unbounded_memory_attack() { - // Adversarial input: 10-byte string produces 100k tokens. - let v = verdict_from_token_count_bound(10, 100_000); - assert_eq!( - v, - Ops007Verdict::Fail, - "DoS-class token explosion must Fail" - ); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — empty input (caller error). - // ------------------------------------------------------------------------- - #[test] - fn fail_zero_input_zero_tokens() { - // Empty input is degenerate — refuse. - let v = verdict_from_token_count_bound(0, 0); - assert_eq!( - v, - Ops007Verdict::Fail, - "zero-byte input must Fail (vacuous Pass refused)" - ); - } - - #[test] - fn fail_zero_input_with_tokens() { - // Counter corruption: 0 bytes but 5 tokens. - let v = verdict_from_token_count_bound(0, 5); - assert_eq!(v, Ops007Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Overflow protection — checked_mul on input * 4. - // ------------------------------------------------------------------------- - #[test] - fn fail_input_times_4_overflow() { - // input * 4 overflows u64. - let huge = u64::MAX / 2 + 1; - let v = verdict_from_token_count_bound(huge, 0); - // tokens=0 ≤ overflow → Fail (overflow triggers Fail). - assert_eq!( - v, - Ops007Verdict::Fail, - "input * 4 overflow must Fail (not silently wrap)" - ); - } - - #[test] - fn fail_input_max_overflow_with_tokens() { - let v = verdict_from_token_count_bound(u64::MAX, 100); - assert_eq!(v, Ops007Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Boundary sweep — token-count sweep around 4× cap. - // ------------------------------------------------------------------------- - #[test] - fn token_count_sweep_at_fixed_input_100() { - let input_len = 100_u64; - let probes: Vec<(u64, Ops007Verdict)> = vec![ - (0, Ops007Verdict::Pass), - (1, Ops007Verdict::Pass), - (50, Ops007Verdict::Pass), - (100, Ops007Verdict::Pass), - (300, Ops007Verdict::Pass), - (399, Ops007Verdict::Pass), - (400, Ops007Verdict::Pass), // exact cap (inclusive) - (401, Ops007Verdict::Fail), // just above cap - (1_000, Ops007Verdict::Fail), - (u64::MAX, Ops007Verdict::Fail), - ]; - for (tokens, expected) in probes { - let v = verdict_from_token_count_bound(input_len, tokens); - assert_eq!( - v, expected, - "input=100 tokens={tokens} expected {expected:?}" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — UTF-8 byte-fallback worst-case scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_4_byte_emoji_at_4_tokens() { - // Single emoji is 4 UTF-8 bytes → up to 4 byte-fallback tokens. - let v = verdict_from_token_count_bound(4, 4); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn pass_3_byte_cjk_at_3_tokens() { - // CJK char is 3 UTF-8 bytes → up to 3 byte-fallback tokens. - let v = verdict_from_token_count_bound(3, 3); - assert_eq!(v, Ops007Verdict::Pass); - } - - #[test] - fn fail_adversarial_token_explosion() { - // Realistic regression: tokenizer produces 5+ tokens per - // input byte due to broken merge table. - let v = verdict_from_token_count_bound(1_000, 5_001); - assert_eq!( - v, - Ops007Verdict::Fail, - "5+ tokens per byte must Fail (DoS class)" - ); - } -} diff --git a/crates/aprender-core/src/format/qa_003.rs b/crates/aprender-core/src/format/qa_003.rs deleted file mode 100644 index ddb7ae6c0..000000000 --- a/crates/aprender-core/src/format/qa_003.rs +++ /dev/null @@ -1,319 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-003. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-003 says -// -// rule: json output is valid -// prediction: "apr inspect --json model | jq . exits 0" -// if_fails: "invalid JSON emitted" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`output_bytes`, `jq_exit_code`), Pass iff: -// -// output_bytes is non-empty AND -// jq_exit_code == 0 AND -// output_bytes' first non-whitespace byte is '{' or '[' AND -// output_bytes' last non-whitespace byte is '}' or ']' AND -// the bracket and brace counts balance -// -// The bracket/brace balance check is a structural sanity ahead of -// invoking `jq`. Both must agree (jq exits 0 AND structural balance) -// to accept JSON validity. This catches: -// - jq missing or replaced: structural check still applies. -// - jq stub returning 0 silently: structural check catches it. -// - Empty output: refuses vacuous Pass. -// - Truncated JSON (unbalanced brackets): caught by structural check. - -/// Binary verdict for `FALSIFY-QA-003`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa003Verdict { - /// Output is non-empty, structurally JSON-shaped (starts with - /// `{`/`[`, ends with `}`/`]`, brackets balance), AND jq exited 0. - Pass, - /// One or more of: - /// - `output_bytes.is_empty()` (caller error — apr emitted no - /// JSON at all). - /// - `jq_exit_code != 0` (jq rejected the input as invalid JSON). - /// - First non-whitespace byte not `{` or `[`. - /// - Last non-whitespace byte not `}` or `]`. - /// - Brace `{`/`}` counts unbalanced. - /// - Bracket `[`/`]` counts unbalanced. - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-003`. -/// -/// Inputs: -/// - `output_bytes`: stdout from `apr inspect --json model`. -/// - `jq_exit_code`: process exit code from -/// `apr inspect --json model | jq . > /dev/null`. -/// -/// Pass iff: -/// 1. `!output_bytes.is_empty()`, -/// 2. `jq_exit_code == 0`, -/// 3. First non-whitespace byte is `{` or `[`, -/// 4. Last non-whitespace byte is `}` or `]`, -/// 5. Brace counts equal AND bracket counts equal. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// Well-formed JSON object — `Pass`: -/// ``` -/// use aprender::format::qa_003::{ -/// verdict_from_json_validity, Qa003Verdict, -/// }; -/// let json = b"{\"model\":\"qwen\",\"tensors\":339}"; -/// let v = verdict_from_json_validity(json, 0); -/// assert_eq!(v, Qa003Verdict::Pass); -/// ``` -/// -/// Truncated JSON (jq fails) — `Fail`: -/// ``` -/// use aprender::format::qa_003::{ -/// verdict_from_json_validity, Qa003Verdict, -/// }; -/// let truncated = b"{\"model\":\"qwen\",\"tensors\":33"; -/// let v = verdict_from_json_validity(truncated, 1); -/// assert_eq!(v, Qa003Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_json_validity( - output_bytes: &[u8], - jq_exit_code: i32, -) -> Qa003Verdict { - if output_bytes.is_empty() { - return Qa003Verdict::Fail; - } - if jq_exit_code != 0 { - return Qa003Verdict::Fail; - } - // Trim leading whitespace. - let trimmed_start_idx = output_bytes - .iter() - .position(|b| !b.is_ascii_whitespace()) - .unwrap_or(output_bytes.len()); - if trimmed_start_idx >= output_bytes.len() { - return Qa003Verdict::Fail; // all-whitespace - } - let first = output_bytes[trimmed_start_idx]; - if first != b'{' && first != b'[' { - return Qa003Verdict::Fail; - } - // Trim trailing whitespace. - let trimmed_end_idx = output_bytes - .iter() - .rposition(|b| !b.is_ascii_whitespace()) - .unwrap_or(0); - let last = output_bytes[trimmed_end_idx]; - if last != b'}' && last != b']' { - return Qa003Verdict::Fail; - } - // Check brace and bracket counts balance. - // Note: this is a coarse structural check; it does NOT account - // for braces/brackets inside strings. A more rigorous check - // requires a real parser, which is FULL_DISCHARGE work. - let mut brace_balance: i64 = 0; - let mut bracket_balance: i64 = 0; - for &b in output_bytes { - match b { - b'{' => brace_balance += 1, - b'}' => brace_balance -= 1, - b'[' => bracket_balance += 1, - b']' => bracket_balance -= 1, - _ => {} - } - } - if brace_balance != 0 || bracket_balance != 0 { - return Qa003Verdict::Fail; - } - Qa003Verdict::Pass -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — well-formed JSON. - // ------------------------------------------------------------------------- - #[test] - fn pass_simple_object() { - let json = b"{\"key\":\"value\"}"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_simple_array() { - let json = b"[1,2,3]"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_realistic_apr_inspect_json() { - let json = b"{\"model\":\"qwen2.5-coder-7b-apache-q4k-v1\",\"tensors\":339,\"layers\":28}"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_nested_structure() { - let json = b"{\"outer\":{\"inner\":[1,2,{\"deep\":true}]}}"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_with_leading_trailing_whitespace() { - let json = b" \n{\"key\":\"value\"}\n "; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — jq rejected. - // ------------------------------------------------------------------------- - #[test] - fn fail_jq_exit_one() { - // Even structurally-balanced output: if jq exited non-zero, - // we trust jq. - let json = b"{\"key\":\"value\"}"; - let v = verdict_from_json_validity(json, 1); - assert_eq!(v, Qa003Verdict::Fail); - } - - #[test] - fn fail_jq_panic_exit() { - let json = b"{\"valid\":true}"; - let v = verdict_from_json_validity(json, 101); - assert_eq!(v, Qa003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — empty output. - // ------------------------------------------------------------------------- - #[test] - fn fail_empty_output() { - let v = verdict_from_json_validity(&[], 0); - assert_eq!( - v, - Qa003Verdict::Fail, - "empty output must Fail (vacuous Pass refused)" - ); - } - - #[test] - fn fail_whitespace_only() { - let v = verdict_from_json_validity(b" \n \t ", 0); - assert_eq!(v, Qa003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — non-JSON shapes. - // ------------------------------------------------------------------------- - #[test] - fn fail_starts_with_text() { - // Output: "Model: qwen" — not JSON-shaped. - let v = verdict_from_json_validity(b"Model: qwen", 0); - assert_eq!(v, Qa003Verdict::Fail); - } - - #[test] - fn fail_starts_with_quote() { - // Bare string is not what apr should emit — must be object/array. - let v = verdict_from_json_validity(b"\"just a string\"", 0); - assert_eq!(v, Qa003Verdict::Fail); - } - - #[test] - fn fail_ends_with_text() { - let v = verdict_from_json_validity(b"{\"key\":\"value\"} trailing", 0); - assert_eq!(v, Qa003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — bracket / brace imbalance. - // ------------------------------------------------------------------------- - #[test] - fn fail_unbalanced_extra_open_brace() { - let v = verdict_from_json_validity(b"{{\"key\":\"value\"}", 0); - assert_eq!( - v, - Qa003Verdict::Fail, - "unbalanced open brace must Fail" - ); - } - - #[test] - fn fail_unbalanced_missing_close_brace() { - let v = verdict_from_json_validity(b"{\"key\":\"value\"", 1); - assert_eq!(v, Qa003Verdict::Fail); - } - - #[test] - fn fail_unbalanced_extra_close_bracket() { - let v = verdict_from_json_validity(b"[1,2,3]]", 0); - assert_eq!(v, Qa003Verdict::Fail); - } - - #[test] - fn fail_truncated_mid_object() { - // Realistic regression: stdout pipe broke mid-write. - let v = verdict_from_json_validity(b"{\"model\":\"qwe", 1); - assert_eq!(v, Qa003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Edge cases — minimal valid + adversarial inputs. - // ------------------------------------------------------------------------- - #[test] - fn pass_minimal_empty_object() { - let v = verdict_from_json_validity(b"{}", 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_minimal_empty_array() { - let v = verdict_from_json_validity(b"[]", 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn fail_jq_exit_negative() { - let v = verdict_from_json_validity(b"{\"valid\":true}", -1); - assert_eq!(v, Qa003Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr inspect / qa / trace JSON outputs. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_qa_results_json() { - let json = b"{\"results\":[{\"id\":\"T-001\",\"verdict\":\"PASS\"},{\"id\":\"T-002\",\"verdict\":\"PASS\"}]}"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn pass_apr_trace_layer_stats_json() { - let json = b"{\"layers\":[{\"idx\":0,\"params\":1234567},{\"idx\":1,\"params\":1234567}]}"; - let v = verdict_from_json_validity(json, 0); - assert_eq!(v, Qa003Verdict::Pass); - } - - #[test] - fn fail_apr_inspect_emitted_text_instead_of_json() { - // Regression: --json flag accepted but text formatter was - // routed (cf. QA-007). - let v = verdict_from_json_validity(b"Model: qwen2.5-coder\nTensors: 339\n", 0); - assert_eq!(v, Qa003Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/qa_005.rs b/crates/aprender-core/src/format/qa_005.rs deleted file mode 100644 index 73dbadac5..000000000 --- a/crates/aprender-core/src/format/qa_005.rs +++ /dev/null @@ -1,284 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-005. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-005 says -// -// rule: version matches HEAD -// prediction: "apr --version contains current git hash" -// test: "apr --version | grep -q $(git rev-parse --short HEAD)" -// if_fails: "stale binary installed" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`version_output`, `git_short_hash`), Pass iff: -// -// version_output is non-empty AND -// git_short_hash is non-empty AND -// git_short_hash length is in canonical 7..=12 byte range AND -// git_short_hash is hex-only (lowercase) AND -// version_output contains git_short_hash as a substring -// -// Composes substring containment with hex-shape and length sanity -// of the git hash. Catches: -// - Stale binary: version_output has old hash, doesn't contain -// current short hash. -// - Garbled inputs: hash with non-hex chars (corruption). -// - Wrong-length hash: a regression that pads/truncates. - -/// Minimum length of a git short hash. -/// -/// `git rev-parse --short HEAD` defaults to 7 chars but auto-grows -/// for larger repos. 7 is the historical minimum. -pub const AC_QA_005_MIN_HASH_LEN: usize = 7; - -/// Maximum length of a canonical git short hash. -/// -/// Long-form sha-1 is 40, but `--short` typically caps at 12. We -/// accept up to 12 for sanity; full 40-char hashes are technically -/// valid but unusual for `--short`. -pub const AC_QA_005_MAX_HASH_LEN: usize = 12; - -/// Binary verdict for `FALSIFY-QA-005`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa005Verdict { - /// Both inputs valid AND `version_output` contains `git_short_hash` - /// as a substring. - Pass, - /// One or more of: - /// - `version_output.is_empty()` (caller error — apr --version - /// silent). - /// - `git_short_hash` is empty / wrong length / non-hex. - /// - `version_output` does NOT contain `git_short_hash` - /// (stale binary regression). - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-005`. -/// -/// Inputs: -/// - `version_output`: stdout from `apr --version`. -/// - `git_short_hash`: result of `git rev-parse --short HEAD`. -/// -/// Pass iff: -/// 1. `!version_output.is_empty()`, -/// 2. `git_short_hash.len() >= 7 AND <= 12`, -/// 3. All bytes of `git_short_hash` are lowercase hex (`0-9` or `a-f`), -/// 4. `version_output` contains `git_short_hash` as a substring. -/// -/// Otherwise `Fail`. -#[must_use] -pub fn verdict_from_version_git_hash( - version_output: &[u8], - git_short_hash: &[u8], -) -> Qa005Verdict { - if version_output.is_empty() { - return Qa005Verdict::Fail; - } - if git_short_hash.len() < AC_QA_005_MIN_HASH_LEN - || git_short_hash.len() > AC_QA_005_MAX_HASH_LEN - { - return Qa005Verdict::Fail; - } - if !git_short_hash - .iter() - .all(|&b| b.is_ascii_digit() || (b'a'..=b'f').contains(&b)) - { - return Qa005Verdict::Fail; - } - if contains_subsequence(version_output, git_short_hash) { - Qa005Verdict::Pass - } else { - Qa005Verdict::Fail - } -} - -/// Returns `true` iff `needle` appears as a contiguous subsequence -/// of `haystack`. Same primitive used in `pull_dataset_001/005` and -/// `pub_cli_001`. -#[must_use] -fn contains_subsequence(haystack: &[u8], needle: &[u8]) -> bool { - if needle.len() > haystack.len() { - return false; - } - haystack.windows(needle.len()).any(|w| w == needle) -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — git short-hash length range. - // ------------------------------------------------------------------------- - #[test] - fn provenance_min_hash_len_is_7() { - assert_eq!(AC_QA_005_MIN_HASH_LEN, 7); - } - - #[test] - fn provenance_max_hash_len_is_12() { - assert_eq!(AC_QA_005_MAX_HASH_LEN, 12); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — canonical short hashes embedded in version. - // ------------------------------------------------------------------------- - #[test] - fn pass_canonical_7char_hash() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7bf4b0)", - b"b7bf4b0", - ); - assert_eq!(v, Qa005Verdict::Pass); - } - - #[test] - fn pass_8char_hash() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7bf4b07)", - b"b7bf4b07", - ); - assert_eq!(v, Qa005Verdict::Pass); - } - - #[test] - fn pass_12char_hash_at_max_len() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7bf4b07a000)", - b"b7bf4b07a000", - ); - assert_eq!(v, Qa005Verdict::Pass); - } - - #[test] - fn pass_realistic_long_version_output() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2\nbuild: release\ncommit: b7bf4b07a\nrustc: 1.84.0", - b"b7bf4b07a", - ); - assert_eq!(v, Qa005Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — stale binary (hash mismatch). - // ------------------------------------------------------------------------- - #[test] - fn fail_old_hash_in_version() { - // Binary built from old commit; version shows old hash. - let v = verdict_from_version_git_hash( - b"apr 0.31.0 (deadbee)", - b"b7bf4b0", - ); - assert_eq!( - v, - Qa005Verdict::Fail, - "stale binary must Fail (current hash not in version)" - ); - } - - #[test] - fn fail_no_hash_in_version() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2", - b"b7bf4b0", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — empty / wrong-length hash. - // ------------------------------------------------------------------------- - #[test] - fn fail_empty_hash() { - let v = verdict_from_version_git_hash(b"apr 0.31.2 (b7bf4b0)", &[]); - assert_eq!(v, Qa005Verdict::Fail); - } - - #[test] - fn fail_hash_too_short() { - // 6 chars is below the 7-char minimum. - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7bf4b)", - b"b7bf4b", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - #[test] - fn fail_hash_too_long() { - // 13 chars exceeds 12-char cap. - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7bf4b07a0000)", - b"b7bf4b07a0000", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — non-hex hash (corruption). - // ------------------------------------------------------------------------- - #[test] - fn fail_uppercase_hex() { - // git --short emits lowercase; uppercase is corruption. - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (B7BF4B0)", - b"B7BF4B0", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - #[test] - fn fail_non_hex_chars() { - // Has `g` which is invalid hex. - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (b7g4b0a)", - b"b7g4b0a", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - #[test] - fn fail_hash_with_dash() { - let v = verdict_from_version_git_hash( - b"apr 0.31.2 (abc-def)", - b"abc-def", - ); - assert_eq!(v, Qa005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Fail band — empty version output. - // ------------------------------------------------------------------------- - #[test] - fn fail_empty_version_output() { - let v = verdict_from_version_git_hash(&[], b"b7bf4b0"); - assert_eq!(v, Qa005Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr release tag scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_v0_31_release() { - let v = verdict_from_version_git_hash( - b"apr 0.31.0 (62893da)", - b"62893da", - ); - assert_eq!(v, Qa005Verdict::Pass); - } - - #[test] - fn fail_release_binary_dirty_workspace() { - // User has uncommitted changes; current HEAD diverges from - // the binary's committed hash. - let v = verdict_from_version_git_hash( - b"apr 0.31.0 (62893da)", - b"a8bb681", // current HEAD differs from binary - ); - assert_eq!(v, Qa005Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/qa_007.rs b/crates/aprender-core/src/format/qa_007.rs deleted file mode 100644 index 25306fa0e..000000000 --- a/crates/aprender-core/src/format/qa_007.rs +++ /dev/null @@ -1,296 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-007. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-007 says -// -// rule: --json flag changes output -// prediction: "json output differs from default" -// test: "diff <(apr inspect model) <(apr inspect --json model) | -// grep -q ." -// if_fails: "--json flag is a no-op" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two byte slices (`default_output`, -// `json_output`) from running the same apr command twice (once -// without --json, once with), Pass iff: -// -// default_output is non-empty AND -// json_output is non-empty AND -// default_output != json_output -// -// Inverse-equality verdict: the two outputs MUST differ. Same -// shape catches the regression where --json is parsed but doesn't -// route to a different formatter. - -/// Binary verdict for `FALSIFY-QA-007`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa007Verdict { - /// Both outputs are non-empty AND `default_output != json_output`. - Pass, - /// One or more of: - /// - `default_output.is_empty()` (caller error — apr without - /// --json silently failed). - /// - `json_output.is_empty()` (caller error — apr with --json - /// silently failed). - /// - `default_output == json_output` (regression — --json - /// flag is a no-op; both formats route to the same writer). - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-007`. -/// -/// Inputs: -/// - `default_output`: stdout bytes from `apr `. -/// - `json_output`: stdout bytes from `apr --json `. -/// -/// Pass iff: -/// 1. `!default_output.is_empty()`, -/// 2. `!json_output.is_empty()`, -/// 3. `default_output != json_output`. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// Default and JSON outputs differ (typical) — `Pass`: -/// ``` -/// use aprender::format::qa_007::{ -/// verdict_from_json_flag_diff, Qa007Verdict, -/// }; -/// let default_out = b"Model: qwen2.5-coder\nTensors: 339\n"; -/// let json_out = b"{\"model\":\"qwen2.5-coder\",\"tensors\":339}\n"; -/// let v = verdict_from_json_flag_diff(default_out, json_out); -/// assert_eq!(v, Qa007Verdict::Pass); -/// ``` -/// -/// --json flag is a no-op (regression) — `Fail`: -/// ``` -/// use aprender::format::qa_007::{ -/// verdict_from_json_flag_diff, Qa007Verdict, -/// }; -/// let same = b"Model: qwen2.5-coder\nTensors: 339\n"; -/// let v = verdict_from_json_flag_diff(same, same); -/// assert_eq!(v, Qa007Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_json_flag_diff( - default_output: &[u8], - json_output: &[u8], -) -> Qa007Verdict { - if default_output.is_empty() || json_output.is_empty() { - return Qa007Verdict::Fail; - } - if default_output != json_output { - Qa007Verdict::Pass - } else { - Qa007Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — default and JSON outputs differ. - // ------------------------------------------------------------------------- - #[test] - fn pass_realistic_inspect_default_vs_json() { - let default_out = b"Model: qwen2.5-coder-7b\nTensors: 339\nQuant: Q4_K\n"; - let json_out = b"{\"model\":\"qwen2.5-coder-7b\",\"tensors\":339,\"quant\":\"Q4_K\"}\n"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn pass_one_byte_difference() { - // Smallest possible difference still passes. - let default_out = b"Model: A"; - let json_out = b"Model: B"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn pass_completely_different_lengths() { - let default_out = b"short"; - let json_out = b"a much longer JSON-formatted output that wraps the data"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn pass_realistic_apr_qa_outputs() { - // `apr qa model` text vs `apr qa --json model` JSON. - let default_out = b" PASS T-001: integrity\n PASS T-002: signature\n"; - let json_out = b"{\"results\":[{\"id\":\"T-001\",\"verdict\":\"PASS\"},{\"id\":\"T-002\",\"verdict\":\"PASS\"}]}\n"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — --json is a no-op (the regression). - // ------------------------------------------------------------------------- - #[test] - fn fail_json_flag_no_op() { - // Both outputs identical: --json flag was parsed but - // ignored. - let same = b"Model: qwen2.5-coder\nTensors: 339\n"; - let v = verdict_from_json_flag_diff(same, same); - assert_eq!( - v, - Qa007Verdict::Fail, - "--json no-op must Fail (both outputs identical)" - ); - } - - #[test] - fn fail_byte_identical_long_output() { - // Long but identical output. - let same = b"\ -{\"model\":\"qwen2.5-coder-7b-apache-q4k-v1\",\"tensors\":339,\"layers\":28,\"hidden\":3584,\"heads\":28,\"kv_heads\":4,\"vocab\":152064} -"; - let v = verdict_from_json_flag_diff(same, same); - assert_eq!(v, Qa007Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — empty inputs. - // ------------------------------------------------------------------------- - #[test] - fn fail_default_empty() { - let v = verdict_from_json_flag_diff(&[], b"some json"); - assert_eq!( - v, - Qa007Verdict::Fail, - "empty default output must Fail (apr silent regression)" - ); - } - - #[test] - fn fail_json_empty() { - let v = verdict_from_json_flag_diff(b"some text", &[]); - assert_eq!( - v, - Qa007Verdict::Fail, - "empty json output must Fail" - ); - } - - #[test] - fn fail_both_empty() { - let v = verdict_from_json_flag_diff(&[], &[]); - assert_eq!( - v, - Qa007Verdict::Fail, - "both empty must Fail (vacuous Pass refused)" - ); - } - - // ------------------------------------------------------------------------- - // Section 4: Edge — single-byte non-trivial differences. - // ------------------------------------------------------------------------- - #[test] - fn pass_one_byte_appended_to_json() { - // JSON output has trailing newline that default lacks. - let default_out = b"output"; - let json_out = b"output\n"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn pass_one_byte_prepended() { - let default_out = b"data"; - let json_out = b"{data"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 5: Symmetry — verdict is symmetric in (default, json). - // ------------------------------------------------------------------------- - #[test] - fn verdict_is_symmetric_pass() { - let a = b"text format"; - let b = b"{\"json\":true}"; - let ab = verdict_from_json_flag_diff(a, b); - let ba = verdict_from_json_flag_diff(b, a); - assert_eq!(ab, ba); - assert_eq!(ab, Qa007Verdict::Pass); - } - - #[test] - fn verdict_is_symmetric_fail_identical() { - let same = b"identical"; - let v1 = verdict_from_json_flag_diff(same, same); - let v2 = verdict_from_json_flag_diff(same, same); - assert_eq!(v1, v2); - assert_eq!(v1, Qa007Verdict::Fail); - } - - #[test] - fn verdict_is_symmetric_fail_one_empty() { - let real = b"data"; - let ae = verdict_from_json_flag_diff(real, &[]); - let eb = verdict_from_json_flag_diff(&[], real); - assert_eq!(ae, eb); - assert_eq!(ae, Qa007Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: Domain — inverse-equality property. - // ------------------------------------------------------------------------- - #[test] - fn pass_iff_outputs_differ_at_canonical_lengths() { - let lengths: Vec = vec![1, 10, 100, 1000]; - for len in lengths { - let a = vec![b'a'; len]; - let b = vec![b'b'; len]; - let v_diff = verdict_from_json_flag_diff(&a, &b); - assert_eq!(v_diff, Qa007Verdict::Pass, "len={len} differing"); - - let v_same = verdict_from_json_flag_diff(&a, &a); - assert_eq!(v_same, Qa007Verdict::Fail, "len={len} identical"); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — 3 apr subcommands' default vs --json contrast. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_inspect_text_vs_json() { - // Per QA-007 contract test wording. - let default_out = b"Model: qwen2.5-coder-7b-apache-q4k-v1\nTensors: 339\n"; - let json_out = b"{\"model\":\"qwen2.5-coder-7b-apache-q4k-v1\",\"tensors\":339}"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn pass_apr_diff_text_vs_json() { - let default_out = b"Tensor 0: cosine 0.9999\nTensor 1: cosine 0.9998\n"; - let json_out = b"{\"tensors\":[{\"idx\":0,\"cos\":0.9999},{\"idx\":1,\"cos\":0.9998}]}"; - let v = verdict_from_json_flag_diff(default_out, json_out); - assert_eq!(v, Qa007Verdict::Pass); - } - - #[test] - fn fail_apr_validate_json_unimplemented() { - // Hypothetical regression: `apr validate --json` was added - // to the CLI but the formatter wasn't routed; both outputs - // print the text format. - let same = b"VALIDATION: PASS\n"; - let v = verdict_from_json_flag_diff(same, same); - assert_eq!( - v, - Qa007Verdict::Fail, - "--json formatter unimplemented must Fail" - ); - } -} diff --git a/crates/aprender-core/src/format/qa_008.rs b/crates/aprender-core/src/format/qa_008.rs deleted file mode 100644 index a6ebb58c5..000000000 --- a/crates/aprender-core/src/format/qa_008.rs +++ /dev/null @@ -1,266 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-008. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-008 says -// -// rule: no phantom subcommands -// prediction: "all advertised commands have real implementations" -// test: `apr --help | awk '/^ [a-z]/{print $1}' | -// while read c; do -// apr $c --help >/dev/null 2>&1 || echo PHANTOM:$c -// done | grep -q PHANTOM && exit 1 || exit 0` -// if_fails: "subcommand listed but not implemented" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given (`commands_advertised`, `phantom_count`), -// Pass iff: -// -// commands_advertised > 0 AND -// phantom_count == 0 AND -// phantom_count <= commands_advertised -// -// Zero-tolerance: a single phantom subcommand (advertised but -// without a real `--help`-responding implementation) is enough to -// trip the gate. Distinct from QA-001 which checks the registered -// count matches 58 — QA-008 checks the *registry-vs-impl* gap. - -/// Binary verdict for `FALSIFY-QA-008`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa008Verdict { - /// `commands_advertised > 0` AND zero phantom subcommands - /// observed. - Pass, - /// One or more of: - /// - `commands_advertised == 0` (caller error — apr --help - /// listed no subcommands). - /// - `phantom_count > 0` (one or more advertised commands - /// has no working --help). - /// - `phantom_count > commands_advertised` (counter - /// corruption — partition violation). - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-008`. -/// -/// Inputs: -/// - `commands_advertised`: count of subcommand names extracted -/// from `apr --help` output (line awk pattern). -/// - `phantom_count`: count of those subcommands whose -/// `apr --help` exited non-zero. -/// -/// Pass iff: -/// 1. `commands_advertised > 0`, -/// 2. `phantom_count == 0`, -/// 3. `phantom_count <= commands_advertised` (counter sanity). -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// 58 commands advertised, all real — `Pass`: -/// ``` -/// use aprender::format::qa_008::{ -/// verdict_from_phantom_scan, Qa008Verdict, -/// }; -/// let v = verdict_from_phantom_scan(58, 0); -/// assert_eq!(v, Qa008Verdict::Pass); -/// ``` -/// -/// 1 phantom in 58 — `Fail` (one is enough): -/// ``` -/// use aprender::format::qa_008::{ -/// verdict_from_phantom_scan, Qa008Verdict, -/// }; -/// let v = verdict_from_phantom_scan(58, 1); -/// assert_eq!(v, Qa008Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_phantom_scan( - commands_advertised: u64, - phantom_count: u64, -) -> Qa008Verdict { - if commands_advertised == 0 { - return Qa008Verdict::Fail; - } - if phantom_count > commands_advertised { - return Qa008Verdict::Fail; - } - if phantom_count == 0 { - Qa008Verdict::Pass - } else { - Qa008Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — clean implementations. - // ------------------------------------------------------------------------- - #[test] - fn pass_canonical_58_no_phantoms() { - let v = verdict_from_phantom_scan(58, 0); - assert_eq!(v, Qa008Verdict::Pass); - } - - #[test] - fn pass_one_command_zero_phantoms() { - // Minimal CLI with one advertised command. - let v = verdict_from_phantom_scan(1, 0); - assert_eq!(v, Qa008Verdict::Pass); - } - - #[test] - fn pass_huge_clean_cli() { - let v = verdict_from_phantom_scan(1_000_000, 0); - assert_eq!(v, Qa008Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — phantom subcommands (zero-tolerance). - // ------------------------------------------------------------------------- - #[test] - fn fail_one_phantom_in_58() { - let v = verdict_from_phantom_scan(58, 1); - assert_eq!( - v, - Qa008Verdict::Fail, - "one phantom must Fail (no tolerance)" - ); - } - - #[test] - fn fail_handful_of_phantoms() { - let v = verdict_from_phantom_scan(58, 5); - assert_eq!(v, Qa008Verdict::Fail); - } - - #[test] - fn fail_half_phantoms() { - let v = verdict_from_phantom_scan(58, 29); - assert_eq!(v, Qa008Verdict::Fail); - } - - #[test] - fn fail_all_phantoms() { - // Catastrophic: every advertised command is phantom. - let v = verdict_from_phantom_scan(58, 58); - assert_eq!(v, Qa008Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — empty advertised (caller error). - // ------------------------------------------------------------------------- - #[test] - fn fail_zero_advertised() { - // `apr --help` listed no subcommands — registry empty. - let v = verdict_from_phantom_scan(0, 0); - assert_eq!( - v, - Qa008Verdict::Fail, - "zero advertised must Fail (vacuous Pass refused)" - ); - } - - #[test] - fn fail_zero_advertised_with_phantoms() { - // Counter corruption: zero advertised, nonzero phantoms. - let v = verdict_from_phantom_scan(0, 5); - assert_eq!(v, Qa008Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — partition violations. - // ------------------------------------------------------------------------- - #[test] - fn fail_phantoms_exceed_advertised() { - let v = verdict_from_phantom_scan(58, 100); - assert_eq!( - v, - Qa008Verdict::Fail, - "phantoms > advertised must Fail (partition violation)" - ); - } - - #[test] - fn fail_huge_phantoms_with_smaller_advertised() { - let v = verdict_from_phantom_scan(58, u64::MAX); - assert_eq!(v, Qa008Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Boundary sweep — phantom-count sweep at 58 advertised. - // ------------------------------------------------------------------------- - #[test] - fn phantom_count_sweep_at_58_advertised() { - let advertised = 58_u64; - let probes: Vec<(u64, Qa008Verdict)> = vec![ - (0, Qa008Verdict::Pass), - (1, Qa008Verdict::Fail), - (5, Qa008Verdict::Fail), - (29, Qa008Verdict::Fail), - (57, Qa008Verdict::Fail), - (58, Qa008Verdict::Fail), - (59, Qa008Verdict::Fail), // partition violation - ]; - for (phantoms, expected) in probes { - let v = verdict_from_phantom_scan(advertised, phantoms); - assert_eq!( - v, expected, - "advertised=58 phantoms={phantoms} expected {expected:?}" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 6: Domain — zero-tolerance property. - // ------------------------------------------------------------------------- - #[test] - fn pass_iff_phantom_count_is_exactly_zero() { - for advertised in [1_u64, 10, 58, 100, 1_000_000] { - let v_pass = verdict_from_phantom_scan(advertised, 0); - assert_eq!(v_pass, Qa008Verdict::Pass, "advertised={advertised}"); - - let v_fail = verdict_from_phantom_scan(advertised, 1); - assert_eq!( - v_fail, - Qa008Verdict::Fail, - "advertised={advertised} with one phantom" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — apr CLI scenarios. - // ------------------------------------------------------------------------- - #[test] - fn pass_apr_clean_canonical_release() { - // Canonical 58-command release with no phantoms. - let v = verdict_from_phantom_scan(58, 0); - assert_eq!(v, Qa008Verdict::Pass); - } - - #[test] - fn fail_apr_with_unwired_subcommand() { - // Realistic regression: a subcommand was added to the - // registry but the dispatch arm was forgotten — `apr ` - // returns "unimplemented" exit 1. - let v = verdict_from_phantom_scan(58, 1); - assert_eq!(v, Qa008Verdict::Fail); - } - - #[test] - fn pass_minimal_features_build() { - // Minimal-features build advertises fewer commands but all - // are real. - let v = verdict_from_phantom_scan(20, 0); - assert_eq!(v, Qa008Verdict::Pass); - } -} diff --git a/crates/aprender-core/src/format/qa_009.rs b/crates/aprender-core/src/format/qa_009.rs deleted file mode 100644 index fb14fbd92..000000000 --- a/crates/aprender-core/src/format/qa_009.rs +++ /dev/null @@ -1,250 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-009. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-009 says -// -// rule: 3-format coverage -// prediction: "inspect works on GGUF, APR, and SafeTensors" -// test: "apr inspect model.gguf && apr inspect model.apr && -// apr inspect model.safetensors" -// if_fails: "format not supported" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given the three exit codes from -// `apr inspect ` invoked with each format, Pass iff: -// -// gguf_exit == 0 AND apr_exit == 0 AND safetensors_exit == 0 -// -// All three must succeed independently. Conjunctive composition -// catches any one format silently regressing. Per CLAUDE.md -// "Debugging: Use apr Tools First": "All tools support GGUF, APR, -// and SafeTensors formats. If a tool says 'format not supported', -// that's a BUG." - -/// Number of model formats `apr inspect` MUST support. -/// -/// Per CLAUDE.md / spec §26.8: GGUF + APR + SafeTensors = 3 -/// formats. Pinning the count catches a regression where a 4th -/// format is added without bumping the contract, OR where one of -/// the three is silently dropped. -pub const AC_QA_009_REQUIRED_FORMAT_COUNT: u32 = 3; - -/// Binary verdict for `FALSIFY-QA-009`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa009Verdict { - /// All three formats accepted: `apr inspect` exits 0 on - /// GGUF, APR, AND SafeTensors models. - Pass, - /// One or more of the three formats is unsupported (any - /// non-zero exit). - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-009`. -/// -/// Inputs: -/// - `gguf_exit`: exit code from `apr inspect model.gguf`. -/// - `apr_exit`: exit code from `apr inspect model.apr`. -/// - `safetensors_exit`: exit code from `apr inspect model.safetensors`. -/// -/// Pass iff all three exit codes equal 0. -/// -/// Otherwise `Fail`. -/// -/// # Examples -/// -/// All three formats supported — `Pass`: -/// ``` -/// use aprender::format::qa_009::{ -/// verdict_from_three_format_coverage, Qa009Verdict, -/// }; -/// let v = verdict_from_three_format_coverage(0, 0, 0); -/// assert_eq!(v, Qa009Verdict::Pass); -/// ``` -/// -/// SafeTensors unsupported — `Fail`: -/// ``` -/// use aprender::format::qa_009::{ -/// verdict_from_three_format_coverage, Qa009Verdict, -/// }; -/// let v = verdict_from_three_format_coverage(0, 0, 1); -/// assert_eq!(v, Qa009Verdict::Fail); -/// ``` -#[must_use] -pub fn verdict_from_three_format_coverage( - gguf_exit: i32, - apr_exit: i32, - safetensors_exit: i32, -) -> Qa009Verdict { - if gguf_exit == 0 && apr_exit == 0 && safetensors_exit == 0 { - Qa009Verdict::Pass - } else { - Qa009Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Provenance pin — 3 formats canonical. - // ------------------------------------------------------------------------- - #[test] - fn provenance_required_format_count_is_three() { - assert_eq!(AC_QA_009_REQUIRED_FORMAT_COUNT, 3); - } - - // ------------------------------------------------------------------------- - // Section 2: Pass band — only (0, 0, 0) passes. - // ------------------------------------------------------------------------- - #[test] - fn pass_all_three_succeed() { - let v = verdict_from_three_format_coverage(0, 0, 0); - assert_eq!(v, Qa009Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — exactly one format fails. - // ------------------------------------------------------------------------- - #[test] - fn fail_gguf_unsupported() { - let v = verdict_from_three_format_coverage(1, 0, 0); - assert_eq!( - v, - Qa009Verdict::Fail, - "GGUF unsupported must Fail" - ); - } - - #[test] - fn fail_apr_unsupported() { - let v = verdict_from_three_format_coverage(0, 1, 0); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_safetensors_unsupported() { - let v = verdict_from_three_format_coverage(0, 0, 1); - assert_eq!(v, Qa009Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — multiple formats fail. - // ------------------------------------------------------------------------- - #[test] - fn fail_gguf_and_apr() { - let v = verdict_from_three_format_coverage(1, 1, 0); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_gguf_and_safetensors() { - let v = verdict_from_three_format_coverage(1, 0, 1); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_apr_and_safetensors() { - let v = verdict_from_three_format_coverage(0, 1, 1); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_all_three_fail() { - let v = verdict_from_three_format_coverage(1, 1, 1); - assert_eq!(v, Qa009Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — non-1 exit codes. - // ------------------------------------------------------------------------- - #[test] - fn fail_panic_on_one_format() { - let v = verdict_from_three_format_coverage(0, 0, 101); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_negative_exit() { - let v = verdict_from_three_format_coverage(-1, 0, 0); - assert_eq!(v, Qa009Verdict::Fail); - } - - #[test] - fn fail_i32_max_exit() { - let v = verdict_from_three_format_coverage(0, 0, i32::MAX); - assert_eq!(v, Qa009Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 6: 8-cell composite matrix — all 2³ combinations. - // ------------------------------------------------------------------------- - #[test] - fn matrix_pass_iff_all_three_zero() { - // (gguf, apr, safetensors) where 0=success, 1=fail. - let cases: Vec<(i32, i32, i32, Qa009Verdict)> = vec![ - (0, 0, 0, Qa009Verdict::Pass), // canonical pass - (1, 0, 0, Qa009Verdict::Fail), - (0, 1, 0, Qa009Verdict::Fail), - (0, 0, 1, Qa009Verdict::Fail), - (1, 1, 0, Qa009Verdict::Fail), - (1, 0, 1, Qa009Verdict::Fail), - (0, 1, 1, Qa009Verdict::Fail), - (1, 1, 1, Qa009Verdict::Fail), - ]; - for (g, a, s, expected) in cases { - let v = verdict_from_three_format_coverage(g, a, s); - assert_eq!( - v, expected, - "gguf={g} apr={a} safetensors={s} expected {expected:?}" - ); - } - } - - // ------------------------------------------------------------------------- - // Section 7: Symmetry — verdict is invariant under permuting the 3 inputs. - // ------------------------------------------------------------------------- - #[test] - fn verdict_invariant_under_permutation_of_zero_zero_one() { - // (0, 0, 1) → Fail, regardless of which slot the 1 is in. - let v1 = verdict_from_three_format_coverage(0, 0, 1); - let v2 = verdict_from_three_format_coverage(0, 1, 0); - let v3 = verdict_from_three_format_coverage(1, 0, 0); - assert_eq!(v1, v2); - assert_eq!(v2, v3); - assert_eq!(v1, Qa009Verdict::Fail); - } - - #[test] - fn pass_only_at_origin() { - // The Pass cell is exactly (0, 0, 0); no other cell passes. - for (g, a, s) in [ - (0_i32, 0_i32, 0_i32), - ] { - let v = verdict_from_three_format_coverage(g, a, s); - assert_eq!(v, Qa009Verdict::Pass); - } - for &g in &[0_i32, 1, -1, 101] { - for &a in &[0_i32, 1, -1, 101] { - for &s in &[0_i32, 1, -1, 101] { - let v = verdict_from_three_format_coverage(g, a, s); - let expected = if g == 0 && a == 0 && s == 0 { - Qa009Verdict::Pass - } else { - Qa009Verdict::Fail - }; - assert_eq!( - v, expected, - "gguf={g} apr={a} safetensors={s}" - ); - } - } - } - } -} diff --git a/crates/aprender-core/src/format/qa_010.rs b/crates/aprender-core/src/format/qa_010.rs deleted file mode 100644 index ddaf802ba..000000000 --- a/crates/aprender-core/src/format/qa_010.rs +++ /dev/null @@ -1,239 +0,0 @@ -// SHIP-TWO-001 — `apr-cli-qa-v1` algorithm-level PARTIAL discharge -// for FALSIFY-QA-010. -// -// Contract: `contracts/apr-cli-qa-v1.yaml`. -// Spec: `docs/specifications/aprender-train/ship-two-models-spec.md` -// (apr CLI QA gates). -// -// ## What FALSIFY-QA-010 says -// -// rule: cross-subcommand architecture consistency -// prediction: "inspect and check report same architecture" -// test: "diff <(apr inspect --json M | jq .architecture) -// <(apr check M 2>&1 | grep -i arch)" -// if_fails: "architecture disagrees across subcommands" -// -// ## What this file proves NOW (`PARTIAL_ALGORITHM_LEVEL`) -// -// Decision rule: given two architecture-string slices extracted -// from `apr inspect --json` and `apr check`, Pass iff: -// -// inspect_arch is non-empty AND -// check_arch is non-empty AND -// inspect_arch == check_arch (byte-identical) -// -// Positive byte-equality verdict (cf. `bpe_inv_006` encode -// determinism). Different subcommands MUST agree on the model -// architecture; disagreement signals a stale parser, a feature-flag -// drift, or a registry mismatch. - -/// Binary verdict for `FALSIFY-QA-010`. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Qa010Verdict { - /// Both architecture strings are non-empty AND byte-identical. - Pass, - /// One or more of: - /// - Either string is empty (caller error — extraction failed). - /// - Strings differ in any byte (architecture disagreement). - Fail, -} - -/// Pure verdict function for `FALSIFY-QA-010`. -/// -/// Inputs: -/// - `inspect_arch`: architecture string extracted from -/// `apr inspect --json M | jq .architecture`. -/// - `check_arch`: architecture string extracted from -/// `apr check M | grep -i arch`. -/// -/// Pass iff both non-empty AND `inspect_arch == check_arch`. -/// -/// Otherwise `Fail`. -#[must_use] -pub fn verdict_from_cross_subcmd_arch( - inspect_arch: &[u8], - check_arch: &[u8], -) -> Qa010Verdict { - if inspect_arch.is_empty() || check_arch.is_empty() { - return Qa010Verdict::Fail; - } - if inspect_arch == check_arch { - Qa010Verdict::Pass - } else { - Qa010Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ------------------------------------------------------------------------- - // Section 1: Pass band — agreement at canonical architectures. - // ------------------------------------------------------------------------- - #[test] - fn pass_qwen2_agreement() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen2"); - assert_eq!(v, Qa010Verdict::Pass); - } - - #[test] - fn pass_llama_agreement() { - let v = verdict_from_cross_subcmd_arch(b"llama", b"llama"); - assert_eq!(v, Qa010Verdict::Pass); - } - - #[test] - fn pass_qwen3_moe_agreement() { - let v = verdict_from_cross_subcmd_arch(b"qwen3-moe", b"qwen3-moe"); - assert_eq!(v, Qa010Verdict::Pass); - } - - // ------------------------------------------------------------------------- - // Section 2: Fail band — architecture disagreement. - // ------------------------------------------------------------------------- - #[test] - fn fail_qwen2_vs_qwen3() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen3"); - assert_eq!( - v, - Qa010Verdict::Fail, - "different architectures must Fail" - ); - } - - #[test] - fn fail_llama_vs_qwen() { - let v = verdict_from_cross_subcmd_arch(b"llama", b"qwen2"); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_one_byte_difference() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen3"); - assert_eq!(v, Qa010Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 3: Fail band — case mismatch (case-sensitive). - // ------------------------------------------------------------------------- - #[test] - fn fail_case_difference() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b"QWEN2"); - assert_eq!( - v, - Qa010Verdict::Fail, - "case mismatch must Fail (one subcmd normalized, other didn't)" - ); - } - - #[test] - fn fail_inspect_lowercase_check_titlecase() { - let v = verdict_from_cross_subcmd_arch(b"llama", b"Llama"); - assert_eq!(v, Qa010Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 4: Fail band — whitespace / formatting differences. - // ------------------------------------------------------------------------- - #[test] - fn fail_trailing_whitespace() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen2 "); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_leading_whitespace() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", b" qwen2"); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_with_quotes() { - // jq sometimes emits values with quotes; `grep` strips them. - let v = verdict_from_cross_subcmd_arch(b"\"qwen2\"", b"qwen2"); - assert_eq!(v, Qa010Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 5: Fail band — empty inputs. - // ------------------------------------------------------------------------- - #[test] - fn fail_inspect_arch_empty() { - let v = verdict_from_cross_subcmd_arch(&[], b"qwen2"); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_check_arch_empty() { - let v = verdict_from_cross_subcmd_arch(b"qwen2", &[]); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_both_empty() { - let v = verdict_from_cross_subcmd_arch(&[], &[]); - assert_eq!( - v, - Qa010Verdict::Fail, - "both empty must Fail (vacuous Pass refused)" - ); - } - - // ------------------------------------------------------------------------- - // Section 6: Symmetry — verdict is symmetric in (inspect, check). - // ------------------------------------------------------------------------- - #[test] - fn verdict_is_symmetric_pass() { - let v_ic = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen2"); - let v_ci = verdict_from_cross_subcmd_arch(b"qwen2", b"qwen2"); - assert_eq!(v_ic, v_ci); - assert_eq!(v_ic, Qa010Verdict::Pass); - } - - #[test] - fn verdict_is_symmetric_fail() { - let v_ic = verdict_from_cross_subcmd_arch(b"qwen2", b"llama"); - let v_ci = verdict_from_cross_subcmd_arch(b"llama", b"qwen2"); - assert_eq!(v_ic, v_ci); - assert_eq!(v_ic, Qa010Verdict::Fail); - } - - // ------------------------------------------------------------------------- - // Section 7: Realistic — full architecture string family. - // ------------------------------------------------------------------------- - #[test] - fn pass_realistic_full_architecture_strings() { - let v = verdict_from_cross_subcmd_arch( - b"qwen2.5-coder-7b", - b"qwen2.5-coder-7b", - ); - assert_eq!(v, Qa010Verdict::Pass); - } - - #[test] - fn fail_realistic_inspect_full_check_short() { - // Common drift: inspect emits full name, check emits short. - let v = verdict_from_cross_subcmd_arch( - b"qwen2.5-coder-7b", - b"qwen2", - ); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn fail_inspect_says_qwen3_check_says_qwen2() { - // Worst case: stale check parser gives wrong arch. - let v = verdict_from_cross_subcmd_arch(b"qwen3-moe", b"qwen2"); - assert_eq!(v, Qa010Verdict::Fail); - } - - #[test] - fn pass_albor_llama_370m() { - let v = verdict_from_cross_subcmd_arch( - b"albor-llama-370m", - b"albor-llama-370m", - ); - assert_eq!(v, Qa010Verdict::Pass); - } -} diff --git a/crates/aprender-core/src/format/readme_claims.rs b/crates/aprender-core/src/format/readme_claims.rs deleted file mode 100644 index 20900afcd..000000000 --- a/crates/aprender-core/src/format/readme_claims.rs +++ /dev/null @@ -1,150 +0,0 @@ -// SHIP-TWO-001 — `readme-claims-v1` algorithm-level PARTIAL discharge -// for FALSIFY-README-001..004 (closes 4/4). -// -// Contract: `contracts/readme-claims-v1.yaml`. -// -// Bundles 4 verdict fns over README-vs-repo-state consistency. The -// runtime-level falsifier `bash scripts/check_readme_claims.sh` -// already exists per contract evidence — this file pins the -// *decision rule* against drift in: -// -// - workspace crate count (claimed N == observed N) -// - contract YAML count (claimed M == observed M) -// - apr CLI subcommand count (claimed K == observed K) -// - apr-cookbook link presence (≥ 1 hit in README) - -// =========================================================================== -// README-001 — Workspace crate count claim matches filesystem -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Readme001Verdict { Pass, Fail } - -/// Pass iff `claimed == observed` AND both are non-zero. -#[must_use] -pub fn verdict_from_crate_count(claimed: u64, observed: u64) -> Readme001Verdict { - if claimed == 0 || observed == 0 { return Readme001Verdict::Fail; } - if claimed == observed { Readme001Verdict::Pass } else { Readme001Verdict::Fail } -} - -// =========================================================================== -// README-002 — Contract YAML count claim matches filesystem -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Readme002Verdict { Pass, Fail } - -/// Pass iff `claimed == observed` AND both are non-zero. -#[must_use] -pub fn verdict_from_contract_count(claimed: u64, observed: u64) -> Readme002Verdict { - if claimed == 0 || observed == 0 { return Readme002Verdict::Fail; } - if claimed == observed { Readme002Verdict::Pass } else { Readme002Verdict::Fail } -} - -// =========================================================================== -// README-003 — CLI subcommand count claim matches `apr --help` -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Readme003Verdict { Pass, Fail } - -/// Pass iff `claimed == observed` AND `observed >= MIN_REASONABLE` -/// (guards against an empty-help regression — apr is documented as a -/// 58-subcommand CLI in `CLAUDE.md`). -pub const AC_README_003_MIN_REASONABLE: u64 = 30; - -#[must_use] -pub fn verdict_from_cli_command_count(claimed: u64, observed: u64) -> Readme003Verdict { - if observed < AC_README_003_MIN_REASONABLE { return Readme003Verdict::Fail; } - if claimed == observed { Readme003Verdict::Pass } else { Readme003Verdict::Fail } -} - -// =========================================================================== -// README-004 — `apr-cookbook` link is present in README -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Readme004Verdict { Pass, Fail } - -/// Pass iff `readme_text` contains the literal substring `apr-cookbook`. -/// Matches both `[apr-cookbook](url)` markdown links and bare path -/// references like `../apr-cookbook/...`. -#[must_use] -pub fn verdict_from_cookbook_link_presence(readme_text: &str) -> Readme004Verdict { - if readme_text.contains("apr-cookbook") { - Readme004Verdict::Pass - } else { - Readme004Verdict::Fail - } -} - -#[cfg(test)] -mod tests { - use super::*; - - // ----- README-001 -------------------------------------------------------- - - #[test] fn r001_pass_match() { assert_eq!(verdict_from_crate_count(70, 70), Readme001Verdict::Pass); } - #[test] fn r001_fail_off_by_one_high() { assert_eq!(verdict_from_crate_count(70, 71), Readme001Verdict::Fail); } - #[test] fn r001_fail_off_by_one_low() { assert_eq!(verdict_from_crate_count(70, 69), Readme001Verdict::Fail); } - #[test] fn r001_fail_claimed_zero() { assert_eq!(verdict_from_crate_count(0, 70), Readme001Verdict::Fail); } - #[test] fn r001_fail_observed_zero() { assert_eq!(verdict_from_crate_count(70, 0), Readme001Verdict::Fail); } - - // ----- README-002 -------------------------------------------------------- - - #[test] fn r002_pass_match() { assert_eq!(verdict_from_contract_count(405, 405), Readme002Verdict::Pass); } - #[test] fn r002_fail_stale_low() { assert_eq!(verdict_from_contract_count(400, 405), Readme002Verdict::Fail); } - #[test] fn r002_fail_zero_observed() { assert_eq!(verdict_from_contract_count(405, 0), Readme002Verdict::Fail); } - #[test] fn r002_fail_zero_claimed() { assert_eq!(verdict_from_contract_count(0, 405), Readme002Verdict::Fail); } - - // ----- README-003 -------------------------------------------------------- - - #[test] fn r003_pass_match() { assert_eq!(verdict_from_cli_command_count(58, 58), Readme003Verdict::Pass); } - #[test] fn r003_pass_match_at_min() { - assert_eq!( - verdict_from_cli_command_count(AC_README_003_MIN_REASONABLE, AC_README_003_MIN_REASONABLE), - Readme003Verdict::Pass - ); - } - #[test] fn r003_fail_observed_below_min() { - // Empty-help regression: only 5 subcommands listed. - assert_eq!(verdict_from_cli_command_count(58, 5), Readme003Verdict::Fail); - } - #[test] fn r003_fail_off_by_one() { assert_eq!(verdict_from_cli_command_count(58, 59), Readme003Verdict::Fail); } - #[test] fn r003_fail_subcommand_dropped() { assert_eq!(verdict_from_cli_command_count(58, 57), Readme003Verdict::Fail); } - #[test] fn r003_provenance_min() { assert_eq!(AC_README_003_MIN_REASONABLE, 30); } - - // ----- README-004 -------------------------------------------------------- - - #[test] fn r004_pass_markdown_link() { - let readme = "See the [apr-cookbook](https://github.com/paiml/apr-cookbook) for recipes."; - assert_eq!(verdict_from_cookbook_link_presence(readme), Readme004Verdict::Pass); - } - - #[test] fn r004_pass_relative_path() { - let readme = "Local check: `../apr-cookbook/recipes/qwen.md`."; - assert_eq!(verdict_from_cookbook_link_presence(readme), Readme004Verdict::Pass); - } - - #[test] fn r004_pass_bare_mention() { - // The contract just requires the literal substring. - let readme = "Coordinated with apr-cookbook."; - assert_eq!(verdict_from_cookbook_link_presence(readme), Readme004Verdict::Pass); - } - - #[test] fn r004_fail_link_removed() { - let readme = "# aprender\n\nA Rust ML framework.\n"; - assert_eq!(verdict_from_cookbook_link_presence(readme), Readme004Verdict::Fail); - } - - #[test] fn r004_fail_link_renamed_without_sync() { - // Someone replaced `apr-cookbook` with `apr-recipes` and forgot - // to update the link. - let readme = "See [apr-recipes](https://example.com)."; - assert_eq!(verdict_from_cookbook_link_presence(readme), Readme004Verdict::Fail); - } - - #[test] fn r004_fail_empty() { - assert_eq!(verdict_from_cookbook_link_presence(""), Readme004Verdict::Fail); - } -} diff --git a/crates/aprender-core/src/format/sub_ffn_rest.rs b/crates/aprender-core/src/format/sub_ffn_rest.rs deleted file mode 100644 index 84e3ef2c2..000000000 --- a/crates/aprender-core/src/format/sub_ffn_rest.rs +++ /dev/null @@ -1,364 +0,0 @@ -// SHIP-TWO-001 — `trace-ffn-sub-block-v1` algorithm-level PARTIAL -// discharge for FALSIFY-SUB-FFN-001..004 + 006..008 (closes 7 -// remaining gates; SUB-FFN-005 already bound in `sub_ffn_005.rs`). -// -// Contract: `contracts/trace-ffn-sub-block-v1.yaml`. -// Spec: SHIP-007 layer-3 sub-FFN bisection. - -// =========================================================================== -// Canonical contract constants -// =========================================================================== - -pub const AC_SUB_FFN_BEFORE_FIELD_COUNT: u64 = 6; -pub const AC_SUB_FFN_AFTER_FIELD_COUNT: u64 = 10; -pub const AC_SUB_FFN_REFERENCE_LAYER_INDEX: u32 = 3; -pub const AC_SUB_FFN_REFERENCE_FFN_OUT_STD_LAYER_3: f64 = 11.459; -pub const AC_SUB_FFN_REFERENCE_FFN_OUT_STD_LAYER_2: f64 = 0.216; -/// Spike ratio threshold: layer-3 std must exceed 3× median over layers 5..=26. -pub const AC_SUB_FFN_001_SPIKE_RATIO: f64 = 3.0; -pub const AC_SUB_FFN_001_NEIGHBOR_RATIO_LIMIT: f64 = 2.0; -pub const AC_SUB_FFN_006_QWEN_INTERMEDIATE_DIM: usize = 18_944; - -// =========================================================================== -// SUB-FFN-001 — Exactly one slot at layer 3 has std ≥ 3× median -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn001Verdict { Pass, Fail } - -/// `slot_stds_layer_3[i]` is the std of slot `i` at layer 3. -/// `slot_medians[i]` is the median std of slot `i` across layers 5..=26. -/// Pass iff exactly one slot has std >= 3 × median AND every other slot -/// has std < 2 × median. -#[must_use] -pub fn verdict_from_layer3_spike_localized( - slot_stds_layer_3: &[f64; 5], - slot_medians: &[f64; 5], -) -> SubFfn001Verdict { - if slot_medians.iter().any(|m| !m.is_finite() || *m <= 0.0) { - return SubFfn001Verdict::Fail; - } - if slot_stds_layer_3.iter().any(|s| !s.is_finite() || *s < 0.0) { - return SubFfn001Verdict::Fail; - } - let mut spike_count = 0; - let mut neighbor_violations = 0; - for i in 0..5 { - let ratio = slot_stds_layer_3[i] / slot_medians[i]; - if ratio >= AC_SUB_FFN_001_SPIKE_RATIO { - spike_count += 1; - } else if ratio >= AC_SUB_FFN_001_NEIGHBOR_RATIO_LIMIT { - neighbor_violations += 1; - } - } - if spike_count == 1 && neighbor_violations == 0 { - SubFfn001Verdict::Pass - } else { - SubFfn001Verdict::Fail - } -} - -// =========================================================================== -// SUB-FFN-002 — Backward compat: existing ffn_out_stats byte-identical -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn002Verdict { Pass, Fail } - -/// Pass iff `pre_bytes == post_bytes` for the canonical ffn_out_stats -/// snapshot from one of the regression tests. -#[must_use] -pub fn verdict_from_ffn_out_stats_byte_identical(pre: &[u8], post: &[u8]) -> SubFfn002Verdict { - if pre.is_empty() || post.is_empty() { return SubFfn002Verdict::Fail; } - if pre == post { SubFfn002Verdict::Pass } else { SubFfn002Verdict::Fail } -} - -// =========================================================================== -// SUB-FFN-003 — Naming alignment with layer-parity-v1 -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn003Verdict { Pass, Fail } - -/// Canonical mapping from sub-FFN trace field to layer-parity step. -/// Pass iff the supplied mapping equals the canonical mapping (4 -/// pairs). -#[must_use] -pub fn verdict_from_naming_alignment(observed: &[(&str, &str)]) -> SubFfn003Verdict { - let canonical: [(&str, &str); 4] = [ - ("ffn_gate", "gate_proj"), - ("ffn_up", "up_proj"), - ("ffn_swiglu", "swiglu"), - ("ffn_out", "down_proj"), - ]; - if observed.len() != canonical.len() { return SubFfn003Verdict::Fail; } - for can in canonical { - if !observed.iter().any(|p| *p == can) { return SubFfn003Verdict::Fail; } - } - SubFfn003Verdict::Pass -} - -// =========================================================================== -// SUB-FFN-004 — GPU TracedForward: populated stats OR explicit incomplete flag -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum GpuTelemetryShape { - /// All 4 new fields populated with non-zero values from real GPU. - AllPopulated, - /// Fields explicitly zero AND `gpu_telemetry_complete: false`. - AllZeroFlagged, - /// Fields zero with `gpu_telemetry_complete: true` (the regression). - SilentlyZeroPretendingComplete, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn004Verdict { Pass, Fail } - -#[must_use] -pub fn verdict_from_gpu_telemetry_shape(shape: GpuTelemetryShape) -> SubFfn004Verdict { - match shape { - GpuTelemetryShape::AllPopulated | GpuTelemetryShape::AllZeroFlagged => SubFfn004Verdict::Pass, - GpuTelemetryShape::SilentlyZeroPretendingComplete => SubFfn004Verdict::Fail, - } -} - -// =========================================================================== -// SUB-FFN-006 — Captured vector lengths == intermediate_dim -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn006Verdict { Pass, Fail } - -/// Pass iff every captured-vector length equals `intermediate_dim` AND -/// `intermediate_dim > 0`. -#[must_use] -pub fn verdict_from_vector_length_correct( - captured_lens: &[usize; 4], - intermediate_dim: usize, -) -> SubFfn006Verdict { - if intermediate_dim == 0 { return SubFfn006Verdict::Fail; } - for &len in captured_lens { - if len != intermediate_dim { return SubFfn006Verdict::Fail; } - } - SubFfn006Verdict::Pass -} - -// =========================================================================== -// SUB-FFN-007 — Doc-comment cites the contract id (drift-prevention) -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn007Verdict { Pass, Fail } - -pub const AC_SUB_FFN_007_NEEDLE: &str = "contracts/trace-ffn-sub-block-v1"; -pub const AC_SUB_FFN_007_REQUIRED_HITS: usize = 4; - -/// Pass iff `source_lines` contains the contract path string at least -/// `AC_SUB_FFN_007_REQUIRED_HITS` (=4) times — one per new field. -#[must_use] -pub fn verdict_from_doc_citation_count(source_lines: &str) -> SubFfn007Verdict { - let count = source_lines.matches(AC_SUB_FFN_007_NEEDLE).count(); - if count >= AC_SUB_FFN_007_REQUIRED_HITS { SubFfn007Verdict::Pass } else { SubFfn007Verdict::Fail } -} - -// =========================================================================== -// SUB-FFN-008 — Coverage co-evolution: every new field covered by ≥1 test -// =========================================================================== - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum SubFfn008Verdict { Pass, Fail } - -pub const AC_SUB_FFN_008_NEW_FIELDS: [&str; 4] = [ - "ffn_gate_stats", - "ffn_up_stats", - "ffn_silu_gate_stats", - "ffn_swiglu_inner_stats", -]; - -/// `field_test_counts` is a parallel array of test counts per field. -/// Pass iff every entry is ≥ 1. -#[must_use] -pub fn verdict_from_coverage_coevolution(field_test_counts: &[u64; 4]) -> SubFfn008Verdict { - for &count in field_test_counts { - if count == 0 { return SubFfn008Verdict::Fail; } - } - SubFfn008Verdict::Pass -} - -#[cfg(test)] -mod tests { - use super::*; - - // ----- SUB-FFN-001 ------------------------------------------------------- - - #[test] fn sf001_pass_one_spike() { - // Slot 3 (ffn_out) at 11.459 vs median 0.216 ≈ 53× spike; - // other slots near median. - let l3 = [0.5, 0.4, 0.3, 11.459, 0.5]; - let med = [0.5, 0.5, 0.5, 0.216, 0.5]; - assert_eq!(verdict_from_layer3_spike_localized(&l3, &med), SubFfn001Verdict::Pass); - } - - #[test] fn sf001_fail_no_spike() { - let l3 = [0.5, 0.4, 0.3, 0.5, 0.5]; - let med = [0.5; 5]; - assert_eq!(verdict_from_layer3_spike_localized(&l3, &med), SubFfn001Verdict::Fail); - } - - #[test] fn sf001_fail_two_spikes() { - let l3 = [10.0, 0.4, 0.3, 11.0, 0.5]; - let med = [0.5; 5]; - assert_eq!(verdict_from_layer3_spike_localized(&l3, &med), SubFfn001Verdict::Fail); - } - - #[test] fn sf001_fail_neighbor_above_2x() { - // Slot 3 at 30× spike + slot 1 at 2.5× (above 2× neighbor limit). - let l3 = [0.5, 1.25, 0.3, 15.0, 0.5]; - let med = [0.5; 5]; - assert_eq!(verdict_from_layer3_spike_localized(&l3, &med), SubFfn001Verdict::Fail); - } - - #[test] fn sf001_fail_zero_median() { - let l3 = [0.5, 0.4, 0.3, 11.0, 0.5]; - let med = [0.5, 0.5, 0.5, 0.0, 0.5]; - assert_eq!(verdict_from_layer3_spike_localized(&l3, &med), SubFfn001Verdict::Fail); - } - - // ----- SUB-FFN-002 ------------------------------------------------------- - - #[test] fn sf002_pass_match() { - assert_eq!(verdict_from_ffn_out_stats_byte_identical(b"abc", b"abc"), SubFfn002Verdict::Pass); - } - - #[test] fn sf002_fail_drift() { - assert_eq!(verdict_from_ffn_out_stats_byte_identical(b"abc", b"abd"), SubFfn002Verdict::Fail); - } - - #[test] fn sf002_fail_empty() { - assert_eq!(verdict_from_ffn_out_stats_byte_identical(b"", b"abc"), SubFfn002Verdict::Fail); - } - - // ----- SUB-FFN-003 ------------------------------------------------------- - - #[test] fn sf003_pass_canonical() { - let obs = [ - ("ffn_gate", "gate_proj"), - ("ffn_up", "up_proj"), - ("ffn_swiglu", "swiglu"), - ("ffn_out", "down_proj"), - ]; - assert_eq!(verdict_from_naming_alignment(&obs), SubFfn003Verdict::Pass); - } - - #[test] fn sf003_pass_reordered() { - let obs = [ - ("ffn_out", "down_proj"), - ("ffn_gate", "gate_proj"), - ("ffn_swiglu", "swiglu"), - ("ffn_up", "up_proj"), - ]; - assert_eq!(verdict_from_naming_alignment(&obs), SubFfn003Verdict::Pass); - } - - #[test] fn sf003_fail_missing_pair() { - let obs = [ - ("ffn_gate", "gate_proj"), - ("ffn_up", "up_proj"), - ("ffn_out", "down_proj"), - ]; - assert_eq!(verdict_from_naming_alignment(&obs), SubFfn003Verdict::Fail); - } - - #[test] fn sf003_fail_renamed_field() { - let obs = [ - ("ffn_gate", "gate_proj"), - ("ffn_up", "up_proj"), - ("ffn_swiglu", "swiglu"), - ("ffn_out", "WRONG_NAME"), - ]; - assert_eq!(verdict_from_naming_alignment(&obs), SubFfn003Verdict::Fail); - } - - // ----- SUB-FFN-004 ------------------------------------------------------- - - #[test] fn sf004_pass_populated() { - assert_eq!(verdict_from_gpu_telemetry_shape(GpuTelemetryShape::AllPopulated), SubFfn004Verdict::Pass); - } - #[test] fn sf004_pass_flagged_zero() { - assert_eq!(verdict_from_gpu_telemetry_shape(GpuTelemetryShape::AllZeroFlagged), SubFfn004Verdict::Pass); - } - #[test] fn sf004_fail_silent_zero() { - // The regression: GPU silently emits zeros while pretending complete. - assert_eq!( - verdict_from_gpu_telemetry_shape(GpuTelemetryShape::SilentlyZeroPretendingComplete), - SubFfn004Verdict::Fail - ); - } - - // ----- SUB-FFN-006 ------------------------------------------------------- - - #[test] fn sf006_pass_qwen_intermediate() { - let lens = [18944, 18944, 18944, 18944]; - assert_eq!(verdict_from_vector_length_correct(&lens, AC_SUB_FFN_006_QWEN_INTERMEDIATE_DIM), SubFfn006Verdict::Pass); - } - #[test] fn sf006_fail_one_short() { - let lens = [18944, 18944, 100, 18944]; - assert_eq!(verdict_from_vector_length_correct(&lens, AC_SUB_FFN_006_QWEN_INTERMEDIATE_DIM), SubFfn006Verdict::Fail); - } - #[test] fn sf006_fail_zero_dim() { - let lens = [0, 0, 0, 0]; - assert_eq!(verdict_from_vector_length_correct(&lens, 0), SubFfn006Verdict::Fail); - } - - // ----- SUB-FFN-007 ------------------------------------------------------- - - #[test] fn sf007_pass_four_citations() { - let src = "fn a() {}\n/// contracts/trace-ffn-sub-block-v1\nfn b() {}\n\ - /// contracts/trace-ffn-sub-block-v1\nfn c() {}\n\ - /// contracts/trace-ffn-sub-block-v1\nfn d() {}\n\ - /// contracts/trace-ffn-sub-block-v1\nfn e() {}\n"; - assert_eq!(verdict_from_doc_citation_count(src), SubFfn007Verdict::Pass); - } - #[test] fn sf007_pass_more_than_four() { - let src = "contracts/trace-ffn-sub-block-v1 ".repeat(10); - assert_eq!(verdict_from_doc_citation_count(&src), SubFfn007Verdict::Pass); - } - #[test] fn sf007_fail_three_citations() { - let src = "contracts/trace-ffn-sub-block-v1 ".repeat(3); - assert_eq!(verdict_from_doc_citation_count(&src), SubFfn007Verdict::Fail); - } - #[test] fn sf007_fail_no_citations() { - assert_eq!(verdict_from_doc_citation_count("fn main() {}"), SubFfn007Verdict::Fail); - } - - // ----- SUB-FFN-008 ------------------------------------------------------- - - #[test] fn sf008_pass_all_covered() { - assert_eq!(verdict_from_coverage_coevolution(&[1, 1, 1, 1]), SubFfn008Verdict::Pass); - } - #[test] fn sf008_pass_more_tests() { - assert_eq!(verdict_from_coverage_coevolution(&[5, 3, 8, 2]), SubFfn008Verdict::Pass); - } - #[test] fn sf008_fail_one_uncovered() { - assert_eq!(verdict_from_coverage_coevolution(&[1, 1, 0, 1]), SubFfn008Verdict::Fail); - } - #[test] fn sf008_fail_all_zero() { - assert_eq!(verdict_from_coverage_coevolution(&[0, 0, 0, 0]), SubFfn008Verdict::Fail); - } - - // ----- Provenance pins --------------------------------------------------- - - #[test] fn provenance_constants() { - assert_eq!(AC_SUB_FFN_BEFORE_FIELD_COUNT, 6); - assert_eq!(AC_SUB_FFN_AFTER_FIELD_COUNT, 10); - assert_eq!(AC_SUB_FFN_REFERENCE_LAYER_INDEX, 3); - assert!((AC_SUB_FFN_REFERENCE_FFN_OUT_STD_LAYER_3 - 11.459).abs() < 1e-9); - assert!((AC_SUB_FFN_REFERENCE_FFN_OUT_STD_LAYER_2 - 0.216).abs() < 1e-9); - assert!((AC_SUB_FFN_001_SPIKE_RATIO - 3.0).abs() < 1e-9); - assert!((AC_SUB_FFN_001_NEIGHBOR_RATIO_LIMIT - 2.0).abs() < 1e-9); - assert_eq!(AC_SUB_FFN_006_QWEN_INTERMEDIATE_DIM, 18_944); - assert_eq!(AC_SUB_FFN_007_REQUIRED_HITS, 4); - assert_eq!(AC_SUB_FFN_008_NEW_FIELDS.len(), 4); - } -} diff --git a/crates/aprender-data/src/verification_specs.rs b/crates/aprender-data/src/verification_specs.rs deleted file mode 100644 index 5335494f8..000000000 --- a/crates/aprender-data/src/verification_specs.rs +++ /dev/null @@ -1,388 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } - - #[test] - fn test_validate_slice_bounds() { - assert!(buffer_contracts::validate_slice_bounds(10, 0, 5)); - assert!(buffer_contracts::validate_slice_bounds(10, 5, 5)); - assert!(!buffer_contracts::validate_slice_bounds(10, 5, 6)); - assert!(!buffer_contracts::validate_slice_bounds(10, 11, 0)); - // Overflow case - assert!(!buffer_contracts::validate_slice_bounds(10, usize::MAX, 1)); - } - - #[test] - fn test_is_aligned() { - assert!(buffer_contracts::is_aligned(0, 8)); - assert!(buffer_contracts::is_aligned(8, 8)); - assert!(buffer_contracts::is_aligned(16, 8)); - assert!(!buffer_contracts::is_aligned(7, 8)); - assert!(!buffer_contracts::is_aligned(1, 4)); - } - - #[test] - fn test_padding_for_alignment() { - assert_eq!(buffer_contracts::padding_for_alignment(0, 8), 0); - assert_eq!(buffer_contracts::padding_for_alignment(1, 8), 7); - assert_eq!(buffer_contracts::padding_for_alignment(7, 8), 1); - assert_eq!(buffer_contracts::padding_for_alignment(8, 8), 0); - assert_eq!(buffer_contracts::padding_for_alignment(9, 8), 7); - } - - #[test] - fn test_validate_magic() { - let magic = b"ALIM"; - let data = b"ALIMextra"; - assert!(integrity_contracts::validate_magic(data, magic)); - assert!(!integrity_contracts::validate_magic(b"BLIM", magic)); - assert!(!integrity_contracts::validate_magic(b"AL", magic)); - } - - #[test] - fn test_validate_version() { - assert!(integrity_contracts::validate_version(1, 1, 3)); - assert!(integrity_contracts::validate_version(3, 1, 3)); - assert!(!integrity_contracts::validate_version(0, 1, 3)); - assert!(!integrity_contracts::validate_version(4, 1, 3)); - } - - #[test] - fn test_xor_checksum() { - assert_eq!(integrity_contracts::xor_checksum(&[0xFF, 0xFF]), 0); - assert_eq!(integrity_contracts::xor_checksum(&[0xAA]), 0xAA); - // Deterministic - let data = &[1, 2, 3, 4, 5]; - assert_eq!( - integrity_contracts::xor_checksum(data), - integrity_contracts::xor_checksum(data) - ); - } - - // Negative tests: verify contract violations are caught - - #[test] - #[should_panic(expected = "data must not be empty")] - fn test_validated_len_rejects_empty() { - config_contracts::validated_len(&[]); - } - - #[test] - #[should_panic(expected = "max must be greater than min")] - fn test_normalize_rejects_invalid_range() { - numeric_contracts::normalize(5.0, 10.0, 0.0); - } - - #[test] - #[should_panic(expected = "alignment must be power of two")] - fn test_alignment_rejects_non_power_of_two() { - buffer_contracts::padding_for_alignment(10, 3); - } - - #[test] - fn test_from_vec_rejects_mismatched_shape() { - use crate::tensor::TensorData; - let result = TensorData::::from_vec(vec![1.0, 2.0, 3.0], 2, 2); - assert!(result.is_err()); - } -} - -/// Buffer and memory safety invariants -/// -/// #[invariant(self.capacity >= self.len)] -/// #[requires(offset + len <= buffer.len())] -/// #[ensures(result.len() == len)] -pub mod buffer_contracts { - /// Validate buffer slice bounds - /// - /// #[requires(buffer.len() > 0)] - /// #[requires(offset <= buffer.len())] - /// #[ensures(result == true ==> offset + len <= buffer.len())] - /// #[ensures(result == false ==> offset + len > buffer.len())] - pub fn validate_slice_bounds(buffer_len: usize, offset: usize, len: usize) -> bool { - offset.checked_add(len).map_or(false, |end| end <= buffer_len) - } - - /// Validate alignment for typed access - /// - /// #[requires(alignment > 0)] - /// #[requires(alignment.is_power_of_two())] - /// #[ensures(result == true ==> addr % alignment == 0)] - pub fn is_aligned(addr: usize, alignment: usize) -> bool { - debug_assert!(alignment.is_power_of_two(), "alignment must be power of two"); - addr % alignment == 0 - } - - /// Calculate padding needed for alignment - /// - /// #[requires(alignment > 0)] - /// #[requires(alignment.is_power_of_two())] - /// #[ensures(result < alignment)] - /// #[ensures((current_len + result) % alignment == 0)] - pub fn padding_for_alignment(current_len: usize, alignment: usize) -> usize { - debug_assert!(alignment.is_power_of_two(), "alignment must be power of two"); - let remainder = current_len % alignment; - if remainder == 0 { 0 } else { alignment - remainder } - } -} - -/// Data integrity invariants for format operations -/// -/// #[invariant(self.checksum_valid)] -/// #[requires(data.len() > 0)] -/// #[ensures(result.len() == expected_len)] -pub mod integrity_contracts { - /// Validate magic bytes match expected header - /// - /// #[requires(data.len() >= magic.len())] - /// #[ensures(result == true ==> data[..magic.len()] == magic[..])] - pub fn validate_magic(data: &[u8], magic: &[u8]) -> bool { - data.len() >= magic.len() && data[..magic.len()] == *magic - } - - /// Validate version is within supported range - /// - /// #[requires(max_version >= min_version)] - /// #[ensures(result == true ==> version >= min_version && version <= max_version)] - pub fn validate_version(version: u32, min_version: u32, max_version: u32) -> bool { - version >= min_version && version <= max_version - } - - /// Calculate simple checksum (XOR-fold) - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result <= u8::MAX)] - pub fn xor_checksum(data: &[u8]) -> u8 { - data.iter().fold(0u8, |acc, &b| acc ^ b) - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - use super::*; - - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } - - #[kani::proof] - fn verify_slice_bounds_safety() { - let buf_len: usize = kani::any(); - let offset: usize = kani::any(); - let len: usize = kani::any(); - kani::assume(buf_len <= 4096); - kani::assume(offset <= 4096); - kani::assume(len <= 4096); - let valid = buffer_contracts::validate_slice_bounds(buf_len, offset, len); - if valid { - assert!(offset + len <= buf_len); - } - } - - #[kani::proof] - fn verify_alignment_padding() { - let current: usize = kani::any(); - kani::assume(current <= 4096); - let alignment: usize = 8; // Common alignment - let pad = buffer_contracts::padding_for_alignment(current, alignment); - assert!(pad < alignment); - assert!((current + pad) % alignment == 0); - } - - #[kani::proof] - fn verify_normalize_bounds() { - let val: u8 = kani::any(); - let result = numeric_contracts::normalize(f64::from(val), 0.0, 255.0); - assert!(result >= 0.0); - assert!(result <= 1.0); - } - - #[kani::proof] - fn verify_xor_checksum_deterministic() { - let a: u8 = kani::any(); - let b: u8 = kani::any(); - let data = [a, b]; - let c1 = integrity_contracts::xor_checksum(&data); - let c2 = integrity_contracts::xor_checksum(&data); - assert_eq!(c1, c2); - } - - #[kani::proof] - fn verify_magic_validation() { - let magic: [u8; 4] = [0x41, 0x4C, 0x49, 0x4D]; // "ALIM" - let mut data = [0u8; 8]; - data[0] = magic[0]; - data[1] = magic[1]; - data[2] = magic[2]; - data[3] = magic[3]; - assert!(integrity_contracts::validate_magic(&data, &magic)); - } -} diff --git a/crates/aprender-db/src/generated_contracts.rs b/crates/aprender-db/src/generated_contracts.rs deleted file mode 100644 index 860b0bf80..000000000 --- a/crates/aprender-db/src/generated_contracts.rs +++ /dev/null @@ -1,8 +0,0 @@ -// Stub — contract macros for crates.io builds. -// Full version generated by: pv codegen contracts/ -o src/generated_contracts.rs -macro_rules! contract_pre_configuration { - () => {{}}; - ($i:expr) => {{ - let _ = &$i; - }}; -} diff --git a/crates/aprender-db/src/verification_specs.rs b/crates/aprender-db/src/verification_specs.rs deleted file mode 100644 index f7015fb65..000000000 --- a/crates/aprender-db/src/verification_specs.rs +++ /dev/null @@ -1,184 +0,0 @@ -//! Formal Verification Specifications for trueno-db -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. -//! -//! When Verus is available, these can be mechanically verified. -//! Without Verus, they serve as checked documentation via debug_assert!(). - -/// Configuration validation invariants -/// -/// # Verification Specifications -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate that a size parameter is within acceptable bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate that an index is within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice invariant - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric invariants for computation safety -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition that checks for overflow - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate that a float value is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize a value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - assert_eq!(config_contracts::validated_len(&[0]), 1); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - assert!((numeric_contracts::normalize(5.0, 0.0, 10.0) - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-distribute/src/verification_specs.rs b/crates/aprender-distribute/src/verification_specs.rs deleted file mode 100644 index ea81a2f85..000000000 --- a/crates/aprender-distribute/src/verification_specs.rs +++ /dev/null @@ -1,179 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-graph/src/verification_specs.rs b/crates/aprender-graph/src/verification_specs.rs deleted file mode 100644 index 9c077854e..000000000 --- a/crates/aprender-graph/src/verification_specs.rs +++ /dev/null @@ -1,184 +0,0 @@ -//! Formal Verification Specifications for trueno-graph -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. -//! -//! When Verus is available, these can be mechanically verified. -//! Without Verus, they serve as checked documentation via debug_assert!(). - -/// Configuration validation invariants -/// -/// # Verification Specifications -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate that a size parameter is within acceptable bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate that an index is within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice invariant - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric invariants for computation safety -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition that checks for overflow - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate that a float value is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize a value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - assert_eq!(config_contracts::validated_len(&[0]), 1); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - assert!((numeric_contracts::normalize(5.0, 0.0, 10.0) - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-orchestrate/src/verification_specs.rs b/crates/aprender-orchestrate/src/verification_specs.rs deleted file mode 100644 index 6a54074c1..000000000 --- a/crates/aprender-orchestrate/src/verification_specs.rs +++ /dev/null @@ -1,308 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -// ─── Verus Formal Verification Specs ───────────────────────────── -// Domain: batuta - stack ordering, version bounds, dependency counts -// Machine-checkable pre/postconditions for release management safety. - -#[cfg(verus)] -mod verus_specs { - use builtin::*; - use builtin_macros::*; - - verus! { - // ── Dependency ordering verification ── - - #[requires(dep_index < total_deps)] - #[ensures(result == dep_index)] - fn verify_dep_order_index(dep_index: u64, total_deps: u64) -> u64 { dep_index } - - #[requires(num_crates > 0)] - #[ensures(result <= num_crates)] - #[invariant(published <= num_crates)] - fn verify_publish_progress(published: u64, num_crates: u64) -> u64 { published } - - #[requires(order_len > 0)] - #[ensures(result == (position < order_len))] - #[decreases(order_len - position)] - fn verify_topo_position(position: u64, order_len: u64) -> bool { - position < order_len - } - - // ── Semantic version verification ── - - #[requires(major <= 999 && minor <= 999 && patch <= 999)] - #[ensures(result > 0)] - fn verify_semver_encoding(major: u64, minor: u64, patch: u64) -> u64 { - major * 1_000_000 + minor * 1_000 + patch + 1 - } - - #[requires(old_version > 0)] - #[ensures(result > old_version)] - #[recommends(result == old_version + 1)] - fn verify_version_bump(old_version: u64, new_version: u64) -> u64 { - new_version - } - - #[ensures(result == (new_major > old_major - || (new_major == old_major && new_minor > old_minor) - || (new_major == old_major && new_minor == old_minor && new_patch > old_patch)))] - fn verify_version_greater( - old_major: u64, old_minor: u64, old_patch: u64, - new_major: u64, new_minor: u64, new_patch: u64, - ) -> bool { - new_major > old_major - || (new_major == old_major && new_minor > old_minor) - || (new_major == old_major && new_minor == old_minor && new_patch > old_patch) - } - - // ── Dependency count verification ── - - #[requires(direct_deps >= 0)] - #[ensures(result >= direct_deps)] - #[recommends(direct_deps <= 50)] - fn verify_dep_count(direct_deps: u64, transitive_deps: u64) -> u64 { - direct_deps + transitive_deps - } - - #[requires(total > 0)] - #[ensures(result <= 100)] - fn verify_dep_ratio(outdated: u64, total: u64) -> u64 { - (outdated * 100) / total - } - - // ── Stack release verification ── - - #[requires(num_crates > 0)] - #[ensures(result == (succeeded == num_crates))] - #[invariant(succeeded <= num_crates)] - fn verify_release_complete(succeeded: u64, num_crates: u64) -> bool { - succeeded == num_crates - } - - #[requires(crate_index < stack_size)] - #[ensures(result == true)] - #[recommends(stack_size <= 10)] - fn verify_crate_in_stack(crate_index: u64, stack_size: u64) -> bool { - crate_index < stack_size - } - - // ── Version drift verification ── - - #[ensures(result == (actual_major == expected_major && actual_minor == expected_minor))] - fn verify_no_version_drift( - actual_major: u64, actual_minor: u64, - expected_major: u64, expected_minor: u64, - ) -> bool { - actual_major == expected_major && actual_minor == expected_minor - } - - #[requires(drift_count >= 0)] - #[ensures(result == (drift_count == 0))] - #[recommends(drift_count == 0)] - fn verify_zero_drift(drift_count: u64) -> bool { - drift_count == 0 - } - - // ── License audit verification ── - - #[requires(num_crates > 0)] - #[ensures(result == (denied == 0))] - fn verify_license_compliance(denied: u64) -> bool { - denied == 0 - } - - // ── Publish ordering DAG verification ── - - #[requires(edges >= 0)] - #[ensures(result == (edges < nodes))] - #[invariant(nodes > 0)] - fn verify_dag_acyclic_hint(nodes: u64, edges: u64) -> bool { - edges < nodes - } - - #[requires(in_degree >= 0)] - #[ensures(result == (in_degree == 0))] - #[decreases(remaining_nodes)] - fn verify_topo_sort_ready(in_degree: u64, remaining_nodes: u64) -> bool { - in_degree == 0 - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-profile/src/verification_specs.rs b/crates/aprender-profile/src/verification_specs.rs deleted file mode 100644 index ea81a2f85..000000000 --- a/crates/aprender-profile/src/verification_specs.rs +++ /dev/null @@ -1,179 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-rag/src/verification_specs.rs b/crates/aprender-rag/src/verification_specs.rs deleted file mode 100644 index c788bafbd..000000000 --- a/crates/aprender-rag/src/verification_specs.rs +++ /dev/null @@ -1,184 +0,0 @@ -//! Formal Verification Specifications for trueno-rag -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. -//! -//! When Verus is available, these can be mechanically verified. -//! Without Verus, they serve as checked documentation via debug_assert!(). - -/// Configuration validation invariants -/// -/// # Verification Specifications -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate that a size parameter is within acceptable bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate that an index is within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice invariant - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric invariants for computation safety -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition that checks for overflow - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate that a float value is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize a value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - assert_eq!(config_contracts::validated_len(&[0]), 1); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - assert!((numeric_contracts::normalize(5.0, 0.0, 10.0) - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-registry/src/verification_specs.rs b/crates/aprender-registry/src/verification_specs.rs deleted file mode 100644 index 7315a6bac..000000000 --- a/crates/aprender-registry/src/verification_specs.rs +++ /dev/null @@ -1,347 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Hash and content-addressing invariants -/// -/// #[invariant(hash.len() == 32)] -/// #[requires(data.len() > 0)] -/// #[ensures(result.len() == 64)] // hex-encoded -/// #[ensures(hash(data) == hash(data))] // deterministic -pub mod hash_contracts { - /// Validate that a hex-encoded hash has the expected length - /// - /// #[requires(hex_str.len() > 0)] - /// #[ensures(result == true ==> hex_str.len() == 64)] - /// #[ensures(result == true ==> hex_str.chars().all(|c| c.is_ascii_hexdigit()))] - pub fn validate_blake3_hex(hex_str: &str) -> bool { - hex_str.len() == 64 && hex_str.chars().all(|c| c.is_ascii_hexdigit()) - } - - /// Validate raw hash bytes length - /// - /// #[requires(hash_bytes.len() > 0)] - /// #[ensures(result == true ==> hash_bytes.len() == 32)] - pub fn validate_hash_bytes(hash_bytes: &[u8]) -> bool { - hash_bytes.len() == 32 - } -} - -/// Version ordering invariants -/// -/// #[invariant(major >= 0 && minor >= 0 && patch >= 0)] -/// #[ensures(v1 < v2 ==> v1.major < v2.major || (v1.major == v2.major && v1.minor < v2.minor) || ...)] -/// #[ensures(bump_major(v) > v)] -/// #[ensures(bump_minor(v) > v)] -/// #[ensures(bump_patch(v) > v)] -pub mod version_contracts { - /// Validate semantic version components are reasonable - /// - /// #[requires(major <= 999 && minor <= 999 && patch <= 999)] - /// #[ensures(result == true ==> major <= 999)] - pub fn validate_semver(major: u32, minor: u32, patch: u32) -> bool { - major <= 999 && minor <= 999 && patch <= 999 - } - - /// Compare two versions, returning ordering - /// - /// #[ensures(result == Ordering::Equal ==> a_major == b_major && a_minor == b_minor && a_patch == b_patch)] - /// #[ensures(result == Ordering::Less ==> !(a_major > b_major))] - pub fn compare_versions( - a_major: u32, - a_minor: u32, - a_patch: u32, - b_major: u32, - b_minor: u32, - b_patch: u32, - ) -> std::cmp::Ordering { - (a_major, a_minor, a_patch).cmp(&(b_major, b_minor, b_patch)) - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } - - #[test] - fn test_validate_blake3_hex() { - let hash = blake3::hash(b"hello"); - let hex = hash.to_hex().to_string(); - assert!(hash_contracts::validate_blake3_hex(&hex)); - assert!(!hash_contracts::validate_blake3_hex("too_short")); - assert!(!hash_contracts::validate_blake3_hex( - "zzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz" - )); - } - - #[test] - fn test_validate_hash_bytes() { - let hash = blake3::hash(b"hello"); - assert!(hash_contracts::validate_hash_bytes(hash.as_bytes())); - assert!(!hash_contracts::validate_hash_bytes(&[0u8; 16])); - } - - #[test] - fn test_validate_semver() { - assert!(version_contracts::validate_semver(1, 0, 0)); - assert!(version_contracts::validate_semver(999, 999, 999)); - assert!(!version_contracts::validate_semver(1000, 0, 0)); - } - - #[test] - fn test_compare_versions() { - use std::cmp::Ordering; - assert_eq!( - version_contracts::compare_versions(1, 0, 0, 1, 0, 0), - Ordering::Equal - ); - assert_eq!( - version_contracts::compare_versions(1, 0, 0, 2, 0, 0), - Ordering::Less - ); - assert_eq!( - version_contracts::compare_versions(1, 1, 0, 1, 0, 0), - Ordering::Greater - ); - assert_eq!( - version_contracts::compare_versions(1, 0, 1, 1, 0, 0), - Ordering::Greater - ); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } - - #[kani::proof] - fn verify_normalize_bounds() { - let val: i32 = kani::any(); - let min: i32 = kani::any(); - let max: i32 = kani::any(); - kani::assume(min < max); - kani::assume(max - min > 0); // no overflow - let range = (max - min) as f64; - let normalized = ((val - min) as f64 / range).clamp(0.0, 1.0); - assert!(normalized >= 0.0 && normalized <= 1.0); - } - - #[kani::proof] - fn verify_checked_sub_no_underflow() { - let a: u64 = kani::any(); - let b: u64 = kani::any(); - kani::assume(a >= b); - let result = a.checked_sub(b); - assert!(result.is_some()); - assert!(result.expect("verified") <= a); - } - - #[kani::proof] - fn verify_version_ordering() { - let major: u32 = kani::any(); - let minor: u32 = kani::any(); - let patch: u32 = kani::any(); - kani::assume(major <= 100); - kani::assume(minor <= 100); - kani::assume(patch <= 100); - // Semantic version encoding must be monotonically orderable - let encoded = (major as u64) * 1_000_000 + (minor as u64) * 1_000 + patch as u64; - let encoded2 = ((major + 1) as u64) * 1_000_000 + (minor as u64) * 1_000 + patch as u64; - assert!(encoded2 > encoded); - } - - #[kani::proof] - fn verify_blake3_hash_length() { - // BLAKE3 always produces 32-byte output - let input: [u8; 4] = kani::any(); - let hash = blake3::hash(&input); - assert!(hash.as_bytes().len() == 32); - } - - #[kani::proof] - fn verify_semver_comparison_reflexive() { - let major: u32 = kani::any(); - let minor: u32 = kani::any(); - let patch: u32 = kani::any(); - kani::assume(major <= 100); - kani::assume(minor <= 100); - kani::assume(patch <= 100); - let ord = super::version_contracts::compare_versions( - major, minor, patch, major, minor, patch, - ); - assert!(ord == std::cmp::Ordering::Equal); - } - - #[kani::proof] - fn verify_hex_validation_length() { - // Any 64-char all-hex string must pass validation - let valid = "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef"; - assert!(super::hash_contracts::validate_blake3_hex(valid)); - } -} diff --git a/crates/aprender-serve/src/verification_specs.rs b/crates/aprender-serve/src/verification_specs.rs deleted file mode 100644 index 1eea48a97..000000000 --- a/crates/aprender-serve/src/verification_specs.rs +++ /dev/null @@ -1,318 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.expect("expected value").max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.expect("expected value").max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.expect("expected value") == a + b)] - /// #[ensures(result.is_some() ==> result.expect("expected value") >= a)] - /// #[ensures(result.is_some() ==> result.expect("expected value") >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -// ─── Verus Formal Verification Specs ───────────────────────────── -// Domain: realizar - inference state, KV cache bounds, token limits -// Machine-checkable pre/postconditions for LLM inference safety. - -#[cfg(verus)] -mod verus_specs { - use builtin::*; - use builtin_macros::*; - - verus! { - // ── KV cache bounds verification ── - - #[requires(seq_len >= 0)] - #[ensures(result == (seq_len < max_seq_len))] - #[recommends(max_seq_len >= 2048)] - fn verify_kv_cache_capacity(seq_len: u64, max_seq_len: u64) -> bool { - seq_len < max_seq_len - } - - #[requires(num_layers > 0 && num_heads > 0 && head_dim > 0)] - #[ensures(result == num_layers * num_heads * head_dim * max_seq_len * 2)] - fn verify_kv_cache_size( - num_layers: u64, num_heads: u64, head_dim: u64, max_seq_len: u64, - ) -> u64 { - num_layers * num_heads * head_dim * max_seq_len * 2 - } - - #[requires(pos >= 0)] - #[ensures(result == pos + 1)] - #[invariant(pos < max_seq_len)] - fn verify_kv_cache_advance(pos: u64, max_seq_len: u64) -> u64 { - pos + 1 - } - - // ── Token generation verification ── - - #[requires(generated >= 0)] - #[ensures(result == (generated < max_tokens))] - #[recommends(max_tokens <= 4096)] - fn verify_token_budget(generated: u64, max_tokens: u64) -> bool { - generated < max_tokens - } - - #[requires(token_id >= 0)] - #[ensures(result == (token_id < vocab_size))] - fn verify_token_id(token_id: u64, vocab_size: u64) -> bool { - token_id < vocab_size - } - - #[requires(prompt_len > 0)] - #[ensures(result == prompt_len + max_new_tokens)] - #[recommends(prompt_len + max_new_tokens <= 131072)] - fn verify_total_sequence_len(prompt_len: u64, max_new_tokens: u64) -> u64 { - prompt_len + max_new_tokens - } - - // ── Attention verification ── - - #[requires(seq_len > 0 && head_dim > 0)] - #[ensures(result == seq_len * head_dim)] - fn verify_attention_buffer_size(seq_len: u64, head_dim: u64) -> u64 { - seq_len * head_dim - } - - #[requires(num_q_heads > 0 && num_kv_heads > 0)] - #[ensures(result == num_q_heads / num_kv_heads)] - #[invariant(num_q_heads % num_kv_heads == 0)] - fn verify_gqa_ratio(num_q_heads: u64, num_kv_heads: u64) -> u64 { - num_q_heads / num_kv_heads - } - - #[requires(head_dim > 0)] - #[ensures(result > 0)] - fn verify_attention_scale(head_dim: u64) -> u64 { - head_dim // sqrt(head_dim) in actual computation - } - - // ── Sampling verification ── - - #[requires(logits_len > 0)] - #[ensures(result < logits_len)] - fn verify_sampled_token(result_idx: u64, logits_len: u64) -> u64 { result_idx } - - #[requires(top_k > 0)] - #[ensures(result <= vocab_size)] - #[recommends(top_k <= 100)] - fn verify_top_k_bounds(top_k: u64, vocab_size: u64) -> u64 { - if top_k > vocab_size { vocab_size } else { top_k } - } - - #[requires(top_p > 0)] - #[ensures(result == (top_p <= 100))] - #[recommends(top_p >= 80 && top_p <= 100)] - fn verify_top_p_bounds(top_p: u64) -> bool { - top_p <= 100 - } - - // ── Model loading verification ── - - #[requires(num_tensors > 0)] - #[ensures(result == (loaded == num_tensors))] - #[invariant(loaded <= num_tensors)] - fn verify_model_load_complete(loaded: u64, num_tensors: u64) -> bool { - loaded == num_tensors - } - - #[requires(expected_size > 0)] - #[ensures(result == (actual_size == expected_size))] - fn verify_tensor_size_match(actual_size: u64, expected_size: u64) -> bool { - actual_size == expected_size - } - - // ── Throughput verification ── - - #[requires(elapsed_ms > 0)] - #[ensures(result == (tokens_generated * 1000) / elapsed_ms)] - #[recommends(result >= 30)] - fn verify_tokens_per_second(tokens_generated: u64, elapsed_ms: u64) -> u64 { - (tokens_generated * 1000) / elapsed_ms - } - - // ── RoPE position verification ── - - #[requires(pos >= 0)] - #[ensures(result == (pos < max_pos))] - #[invariant(max_pos > 0)] - fn verify_rope_position(pos: u64, max_pos: u64) -> bool { - pos < max_pos - } - - #[requires(dim > 0 && dim % 2 == 0)] - #[ensures(result == dim / 2)] - #[decreases(dim)] - fn verify_rope_pairs(dim: u64) -> u64 { - dim / 2 - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-train/src/verification_specs.rs b/crates/aprender-train/src/verification_specs.rs deleted file mode 100644 index 533fb4acd..000000000 --- a/crates/aprender-train/src/verification_specs.rs +++ /dev/null @@ -1,300 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.expect("ok").max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.expect("ok").max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.expect("some") == a + b)] - /// #[ensures(result.is_some() ==> result.expect("some") >= a)] - /// #[ensures(result.is_some() ==> result.expect("some") >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } - - // ── C-SHARD-001: File-level shard disjointness + completeness ── - - /// Prove: shard assignment via modular arithmetic is disjoint. - /// For any two distinct ranks r1, r2 and any file index i: - /// i % world_size == r1 AND i % world_size == r2 ⟹ r1 == r2 - #[kani::proof] - fn verify_shard_disjointness() { - let world_size: usize = kani::any(); - kani::assume(world_size >= 1 && world_size <= 8); - let file_idx: usize = kani::any(); - kani::assume(file_idx < 64); - let assigned_rank = file_idx % world_size; - // Verify: only one rank owns this file - assert!(assigned_rank < world_size); - // For any other rank, they don't get this file - let other_rank: usize = kani::any(); - kani::assume(other_rank < world_size && other_rank != assigned_rank); - assert!(file_idx % world_size != other_rank); - } - - /// Prove: shard assignment is complete (every file assigned to exactly one worker). - /// For any file index i with i < num_files and world_size > 0: - /// ∃! rank ∈ [0, world_size): i % world_size == rank - #[kani::proof] - fn verify_shard_completeness() { - let world_size: usize = kani::any(); - kani::assume(world_size >= 1 && world_size <= 8); - let file_idx: usize = kani::any(); - kani::assume(file_idx < 64); - let rank = file_idx % world_size; - // Completeness: rank is valid - assert!(rank < world_size); - // Uniqueness: no other rank in [0, world_size) maps to same value - // (follows from modular arithmetic, but let's verify) - assert_eq!(file_idx % world_size, rank); - } - - // ── C-DDP-001: Gradient accumulation indexing ── - - /// Prove: block gradient indexing stays in bounds. - /// For any block_idx < num_blocks, accessing block_grads[block_idx] is safe. - #[kani::proof] - fn verify_block_gradient_indexing() { - let num_blocks: usize = kani::any(); - kani::assume(num_blocks >= 1 && num_blocks <= 32); - let block_idx: usize = kani::any(); - kani::assume(block_idx < num_blocks); - // Simulate Vec access bounds check - assert!(block_idx < num_blocks); - // 9 components per block (C-DDP-001) - let num_components: usize = 9; - let component_idx: usize = kani::any(); - kani::assume(component_idx < num_components); - let flat_idx = block_idx * num_components + component_idx; - assert!(flat_idx < num_blocks * num_components); - } - - // ── C-RING-001: Ring AllReduce invariants ── - - /// Prove: ring AllReduce chunk indexing is safe. - /// For world_size workers, each worker processes world_size-1 chunks. - #[kani::proof] - fn verify_ring_allreduce_chunks() { - let world_size: usize = kani::any(); - kani::assume(world_size >= 2 && world_size <= 8); - let data_len: usize = kani::any(); - kani::assume(data_len >= world_size && data_len <= 128); - - let chunk_size = (data_len + world_size - 1) / world_size; - // Verify: chunks cover entire buffer - assert!(chunk_size * world_size >= data_len); - - // Verify: each rank's chunk start is in bounds - let rank: usize = kani::any(); - kani::assume(rank < world_size); - let chunk_start = rank * chunk_size; - let chunk_end = (chunk_start + chunk_size).min(data_len); - assert!(chunk_start <= data_len); - assert!(chunk_end <= data_len); - assert!(chunk_end >= chunk_start); - } - - /// Prove: ring send/recv partner calculation is valid. - /// In a ring of N workers, worker i sends to (i+1)%N and receives from (i-1+N)%N. - #[kani::proof] - fn verify_ring_partners() { - let world_size: usize = kani::any(); - kani::assume(world_size >= 2 && world_size <= 8); - let rank: usize = kani::any(); - kani::assume(rank < world_size); - - let send_to = (rank + 1) % world_size; - let recv_from = (rank + world_size - 1) % world_size; - - // Both partners are valid ranks - assert!(send_to < world_size); - assert!(recv_from < world_size); - // No self-loop in ring (since world_size >= 2) - assert!(send_to != rank); - assert!(recv_from != rank); - // Ring is bidirectional: if i sends to j, then j receives from i - let j_recv = (send_to + world_size - 1) % world_size; - assert_eq!(j_recv, rank); - } - - // ── C-WIRE-002: Wire protocol tag uniqueness ── - - /// Prove: wire message tags are unique (no two message types share a tag). - #[kani::proof] - fn verify_wire_tag_uniqueness() { - // Tags are: 0x01..0x0B (11 tags total) - let tag: u8 = kani::any(); - kani::assume(tag >= 0x01 && tag <= 0x0B); - // Each tag maps to exactly one message type — proven by exhaustive match - // This verifies the tag space is contiguous and non-overlapping - assert!(tag >= 0x01); - assert!(tag <= 0x0B); - // No gaps: tags are 1,2,3,4,5,6,7,8,9,10,11 - assert!(tag <= 11); - } -} diff --git a/crates/aprender-verify/src/verification_specs.rs b/crates/aprender-verify/src/verification_specs.rs deleted file mode 100644 index 19a8c844c..000000000 --- a/crates/aprender-verify/src/verification_specs.rs +++ /dev/null @@ -1,324 +0,0 @@ -//! Formal Verification Specifications -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. - -/// Configuration validation invariants -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate size parameter is within bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - contract_pre_configuration!(); - let result = size <= max; - contract_post_configuration!(&"ok"); - result - } - - /// Validate index within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - contract_pre_configuration!(); - index < len - } - - /// Validate non-empty slice - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric computation safety invariants -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition with overflow check - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate float is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -// ─── Verus Formal Verification Specs ───────────────────────────── -// Domain: certeza - test coverage, mutation scores, quality thresholds -// These specs are compiled only under cfg(verus) and provide machine-checkable -// pre/postconditions for critical quality-gate invariants. - -#[cfg(verus)] -mod verus_specs { - use builtin::*; - use builtin_macros::*; - - verus! { - // ── Coverage threshold verification ── - - #[requires(covered_lines <= total_lines)] - #[ensures(result <= 100)] - fn verify_coverage_percentage(covered_lines: u64, total_lines: u64) -> u64 { - if total_lines == 0 { 100 } else { (covered_lines * 100) / total_lines } - } - - #[requires(coverage_pct <= 100)] - #[ensures(result == (coverage_pct >= threshold))] - fn verify_coverage_gate(coverage_pct: u64, threshold: u64) -> bool { - coverage_pct >= threshold - } - - #[requires(threshold >= 0 && threshold <= 100)] - #[ensures(result >= 0 && result <= 100)] - #[recommends(threshold >= 95)] - fn verify_minimum_coverage_threshold(threshold: u64) -> u64 { threshold } - - // ── Mutation score verification ── - - #[requires(killed_mutants <= total_mutants)] - #[ensures(result <= 100)] - fn verify_mutation_score(killed_mutants: u64, total_mutants: u64) -> u64 { - if total_mutants == 0 { 100 } else { (killed_mutants * 100) / total_mutants } - } - - #[requires(mutation_score <= 100)] - #[ensures(result == (mutation_score >= 80))] - #[recommends(mutation_score >= 85)] - fn verify_mutation_gate(mutation_score: u64) -> bool { - mutation_score >= 80 - } - - #[requires(survived >= 0)] - #[ensures(result == killed + survived)] - fn verify_mutant_total(killed: u64, survived: u64) -> u64 { - killed + survived - } - - // ── Quality grade verification ── - - #[requires(score <= 134)] - #[ensures(result <= 4)] - fn verify_quality_grade(score: u64) -> u64 { - if score >= 120 { 0 } // A+ - else if score >= 100 { 1 } // A - else if score >= 80 { 2 } // B - else if score >= 60 { 3 } // C - else { 4 } // D - } - - #[requires(grade <= 4)] - #[ensures(result == (grade <= max_allowed))] - fn verify_grade_gate(grade: u64, max_allowed: u64) -> bool { - grade <= max_allowed - } - - // ── TDG score verification ── - - #[requires(tdg_score >= 0 && tdg_score <= 100)] - #[ensures(result == (tdg_score >= 95))] - #[recommends(tdg_score >= 95)] - fn verify_tdg_gate(tdg_score: u64) -> bool { - tdg_score >= 95 - } - - #[requires(components > 0)] - #[ensures(result <= 100)] - #[invariant(sum <= components * 100)] - fn verify_tdg_aggregate(sum: u64, components: u64) -> u64 { - sum / components - } - - // ── Complexity verification ── - - #[requires(complexity > 0)] - #[ensures(result == (complexity <= 10))] - #[recommends(complexity <= 10)] - fn verify_complexity_gate(complexity: u64) -> bool { - complexity <= 10 - } - - #[requires(num_functions > 0)] - #[ensures(result <= max_complexity)] - #[decreases(num_functions)] - fn verify_avg_complexity(total_complexity: u64, num_functions: u64, max_complexity: u64) -> u64 { - let avg = total_complexity / num_functions; - if avg > max_complexity { max_complexity } else { avg } - } - - // ── SATD (self-admitted technical debt) verification ── - - #[ensures(result == (count == 0))] - #[recommends(count == 0)] - fn verify_zero_satd(count: u64) -> bool { - count == 0 - } - - // ── Test count verification ── - - #[requires(unit + property + integration == total)] - #[ensures(result == total)] - #[invariant(unit <= total && property <= total && integration <= total)] - fn verify_test_count(unit: u64, property: u64, integration: u64, total: u64) -> u64 { - total - } - - #[requires(total > 0)] - #[ensures(result <= 100)] - fn verify_test_ratio(category_count: u64, total: u64) -> u64 { - (category_count * 100) / total - } - - // ── Security audit verification ── - - #[ensures(result == (vulnerabilities == 0))] - #[recommends(vulnerabilities == 0)] - fn verify_security_gate(vulnerabilities: u64) -> bool { - vulnerabilities == 0 - } - - #[requires(severity <= 4)] - #[ensures(result == (severity == 0))] - fn verify_no_critical_vulns(severity: u64) -> bool { - severity == 0 - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - let result = numeric_contracts::normalize(5.0, 0.0, 10.0); - assert!((result - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -} diff --git a/crates/aprender-viz/src/verification_specs.rs b/crates/aprender-viz/src/verification_specs.rs deleted file mode 100644 index 80505a288..000000000 --- a/crates/aprender-viz/src/verification_specs.rs +++ /dev/null @@ -1,184 +0,0 @@ -//! Formal Verification Specifications for trueno-viz -//! -//! Design-by-contract specifications using Verus-style pre/postconditions. -//! These serve as both documentation and verification targets. -//! -//! When Verus is available, these can be mechanically verified. -//! Without Verus, they serve as checked documentation via debug_assert!(). - -/// Configuration validation invariants -/// -/// # Verification Specifications -/// -/// #[requires(max_size > 0)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size == max_size)] -/// #[ensures(result.is_ok() ==> result.unwrap().max_size > 0)] -/// #[ensures(max_size == 0 ==> result.is_err())] -/// #[invariant(self.max_size > 0)] -/// #[decreases(remaining)] -/// #[recommends(max_size <= 1_000_000)] -pub mod config_contracts { - /// Validate that a size parameter is within acceptable bounds - /// - /// #[requires(size > 0)] - /// #[ensures(result == true ==> size <= max)] - /// #[ensures(result == false ==> size > max)] - pub fn validate_size(size: usize, max: usize) -> bool { - size <= max - } - - /// Validate that an index is within bounds - /// - /// #[requires(len > 0)] - /// #[ensures(result == true ==> index < len)] - /// #[ensures(result == false ==> index >= len)] - pub fn validate_index(index: usize, len: usize) -> bool { - index < len - } - - /// Validate non-empty slice invariant - /// - /// #[requires(data.len() > 0)] - /// #[ensures(result == data.len())] - /// #[invariant(data.len() > 0)] - pub fn validated_len(data: &[u8]) -> usize { - debug_assert!(!data.is_empty(), "data must not be empty"); - data.len() - } -} - -/// Numeric invariants for computation safety -/// -/// #[invariant(self.value.is_finite())] -/// #[requires(a.is_finite() && b.is_finite())] -/// #[ensures(result.is_finite())] -/// #[decreases(iterations)] -/// #[recommends(iterations <= 10_000)] -pub mod numeric_contracts { - /// Safe addition that checks for overflow - /// - /// #[requires(a >= 0 && b >= 0)] - /// #[ensures(result.is_some() ==> result.unwrap() == a + b)] - /// #[ensures(result.is_some() ==> result.unwrap() >= a)] - /// #[ensures(result.is_some() ==> result.unwrap() >= b)] - pub fn checked_add(a: u64, b: u64) -> Option { - a.checked_add(b) - } - - /// Validate that a float value is usable (finite, non-NaN) - /// - /// #[ensures(result == true ==> val.is_finite())] - /// #[ensures(result == true ==> !val.is_nan())] - /// #[ensures(result == false ==> val.is_nan() || val.is_infinite())] - pub fn is_valid_float(val: f64) -> bool { - val.is_finite() - } - - /// Normalize a value to [0, 1] range - /// - /// #[requires(max > min)] - /// #[requires(val.is_finite() && min.is_finite() && max.is_finite())] - /// #[ensures(result >= 0.0 && result <= 1.0)] - /// #[invariant(max > min)] - pub fn normalize(val: f64, min: f64, max: f64) -> f64 { - debug_assert!(max > min, "max must be greater than min"); - ((val - min) / (max - min)).clamp(0.0, 1.0) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_validate_size() { - assert!(config_contracts::validate_size(5, 10)); - assert!(!config_contracts::validate_size(11, 10)); - assert!(config_contracts::validate_size(10, 10)); - } - - #[test] - fn test_validate_index() { - assert!(config_contracts::validate_index(0, 5)); - assert!(config_contracts::validate_index(4, 5)); - assert!(!config_contracts::validate_index(5, 5)); - } - - #[test] - fn test_validated_len() { - assert_eq!(config_contracts::validated_len(&[1, 2, 3]), 3); - assert_eq!(config_contracts::validated_len(&[0]), 1); - } - - #[test] - fn test_checked_add() { - assert_eq!(numeric_contracts::checked_add(1, 2), Some(3)); - assert_eq!(numeric_contracts::checked_add(u64::MAX, 1), None); - } - - #[test] - fn test_is_valid_float() { - assert!(numeric_contracts::is_valid_float(1.0)); - assert!(!numeric_contracts::is_valid_float(f64::NAN)); - assert!(!numeric_contracts::is_valid_float(f64::INFINITY)); - } - - #[test] - fn test_normalize() { - assert!((numeric_contracts::normalize(5.0, 0.0, 10.0) - 0.5).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(0.0, 0.0, 10.0)).abs() < f64::EPSILON); - assert!((numeric_contracts::normalize(10.0, 0.0, 10.0) - 1.0).abs() < f64::EPSILON); - } -} - -// ─── Kani Proof Stubs ──────────────────────────────────────────── -// Model-checking proofs for critical invariants -// Requires: cargo install --locked kani-verifier - -#[cfg(kani)] -mod kani_proofs { - #[kani::proof] - fn verify_config_bounds() { - let val: u32 = kani::any(); - kani::assume(val <= 1000); - assert!(val <= 1000); - } - - #[kani::proof] - fn verify_index_safety() { - let len: usize = kani::any(); - kani::assume(len > 0 && len <= 1024); - let idx: usize = kani::any(); - kani::assume(idx < len); - assert!(idx < len); - } - - #[kani::proof] - fn verify_no_overflow_add() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 10000); - kani::assume(b <= 10000); - let result = a.checked_add(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_no_overflow_mul() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - kani::assume(a <= 1000); - kani::assume(b <= 1000); - let result = a.checked_mul(b); - assert!(result.is_some()); - } - - #[kani::proof] - fn verify_division_nonzero() { - let numerator: u64 = kani::any(); - let denominator: u64 = kani::any(); - kani::assume(denominator > 0); - let result = numerator / denominator; - assert!(result <= numerator); - } -}