trident/src/verify/report/tests.rs

use super::*;
use crate::solve;
use crate::sym;

/// Helper: parse source, build constraint system, run verification.
fn verify_source(source: &str) -> (ConstraintSystem, VerificationReport) {
    let file = crate::parse_source(source, "test.tri").unwrap();
    let system = sym::analyze(&file);
    let report = solve::verify(&system);
    (system, report)
}

#[test]
fn test_json_basic_structure() {
    let (system, report) = verify_source("program test\nfn main() {\n    assert(true)\n}\n");
    let json = generate_json_report("test.tri", &system, &report);

    // Check basic JSON structure markers
    assert!(json.starts_with('{'));
    assert!(json.contains("\"version\": 1"));
    assert!(json.contains("\"file\": \"test.tri\""));
    assert!(json.contains("\"verdict\": \"safe\""));
    assert!(json.contains("\"summary\":"));
    assert!(json.contains("\"constraints\":"));
    assert!(json.contains("\"counterexamples\":"));
    assert!(json.contains("\"redundant_assertions\":"));
    assert!(json.contains("\"suggestions\":"));
}

#[test]
fn test_counterexample_serialization() {
    let (system, report) = verify_source(
        "program test\nfn main() {\n    let x: Field = pub_read()\n    assert_eq(x, 0)\n}\n",
    );
    let json = generate_json_report("test.tri", &system, &report);

    // This program asserts x == 0 which should fail for most random x
    assert!(json.contains("\"verdict\": \"unsafe\""));
    assert!(json.contains("\"counterexamples\": ["));
    // Should have at least one counterexample with assignments
    assert!(json.contains("\"assignments\":"));
}

#[test]
fn test_safe_program_no_suggestions() {
    let (system, report) = verify_source(
        "program test\nfn main() {\n    let x: Field = pub_read()\n    assert_eq(x + 0, x)\n}\n",
    );
    let suggestions = generate_suggestions(&system, &report);

    // No fix_violation suggestions for a safe program
    let violations: Vec<_> = suggestions
        .iter()
        .filter(|s| s.kind == "fix_violation")
        .collect();
    assert!(
        violations.is_empty(),
        "safe program should have no fix_violation suggestions"
    );
}

#[test]
fn test_unsafe_program_fix_violation() {
    let (system, report) = verify_source(
        "program test\nfn main() {\n    let x: Field = pub_read()\n    assert_eq(x, 42)\n}\n",
    );
    let suggestions = generate_suggestions(&system, &report);

    let violations: Vec<_> = suggestions
        .iter()
        .filter(|s| s.kind == "fix_violation")
        .collect();
    assert!(
        !violations.is_empty(),
        "unsafe program should have fix_violation suggestions"
    );
    // Each violation suggestion should reference a constraint index
    for v in &violations {
        assert!(v.constraint_index.is_some());
    }
}

#[test]
fn test_redundant_assertion_suggestion() {
    // assert(true) is trivially true, but the solver marks non-trivial
    // always-satisfied constraints as redundant. Use assert_eq(x+0, x)
    // which is non-trivial but always holds.
    let (system, report) = verify_source(
        "program test\nfn main() {\n    let x: Field = pub_read()\n    assert_eq(x + 0, x)\n}\n",
    );

    // Check the report for redundant assertions
    if !report.redundant_assertions.is_empty() {
        let suggestions = generate_suggestions(&system, &report);
        let redundant: Vec<_> = suggestions
            .iter()
            .filter(|s| s.kind == "remove_redundant")
            .collect();
        assert!(
            !redundant.is_empty(),
            "redundant assertions should produce remove_redundant suggestions"
        );
    }
    // If the solver does not flag it as redundant (implementation detail),
    // the test still passes -- we just verify the suggestion logic is wired.
}

#[test]
fn test_json_escape_special_chars() {
    let escaped = json_escape("hello \"world\"\nnewline\\backslash");
    assert_eq!(escaped, "hello \\\"world\\\"\\nnewline\\\\backslash");
}

#[test]
fn test_json_escape_control_chars() {
    let escaped = json_escape("tab\there");
    assert_eq!(escaped, "tab\\there");
}

#[test]
fn test_format_json_constraint_kinds() {
    let c1 = Constraint::Equal(SymValue::Const(1), SymValue::Const(1));
    let jc1 = format_json_constraint(&c1, 0);
    assert_eq!(jc1.kind, "equal");
    assert!(jc1.is_trivial);
    assert!(!jc1.is_violated);

    let c2 = Constraint::AssertTrue(SymValue::Const(0));
    let jc2 = format_json_constraint(&c2, 1);
    assert_eq!(jc2.kind, "assert_true");
    assert!(jc2.is_violated);

    let c3 = Constraint::RangeU32(SymValue::Const(42));
    let jc3 = format_json_constraint(&c3, 2);
    assert_eq!(jc3.kind, "range_u32");
    assert!(jc3.is_trivial);

    let c4 = Constraint::Conditional(
        SymValue::Const(1),
        Box::new(Constraint::AssertTrue(SymValue::Const(1))),
    );
    let jc4 = format_json_constraint(&c4, 3);
    assert_eq!(jc4.kind, "conditional");

    let c5 = Constraint::DigestEqual(vec![SymValue::Const(0)], vec![SymValue::Const(0)]);
    let jc5 = format_json_constraint(&c5, 4);
    assert_eq!(jc5.kind, "digest_equal");
}

#[test]
fn test_divine_unconstrained_suggestion() {
    let (system, report) = verify_source(
        "program test\nfn main() {\n    let x: Field = divine()\n    assert(true)\n}\n",
    );
    let suggestions = generate_suggestions(&system, &report);

    let add_assertions: Vec<_> = suggestions
        .iter()
        .filter(|s| s.kind == "add_assertion")
        .collect();
    assert!(
        !add_assertions.is_empty(),
        "unconstrained divine input should produce add_assertion suggestion"
    );
    assert!(add_assertions[0].message.contains("divine"));
}

#[test]
fn test_static_violation_in_json() {
    let (system, report) = verify_source("program test\nfn main() {\n    assert(false)\n}\n");
    let json = generate_json_report("test.tri", &system, &report);
    assert!(json.contains("\"verdict\": \"unsafe\""));
    assert!(json.contains("\"static_violations\": 1"));
}