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.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.expectObject (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 ℕ

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 ℕ

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.parseFiniteFloat (ctx : String) (j : Lean.Json) : Except String Float

Parse a finite floating-point value with contextual errors.

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

Parse a JSON array of finite floats with contextual errors.

def NN.Verification.Json.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"

Fraction strings represent arbitrary rationals without a floating-point conversion, including values such as 1/3 that cannot be written as a finite JSON decimal.

structure NN.Verification.Json.BoxRegion : Type

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

• dim : ℕ

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

• lo : Array Float

  Lower coordinate bounds.

• hi : Array Float

  Upper coordinate bounds.

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

@[instance_reducible]

instance NN.Verification.Json.instReprBoxRegion : Repr BoxRegion

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.parseBoxRegion (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. Numbers are first decoded to host binary64. The {center, eps} arithmetic rounds outward from those decoded values, not from the original exact JSON decimals. Endpoint notation uses the decoded values directly. The parser 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.parseEndpointBoxRegion (ctx : String) (j : Lean.Json) : Except String BoxRegion

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

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

Parse a finite floating-point-valued field with contextual errors.

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

Parse a string-valued field with contextual errors.

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.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.expectFiniteFloatArray (j : Lean.Json) (ctx : String) : IO (Array Float)

Require a JSON array of finite 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.expectFieldObject (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 ℕ

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.fieldArrayOrEmpty (ctx key : String) (j : Lean.Json) : Except String (Array Lean.Json)

Extract an array field, using #[] when it is absent or null.

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.optionalFieldNat? (j : Lean.Json) (k ctx : String) : IO (Option ℕ)

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.