Json

Shared JSON helpers for TorchLean verification tools.

Many verification workflows consume small JSON “certificates” produced by Python tooling (often PyTorch-based). This module centralizes:

• “shape” checks (object + field existence),
• simple scalar parsing (Nat/Float/Bool),
• small array helpers used across checkers.

These helpers take a strict stance: malformed certificates fail fast with contextual error messages instead of silently defaulting.

def NN.Verification.Json.fromExcept {α : Type} (x : Except String α) : IO α

Turn an Except String α parser result into IO, preserving the parser's error text.

def NN.Verification.Json.readJsonFile (path : String) : IO Lean.Json

Read and parse a JSON verification artifact from disk.

Use this at checker boundaries instead of repeating IO.FS.readFile and Json.parse in every tool. The file path is included in parse errors.

def NN.Verification.Json.expectObj (j : Lean.Json) (ctx : String) : IO Lean.Json

Ensure a JSON value is an object.

def NN.Verification.Json.expectField (j : Lean.Json) (k ctx : String) : IO Lean.Json

Extract a required field from a JSON object.

def NN.Verification.Json.readJsonObjectFile (path : String) (ctx : String := "top-level") : IO Lean.Json

Read a JSON artifact and require the top-level value to be an object.

def NN.Verification.Json.optionalField? (j : Lean.Json) (k ctx : String) : IO (Option Lean.Json)

Extract an optional field from a JSON object.

def NN.Verification.Json.expectString (j : Lean.Json) (ctx : String) : IO String

Require a JSON string in an IO parser, preserving contextual error messages.

def NN.Verification.Json.expectNat (j : Lean.Json) (ctx : String) : IO Nat

Require a natural number, accepting either JSON numeric syntax or a decimal string.

def NN.Verification.Json.expectArray (j : Lean.Json) (ctx : String) : IO (Array Lean.Json)

Require a JSON array and return its entries.

def NN.Verification.Json.asNat? (j : Lean.Json) : Option Nat

Parse a Nat from a JSON number or decimal string.

def NN.Verification.Json.asFloat? (j : Lean.Json) : Option Float

Parse a Float from a JSON number or a string containing a JSON number.

def NN.Verification.Json.asFiniteFloat? (j : Lean.Json) : Option Float

Parse a finite Float from a JSON number or a string containing a JSON number.

def NN.Verification.Json.expectFloatE (ctx : String) (j : Lean.Json) : Except String Float

Require a floating-point value in an Except parser.

def NN.Verification.Json.expectFiniteFloatE (ctx : String) (j : Lean.Json) : Except String Float

Require a finite floating-point value in an Except parser.

def NN.Verification.Json.expectFiniteFloatArrayE (ctx : String) (j : Lean.Json) : Except String (Array Float)

Parse a JSON array of finite floats in an Except parser.

structure NN.Verification.Json.BoxRegion : Type

A finite axis-aligned region parsed from a verification artifact.

• dim : Nat

  Declared dimension, or the inferred endpoint-array length when dim is absent.

• lo : Array Float

  Lower coordinate bounds.

• hi : Array Float

  Upper coordinate bounds.

@[implicit_reducible]

instance NN.Verification.Json.instReprBoxRegion : Repr BoxRegion

def NN.Verification.Json.instReprBoxRegion.repr : BoxRegion → Nat → Std.Format

def NN.Verification.Json.BoxRegion.validate (ctx : String) (region : BoxRegion) : Except String Unit

Check the dimensional and ordering invariants of an axis-aligned region.

def NN.Verification.Json.expectBoxRegionE (ctx : String) (j : Lean.Json) : Except String BoxRegion

Parse either {lo, hi} or {center, eps} notation for a finite axis-aligned region.

When dim is absent, it is inferred from the endpoint or center array. When present, it must be a natural number equal to the resulting endpoint lengths. The parser also rejects negative radii, non-finite values, incomplete schemas, and intervals whose lower endpoint exceeds the upper one. Keeping these checks here gives certificate consumers one well-formed region type instead of several subtly different parsers.

def NN.Verification.Json.expectEndpointBoxRegionE (ctx : String) (j : Lean.Json) : Except String BoxRegion

Parse the exact endpoint schema {lo, hi}, with an optional matching dim field.

def NN.Verification.Json.expectFieldFloatE (ctx key : String) (j : Lean.Json) : Except String Float

Extract a floating-point-valued field in an Except parser.

def NN.Verification.Json.expectFieldFiniteFloatE (ctx key : String) (j : Lean.Json) : Except String Float

Extract a finite floating-point-valued field in an Except parser.

def NN.Verification.Json.expectFieldStringE (ctx key : String) (j : Lean.Json) : Except String String

Extract a string-valued field in an Except parser.

def NN.Verification.Json.parseBool? (j : Lean.Json) : Option Bool

Decode a JSON boolean if the value is exactly true or false.

def NN.Verification.Json.expectFloat (j : Lean.Json) (ctx : String) : IO Float

Require a floating-point value, accepting JSON numbers and string-encoded numbers.

def NN.Verification.Json.expectFiniteFloat (j : Lean.Json) (ctx : String) : IO Float

Require a finite floating-point value, accepting JSON numbers and string-encoded numbers.

def NN.Verification.Json.expectBool (j : Lean.Json) (ctx : String) : IO Bool

Require a JSON boolean and report ctx on mismatch.

def NN.Verification.Json.parseFloatArray (j : Lean.Json) : Option (Array Float)

Parse a JSON array of floats.

def NN.Verification.Json.parseFloatMatrix (j : Lean.Json) : Option (Array (Array Float))

Parse a JSON matrix represented as an array of float arrays.

def NN.Verification.Json.expectFloatArray (j : Lean.Json) (ctx : String) : IO (Array Float)

Parse a JSON array of floats with contextual errors.

def NN.Verification.Json.expectFiniteFloatArray (j : Lean.Json) (ctx : String) : IO (Array Float)

Parse a JSON array of finite floats with contextual errors.

def NN.Verification.Json.expectFloatMatrix (j : Lean.Json) (ctx : String) : IO (Array (Array Float))

Parse a JSON matrix of floats with contextual errors.

def NN.Verification.Json.expectFiniteFloatMatrix (j : Lean.Json) (ctx : String) : IO (Array (Array Float))

Parse a JSON matrix whose entries are all finite floats.

def NN.Verification.Json.expectFieldObj (j : Lean.Json) (k ctx : String) : IO Lean.Json

Extract an object-valued field.

def NN.Verification.Json.expectFieldString (j : Lean.Json) (k ctx : String) : IO String

Extract a string-valued field.

def NN.Verification.Json.expectFieldNat (j : Lean.Json) (k ctx : String) : IO Nat

Extract a natural-number-valued field.

def NN.Verification.Json.expectFieldArray (j : Lean.Json) (k ctx : String) : IO (Array Lean.Json)

Extract an array-valued field.

def NN.Verification.Json.optionalFieldArrayD (ctx key : String) (j : Lean.Json) : Except String (Array Lean.Json)

Extract an optional array-valued field in an Except parser, using #[] when absent/null.

def NN.Verification.Json.expectFieldFloatArray (j : Lean.Json) (k ctx : String) : IO (Array Float)

Extract a float-array-valued field.

def NN.Verification.Json.expectFieldFiniteFloatArray (j : Lean.Json) (k ctx : String) : IO (Array Float)

Extract a finite-float-array-valued field.

def NN.Verification.Json.expectFieldFloatMatrix (j : Lean.Json) (k ctx : String) : IO (Array (Array Float))

Extract a float-matrix-valued field.

def NN.Verification.Json.expectFieldFiniteFloatMatrix (j : Lean.Json) (k ctx : String) : IO (Array (Array Float))

Extract a finite-float-matrix-valued field.

def NN.Verification.Json.optionalFieldString? (j : Lean.Json) (k ctx : String) : IO (Option String)

Extract an optional string-valued field.

def NN.Verification.Json.optionalFieldNat? (j : Lean.Json) (k ctx : String) : IO (Option Nat)

Extract an optional natural-number-valued field.

def NN.Verification.Json.optionalFieldFiniteFloat? (j : Lean.Json) (k ctx : String) : IO (Option Float)

Extract an optional finite floating-point-valued field.

def NN.Verification.Json.optionalFieldBool? (j : Lean.Json) (k ctx : String) : IO (Option Bool)

Extract an optional boolean-valued field.

def NN.Verification.Json.expectFormat (j : Lean.Json) (expected : String) (ctx : String := "top-level") : IO Unit

Require a top-level format field to match an expected artifact schema string.

This makes schema checks uniform across verification tools and keeps examples from hand-rolling their own unsupported-format errors.

def NN.Verification.Json.allPairwise (a b : Array Float) (p : Float → Float → Bool) : Bool

Pointwise all on two float arrays of equal length.

def NN.Verification.Json.anyPairwise (a b : Array Float) (p : Float → Float → Bool) : Bool

Pointwise any on two float arrays of equal length.