aprender-contracts 0.72.3

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation
use super::*;

fn test_entry(
    stem: &str,
    equations: Vec<&str>,
    obligs: usize,
    kani: usize,
) -> types::ContractEntry {
    types::ContractEntry {
        stem: stem.into(),
        path: format!("{stem}.yaml"),
        description: "desc".into(),
        equations: equations.into_iter().map(Into::into).collect(),
        obligation_types: vec![],
        properties: vec![],
        references: vec![],
        depends_on: vec![],
        is_registry: false,
        kind: Default::default(),
        obligation_count: obligs,
        falsification_count: 0,
        kani_count: kani,
        corpus_text: String::new(),
    }
}

#[test]
fn parse_iso_days_ago_valid_date() {
    let now = 1_767_225_600; // approx 2026-01-01 00:00 UTC
    let days = parse_iso_days_ago("2025-12-31", now);
    assert!(days <= 3, "Expected ~1 day, got {days}");
}

#[test]
fn parse_iso_days_ago_invalid_format() {
    // Empty and single-segment strings have < 3 parts → returns 0
    assert_eq!(parse_iso_days_ago("", 1_000_000), 0);
    assert_eq!(parse_iso_days_ago("2025", 1_000_000), 0);
    // "not-a-date" has 3 dash-separated parts but parse fails → doesn't panic
    let _ = parse_iso_days_ago("not-a-date", 1_000_000);
}

#[test]
fn parse_iso_days_ago_recent() {
    // Use a known epoch and date: 2025-01-02 vs now=2025-01-03
    let now = 1_735_862_400; // approx 2025-01-03 UTC
    let days = parse_iso_days_ago("2025-01-02", now);
    assert!(days <= 5, "Expected ~1 day, got {days}");
}

#[test]
fn month_days_boundaries() {
    assert_eq!(month_days(0), 0);
    assert_eq!(month_days(1), 0);
    assert_eq!(month_days(2), 31);
    assert_eq!(month_days(12), 334);
    assert_eq!(month_days(13), 0);
    assert_eq!(month_days(100), 0);
}

#[test]
fn parse_proof_level_all_variants() {
    assert_eq!(parse_proof_level("L1"), crate::proof_status::ProofLevel::L1);
    assert_eq!(parse_proof_level("L2"), crate::proof_status::ProofLevel::L2);
    assert_eq!(parse_proof_level("L3"), crate::proof_status::ProofLevel::L3);
    assert_eq!(parse_proof_level("L4"), crate::proof_status::ProofLevel::L4);
    assert_eq!(parse_proof_level("L5"), crate::proof_status::ProofLevel::L5);
}

#[test]
fn parse_proof_level_case_insensitive() {
    assert_eq!(parse_proof_level("l3"), crate::proof_status::ProofLevel::L3);
    assert_eq!(parse_proof_level("l5"), crate::proof_status::ProofLevel::L5);
}

#[test]
fn parse_proof_level_unknown_defaults_l1() {
    assert_eq!(parse_proof_level("L9"), crate::proof_status::ProofLevel::L1);
    assert_eq!(
        parse_proof_level("garbage"),
        crate::proof_status::ProofLevel::L1
    );
}

#[test]
fn filter_by_project_none_returns_all() {
    let sites = vec![
        CallSiteInfo {
            project: "alpha".into(),
            file: "a.rs".into(),
            line: 1,
            equation: Some("eq1".into()),
        },
        CallSiteInfo {
            project: "beta".into(),
            file: "b.rs".into(),
            line: 2,
            equation: Some("eq2".into()),
        },
    ];
    let result = filter_by_project(sites.clone(), None);
    assert_eq!(result.len(), 2);
}

#[test]
fn filter_by_project_some_filters() {
    let sites = vec![
        CallSiteInfo {
            project: "alpha".into(),
            file: "a.rs".into(),
            line: 1,
            equation: Some("eq1".into()),
        },
        CallSiteInfo {
            project: "beta".into(),
            file: "b.rs".into(),
            line: 2,
            equation: Some("eq2".into()),
        },
    ];
    let result = filter_by_project(sites, Some("alpha"));
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].project, "alpha");
}

#[test]
fn filter_by_project_no_match() {
    let sites = vec![CallSiteInfo {
        project: "alpha".into(),
        file: "a.rs".into(),
        line: 1,
        equation: Some("eq1".into()),
    }];
    let result = filter_by_project(sites, Some("gamma"));
    assert!(result.is_empty());
}

#[test]
fn filter_violations_none_returns_all() {
    let v = vec![
        ViolationInfo {
            project: "a".into(),
            kind: "gap".into(),
            detail: "d".into(),
        },
        ViolationInfo {
            project: "b".into(),
            kind: "gap".into(),
            detail: "d".into(),
        },
    ];
    let result = filter_violations(v, None);
    assert_eq!(result.len(), 2);
}

#[test]
fn filter_violations_some_filters() {
    let v = vec![
        ViolationInfo {
            project: "a".into(),
            kind: "gap".into(),
            detail: "d".into(),
        },
        ViolationInfo {
            project: "b".into(),
            kind: "gap".into(),
            detail: "d".into(),
        },
    ];
    let result = filter_violations(v, Some("a"));
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].project, "a");
}

#[test]
fn filter_coverage_none_returns_all() {
    let c = vec![
        ProjectCoverage {
            project: "x".into(),
            call_sites: 5,
            binding_refs: 2,
            binding_implemented: 1,
            binding_total: 2,
        },
        ProjectCoverage {
            project: "y".into(),
            call_sites: 3,
            binding_refs: 1,
            binding_implemented: 1,
            binding_total: 1,
        },
    ];
    let result = filter_coverage(c, None);
    assert_eq!(result.len(), 2);
}

#[test]
fn filter_coverage_some_filters() {
    let c = vec![
        ProjectCoverage {
            project: "x".into(),
            call_sites: 5,
            binding_refs: 2,
            binding_implemented: 1,
            binding_total: 2,
        },
        ProjectCoverage {
            project: "y".into(),
            call_sites: 3,
            binding_refs: 1,
            binding_implemented: 1,
            binding_total: 1,
        },
    ];
    let result = filter_coverage(c, Some("y"));
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].project, "y");
}

#[test]
fn build_call_sites_no_index() {
    let result = build_call_sites("softmax-kernel-v1", None);
    assert!(result.is_empty());
}

#[test]
fn build_violations_show_false() {
    let entry = test_entry("test", vec!["eq1"], 1, 0);
    let result = build_violations(&entry, None, false);
    assert!(result.is_empty());
}

#[test]
fn build_violations_show_true_no_index() {
    let entry = test_entry("test", vec!["eq1"], 1, 0);
    let result = build_violations(&entry, None, true);
    assert!(result.is_empty());
}

#[test]
fn build_coverage_map_show_false() {
    let result = build_coverage_map("test", None, false);
    assert!(result.is_empty());
}

#[test]
fn build_coverage_map_show_true_no_index() {
    let result = build_coverage_map("test", None, true);
    assert!(result.is_empty());
}

#[test]
fn build_binding_info_no_registry() {
    let entry = test_entry("test", vec!["alpha", "beta"], 0, 0);
    let result = build_binding_info(&entry, None);
    assert_eq!(result.len(), 2);
    assert_eq!(result[0].equation, "alpha");
    assert_eq!(result[0].status, "no binding registry");
    assert!(result[0].module_path.is_none());
}

#[test]
fn build_binding_info_with_registry() {
    let entry = test_entry("test", vec!["f", "g"], 0, 0);
    let binding = crate::binding::parse_binding_str(
        r#"
version: "1.0.0"
target_crate: test
bindings:
  - contract: test.yaml
    equation: f
    module_path: "test::f"
    function: f
    status: implemented
"#,
    )
    .unwrap();
    let result = build_binding_info(&entry, Some(&binding));
    assert_eq!(result.len(), 2);
    let f_binding = result.iter().find(|b| b.equation == "f").unwrap();
    assert_eq!(f_binding.status, "implemented");
    assert!(f_binding.module_path.is_some());
    let g_binding = result.iter().find(|b| b.equation == "g").unwrap();
    assert_eq!(g_binding.status, "unbound");
    assert!(g_binding.module_path.is_none());
}

fn entry_at(path: &str) -> types::ContractEntry {
    let mut e = test_entry("diff-info", vec![], 0, 0);
    e.path = path.into();
    e
}

/// Hermetic fixture: a throwaway git repo with one committed file, so the
/// tests do not depend on the source tree having `.git` (the clean-room copy
/// is made with `tar --exclude=.git`, PMAT-6487).
fn committed_fixture() -> (tempfile::TempDir, String) {
    let dir = tempfile::tempdir().expect("tempdir");
    let git = |args: &[&str]| {
        let st = std::process::Command::new("git")
            .arg("-C")
            .arg(dir.path())
            .args(args)
            .env_remove("GIT_DIR")
            .env_remove("GIT_WORK_TREE")
            .env_remove("GIT_INDEX_FILE")
            .status()
            .expect("git is runnable");
        assert!(st.success(), "git {args:?} failed");
    };
    git(&["init", "-q"]);
    git(&["config", "user.name", "fixture"]);
    git(&["config", "user.email", "fixture@example.invalid"]);
    git(&["config", "commit.gpgsign", "false"]);
    // A user-global hooksPath must not fire inside the throwaway repo.
    git(&["config", "core.hooksPath", ".no-hooks"]);
    let file = dir.path().join("contract.yaml");
    std::fs::write(&file, "metadata: {}\n").expect("write fixture");
    git(&["add", "contract.yaml"]);
    git(&["commit", "-q", "-m", "fixture"]);
    let path = file.to_str().expect("utf8 path").to_string();
    (dir, path)
}

#[test]
fn build_diff_info_reports_the_last_commit_of_a_tracked_file() {
    let (_dir, path) = committed_fixture();
    let info = build_diff_info(&entry_at(&path)).expect("fixture file is tracked");
    assert_eq!(info.commit_hash.len(), 40, "full sha: {}", info.commit_hash);
    assert!(info.commit_hash.bytes().all(|b| b.is_ascii_hexdigit()));
    let parts: Vec<&str> = info.last_modified.split('-').collect();
    assert_eq!(parts.len(), 3, "date part is Y-M-D: {}", info.last_modified);
    assert_eq!(parts[0].len(), 4);
    assert_eq!(info.last_modified.len(), 10, "time part is stripped");
    assert!(info.days_ago < 36_500, "days_ago is relative to now");
}

#[test]
fn build_diff_info_days_ago_matches_parse_iso_days_ago() {
    let (_dir, path) = committed_fixture();
    let info = build_diff_info(&entry_at(&path)).expect("tracked");
    let now = std::time::SystemTime::now()
        .duration_since(std::time::UNIX_EPOCH)
        .unwrap()
        .as_secs();
    let expect = parse_iso_days_ago(&info.last_modified, now);
    assert!(
        info.days_ago.abs_diff(expect) <= 1,
        "{} vs {expect}",
        info.days_ago
    );
}

#[test]
fn build_diff_info_is_none_for_a_file_outside_any_repo() {
    let dir = tempfile::tempdir().expect("tempdir");
    let file = dir.path().join("loose.yaml");
    std::fs::write(&file, "x: 1\n").expect("write");
    let path = file.to_str().expect("utf8 path");
    assert!(build_diff_info(&entry_at(path)).is_none());
}

#[test]
fn build_diff_info_is_none_for_a_path_git_has_no_history_for() {
    let missing = concat!(env!("CARGO_MANIFEST_DIR"), "/no-such-file-5580.yaml");
    assert!(build_diff_info(&entry_at(missing)).is_none());
}