Exact scalar encodings for custom computations

Native floats use hardware arithmetic. Configured binary values use their complete interchange words; the device selects compatible native operations or software arithmetic from the format. Wide values are never narrowed through binary64. The packing law concerns Lean values, not the foreign transfer or arithmetic implementation.

def NN.Kernel.Arithmetic.ofOps {α : Type} [Add α] [Sub α] [Mul α] [Div α] [Neg α] [BEq α] [LT α] [LE α] [DecidableLT α] [DecidableLE α] : Arithmetic α

Scalar operations in their original evaluation order, without algebraic reassociation.

inductive NN.Kernel.Precision : Type

Arithmetic representation selected by a scalar type, independently of the execution device.

• native (format : Cuda.Format) : Precision
• binary (format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) : Precision

class NN.Kernel.Scalar (α : Type) : Type

Complete unsigned encodings and their lossless reconstruction.

• precision : Precision
• arithmetic : Arithmetic α

  Operations implemented by the selected GPU representation.

• encode : α → ℕ
• decode : ℕ → α
• decode_encode (x : α) : decode (encode x) = x

@[instance_reducible]

instance NN.Kernel.instScalarFloat32 : Scalar Float32

@[instance_reducible]

instance NN.Kernel.instScalarFloat : Scalar Float

@[instance_reducible]

instance NN.Kernel.instScalarConfigured {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] : Scalar (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))

def NN.Kernel.Precision.bytes : Precision → ℕ

Byte width of one complete value, padded only to a whole number of bytes.

def NN.Kernel.Precision.supportsGpu : Precision → Bool

Whether the custom GPU arithmetic implementation accepts this complete scalar format. This is a type/format capability check, not a claim that a GPU or enough memory is available.

def NN.Kernel.Scalar.pack {α : Type} [TorchLean.Storage α] {shape : Spec.Shape} (scalar : Scalar α) (tensor : TorchLean.Tensor α shape) : Except String ByteArray

Serialize complete scalar words in row-major little-endian order.

def NN.Kernel.Scalar.unpack {α : Type} [TorchLean.Storage α] (scalar : Scalar α) (shape : Spec.Shape) (bytes : ByteArray) : Except String (TorchLean.Tensor α shape)

Decode complete words only after checking the requested shape and byte extent.