lean/ExprSpecAeneas.lean

-- File: lean/ExprSpecAeneas.lean
-- Expression Evaluator — Aeneas-compatible specification.
-- Types mirror what Aeneas generates from Rust enum/i64 code.
-- Requires: lake update  (fetches the Aeneas package)

import Aeneas
open Aeneas.Primitives

namespace ExprSpecAeneas

-- Mirrors Rust Op enum
inductive Op | Add | Sub | Mul | Div
  deriving BEq, DecidableEq

-- Mirrors Rust Expr enum (as Aeneas-generated algebraic type)
inductive Expr
  | Lit (n : I64)
  | BinOp (op : Op) (l r : Expr)
  deriving BEq, DecidableEq

-- Evaluate binary op; Div by zero → Err (maps to Rust's Err/None path)
def evalBinOp (op : Op) (a b : I64) : Result I64 :=
  match op with
  | .Add => do let r ← a + b; .ok r   -- scalar overflow → Err
  | .Sub => do let r ← a - b; .ok r
  | .Mul => do let r ← a * b; .ok r
  | .Div => if b == (0 : I64) then .fail .panic else do let r ← a / b; .ok r

-- Recursively evaluate expression tree
def evalExpr : Expr → Result I64
  | .Lit n      => .ok n
  | .BinOp op l r => do
      let a ← evalExpr l
      let b ← evalExpr r
      evalBinOp op a b

-- Division by zero always fails
theorem division_by_zero (a : I64) : evalBinOp .Div a 0 = .fail .panic := by
  simp [evalBinOp, I64.instBEq]

end ExprSpecAeneas