Typed reference execution

Binary arithmetic reuses FloatLib at the declared precision. Boolean and fixed-width integer values can also pass through the shared storage-only tensor operations. Integers of any positive width use Lean's BitVec; their signedness remains in DType, rather than in a second carrier. Integers also implement PyTorch's integer pointwise operators: two's-complement negation, truncating and flooring division, and powers with wrapping multiplication. Other integer arithmetic is not inferred from the representation. Integers and Booleans convert to binary formats by rounding their exact value once; no other cross-type conversion is implemented.

Element words are unsigned, including signed integer encodings. Boolean words are canonically zero or one. Loading rejects excessive words, invalid descriptors and incompatible tensor sizes; Reference.read_write proves that decoding a valid word does not change its encoding.

This interpreter is a software reference, not a proof of XLA or LibTorch execution. Other element representations and operations still need implementations before they can run.

@[reducible, inline]

abbrev NN.IR.Reference.scalar : DType → Type

Configured binary values, Boolean values, and arbitrary-width integer bit vectors.

def NN.IR.Reference.supported (dtype : DType) : Bool

Whether this reference implements a valid element representation.

def NN.IR.Reference.read (dtype : DType) : ℕ → Except String (scalar dtype)

Decode one complete element word, rejecting rather than truncating excessive bits.

def NN.IR.Reference.write (dtype : DType) : scalar dtype → Except String ℕ

Encode one element without interpreting signed integer words as host floats.

def NN.IR.Reference.integerToBinary (target : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (value : ℤ) : Binary.Scalar target × FloatLib.Floats.ExecFloat.ConversionStatus

Round an exact integer once to a binary format, reporting inexactness and overflow.

def NN.IR.Reference.cast (source target : DType) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (value : scalar source) : Except String (scalar target × FloatLib.Floats.ExecFloat.ConversionStatus)

Reuse directed binary conversion; integers and Booleans round their exact value once.

Other nonbinary conversions require identical types. Binary conversions still use FloatLib when the formats are equal, since exceptional-value handling and flags belong to the conversion semantics, not to a tensor relabeling.

theorem NN.IR.Reference.read_write (dtype : DType) (word : ℕ) (value : scalar dtype) (h : read dtype word = Except.ok value) : write dtype value = Except.ok word

A successfully decoded element retains its entire original word on encoding.

@[irreducible]

def NN.IR.Reference.powWrapping {width : ℕ} (base : BitVec width) (exponent : ℕ) : BitVec width

Two's-complement power by repeated squaring, the loop of PyTorch's powi_impl.

def NN.IR.Reference.integerPointwise (signed : Bool) (width : ℕ) : Spec.PointwiseTable (BitVec width)

PyTorch's integer meanings of the pointwise operators.

Negation and powers wrap in two's complement. Division by zero is an error, as PyTorch raises RuntimeError: ZeroDivisionError. The most negative value divided by -1 wraps to itself, which PyTorch returns in flooring division and in truncating division up to 16 bits; its truncating division of 32- and 64-bit integers traps there with SIGFPE. A negative exponent gives 1 for base 1, ±1 for base -1 and 0 otherwise, as PyTorch's powi does for tensor exponents. clamp_min returns the bound where the operand is below it, as eager PyTorch does for a scalar bound. True division, rsqrt, erf and GELU are absent: PyTorch promotes integer operands to floating point for them, so a frontend inserts explicit casts.

def NN.IR.Reference.pointwise (dtype : DType) : Spec.PointwiseTable (scalar dtype)

Pointwise operators of element types without an arithmetic dictionary.

theorem NN.IR.Reference.cast_binary_value (source target : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (value : Binary.Scalar source) (converted : Binary.Scalar target) (flags : FloatLib.Floats.ExecFloat.ConversionStatus) (h : cast (DType.binary source) (DType.binary target) rounding value = Except.ok (converted, flags)) : FloatLib.Floats.ExecFloat.Binary.toModel converted = FloatLib.Floats.Formats.BinaryInterchange.Model.cast source target (FloatLib.Floats.ExecFloat.Binary.toModel value) rounding

The binary part of reference conversion satisfies the same FloatLib specification.

def NN.IR.Interpreter.reference : Interpreter

Binary numerical evaluation and storage-only Boolean/arbitrary-width integer evaluation.

def NN.IR.Reference.load (dtype : DType) (shape : Spec.Shape) (words : Array ℕ) : Except String Interpreter.reference.Value

Load a typed tensor from complete element words, checking its type, size and word ranges.

def NN.IR.Reference.words (value : Interpreter.reference.Value) : Except String (Array ℕ)

Complete element words of a typed tensor, retaining binary special values and integer bits.