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

@[implicit_reducible]

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

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

@[implicit_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

@[implicit_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)

  u.

• duX : Option (Float × Float)

  du X.

• duY : Option (Float × Float)

  du Y.

• d2uX : Option (Float × Float)

  d 2 u X.

• d2uY : Option (Float × Float)

  d 2 u Y.

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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.

def NN.Verification.PINN.PdeAst.allenCahn2D (ε : Float) : Expr

2D Allen–Cahn residual: R = ε (u_xx + u_yy) - (u^3 - u).

def NN.Verification.PINN.PdeAst.poissonPlusU : Expr

2D Poisson-like residual: R = u_xx + u_yy + u.