aprender-contracts 0.70.1

use crate::obligation_matrix::{
    format_obligation_table, obligation_matrix, property_words_match, truncate, L2Status,
};
use crate::proof_status::*;
use crate::schema::{parse_contract_str, Contract};

use crate::proof_status::count_bindings;

/// Build a minimal contract with configurable obligation, test, and harness counts
fn minimal_contract(n_ob: usize, n_ft: usize, n_kani: usize) -> Contract {
    let mut yaml = String::from(
        r#"
metadata:
  version: "1.0.0"
  description: "Test"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
"#,
    );
    for i in 0..n_ob {
        yaml.push_str(&format!(
            "  - type: invariant\n    property: \"prop {i}\"\n"
        ));
    }
    yaml.push_str("falsification_tests:\n");
    for i in 0..n_ft {
        yaml.push_str(&format!(
            "  - id: FT-{i:03}\n    rule: \"r\"\n    prediction: \"p\"\n    if_fails: \"f\"\n"
        ));
    }
    yaml.push_str("kani_harnesses:\n");
    for i in 0..n_kani {
        yaml.push_str(&format!(
            "  - id: KH-{i:03}\n    obligation: OBL-{i:03}\n    bound: 16\n"
        ));
    }
    parse_contract_str(&yaml).unwrap()
}

/// Build a contract with Lean verification summary for L4/L5 level testing
fn contract_with_lean(total: u32, lean_proved: u32) -> Contract {
    let mut c = minimal_contract(total as usize, total as usize, total as usize);
    c.verification_summary = Some(crate::schema::VerificationSummary {
        total_obligations: total,
        l2_property_tested: total,
        l3_kani_proved: total,
        l4_lean_proved: lean_proved,
        l4_sorry_count: total - lean_proved,
        l4_not_applicable: 0,
    });
    c
}

#[test]
fn proof_level_display() {
    assert_eq!(ProofLevel::L1.to_string(), "L1");
    assert_eq!(ProofLevel::L2.to_string(), "L2");
    assert_eq!(ProofLevel::L3.to_string(), "L3");
    assert_eq!(ProofLevel::L4.to_string(), "L4");
    assert_eq!(ProofLevel::L5.to_string(), "L5");
}

#[test]
fn proof_level_ordering() {
    assert!(ProofLevel::L1 < ProofLevel::L2);
    assert!(ProofLevel::L2 < ProofLevel::L3);
    assert!(ProofLevel::L3 < ProofLevel::L4);
    assert!(ProofLevel::L4 < ProofLevel::L5);
}

#[test]
fn level_l1_for_equations_only() {
    let c = minimal_contract(0, 0, 0);
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L1);
}

#[test]
fn level_l2_for_falsification_covered() {
    let c = minimal_contract(3, 3, 0);
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L2);
}

#[test]
fn level_l2_not_enough_tests() {
    let c = minimal_contract(3, 2, 0);
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L1);
}

#[test]
fn level_l3_kani_plus_falsification() {
    let c = minimal_contract(3, 3, 2);
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L3);
}

#[test]
fn level_l3_kani_without_enough_tests() {
    // Has kani but not enough falsification tests
    let c = minimal_contract(3, 2, 2);
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L1);
}

#[test]
fn level_l4_all_lean_proved() {
    let c = contract_with_lean(3, 3);
    // ONT-2a: grounded — the tree has the theorems the equations name.
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 3),
        ProofLevel::L4
    );
    // …and the same contract with nothing grounding it is the andon's case.
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 0),
        ProofLevel::L3
    );
}

#[test]
fn level_l4_partial_lean_stays_l3() {
    let c = contract_with_lean(3, 2);
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 2),
        ProofLevel::L3
    );
}

#[test]
fn level_l5_lean_plus_all_bound() {
    let c = contract_with_lean(3, 3);
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((1, 1)), 3),
        ProofLevel::L5
    );
}

#[test]
fn level_l4_when_bindings_incomplete() {
    let c = contract_with_lean(3, 3);
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((0, 1)), 3),
        ProofLevel::L4
    );
}

/// Build a contract with an explicit not-applicable count in its summary.
fn contract_with_lean_na(total: u32, lean_proved: u32, not_applicable: u32) -> Contract {
    let mut c = minimal_contract(total as usize, total as usize, total as usize);
    c.verification_summary = Some(crate::schema::VerificationSummary {
        total_obligations: total,
        l2_property_tested: total,
        l3_kani_proved: total,
        l4_lean_proved: lean_proved,
        l4_sorry_count: total - lean_proved - not_applicable,
        l4_not_applicable: not_applicable,
    });
    c
}

/// STRICT: proved + N/A must cover EVERY obligation. Partial Lean coverage
/// (the old "≥1 resolving ref → L4" over-promotion) now reports L3, even when
/// fully bound (which would previously have inflated it to L5). This is the
/// `lora-algebra`/`attention-kernel` case (4-of-6, 0-of-5, …).
#[test]
fn level_strict_partial_coverage_stays_l3_even_when_bound() {
    let c = contract_with_lean_na(6, 4, 1); // 4 grounded + 1 N/A = 5 < 6
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 4),
        ProofLevel::L3
    );
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((3, 3)), 4),
        ProofLevel::L3
    );
}

/// STRICT: a contract whose provable obligations are ALL discharged — some
/// proved, the rest explicitly N/A — is a legitimate L4/L5 (the `softmax-kernel`
/// case: 5 proved + 4 N/A of 9).
#[test]
fn level_strict_full_coverage_with_na_is_l4() {
    let c = contract_with_lean_na(9, 5, 4); // 5 grounded + 4 N/A == 9
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 5),
        ProofLevel::L4
    );
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((1, 1)), 5),
        ProofLevel::L5
    );
    // ONT-2a: the SAME coverage, claimed and not grounded, is not L4.
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((1, 1)), 0),
        ProofLevel::L3
    );
}

/// STRICT: `total` is `proof_obligations.len()`, NOT `verification_summary.
/// total_obligations`, so a summary cannot manufacture L4 by understating the
/// obligation count. Here the contract has 6 real obligations but the summary
/// claims a total of 3 (all "proved") — strict measures 3 proved against 6 real
/// obligations and correctly withholds L4.
#[test]
fn level_strict_summary_cannot_understate_total() {
    let mut c = minimal_contract(6, 6, 6); // 6 real proof_obligations
    c.verification_summary = Some(crate::schema::VerificationSummary {
        total_obligations: 3, // understated
        l2_property_tested: 3,
        l3_kani_proved: 3,
        l4_lean_proved: 3,
        l4_sorry_count: 0,
        l4_not_applicable: 0,
    });
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 3),
        ProofLevel::L3
    );
}

#[test]
fn report_empty_contracts() {
    let report = proof_status_report(&[], None, false);
    assert_eq!(report.totals.contracts, 0);
    assert_eq!(report.totals.obligations, 0);
    assert!(report.contracts.is_empty());
}

#[test]
fn report_single_contract() {
    let c = minimal_contract(3, 3, 2);
    let report = proof_status_report(&[("test-v1".to_string(), &c)], None, false);
    assert_eq!(report.contracts.len(), 1);
    assert_eq!(report.contracts[0].stem, "test-v1");
    assert_eq!(report.contracts[0].proof_level, ProofLevel::L3);
    assert_eq!(report.totals.obligations, 3);
    assert_eq!(report.totals.falsification_tests, 3);
    assert_eq!(report.totals.kani_harnesses, 2);
}

#[test]
fn report_with_binding() {
    let c = minimal_contract(3, 3, 2);
    let binding = crate::binding::parse_binding_str(
        r#"
version: "1.0.0"
target_crate: test
bindings:
  - contract: test-v1.yaml
    equation: f
    module_path: "test::f"
    function: f
    status: implemented
"#,
    )
    .unwrap();
    let report = proof_status_report(&[("test-v1".to_string(), &c)], Some(&binding), false);
    assert_eq!(report.contracts[0].bindings_implemented, 1);
    assert_eq!(report.contracts[0].bindings_total, 1);
}

#[test]
fn report_with_kernel_classes() {
    let c = minimal_contract(3, 3, 2);
    let report = proof_status_report(&[("softmax-kernel-v1".to_string(), &c)], None, true);
    assert!(!report.kernel_classes.is_empty());
    // Softmax is in classes A, B, C, D, E
    let class_a = report
        .kernel_classes
        .iter()
        .find(|kc| kc.label == "A")
        .unwrap();
    assert!(class_a
        .contract_stems
        .contains(&"softmax-kernel-v1".to_string()));
}

#[test]
fn format_text_produces_output() {
    let c = minimal_contract(3, 3, 2);
    let report = proof_status_report(&[("softmax-kernel-v1".to_string(), &c)], None, true);
    let text = format_text(&report);
    assert!(text.contains("Proof Status"));
    assert!(text.contains("softmax-kernel-v1"));
    assert!(text.contains("Kernel Classes:"));
    assert!(text.contains("Totals:"));
}

#[test]
fn format_text_without_classes() {
    let c = minimal_contract(2, 2, 0);
    let report = proof_status_report(&[("test-v1".to_string(), &c)], None, false);
    let text = format_text(&report);
    assert!(text.contains("test-v1"));
    assert!(!text.contains("Kernel Classes:"));
}

#[test]
fn json_roundtrip() {
    let c = minimal_contract(3, 3, 2);
    let report = proof_status_report(&[("test-v1".to_string(), &c)], None, true);
    let json = serde_json::to_string(&report).unwrap();
    let parsed: ProofStatusReport = serde_json::from_str(&json).unwrap();
    assert_eq!(parsed.contracts.len(), 1);
    assert_eq!(parsed.contracts[0].proof_level, ProofLevel::L3);
    assert_eq!(parsed.totals.obligations, 3);
}

#[test]
fn kernel_class_min_level() {
    let c1 = minimal_contract(3, 3, 2); // L3
    let c2 = minimal_contract(3, 3, 0); // L2
    let report = proof_status_report(
        &[
            ("softmax-kernel-v1".to_string(), &c1),
            ("matmul-kernel-v1".to_string(), &c2),
        ],
        None,
        true,
    );
    let class_a = report
        .kernel_classes
        .iter()
        .find(|kc| kc.label == "A")
        .unwrap();
    // min of L3 and L2 is L2
    assert_eq!(class_a.min_proof_level, ProofLevel::L2);
}

#[test]
fn count_bindings_helper() {
    let c = minimal_contract(1, 1, 1);
    let binding = crate::binding::parse_binding_str(
        r#"
version: "1.0.0"
target_crate: test
bindings:
  - contract: test.yaml
    equation: f
    status: implemented
  - contract: other.yaml
    equation: g
    status: implemented
"#,
    )
    .unwrap();
    let (implemented, total) = count_bindings("test.yaml", &c, &binding);
    assert_eq!(implemented, 1);
    assert_eq!(total, 1);
}

#[test]
fn truncate_helper() {
    assert_eq!(truncate("hello", 10), "hello");
    assert_eq!(truncate("hello world", 5), "hello");
}

/// #3338: `pv proof-status contracts/ --table` PANICKED on the real corpus.
///
/// `truncate` sliced by BYTE index, and the width is `min(max byte len, 40)`.
/// Eight contracts hold an obligation property whose byte 40 lands inside a
/// multi-byte char; the first one walked is
/// `contracts/apr-inspect-quantization-v1.yaml`:
///
/// ```text
/// byte index 40 is not a char boundary; it is inside '∈' (bytes 39..42)
/// of `for Q4_K_M Qwen2.5-Coder, quantization ∈ {Q4_K, Q6_K}`
/// ```
///
/// The fixture IS that property, so the cut is inside the same char.
#[test]
fn truncate_cuts_on_a_char_boundary_not_a_byte() {
    let s = "for Q4_K_M Qwen2.5-Coder, quantization ∈ {Q4_K, Q6_K}";
    assert!(
        !s.is_char_boundary(40),
        "fixture must cut INSIDE a multi-byte char, else it proves nothing"
    );
    let t = truncate(s, 40);
    assert!(s.starts_with(t), "truncation must be a prefix");
    assert!(t.len() <= 40, "truncation must not exceed the budget");
    assert_eq!(t, "for Q4_K_M Qwen2.5-Coder, quantization ");
}

/// The panic reached the operator through `format_obligation_table`, so the
/// table path gets its own row rather than only the helper.
#[test]
fn format_obligation_table_survives_a_multibyte_property() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "Multi-byte property at the cut"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "for Q4_K_M Qwen2.5-Coder, quantization ∈ {Q4_K, Q6_K}"
falsification_tests: []
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let matrices = obligation_matrix(&[("multibyte-v1".to_string(), &c)]);
    let text = format_obligation_table(&matrices);
    assert!(text.contains("Contract: multibyte-v1"));
}

#[test]
fn schema_version_present() {
    let report = proof_status_report(&[], None, false);
    assert_eq!(report.schema_version, "1.0.0");
}

#[test]
fn timestamp_is_populated() {
    let report = proof_status_report(&[], None, false);
    assert!(!report.timestamp.is_empty());
    assert!(report.timestamp.ends_with('Z'));
}

// ── Obligation matrix tests ─────────────────────────────────────

#[test]
fn obligation_matrix_empty() {
    let matrices = obligation_matrix(&[]);
    assert!(matrices.is_empty());
}

/// #3347: this test used to be named `obligation_matrix_index_based_l2` and
/// asserted the defect -- 3 obligations and 3 tests, none of them linked to
/// anything, scored L2 across the board because `idx < 3`.
///
/// The contract says nothing about which test covers which obligation, so the
/// honest verdict is Unknown and the level stays L1.
#[test]
fn obligation_matrix_unlinked_tests_are_unknown_not_l2() {
    let c = minimal_contract(3, 3, 0);
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    assert_eq!(matrices.len(), 1);
    assert_eq!(matrices[0].obligations.len(), 3);
    for ob in &matrices[0].obligations {
        assert_eq!(ob.l2, L2Status::Unknown);
        assert!(!ob.l2.is_tested());
        assert!(!ob.l3_kani);
        assert!(!ob.l4_lean);
        assert_eq!(ob.max_level, ProofLevel::L1);
    }
}

/// Zero falsification tests is a READING, not an unread window: no test
/// exists, so no test covers this obligation. Untested, not Unknown.
#[test]
fn obligation_matrix_no_tests_is_untested_and_l1() {
    let c = minimal_contract(2, 0, 0);
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    assert_eq!(matrices[0].obligations.len(), 2);
    for ob in &matrices[0].obligations {
        assert_eq!(ob.l2, L2Status::Untested);
        assert_eq!(ob.max_level, ProofLevel::L1);
    }
}

/// `proof_obligations[].discharged_by` -- the link written from the
/// obligation's side, and the most-used spelling in `contracts/` (89).
#[test]
fn discharged_by_links_an_obligation_to_its_test() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "discharged_by, both resolvable shapes"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "By index"
    discharged_by: falsification_tests[0]
  - type: invariant
    property: "By test id"
    discharged_by: FT-002
  - type: invariant
    property: "Out of range"
    discharged_by: falsification_tests[9]
  - type: invariant
    property: "Names a kani harness, not a test"
    discharged_by: KANI-X-001
falsification_tests:
  - id: FT-001
    rule: "r"
    prediction: "p"
    if_fails: "f"
  - id: FT-002
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let obs = &obligation_matrix(&[("db-v1".to_string(), &c)])[0].obligations;
    assert_eq!(obs[0].l2, L2Status::Tested, "falsification_tests[0] exists");
    assert_eq!(obs[1].l2, L2Status::Tested, "FT-002 exists");
    assert_eq!(
        obs[2].l2,
        L2Status::Untested,
        "falsification_tests[9] is out of range over 2 tests -- a dangling \
         citation is not a proof"
    );
    assert_eq!(
        obs[3].l2,
        L2Status::Untested,
        "a kani harness id is the L3 column, never an L2 link"
    );
}

/// `binds_to:` is the second spelling of `falsification_tests[].obligation`
/// (38 entries vs 26). It is a serde alias, which is safe ONLY because no
/// entry in `contracts/` carries both keys -- serde would make that a
/// `duplicate field` parse error rather than a silent pick.
#[test]
fn binds_to_is_the_same_link_as_obligation() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "binds_to alias"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - id: OB-1
    type: invariant
    property: "Bound by alias"
  - id: OB-2
    type: invariant
    property: "Bound by nothing"
falsification_tests:
  - id: FT-001
    binds_to: OB-1
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let cited: Vec<&str> = c.falsification_tests[0]
        .obligation
        .as_ref()
        .expect("binds_to must land on the obligation field, not be dropped")
        .targets()
        .collect();
    assert_eq!(cited, vec!["OB-1"]);
    let obs = &obligation_matrix(&[("alias-v1".to_string(), &c)])[0].obligations;
    assert_eq!(obs[0].l2, L2Status::Tested);
    assert_eq!(obs[1].l2, L2Status::Untested);
}

/// A contract whose every link DANGLES was not read -- reporting its
/// obligations as Untested would be inventing a finding out of a parse
/// failure. `apr-code-harness-ir-v1` is the real instance: 8 tests cite
/// `OBLIG-IR-N` and that contract's obligations carry no `id` at all.
#[test]
fn links_that_all_dangle_are_unknown_not_untested() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "every citation dangles"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "Alpha"
  - type: invariant
    property: "Beta"
falsification_tests:
  - id: FT-001
    obligation: OBLIG-NOBODY-1
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let obs = &obligation_matrix(&[("dangle-v1".to_string(), &c)])[0].obligations;
    for ob in obs {
        assert_eq!(ob.l2, L2Status::Unknown);
    }
}

/// One test may discharge several obligations in one comma-separated field.
#[test]
fn a_comma_separated_citation_names_several_obligations() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "comma list"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - id: OB-1
    type: invariant
    property: "One"
  - id: OB-2
    type: invariant
    property: "Two"
  - id: OB-3
    type: invariant
    property: "Three"
falsification_tests:
  - id: FT-001
    obligation: "OB-1, OB-3"
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let obs = &obligation_matrix(&[("comma-v1".to_string(), &c)])[0].obligations;
    assert_eq!(obs[0].l2, L2Status::Tested);
    assert_eq!(obs[1].l2, L2Status::Untested);
    assert_eq!(obs[2].l2, L2Status::Tested);
}

/// A citation may also name the obligation by its exact `property` text --
/// `apr-mcp-stdio-drain-v1` binds all six of its tests that way.
#[test]
fn a_citation_may_name_the_property_text() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "property-text citation"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "drain-on-every-exit"
  - type: invariant
    property: "no-false-error"
falsification_tests:
  - id: FT-001
    obligation: drain-on-every-exit
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let obs = &obligation_matrix(&[("prop-v1".to_string(), &c)])[0].obligations;
    assert_eq!(obs[0].l2, L2Status::Tested);
    assert_eq!(obs[1].l2, L2Status::Untested);
}

#[test]
fn obligation_matrix_lean_proved() {
    // Build a contract with a Lean-proved obligation
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "Test lean"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "Output sums to 1"
    lean:
      theorem: Softmax.partition_of_unity
      module: ProvableContracts.Softmax
      status: proved
  - type: bound
    property: "Range is strictly positive"
falsification_tests:
  - id: FT-001
    rule: "normalization"
    prediction: "sums to 1"
    if_fails: "bug"
  - id: FT-002
    rule: "bounded"
    prediction: "in range"
    if_fails: "bug"
kani_harnesses:
  - id: KH-001
    obligation: OB-001
    property: "Output sums to 1"
    bound: 8
"#;
    let c = parse_contract_str(yaml).unwrap();
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    assert_eq!(matrices[0].obligations.len(), 2);

    // First obligation: L3 (kani property match "sums"), L4 (lean proved). Its
    // L2 is Unknown -- the two tests name no obligation (#3347) -- which does
    // not disturb a level earned higher up the ladder.
    let ob0 = &matrices[0].obligations[0];
    assert_eq!(ob0.l2, L2Status::Unknown);
    assert!(ob0.l3_kani);
    assert!(ob0.l4_lean);
    assert_eq!(ob0.max_level, ProofLevel::L4);

    // Second obligation "Range is strictly positive": nothing at all.
    let ob1 = &matrices[0].obligations[1];
    assert_eq!(ob1.l2, L2Status::Unknown);
    assert!(!ob1.l3_kani);
    assert!(!ob1.l4_lean);
    assert_eq!(ob1.max_level, ProofLevel::L1);
}

#[test]
fn obligation_matrix_sorry_is_not_l4() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "Test sorry"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - type: invariant
    property: "Prop with sorry"
    lean:
      theorem: Foo.bar
      status: sorry
falsification_tests:
  - id: FT-001
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    let ob = &matrices[0].obligations[0];
    assert!(!ob.l4_lean);
    // The lone test names no obligation, so L2 is Unknown and the level is L1.
    assert_eq!(ob.l2, L2Status::Unknown);
    assert_eq!(ob.max_level, ProofLevel::L1);
}

/// RED FIRST (#3347). The L2 column ticked on `idx < falsification_tests.len()`
/// — a COUNT, not a link — so every obligation of a contract with enough tests
/// showed ✓ whoever those tests were about.
///
/// This fixture makes the two disagree: TWO obligations, TWO tests, and BOTH
/// tests cite `OB-A`. Nothing anywhere claims `OB-B` is tested. Under the index
/// rule `OB-B` is index 1 < 2 tests, so it ticked.
///
/// The assertion goes through `format_obligation_table` deliberately: the
/// rendered L2 cell is the surface the operator reads, and it is the surface
/// that was lying. It is also API-stable, so this row is the SAME test before
/// and after the fix — it fails on the old code and passes on the new.
#[test]
fn l2_does_not_tick_for_an_obligation_no_test_cites() {
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "Two obligations, two tests, both tests cite OB-A"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - id: OB-A
    type: invariant
    property: "Alpha holds"
  - id: OB-B
    type: invariant
    property: "Beta holds"
falsification_tests:
  - id: FT-001
    obligation: OB-A
    rule: "alpha one"
    prediction: "p"
    if_fails: "f"
  - id: FT-002
    obligation: OB-A
    rule: "alpha two"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let c = parse_contract_str(yaml).unwrap();
    let matrices = obligation_matrix(&[("cross-cited-v1".to_string(), &c)]);
    let text = format_obligation_table(&matrices);

    let row_a = table_row(&text, "Alpha holds");
    let row_b = table_row(&text, "Beta holds");

    // Discrimination: the contract DOES bind OB-A, so a fix that simply stopped
    // ticking everything would fail here.
    assert!(
        row_a.contains('\u{2713}'),
        "OB-A is cited by two tests and must stay ticked\nrow: {row_a}"
    );
    assert!(
        !row_b.contains('\u{2713}'),
        "OB-B is cited by NO test — the L2 column ticked it from a count, not a link\nrow: {row_b}"
    );
}

/// Pull one obligation's rendered row out of the table by its property text.
fn table_row<'a>(table: &'a str, property: &str) -> &'a str {
    table
        .lines()
        .find(|l| l.contains(property))
        .unwrap_or_else(|| panic!("no table row for property `{property}`:\n{table}"))
}

#[test]
fn property_words_match_basic() {
    assert!(property_words_match(
        "output sums to one",
        "sums to one check"
    ));
    assert!(property_words_match(
        "softmax normalization",
        "verify normalization"
    ));
    assert!(!property_words_match("positivity check", "bounded range"));
}

#[test]
fn property_words_match_ignores_stop_words() {
    // "the" and "for" are stop words, should not cause a match
    assert!(!property_words_match("the output", "the input"));
    // But "output" is not a stop word
    assert!(property_words_match("output range", "output check"));
}

#[test]
fn format_obligation_table_header() {
    let c = minimal_contract(1, 1, 0);
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    let text = format_obligation_table(&matrices);
    assert!(text.contains("Obligation Status Matrix"));
    assert!(text.contains("Contract: test-v1"));
    assert!(text.contains("L2 Test"));
    assert!(text.contains("L3 Kani"));
    assert!(text.contains("L4 Lean"));
    assert!(text.contains("Status"));
}

/// All three L2 cells are reachable from the renderer, and they are distinct
/// glyphs. A fix that collapsed Unknown onto either tick or cross would fail
/// here rather than pass quietly.
#[test]
fn format_obligation_table_renders_all_three_l2_cells() {
    // 1 obligation, 1 test, no link => `?`; L3/L4 crossed.
    let unknown = minimal_contract(1, 1, 0);
    let text = format_obligation_table(&obligation_matrix(&[("u-v1".to_string(), &unknown)]));
    assert!(text.contains('?'), "unlinked L2 renders as `?`:\n{text}");
    assert!(
        text.contains('\u{2717}'),
        "L3/L4 render as crosses:\n{text}"
    );

    // 0 tests => a cross in the L2 column, not a `?`.
    let untested = minimal_contract(1, 0, 0);
    let text = format_obligation_table(&obligation_matrix(&[("x-v1".to_string(), &untested)]));
    assert!(
        !text.contains('?'),
        "0 tests is a reading, not Unknown:\n{text}"
    );

    // A linked obligation still ticks.
    let yaml = r#"
metadata:
  version: "1.0.0"
  description: "linked"
  references: ["Paper"]
equations:
  f:
    formula: "f(x) = x"
proof_obligations:
  - id: OB-1
    type: invariant
    property: "Linked prop"
falsification_tests:
  - id: FT-001
    obligation: OB-1
    rule: "r"
    prediction: "p"
    if_fails: "f"
kani_harnesses: []
"#;
    let linked = parse_contract_str(yaml).unwrap();
    let text = format_obligation_table(&obligation_matrix(&[("l-v1".to_string(), &linked)]));
    assert!(
        text.contains('\u{2713}'),
        "a linked obligation ticks:\n{text}"
    );
}

#[test]
fn format_obligation_table_empty_obligations() {
    let c = minimal_contract(0, 0, 0);
    let matrices = obligation_matrix(&[("test-v1".to_string(), &c)]);
    let text = format_obligation_table(&matrices);
    // Should not have "Contract: test-v1" since obligations are empty
    assert!(!text.contains("Contract: test-v1"));
}

#[test]
fn obligation_matrix_multiple_contracts() {
    let c1 = minimal_contract(2, 2, 0);
    let c2 = minimal_contract(1, 0, 0);
    let matrices =
        obligation_matrix(&[("alpha-v1".to_string(), &c1), ("beta-v1".to_string(), &c2)]);
    assert_eq!(matrices.len(), 2);
    assert_eq!(matrices[0].stem, "alpha-v1");
    assert_eq!(matrices[0].obligations.len(), 2);
    assert_eq!(matrices[1].stem, "beta-v1");
    assert_eq!(matrices[1].obligations.len(), 1);
}

#[test]
fn is_fully_bound_edge_cases() {
    let c1 = minimal_contract(1, 1, 1);
    assert_eq!(compute_proof_level(&c1, None), ProofLevel::L3);
    let c2 = contract_with_lean(1, 1);
    assert_eq!(
        compute_proof_level_with_grounding(&c2, Some((0, 0)), 1),
        ProofLevel::L4
    );
    assert_eq!(
        compute_proof_level_with_grounding(&c2, Some((1, 2)), 1),
        ProofLevel::L4
    );
}

#[test]
fn report_multiple_contracts_totals() {
    let c1 = minimal_contract(3, 3, 2);
    let c2 = minimal_contract(5, 5, 1);
    let report = proof_status_report(&[("a-v1".into(), &c1), ("b-v1".into(), &c2)], None, false);
    assert_eq!(report.totals.contracts, 2);
    assert_eq!(report.totals.obligations, 8);
    assert_eq!(report.totals.falsification_tests, 8);
    assert_eq!(report.totals.kani_harnesses, 3);
}

#[test]
fn kernel_class_all_bound_false_when_partial() {
    let c = minimal_contract(3, 3, 2);
    let report = proof_status_report(&[("softmax-kernel-v1".into(), &c)], None, true);
    let class_a = report
        .kernel_classes
        .iter()
        .find(|kc| kc.label == "A")
        .unwrap();
    assert!(!class_a.all_bound);
}

/// CI GUARD (Rank #1): the Lean scan must be self-sufficient from the in-tree
/// staging tree, NOT dependent on a co-located `../provable-contracts` sibling.
///
/// Before the scan-path fix, `proof_status.rs` scanned only
/// `["lean", "../provable-contracts/lean"]`; `./lean` does not exist, so on a
/// fresh clone / CI (no sibling checkout) every Lean-backed contract silently
/// collapsed — the 25 L4 dropped to L3 and both L5 to L3. This test fails if the
/// in-tree tree is removed/emptied or demoted from primary, which is exactly the
/// condition that would make L4/L5 non-reproducible.
#[test]
fn lean_scan_in_tree_is_primary_and_self_sufficient() {
    // (1) The in-tree staging tree must be the FIRST scan base.
    assert_eq!(
        LEAN_THEOREM_BASES[0], "crates/aprender-contracts-staging/lean",
        "the in-tree staging Lean tree must be the primary scan base so proof \
         levels are reproducible without the external ../provable-contracts sibling"
    );

    // (2) That tree must exist and carry a healthy set of sorry-free theorems.
    let theorems = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
        .join("../../crates/aprender-contracts-staging/lean/ProvableContracts/Theorems");
    assert!(
        theorems.is_dir(),
        "in-tree Lean theorems dir missing: {}",
        theorems.display()
    );

    let mut sorry_free = 0usize;
    let mut stack = vec![theorems.clone()];
    while let Some(dir) = stack.pop() {
        let Ok(entries) = std::fs::read_dir(&dir) else {
            continue;
        };
        for entry in entries.flatten() {
            let path = entry.path();
            if path.is_dir() {
                stack.push(path);
            } else if path.extension().is_some_and(|e| e == "lean") {
                if let Ok(content) = std::fs::read_to_string(&path) {
                    if !guarded(move || lean_has_sorry(&content)) {
                        sorry_free += 1;
                    }
                }
            }
        }
    }
    assert!(
        sorry_free >= 40,
        "expected the in-tree Lean tree to carry the corpus of sorry-free \
         theorems (>=40), found {sorry_free} — L4/L5 levels would not be \
         reproducible on CI"
    );
}

// ── ONT-2a (ONT-001 R-4, andon): a claim is not a proof ───────────

/// A summary that claims Lean proof, with no in-tree theorem to ground it, is SELF-DECLARED. It does not
/// reach L4, and bindings cannot promote it to L5 either: `is_lean_proved` now reads the tree, not the
/// contract's opinion of itself.
#[test]
fn ont2a_a_claim_with_nothing_under_it_is_not_l4() {
    let c = contract_with_lean(3, 3); // the summary says 3 of 3 proved; no .lean theorem resolves
    assert!(
        is_l4_self_declared(&c),
        "the claim covers every obligation and nothing in the tree grounds it"
    );
    assert_eq!(compute_proof_level(&c, None), ProofLevel::L3);
    assert_eq!(
        compute_proof_level(&c, Some((1, 1))),
        ProofLevel::L3,
        "bindings must not promote an ungrounded claim to L5"
    );
}

/// The report performs the withdrawal in the open: the contract is flagged, its grounded count is zero,
/// and the report says the L4 total excludes such contracts.
#[test]
fn ont2a_the_report_flags_the_claim_and_says_the_total_excludes_it() {
    let c = contract_with_lean(2, 2);
    let report = proof_status_report(&[("claims-l4".to_string(), &c)], None, false);
    assert!(report.l4_self_declared_excluded);
    assert_eq!(report.totals.l4_self_declared, 1);
    assert_eq!(report.totals.lean_grounded, 0);
    assert!(report.contracts[0].l4_self_declared);
    assert_ne!(report.contracts[0].proof_level, ProofLevel::L4);
}

/// Both words are printed. A withdrawal nobody can see on the line is the silence this row exists to end.
#[test]
fn ont2a_the_text_output_prints_self_declared_and_grounded() {
    let c = contract_with_lean(2, 2);
    let report = proof_status_report(&[("claims-l4".to_string(), &c)], None, false);
    let text = format_text(&report);
    assert!(
        text.contains("self-declared"),
        "the line must say it:\n{text}"
    );
    assert!(
        text.contains("grounded"),
        "and the other column must be named:\n{text}"
    );
}

/// The flag marks an unbacked CLAIM, not the mere absence of a proof: a contract that claims nothing is
/// not self-declared, it is just not L4.
#[test]
fn ont2a_a_contract_that_claims_nothing_is_not_flagged() {
    let c = minimal_contract(2, 2, 2);
    assert!(!is_l4_self_declared(&c));
    let report = proof_status_report(&[("quiet".to_string(), &c)], None, false);
    assert_eq!(report.totals.l4_self_declared, 0);
    assert!(report.l4_self_declared_excluded);
}

// ── PMAT-3091: N/A obligations are counted apart and never raise a level ────

/// `n_ob` ordinary obligations plus `n_na` declared `applies_to: not_applicable`.
fn contract_with_na_obligations(n_ob: usize, n_na: usize, n_ft: usize, n_kani: usize) -> Contract {
    let mut c = minimal_contract(n_ob, n_ft, n_kani);
    for i in 0..n_na {
        let ob: crate::schema::ProofObligation = serde_yaml::from_str(&format!(
            "property: \"na {i}\"\napplies_to: not_applicable\nna_reason: r\nna_owner: o\n"
        ))
        .expect("N/A obligation fixture must parse");
        c.proof_obligations.push(ob);
    }
    c
}

#[test]
fn na_obligations_are_counted_separately_as_k_na() {
    let c = contract_with_na_obligations(3, 2, 5, 0);
    let report = proof_status_report(&[("na-v1".to_string(), &c)], None, false);
    assert_eq!(report.contracts[0].obligations, 5);
    assert_eq!(report.contracts[0].not_applicable, 2);
    assert_eq!(report.totals.not_applicable, 2);
    let text = format_text(&report);
    assert!(text.contains("2 N/A"), "{text}");
}

#[test]
fn na_count_is_zero_without_declarations() {
    let c = minimal_contract(3, 3, 0);
    let report = proof_status_report(&[("plain-v1".to_string(), &c)], None, false);
    assert_eq!(report.contracts[0].not_applicable, 0);
    assert_eq!(report.totals.not_applicable, 0);
}

/// 3 tests cover the 3 ordinary obligations; the 4th is N/A. Were N/A dropped
/// from the denominator, 3 >= 3 would promote the contract to L2 on the
/// strength of a declaration. It stays where an undeclared 4th would leave it.
#[test]
fn na_obligation_does_not_raise_the_level() {
    let with_na = contract_with_na_obligations(3, 1, 3, 0);
    let undeclared = minimal_contract(4, 3, 0);
    assert_eq!(compute_proof_level(&with_na, None), ProofLevel::L1);
    assert_eq!(
        compute_proof_level(&with_na, None),
        compute_proof_level(&undeclared, None)
    );
    let kani = contract_with_na_obligations(3, 1, 3, 3);
    assert_eq!(compute_proof_level(&kani, None), ProofLevel::L1);
}

/// An all-N/A contract has nothing proved, so no L4 credit from the grounding
/// path: the schema N/A is not `verification_summary.l4_not_applicable`.
#[test]
fn na_obligations_grant_no_lean_credit() {
    let c = contract_with_na_obligations(0, 3, 3, 3);
    assert!(!is_lean_proved_with_grounding(&c, 0));
    let one = contract_with_na_obligations(1, 3, 4, 4);
    assert!(!is_lean_proved_with_grounding(&one, 1));
}

/// PVL-001 EV-3 (quorum round 4, measured): "every obligation is proved or not
/// applicable" must not be satisfied VACUOUSLY. All obligations not applicable and none
/// grounded is not L4 (ONT-2a: `grounded > 0`); with Kani and full falsification
/// coverage it is L3. ProofLevel::L4's method says "with at least one proved".
#[test]
fn level_all_not_applicable_is_not_l4() {
    let c = contract_with_lean_na(5, 0, 5);
    assert_eq!(
        compute_proof_level_with_grounding(&c, None, 0),
        ProofLevel::L3
    );
}

/// PVL-001 EV-3 (quorum round 4, measured): L5 needs at least one binding. A fully
/// grounded contract with ZERO bindings is L4, not L5 (`is_fully_bound` requires a
/// non-zero total). ProofLevel::L5's method says "at least one binding".
#[test]
fn level_l5_needs_at_least_one_binding() {
    let c = contract_with_lean(3, 3);
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((0, 0)), 3),
        ProofLevel::L4
    );
    assert_eq!(
        compute_proof_level_with_grounding(&c, Some((1, 1)), 3),
        ProofLevel::L5
    );
}

// ── EV-8b (#4082): L4 credit from the discharge summary, not the YAML ──

fn discharged_of(theorems: &[&str]) -> crate::discharge::summary::Discharged {
    crate::discharge::summary::Discharged {
        theorems: theorems.iter().map(|t| (*t).to_string()).collect(),
        withheld: None,
        ..Default::default()
    }
}

fn contract_naming_theorems(total: u32) -> Contract {
    let mut c = contract_with_lean(total, total);
    for (i, eq) in c.equations.values_mut().enumerate() {
        eq.lean_theorem = Some(format!("Gelu.t{i}"));
    }
    c
}

#[test]
fn ev8b_a_yaml_claim_the_summary_does_not_list_is_not_l4() {
    let c = contract_naming_theorems(1);
    let none = count_discharged_for_contract(&c, &discharged_of(&[]));
    assert_eq!(none, 0);
    assert!(!is_lean_proved_with_grounding(&c, none));
    assert!(is_l4_self_declared_with_grounding(&c, none));
}

#[test]
fn ev8b_a_summary_listing_every_named_theorem_grounds_l4() {
    let c = contract_naming_theorems(1);
    let names: Vec<String> = (0..c.equations.len())
        .map(|i| format!("ProvableContracts.Gelu.t{i}"))
        .collect();
    let refs: Vec<&str> = names.iter().map(String::as_str).collect();
    let n = count_discharged_for_contract(&c, &discharged_of(&refs));
    assert_eq!(n as usize, c.equations.len());
    assert!(is_lean_proved_with_grounding(&c, n));
    assert!(!is_l4_self_declared_with_grounding(&c, n));
}

#[test]
fn ev8b_a_withheld_summary_grants_nothing() {
    let c = contract_naming_theorems(1);
    let d = crate::discharge::summary::Discharged {
        theorems: std::collections::BTreeSet::new(),
        withheld: Some("stale discharge".into()),
        ..Default::default()
    };
    assert_eq!(count_discharged_for_contract(&c, &d), 0);
}

// ── ONT-3b (#4073): the refinement filter on the discharge grant ──

#[test]
fn refine_without_a_formalization_record_grants_nothing_l4() {
    let dir = tempfile::tempdir().expect("tempdir");
    let mut d = discharged_of(&["ProvableContracts.Softmax.sum_one"]);
    d.module_of.insert(
        "ProvableContracts.Softmax.sum_one".into(),
        "ProvableContracts/Softmax.lean".into(),
    );
    super::refine(dir.path(), &mut d);
    assert!(d.theorems.is_empty(), "no model covers the module: not L4");
    assert!(d.unrefined.contains("ProvableContracts.Softmax.sum_one"));
}

#[test]
fn refine_leaves_an_empty_grant_untouched() {
    let dir = tempfile::tempdir().expect("tempdir");
    let mut d = discharged_of(&[]);
    super::refine(dir.path(), &mut d);
    assert!(d.theorems.is_empty() && d.unrefined.is_empty());
}

#[test]
fn workspace_root_is_the_nearest_workspace_manifest() {
    let dir = tempfile::tempdir().expect("tempdir");
    let ws = dir.path().join("ws");
    let inner = ws.join("crates/c/lean");
    std::fs::create_dir_all(&inner).expect("mkdir");
    std::fs::write(ws.join("Cargo.toml"), "[workspace]\nmembers = []\n").expect("write");
    std::fs::write(ws.join("crates/c/Cargo.toml"), "[package]\nname = \"c\"\n").expect("write");
    let got = super::workspace_root(&inner);
    assert_eq!(got, std::fs::canonicalize(&ws).expect("canon"));
}

/// ONT-3b (#4073) falsifier for the call site: a green, fresh, closed discharge beside a Lean dir that has no
/// formalization record must reach the caller with NOTHING granted. If `grounding_from` skipped `refine`, the
/// summary's theorem would come back as L4 credit.
#[test]
fn grounding_applies_refinement_to_a_green_discharge() {
    use crate::discharge::summary::{Module, Summary, SUMMARY_FILE};
    let root = tempfile::tempdir().expect("tempdir");
    let lean = root.path().join("lean");
    std::fs::create_dir_all(&lean).expect("mkdir");
    let s = Summary {
        tree_sha: Some("t".into()),
        build_exit: Some(0),
        lake_exit: Some(0),
        leanchecker_exit: Some(0),
        axioms_ok: true,
        escapes_ok: true,
        challenges_closed: Some("1/1".into()),
        modules: vec![Module {
            path: "ProvableContracts/Softmax.lean".into(),
            blake3: "b".into(),
            theorems: vec!["ProvableContracts.Softmax.sum_one".into()],
        }],
        ..Summary::default()
    };
    std::fs::write(
        root.path().join(SUMMARY_FILE),
        serde_json::to_string(&s).expect("json"),
    )
    .expect("write summary");
    let g = super::grounding_from(&[lean.as_path()], |_| Some("t".into()));
    assert!(matches!(g.source, super::L4Source::Discharge));
    assert!(
        g.discharged.withheld.is_none(),
        "fixture must be a granting discharge, else the test proves nothing: {:?}",
        g.discharged.withheld
    );
    assert!(
        !g.discharged.grants("ProvableContracts.Softmax.sum_one"),
        "no model covers the module, so the call site must drop its credit"
    );
    assert!(g
        .discharged
        .unrefined
        .contains("ProvableContracts.Softmax.sum_one"));
}

// ── #4351: the sorry scan reads TOKENS, not bytes ─────────────────

/// The case table for `lean_has_sorry`. A comment that only mentions `sorry` grounds; every other
/// row either admits a hole or is shaped to HIDE one from a scanner that gets comments wrong.
#[test]
fn lean_sorry_token_case_table() {
    let rows: &[(&str, bool, &str)] = &[
        // grounds (false): the word is commentary only
        ("theorem t : True := trivial", false, "no sorry at all"),
        (
            "-- sorry here\ntheorem t : True := trivial",
            false,
            "line comment",
        ),
        (
            "/-- compiles sorry-free -/\ntheorem t : True := trivial",
            false,
            "doc comment (#4351)",
        ),
        (
            "/-! module: sorry-free -/\ntheorem t : True := trivial",
            false,
            "module doc comment",
        ),
        (
            "/- a /- b -/ sorry -/\ntheorem t : True := trivial",
            false,
            "sorry inside a NESTED comment",
        ),
        (
            "theorem sorry_free : True := trivial",
            false,
            "identifier sorry_free",
        ),
        (
            "theorem t' : True := trivial -- no sorry",
            false,
            "trailing line comment at EOF",
        ),
        // denies (true): a real hole
        ("theorem t : False := sorry", true, "term sorry"),
        ("theorem t : False := by\n  sorry", true, "tactic sorry"),
        (
            "theorem t : False := by sorry -- ok",
            true,
            "sorry before a comment",
        ),
        (
            "/- a /- b -/ -/ theorem t : False := sorry",
            true,
            "sorry after a nested comment closes",
        ),
        (
            "def s := \"sorry\"",
            true,
            "sorry in a string counts (code, not commentary)",
        ),
        ("def s := r#\"x \" sorry\"#", true, "sorry in a raw string"),
        // denies (true): a real hole a naive comment stripper would hide
        (
            "def s := \"--\"\ntheorem t : False := by sorry",
            true,
            "string holding -- is not a comment",
        ),
        (
            "def s := \"/-\" theorem t : False := sorry",
            true,
            "string holding /- is not a comment",
        ),
        (
            "def c := '\"' theorem t : False := sorry -- \"",
            true,
            "char literal '\"' opens no string",
        ),
        (
            "def s := \"a\\\" -- b\" theorem t : False := sorry",
            true,
            "escaped quote keeps the string open",
        ),
        // denies (true): does not compile, so proves nothing
        (
            "/- unterminated\ntheorem t : True := trivial",
            true,
            "EOF inside a block comment",
        ),
        ("def s := \"unterminated", true, "EOF inside a string"),
    ];
    for (src, want, why) in rows {
        assert_eq!(guarded(|| lean_has_sorry(src)), *want, "{why}: {src:?}");
    }
}

/// The three in-tree files #4351 names are sorry-free except in their doc comments, and each now
/// grounds; `Theorems.<Domain>.<Stem>` is registered for the domain.file citation form.
#[test]
fn lean_scan_grounds_doc_comment_sorry_and_domain_file_form() {
    let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
        .join("../../crates/aprender-contracts-staging/lean/ProvableContracts/Theorems");
    for rel in [
        "TensorTranspose/Roundtrip.lean",
        "Metrics/RegressionAnalytic.lean",
        "AbsolutePosition/Core.lean",
    ] {
        let content = std::fs::read_to_string(root.join(rel)).expect("in-tree lean file");
        assert!(
            content.contains("sorry"),
            "{rel}: the byte-level trap this test pins"
        );
        assert!(
            !guarded(move || lean_has_sorry(&content)),
            "{rel}: its only sorry is commentary"
        );
    }

    let base = tempfile::tempdir().expect("tempdir");
    let dom = base
        .path()
        .join("ProvableContracts/Theorems/GgufExportSymmetry");
    std::fs::create_dir_all(&dom).expect("mkdir");
    std::fs::write(
        dom.join("Roundtrip.lean"),
        "/-- sorry-free -/\ntheorem dtype_roundtrip : True := trivial\n",
    )
    .expect("write");
    let holed = base.path().join("ProvableContracts/Theorems/Holed");
    std::fs::create_dir_all(&holed).expect("mkdir");
    std::fs::write(
        holed.join("Open.lean"),
        "theorem open_goal : False := by sorry\n",
    )
    .expect("write");

    let base_str = base.path().to_str().expect("utf8 path").to_string();
    let names = guarded(move || scan_theorem_base(&base_str));
    assert!(
        names.contains("Theorems.GgufExportSymmetry.Roundtrip"),
        "domain.file form: {names:?}"
    );
    assert!(names.contains("Theorems.DtypeRoundtrip"));
    assert!(
        !names
            .iter()
            .any(|n| n.contains("Holed") || n.contains("OpenGoal")),
        "a real sorry grounds nothing"
    );
}

/// `sorry` is a token only with no identifier byte before it; at byte 0 there is nothing before it (#4587).
#[test]
fn sorry_token_at_checks_the_byte_before() {
    assert!(super::sorry_token_at(b"sorry", 0));
    assert!(super::sorry_token_at(b" sorry", 1));
    assert!(!super::sorry_token_at(b"xsorry", 1));
}

/// A nested `/-` advances two bytes past where it starts, not to twice its offset (#4587).
#[test]
fn step_block_comment_opens_a_nested_comment_two_bytes_on() {
    assert_eq!(super::step_block_comment(b"xxx/-", 3, 1), (5, 2));
    assert_eq!(super::step_block_comment(b"xxx-/", 3, 2), (5, 1));
    assert_eq!(super::step_block_comment(b"xxxab", 3, 1), (4, 1));
}

/// Run `f` on a helper thread with a 60 s deadline. A mutated cursor that never advances would spin
/// forever; this PANICS (failing only the calling test) instead of hanging the lib binary.
fn guarded<T: Send + 'static>(f: impl FnOnce() -> T + Send + 'static) -> T {
    let (tx, rx) = std::sync::mpsc::channel();
    std::thread::spawn(move || {
        let _ = tx.send(f());
    });
    rx.recv_timeout(std::time::Duration::from_secs(60))
        .expect("the Lean scan did not finish within 60s: its cursor is not advancing")
}

/// Collapse a `LeanScan` to (kind, resume byte) so tests can pin the exact cursor (#4587).
fn show(s: super::LeanScan) -> (u8, usize) {
    match s {
        super::LeanScan::Next(j) => (0, j),
        super::LeanScan::OpenBlock(j) => (1, j),
        super::LeanScan::Sorry => (2, 0),
        super::LeanScan::EndsInLineComment => (3, 0),
    }
}

/// A `--` comment resumes one byte past its newline; one with no newline ends the scan.
#[test]
fn scan_code_at_line_comment_resumes_after_the_newline() {
    assert_eq!(show(super::scan_code_at(b"ab--c\nd", 2)), (0, 6));
    assert_eq!(show(super::scan_code_at(b"ab--c", 2)), (3, 0));
    assert_eq!(show(super::scan_code_at(b"a/-b", 1)), (1, 3));
}

/// `r"` opens a raw string only when no identifier byte precedes the `r`; a `'` likewise.
#[test]
fn scan_code_at_raw_string_and_char_need_a_non_ident_prefix() {
    assert_eq!(show(super::scan_code_at(b" r\"x\"", 1)), (0, 5));
    assert_eq!(show(super::scan_code_at(b" r\"sorry\"", 1)), (2, 0));
    assert_eq!(show(super::scan_code_at(b"xr\"a\"", 1)), (0, 2));
    assert_eq!(show(super::scan_code_at(b" r#\"x\"#", 1)), (0, 7));
    assert_eq!(show(super::scan_code_at(b"r\"x\"", 0)), (0, 4));
    assert_eq!(show(super::scan_code_at(b"a'b", 1)), (0, 2));
    assert_eq!(show(super::scan_code_at(b" 'a'", 1)), (0, 4));
    assert_eq!(show(super::scan_code_at(b" sorry", 1)), (2, 0));
    assert_eq!(show(super::scan_code_at(b"abc", 1)), (0, 2));
}

/// Raw strings: the cursor lands one past the closing `"` + hashes; a body `sorry` counts.
#[test]
fn scan_raw_string_pins_open_close_and_resume() {
    assert_eq!(show(super::scan_raw_string(b"r\"ab\"", 0)), (0, 5));
    assert_eq!(show(super::scan_raw_string(b"r##\"a\"#b\"##", 0)), (0, 11));
    assert_eq!(show(super::scan_raw_string(b" r#\"x\"#", 1)), (0, 7));
    assert_eq!(show(super::scan_raw_string(b"  r#x", 2)), (0, 3));
    assert_eq!(show(super::scan_raw_string(b"r#x", 0)), (0, 1));
    assert_eq!(show(super::scan_raw_string(b"r\"sorry\"", 0)), (2, 0));
    assert_eq!(show(super::scan_raw_string(b"r\"a\"sorry", 0)), (0, 4));
    assert_eq!(show(super::scan_raw_string(b"r\"abc", 0)), (2, 0));
    assert_eq!(show(super::scan_raw_string(b"r\"ab\"x\"", 0)), (0, 5));
}

/// Strings: `\` skips two bytes, the cursor lands one past the closing quote.
#[test]
fn scan_string_pins_escape_and_resume() {
    assert_eq!(show(super::scan_string(b"\"ab\"", 0)), (0, 4));
    assert_eq!(show(super::scan_string(b" \"a\\\"b\"c", 1)), (0, 7));
    assert_eq!(show(super::scan_string(b"\"a\\\"", 0)), (2, 0));
    assert_eq!(show(super::scan_string(b"\"sorry\"", 0)), (2, 0));
    assert_eq!(show(super::scan_string(b"\"a\"sorry", 0)), (0, 3));
    assert_eq!(show(super::scan_string(b"\"abc", 0)), (2, 0));
    assert_eq!(show(super::scan_string(b"x\"a\\nb\"", 1)), (0, 7));
}

/// A char literal is skipped to just past its closing `'`; a non-literal advances one byte.
#[test]
fn skip_char_literal_pins_each_branch() {
    assert_eq!(super::skip_char_literal(b" 'a' x", 1), 4);
    assert_eq!(super::skip_char_literal(b" '\\n' x", 1), 5);
    assert_eq!(super::skip_char_literal(b" '\\'' x", 1), 5);
    assert_eq!(super::skip_char_literal(b" 'a", 1), 2);
    assert_eq!(super::skip_char_literal(b"'a' ", 0), 3);
    assert_eq!(super::skip_char_literal(b"'\\n'", 0), 4);
    // the closing quote must lie within i+7: 'é' (2 bytes) fits, a far quote does not
    assert_eq!(super::skip_char_literal("'é'".as_bytes(), 0), 4);
    assert_eq!(super::skip_char_literal(b"'abcdefgh'", 0), 1);
    assert_eq!(super::skip_char_literal(b"'abcde'", 0), 7);
    assert_eq!(super::skip_char_literal(b"'a' 'b'", 0), 3);
    assert_eq!(super::skip_char_literal(b"'", 0), 1);
}