intent_runtime/
eval.rs

1use intent_ir::{ArithOp, CmpOp, IrExpr, IrLiteral};
2use serde_json::Value;
3
4use crate::error::RuntimeError;
5use crate::value::EvalContext;
6
7/// Evaluate an IR expression against a context of concrete values.
8///
9/// Returns a JSON `Value` on success. Boolean expressions return `Value::Bool`,
10/// numeric expressions return `Value::Number`, etc.
11pub fn evaluate(expr: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
12    match expr {
13        IrExpr::Literal(lit) => eval_literal(lit),
14        IrExpr::Var(name) => eval_var(name, ctx),
15        IrExpr::FieldAccess { root, field } => eval_field_access(root, field, ctx),
16        IrExpr::Compare { left, op, right } => eval_compare(left, *op, right, ctx),
17        IrExpr::Arithmetic { left, op, right } => eval_arithmetic(left, *op, right, ctx),
18        IrExpr::And(left, right) => eval_and(left, right, ctx),
19        IrExpr::Or(left, right) => eval_or(left, right, ctx),
20        IrExpr::Not(inner) => eval_not(inner, ctx),
21        IrExpr::Implies(left, right) => eval_implies(left, right, ctx),
22        IrExpr::Old(inner) => eval_old(inner, ctx),
23        IrExpr::Forall { binding, ty, body } => eval_forall(binding, ty, body, ctx),
24        IrExpr::Exists { binding, ty, body } => eval_exists(binding, ty, body, ctx),
25        IrExpr::Call { name, args } => eval_call(name, args, ctx),
26        IrExpr::List(items) => eval_list(items, ctx),
27    }
28}
29
30fn eval_literal(lit: &IrLiteral) -> Result<Value, RuntimeError> {
31    match lit {
32        IrLiteral::Null => Ok(Value::Null),
33        IrLiteral::Bool(b) => Ok(Value::Bool(*b)),
34        IrLiteral::Int(n) => Ok(json_number_i64(*n)),
35        IrLiteral::Decimal(s) => parse_decimal_value(s),
36        IrLiteral::String(s) => Ok(Value::String(s.clone())),
37    }
38}
39
40fn eval_var(name: &str, ctx: &EvalContext) -> Result<Value, RuntimeError> {
41    // Check bindings first
42    if let Some(val) = ctx.bindings.get(name) {
43        return Ok(val.clone());
44    }
45    // Uppercase identifiers are union variant labels — return as strings
46    if name.starts_with(|c: char| c.is_uppercase()) {
47        return Ok(Value::String(name.to_string()));
48    }
49    Err(RuntimeError::UnboundVariable(name.to_string()))
50}
51
52fn eval_field_access(root: &IrExpr, field: &str, ctx: &EvalContext) -> Result<Value, RuntimeError> {
53    let root_val = evaluate(root, ctx)?;
54    match &root_val {
55        Value::Object(map) => map.get(field).cloned().ok_or(RuntimeError::FieldNotFound {
56            field: field.to_string(),
57        }),
58        Value::Null => Err(RuntimeError::FieldNotFound {
59            field: field.to_string(),
60        }),
61        _ => Err(RuntimeError::NotAnObject),
62    }
63}
64
65fn eval_compare(
66    left: &IrExpr,
67    op: CmpOp,
68    right: &IrExpr,
69    ctx: &EvalContext,
70) -> Result<Value, RuntimeError> {
71    let lhs = evaluate(left, ctx)?;
72    let rhs = evaluate(right, ctx)?;
73
74    let result = match op {
75        CmpOp::Eq => values_equal(&lhs, &rhs),
76        CmpOp::Ne => !values_equal(&lhs, &rhs),
77        CmpOp::Lt => values_compare(&lhs, &rhs)?.is_some_and(|o| o.is_lt()),
78        CmpOp::Gt => values_compare(&lhs, &rhs)?.is_some_and(|o| o.is_gt()),
79        CmpOp::Le => values_compare(&lhs, &rhs)?.is_some_and(|o| o.is_le()),
80        CmpOp::Ge => values_compare(&lhs, &rhs)?.is_some_and(|o| o.is_ge()),
81    };
82    Ok(Value::Bool(result))
83}
84
85fn eval_arithmetic(
86    left: &IrExpr,
87    op: ArithOp,
88    right: &IrExpr,
89    ctx: &EvalContext,
90) -> Result<Value, RuntimeError> {
91    let lhs = evaluate(left, ctx)?;
92    let rhs = evaluate(right, ctx)?;
93
94    match (&lhs, &rhs) {
95        (Value::Number(a), Value::Number(b)) => {
96            let af = as_f64(a);
97            let bf = as_f64(b);
98            let result = match op {
99                ArithOp::Add => af + bf,
100                ArithOp::Sub => af - bf,
101            };
102            Ok(json_number_f64(result))
103        }
104        _ => Err(RuntimeError::TypeError {
105            expected: "number".into(),
106            got: type_name(&lhs),
107        }),
108    }
109}
110
111fn eval_and(left: &IrExpr, right: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
112    let lhs = as_bool(&evaluate(left, ctx)?)?;
113    if !lhs {
114        return Ok(Value::Bool(false)); // short-circuit
115    }
116    let rhs = as_bool(&evaluate(right, ctx)?)?;
117    Ok(Value::Bool(rhs))
118}
119
120fn eval_or(left: &IrExpr, right: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
121    let lhs = as_bool(&evaluate(left, ctx)?)?;
122    if lhs {
123        return Ok(Value::Bool(true)); // short-circuit
124    }
125    let rhs = as_bool(&evaluate(right, ctx)?)?;
126    Ok(Value::Bool(rhs))
127}
128
129fn eval_not(inner: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
130    let val = as_bool(&evaluate(inner, ctx)?)?;
131    Ok(Value::Bool(!val))
132}
133
134fn eval_implies(left: &IrExpr, right: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
135    // a => b  ≡  !a || b
136    let lhs = as_bool(&evaluate(left, ctx)?)?;
137    if !lhs {
138        return Ok(Value::Bool(true));
139    }
140    let rhs = as_bool(&evaluate(right, ctx)?)?;
141    Ok(Value::Bool(rhs))
142}
143
144fn eval_old(inner: &IrExpr, ctx: &EvalContext) -> Result<Value, RuntimeError> {
145    let old_bindings = ctx
146        .old_bindings
147        .as_ref()
148        .ok_or(RuntimeError::OldWithoutContext)?;
149
150    let old_ctx = EvalContext {
151        bindings: old_bindings.clone(),
152        old_bindings: None,
153        instances: ctx.instances.clone(),
154    };
155    evaluate(inner, &old_ctx)
156}
157
158fn eval_forall(
159    binding: &str,
160    ty: &str,
161    body: &IrExpr,
162    ctx: &EvalContext,
163) -> Result<Value, RuntimeError> {
164    let instances = ctx
165        .instances
166        .get(ty)
167        .ok_or_else(|| RuntimeError::NoInstances(ty.to_string()))?;
168
169    for instance in instances {
170        let child_ctx = ctx.with_binding(binding.to_string(), instance.clone());
171        let result = as_bool(&evaluate(body, &child_ctx)?)?;
172        if !result {
173            return Ok(Value::Bool(false));
174        }
175    }
176    Ok(Value::Bool(true))
177}
178
179fn eval_exists(
180    binding: &str,
181    ty: &str,
182    body: &IrExpr,
183    ctx: &EvalContext,
184) -> Result<Value, RuntimeError> {
185    let instances = ctx
186        .instances
187        .get(ty)
188        .ok_or_else(|| RuntimeError::NoInstances(ty.to_string()))?;
189
190    for instance in instances {
191        let child_ctx = ctx.with_binding(binding.to_string(), instance.clone());
192        let result = as_bool(&evaluate(body, &child_ctx)?)?;
193        if result {
194            return Ok(Value::Bool(true));
195        }
196    }
197    Ok(Value::Bool(false))
198}
199
200fn eval_call(name: &str, args: &[IrExpr], ctx: &EvalContext) -> Result<Value, RuntimeError> {
201    let evaluated_args: Vec<Value> = args
202        .iter()
203        .map(|a| evaluate(a, ctx))
204        .collect::<Result<_, _>>()?;
205
206    // Built-in functions
207    match name {
208        "len" => {
209            if let Some(val) = evaluated_args.first() {
210                match val {
211                    Value::Array(arr) => Ok(json_number_i64(arr.len() as i64)),
212                    Value::String(s) => Ok(json_number_i64(s.len() as i64)),
213                    _ => Err(RuntimeError::TypeError {
214                        expected: "array or string".into(),
215                        got: type_name(val),
216                    }),
217                }
218            } else {
219                Err(RuntimeError::TypeError {
220                    expected: "1 argument".into(),
221                    got: "0 arguments".into(),
222                })
223            }
224        }
225        "now" => Ok(Value::String("now()".to_string())),
226        _ => Err(RuntimeError::UnknownFunction(name.to_string())),
227    }
228}
229
230fn eval_list(items: &[IrExpr], ctx: &EvalContext) -> Result<Value, RuntimeError> {
231    let values: Vec<Value> = items
232        .iter()
233        .map(|i| evaluate(i, ctx))
234        .collect::<Result<_, _>>()?;
235    Ok(Value::Array(values))
236}
237
238// ── Helpers ──────────────────────────────────────────────────
239
240fn as_bool(val: &Value) -> Result<bool, RuntimeError> {
241    match val {
242        Value::Bool(b) => Ok(*b),
243        _ => Err(RuntimeError::TypeError {
244            expected: "bool".into(),
245            got: type_name(val),
246        }),
247    }
248}
249
250fn as_f64(n: &serde_json::Number) -> f64 {
251    n.as_f64().unwrap_or(0.0)
252}
253
254fn json_number_i64(n: i64) -> Value {
255    Value::Number(serde_json::Number::from(n))
256}
257
258fn json_number_f64(n: f64) -> Value {
259    serde_json::Number::from_f64(n).map_or(Value::Null, Value::Number)
260}
261
262fn parse_decimal_value(s: &str) -> Result<Value, RuntimeError> {
263    s.parse::<f64>()
264        .map(json_number_f64)
265        .map_err(|_| RuntimeError::DecimalError(format!("invalid decimal: {s}")))
266}
267
268fn type_name(val: &Value) -> String {
269    match val {
270        Value::Null => "null".into(),
271        Value::Bool(_) => "bool".into(),
272        Value::Number(_) => "number".into(),
273        Value::String(_) => "string".into(),
274        Value::Array(_) => "array".into(),
275        Value::Object(_) => "object".into(),
276    }
277}
278
279fn values_equal(a: &Value, b: &Value) -> bool {
280    match (a, b) {
281        (Value::Number(a), Value::Number(b)) => as_f64(a) == as_f64(b),
282        _ => a == b,
283    }
284}
285
286fn values_compare(a: &Value, b: &Value) -> Result<Option<std::cmp::Ordering>, RuntimeError> {
287    match (a, b) {
288        (Value::Number(a), Value::Number(b)) => Ok(as_f64(a).partial_cmp(&as_f64(b))),
289        (Value::String(a), Value::String(b)) => Ok(Some(a.cmp(b))),
290        _ => Err(RuntimeError::TypeError {
291            expected: "comparable types (number or string)".into(),
292            got: format!("{} vs {}", type_name(a), type_name(b)),
293        }),
294    }
295}
296
297#[cfg(test)]
298mod tests {
299    use super::*;
300    use serde_json::json;
301    use std::collections::HashMap;
302
303    fn empty_ctx() -> EvalContext {
304        EvalContext::new()
305    }
306
307    fn ctx_with(bindings: Vec<(&str, Value)>) -> EvalContext {
308        let mut ctx = EvalContext::new();
309        for (k, v) in bindings {
310            ctx.bindings.insert(k.to_string(), v);
311        }
312        ctx
313    }
314
315    // ── Literals ──────────────────────────────────────────
316
317    #[test]
318    fn eval_literal_null() {
319        let expr = IrExpr::Literal(IrLiteral::Null);
320        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), Value::Null);
321    }
322
323    #[test]
324    fn eval_literal_bool() {
325        let expr = IrExpr::Literal(IrLiteral::Bool(true));
326        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
327    }
328
329    #[test]
330    fn eval_literal_int() {
331        let expr = IrExpr::Literal(IrLiteral::Int(42));
332        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(42));
333    }
334
335    #[test]
336    fn eval_literal_decimal() {
337        let expr = IrExpr::Literal(IrLiteral::Decimal("10.50".into()));
338        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(10.50));
339    }
340
341    #[test]
342    fn eval_literal_string() {
343        let expr = IrExpr::Literal(IrLiteral::String("hello".into()));
344        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!("hello"));
345    }
346
347    // ── Variables ─────────────────────────────────────────
348
349    #[test]
350    fn eval_bound_variable() {
351        let ctx = ctx_with(vec![("amount", json!(100))]);
352        let expr = IrExpr::Var("amount".into());
353        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(100));
354    }
355
356    #[test]
357    fn eval_unbound_variable_error() {
358        let expr = IrExpr::Var("unknown".into());
359        assert_eq!(
360            evaluate(&expr, &empty_ctx()),
361            Err(RuntimeError::UnboundVariable("unknown".into()))
362        );
363    }
364
365    #[test]
366    fn eval_union_variant_as_string() {
367        let expr = IrExpr::Var("Active".into());
368        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!("Active"));
369    }
370
371    // ── Field Access ──────────────────────────────────────
372
373    #[test]
374    fn eval_field_access() {
375        let ctx = ctx_with(vec![("account", json!({"balance": 500, "name": "Alice"}))]);
376        let expr = IrExpr::FieldAccess {
377            root: Box::new(IrExpr::Var("account".into())),
378            field: "balance".into(),
379        };
380        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(500));
381    }
382
383    #[test]
384    fn eval_nested_field_access() {
385        let ctx = ctx_with(vec![("user", json!({"profile": {"email": "a@b.com"}}))]);
386        let expr = IrExpr::FieldAccess {
387            root: Box::new(IrExpr::FieldAccess {
388                root: Box::new(IrExpr::Var("user".into())),
389                field: "profile".into(),
390            }),
391            field: "email".into(),
392        };
393        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!("a@b.com"));
394    }
395
396    #[test]
397    fn eval_field_not_found() {
398        let ctx = ctx_with(vec![("obj", json!({"a": 1}))]);
399        let expr = IrExpr::FieldAccess {
400            root: Box::new(IrExpr::Var("obj".into())),
401            field: "missing".into(),
402        };
403        assert_eq!(
404            evaluate(&expr, &ctx),
405            Err(RuntimeError::FieldNotFound {
406                field: "missing".into()
407            })
408        );
409    }
410
411    #[test]
412    fn eval_field_access_on_non_object() {
413        let ctx = ctx_with(vec![("x", json!(42))]);
414        let expr = IrExpr::FieldAccess {
415            root: Box::new(IrExpr::Var("x".into())),
416            field: "f".into(),
417        };
418        assert_eq!(evaluate(&expr, &ctx), Err(RuntimeError::NotAnObject));
419    }
420
421    // ── Comparison ────────────────────────────────────────
422
423    #[test]
424    fn eval_compare_eq() {
425        let ctx = ctx_with(vec![("a", json!(5)), ("b", json!(5))]);
426        let expr = IrExpr::Compare {
427            left: Box::new(IrExpr::Var("a".into())),
428            op: CmpOp::Eq,
429            right: Box::new(IrExpr::Var("b".into())),
430        };
431        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
432    }
433
434    #[test]
435    fn eval_compare_ne() {
436        let ctx = ctx_with(vec![("a", json!(5)), ("b", json!(3))]);
437        let expr = IrExpr::Compare {
438            left: Box::new(IrExpr::Var("a".into())),
439            op: CmpOp::Ne,
440            right: Box::new(IrExpr::Var("b".into())),
441        };
442        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
443    }
444
445    #[test]
446    fn eval_compare_gt() {
447        let ctx = ctx_with(vec![("a", json!(10)), ("b", json!(5))]);
448        let expr = IrExpr::Compare {
449            left: Box::new(IrExpr::Var("a".into())),
450            op: CmpOp::Gt,
451            right: Box::new(IrExpr::Var("b".into())),
452        };
453        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
454    }
455
456    #[test]
457    fn eval_compare_le() {
458        let expr = IrExpr::Compare {
459            left: Box::new(IrExpr::Literal(IrLiteral::Int(3))),
460            op: CmpOp::Le,
461            right: Box::new(IrExpr::Literal(IrLiteral::Int(3))),
462        };
463        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
464    }
465
466    #[test]
467    fn eval_compare_strings() {
468        let expr = IrExpr::Compare {
469            left: Box::new(IrExpr::Literal(IrLiteral::String("apple".into()))),
470            op: CmpOp::Lt,
471            right: Box::new(IrExpr::Literal(IrLiteral::String("banana".into()))),
472        };
473        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
474    }
475
476    #[test]
477    fn eval_compare_union_variant() {
478        // status == Active where status is stored as string "Active"
479        let ctx = ctx_with(vec![("account", json!({"status": "Active"}))]);
480        let expr = IrExpr::Compare {
481            left: Box::new(IrExpr::FieldAccess {
482                root: Box::new(IrExpr::Var("account".into())),
483                field: "status".into(),
484            }),
485            op: CmpOp::Eq,
486            right: Box::new(IrExpr::Var("Active".into())),
487        };
488        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
489    }
490
491    // ── Arithmetic ────────────────────────────────────────
492
493    #[test]
494    fn eval_arithmetic_add() {
495        let expr = IrExpr::Arithmetic {
496            left: Box::new(IrExpr::Literal(IrLiteral::Int(3))),
497            op: ArithOp::Add,
498            right: Box::new(IrExpr::Literal(IrLiteral::Int(4))),
499        };
500        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(7.0));
501    }
502
503    #[test]
504    fn eval_arithmetic_sub() {
505        let expr = IrExpr::Arithmetic {
506            left: Box::new(IrExpr::Literal(IrLiteral::Int(10))),
507            op: ArithOp::Sub,
508            right: Box::new(IrExpr::Literal(IrLiteral::Int(3))),
509        };
510        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(7.0));
511    }
512
513    #[test]
514    fn eval_arithmetic_type_error() {
515        let expr = IrExpr::Arithmetic {
516            left: Box::new(IrExpr::Literal(IrLiteral::String("x".into()))),
517            op: ArithOp::Add,
518            right: Box::new(IrExpr::Literal(IrLiteral::Int(1))),
519        };
520        assert!(matches!(
521            evaluate(&expr, &empty_ctx()),
522            Err(RuntimeError::TypeError { .. })
523        ));
524    }
525
526    // ── Logical ───────────────────────────────────────────
527
528    #[test]
529    fn eval_and_true() {
530        let expr = IrExpr::And(
531            Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
532            Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
533        );
534        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
535    }
536
537    #[test]
538    fn eval_and_short_circuit() {
539        // false && (error) should not evaluate the right side
540        let expr = IrExpr::And(
541            Box::new(IrExpr::Literal(IrLiteral::Bool(false))),
542            Box::new(IrExpr::Var("nonexistent".into())),
543        );
544        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(false));
545    }
546
547    #[test]
548    fn eval_or_short_circuit() {
549        // true || (error) should not evaluate the right side
550        let expr = IrExpr::Or(
551            Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
552            Box::new(IrExpr::Var("nonexistent".into())),
553        );
554        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
555    }
556
557    #[test]
558    fn eval_not() {
559        let expr = IrExpr::Not(Box::new(IrExpr::Literal(IrLiteral::Bool(false))));
560        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
561    }
562
563    #[test]
564    fn eval_implies_true_antecedent() {
565        // true => true == true
566        let expr = IrExpr::Implies(
567            Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
568            Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
569        );
570        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
571    }
572
573    #[test]
574    fn eval_implies_false_antecedent() {
575        // false => anything == true (vacuously true)
576        let expr = IrExpr::Implies(
577            Box::new(IrExpr::Literal(IrLiteral::Bool(false))),
578            Box::new(IrExpr::Var("nonexistent".into())),
579        );
580        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(true));
581    }
582
583    // ── old() ─────────────────────────────────────────────
584
585    #[test]
586    fn eval_old_with_context() {
587        let mut ctx = ctx_with(vec![("balance", json!(500))]);
588        let mut old = HashMap::new();
589        old.insert("balance".to_string(), json!(1000));
590        ctx.old_bindings = Some(old);
591
592        let expr = IrExpr::Old(Box::new(IrExpr::Var("balance".into())));
593        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(1000));
594    }
595
596    #[test]
597    fn eval_old_without_context() {
598        let expr = IrExpr::Old(Box::new(IrExpr::Var("x".into())));
599        assert_eq!(
600            evaluate(&expr, &empty_ctx()),
601            Err(RuntimeError::OldWithoutContext)
602        );
603    }
604
605    #[test]
606    fn eval_old_field_access() {
607        // old(account.balance)
608        let mut ctx = ctx_with(vec![("account", json!({"balance": 200}))]);
609        let mut old = HashMap::new();
610        old.insert("account".to_string(), json!({"balance": 500}));
611        ctx.old_bindings = Some(old);
612
613        let expr = IrExpr::Old(Box::new(IrExpr::FieldAccess {
614            root: Box::new(IrExpr::Var("account".into())),
615            field: "balance".into(),
616        }));
617        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(500));
618    }
619
620    // ── Quantifiers ───────────────────────────────────────
621
622    #[test]
623    fn eval_forall_true() {
624        // forall a: Account => a.balance >= 0
625        let mut ctx = EvalContext::new();
626        ctx.instances.insert(
627            "Account".into(),
628            vec![
629                json!({"balance": 100}),
630                json!({"balance": 0}),
631                json!({"balance": 50}),
632            ],
633        );
634
635        let expr = IrExpr::Forall {
636            binding: "a".into(),
637            ty: "Account".into(),
638            body: Box::new(IrExpr::Compare {
639                left: Box::new(IrExpr::FieldAccess {
640                    root: Box::new(IrExpr::Var("a".into())),
641                    field: "balance".into(),
642                }),
643                op: CmpOp::Ge,
644                right: Box::new(IrExpr::Literal(IrLiteral::Int(0))),
645            }),
646        };
647        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
648    }
649
650    #[test]
651    fn eval_forall_false() {
652        let mut ctx = EvalContext::new();
653        ctx.instances.insert(
654            "Account".into(),
655            vec![
656                json!({"balance": 100}),
657                json!({"balance": -5}), // violates
658            ],
659        );
660
661        let expr = IrExpr::Forall {
662            binding: "a".into(),
663            ty: "Account".into(),
664            body: Box::new(IrExpr::Compare {
665                left: Box::new(IrExpr::FieldAccess {
666                    root: Box::new(IrExpr::Var("a".into())),
667                    field: "balance".into(),
668                }),
669                op: CmpOp::Ge,
670                right: Box::new(IrExpr::Literal(IrLiteral::Int(0))),
671            }),
672        };
673        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(false));
674    }
675
676    #[test]
677    fn eval_exists_true() {
678        let mut ctx = EvalContext::new();
679        ctx.instances.insert(
680            "Record".into(),
681            vec![json!({"status": "Pending"}), json!({"status": "Completed"})],
682        );
683
684        let expr = IrExpr::Exists {
685            binding: "r".into(),
686            ty: "Record".into(),
687            body: Box::new(IrExpr::Compare {
688                left: Box::new(IrExpr::FieldAccess {
689                    root: Box::new(IrExpr::Var("r".into())),
690                    field: "status".into(),
691                }),
692                op: CmpOp::Eq,
693                right: Box::new(IrExpr::Var("Completed".into())),
694            }),
695        };
696        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
697    }
698
699    #[test]
700    fn eval_exists_false() {
701        let mut ctx = EvalContext::new();
702        ctx.instances
703            .insert("Record".into(), vec![json!({"status": "Pending"})]);
704
705        let expr = IrExpr::Exists {
706            binding: "r".into(),
707            ty: "Record".into(),
708            body: Box::new(IrExpr::Compare {
709                left: Box::new(IrExpr::FieldAccess {
710                    root: Box::new(IrExpr::Var("r".into())),
711                    field: "status".into(),
712                }),
713                op: CmpOp::Eq,
714                right: Box::new(IrExpr::Var("Completed".into())),
715            }),
716        };
717        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(false));
718    }
719
720    #[test]
721    fn eval_forall_no_instances() {
722        let expr = IrExpr::Forall {
723            binding: "x".into(),
724            ty: "Missing".into(),
725            body: Box::new(IrExpr::Literal(IrLiteral::Bool(true))),
726        };
727        assert_eq!(
728            evaluate(&expr, &empty_ctx()),
729            Err(RuntimeError::NoInstances("Missing".into()))
730        );
731    }
732
733    // ── List ──────────────────────────────────────────────
734
735    #[test]
736    fn eval_list_literal() {
737        let expr = IrExpr::List(vec![
738            IrExpr::Literal(IrLiteral::Int(1)),
739            IrExpr::Literal(IrLiteral::Int(2)),
740            IrExpr::Literal(IrLiteral::Int(3)),
741        ]);
742        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!([1, 2, 3]));
743    }
744
745    // ── Call ──────────────────────────────────────────────
746
747    #[test]
748    fn eval_call_len_array() {
749        let ctx = ctx_with(vec![("items", json!([1, 2, 3]))]);
750        let expr = IrExpr::Call {
751            name: "len".into(),
752            args: vec![IrExpr::Var("items".into())],
753        };
754        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(3));
755    }
756
757    #[test]
758    fn eval_call_len_string() {
759        let expr = IrExpr::Call {
760            name: "len".into(),
761            args: vec![IrExpr::Literal(IrLiteral::String("hello".into()))],
762        };
763        assert_eq!(evaluate(&expr, &empty_ctx()).unwrap(), json!(5));
764    }
765
766    #[test]
767    fn eval_call_unknown() {
768        let expr = IrExpr::Call {
769            name: "bogus".into(),
770            args: vec![],
771        };
772        assert_eq!(
773            evaluate(&expr, &empty_ctx()),
774            Err(RuntimeError::UnknownFunction("bogus".into()))
775        );
776    }
777
778    // ── Complex expressions ───────────────────────────────
779
780    #[test]
781    fn eval_postcondition_with_old() {
782        // from.balance == old(from.balance) - amount
783        let mut ctx = ctx_with(vec![
784            ("from", json!({"balance": 800})),
785            ("amount", json!(200)),
786        ]);
787        let mut old = HashMap::new();
788        old.insert("from".to_string(), json!({"balance": 1000}));
789        ctx.old_bindings = Some(old);
790
791        let expr = IrExpr::Compare {
792            left: Box::new(IrExpr::FieldAccess {
793                root: Box::new(IrExpr::Var("from".into())),
794                field: "balance".into(),
795            }),
796            op: CmpOp::Eq,
797            right: Box::new(IrExpr::Arithmetic {
798                left: Box::new(IrExpr::Old(Box::new(IrExpr::FieldAccess {
799                    root: Box::new(IrExpr::Var("from".into())),
800                    field: "balance".into(),
801                }))),
802                op: ArithOp::Sub,
803                right: Box::new(IrExpr::Var("amount".into())),
804            }),
805        };
806        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
807    }
808
809    #[test]
810    fn eval_nested_forall_implies() {
811        // forall a: Account => forall b: Account =>
812        //   a.id != b.id => a.name != b.name
813        let mut ctx = EvalContext::new();
814        ctx.instances.insert(
815            "Account".into(),
816            vec![
817                json!({"id": "1", "name": "Alice"}),
818                json!({"id": "2", "name": "Bob"}),
819            ],
820        );
821
822        let expr = IrExpr::Forall {
823            binding: "a".into(),
824            ty: "Account".into(),
825            body: Box::new(IrExpr::Forall {
826                binding: "b".into(),
827                ty: "Account".into(),
828                body: Box::new(IrExpr::Implies(
829                    Box::new(IrExpr::Compare {
830                        left: Box::new(IrExpr::FieldAccess {
831                            root: Box::new(IrExpr::Var("a".into())),
832                            field: "id".into(),
833                        }),
834                        op: CmpOp::Ne,
835                        right: Box::new(IrExpr::FieldAccess {
836                            root: Box::new(IrExpr::Var("b".into())),
837                            field: "id".into(),
838                        }),
839                    }),
840                    Box::new(IrExpr::Compare {
841                        left: Box::new(IrExpr::FieldAccess {
842                            root: Box::new(IrExpr::Var("a".into())),
843                            field: "name".into(),
844                        }),
845                        op: CmpOp::Ne,
846                        right: Box::new(IrExpr::FieldAccess {
847                            root: Box::new(IrExpr::Var("b".into())),
848                            field: "name".into(),
849                        }),
850                    }),
851                )),
852            }),
853        };
854        assert_eq!(evaluate(&expr, &ctx).unwrap(), json!(true));
855    }
856}
intent_runtime/eval.rs

intent_runtime/
eval.rs
