PdeAst

A compact PDE mini-language (AST) and interval evaluator.

This module defines a small expression language to describe PDE residuals in terms of u, its first/second partial derivatives along axes, and arithmetic combinators. An interval evaluator consumes primitive bounds (u, u_x, u_y, u_xx, ...) and assembles a conservative residual bound for the whole expression.

We focus on 2D workflows: axes are X and Y, but the evaluator works for 1D by ignoring Y.

References:

• PINNs: https://arxiv.org/abs/1711.10561
• Interval/CROWN-style primitive bounds used by the surrounding workflows: https://arxiv.org/abs/1811.00866

inductive NN.Verification.PINN.PdeAst.Axis : Type

Coordinate axis used by the PDE residual language.

• X : Axis
• Y : Axis

@[instance_reducible]

instance NN.Verification.PINN.PdeAst.instDecidableEqAxis : DecidableEq Axis

def NN.Verification.PINN.PdeAst.instReprAxis.repr : Axis → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.PINN.PdeAst.instReprAxis : Repr Axis

inductive NN.Verification.PINN.PdeAst.Expr : Type

Expression language for scalar PDE residuals.

The constructors refer to u, first partials, second partials, constants, and arithmetic combinators. Evaluation is interval-valued because the surrounding PINN checker works with bounds rather than single floating-point samples.

• const (c : Float) : Expr
• u : Expr
• du (a : Axis) : Expr
• d2u (a : Axis) : Expr
• add (e1 e2 : Expr) : Expr
• sub (e1 e2 : Expr) : Expr
• mul (e1 e2 : Expr) : Expr
• scale (c : Float) (e : Expr) : Expr
• neg (e : Expr) : Expr

@[instance_reducible]

instance NN.Verification.PINN.PdeAst.instReprExpr : Repr Expr

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

structure NN.Verification.PINN.PdeAst.Prims : Type

Primitive interval bounds supplied to the PDE expression evaluator.

• u : Option (Float × Float)

  Enclosure for the solution value u itself.

• duX : Option (Float × Float)

  Enclosure for ∂u/∂x.

• duY : Option (Float × Float)

  Enclosure for ∂u/∂y.

• d2uX : Option (Float × Float)

  Enclosure for ∂²u/∂x².

• d2uY : Option (Float × Float)

  Enclosure for ∂²u/∂y². Every field is optional because a residual only needs the derivatives its own PDE mentions; a missing one makes evaluation fail loudly instead of silently substituting a default.

@[inline]

def NN.Verification.PINN.PdeAst.ivalAdd (a b : Float × Float) : Float × Float

Add two closed Float intervals endpointwise.

@[inline]

def NN.Verification.PINN.PdeAst.ivalSub (a b : Float × Float) : Float × Float

Subtract two closed Float intervals using outward endpoint selection.

@[inline]

def NN.Verification.PINN.PdeAst.ivalScale (c : Float) (a : Float × Float) : Float × Float

Scale a closed Float interval, reversing endpoint order for negative coefficients.

@[inline]

def NN.Verification.PINN.PdeAst.ivalNeg (a : Float × Float) : Float × Float

Negate a closed Float interval by swapping and negating its endpoints.

@[inline]

def NN.Verification.PINN.PdeAst.ivalMul (a b : Float × Float) : Float × Float

Bound the product of two Float intervals through the shared McCormick envelopes.

def NN.Verification.PINN.PdeAst.evalWithFuel (fuel : ℕ) (p : Prims) (e : Expr) : Option (Float × Float)

Evaluate a PDE expression to an interval, given primitive bounds.

def NN.Verification.PINN.PdeAst.eval (p : Prims) (e : Expr) : Option (Float × Float)

Evaluate a PDE expression with the default recursion budget.