flux-verify-api 0.1.1

Natural Language Verification API — prove or disprove claims with mathematical traces
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

use super::{parser, ConstraintProblem};

/// Generic constraint parser.
/// Handles comparison operators, bounds, and simple numeric constraints.
pub fn parse(claim: &str) -> Result<ConstraintProblem, String> {
    let lower = claim.to_lowercase();
    let original = claim.to_string();

    // Try to parse as a comparison: "X is greater than Y", "X > Y", "X is at least Y"
    if let Some((left, op, right, _desc)) = parser::extract_comparison(&lower) {
        return Ok(ConstraintProblem {
            domain: "generic".into(),
            variables: vec![
                super::Variable { name: "left".into(), value: left, desc: "left operand".into() },
                super::Variable { name: "right".into(), value: right, desc: "right operand".into() },
            ],
            constraints: vec![
                super::Constraint::GenericCompare {
                    left, operator: op.clone(), right, desc: original.clone(),
                },
            ],
            assertion: super::Assertion {
                assertion_type: op,
                expected: right,
                actual_expr: original,
            },
        });
    }

    // Try to parse as a range check: "X is between Y and Z", "X is within [Y, Z]"
    if let Some((value, min, max, _desc)) = parser::extract_range_check(&lower) {
        return Ok(ConstraintProblem {
            domain: "generic".into(),
            variables: vec![
                super::Variable { name: "value".into(), value, desc: "value".into() },
                super::Variable { name: "min".into(), value: min, desc: "minimum bound".into() },
                super::Variable { name: "max".into(), value: max, desc: "maximum bound".into() },
            ],
            constraints: vec![
                super::Constraint::GenericRangeCheck { value, min, max, desc: original.clone() },
            ],
            assertion: super::Assertion {
                assertion_type: "in_range".into(),
                expected: 0.0,
                actual_expr: original,
            },
        });
    }

    // Try to parse as a simple bound: "X is within Y of Z"
    if let Some((value, min, max, _desc)) = parser::extract_bound(&lower) {
        return Ok(ConstraintProblem {
            domain: "generic".into(),
            variables: vec![
                super::Variable { name: "value".into(), value, desc: "value".into() },
                super::Variable { name: "min".into(), value: min, desc: "minimum".into() },
                super::Variable { name: "max".into(), value: max, desc: "maximum".into() },
            ],
            constraints: vec![
                super::Constraint::GenericBound { value, min, max, desc: original.clone() },
            ],
            assertion: super::Assertion {
                assertion_type: "in_range".into(),
                expected: 0.0,
                actual_expr: original,
            },
        });
    }

    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())
}