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, Serialize, Deserialize, PartialEq)]
25#[serde(tag = "kind", rename_all = "snake_case")]
26pub enum SpecType {
27    Int,
28    Float,
29    Bool,
30    Str,
31    /// Record type with named fields (#208). Quantifying over a
32    /// record-shaped binding lets specs reference structured agent
33    /// state without flattening into per-field scalar bindings.
34    /// Fields are stored in declaration order; the gate evaluator
35    /// resolves `expr.field` against `Value::Record`'s `IndexMap`,
36    /// which preserves insertion order.
37    Record { fields: Vec<(String, SpecType)> },
38    /// List of an element type (#208). Quantifying over a list lets
39    /// specs reason about agent collections — outstanding orders,
40    /// active charging sessions, message queues — via `length`,
41    /// `head`, `tail`, and indexed access (`xs[i]`).
42    List { element: Box<SpecType> },
43    /// Named user type (#208 slice 3). Refers to a user-defined ADT
44    /// from the host program (e.g. `Message`, `Order`). The gate
45    /// evaluator inspects the value's variant tag at match time;
46    /// no compile-time variant table is needed for the gate path.
47    /// The random-input prover (`check_spec`) can't sample arbitrary
48    /// user types and fails out — those tests should provide
49    /// concrete bindings instead.
50    Named { name: String },
51}
52
53#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
54#[serde(tag = "node")]
55pub enum SpecExpr {
56    Var { name: String },
57    IntLit { value: i64 },
58    FloatLit { value: f64 },
59    BoolLit { value: bool },
60    StrLit { value: String },
61    /// A call into the target Lex function (or another helper).
62    Call { func: String, args: Vec<SpecExpr> },
63    Let { name: String, value: Box<SpecExpr>, body: Box<SpecExpr> },
64    BinOp { op: SpecOp, lhs: Box<SpecExpr>, rhs: Box<SpecExpr> },
65    Not { expr: Box<SpecExpr> },
66    /// Field access on a record-typed expression (#208). Evaluated by
67    /// drilling into `Value::Record`'s field map; fails-loudly if the
68    /// underlying value isn't a record or doesn't contain the field.
69    FieldAccess { value: Box<SpecExpr>, field: String },
70    /// Indexed access on a list-typed expression (#208). `xs[i]`
71    /// evaluates to the i-th element of the list (zero-based).
72    /// Out-of-bounds indices fail loudly via Inconclusive — agents
73    /// that want defensive behavior wrap with a `length(xs) > i`
74    /// check.
75    Index { list: Box<SpecExpr>, index: Box<SpecExpr> },
76    /// Pattern match on a sum-typed expression (#208 slice 3). Arms
77    /// are tried in order; the first matching arm's body is the
78    /// result. A `_` wildcard pattern is exhaustive. Variant
79    /// patterns (`Charge(x)`) bind positional args by name in the
80    /// arm's body. Non-exhaustive matches fall through to
81    /// Inconclusive at evaluation time.
82    Match { scrutinee: Box<SpecExpr>, arms: Vec<MatchArm> },
83}
84
85#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
86pub struct MatchArm {
87    pub pattern: SpecPattern,
88    pub body: SpecExpr,
89}
90
91#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
92#[serde(tag = "kind", rename_all = "snake_case")]
93pub enum SpecPattern {
94    /// `_` — matches anything, binds nothing.
95    Wildcard,
96    /// `Variant(x, y)` — matches `Value::Variant { name, args }`
97    /// where `name == self.name` and `args.len() == bindings.len()`.
98    /// Each binding name is bound to the corresponding positional
99    /// arg in the arm's body. `Variant()` (no parens) and `Variant`
100    /// (no args) parse identically; both have `bindings: vec![]`.
101    Variant { name: String, bindings: Vec<String> },
102}
103
104#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq)]
105#[serde(rename_all = "snake_case")]
106pub enum SpecOp {
107    Add, Sub, Mul, Div, Mod,
108    Eq, Neq, Lt, Le, Gt, Ge,
109    And, Or,
110}
111
112impl SpecOp {
113    pub fn as_str(self) -> &'static str {
114        use SpecOp::*;
115        match self {
116            Add => "+", Sub => "-", Mul => "*", Div => "/", Mod => "%",
117            Eq => "==", Neq => "!=", Lt => "<", Le => "<=", Gt => ">", Ge => ">=",
118            And => "and", Or => "or",
119        }
120    }
121    pub fn is_arith(self) -> bool {
122        use SpecOp::*; matches!(self, Add | Sub | Mul | Div | Mod)
123    }
124    pub fn is_compare(self) -> bool {
125        use SpecOp::*; matches!(self, Eq | Neq | Lt | Le | Gt | Ge)
126    }
127    pub fn is_bool(self) -> bool {
128        use SpecOp::*; matches!(self, And | Or)
129    }
130}
spec_checker/ast.rs

spec_checker/
ast.rs
