clifford_codegen/symbolic/
verify.rs

1//! Constraint verification.
2//!
3//! This module verifies that product outputs satisfy algebraic constraints
4//! when inputs satisfy their constraints.
5
6use symbolica::atom::{Atom, AtomCore};
7
8use super::ConstraintExpr;
9
10/// Result of constraint verification.
11#[derive(Debug, Clone)]
12pub enum VerificationResult {
13    /// Constraint is always satisfied when inputs satisfy their constraints.
14    Always,
15    /// Verification was inconclusive (expression too complex).
16    Inconclusive(String),
17}
18
19/// Verifies that outputs satisfy constraints given input constraints.
20#[derive(Debug, Default)]
21pub struct ConstraintVerifier;
22
23impl ConstraintVerifier {
24    /// Creates a new constraint verifier.
25    pub fn new() -> Self {
26        Self
27    }
28
29    /// Checks if a constraint expression is trivially satisfied (both sides equal).
30    ///
31    /// This is a simpler verification that doesn't require substitution - it just
32    /// checks if lhs == rhs after expansion.
33    pub fn check_trivial(&self, constraint: &ConstraintExpr) -> VerificationResult {
34        let zero_form = constraint.as_zero_form();
35        self.check_is_zero(&zero_form)
36    }
37
38    /// Checks if an expression is zero.
39    fn check_is_zero(&self, expr: &Atom) -> VerificationResult {
40        // Create zero atom using Atom::num
41        let zero = Atom::num(0);
42
43        // Check if the expression is literally zero
44        if expr == &zero {
45            return VerificationResult::Always;
46        }
47
48        // Try expanding and simplifying
49        let expanded = expr.expand();
50        if expanded == zero {
51            return VerificationResult::Always;
52        }
53
54        // Check if it's a simple numeric value by string comparison
55        let expr_str = format!("{}", expanded);
56        if expr_str == "0" {
57            return VerificationResult::Always;
58        }
59
60        // For complex expressions, we may need more sophisticated analysis
61        // For now, return inconclusive
62        VerificationResult::Inconclusive(format!(
63            "Could not verify: expression simplifies to {}",
64            expanded
65        ))
66    }
67}
68
69#[cfg(test)]
70mod tests {
71    use super::*;
72    use std::sync::Mutex;
73
74    // Symbolica uses global state that conflicts when tests run in parallel.
75    // Tests prefixed with `symbolica_` are configured to run serially via nextest.
76    // The mutex provides a fallback for `cargo test` users.
77    static SYMBOLICA_LOCK: Mutex<()> = Mutex::new(());
78
79    #[test]
80    fn symbolica_verify_numeric_constraint() {
81        let _guard = SYMBOLICA_LOCK.lock().unwrap();
82        // Test with a numeric constraint directly constructed
83        let verifier = ConstraintVerifier::new();
84
85        // Create atoms for 5 - 5 = 0
86        let lhs = Atom::num(5);
87        let rhs = Atom::num(5);
88        let constraint = super::super::ConstraintExpr {
89            lhs,
90            rhs,
91            original: "5 = 5".to_string(),
92        };
93
94        let result = verifier.check_trivial(&constraint);
95        assert!(matches!(result, VerificationResult::Always));
96    }
97
98    #[test]
99    fn symbolica_verify_zero_atom() {
100        let _guard = SYMBOLICA_LOCK.lock().unwrap();
101        let verifier = ConstraintVerifier::new();
102
103        // Create atoms for 0 = 0
104        let lhs = Atom::num(0);
105        let rhs = Atom::num(0);
106        let constraint = super::super::ConstraintExpr {
107            lhs,
108            rhs,
109            original: "0 = 0".to_string(),
110        };
111
112        let result = verifier.check_trivial(&constraint);
113        assert!(matches!(result, VerificationResult::Always));
114    }
115}
clifford_codegen/symbolic/verify.rs

clifford_codegen/symbolic/
verify.rs
