Ast

ODE right-hand-side expressions and interval endpoint calculations.

This is a small companion to the existing PINN PDE DSL, specialized for ODE IVPs:

$$ u'(t)=f(t,u(t)). $$

The evaluator uses α × α endpoint pairs and the arithmetic supplied by Context α, including sin, cos, exp, and log for the benchmarks in arXiv:2601.19818. It does not request directed rounding or supply transcendental error bounds. Floating-point evaluation therefore does not automatically establish an enclosure of the exact-real expression.

For the trigonometric cases we use a 1-Lipschitz enclosure around the midpoint and then clamp to $[-1,1]$. That is the exact-real enclosure argument; finite arithmetic needs separate rounding and function-approximation bounds before the same conclusion follows.

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

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

@[instance_reducible]

instance NN.Verification.ODE.instReprExpr : Repr Expr

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 ExecFloat.Binary 8 23 (or other executable scalars).

@[noinline]

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

Whether a checker scalar is finite under the supported Float and ExecFloat.Binary 8 23 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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [Context α] (x y : α × α) : α × α

Add two closed intervals endpointwise.

@[inline]

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

Subtract endpoint pairs with the standard interval formula, using the selected arithmetic.

@[inline]

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

Negate a closed interval by swapping and negating endpoints.

@[inline]

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

Interval multiplication using the standard four-product enclosure.

@[inline]

def NN.Verification.ODE.Ival.inv {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [Context α] (x y : α × α) : Option (α × α)

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

@[inline]

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

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

@[inline]

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

Interval logarithm.

Returns none unless the interval is strictly positive.

@[inline]

def NN.Verification.ODE.Ival.lipschitzOneClamped {α : Type} [TorchLean.Storage α] [Context α] (f : α → α) (x : α × α) : α × α

Enclosure of a 1-Lipschitz function with range in $[-1,1]$: evaluate at the midpoint, widen by the radius, and clamp. Shared by sin and cos.

@[inline]

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

Interval sine enclosure: 1-Lipschitz around the midpoint, clamped to [-1, 1].

@[inline]

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

Interval cosine enclosure: same strategy as sin.

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

Interval evaluation for Expr.

Structural recursion on Expr is already total; the fuel parameter caps the accepted expression depth (512 via eval), so deeper expressions are rejected with none instead of evaluated.

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

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