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 runtime-selected trainer.open and trainer.train paths accept the two real modes; trainer.openTyped chooses its scalar directly on CPU. 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.

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

Convert a binary64 value toward -∞ (up = false) or +∞ (up = true).

This requires roundForValidation to report the converted scalar's value faithfully in binary64, as it does for the native and configured binary32 instances. Move the source away from x until its conversion lands on the requested side, falling back to that side's infinity after 64 attempts. Custom instances whose validation hook is only the default identity do not supply this guarantee.

@[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.instFromFloatBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode : FromFloat (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instFromFloatBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_1 instFromFloatBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_2 instFromFloatBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_3 instFromFloatBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode._proof_4)

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

@[instance_reducible, instance 100]

instance TorchLean.Runtime.configuredBinaryFromFloat {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] : FromFloat (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))

Round the exact binary64 source value once into any configured binary format.

The binary32 specialization above retains its native conversion path. Validation converts the rounded destination value back to binary64, exposing overflow, underflow, and domain changes. Explicit scalar-valued tensors and state do not use this conversion.

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

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

@[instance_reducible]

instance TorchLean.Runtime.instReprArithmetic : Repr Arithmetic

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