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 α

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

Parse a JSON string.

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

Parse a JSON natural number.

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

Parse a JSON array.

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.parseBool? (j : Lean.Json) : Option Bool

Parse a JSON boolean.

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

Parse a JSON float.

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

Parse a JSON boolean.

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

Parse a JSON array of floats.

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

Extract a float-array-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.