spec_checker/
ast.rs

1//! Spec AST.
2
3use serde::{Deserialize, Serialize};
4
5#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
6pub struct Spec {
7    /// Spec name (typically the target function's name).
8    pub name: String,
9    pub quantifiers: Vec<Quantifier>,
10    /// The boolean property. Free variables refer to quantifiers.
11    pub body: SpecExpr,
12}
13
14#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
15pub struct Quantifier {
16    pub name: String,
17    pub ty: SpecType,
18    /// Optional `where` predicate restricting the quantifier domain.
19    /// Variables in scope are previously-declared quantifiers and `name` itself.
20    #[serde(default, skip_serializing_if = "Option::is_none")]
21    pub constraint: Option<SpecExpr>,
22}
23
24#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq)]
25#[serde(rename_all = "snake_case")]
26pub enum SpecType { Int, Float, Bool, Str }
27
28#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
29#[serde(tag = "node")]
30pub enum SpecExpr {
31    Var { name: String },
32    IntLit { value: i64 },
33    FloatLit { value: f64 },
34    BoolLit { value: bool },
35    StrLit { value: String },
36    /// A call into the target Lex function (or another helper).
37    Call { func: String, args: Vec<SpecExpr> },
38    Let { name: String, value: Box<SpecExpr>, body: Box<SpecExpr> },
39    BinOp { op: SpecOp, lhs: Box<SpecExpr>, rhs: Box<SpecExpr> },
40    Not { expr: Box<SpecExpr> },
41}
42
43#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq)]
44#[serde(rename_all = "snake_case")]
45pub enum SpecOp {
46    Add, Sub, Mul, Div, Mod,
47    Eq, Neq, Lt, Le, Gt, Ge,
48    And, Or,
49}
50
51impl SpecOp {
52    pub fn as_str(self) -> &'static str {
53        use SpecOp::*;
54        match self {
55            Add => "+", Sub => "-", Mul => "*", Div => "/", Mod => "%",
56            Eq => "==", Neq => "!=", Lt => "<", Le => "<=", Gt => ">", Ge => ">=",
57            And => "and", Or => "or",
58        }
59    }
60    pub fn is_arith(self) -> bool {
61        use SpecOp::*; matches!(self, Add | Sub | Mul | Div | Mod)
62    }
63    pub fn is_compare(self) -> bool {
64        use SpecOp::*; matches!(self, Eq | Neq | Lt | Le | Gt | Ge)
65    }
66    pub fn is_bool(self) -> bool {
67        use SpecOp::*; matches!(self, And | Or)
68    }
69}
spec_checker/ast.rs

spec_checker/
ast.rs
