use crate::{
ArtifactBatch, Certificate, DryRunner, ExecutionResult, ExecutionStatus, Obligation,
ObligationBundle, VerifierRunner,
};
#[cfg(feature = "std")]
use std::fmt::Write as _;
#[cfg(not(feature = "std"))]
use alloc::{string::String, vec::Vec};
#[cfg(feature = "std")]
use std::{string::String, vec::Vec};
pub const VERIFICATION_REPORT_SCHEMA_VERSION: &str = "1";
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ObligationReport {
pub obligation_name: String,
pub summary: String,
pub artifact_path: Option<String>,
pub lean_theorem_ref: Option<String>,
pub lean_diagnostics: Vec<String>,
pub result: Option<ExecutionResult>,
pub certificate: Option<Certificate>,
pub kani_result: Option<ExecutionResult>,
pub kani_certificate: Option<Certificate>,
pub lean_certificate: Option<Certificate>,
}
impl ObligationReport {
pub fn status(&self) -> Option<ExecutionStatus> {
self.result.as_ref().map(|result| result.status)
}
pub fn succeeded(&self) -> bool {
self.result
.as_ref()
.map(|result| result.is_success())
.unwrap_or(false)
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ModuleReport {
pub module_name: String,
pub artifact_path: Option<String>,
pub theorem_refs: Vec<String>,
pub prelude_imports: Vec<String>,
pub prelude_aliases: Vec<String>,
pub diagnostics: Vec<String>,
pub theorem_failures: Vec<String>,
pub result: Option<ExecutionResult>,
pub certificate: Option<Certificate>,
}
impl ModuleReport {
pub fn status(&self) -> Option<ExecutionStatus> {
self.result.as_ref().map(|result| result.status)
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct VerificationReport {
pub bundle_name: String,
pub root: String,
pub obligations: Vec<ObligationReport>,
pub lean_module: Option<ModuleReport>,
}
impl VerificationReport {
pub fn obligation_count(&self) -> usize {
self.obligations.len()
}
pub fn success_count(&self) -> usize {
self.obligations
.iter()
.filter(|report| report.succeeded())
.count()
}
pub fn failure_count(&self) -> usize {
self.obligation_count().saturating_sub(self.success_count())
}
pub fn is_success(&self) -> bool {
self.failure_count() == 0
}
#[cfg(feature = "std")]
pub fn to_json(&self) -> String {
fn esc(s: &str) -> String {
s.replace('\\', "\\\\")
.replace('"', "\\\"")
.replace('\n', "\\n")
}
fn render_certificate_json(certificate: &Certificate) -> String {
format!(
"{{\"backend\":\"{}\",\"witness_ref\":\"{}\"}}",
esc(certificate.backend),
esc(&certificate.witness_ref)
)
}
let mut out = String::new();
let _ = write!(
out,
"{{\"schema_version\":\"{}\",\"bundle_name\":\"{}\",\"root\":\"{}\",\"success_count\":{},\"failure_count\":{},\"obligations\":[",
VERIFICATION_REPORT_SCHEMA_VERSION,
esc(&self.bundle_name),
esc(&self.root),
self.success_count(),
self.failure_count()
);
for (idx, obligation) in self.obligations.iter().enumerate() {
if idx > 0 {
out.push(',');
}
let _ = write!(
out,
"{{\"name\":\"{}\",\"summary\":\"{}\",\"status\":\"{}\",\"artifact_path\":{},\"lean_theorem_ref\":{},\"lean_diagnostic_count\":{},\"certificate\":{},\"kani_certificate\":{},\"lean_certificate\":{}}}",
esc(&obligation.obligation_name),
esc(&obligation.summary),
obligation
.status()
.map(|s| format!("{s:?}"))
.unwrap_or_else(|| "None".into()),
obligation
.artifact_path
.as_ref()
.map(|p| format!("\"{}\"", esc(p)))
.unwrap_or_else(|| "null".into()),
obligation
.lean_theorem_ref
.as_ref()
.map(|r| format!("\"{}\"", esc(r)))
.unwrap_or_else(|| "null".into()),
obligation.lean_diagnostics.len(),
obligation
.certificate
.as_ref()
.map(render_certificate_json)
.unwrap_or_else(|| "null".into()),
obligation
.kani_certificate
.as_ref()
.map(render_certificate_json)
.unwrap_or_else(|| "null".into()),
obligation
.lean_certificate
.as_ref()
.map(render_certificate_json)
.unwrap_or_else(|| "null".into())
);
}
out.push(']');
if let Some(module) = &self.lean_module {
let _ = write!(
out,
",\"lean_module\":{{\"module_name\":\"{}\",\"status\":\"{}\",\"theorem_count\":{},\"import_count\":{},\"alias_count\":{},\"diagnostic_count\":{},\"theorem_failure_count\":{},\"certificate\":{}}}",
esc(&module.module_name),
module
.status()
.map(|s| format!("{s:?}"))
.unwrap_or_else(|| "None".into()),
module.theorem_refs.len(),
module.prelude_imports.len(),
module.prelude_aliases.len(),
module.diagnostics.len(),
module.theorem_failures.len(),
module
.certificate
.as_ref()
.map(render_certificate_json)
.unwrap_or_else(|| "null".into())
);
}
out.push('}');
out
}
#[cfg(feature = "std")]
pub fn to_markdown(&self) -> String {
let mut out = String::new();
let _ = writeln!(out, "# Verification Report");
let _ = writeln!(out);
let _ = writeln!(
out,
"- Schema version: `{}`",
VERIFICATION_REPORT_SCHEMA_VERSION
);
let _ = writeln!(out, "- Bundle: `{}`", self.bundle_name);
let _ = writeln!(out, "- Root: `{}`", self.root);
let _ = writeln!(out, "- Successes: {}", self.success_count());
let _ = writeln!(out, "- Failures: {}", self.failure_count());
let _ = writeln!(out);
let _ = writeln!(
out,
"| Obligation | Status | Artifact | Lean theorem | Lean diagnostics | SMT certificate | Kani certificate | Lean certificate |"
);
let _ = writeln!(out, "|---|---|---|---|---|---|---|---|");
for obligation in &self.obligations {
let _ = writeln!(
out,
"| `{}` | `{}` | `{}` | `{}` | `{}` | `{}` | `{}` | `{}` |",
obligation.obligation_name,
obligation
.status()
.map(|s| format!("{s:?}"))
.unwrap_or_else(|| "None".into()),
obligation.artifact_path.as_deref().unwrap_or("-"),
obligation.lean_theorem_ref.as_deref().unwrap_or("-"),
if obligation.lean_diagnostics.is_empty() {
"-".into()
} else {
obligation.lean_diagnostics.join("; ")
},
obligation
.certificate
.as_ref()
.map(|c| c.backend)
.unwrap_or("-"),
obligation
.kani_certificate
.as_ref()
.map(|c| c.backend)
.unwrap_or("-"),
obligation
.lean_certificate
.as_ref()
.map(|c| c.backend)
.unwrap_or("-")
);
}
if let Some(module) = &self.lean_module {
let _ = writeln!(out);
let _ = writeln!(out, "Lean module: `{}`", module.module_name);
let _ = writeln!(out, "Lean theorems: {}", module.theorem_refs.len());
let _ = writeln!(out, "Lean imports: {}", module.prelude_imports.len());
let _ = writeln!(out, "Lean aliases: {}", module.prelude_aliases.len());
let _ = writeln!(out, "Lean diagnostics: {}", module.diagnostics.len());
let _ = writeln!(
out,
"Lean theorem failures: {}",
module.theorem_failures.len()
);
let _ = writeln!(
out,
"Lean certificate: `{}`",
module
.certificate
.as_ref()
.map(|c| c.witness_ref.as_str())
.unwrap_or("-")
);
}
out
}
}
pub fn dry_run_report(bundle: &ObligationBundle, artifacts: &ArtifactBatch) -> VerificationReport {
execute_report(bundle, artifacts, &DryRunner)
}
pub fn execute_report(
bundle: &ObligationBundle,
artifacts: &ArtifactBatch,
runner: &impl VerifierRunner,
) -> VerificationReport {
let lean_record = artifacts
.records
.iter()
.find(|record| record.path.ends_with(".lean"));
let lean_result = lean_record.and_then(|record| {
artifacts
.plans
.iter()
.find(|plan| {
plan.kind == crate::CommandKind::Lean
&& plan.input_files.iter().any(|f| f == &record.path)
})
.map(|plan| runner.run(plan))
});
let mut obligations = Vec::new();
for obligation in bundle.obligations() {
let artifact_path = artifacts
.records
.iter()
.find(|record| record.name == obligation.name)
.map(|record| record.path.clone());
let result = artifacts
.plans
.iter()
.find(|plan| {
plan.kind == crate::CommandKind::Smt
&& plan
.input_files
.iter()
.any(|f| artifact_path.as_ref() == Some(f))
})
.map(|plan| runner.run(plan));
let certificate = result.as_ref().and_then(|result| {
certificate_for_obligation(result, obligation, artifact_path.clone())
});
let kani_artifact_path = artifacts
.records
.iter()
.find(|record| record.name == format!("{}_kani", obligation.name))
.map(|record| record.path.clone());
let kani_result = artifacts
.plans
.iter()
.find(|plan| {
plan.kind == crate::CommandKind::Kani
&& plan
.input_files
.iter()
.any(|f| kani_artifact_path.as_ref() == Some(f))
})
.map(|plan| runner.run(plan));
let kani_certificate = kani_result.as_ref().and_then(|result| {
certificate_for_obligation(result, obligation, kani_artifact_path.clone())
});
let lean_theorem = artifacts
.lean_export
.as_ref()
.and_then(|export| export.theorem_for_obligation(&obligation.name).cloned());
let lean_theorem_ref = artifacts.lean_export.as_ref().and_then(|export| {
lean_theorem
.as_ref()
.map(|theorem| theorem.witness_ref(&export.module_name))
});
let lean_diagnostics = lean_result
.as_ref()
.and_then(|result| result.lean_output.as_ref())
.and_then(|output| {
lean_theorem.as_ref().map(|theorem| {
output
.theorem_diagnostics(theorem)
.into_iter()
.map(|diagnostic| diagnostic.message.clone())
.collect::<Vec<_>>()
})
})
.unwrap_or_default();
let lean_certificate = lean_result.as_ref().and_then(|result| {
lean_theorem_ref.as_ref().and_then(|witness_ref| {
certificate_for_witness::<crate::LeanCertificate>(
result,
obligation,
witness_ref.clone(),
lean_record.map(|record| record.path.clone()),
)
})
});
obligations.push(ObligationReport {
obligation_name: obligation.name.clone(),
summary: obligation.summary(),
artifact_path,
lean_theorem_ref,
lean_diagnostics,
result,
certificate,
kani_result,
kani_certificate,
lean_certificate,
});
}
let lean_module = lean_record.map(|record| {
let theorem_refs = artifacts
.lean_export
.as_ref()
.map(|export| {
export
.theorems
.iter()
.map(|theorem| theorem.witness_ref(&export.module_name))
.collect::<Vec<_>>()
})
.unwrap_or_default();
let prelude_imports = artifacts
.lean_export
.as_ref()
.map(|export| {
export
.prelude
.imports
.iter()
.map(|import| import.module.clone())
.collect::<Vec<_>>()
})
.unwrap_or_default();
let prelude_aliases = artifacts
.lean_export
.as_ref()
.map(|export| {
export
.prelude
.aliases
.iter()
.map(|alias| format!("{} := {}", alias.alias, alias.target))
.collect::<Vec<_>>()
})
.unwrap_or_default();
let diagnostics = lean_result
.as_ref()
.and_then(|result| result.lean_output.as_ref())
.map(|output| {
output
.diagnostics
.iter()
.map(|diagnostic| diagnostic.message.clone())
.collect::<Vec<_>>()
})
.unwrap_or_default();
let theorem_failures = match (
artifacts.lean_export.as_ref(),
lean_result
.as_ref()
.and_then(|result| result.lean_output.as_ref()),
) {
(Some(export), Some(output)) => export
.theorems
.iter()
.filter(|theorem| output.has_theorem_failure(theorem))
.map(|theorem| theorem.witness_ref(&export.module_name))
.collect::<Vec<_>>(),
_ => Vec::new(),
};
let certificate = lean_result.as_ref().and_then(|result| {
certificate_for_module(
result,
&record.name,
Some(record.path.clone()),
theorem_refs.len(),
)
});
ModuleReport {
module_name: record.name.clone(),
artifact_path: Some(record.path.clone()),
theorem_refs,
prelude_imports,
prelude_aliases,
diagnostics,
theorem_failures,
result: lean_result.clone(),
certificate,
}
});
VerificationReport {
bundle_name: bundle.name.clone(),
root: artifacts.root.clone(),
obligations,
lean_module,
}
}
fn certificate_for_obligation(
result: &ExecutionResult,
obligation: &Obligation,
artifact_path: Option<String>,
) -> Option<Certificate> {
let policy = result.verification_policy();
let witness_ref = format!("{}:{}", result.plan.executable, policy.witness_suffix);
match result.plan.kind {
crate::CommandKind::Smt => certificate_for_witness::<crate::SmtCertificate>(
result,
obligation,
witness_ref,
artifact_path,
),
crate::CommandKind::Lean => certificate_for_witness::<crate::LeanCertificate>(
result,
obligation,
witness_ref,
artifact_path,
),
crate::CommandKind::Kani => certificate_for_witness::<crate::KaniCertificate>(
result,
obligation,
witness_ref,
artifact_path,
),
}
}
fn certificate_for_witness<B: crate::VerificationBackend>(
result: &ExecutionResult,
obligation: &Obligation,
witness_ref: String,
artifact_path: Option<String>,
) -> Option<Certificate> {
if !result.is_success() {
return None;
}
let mut cert = Certificate::from_obligation::<B>(obligation, witness_ref);
if let Some(version) = &result.backend_version {
cert = cert.with_backend_version(version.clone());
}
if let Some(path) = artifact_path {
cert = cert.with_artifact_path(path);
}
Some(cert)
}
fn certificate_for_module(
result: &ExecutionResult,
module_name: &str,
artifact_path: Option<String>,
theorem_count: usize,
) -> Option<Certificate> {
if !result.is_success() {
return None;
}
let mut cert = Certificate::new(
<crate::LeanCertificate as crate::VerificationBackend>::NAME,
format!("Lean module {module_name}"),
crate::LeanCertificate::module_ref(module_name),
)
.with_notes(format!(
"verified module containing {theorem_count} theorem(s)"
));
if let Some(version) = &result.backend_version {
cert = cert.with_backend_version(version.clone());
}
if let Some(path) = artifact_path {
cert = cert.with_artifact_path(path);
}
Some(cert)
}
#[cfg(test)]
mod tests {
use super::*;
use crate::{
AlgebraicSignature, ArtifactLayout, LeanConfig, Origin, SmtConfig, Sort,
dry_run_bundle_artifacts,
};
#[test]
fn dry_run_report_attaches_results_to_all_obligations() {
let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
let bundle = ObligationBundle::monoid(
"sum_monoid",
Origin::new("karpal-core", "Monoid for Sum<i32>"),
&sig,
);
let layout = ArtifactLayout::new("target/karpal-verify-report-test");
let artifacts = dry_run_bundle_artifacts(
&bundle,
&layout,
"KarpalVerify",
&SmtConfig::default(),
&LeanConfig::default(),
);
let report = dry_run_report(&bundle, &artifacts);
assert_eq!(report.obligation_count(), 3);
assert!(
report
.obligations
.iter()
.all(|entry| entry.status() == Some(ExecutionStatus::DryRun))
);
assert_eq!(
report.lean_module.as_ref().unwrap().status(),
Some(ExecutionStatus::DryRun)
);
assert_eq!(report.lean_module.as_ref().unwrap().theorem_refs.len(), 3);
}
#[test]
fn successful_execution_yields_certificates() {
let sig = AlgebraicSignature::semigroup(Sort::Int, "combine");
let bundle = ObligationBundle::semigroup(
"sum_semigroup",
Origin::new("karpal-core", "Semigroup for Sum<i32>"),
&sig,
);
let layout = ArtifactLayout::new("target/karpal-verify-report-test-2");
let artifacts = dry_run_bundle_artifacts(
&bundle,
&layout,
"KarpalVerify",
&SmtConfig::default(),
&LeanConfig::default(),
);
struct SuccessRunner;
impl VerifierRunner for SuccessRunner {
fn run(&self, plan: &crate::InvocationPlan) -> ExecutionResult {
ExecutionResult {
plan: plan.clone(),
status: match plan.kind {
crate::CommandKind::Smt => ExecutionStatus::Unsat,
crate::CommandKind::Lean | crate::CommandKind::Kani => {
ExecutionStatus::Success
}
},
stdout: String::new(),
stderr: String::new(),
exit_code: Some(0),
backend_version: Some("tool 1.0".into()),
smt_output: Some(crate::SmtOutput {
status: Some(ExecutionStatus::Unsat),
model: None,
reason_unknown: None,
}),
lean_output: (plan.kind == crate::CommandKind::Lean).then(|| {
crate::LeanOutput {
diagnostics: vec![crate::LeanDiagnostic {
file: Some("lean/KarpalVerify.lean".into()),
line: Some(7),
column: Some(2),
severity: "error".into(),
message: "unsolved goals in theorem associativity".into(),
theorem_hits: vec!["associativity".into()],
}],
theorem_hits: vec!["associativity".into()],
}
}),
}
}
}
let report = execute_report(&bundle, &artifacts, &SuccessRunner);
assert_eq!(report.success_count(), 1);
assert!(report.obligations[0].certificate.is_some());
assert_eq!(
report.obligations[0]
.certificate
.as_ref()
.and_then(|c| c.backend_version.as_deref()),
Some("tool 1.0")
);
assert_eq!(
report
.lean_module
.as_ref()
.map(|module| module.theorem_refs.len()),
Some(1)
);
assert_eq!(
report.obligations[0].lean_theorem_ref.as_deref(),
Some("KarpalVerify.associativity")
);
assert_eq!(
report.obligations[0].lean_diagnostics,
vec!["unsolved goals in theorem associativity".to_string()]
);
assert_eq!(
report.obligations[0]
.lean_certificate
.as_ref()
.map(|certificate| certificate.backend),
Some("lean4")
);
assert_eq!(
report
.lean_module
.as_ref()
.and_then(|module| module.certificate.as_ref())
.map(|certificate| certificate.witness_ref.as_str()),
Some("KarpalVerify")
);
assert_eq!(
report
.lean_module
.as_ref()
.map(|module| module.theorem_failures.clone()),
Some(vec!["KarpalVerify.associativity".to_string()])
);
}
#[test]
fn report_serialization_includes_summary_data() {
let report = VerificationReport {
bundle_name: "demo".into(),
root: "target/demo".into(),
obligations: vec![ObligationReport {
obligation_name: "assoc".into(),
summary: "demo::assoc [associativity]".into(),
artifact_path: Some("target/demo/smt/assoc.smt2".into()),
lean_theorem_ref: None,
lean_diagnostics: Vec::new(),
result: None,
certificate: None,
kani_result: None,
kani_certificate: None,
lean_certificate: None,
}],
lean_module: None,
};
let json = report.to_json();
let markdown = report.to_markdown();
assert!(json.contains("\"schema_version\":\"1\""));
assert!(json.contains("\"bundle_name\":\"demo\""));
assert!(markdown.contains("# Verification Report"));
assert!(markdown.contains("Schema version: `1`"));
assert!(markdown.contains("`assoc`"));
}
#[test]
fn theorem_mapping_uses_exported_theorem_identity_not_obligation_name() {
let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
let bundle = ObligationBundle::semiring(
"sum_semiring",
Origin::new("karpal-core", "Semiring for Sum<i32>"),
&sig,
);
let layout = ArtifactLayout::new("target/karpal-verify-report-test-3");
let artifacts = dry_run_bundle_artifacts(
&bundle,
&layout,
"KarpalVerify",
&SmtConfig::default(),
&LeanConfig::default(),
);
struct TheoremNameRunner;
impl VerifierRunner for TheoremNameRunner {
fn run(&self, plan: &crate::InvocationPlan) -> ExecutionResult {
ExecutionResult {
plan: plan.clone(),
status: match plan.kind {
crate::CommandKind::Smt => ExecutionStatus::Unsat,
crate::CommandKind::Lean => ExecutionStatus::Failure,
crate::CommandKind::Kani => ExecutionStatus::Success,
},
stdout: String::new(),
stderr: String::new(),
exit_code: Some(1),
backend_version: Some("tool 1.0".into()),
smt_output: Some(crate::SmtOutput {
status: Some(ExecutionStatus::Unsat),
model: None,
reason_unknown: None,
}),
lean_output: (plan.kind == crate::CommandKind::Lean).then(|| {
crate::LeanOutput {
diagnostics: vec![crate::LeanDiagnostic {
file: Some("lean/KarpalVerify.lean".into()),
line: Some(9),
column: Some(2),
severity: "error".into(),
message: "unsolved goals in theorem left_distributivity".into(),
theorem_hits: vec!["left_distributivity".into()],
}],
theorem_hits: vec!["left_distributivity".into()],
}
}),
}
}
}
let report = execute_report(&bundle, &artifacts, &TheoremNameRunner);
let left_distributivity = report
.obligations
.iter()
.find(|entry| entry.obligation_name == "left_distributivity")
.expect("left distributivity obligation should be present");
assert_eq!(
left_distributivity.lean_diagnostics,
vec!["unsolved goals in theorem left_distributivity".to_string()]
);
assert_eq!(
report
.lean_module
.as_ref()
.map(|module| module.theorem_failures.clone()),
Some(vec!["KarpalVerify.left_distributivity".to_string()])
);
}
#[test]
fn theorem_mapping_can_fall_back_to_exported_line_spans() {
let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
let bundle = ObligationBundle::semiring(
"sum_semiring",
Origin::new("karpal-core", "Semiring for Sum<i32>"),
&sig,
);
let layout = ArtifactLayout::new("target/karpal-verify-report-test-4");
let artifacts = dry_run_bundle_artifacts(
&bundle,
&layout,
"KarpalVerify",
&SmtConfig::default(),
&LeanConfig::default(),
);
let failure_line = artifacts
.lean_export
.as_ref()
.and_then(|export| export.theorem_for_obligation("left_distributivity"))
.map(|theorem| theorem.declaration_start_line)
.expect("left distributivity theorem span should be present");
struct LocationRunner {
failure_line: usize,
}
impl VerifierRunner for LocationRunner {
fn run(&self, plan: &crate::InvocationPlan) -> ExecutionResult {
ExecutionResult {
plan: plan.clone(),
status: match plan.kind {
crate::CommandKind::Smt => ExecutionStatus::Unsat,
crate::CommandKind::Lean => ExecutionStatus::Failure,
crate::CommandKind::Kani => ExecutionStatus::Success,
},
stdout: String::new(),
stderr: String::new(),
exit_code: Some(1),
backend_version: Some("tool 1.0".into()),
smt_output: Some(crate::SmtOutput {
status: Some(ExecutionStatus::Unsat),
model: None,
reason_unknown: None,
}),
lean_output: (plan.kind == crate::CommandKind::Lean).then(|| {
crate::LeanOutput {
diagnostics: vec![crate::LeanDiagnostic {
file: Some("lean/KarpalVerify.lean".into()),
line: Some(self.failure_line),
column: Some(2),
severity: "error".into(),
message: "type mismatch".into(),
theorem_hits: Vec::new(),
}],
theorem_hits: Vec::new(),
}
}),
}
}
}
let report = execute_report(&bundle, &artifacts, &LocationRunner { failure_line });
let left_distributivity = report
.obligations
.iter()
.find(|entry| entry.obligation_name == "left_distributivity")
.expect("left distributivity obligation should be present");
assert_eq!(
left_distributivity.lean_diagnostics,
vec!["type mismatch".to_string()]
);
assert_eq!(
report
.lean_module
.as_ref()
.map(|module| module.theorem_failures.clone()),
Some(vec!["KarpalVerify.left_distributivity".to_string()])
);
}
}