sentri_core/
model.rs

1//! Core domain models for invariant analysis.
2
3use serde::{Deserialize, Serialize};
4use std::collections::{BTreeMap, BTreeSet};
5
6/// A compiled invariant expression with metadata.
7#[derive(Debug, Clone, Serialize, Deserialize)]
8pub struct Invariant {
9    /// Unique identifier for the invariant.
10    pub name: String,
11
12    /// Human-readable description.
13    pub description: Option<String>,
14
15    /// The invariant expression in IR form.
16    pub expression: Expression,
17
18    /// Severity level: "critical", "high", "medium", "low".
19    pub severity: String,
20
21    /// Category: "core", "defi", "bridge", "governance", "account-abstraction", etc.
22    pub category: String,
23
24    /// Whether this invariant should always hold.
25    pub is_always_true: bool,
26
27    /// Layer scopes for cross-layer analysis (e.g., ["bundler", "account", "paymaster"]).
28    /// If empty, applies to all layers.
29    pub layers: Vec<String>,
30
31    /// Execution phases (e.g., ["validation", "execution", "settlement"]).
32    /// For AA invariants that must hold at specific phases. Empty means all phases.
33    pub phases: Vec<String>,
34}
35
36/// An expression tree representing invariant conditions.
37#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
38pub enum Expression {
39    /// Boolean literal.
40    Boolean(bool),
41
42    /// Variable reference.
43    Var(String),
44
45    /// Layer-qualified variable reference (e.g., bundler::nonce).
46    LayerVar {
47        /// Layer name (bundler, account, paymaster, protocol, entrypoint).
48        layer: String,
49        /// Variable name within the layer.
50        var: String,
51    },
52
53    /// Phase-qualified variable reference (e.g., validation::account::balance).
54    /// Checks state at a specific execution phase (validation, execution, settlement).
55    PhaseQualifiedVar {
56        /// Execution phase: "validation", "execution", or "settlement".
57        phase: String,
58        /// Layer name within that phase.
59        layer: String,
60        /// Variable name within the layer.
61        var: String,
62    },
63
64    /// Phase constraint: ensures a condition holds during a specific phase.
65    /// Example: ensure `account::balance >= min_required` during validation phase.
66    PhaseConstraint {
67        /// Phase to enforce the constraint in.
68        phase: String,
69        /// The constraint expression to hold in this phase.
70        constraint: Box<Expression>,
71    },
72
73    /// Cross-phase relation: relates variable values across two phases.
74    /// Example: `validation::account::balance >= execution::account::balance`
75    /// used to track state changes across phases.
76    CrossPhaseRelation {
77        /// First phase.
78        phase1: String,
79        /// First phase expression.
80        expr1: Box<Expression>,
81        /// Second phase.
82        phase2: String,
83        /// Second phase expression.
84        expr2: Box<Expression>,
85        /// Relation operator.
86        op: BinaryOp,
87    },
88
89    /// Integer constant.
90    Int(i128),
91
92    /// Comparison: left op right.
93    BinaryOp {
94        /// Left operand.
95        left: Box<Expression>,
96        /// Operator: ==, !=, <, >, <=, >=.
97        op: BinaryOp,
98        /// Right operand.
99        right: Box<Expression>,
100    },
101
102    /// Logical operation: &&, ||.
103    Logical {
104        /// Left operand.
105        left: Box<Expression>,
106        /// Operator: And, Or.
107        op: LogicalOp,
108        /// Right operand.
109        right: Box<Expression>,
110    },
111
112    /// Logical negation.
113    Not(Box<Expression>),
114
115    /// Function call.
116    FunctionCall {
117        /// Function name.
118        name: String,
119        /// Arguments.
120        args: Vec<Expression>,
121    },
122
123    /// Tuple of expressions.
124    Tuple(Vec<Expression>),
125}
126
127impl std::fmt::Display for Expression {
128    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
129        match self {
130            Self::Boolean(b) => write!(f, "{}", b),
131            Self::Var(v) => write!(f, "{}", v),
132            Self::LayerVar { layer, var } => write!(f, "{}::{}", layer, var),
133            Self::PhaseQualifiedVar { phase, layer, var } => {
134                write!(f, "{}::{}::{}", phase, layer, var)
135            }
136            Self::PhaseConstraint { phase, constraint } => {
137                write!(f, "({} @ {})", constraint, phase)
138            }
139            Self::CrossPhaseRelation {
140                phase1,
141                expr1,
142                phase2,
143                expr2,
144                op,
145            } => {
146                write!(f, "({}[{}] {} {}[{}])", expr1, phase1, op, expr2, phase2)
147            }
148            Self::Int(i) => write!(f, "{}", i),
149            Self::BinaryOp { left, op, right } => {
150                write!(f, "({} {} {})", left, op, right)
151            }
152            Self::Logical { left, op, right } => {
153                write!(f, "({} {} {})", left, op, right)
154            }
155            Self::Not(e) => write!(f, "!({})", e),
156            Self::FunctionCall { name, args } => {
157                write!(f, "{}(", name)?;
158                for (i, arg) in args.iter().enumerate() {
159                    if i > 0 {
160                        write!(f, ", ")?;
161                    }
162                    write!(f, "{}", arg)?;
163                }
164                write!(f, ")")
165            }
166            Self::Tuple(exprs) => {
167                write!(f, "(")?;
168                for (i, e) in exprs.iter().enumerate() {
169                    if i > 0 {
170                        write!(f, ", ")?;
171                    }
172                    write!(f, "{}", e)?;
173                }
174                write!(f, ")")
175            }
176        }
177    }
178}
179
180/// Binary operators for expressions.
181#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
182pub enum BinaryOp {
183    /// Equality.
184    Eq,
185    /// Not equal.
186    Neq,
187    /// Less than.
188    Lt,
189    /// Greater than.
190    Gt,
191    /// Less than or equal.
192    Lte,
193    /// Greater than or equal.
194    Gte,
195}
196
197impl std::fmt::Display for BinaryOp {
198    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
199        match self {
200            Self::Eq => write!(f, "=="),
201            Self::Neq => write!(f, "!="),
202            Self::Lt => write!(f, "<"),
203            Self::Gt => write!(f, ">"),
204            Self::Lte => write!(f, "<="),
205            Self::Gte => write!(f, ">="),
206        }
207    }
208}
209
210/// Logical operators.
211#[derive(Debug, Clone, Copy, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
212pub enum LogicalOp {
213    /// Logical AND.
214    And,
215    /// Logical OR.
216    Or,
217}
218
219impl std::fmt::Display for LogicalOp {
220    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
221        match self {
222            Self::And => write!(f, "&&"),
223            Self::Or => write!(f, "||"),
224        }
225    }
226}
227
228/// A state variable in a program.
229#[derive(Debug, Clone, Serialize, Deserialize)]
230pub struct StateVar {
231    /// Variable name.
232    pub name: String,
233
234    /// Data type (chain-specific).
235    pub type_name: String,
236
237    /// Whether it's mutable.
238    pub is_mutable: bool,
239
240    /// Visibility: "public", "private", "internal", etc.
241    pub visibility: Option<String>,
242}
243
244/// A function or entry point in a program.
245#[derive(Debug, Clone, Serialize, Deserialize)]
246pub struct FunctionModel {
247    /// Function name.
248    pub name: String,
249
250    /// Function signature/parameters.
251    pub parameters: Vec<String>,
252
253    /// Return type.
254    pub return_type: Option<String>,
255
256    /// State variables this function mutates.
257    pub mutates: BTreeSet<String>,
258
259    /// State variables this function reads.
260    pub reads: BTreeSet<String>,
261
262    /// Whether this is an entry point.
263    pub is_entry_point: bool,
264
265    /// Whether it's pure/view (doesn't mutate state).
266    pub is_pure: bool,
267}
268
269/// A complete program model extracted from source code.
270#[derive(Debug, Clone, Serialize, Deserialize)]
271pub struct ProgramModel {
272    /// Program/contract/module name.
273    pub name: String,
274
275    /// State variables.
276    pub state_vars: BTreeMap<String, StateVar>,
277
278    /// Functions/entry points.
279    pub functions: BTreeMap<String, FunctionModel>,
280
281    /// Functions → Mutations mapping (deterministic).
282    pub mutation_graph: BTreeMap<String, BTreeSet<String>>,
283
284    /// Chains supported: "solana", "evm", "move".
285    pub chain: String,
286
287    /// Source file path.
288    pub source_path: String,
289}
290
291impl ProgramModel {
292    /// Create a new program model.
293    pub fn new(name: String, chain: String, source_path: String) -> Self {
294        Self {
295            name,
296            chain,
297            source_path,
298            state_vars: BTreeMap::new(),
299            functions: BTreeMap::new(),
300            mutation_graph: BTreeMap::new(),
301        }
302    }
303
304    /// Add a state variable to the model.
305    pub fn add_state_var(&mut self, var: StateVar) {
306        self.state_vars.insert(var.name.clone(), var);
307    }
308
309    /// Add a function to the model.
310    pub fn add_function(&mut self, func: FunctionModel) {
311        self.mutation_graph
312            .insert(func.name.clone(), func.mutates.clone());
313        self.functions.insert(func.name.clone(), func);
314    }
315}
316
317/// Output from code generation.
318#[derive(Debug, Clone, Serialize, Deserialize)]
319pub struct GenerationOutput {
320    /// The generated code.
321    pub code: String,
322
323    /// Assertions injected.
324    pub assertions: Vec<String>,
325
326    /// Generated tests (if any).
327    pub tests: Option<String>,
328
329    /// Coverage percentage (0-100).
330    pub coverage_percent: u8,
331}
332
333/// Report from a simulation run.
334#[derive(Debug, Clone, Serialize, Deserialize)]
335pub struct SimulationReport {
336    /// Number of violations found.
337    pub violations: usize,
338
339    /// Violation traces.
340    pub traces: Vec<String>,
341
342    /// Coverage percentage.
343    pub coverage: f64,
344
345    /// Deterministic seed used.
346    pub seed: u64,
347}
sentri_core/model.rs

sentri_core/
model.rs
