Ast

ODE RHS expression language + interval evaluator.

This is a small companion to the existing PINN PDE DSL, specialized for ODE IVPs: u'(t) = f(t, u(t)).

We use conservative interval arithmetic over α × α intervals (for any scalar α with a Context instance), with a few common transcendentals (sin, cos, exp, log) needed by the benchmarks in arXiv:2601.19818.

For the trigonometric cases we use a 1-Lipschitz enclosure around the midpoint and then clamp to [-1,1]. Over real-valued semantics this is the intended enclosure argument; executable scalar backends rely on their Context operations matching the assumed real behavior closely enough for the checker mode being used.

Expr is an AST for ODE right-hand sides f(t,u).

We cover the arithmetic and elementary functions needed by the ODE certificate format used in TorchLean: constants, the independent variable t, the state variable u, field arithmetic, and the common scalar functions sin, cos, exp, and log. Keeping this language explicit makes the checker easier to inspect while still covering the benchmark equations we want to verify.

inductive NN.Verification.ODE.Expr : Type

• const (c : Float) : Expr
• t : Expr
• u : Expr
• add (a b : Expr) : Expr
• sub (a b : Expr) : Expr
• mul (a b : Expr) : Expr
• div (a b : Expr) : Expr
• neg (a : Expr) : Expr
• sin (a : Expr) : Expr
• cos (a : Expr) : Expr
• exp (a : Expr) : Expr
• log (a : Expr) : Expr

@[implicit_reducible]

instance NN.Verification.ODE.instReprExpr : Repr Expr

def NN.Verification.ODE.instReprExpr.repr : Expr → ℕ → Std.Format

An evaluation environment for Expr.

We interpret t and u as intervals (lo,hi); everything evaluates to an interval.

structure NN.Verification.ODE.Env (α : Type) : Type

• t : α × α

  Interval for the independent time variable t.

• u : α × α

  Interval for the current state value u(t).

Interval primitives used by eval.

These operations are written against the abstract scalar interface Context α so we can evaluate the same expression under Float or IEEE32Exec (or other executable scalars).

@[inline]

def NN.Verification.ODE.Ival.leBool {α : Type} [Context α] (x y : α) : Bool

Boolean x ≤ y test, implemented via the primitive Context.gtBool.

@[inline]

def NN.Verification.ODE.Ival.min2 {α : Type} [Context α] (a b : α) : α

Binary minimum.

@[inline]

def NN.Verification.ODE.Ival.max2 {α : Type} [Context α] (a b : α) : α

Binary maximum.

@[inline]

def NN.Verification.ODE.Ival.add {α : Type} [Context α] (x y : α × α) : α × α

Interval addition.

@[inline]

def NN.Verification.ODE.Ival.sub {α : Type} [Context α] (x y : α × α) : α × α

Interval subtraction.

@[inline]

def NN.Verification.ODE.Ival.neg {α : Type} [Context α] (x : α × α) : α × α

Interval negation.

@[inline]

def NN.Verification.ODE.Ival.mul {α : Type} [Context α] (x y : α × α) : α × α

Interval multiplication using the standard four-product enclosure.

@[inline]

def NN.Verification.ODE.Ival.inv {α : Type} [Context α] (y : α × α) : Option (α × α)

Interval reciprocal.

Returns none if the interval contains 0, because 1/x is not interval-safe across a pole.

@[inline]

def NN.Verification.ODE.Ival.div {α : Type} [Context α] (x y : α × α) : Option (α × α)

Interval division, returning none if the denominator interval contains 0.

@[inline]

def NN.Verification.ODE.Ival.exp {α : Type} [Context α] (x : α × α) : α × α

Interval exponential (monotone, so endpoints map to endpoints).

@[inline]

def NN.Verification.ODE.Ival.log {α : Type} [Context α] (x : α × α) : Option (α × α)

Interval logarithm.

Returns none unless the interval is strictly positive.

@[inline]

def NN.Verification.ODE.Ival.sin {α : Type} [Context α] (x : α × α) : α × α

Interval sine enclosure.

We use a 1‑Lipschitz enclosure around the midpoint and clamp to [-1, 1].

@[inline]

def NN.Verification.ODE.Ival.cos {α : Type} [Context α] (x : α × α) : α × α

Interval cosine enclosure.

Same strategy as sin: 1‑Lipschitz around the midpoint, clamped to [-1, 1].

Interval evaluation for Expr.

evalWithFuel uses a fuel parameter so the evaluator is total even for malformed/self-referential expressions (though Expr itself has no recursion).

def NN.Verification.ODE.evalWithFuel {α : Type} [Context α] (ofFloat : Float → α) (fuel : ℕ) (env : Env α) (e : Expr) : Option (α × α)

Convenience wrapper with a generous fixed fuel.

def NN.Verification.ODE.eval {α : Type} [Context α] (ofFloat : Float → α) (env : Env α) (e : Expr) : Option (α × α)