flux_verify_api/compiler/
generic.rs

1use super::{parser, ConstraintProblem};
2
3/// Generic constraint parser.
4/// Handles comparison operators, bounds, and simple numeric constraints.
5pub fn parse(claim: &str) -> Result<ConstraintProblem, String> {
6    let lower = claim.to_lowercase();
7    let original = claim.to_string();
8
9    // Try to parse as a comparison: "X is greater than Y", "X > Y", "X is at least Y"
10    if let Some((left, op, right, _desc)) = parser::extract_comparison(&lower) {
11        return Ok(ConstraintProblem {
12            domain: "generic".into(),
13            variables: vec![
14                super::Variable { name: "left".into(), value: left, desc: "left operand".into() },
15                super::Variable { name: "right".into(), value: right, desc: "right operand".into() },
16            ],
17            constraints: vec![
18                super::Constraint::GenericCompare {
19                    left, operator: op.clone(), right, desc: original.clone(),
20                },
21            ],
22            assertion: super::Assertion {
23                assertion_type: op,
24                expected: right,
25                actual_expr: original,
26            },
27        });
28    }
29
30    // Try to parse as a range check: "X is between Y and Z", "X is within [Y, Z]"
31    if let Some((value, min, max, _desc)) = parser::extract_range_check(&lower) {
32        return Ok(ConstraintProblem {
33            domain: "generic".into(),
34            variables: vec![
35                super::Variable { name: "value".into(), value, desc: "value".into() },
36                super::Variable { name: "min".into(), value: min, desc: "minimum bound".into() },
37                super::Variable { name: "max".into(), value: max, desc: "maximum bound".into() },
38            ],
39            constraints: vec![
40                super::Constraint::GenericRangeCheck { value, min, max, desc: original.clone() },
41            ],
42            assertion: super::Assertion {
43                assertion_type: "in_range".into(),
44                expected: 0.0,
45                actual_expr: original,
46            },
47        });
48    }
49
50    // Try to parse as a simple bound: "X is within Y of Z"
51    if let Some((value, min, max, _desc)) = parser::extract_bound(&lower) {
52        return Ok(ConstraintProblem {
53            domain: "generic".into(),
54            variables: vec![
55                super::Variable { name: "value".into(), value, desc: "value".into() },
56                super::Variable { name: "min".into(), value: min, desc: "minimum".into() },
57                super::Variable { name: "max".into(), value: max, desc: "maximum".into() },
58            ],
59            constraints: vec![
60                super::Constraint::GenericBound { value, min, max, desc: original.clone() },
61            ],
62            assertion: super::Assertion {
63                assertion_type: "in_range".into(),
64                expected: 0.0,
65                actual_expr: original,
66            },
67        });
68    }
69
70    Err("Could not parse claim as a generic constraint. Try: 'X is greater than Y', 'X is between Y and Z', or 'X > Y'".into())
71}
flux_verify_api/compiler/generic.rs

flux_verify_api/compiler/
generic.rs
