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 small parsing functions (parseResult) and convenience wrappers (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 queries (compatibility)

The original Lean integration called the oracle in “unary” mode via --func, --lo, --hi. This API remains because it is convenient for quick demos.

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 demos.

• 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

def TorchLean.Floats.Arb.instInhabitedQuery.default : 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

def TorchLean.Floats.Arb.instInhabitedMidRad10Exp.default : 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

def TorchLean.Floats.Arb.instInhabitedResult.default : Result

@[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.

@[implicit_reducible]

instance TorchLean.Floats.Arb.instReprExprResult : Repr ExprResult

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

@[implicit_reducible]

instance TorchLean.Floats.Arb.instInhabitedExprResult : Inhabited ExprResult

def TorchLean.Floats.Arb.instInhabitedExprResult.default : 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 human-readable endpoints.

@[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.instInhabitedMLPResult.default : 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 human-readable error message.

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

Run a unary Query and parse the result.

This is the convenience wrapper most demos should use.

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 temporary filepath for a request 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.

This is a convenience wrapper around runRequestJson with kind = "expr".

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.

This is a convenience wrapper around runRequestJson with kind = "mlp".