karpal-verify 0.5.0

External prover bridge and trust model for the Industrial Algebra ecosystem
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

#[cfg(not(feature = "std"))]
use alloc::{string::String, vec::Vec};
#[cfg(feature = "std")]
use std::{string::String, vec::Vec};

use crate::{
    LeanExport, LeanPrelude, Obligation, ObligationBundle, export_lean_module,
    export_module_with_prelude as export_lean_module_with_prelude, export_smt_obligation,
};

/// Export an entire bundle as one SMT-LIB2 script per obligation.
pub fn export_smt_bundle(bundle: &ObligationBundle) -> Vec<(String, String)> {
    bundle
        .obligations()
        .iter()
        .map(|obligation| (obligation.name.clone(), export_smt_obligation(obligation)))
        .collect()
}

/// Export a whole bundle as a single Lean 4 module.
pub fn export_lean_bundle(module_name: &str, bundle: &ObligationBundle) -> String {
    export_lean_module(module_name, bundle.obligations())
}

/// Export a whole bundle as a single Lean 4 module with explicit prelude metadata.
pub fn export_lean_bundle_with_prelude(
    module_name: &str,
    bundle: &ObligationBundle,
    prelude: LeanPrelude,
) -> String {
    export_lean_module_with_prelude(module_name, bundle.obligations(), prelude)
}

/// Export a whole bundle as structured Lean module metadata plus source.
pub fn export_lean_bundle_structured(module_name: &str, bundle: &ObligationBundle) -> LeanExport {
    crate::lean::export(module_name, bundle.obligations())
}

/// Export a whole bundle as structured Lean module metadata plus source with explicit prelude metadata.
pub fn export_lean_bundle_structured_with_prelude(
    module_name: &str,
    bundle: &ObligationBundle,
    prelude: LeanPrelude,
) -> LeanExport {
    crate::lean::export_with_prelude(module_name, bundle.obligations(), prelude)
}

/// Export a list of obligations as one SMT-LIB2 script per obligation.
pub fn export_smt_batch(obligations: &[Obligation]) -> Vec<(String, String)> {
    obligations
        .iter()
        .map(|obligation| (obligation.name.clone(), export_smt_obligation(obligation)))
        .collect()
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::{AlgebraicSignature, Origin, Sort};

    #[test]
    fn smt_bundle_export_returns_one_script_per_obligation() {
        let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
        let bundle = ObligationBundle::monoid("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
        let scripts = export_smt_bundle(&bundle);
        assert_eq!(scripts.len(), 3);
        assert!(scripts[0].1.contains("(check-sat)"));
    }

    #[test]
    fn lean_bundle_export_contains_multiple_theorems() {
        let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
        let bundle = ObligationBundle::group("sum", Origin::new("karpal-algebra", "i32"), &sig);
        let module = export_lean_bundle("KarpalVerify", &bundle);
        assert!(module.contains("theorem associativity"));
        assert!(module.contains("theorem left_inverse"));
        assert!(module.contains("theorem right_inverse"));

        let structured = export_lean_bundle_structured("KarpalVerify", &bundle);
        assert_eq!(structured.theorems.len(), 5);
        assert_eq!(
            structured
                .theorem_for_obligation("left_inverse")
                .map(|t| t.witness_ref("KarpalVerify")),
            Some("KarpalVerify.left_inverse".into())
        );
    }

    #[test]
    fn lean_bundle_export_with_prelude_renders_imports() {
        let sig = AlgebraicSignature::semigroup(Sort::Int, "combine");
        let bundle =
            ObligationBundle::semigroup("sum", Origin::new("karpal-core", "Sum<i32>"), &sig);
        let module = export_lean_bundle_with_prelude(
            "KarpalVerify",
            &bundle,
            LeanPrelude::new().with_import("Mathlib"),
        );

        assert!(module.starts_with("import Mathlib\n\nnamespace KarpalVerify"));
    }
}