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

Require a floating-point value in an Except parser.

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

Parse a JSON matrix of floats with contextual errors.

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

Extract a 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.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.all2 (a b : Array Float) (p : Float → Float → Bool) : Bool

Pointwise all on two float arrays of equal length.

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

Pointwise any on two float arrays of equal length.