logicaffeine_verify/
ir.rs

1//! Verification IR (Intermediate Representation)
2//!
3//! A lightweight AST for Z3 verification that decouples from the main Logicaffeine AST.
4//! This avoids circular dependencies: logicaffeine depends on logicaffeine_verify,
5//! so logicaffeine_verify cannot depend on logicaffeine.
6//!
7//! ## Usage
8//!
9//! Build expressions using the [`VerifyExpr`] constructors:
10//!
11//! ```
12//! use logicaffeine_verify::{VerifyExpr, VerifyOp, VerifyType};
13//!
14//! // Build: x > 5 && y < 10
15//! let expr = VerifyExpr::and(
16//!     VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5)),
17//!     VerifyExpr::lt(VerifyExpr::var("y"), VerifyExpr::int(10)),
18//! );
19//! ```
20//!
21//! ## Encoding Strategy
22//!
23//! Complex types (modals, temporals, predicates) become uninterpreted functions.
24//! Z3 reasons about their structure without semantic understanding.
25//!
26//! For example, given `Possible(A) -> Possible(B)` and `Possible(A)`, Z3 deduces `Possible(B)`.
27
28use serde::{Serialize, Deserialize};
29
30/// Type declarations for verification variables.
31///
32/// Each type maps to a Z3 sort:
33///
34/// | VerifyType | Z3 Sort | Usage |
35/// |------------|---------|-------|
36/// | `Int` | `IntSort` | Numeric constraints, bounds checking |
37/// | `Bool` | `BoolSort` | Logical propositions |
38/// | `Object` | Uninterpreted | Entities (people, objects, propositions) |
39#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
40pub enum VerifyType {
41    /// Integer type, maps to Z3 `IntSort`.
42    Int,
43    /// Boolean type, maps to Z3 `BoolSort`.
44    Bool,
45    /// Opaque object type for entities, maps to an uninterpreted sort.
46    Object,
47    /// Fixed-width bitvector, maps to Z3 `BitVecSort(n)`.
48    BitVector(u32),
49    /// Array type (index → element), maps to Z3 `ArraySort`.
50    Array(Box<VerifyType>, Box<VerifyType>),
51    /// Real number type, maps to Z3 `RealSort` (IEEE 1800-2023).
52    Real,
53}
54
55/// Binary operations in the verification IR.
56///
57/// Operations are grouped by category:
58/// - **Arithmetic**: `Add`, `Sub`, `Mul`, `Div` (Int × Int → Int)
59/// - **Comparison**: `Eq`, `Neq`, `Gt`, `Lt`, `Gte`, `Lte` (Int × Int → Bool)
60/// - **Logic**: `And`, `Or`, `Implies` (Bool × Bool → Bool)
61#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
62pub enum VerifyOp {
63    // ---- Arithmetic (Int × Int → Int) ----
64
65    /// Addition.
66    Add,
67    /// Subtraction.
68    Sub,
69    /// Multiplication.
70    Mul,
71    /// Integer division (Euclidean, matching Z3's `div`).
72    Div,
73    /// Floor division (`a // b`) — the quotient rounded toward negative infinity, exactly.
74    /// Encoded as `to_int(to_real(a) / to_real(b))` (Z3's `to_int` is the floor function),
75    /// which is precise across every sign combination — unlike [`VerifyOp::Div`], whose
76    /// Euclidean rounding only coincides with floor when the divisor is positive.
77    FloorDiv,
78
79    // ---- Comparison (Int × Int → Bool) ----
80
81    /// Equality.
82    Eq,
83    /// Inequality.
84    Neq,
85    /// Greater than.
86    Gt,
87    /// Less than.
88    Lt,
89    /// Greater than or equal.
90    Gte,
91    /// Less than or equal.
92    Lte,
93
94    // ---- Logic (Bool × Bool → Bool) ----
95
96    /// Conjunction.
97    And,
98    /// Disjunction.
99    Or,
100    /// Material implication.
101    Implies,
102}
103
104/// Bitvector operations for hardware verification.
105///
106/// These map directly to Z3's bitvector theory operations.
107#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
108pub enum BitVecOp {
109    // ---- Bitwise ----
110    And,
111    Or,
112    Xor,
113    Not,
114
115    // ---- Shift ----
116    Shl,
117    Shr,
118    /// Arithmetic shift right (sign-extending).
119    AShr,
120
121    // ---- Arithmetic ----
122    Add,
123    Sub,
124    Mul,
125    /// Signed division, truncating toward zero (matches Rust `i64` `/`).
126    SDiv,
127    /// Signed remainder, sign following the dividend (matches Rust `i64` `%`).
128    SRem,
129
130    // ---- Comparison ----
131    /// Unsigned less than.
132    ULt,
133    /// Signed less than.
134    SLt,
135    /// Unsigned less than or equal.
136    ULe,
137    /// Signed less than or equal.
138    SLe,
139    /// Bitvector equality.
140    Eq,
141}
142
143/// Expression AST for verification.
144///
145/// This IR is designed to be easily encodable into Z3 ASTs.
146#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
147pub enum VerifyExpr {
148    /// Integer literal
149    Int(i64),
150
151    /// Boolean literal
152    Bool(bool),
153
154    /// Variable reference
155    Var(String),
156
157    /// Binary operation
158    Binary {
159        op: VerifyOp,
160        left: Box<VerifyExpr>,
161        right: Box<VerifyExpr>,
162    },
163
164    /// Logical negation
165    Not(Box<VerifyExpr>),
166
167    /// Universal quantifier: forall x: T. P(x)
168    ForAll {
169        vars: Vec<(String, VerifyType)>,
170        body: Box<VerifyExpr>,
171    },
172
173    /// Existential quantifier: exists x: T. P(x)
174    Exists {
175        vars: Vec<(String, VerifyType)>,
176        body: Box<VerifyExpr>,
177    },
178
179    /// Uninterpreted function application (the "catch-all")
180    ///
181    /// Used for predicates, modals, temporals, etc. that we can't
182    /// directly encode semantically. Z3 treats these as opaque functions
183    /// and reasons about them structurally.
184    ///
185    /// Examples:
186    /// - `Mortal(socrates)` -> `Apply { name: "Mortal", args: [Var("socrates")] }`
187    /// - `Possible(P)` -> `Apply { name: "Possible", args: [P] }`
188    Apply {
189        name: String,
190        args: Vec<VerifyExpr>,
191    },
192
193    /// Uninterpreted INT-valued function application: `Int^n → Int`.
194    ///
195    /// For function symbols in TERM position — `sum(a, b)` (the Link-lattice
196    /// join ⊕), `GovernmentOf(x)`, `has(x, y)` — where [`VerifyExpr::Apply`]
197    /// (which encodes as `Int^n → Bool`) would be ill-sorted.
198    ApplyInt {
199        name: String,
200        args: Vec<VerifyExpr>,
201    },
202
203    // ---- Bitvector operations (hardware verification) ----
204
205    /// Bitvector constant with explicit width.
206    BitVecConst { width: u32, value: u64 },
207
208    /// Bitvector binary operation.
209    BitVecBinary {
210        op: BitVecOp,
211        left: Box<VerifyExpr>,
212        right: Box<VerifyExpr>,
213    },
214
215    /// Bitvector bit extraction: operand\[high:low\].
216    BitVecExtract {
217        high: u32,
218        low: u32,
219        operand: Box<VerifyExpr>,
220    },
221
222    /// Bitvector concatenation.
223    BitVecConcat(Box<VerifyExpr>, Box<VerifyExpr>),
224
225    // ---- Temporal (BMC encoding) ----
226
227    /// Expression evaluated at a specific state (for BMC unrolling).
228    AtState {
229        state: Box<VerifyExpr>,
230        expr: Box<VerifyExpr>,
231    },
232
233    /// State transition relation: from → to.
234    Transition {
235        from: Box<VerifyExpr>,
236        to: Box<VerifyExpr>,
237    },
238
239    // ---- Array theory ----
240
241    /// Array select: array\[index\].
242    Select {
243        array: Box<VerifyExpr>,
244        index: Box<VerifyExpr>,
245    },
246
247    /// Array store: array\[index\] := value.
248    Store {
249        array: Box<VerifyExpr>,
250        index: Box<VerifyExpr>,
251        value: Box<VerifyExpr>,
252    },
253
254    // ---- Biconditional (equivalence checking) ----
255
256    /// Biconditional: left ↔ right. Used for Z3 equivalence queries.
257    Iff(Box<VerifyExpr>, Box<VerifyExpr>),
258}
259
260impl VerifyExpr {
261    /// Create a variable reference.
262    ///
263    /// # Examples
264    ///
265    /// ```
266    /// use logicaffeine_verify::VerifyExpr;
267    ///
268    /// let x = VerifyExpr::var("x");
269    /// let counter = VerifyExpr::var("counter");
270    /// ```
271    pub fn var(name: impl Into<String>) -> Self {
272        VerifyExpr::Var(name.into())
273    }
274
275    /// Create an integer literal.
276    ///
277    /// # Examples
278    ///
279    /// ```
280    /// use logicaffeine_verify::VerifyExpr;
281    ///
282    /// let five = VerifyExpr::int(5);
283    /// let negative = VerifyExpr::int(-42);
284    /// ```
285    pub fn int(n: i64) -> Self {
286        VerifyExpr::Int(n)
287    }
288
289    /// Create a boolean literal.
290    ///
291    /// # Examples
292    ///
293    /// ```
294    /// use logicaffeine_verify::VerifyExpr;
295    ///
296    /// let truth = VerifyExpr::bool(true);
297    /// let falsity = VerifyExpr::bool(false);
298    /// ```
299    pub fn bool(b: bool) -> Self {
300        VerifyExpr::Bool(b)
301    }
302
303    /// Create a binary operation.
304    ///
305    /// For common operations, prefer the convenience methods like [`eq`](Self::eq),
306    /// [`gt`](Self::gt), [`and`](Self::and), etc.
307    ///
308    /// # Examples
309    ///
310    /// ```
311    /// use logicaffeine_verify::{VerifyExpr, VerifyOp};
312    ///
313    /// // x + y
314    /// let sum = VerifyExpr::binary(
315    ///     VerifyOp::Add,
316    ///     VerifyExpr::var("x"),
317    ///     VerifyExpr::var("y"),
318    /// );
319    /// ```
320    pub fn binary(op: VerifyOp, left: VerifyExpr, right: VerifyExpr) -> Self {
321        VerifyExpr::Binary {
322            op,
323            left: Box::new(left),
324            right: Box::new(right),
325        }
326    }
327
328    /// Create a negation.
329    ///
330    /// # Examples
331    ///
332    /// ```
333    /// use logicaffeine_verify::VerifyExpr;
334    ///
335    /// // ¬p
336    /// let not_p = VerifyExpr::not(VerifyExpr::var("p"));
337    ///
338    /// // ¬(x > 5)
339    /// let not_gt = VerifyExpr::not(
340    ///     VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))
341    /// );
342    /// ```
343    pub fn not(expr: VerifyExpr) -> Self {
344        VerifyExpr::Not(Box::new(expr))
345    }
346
347    /// Create an uninterpreted function application.
348    ///
349    /// Use this for predicates, modals, temporals, and other constructs
350    /// that cannot be directly encoded semantically. Z3 treats these as
351    /// opaque functions and reasons about them structurally.
352    ///
353    /// # Examples
354    ///
355    /// ```
356    /// use logicaffeine_verify::VerifyExpr;
357    ///
358    /// // Mortal(socrates)
359    /// let mortal = VerifyExpr::apply("Mortal", vec![VerifyExpr::var("socrates")]);
360    ///
361    /// // Possible(P) for modal logic
362    /// let possible_p = VerifyExpr::apply("Possible", vec![VerifyExpr::var("P")]);
363    ///
364    /// // Before(e1, e2) for temporal relations
365    /// let before = VerifyExpr::apply("Before", vec![
366    ///     VerifyExpr::var("e1"),
367    ///     VerifyExpr::var("e2"),
368    /// ]);
369    /// ```
370    pub fn apply(name: impl Into<String>, args: Vec<VerifyExpr>) -> Self {
371        VerifyExpr::Apply {
372            name: name.into(),
373            args,
374        }
375    }
376
377    /// Create an uninterpreted INT-valued function application (`Int^n → Int`)
378    /// for function symbols in term position, e.g. the lattice join
379    /// `sum(a, b)`.
380    pub fn apply_int(name: impl Into<String>, args: Vec<VerifyExpr>) -> Self {
381        VerifyExpr::ApplyInt {
382            name: name.into(),
383            args,
384        }
385    }
386
387    /// Create a universal quantifier.
388    ///
389    /// # Examples
390    ///
391    /// ```
392    /// use logicaffeine_verify::{VerifyExpr, VerifyType};
393    ///
394    /// // ∀x: Object. Mortal(x) → Human(x)
395    /// let all_mortals_are_human = VerifyExpr::forall(
396    ///     vec![("x".to_string(), VerifyType::Object)],
397    ///     VerifyExpr::implies(
398    ///         VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
399    ///         VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
400    ///     ),
401    /// );
402    /// ```
403    pub fn forall(vars: Vec<(String, VerifyType)>, body: VerifyExpr) -> Self {
404        VerifyExpr::ForAll {
405            vars,
406            body: Box::new(body),
407        }
408    }
409
410    /// Create an existential quantifier.
411    ///
412    /// # Examples
413    ///
414    /// ```
415    /// use logicaffeine_verify::{VerifyExpr, VerifyType};
416    ///
417    /// // ∃x: Object. Mortal(x)
418    /// let something_is_mortal = VerifyExpr::exists(
419    ///     vec![("x".to_string(), VerifyType::Object)],
420    ///     VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
421    /// );
422    /// ```
423    pub fn exists(vars: Vec<(String, VerifyType)>, body: VerifyExpr) -> Self {
424        VerifyExpr::Exists {
425            vars,
426            body: Box::new(body),
427        }
428    }
429
430    // ---- Convenience methods for common operations ----
431
432    /// Equality: `left == right`.
433    ///
434    /// # Examples
435    ///
436    /// ```
437    /// use logicaffeine_verify::VerifyExpr;
438    ///
439    /// let x_equals_10 = VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10));
440    /// ```
441    pub fn eq(left: VerifyExpr, right: VerifyExpr) -> Self {
442        Self::binary(VerifyOp::Eq, left, right)
443    }
444
445    /// Greater than: `left > right`.
446    ///
447    /// # Examples
448    ///
449    /// ```
450    /// use logicaffeine_verify::VerifyExpr;
451    ///
452    /// let x_gt_5 = VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5));
453    /// ```
454    pub fn gt(left: VerifyExpr, right: VerifyExpr) -> Self {
455        Self::binary(VerifyOp::Gt, left, right)
456    }
457
458    /// Less than: `left < right`.
459    ///
460    /// # Examples
461    ///
462    /// ```
463    /// use logicaffeine_verify::VerifyExpr;
464    ///
465    /// let x_lt_100 = VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(100));
466    /// ```
467    pub fn lt(left: VerifyExpr, right: VerifyExpr) -> Self {
468        Self::binary(VerifyOp::Lt, left, right)
469    }
470
471    /// Greater than or equal: `left >= right`.
472    ///
473    /// # Examples
474    ///
475    /// ```
476    /// use logicaffeine_verify::VerifyExpr;
477    ///
478    /// let x_gte_0 = VerifyExpr::gte(VerifyExpr::var("x"), VerifyExpr::int(0));
479    /// ```
480    pub fn gte(left: VerifyExpr, right: VerifyExpr) -> Self {
481        Self::binary(VerifyOp::Gte, left, right)
482    }
483
484    /// Less than or equal: `left <= right`.
485    ///
486    /// # Examples
487    ///
488    /// ```
489    /// use logicaffeine_verify::VerifyExpr;
490    ///
491    /// let x_lte_max = VerifyExpr::lte(VerifyExpr::var("x"), VerifyExpr::var("max"));
492    /// ```
493    pub fn lte(left: VerifyExpr, right: VerifyExpr) -> Self {
494        Self::binary(VerifyOp::Lte, left, right)
495    }
496
497    /// Inequality: `left != right`.
498    ///
499    /// # Examples
500    ///
501    /// ```
502    /// use logicaffeine_verify::VerifyExpr;
503    ///
504    /// let x_neq_0 = VerifyExpr::neq(VerifyExpr::var("x"), VerifyExpr::int(0));
505    /// ```
506    pub fn neq(left: VerifyExpr, right: VerifyExpr) -> Self {
507        Self::binary(VerifyOp::Neq, left, right)
508    }
509
510    /// Conjunction: `left && right`.
511    ///
512    /// # Examples
513    ///
514    /// ```
515    /// use logicaffeine_verify::VerifyExpr;
516    ///
517    /// // x > 0 && x < 100
518    /// let in_range = VerifyExpr::and(
519    ///     VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)),
520    ///     VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(100)),
521    /// );
522    /// ```
523    pub fn and(left: VerifyExpr, right: VerifyExpr) -> Self {
524        Self::binary(VerifyOp::And, left, right)
525    }
526
527    /// Disjunction: `left || right`.
528    ///
529    /// # Examples
530    ///
531    /// ```
532    /// use logicaffeine_verify::VerifyExpr;
533    ///
534    /// // x < 0 || x > 100
535    /// let out_of_range = VerifyExpr::or(
536    ///     VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(0)),
537    ///     VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(100)),
538    /// );
539    /// ```
540    pub fn or(left: VerifyExpr, right: VerifyExpr) -> Self {
541        Self::binary(VerifyOp::Or, left, right)
542    }
543
544    /// Material implication: `left → right`.
545    ///
546    /// # Examples
547    ///
548    /// ```
549    /// use logicaffeine_verify::VerifyExpr;
550    ///
551    /// // Mortal(x) → Human(x)
552    /// let mortals_are_human = VerifyExpr::implies(
553    ///     VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
554    ///     VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
555    /// );
556    /// ```
557    pub fn implies(left: VerifyExpr, right: VerifyExpr) -> Self {
558        Self::binary(VerifyOp::Implies, left, right)
559    }
560
561    // ---- Bitvector convenience constructors ----
562
563    /// Create a bitvector constant.
564    pub fn bv_const(width: u32, value: u64) -> Self {
565        VerifyExpr::BitVecConst { width, value }
566    }
567
568    /// Create a bitvector binary operation.
569    pub fn bv_binary(op: BitVecOp, left: VerifyExpr, right: VerifyExpr) -> Self {
570        VerifyExpr::BitVecBinary {
571            op,
572            left: Box::new(left),
573            right: Box::new(right),
574        }
575    }
576
577    /// Biconditional: `left ↔ right`.
578    pub fn iff(left: VerifyExpr, right: VerifyExpr) -> Self {
579        VerifyExpr::Iff(Box::new(left), Box::new(right))
580    }
581}
582
583#[cfg(test)]
584mod tests {
585    use super::*;
586
587    #[test]
588    fn test_verify_expr_construction() {
589        // Test that we can construct expressions
590        let x = VerifyExpr::var("x");
591        let five = VerifyExpr::int(5);
592        let ten = VerifyExpr::int(10);
593
594        // x > 5
595        let gt = VerifyExpr::gt(x.clone(), five);
596        assert!(matches!(gt, VerifyExpr::Binary { op: VerifyOp::Gt, .. }));
597
598        // x == 10
599        let eq = VerifyExpr::eq(x.clone(), ten);
600        assert!(matches!(eq, VerifyExpr::Binary { op: VerifyOp::Eq, .. }));
601    }
602
603    #[test]
604    fn test_uninterpreted_function() {
605        // Mortal(x)
606        let mortal_x = VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]);
607        assert!(matches!(mortal_x, VerifyExpr::Apply { name, args } if name == "Mortal" && args.len() == 1));
608    }
609
610    #[test]
611    fn test_implication() {
612        // Mortal(x) -> Human(x)
613        let mortal = VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]);
614        let human = VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]);
615        let impl_expr = VerifyExpr::implies(mortal, human);
616
617        assert!(matches!(impl_expr, VerifyExpr::Binary { op: VerifyOp::Implies, .. }));
618    }
619
620    #[test]
621    fn test_quantifier() {
622        // forall x: Object. Mortal(x) -> Human(x)
623        let body = VerifyExpr::implies(
624            VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
625            VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
626        );
627        let forall = VerifyExpr::forall(
628            vec![("x".to_string(), VerifyType::Object)],
629            body,
630        );
631
632        assert!(matches!(forall, VerifyExpr::ForAll { vars, .. } if vars.len() == 1));
633    }
634}
logicaffeine_verify/ir.rs

logicaffeine_verify/
ir.rs
