CUDA float32 contract

The binary32 path stores values in opaque LibTorch tensors. This module's agreement contracts concern binary32 only; the native tape also supports binary64, without deriving binary64 agreement from these theorems. The Lean proofs do not inspect compiled ATen operations, their library dependencies, or the device. The native backend therefore remains an explicit implementation boundary.

This module keeps that boundary precise:

• ExecFloat.Binary 8 23 is the executable, bit-level reference model for scalar binary32.
• host Float inputs enter the float32 world through FloatLib’s Model.cast, matching the intended "round binary64 host literals to binary32" contract;
• external/native CUDA scalar results are represented only by their raw 32-bit result bits;
• if those native bits agree with the ExecFloat.Binary 8 23 reference op, up to the implementation-defined encoding of NaN, then the existing proved configured binary32 → FP32-on-ℝ theorems apply immediately.

In other words, the proof route is:

native CUDA bits --(explicit agreement assumption / tests / toolchain contract)--> ExecFloat.Binary 8 23 --(proved in Lean)--> FP32 rounding-on-ℝ error bounds.

What is not proved here:

• that a particular compiled CUDA kernel, C compiler, device, libdevice implementation, or cuBLAS version produces the reference bits;
• deterministic ordering for atomic reductions unless the backend uses a fixed reduction tree;
• correct-rounding for transcendental functions that IEEE-754 itself does not specify.

Those are runtime/toolchain assumptions, and the CUDA stress tests are intended to validate them against this reference contract. The primitive-level part of that validation is scripts/checks/cuda.sh parity, which compares cases for the five fields of NativePrimitiveAgreement against compiled host arithmetic and ATen GPU operations, bit for bit. A passing case is evidence for that input and build, not the universally quantified agreement hypothesis. Operator policy settings alone do not supply that hypothesis.

Reference scalar and host conversion

@[reducible, inline]

abbrev Runtime.Autograd.LibTorch.Float32Contract.RefScalar : Type

The scalar reference for CUDA float32 reasoning.

CUDA buffers are opaque to Lean; this is the scalar model we compare their 32-bit elements against.

@[inline]

def Runtime.Autograd.LibTorch.Float32Contract.fromNativeBits (bits : UInt32) : RefScalar

Interpret raw native binary32 bits as the ExecFloat.Binary 8 23 reference scalar.

@[inline]

def Runtime.Autograd.LibTorch.Float32Contract.toNativeBits (x : RefScalar) : UInt32

Extract the binary32 bit pattern used for native/reference comparisons.

@[inline]

def Runtime.Autograd.LibTorch.Float32Contract.fromLeanFloat (x : Float) : RefScalar

Reference meaning of uploading a Lean Float into a CUDA float32 buffer.

Lean Float is binary64. The CUDA buffer path casts host doubles to native float; the reference contract for that cast is round-to-nearest-even binary32, implemented by FloatLib’s Model.cast.

@[simp]

theorem Runtime.Autograd.LibTorch.Float32Contract.toNativeBits_fromNativeBits (bits : UInt32) : toNativeBits (fromNativeBits bits) = bits

Bit patterns survive a round trip through the reference scalar type.

@[simp]

theorem Runtime.Autograd.LibTorch.Float32Contract.fromNativeBits_toNativeBits (x : RefScalar) : fromNativeBits (toNativeBits x) = x

And so do reference scalars through their bits, which is what makes the C boundary lossless: whatever the kernel writes back can be read as the same value we would have computed.

theorem Runtime.Autograd.LibTorch.Float32Contract.fromLeanFloat_eq_cast (x : Float) : fromLeanFloat x = FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.cast FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary64 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (FloatLib.Floats.ExecFloat.Binary.ofFloat x).toModel)

Host Float upload is exactly the FloatLib model cast to the buffer format.

theorem Runtime.Autograd.LibTorch.Float32Contract.fromLeanFloat_bits_eq_cast_bits (x : Float) : toNativeBits (fromLeanFloat x) = (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.cast FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary64 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (FloatLib.Floats.ExecFloat.Binary.ofFloat x).toModel)).toBits32

The upload bit pattern is the bit pattern of the reference model cast.

theorem Runtime.Autograd.LibTorch.Float32Contract.fromNativeBits_toBits (x : Float32) : fromNativeBits x.toBits = FloatLib.Floats.ExecFloat.Binary.ofFloat32 x

Reinterpreting native Float32 bits agrees with FloatLib's native-value conversion.

Abstract native scalar semantics

structure Runtime.Autograd.LibTorch.Float32Contract.NativePrimitiveBits : Type

Abstract result bits for native CUDA scalar primitives.

This structure provides a bit-by-bit comparison point between the FFI/runtime implementation and the ExecFloat.Binary 8 23 reference. It makes no claim that Lean proves the CUDA implementation correct. Rank-one and higher-rank tensor kernels lift the comparison elementwise, except for reductions whose order must also be specified.

• addBits : RefScalar → RefScalar → UInt32
• mulBits : RefScalar → RefScalar → UInt32
• divBits : RefScalar → RefScalar → UInt32
• fmaBits : RefScalar → RefScalar → RefScalar → UInt32
• sqrtBits : RefScalar → UInt32

def Runtime.Autograd.LibTorch.Float32Contract.AgreeUpToNaN (native reference : UInt32) : Prop

Agreement between a native result and the reference result, in the sense the theorems below need: either the two bit patterns are equal, or both encode NaN.

The relation permits different NaN encodings while requiring identical bits for every non-NaN result, including signed zeros. scripts/checks/cuda.sh parity tests this relation against the linked native backend and counts NaN encoding differences separately.

Every error bound below requires a finite result. That hypothesis rules out the second disjunct, so allowing different NaN encodings does not weaken those finite-result bounds.

theorem Runtime.Autograd.LibTorch.Float32Contract.AgreeUpToNaN.eq_of_isFinite {native reference : UInt32} (h : AgreeUpToNaN native reference) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits native) = true) : native = reference

A finite native result pins the bits exactly, because the NaN case cannot apply to it.

structure Runtime.Autograd.LibTorch.Float32Contract.NativePrimitiveAgreement (native : NativePrimitiveBits) : Prop

The trusted/validated CUDA scalar agreement assumption.

For a concrete CUDA build, these fields are what parity tests, compiler flags, and backend policy are checking: native result bits match the executable ExecFloat.Binary 8 23 reference for primitive float32 ops, up to the encoding of NaN.

• add_bits (x y : RefScalar) : AgreeUpToNaN (native.addBits x y) (toNativeBits (FloatLib.Floats.ExecFloat.add x y))
• mul_bits (x y : RefScalar) : AgreeUpToNaN (native.mulBits x y) (toNativeBits (FloatLib.Floats.ExecFloat.mul x y))
• div_bits (x y : RefScalar) : AgreeUpToNaN (native.divBits x y) (toNativeBits (FloatLib.Floats.ExecFloat.div x y))
• fma_bits (x y z : RefScalar) : AgreeUpToNaN (native.fmaBits x y z) (toNativeBits ((fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5))) => left.fma right addend) x y z))
• sqrt_bits (x : RefScalar) : AgreeUpToNaN (native.sqrtBits x) (toNativeBits ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5))) => value.sqrt) x))

theorem Runtime.Autograd.LibTorch.Float32Contract.ref_ext {x y : RefScalar} (h : toNativeBits x = toNativeBits y) : x = y

Reference scalars are determined by their bits, NaN payloads included.

This is the extensionality principle the kernel proofs use: agreeing bitwise with the C result is enough to conclude agreement as values, with no float equality anywhere in the argument.

From bits to values

Each of these says: if the native result is finite, it is the reference value. Finiteness is what turns the NaN-tolerant contract into an equation, and every error bound below needs it anyway, so the hypothesis costs nothing in practice.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_add_eq_reference_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.addBits x y)) = true) : fromNativeBits (native.addBits x y) = FloatLib.Floats.ExecFloat.add x y

Native addition is the reference value when its result is finite and the contract holds.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_mul_eq_reference_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.mulBits x y)) = true) : fromNativeBits (native.mulBits x y) = FloatLib.Floats.ExecFloat.mul x y

Native multiplication is the reference value when its result is finite and the contract holds.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_div_eq_reference_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.divBits x y)) = true) : fromNativeBits (native.divBits x y) = FloatLib.Floats.ExecFloat.div x y

Native division is the reference value when its result is finite and the contract holds.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_fma_eq_reference_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y z : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.fmaBits x y z)) = true) : fromNativeBits (native.fmaBits x y z) = (fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5))) => left.fma right addend) x y z

Native fused multiply-add is the reference value when its result is finite and the contract holds.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_sqrt_eq_reference_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.sqrtBits x)) = true) : fromNativeBits (native.sqrtBits x) = (fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := RefScalar._proof_1, fracWidth := 23, fracWidth_pos := RefScalar._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := RefScalar._proof_3, exponentBias_le_maxFinite := RefScalar._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RefScalar._proof_1 RefScalar._proof_2 RefScalar._proof_3 RefScalar._proof_4) (1 + 8 + 23) RefScalar._proof_5))) => value.sqrt) x

Native square root is the reference value when its result is finite and the contract holds.

Inheriting the proved configured binary32 → FP32 bounds

theorem Runtime.Autograd.LibTorch.Float32Contract.native_add_abs_error_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.addBits x y)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (fromNativeBits (native.addBits x y))).toReal - ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

If native CUDA addition matches the ExecFloat.Binary 8 23 result bits and the result is finite, then it has the standard binary32 half-ULP absolute error bound against real addition.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_mul_abs_error_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.mulBits x y)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (fromNativeBits (native.mulBits x y))).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

If native CUDA multiplication matches the ExecFloat.Binary 8 23 result bits and the result is finite, then it has the standard binary32 half-ULP absolute error bound against real multiplication.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_div_abs_error_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.divBits x y)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (fromNativeBits (native.divBits x y))).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

If native CUDA division matches the ExecFloat.Binary 8 23 result bits and the result is finite, then it has the standard binary32 half-ULP absolute error bound against real division.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_fma_abs_error_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x y z : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.fmaBits x y z)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (fromNativeBits (native.fmaBits x y z))).toReal - ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)

If native CUDA FMA matches the ExecFloat.Binary 8 23 result bits and the result is finite, then it has the standard binary32 half-ULP absolute error bound against real x*y+z.

theorem Runtime.Autograd.LibTorch.Float32Contract.native_sqrt_abs_error_of_isFinite {native : NativePrimitiveBits} (h : NativePrimitiveAgreement native) (x : RefScalar) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (fromNativeBits (native.sqrtBits x)) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (fromNativeBits (native.sqrtBits x))).toReal - √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

If native CUDA square root matches the ExecFloat.Binary 8 23 result bits and the result is finite, then it has the standard binary32 half-ULP absolute error bound against real square root.