flux_verify_api/compiler/
mod.rs

1pub mod generic;
2pub mod parser;
3pub mod sonar;
4pub mod thermal;
5
6use crate::engine::vm::Bytecode;
7
8/// A parsed constraint problem ready for FLUX compilation.
9#[derive(Debug, Clone)]
10pub struct ConstraintProblem {
11    pub domain: String,
12    pub variables: Vec<Variable>,
13    pub constraints: Vec<Constraint>,
14    pub assertion: Assertion,
15}
16
17#[derive(Debug, Clone)]
18pub struct Variable {
19    pub name: String,
20    pub value: f64,
21    pub desc: String,
22}
23
24#[derive(Debug, Clone)]
25pub enum Constraint {
26    SoundVelocity { depth_m: f64, temp_c: f64, salinity_ppt: f64 },
27    Absorption { frequency_khz: f64, depth_m: f64, temp_c: f64, salinity_ppt: f64 },
28    TransmissionLoss { range_m: f64, frequency_khz: f64, depth_m: f64, temp_c: f64, salinity_ppt: f64 },
29    ThermalBound { temp_c: f64, min_safe: f64, max_safe: f64 },
30    GenericCompare { left: f64, operator: String, right: f64, desc: String },
31    GenericBound { value: f64, min: f64, max: f64, desc: String },
32    GenericRangeCheck { value: f64, min: f64, max: f64, desc: String },
33}
34
35#[derive(Debug, Clone)]
36pub struct Assertion {
37    pub assertion_type: String, // "gt" | "lt" | "eq" | "in_range"
38    pub expected: f64,
39    pub actual_expr: String, // description of what's being checked
40}
41
42/// Parse a natural language claim into a constraint problem.
43pub fn parse_claim(claim: &str, domain: &str) -> Result<ConstraintProblem, String> {
44    match domain {
45        "sonar" => sonar::parse(claim),
46        "thermal" => thermal::parse(claim),
47        "generic" => generic::parse(claim),
48        _ => Err(format!("Unknown domain: '{}'. Use sonar, thermal, or generic.", domain)),
49    }
50}
51
52/// Compile a constraint problem into FLUX bytecodes.
53pub fn compile(problem: &ConstraintProblem) -> Vec<Bytecode> {
54    let mut bytecodes = Vec::new();
55
56    // Load all variables
57    for var in &problem.variables {
58        bytecodes.push(Bytecode::Load {
59            name: var.name.clone(),
60            value: var.value,
61            desc: var.desc.clone(),
62        });
63    }
64
65    // Evaluate constraints
66    for constraint in &problem.constraints {
67        match constraint {
68            Constraint::SoundVelocity { depth_m, temp_c, salinity_ppt } => {
69                bytecodes.push(Bytecode::SonarSvp {
70                    depth_m: *depth_m,
71                    temp_c: *temp_c,
72                    salinity_ppt: *salinity_ppt,
73                });
74            }
75            Constraint::Absorption { frequency_khz, depth_m, temp_c, salinity_ppt } => {
76                bytecodes.push(Bytecode::SonarAbsorption {
77                    frequency_khz: *frequency_khz,
78                    depth_m: *depth_m,
79                    temp_c: *temp_c,
80                    salinity_ppt: *salinity_ppt,
81                });
82            }
83            Constraint::TransmissionLoss { range_m, frequency_khz, depth_m, temp_c, salinity_ppt } => {
84                bytecodes.push(Bytecode::SonarTl {
85                    range_m: *range_m,
86                    frequency_khz: *frequency_khz,
87                    depth_m: *depth_m,
88                    temp_c: *temp_c,
89                    salinity_ppt: *salinity_ppt,
90                });
91            }
92            Constraint::ThermalBound { temp_c, min_safe, max_safe } => {
93                bytecodes.push(Bytecode::ThermalBound {
94                    temp_c: *temp_c,
95                    min_safe: *min_safe,
96                    max_safe: *max_safe,
97                });
98            }
99            Constraint::GenericCompare { left, operator, right, desc } => {
100                bytecodes.push(Bytecode::GenericCompare {
101                    left: *left,
102                    operator: operator.clone(),
103                    right: *right,
104                    desc: desc.clone(),
105                });
106            }
107            Constraint::GenericBound { value, min, max, desc } => {
108                bytecodes.push(Bytecode::GenericBound {
109                    value: *value,
110                    min: *min,
111                    max: *max,
112                    desc: desc.clone(),
113                });
114            }
115            Constraint::GenericRangeCheck { value, min, max, desc } => {
116                bytecodes.push(Bytecode::GenericRangeCheck {
117                    value: *value,
118                    min: *min,
119                    max: *max,
120                    desc: desc.clone(),
121                });
122            }
123        }
124    }
125
126    // Add assertion
127    bytecodes.push(Bytecode::Assert {
128        assertion_type: problem.assertion.assertion_type.clone(),
129        expected: problem.assertion.expected,
130        desc: problem.assertion.actual_expr.clone(),
131    });
132
133    bytecodes
134}
flux_verify_api/compiler/mod.rs

flux_verify_api/compiler/
mod.rs
