Piecewise polynomial certificates

This module implements a Lean checker for one-dimensional piecewise-polynomial certificates.

Why this exists:

• In TorchLean’s “external producer, Lean checker” workflow, an external tool (Julia, Python, ...) can fit or search for a piecewise-polynomial surrogate and export a compact JSON artifact.
• Lean then checks basic algebraic consistency conditions on that artifact.

Our checker is conservative: it checks exact equalities over Rat with no floating-point tolerance.

Optionally, you can also run an executable float32 cross-check via checkJsonIEEE32ExecExact: if every rational in the certificate is exactly representable as a finite IEEE-754 binary32 (ExecFloat.Binary 8 23), we re-run the endpoint equalities under ExecFloat.Binary 8 23 arithmetic. This is useful when the producer is actually operating in float32 and you want to confirm the certificate’s equalities hold under the same semantics.

What is checked in format = "piecewise_poly_v0":

• xs is strictly increasing,
• ys has the same length as xs,
• there is one piece per interval $[\mathrm{xs}[i],\mathrm{xs}[i+1]]$,
• each piece’s (lo, hi) matches the corresponding interval endpoints,
• the local-coordinate polynomial interpolates the endpoints exactly: $p_i(\mathrm{xs}[i])=\mathrm{ys}[i]$ and $p_i(\mathrm{xs}[i+1])=\mathrm{ys}[i+1]$.

This certificate format focuses on endpoint and piece consistency. It does not claim global range bounds for higher-degree polynomials; those require additional machinery such as Bernstein bounds or interval arithmetic with derivative-based splitting.

References (background):

• de Boor, A Practical Guide to Splines (1978).
• Certificate checking pattern: export an artifact, then check it in a small Lean checker core.

Utilities: exact rationals in JSON

def NN.Verification.Splines.PiecewisePolyCert.parseRatString (s : String) : Except String ℚ

Parse a rational in the format emitted by TorchLean’s Arb helpers:

• integer: "5", "-3"
• fraction: "5/2", "-7/10"

We avoid JSON numbers here because they are stored as Scientific and are not guaranteed to round-trip exactly for large integers.

def NN.Verification.Splines.PiecewisePolyCert.parseRat (ctx : String) (j : Lean.Json) : IO ℚ

Parse a Rat from a JSON string field with context.

Certificate schema

structure NN.Verification.Splines.PiecewisePolyCert.PolynomialPiece : Type

One polynomial segment on an interval $[\mathrm{lo},\mathrm{hi}]$, using local coordinate $t=x-\mathrm{lo}$.

• lo : ℚ
• hi : ℚ
• coeffs : Array ℚ

@[instance_reducible]

instance NN.Verification.Splines.PiecewisePolyCert.instReprPolynomialPiece : Repr PolynomialPiece

def NN.Verification.Splines.PiecewisePolyCert.instReprPolynomialPiece.repr : PolynomialPiece → ℕ → Std.Format

@[instance_reducible]

instance NN.Verification.Splines.PiecewisePolyCert.instInhabitedPolynomialPiece : Inhabited PolynomialPiece

structure NN.Verification.Splines.PiecewisePolyCert.PiecewisePolyCertificate : Type

Parsed certificate payload for piecewise_poly_v0.

degree is redundant (it should equal coeffs.size - 1), but it is useful for fast validation.

• degree : ℕ

  Polynomial degree d (so each piece has d+1 coefficients).

• n : ℕ

  Number of knot points.

• xs : TorchLean.Tensor ℚ [self.n]

  Knot x-coordinates as a rank-one tensor of length n.

• ys : TorchLean.Tensor ℚ [self.n]

  Knot y-values as a rank-one tensor of length n.

• pieces : Array PolynomialPiece

  One piece per interval $[\mathrm{xs}[i],\mathrm{xs}[i+1]]$.

Polynomial evaluation

def NN.Verification.Splines.PiecewisePolyCert.evalPolyHorner {α : Type} [Zero α] [Add α] [Mul α] (coeffs : Array α) (t : α) : α

Evaluate a polynomial in local coordinate $t$ using Horner’s rule.

Given coefficients $[a_0,a_1,\ldots,a_d]$ representing:

$$ a_0+a_1t+a_2t^2+\cdots+a_dt^d. $$

This helper is generic so we can reuse it for Rat (exact checking) and for ExecFloat.Binary 8 23 (executable float32 semantics).

Parsing

def NN.Verification.Splines.PiecewisePolyCert.Internal.parseRatArray (ctx : String) (j : Lean.Json) : IO (Array ℚ)

Parse an array of rational strings, attaching ctx to any error message.

def NN.Verification.Splines.PiecewisePolyCert.Internal.parsePolynomialPiece (ctx : String) (j : Lean.Json) : IO PolynomialPiece

Parse one polynomial segment from the certificate JSON object.

def NN.Verification.Splines.PiecewisePolyCert.requireArrayEntry {α : Type} (ctx : String) (xs : Array α) (i : ℕ) : IO α

Require an array entry at a certificate-checking boundary, with a schema-oriented error.

def NN.Verification.Splines.PiecewisePolyCert.parsePiecewisePolyCertificate (j : Lean.Json) : IO PiecewisePolyCertificate

Parse the piecewise_poly_v0 JSON payload into a structured certificate.

Checking

def NN.Verification.Splines.PiecewisePolyCert.checkCertificateRat (cert : PiecewisePolyCertificate) : IO Unit

Check a piecewise-polynomial certificate exactly over Rat.

This is the smallest checker core for this format: it uses exact rational arithmetic with no tolerances, so a passing check means the certificate's equalities hold exactly as stated.

def NN.Verification.Splines.PiecewisePolyCert.checkJson (j : Lean.Json) : IO Unit

Check a piecewise_poly_v0 certificate payload.

Raises IO.userError on the first mismatch; prints a short success message otherwise.

def NN.Verification.Splines.PiecewisePolyCert.ratToIEEE32ExecExact (ctx : String) (q : ℚ) : IO (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) ratToIEEE32ExecExact._proof_1 ratToIEEE32ExecExact._proof_2 ratToIEEE32ExecExact._proof_3 ratToIEEE32ExecExact._proof_4)

Attempt to convert a rational to an exact finite ExecFloat.Binary 8 23 value.

This is used for optional “float32 semantics” checking: we only accept values that are exactly representable on the binary32 grid, so equality checks are meaningful at the executable IEEE level.

Implementation note:

• FloatLib rounds the rational outward in its binary32 model; packing that model preserves its bits. We accept only when the lower and upper rounding compare equal.

def NN.Verification.Splines.PiecewisePolyCert.checkCertificateIEEE32ExecExact (cert : PiecewisePolyCertificate) : IO Unit

Check the same endpoint equalities as checkCertificateRat, but under ExecFloat.Binary 8 23 arithmetic.

This is an additional (optional) check that answers: “if we interpret the certificate data as binary32 values and run the polynomial evaluation with executable IEEE-754 ops, do we still hit the claimed endpoints?”

The check is deliberately strict:

• every rational in the cert must be exactly representable as a finite ExecFloat.Binary 8 23,
• comparisons use IEEE-style BEq (so +0 == -0, and NaNs never compare equal).

def NN.Verification.Splines.PiecewisePolyCert.checkJsonIEEE32ExecExact (j : Lean.Json) : IO Unit

Check a piecewise-polynomial certificate stored as JSON, including ExecFloat.Binary 8 23 semantics.

def NN.Verification.Splines.PiecewisePolyCert.checkFile (path : String) : IO Unit

Check a piecewise-polynomial certificate stored as a JSON file.