use super::*;
fn contracts_dir() -> std::path::PathBuf {
std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../contracts")
}
fn knob_corpus() -> (tempfile::TempDir, std::path::PathBuf) {
let tmp = tempfile::tempdir().unwrap();
let dir = tmp.path().join("contracts");
std::fs::create_dir_all(&dir).unwrap();
for stem in [
"softmax-kernel-v1",
"special-tokens-registry-v1",
"arch-constraints-v1",
] {
let f = format!("{stem}.yaml");
std::fs::copy(contracts_dir().join(&f), dir.join(&f)).unwrap();
}
(tmp, dir)
}
#[test]
fn lint_passes_on_real_contracts() {
let report = run_lint(&LintConfig::new(&contracts_dir(), None, 0.0));
lint_report_serializes_to_json(&report);
lint_cache_populates_stats(&report);
every_gate_verdict_agrees_with_passed_and_skipped_on_the_real_corpus(&report);
valid_under_is_computed_on_the_real_corpus(&report);
the_refinement_gate_measured_head_against_base(&report);
assert!(report.passed, "lint should pass: {report:?}");
assert_eq!(report.gates.len(), 23);
}
fn the_refinement_gate_measured_head_against_base(report: &LintReport) {
let gate = report
.gates
.iter()
.find(|g| g.name == refinement_gate::GATE)
.expect("the refinement gate is one of the 22");
let base_resolves = std::process::Command::new("git")
.arg("-C")
.arg(contracts_dir())
.args(["rev-parse", "--verify", "--quiet", "origin/main^{commit}"])
.output()
.is_ok_and(|o| o.status.success());
if base_resolves || std::env::var_os("CI").is_some() {
assert!(
!gate.skipped,
"the refinement gate declined, so nothing compared HEAD with BASE: {:?}",
gate.detail
);
}
}
fn lint_score_gate_fails_with_high_threshold(report: &LintReport) {
assert!(!report.passed);
assert!(!report.findings.is_empty());
}
#[test]
fn lint_empty_dir() {
let tmp = tempfile::tempdir().unwrap();
let dir = tmp.path().join("contracts");
std::fs::create_dir_all(&dir).unwrap();
let config = LintConfig::new(&dir, None, 0.0);
let report = run_lint(&config);
assert!(report.passed, "empty dir should pass: {report:?}");
assert_eq!(pv_state_dir(&dir), tmp.path().join(".pv"));
assert!(tmp.path().join(".pv/lint-previous.json").is_file());
}
#[test]
fn no_lint_test_points_the_lint_at_a_bare_tempdir() {
let bare = |line: &str| {
let l: String = line.chars().filter(|c| !c.is_whitespace()).collect();
["(tmp.path()", "(&tmp.path()"].iter().any(|arg| {
let pat = format!("{}{arg}", concat!("LintConfig::", "new"));
l.match_indices(&pat)
.any(|(k, _)| matches!(l[k + pat.len()..].chars().next(), Some(',' | ')')))
})
};
for (line, want) in [
(
concat!("run_lint(&LintConfig::new", "(tmp.path(), None, 0.0));"),
true,
),
(
concat!("let c = LintConfig::new", "( &tmp.path(), None, 0.0);"),
true,
),
("let c = LintConfig::new(&corpus, None, 0.0);", false),
(
"let c = LintConfig::new(&tmp.path().join(\"contracts\"), None, 0.0);",
false,
),
] {
assert_eq!(bare(line), want, "case table: {line}");
}
let lint_src = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("src/lint");
let mut scanned = 0;
for entry in std::fs::read_dir(&lint_src).unwrap() {
let path = entry.unwrap().path();
if path.extension().is_some_and(|e| e == "rs") {
scanned += 1;
let src = std::fs::read_to_string(&path).unwrap();
for (i, line) in src.lines().enumerate() {
assert!(
!bare(line),
"{}:{}: lints a bare tempdir: {line}",
path.display(),
i + 1
);
}
}
}
assert!(
scanned > 5,
"scanned only {scanned} files under {}",
lint_src.display()
);
}
fn lint_report_serializes_to_json(report: &LintReport) {
let json = serde_json::to_string_pretty(report).unwrap();
assert!(json.contains("\"passed\""));
}
#[test]
fn gate_detail_variants() {
let skipped = GateDetail::Skipped {
reason: "test".into(),
};
let json = serde_json::to_string(&skipped).unwrap();
assert!(json.contains("skipped"));
}
#[test]
fn lint_findings_on_failure() {
let report = run_lint(&LintConfig::new(&contracts_dir(), None, 0.99));
lint_score_gate_fails_with_high_threshold(&report);
lint_sarif_output(&report);
assert!(report.findings.iter().any(|f| f.rule_id == "PV-SCR-001"));
}
#[test]
fn lint_severity_filter() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.99);
let unfiltered = run_lint(&config);
assert!(
unfiltered
.findings
.iter()
.any(|f| f.severity < RuleSeverity::Error),
"knob corpus has no below-Error finding — the filter test is vacuous"
);
config.severity_filter = Some(RuleSeverity::Error);
let report = run_lint(&config);
assert!(report
.findings
.iter()
.all(|f| f.severity >= RuleSeverity::Error));
assert!(report.findings.len() < unfiltered.findings.len());
}
#[test]
fn lint_suppression_by_rule() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.99);
config.suppressed_rules = vec!["PV-SCR-001".into()];
let report = run_lint(&config);
assert!(report.findings.iter().any(|f| f.rule_id == "PV-SCR-001"));
for f in &report.findings {
if f.rule_id == "PV-SCR-001" {
assert!(f.suppressed);
}
}
}
#[test]
fn lint_strict_mode() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.0);
config.strict = true;
let report = run_lint(&config);
for f in &report.findings {
assert_ne!(f.severity, RuleSeverity::Warning);
}
}
fn lint_sarif_output(report: &LintReport) {
let sarif_log = sarif::findings_to_sarif(&report.findings, "0.1.0");
let json = sarif::sarif_to_json(&sarif_log, true);
assert!(json.contains("sarif-schema-2.1.0"));
assert!(json.contains("PV-SCR-001"));
}
#[test]
fn skipped_gate_creates_correct_result() {
let g = skipped_gate("test", "reason");
assert_eq!(g.name, "test");
assert!(!g.passed);
assert!(g.skipped);
}
fn lint_cache_populates_stats(report: &LintReport) {
assert!(report.cache_stats.total > 0);
assert_eq!(
report.cache_stats.total,
report.cache_stats.hits + report.cache_stats.misses
);
}
#[test]
fn lint_no_cache_skips_stats() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.0);
config.no_cache = true;
let report = run_lint(&config);
assert_eq!(report.cache_stats.total, 0);
}
#[test]
fn lint_cache_second_run_hits() {
let tmp = tempfile::tempdir().unwrap();
let tmp_dir = tmp.path().join("contracts");
std::fs::create_dir_all(&tmp_dir).unwrap();
let src = contracts_dir().join("softmax-kernel-v1.yaml");
std::fs::copy(&src, tmp_dir.join("softmax-kernel-v1.yaml")).unwrap();
let config = LintConfig::new(&tmp_dir, None, 0.0);
let r1 = run_lint(&config);
assert!(r1.cache_stats.misses > 0);
let r2 = run_lint(&config);
assert!(r2.cache_stats.hits > 0);
}
#[test]
fn lint_validation_failure_skips_audit_and_score() {
let tmp = tempfile::tempdir().unwrap();
let dir = tmp.path().join("contracts");
std::fs::create_dir_all(&dir).unwrap();
std::fs::write(dir.join("bad.yaml"), "not: valid: yaml: {{{{").unwrap();
let config = LintConfig::new(&dir, None, 0.0);
let report = run_lint(&config);
assert!(!report.passed);
assert_eq!(report.gates.len(), 23);
assert!(!report.gates[0].passed); assert!(report.gates[1].skipped); assert!(report.gates[2].skipped); assert!(report.gates[3].skipped); assert!(report.gates[4].skipped); assert!(report.gates[5].skipped); assert!(report.gates[6].skipped); assert!(report.gates[7].skipped); assert!(report.gates[8].skipped); }
#[test]
fn lint_suppression_by_stem() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.99);
config.suppressed_findings = vec!["special-tokens-registry-v1".into()];
let report = run_lint(&config);
assert!(report
.findings
.iter()
.any(|f| f.contract_stem.as_deref() == Some("special-tokens-registry-v1")));
for f in &report.findings {
if f.contract_stem.as_deref() == Some("special-tokens-registry-v1") {
assert!(f.suppressed);
}
}
}
#[test]
fn lint_suppression_by_file_pattern() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.99);
config.suppressed_files = vec!["arch-constraints".into()];
let report = run_lint(&config);
assert!(report
.findings
.iter()
.any(|f| f.file.contains("arch-constraints")));
for f in &report.findings {
if f.file.contains("arch-constraints") {
assert!(f.suppressed);
}
}
}
#[test]
fn lint_severity_override() {
let (_tmp, dir) = knob_corpus();
let mut config = LintConfig::new(&dir, None, 0.99);
let mut overrides = HashMap::new();
overrides.insert("PV-SCR-001".into(), RuleSeverity::Warning);
config.severity_overrides = overrides;
let report = run_lint(&config);
assert!(report.findings.iter().any(|f| f.rule_id == "PV-SCR-001"));
for f in &report.findings {
if f.rule_id == "PV-SCR-001" {
assert_eq!(f.severity, RuleSeverity::Warning);
}
}
}
#[test]
fn lifecycle_first_run_all_new() {
let tmp = tempfile::tempdir().unwrap();
let contract_dir = tmp.path().join("contracts");
std::fs::create_dir_all(&contract_dir).unwrap();
let src = contracts_dir().join("softmax-kernel-v1.yaml");
std::fs::copy(&src, contract_dir.join("softmax-kernel-v1.yaml")).unwrap();
let config = LintConfig::new(&contract_dir, None, 0.99);
let report = run_lint(&config);
let active: Vec<_> = report.findings.iter().filter(|f| !f.suppressed).collect();
assert!(!active.is_empty(), "should have findings");
assert!(
active.iter().all(|f| f.is_new),
"first run: all findings should be new"
);
}
#[test]
fn lifecycle_second_run_pre_existing() {
let tmp = tempfile::tempdir().unwrap();
let contract_dir = tmp.path().join("contracts");
std::fs::create_dir_all(&contract_dir).unwrap();
let src = contracts_dir().join("softmax-kernel-v1.yaml");
std::fs::copy(&src, contract_dir.join("softmax-kernel-v1.yaml")).unwrap();
let config = LintConfig::new(&contract_dir, None, 0.99);
let _ = run_lint(&config);
let report2 = run_lint(&config);
let active: Vec<_> = report2.findings.iter().filter(|f| !f.suppressed).collect();
assert!(!active.is_empty(), "should have findings");
assert!(
active.iter().all(|f| !f.is_new),
"second identical run: no finding should be new"
);
}
#[test]
fn lifecycle_persists_fingerprints() {
let tmp = tempfile::tempdir().unwrap();
let contract_dir = tmp.path().join("contracts");
std::fs::create_dir_all(&contract_dir).unwrap();
let src = contracts_dir().join("softmax-kernel-v1.yaml");
std::fs::copy(&src, contract_dir.join("softmax-kernel-v1.yaml")).unwrap();
let config = LintConfig::new(&contract_dir, None, 0.99);
let _ = run_lint(&config);
let previous_path = tmp.path().join(".pv").join("lint-previous.json");
assert!(
previous_path.exists(),
".pv/lint-previous.json should be created"
);
let content = std::fs::read_to_string(&previous_path).unwrap();
let fps: std::collections::HashSet<String> = serde_json::from_str(&content).unwrap();
assert!(!fps.is_empty(), "fingerprint set should not be empty");
}
#[test]
fn lifecycle_mark_new_findings_unit() {
use super::mark_new_findings;
let tmp = tempfile::tempdir().unwrap();
let contract_dir = tmp.path().join("contracts");
std::fs::create_dir_all(&contract_dir).unwrap();
let mut findings = vec![
finding::LintFinding::new("PV-VAL-001", RuleSeverity::Error, "msg1", "a.yaml"),
finding::LintFinding::new("PV-VAL-002", RuleSeverity::Warning, "msg2", "b.yaml"),
];
mark_new_findings(&mut findings, &contract_dir);
assert!(findings[0].is_new);
assert!(findings[1].is_new);
for f in &mut findings {
f.is_new = false;
}
mark_new_findings(&mut findings, &contract_dir);
assert!(!findings[0].is_new);
assert!(!findings[1].is_new);
findings.push(finding::LintFinding::new(
"PV-VAL-003",
RuleSeverity::Info,
"msg3",
"c.yaml",
));
for f in &mut findings {
f.is_new = false;
}
mark_new_findings(&mut findings, &contract_dir);
assert!(
!findings[0].is_new,
"pre-existing finding should not be new"
);
assert!(
!findings[1].is_new,
"pre-existing finding should not be new"
);
assert!(findings[2].is_new, "newly added finding should be new");
}
fn every_gate_verdict_agrees_with_passed_and_skipped_on_the_real_corpus(report: &LintReport) {
for g in &report.gates {
assert_eq!(
g.verdict,
Verdict::from_gate(g.passed, g.skipped),
"gate {}",
g.name
);
}
let armed = ArmedGates::default_set();
let expected = armed
.names()
.iter()
.map(|n| {
report.gates.iter().find(|g| &g.name == n).map_or(
Verdict::Unknown(crate::ontology::verdict::Reason::NotRun),
|g| g.verdict,
)
})
.fold(Verdict::Pass, Verdict::meet);
assert_eq!(report.verdict, expected);
assert_eq!(
report.verdict,
Verdict::Pass,
"the repo corpus passes its armed meet"
);
assert_eq!(
report.not_armed,
vec![
"reverse-coverage".to_string(),
"sigma".to_string(),
"relations".to_string(),
"shapes".to_string(),
"valid-under".to_string(),
"theorem-pairing".to_string(),
"depends-on-present".to_string(),
"proved-is-derived".to_string(),
"references-resolve".to_string(),
"challenge-fresh".to_string(),
"ont-consistency".to_string(),
"refines".to_string(),
"bindings".to_string(),
"refinement".to_string(),
"evidence".to_string(),
],
"challenge-fresh is reported, never armed by default: it moves only via `make ont-ratchet`"
);
}
#[test]
fn a_gate_a_flag_ran_is_reported_but_not_armed() {
let tmp = tempfile::tempdir().unwrap();
let corpus = tmp.path().join("contracts");
std::fs::create_dir_all(&corpus).unwrap();
std::fs::copy(
contracts_dir().join("softmax-kernel-v1.yaml"),
corpus.join("softmax-kernel-v1.yaml"),
)
.unwrap();
let mut config = LintConfig::new(&corpus, None, 0.0);
config.strict_test_binding = true;
let report = run_lint(&config);
assert!(
report.gates.iter().any(|g| g.name == "strict-test-binding"),
"the flag ran the gate"
);
assert!(
report.not_armed.iter().any(|n| n == "strict-test-binding"),
"not declared, so not armed: {:?}",
report.not_armed
);
assert!(!report
.armed_gates
.iter()
.any(|g| g.name == "strict-test-binding"));
assert_eq!(report.armed_gates.len(), 8);
}
fn valid_under_is_computed_on_the_real_corpus(report: &LintReport) {
let g = report
.gates
.iter()
.find(|g| g.name == "valid-under")
.expect("gate 13 is in every run");
assert!(
!g.skipped && g.passed,
"computed and Pass on the repo corpus: {g:?}"
);
}
#[test]
fn valid_under_is_computed_when_validation_passes_and_skipped_when_it_fails() {
let tmp = tempfile::tempdir().unwrap();
let corpus = tmp.path().join("contracts");
std::fs::create_dir_all(&corpus).unwrap();
let fixture = contracts_dir().join("../tests/fixtures/ont/valid-under-ok");
for f in ["ontology.yaml", "fixture-vu-v1.yaml"] {
std::fs::copy(fixture.join(f), corpus.join(f)).unwrap();
}
std::fs::write(corpus.join("bad.yaml"), "not: valid: yaml: {{{{").unwrap();
let report = run_lint(&LintConfig::new(&corpus, None, 0.0));
let g = report
.gates
.iter()
.find(|g| g.name == "valid-under")
.expect("gate 13 is in every run");
assert!(
g.skipped,
"validation failed, so the gate is skipped: {g:?}"
);
assert!(
matches!(&g.detail, GateDetail::Skipped { reason } if reason == "validation failed"),
"{g:?}"
);
}
fn challenge_tree(bad: bool) -> tempfile::TempDir {
let d = tempfile::tempdir().expect("tempdir");
let w = |rel: &str, text: &str| {
let p = d.path().join(rel);
std::fs::create_dir_all(p.parent().expect("parent")).expect("mkdir");
std::fs::write(p, text).expect("write");
};
let mut root = String::new();
if !bad {
root.push_str("import ProvableContracts.Theorems.Gelu.Bound\n");
w(
"lean/ProvableContracts/Theorems/Gelu/Bound.lean",
"namespace ProvableContracts.Gelu\n\
theorem gelu_bound (x : Nat) : x ≤ x + 1 := Nat.le_succ x\n\
end ProvableContracts.Gelu\n",
);
w(
"contracts/gelu-v1.yaml",
"equations:\n e:\n lean_theorem: ProvableContracts.Gelu.gelu_bound\n",
);
}
root.push_str("import ProvableContracts.Theorems.Bad.Bound\n");
w(
"lean/ProvableContracts/Theorems/Bad/Bound.lean",
"namespace ProvableContracts.Bad\n\
theorem bad_bound : True\n\
def g := 1\n\
end ProvableContracts.Bad\n",
);
w(
"contracts/bad-v1.yaml",
"equations:\n e:\n lean_theorem: ProvableContracts.Bad.bad_bound\n",
);
w("lean/ProvableContracts.lean", &root);
d
}
fn challenge_errors(g: &GateResult) -> usize {
match g.detail {
GateDetail::Validate { errors, .. } => errors,
ref other => panic!("challenge-fresh carries a Validate detail: {other:?}"),
}
}
#[test]
fn challenge_fresh_is_green_when_the_challenge_files_match() {
let t = challenge_tree(false);
std::fs::remove_file(t.path().join("contracts/bad-v1.yaml")).expect("rm");
let lean = t.path().join("lean");
let contracts = t.path().join("contracts");
let r = crate::discharge::challenge::render(&lean, &contracts).expect("render");
assert!(!r.files.is_empty() && r.unrestated.is_empty());
crate::discharge::challenge::write(&lean, &r).expect("write");
let g = challenge_result(&contracts);
assert!(!g.skipped, "one challenge present is measured: {g:?}");
assert!(g.passed, "{g:?}");
assert_eq!(challenge_errors(&g), 0);
}
#[test]
fn challenge_fresh_fails_on_a_stale_file_alone() {
let t = challenge_tree(false);
std::fs::remove_file(t.path().join("contracts/bad-v1.yaml")).expect("rm");
let g = challenge_result(&t.path().join("contracts"));
assert!(!g.skipped && !g.passed, "{g:?}");
assert_eq!(challenge_errors(&g), 1);
}
#[test]
fn challenge_fresh_fails_on_an_unrestated_root_alone() {
let t = challenge_tree(true);
let g = challenge_result(&t.path().join("contracts"));
assert!(
!g.skipped,
"an unrestated root is not zero challenges: {g:?}"
);
assert!(!g.passed, "{g:?}");
assert_eq!(challenge_errors(&g), 1);
}
#[test]
fn challenge_fresh_counts_stale_plus_unrestated() {
let t = challenge_tree(false);
let g = challenge_result(&t.path().join("contracts"));
assert!(!g.skipped && !g.passed, "{g:?}");
assert_eq!(challenge_errors(&g), 2, "{g:?}");
}
fn ver002(report: &LintReport) -> Vec<(String, String)> {
report
.findings
.iter()
.filter(|f| f.rule_id == "PV-VER-002")
.map(|f| (f.file.clone(), f.message.clone()))
.collect()
}
#[test]
fn strict_test_binding_only_answers_as_the_full_run_does() {
let (_tmp, dir) = knob_corpus();
let mut full = LintConfig::new(&dir, None, 0.0);
full.strict_test_binding = true;
full.no_cache = true;
let full = run_lint(&full);
let mut only = LintConfig::new(&dir, None, 0.0);
only.strict_test_binding = true;
only.strict_test_binding_only = true;
let only = run_lint(&only);
let names: Vec<&str> = only.gates.iter().map(|g| g.name.as_str()).collect();
assert_eq!(names, ["validate", "strict-test-binding"]);
let gate = |r: &LintReport| {
let g = r
.gates
.iter()
.find(|g| g.name == "strict-test-binding")
.expect("the gate ran")
.clone();
(
g.passed,
g.skipped,
g.verdict,
serde_json::to_value(&g.detail).unwrap(),
)
};
assert_eq!(gate(&only), gate(&full));
assert!(
!gate(&only).1,
"the gate was skipped, so nothing was compared"
);
assert!(
!ver002(&full).is_empty(),
"no PV-VER-002 findings to compare"
);
assert_eq!(ver002(&only), ver002(&full));
assert_eq!(only.cache_stats.total, 0, "a scoped run must not cache");
assert_eq!(
only.verdict,
Verdict::Unknown(crate::ontology::verdict::Reason::NotRun)
);
}
#[test]
fn strict_test_binding_only_skips_the_gate_when_validate_fails() {
let tmp = tempfile::tempdir().unwrap();
let dir = tmp.path().join("contracts");
std::fs::create_dir_all(&dir).unwrap();
std::fs::write(dir.join("bad.yaml"), "not: valid: yaml: {{{{").unwrap();
let mut config = LintConfig::new(&dir, None, 0.0);
config.strict_test_binding = true;
config.strict_test_binding_only = true;
let report = run_lint(&config);
assert_eq!(report.gates.len(), 2);
assert!(!report.gates[0].passed, "validate must fail on bad.yaml");
assert!(report.gates[1].skipped, "{:?}", report.gates[1]);
assert!(!report.passed);
}