oxiz_proof/
lfsc.rs

1//! LFSC proof format (Logical Framework with Side Conditions).
2//!
3//! LFSC is a typed first-order language with side conditions, used for
4//! certified verification of SMT proofs. It was developed for use with
5//! CVC4/CVC5 and is checkable by the LFSC checker.
6//!
7//! ## Structure
8//!
9//! LFSC proofs consist of:
10//! - **Type declarations**: Define sorts and kinds
11//! - **Term declarations**: Define functions and constants
12//! - **Side conditions**: Computational side conditions for proof rules
13//! - **Proof terms**: The actual proof derivation
14
15use std::fmt;
16use std::io::{self, Write};
17
18/// An LFSC sort/type
19#[derive(Debug, Clone, PartialEq, Eq)]
20pub enum LfscSort {
21    /// Kind (type of types)
22    Kind,
23    /// Type (type of proofs)
24    Type,
25    /// Boolean sort
26    Bool,
27    /// Integer sort
28    Int,
29    /// Real sort
30    Real,
31    /// BitVector sort with width
32    BitVec(u32),
33    /// Arrow type (function type)
34    Arrow(Box<LfscSort>, Box<LfscSort>),
35    /// Named sort
36    Named(String),
37    /// Application of type constructor
38    App(String, Vec<LfscSort>),
39}
40
41impl fmt::Display for LfscSort {
42    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
43        match self {
44            Self::Kind => write!(f, "kind"),
45            Self::Type => write!(f, "type"),
46            Self::Bool => write!(f, "bool"),
47            Self::Int => write!(f, "mpz"),
48            Self::Real => write!(f, "mpq"),
49            Self::BitVec(w) => write!(f, "(bitvec {})", w),
50            Self::Arrow(a, b) => write!(f, "(! _ {} {})", a, b),
51            Self::Named(n) => write!(f, "{}", n),
52            Self::App(n, args) => {
53                write!(f, "({}", n)?;
54                for arg in args {
55                    write!(f, " {}", arg)?;
56                }
57                write!(f, ")")
58            }
59        }
60    }
61}
62
63/// An LFSC term
64#[derive(Debug, Clone)]
65pub enum LfscTerm {
66    /// Variable reference
67    Var(String),
68    /// Integer literal
69    IntLit(i64),
70    /// Rational literal (numerator, denominator)
71    RatLit(i64, i64),
72    /// Boolean true
73    True,
74    /// Boolean false
75    False,
76    /// Application
77    App(String, Vec<LfscTerm>),
78    /// Lambda abstraction
79    Lambda(String, Box<LfscSort>, Box<LfscTerm>),
80    /// Pi type (dependent function type)
81    Pi(String, Box<LfscSort>, Box<LfscTerm>),
82    /// Side condition application
83    SideCondition(String, Vec<LfscTerm>),
84    /// Proof hold (assertion)
85    Hold(Box<LfscTerm>),
86    /// Type annotation
87    Annotate(Box<LfscTerm>, Box<LfscSort>),
88}
89
90impl fmt::Display for LfscTerm {
91    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
92        match self {
93            Self::Var(v) => write!(f, "{}", v),
94            Self::IntLit(n) => write!(f, "{}", n),
95            Self::RatLit(n, d) => write!(f, "{}/{}", n, d),
96            Self::True => write!(f, "tt"),
97            Self::False => write!(f, "ff"),
98            Self::App(func, args) => {
99                write!(f, "({}", func)?;
100                for arg in args {
101                    write!(f, " {}", arg)?;
102                }
103                write!(f, ")")
104            }
105            Self::Lambda(var, sort, body) => {
106                write!(f, "(\\ {} {} {})", var, sort, body)
107            }
108            Self::Pi(var, sort, body) => {
109                write!(f, "(! {} {} {})", var, sort, body)
110            }
111            Self::SideCondition(name, args) => {
112                write!(f, "(# {} (", name)?;
113                for (i, arg) in args.iter().enumerate() {
114                    if i > 0 {
115                        write!(f, " ")?;
116                    }
117                    write!(f, "{}", arg)?;
118                }
119                write!(f, "))")
120            }
121            Self::Hold(t) => write!(f, "(holds {})", t),
122            Self::Annotate(t, s) => write!(f, "(: {} {})", t, s),
123        }
124    }
125}
126
127/// An LFSC declaration
128#[derive(Debug, Clone)]
129pub enum LfscDecl {
130    /// Declare a new sort
131    DeclareSort { name: String, arity: u32 },
132    /// Declare a new constant/function
133    DeclareConst { name: String, sort: LfscSort },
134    /// Define a term
135    Define {
136        name: String,
137        sort: LfscSort,
138        value: LfscTerm,
139    },
140    /// Declare a proof rule
141    DeclareRule {
142        name: String,
143        params: Vec<(String, LfscSort)>,
144        conclusion: LfscTerm,
145    },
146    /// Side condition program
147    SideCondition {
148        name: String,
149        params: Vec<(String, LfscSort)>,
150        return_sort: LfscSort,
151        body: String, // LFSC program text
152    },
153    /// Proof step (check)
154    Check(LfscTerm),
155}
156
157impl fmt::Display for LfscDecl {
158    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
159        match self {
160            Self::DeclareSort { name, arity } => {
161                write!(f, "(declare {} ", name)?;
162                for _ in 0..*arity {
163                    write!(f, "(! _ type ")?;
164                }
165                write!(f, "type")?;
166                for _ in 0..*arity {
167                    write!(f, ")")?;
168                }
169                write!(f, ")")
170            }
171            Self::DeclareConst { name, sort } => {
172                write!(f, "(declare {} {})", name, sort)
173            }
174            Self::Define { name, sort, value } => {
175                write!(f, "(define {} (: {} {}))", name, value, sort)
176            }
177            Self::DeclareRule {
178                name,
179                params,
180                conclusion,
181            } => {
182                write!(f, "(declare {} ", name)?;
183                for (pname, psort) in params {
184                    write!(f, "(! {} {} ", pname, psort)?;
185                }
186                write!(f, "{}", conclusion)?;
187                for _ in params {
188                    write!(f, ")")?;
189                }
190                write!(f, ")")
191            }
192            Self::SideCondition {
193                name,
194                params,
195                return_sort,
196                body,
197            } => {
198                write!(f, "(program {} (", name)?;
199                for (i, (pname, psort)) in params.iter().enumerate() {
200                    if i > 0 {
201                        write!(f, " ")?;
202                    }
203                    write!(f, "({} {})", pname, psort)?;
204                }
205                write!(f, ") {} {})", return_sort, body)
206            }
207            Self::Check(term) => {
208                write!(f, "(check {})", term)
209            }
210        }
211    }
212}
213
214/// An LFSC proof
215#[derive(Debug, Default)]
216pub struct LfscProof {
217    /// Declarations and proof steps
218    decls: Vec<LfscDecl>,
219}
220
221impl LfscProof {
222    /// Create a new empty LFSC proof
223    #[must_use]
224    pub fn new() -> Self {
225        Self { decls: Vec::new() }
226    }
227
228    /// Add a sort declaration
229    pub fn declare_sort(&mut self, name: impl Into<String>, arity: u32) {
230        self.decls.push(LfscDecl::DeclareSort {
231            name: name.into(),
232            arity,
233        });
234    }
235
236    /// Add a constant declaration
237    pub fn declare_const(&mut self, name: impl Into<String>, sort: LfscSort) {
238        self.decls.push(LfscDecl::DeclareConst {
239            name: name.into(),
240            sort,
241        });
242    }
243
244    /// Add a definition
245    pub fn define(&mut self, name: impl Into<String>, sort: LfscSort, value: LfscTerm) {
246        self.decls.push(LfscDecl::Define {
247            name: name.into(),
248            sort,
249            value,
250        });
251    }
252
253    /// Add a proof rule declaration
254    pub fn declare_rule(
255        &mut self,
256        name: impl Into<String>,
257        params: Vec<(String, LfscSort)>,
258        conclusion: LfscTerm,
259    ) {
260        self.decls.push(LfscDecl::DeclareRule {
261            name: name.into(),
262            params,
263            conclusion,
264        });
265    }
266
267    /// Add a side condition program
268    pub fn side_condition(
269        &mut self,
270        name: impl Into<String>,
271        params: Vec<(String, LfscSort)>,
272        return_sort: LfscSort,
273        body: impl Into<String>,
274    ) {
275        self.decls.push(LfscDecl::SideCondition {
276            name: name.into(),
277            params,
278            return_sort,
279            body: body.into(),
280        });
281    }
282
283    /// Add a proof check
284    pub fn check(&mut self, term: LfscTerm) {
285        self.decls.push(LfscDecl::Check(term));
286    }
287
288    /// Get the number of declarations
289    #[must_use]
290    pub fn len(&self) -> usize {
291        self.decls.len()
292    }
293
294    /// Check if the proof is empty
295    #[must_use]
296    pub fn is_empty(&self) -> bool {
297        self.decls.is_empty()
298    }
299
300    /// Get the declarations
301    #[must_use]
302    pub fn decls(&self) -> &[LfscDecl] {
303        &self.decls
304    }
305
306    /// Clear all declarations
307    pub fn clear(&mut self) {
308        self.decls.clear();
309    }
310
311    /// Write the proof in LFSC format
312    pub fn write<W: Write>(&self, mut writer: W) -> io::Result<()> {
313        writeln!(writer, "; LFSC proof generated by OxiZ")?;
314        writeln!(writer)?;
315
316        for decl in &self.decls {
317            writeln!(writer, "{}", decl)?;
318        }
319
320        Ok(())
321    }
322
323    /// Convert to string
324    #[must_use]
325    #[allow(clippy::inherent_to_string)]
326    pub fn to_string(&self) -> String {
327        let mut buf = Vec::new();
328        self.write(&mut buf)
329            .expect("writing to Vec should not fail");
330        String::from_utf8(buf).expect("LFSC output is UTF-8")
331    }
332}
333
334/// Standard LFSC signatures for common theories
335pub mod signatures {
336    use super::*;
337
338    /// Create declarations for the boolean theory
339    pub fn boolean_theory() -> Vec<LfscDecl> {
340        vec![
341            LfscDecl::DeclareSort {
342                name: "formula".to_string(),
343                arity: 0,
344            },
345            LfscDecl::DeclareConst {
346                name: "true".to_string(),
347                sort: LfscSort::Named("formula".to_string()),
348            },
349            LfscDecl::DeclareConst {
350                name: "false".to_string(),
351                sort: LfscSort::Named("formula".to_string()),
352            },
353            LfscDecl::DeclareConst {
354                name: "not".to_string(),
355                sort: LfscSort::Arrow(
356                    Box::new(LfscSort::Named("formula".to_string())),
357                    Box::new(LfscSort::Named("formula".to_string())),
358                ),
359            },
360            LfscDecl::DeclareConst {
361                name: "and".to_string(),
362                sort: LfscSort::Arrow(
363                    Box::new(LfscSort::Named("formula".to_string())),
364                    Box::new(LfscSort::Arrow(
365                        Box::new(LfscSort::Named("formula".to_string())),
366                        Box::new(LfscSort::Named("formula".to_string())),
367                    )),
368                ),
369            },
370            LfscDecl::DeclareConst {
371                name: "or".to_string(),
372                sort: LfscSort::Arrow(
373                    Box::new(LfscSort::Named("formula".to_string())),
374                    Box::new(LfscSort::Arrow(
375                        Box::new(LfscSort::Named("formula".to_string())),
376                        Box::new(LfscSort::Named("formula".to_string())),
377                    )),
378                ),
379            },
380            LfscDecl::DeclareConst {
381                name: "impl".to_string(),
382                sort: LfscSort::Arrow(
383                    Box::new(LfscSort::Named("formula".to_string())),
384                    Box::new(LfscSort::Arrow(
385                        Box::new(LfscSort::Named("formula".to_string())),
386                        Box::new(LfscSort::Named("formula".to_string())),
387                    )),
388                ),
389            },
390        ]
391    }
392
393    /// Create declarations for holds (proof type)
394    pub fn holds_theory() -> Vec<LfscDecl> {
395        vec![LfscDecl::DeclareConst {
396            name: "holds".to_string(),
397            sort: LfscSort::Arrow(
398                Box::new(LfscSort::Named("formula".to_string())),
399                Box::new(LfscSort::Type),
400            ),
401        }]
402    }
403}
404
405/// Trait for solvers that can produce LFSC proofs
406pub trait LfscProofProducer {
407    /// Enable LFSC proof production
408    fn enable_lfsc_proof(&mut self);
409
410    /// Disable LFSC proof production
411    fn disable_lfsc_proof(&mut self);
412
413    /// Get the LFSC proof (if available)
414    fn get_lfsc_proof(&self) -> Option<&LfscProof>;
415
416    /// Take the LFSC proof, leaving None
417    fn take_lfsc_proof(&mut self) -> Option<LfscProof>;
418}
419
420#[cfg(test)]
421mod tests {
422    use super::*;
423
424    #[test]
425    fn test_lfsc_sort_display() {
426        assert_eq!(format!("{}", LfscSort::Bool), "bool");
427        assert_eq!(format!("{}", LfscSort::Int), "mpz");
428        assert_eq!(format!("{}", LfscSort::BitVec(32)), "(bitvec 32)");
429
430        let arrow = LfscSort::Arrow(Box::new(LfscSort::Int), Box::new(LfscSort::Bool));
431        assert_eq!(format!("{}", arrow), "(! _ mpz bool)");
432    }
433
434    #[test]
435    fn test_lfsc_term_display() {
436        assert_eq!(format!("{}", LfscTerm::Var("x".to_string())), "x");
437        assert_eq!(format!("{}", LfscTerm::IntLit(42)), "42");
438        assert_eq!(format!("{}", LfscTerm::True), "tt");
439        assert_eq!(format!("{}", LfscTerm::False), "ff");
440
441        let app = LfscTerm::App(
442            "add".to_string(),
443            vec![LfscTerm::IntLit(1), LfscTerm::IntLit(2)],
444        );
445        assert_eq!(format!("{}", app), "(add 1 2)");
446    }
447
448    #[test]
449    fn test_lfsc_declare_sort() {
450        let mut proof = LfscProof::new();
451        proof.declare_sort("mySort", 0);
452        proof.declare_sort("myParam", 1);
453
454        let output = proof.to_string();
455        assert!(output.contains("(declare mySort type)"));
456        assert!(output.contains("(declare myParam (! _ type type))"));
457    }
458
459    #[test]
460    fn test_lfsc_declare_const() {
461        let mut proof = LfscProof::new();
462        proof.declare_const("x", LfscSort::Int);
463
464        let output = proof.to_string();
465        assert!(output.contains("(declare x mpz)"));
466    }
467
468    #[test]
469    fn test_lfsc_check() {
470        let mut proof = LfscProof::new();
471        proof.check(LfscTerm::Hold(Box::new(LfscTerm::True)));
472
473        let output = proof.to_string();
474        assert!(output.contains("(check (holds tt))"));
475    }
476
477    #[test]
478    fn test_lfsc_boolean_theory() {
479        let decls = signatures::boolean_theory();
480        assert!(!decls.is_empty());
481
482        // Check that we have the expected declarations
483        let names: Vec<_> = decls
484            .iter()
485            .filter_map(|d| match d {
486                LfscDecl::DeclareSort { name, .. } => Some(name.as_str()),
487                LfscDecl::DeclareConst { name, .. } => Some(name.as_str()),
488                _ => None,
489            })
490            .collect();
491
492        assert!(names.contains(&"formula"));
493        assert!(names.contains(&"true"));
494        assert!(names.contains(&"false"));
495        assert!(names.contains(&"not"));
496        assert!(names.contains(&"and"));
497        assert!(names.contains(&"or"));
498    }
499
500    #[test]
501    fn test_lfsc_proof_clear() {
502        let mut proof = LfscProof::new();
503        proof.declare_sort("test", 0);
504        assert!(!proof.is_empty());
505
506        proof.clear();
507        assert!(proof.is_empty());
508    }
509
510    #[test]
511    fn test_lfsc_lambda() {
512        let lambda = LfscTerm::Lambda(
513            "x".to_string(),
514            Box::new(LfscSort::Int),
515            Box::new(LfscTerm::Var("x".to_string())),
516        );
517
518        assert_eq!(format!("{}", lambda), "(\\ x mpz x)");
519    }
520}
oxiz_proof/lfsc.rs

oxiz_proof/
lfsc.rs
