Runtime Arithmetic

Runtime commands may choose native binary32, reference IEEE binary32, or complex arithmetic. Arithmetic records that semantic choice. FromFloat supplies conversion from Lean binary64 Float literals and scalar-specific rounding for parameter validation.

The generic runtime dispatcher supports all three modes. The public supervised trainer accepts the two real modes. Explicit complex training uses autograd.complex.grad for a real objective and nn.sgdStep on complex state; its predictions and Checkpoint.State retain both components.

Model definitions remain polymorphic over the existing Context α interface. The arithmetic choice does not replace that mathematical interface; it selects a concrete executable element representation that satisfies it. Proof-only models such as ℝ and rounded-real binary32 are selected directly in theorems rather than through a command-line flag.

class TorchLean.Runtime.FromFloat (α : Type) : Type

Conversion from Lean Float constants into a selected runtime arithmetic representation.

• ofFloat : Float → α

  Convert a Lean binary64 Float literal into this runtime element representation.

• roundForValidation : Float → Float

  Represent the rounding of ofFloat in binary64 for parameter-domain checks.

  The default validates only the supplied binary64 value, preserving custom scalar instances. Finite-precision instances override this to reject values that leave the required domain after conversion. This capability needs no arithmetic or order operations from Context.

def TorchLean.Runtime.ofFloat {α : Type} [FromFloat α] (x : Float) : α

Convert a Lean Float literal into a TorchLean runtime arithmetic representation.

@[instance_reducible]

instance TorchLean.Runtime.instFromFloatFloat : FromFloat Float

Float values inject into the same type by identity.

@[instance_reducible]

instance TorchLean.Runtime.instFromFloatFloat32 : FromFloat Float32

Round binary64 literals to Lean's native binary32 representation.

@[instance_reducible]

instance TorchLean.Runtime.instFromFloatBinaryOfNatNatIeeeDefaultBias : FromFloat (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instFromFloatBinaryOfNatNatIeeeDefaultBias._proof_1 instFromFloatBinaryOfNatNatIeeeDefaultBias._proof_2 instFromFloatBinaryOfNatNatIeeeDefaultBias._proof_3 instFromFloatBinaryOfNatNatIeeeDefaultBias._proof_4)

Inject binary64 literals into the executable IEEE-754 binary32 backend.

@[instance_reducible]

instance TorchLean.Runtime.instFromFloatDualOfZero {α : Type} [FromFloat α] [Zero α] : FromFloat (Runtime.Autograd.Model.Dual α)

Inject binary64 literals into the dual-number backend used by the runtime autograd engine.

We interpret a literal as a primal value with zero tangent/adjoint component.

@[instance_reducible]

instance TorchLean.Runtime.instFromFloatComplexOfZero {α : Type} [FromFloat α] [Zero α] : FromFloat (Complex α)

Inject binary64 literals into TorchLean's complex representation with zero imaginary part.

inductive TorchLean.Runtime.Arithmetic : Type

Arithmetic semantics for runnable executables.

This is a runtime selection mechanism used by example programs; the core library itself is parametric in the element type α.

Unlike a PyTorch per-tensor dtype, this choice fixes one arithmetic semantics for the complete run:

• .native uses Lean's native Float32 operations on CPU and binary32 CUDA storage on GPU,
• .ieee uses FloatLib's configured software IEEE-754 binary32 arithmetic,
• .complex uses TorchLean's complex representation with binary32 real and imaginary components.

• native : Arithmetic
• ieee : Arithmetic
• complex : Arithmetic

@[instance_reducible]

instance TorchLean.Runtime.instReprArithmetic : Repr Arithmetic

def TorchLean.Runtime.instReprArithmetic.repr : Arithmetic → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Runtime.instDecidableEqArithmetic : DecidableEq Arithmetic

def TorchLean.Runtime.Arithmetic.cliName : Arithmetic → String

Stable spelling used by command-line flags.

def TorchLean.Runtime.Arithmetic.log : Arithmetic → IO Unit

Log a short description of the selected arithmetic semantics.

@[instance_reducible]

instance TorchLean.Runtime.Arithmetic.instToString : ToString Arithmetic

def TorchLean.Runtime.Arithmetic.parse (value : String) : Except String Arithmetic

Parse the value of --arithmetic.

def TorchLean.Runtime.Arithmetic.parseAndStrip (arguments : List String) (default : Arithmetic := native) : Except String (Arithmetic × List String)

Parse and remove --arithmetic, using default when the flag is absent.

def TorchLean.Runtime.Arithmetic.withRuntime (arithmetic : Arithmetic) (continuation : {α : Type} → [Storage α] → [Context α] → [ToString α] → [FromFloat α] → IO Unit) : IO Unit

Run continuation under the type selected by arithmetic.