Arb oracle (python-flint) integration

This module provides a small Lean wrapper around an external Arb/FLINT process:

• spawn python to run NN/Floats/Arb/arb_oracle.py,
• parse its JSON output,
• expose the result in a structured way (including an exact Rat enclosure reconstructed from Arb's mid_rad_10exp integers).

Trust boundary: this is an oracle. The Lean side parses and packages the returned enclosure; it does not prove the Arb computation itself.

Notes on design

We expose two layers:

• a raw layer returning Lean.Json (runJson, runRequestJson), and
• a typed layer with parsers and request-specific entrypoints (parseResult, run, runExpr, runMLP).

The raw layer is useful for debugging and for experimenting with new request schemas, while the typed layer is nicer for examples and "certificate-like" workflows.

Unary interval queries

Unary mode sends one function name and one input interval to Arb. It is the most direct interface when a proof or example needs a certified enclosure for exp, log, tanh, or a related scalar function.

For more general evaluation (expression ASTs / small MLPs), use the request API further below.

structure TorchLean.Floats.Arb.Query : Type

Unary interval query sent to the Python Arb oracle.

In words: evaluate func over the input interval [lo, hi] using Arb ball arithmetic at the requested precision, and return a rigorous enclosure of the output.

Why endpoints are strings:

• we pass them straight through to Python/Arb without any intermediate parsing in Lean, and
• it avoids accidental loss of precision from Float parsing when writing examples.

• func : String

  Unary function name (e.g. "tanh", "exp", "log").

• lo : String

  Lower endpoint of the input interval, as a decimal string.

• hi : String

  Upper endpoint of the input interval, as a decimal string.

• precBits : Nat

  Working precision (in bits) used inside Arb.

• digits : Nat

  Number of decimal digits used in printed endpoints.

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprQuery : Repr Query

def TorchLean.Floats.Arb.instReprQuery.repr : Query → Nat → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedQuery : Inhabited Query

structure TorchLean.Floats.Arb.MidRad10Exp : Type

Arb mid_rad_10exp ball encoding.

In words: this represents the exact rational enclosure [(mid - rad) * 10^exp, (mid + rad) * 10^exp].

The Python oracle emits mid, rad, and exp as strings (then we parse them into Int) to avoid JSON integer-size limitations.

• mid : Int

  Midpoint integer.

• rad : Int

  Radius integer (nonnegative for well-formed payloads).

• exp : Int

  Base-10 exponent scaling both mid and rad.

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprMidRad10Exp : Repr MidRad10Exp

def TorchLean.Floats.Arb.instReprMidRad10Exp.repr : MidRad10Exp → Nat → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedMidRad10Exp : Inhabited MidRad10Exp

structure TorchLean.Floats.Arb.Result : Type

Typed result for a unary query.

We keep both:

• the raw decimal endpoints (outLo/outHi) for logs, and
• the exact MidRad10Exp ball (outputBall) that can be converted into exact Rat bounds.

• func : String

  Echoed func name.

• precBits : Nat

  Working precision (bits) used by Arb.

• digits : Nat

  Decimal digits used in printed endpoints.

• inputBall : MidRad10Exp

  Input interval as an Arb ball (exact integer encoding).

• outputBall : MidRad10Exp

  Output interval as an Arb ball (exact integer encoding).

• outLo : String

  Lower endpoint as a decimal string (human-friendly).

• outHi : String

  Upper endpoint as a decimal string (human-friendly).

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprResult : Repr Result

def TorchLean.Floats.Arb.instReprResult.repr : Result → Nat → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedResult : Inhabited Result

General request API (kind = "expr" / "mlp")

The Python oracle supports JSON requests (see NN/Floats/Arb/arb_oracle.py):

• kind = "expr": evaluate a small, whitelisted expression language over Arb balls.
• kind = "mlp": evaluate a small feedforward MLP given weights/biases/activations, over a box input.

These are still oracle calls; they let us move beyond one unary op while keeping the external computation boundary explicit.

structure TorchLean.Floats.Arb.ExprResult : Type

Typed result for an expr request.

In words: an enclosure of a small expression AST evaluated over a box of interval variables.

• precBits : Nat

  Working precision (bits) used by Arb.

• digits : Nat

  Decimal digits used in printed endpoints.

• outputBall : MidRad10Exp

  Output enclosure encoded as mid_rad_10exp.

• outLo : String

  Lower decimal endpoint of the enclosure.

• outHi : String

  Upper decimal endpoint of the enclosure.

def TorchLean.Floats.Arb.instReprExprResult.repr : ExprResult → Nat → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprExprResult : Repr ExprResult

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedExprResult : Inhabited ExprResult

structure TorchLean.Floats.Arb.MLPResult : Type

Typed result for an mlp request.

The output is a vector of per-output-coordinate enclosures (ball, lo, hi).

• precBits : Nat

  Working precision (bits) used by Arb.

• digits : Nat

  Decimal digits used in printed endpoints.

• output : Array (MidRad10Exp × String × String)

  Per-output enclosures, each paired with decimal endpoint strings.

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprMLPResult : Repr MLPResult

def TorchLean.Floats.Arb.instReprMLPResult.repr : MLPResult → Nat → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedMLPResult : Inhabited MLPResult

def TorchLean.Floats.Arb.oracleScriptPath : String

Relative path to the Python oracle entrypoint script (used in all invocation modes).

def TorchLean.Floats.Arb.resolvePythonCmd (pythonCmd : String) : IO String

Resolve which Python executable to use.

In words: if the environment variable TORCHLEAN_ARB_PY is set, use it; otherwise fall back to the provided pythonCmd (default: "python3").

def TorchLean.Floats.Arb.runPythonJson (pythonCmd : String) (args : Array String) : IO Lean.Json

Run the oracle script as a subprocess and parse its stdout as JSON.

This is the shared IO boundary used by both unary queries and general JSON requests.

def TorchLean.Floats.Arb.jsonToString (j : Lean.Json) : Except String String

Internal JSON helper: interpret a JSON string as a String, or return an error.

def TorchLean.Floats.Arb.jsonToNat (j : Lean.Json) : Except String Nat

Internal JSON helper: interpret a JSON number as a Nat, or return an error.

The oracle schema uses Nats only for metadata fields such as precision/digits.

def TorchLean.Floats.Arb.jsonToIntFromStringKey (o : Lean.Json) (k : String) : Except String Int

Internal JSON helper: read an integer encoded as a decimal string from the given object field.

The oracle emits mid/rad/exp as strings to avoid JSON integer-size limitations.

def TorchLean.Floats.Arb.parseMidRad10Exp (j : Lean.Json) : Except String MidRad10Exp

Parse an Arb mid_rad_10exp object into MidRad10Exp.

In words: this reads the exact integer encoding of an interval ball.

def TorchLean.Floats.Arb.MidRad10Exp.toRatBounds (m : MidRad10Exp) : Rat × Rat

Convert a MidRad10Exp ball into an exact rational enclosure.

In words: if the payload encodes mid ± rad scaled by 10^exp, then toRatBounds returns the pair ((mid - rad) * 10^exp, (mid + rad) * 10^exp) as exact rationals.

def TorchLean.Floats.Arb.Query.toArgs (q : Query) : Array String

Render a unary Query into the CLI arguments expected by arb_oracle.py in unary mode.

This is separated out so tools can log or override arguments more easily.

def TorchLean.Floats.Arb.runJson (q : Query) (pythonCmd : String := "python3") : IO Lean.Json

Run a unary Query via the Python oracle and return the raw JSON payload.

This only checks that:

• the process exits successfully, and
• the output parses as JSON.

Use parseResult if you want the typed Result.

def TorchLean.Floats.Arb.parseCtx (j : Lean.Json) : Except String (Nat × Nat)

Parse the ctx object shared by all oracle responses.

In words: extract (precBits, digits) from the payload metadata.

def TorchLean.Floats.Arb.parseBallField (o : Lean.Json) : Except String MidRad10Exp

Internal helper: parse a ball field (in mid_rad_10exp format) from an object.

This is used by both unary results and request-mode results.

def TorchLean.Floats.Arb.parseLoHi (o : Lean.Json) : Except String (String × String)

Internal helper: parse (lo, hi) endpoint strings from an object.

The oracle includes both human-friendly decimal endpoints and exact integer ball encodings.

def TorchLean.Floats.Arb.parseBallLoHi (o : Lean.Json) : Except String (MidRad10Exp × String × String)

Internal helper: parse a ball plus decimal (lo, hi) endpoints from an object.

The oracle includes both:

• human-friendly decimal endpoints (lo/hi), and
• an exact mid_rad_10exp ball encoding (ball).

def TorchLean.Floats.Arb.parseResult (j : Lean.Json) : Except String Result

Parse a unary-mode JSON payload into a typed Result.

In words: if the JSON matches the schema emitted by arb_oracle.py --func ..., then parseResult extracts the input/output enclosures and context parameters; otherwise it returns a plain error message.

def TorchLean.Floats.Arb.run (q : Query) (pythonCmd : String := "python3") : IO Result

Run a unary Query and parse the result.

It respects TORCHLEAN_ARB_PY (if set) to choose the Python executable.

def TorchLean.Floats.Arb.ensureTmpDir : IO Unit

Ensure the temp directory used for request files exists.

We write request JSON payloads to .lake/build/tmp/ so they are available for debugging if the oracle subprocess fails or its output cannot be parsed. On success, we delete the file unless TORCHLEAN_ARB_KEEP_TMP is set.

def TorchLean.Floats.Arb.keepTmpRequests : IO Bool

Return true iff request payload files should be kept on disk even on success.

def TorchLean.Floats.Arb.tryRemoveFile (path : System.FilePath) : IO Unit

Best-effort file removal helper (ignore errors).

def TorchLean.Floats.Arb.freshReqPath : IO System.FilePath

Generate a fresh request filepath for an Arb oracle payload.

In words: use the current monotone time in milliseconds plus a random suffix to reduce collisions across concurrent processes.

def TorchLean.Floats.Arb.runRequestJson (req : Lean.Json) (precBits : Nat := 200) (digits : Nat := 50) (pythonCmd : String := "python3") : IO Lean.Json

Run the oracle with a general --request <file.json> payload (returns raw JSON).

This is the entrypoint for the richer request schemas supported by arb_oracle.py, such as:

• kind = "expr" (expression AST evaluation), and
• kind = "mlp" (small feedforward MLP evaluation).

This respects TORCHLEAN_ARB_PY (if set) to choose the Python executable.

def TorchLean.Floats.Arb.parseExprResult (j : Lean.Json) : Except String ExprResult

Parse an expr response payload into ExprResult.

In words: extract the output enclosure and context metadata from the response JSON.

def TorchLean.Floats.Arb.parseMLPResult (j : Lean.Json) : Except String MLPResult

Parse an mlp response payload into MLPResult.

In words: extract the vector of per-coordinate output enclosures and context metadata.

def TorchLean.Floats.Arb.runExpr (vars : List (String × String × String)) (expr : Lean.Json) (precBits : Nat := 200) (digits : Nat := 50) (pythonCmd : String := "python3") : IO ExprResult

Run an expr request and parse the output interval.

In words: evaluate an expression AST over a box of interval variables using Arb ball arithmetic, returning an enclosure of the result.

def TorchLean.Floats.Arb.runMLP (req : Lean.Json) (precBits : Nat := 200) (digits : Nat := 50) (pythonCmd : String := "python3") : IO MLPResult

Run an mlp request (box input + layers) and parse the output vector intervals.

In words: run a small feedforward MLP using ball arithmetic, where the input is a box interval, and return per-output-coordinate enclosures.