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.

inductive NN.Verification.ODE.Expr : Type

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.

• 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

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

An evaluation environment for Expr.

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

• 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).

@[noinline]

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

Whether a checker scalar is finite under the supported Float and IEEE32Exec backends.

Both backends produce NaN for $\infty-\infty$ and for $\mathrm{NaN}-\mathrm{NaN}$, whereas every finite value subtracts from itself to zero. Expressing the guard through Context keeps the interval evaluator generic without relying on a backend-specific bit decoder.

@[noinline]

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

Boolean $x\leq y$ test that rejects NaN and infinite endpoints.

Writing this as $\neg(x>y)$ would treat unordered values as less than or equal to every value. Some host Float comparisons also use a total implementation order, so the explicit finite guards are part of the certificate check rather than an optimization.

@[inline]

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

Minimum of two scalar endpoints, propagating a non-finite operand so later checks reject it.

@[inline]

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

Maximum of two scalar endpoints, propagating a non-finite operand so later checks reject it.

@[inline]

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

Add two closed intervals endpointwise.

@[inline]

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

Subtract closed intervals using the standard outward endpoint formula.

@[inline]

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

Negate a closed interval by swapping and negating endpoints.

@[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].

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

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.eval {α : Type} [Context α] (ofFloat : Float → α) (env : Env α) (e : Expr) : Option (α × α)

Evaluate an ODE expression with the default recursion fuel used by certificate checking.