Certified native pointwise kernels

Packed scalar types can replace the generic output-building loop with one operation-specific native loop while retaining the ordinary pointwise tensor definition as their proof-visible semantics. Mixed packed byte/float addition also fuses scalar promotion into the output loop.

Reference bodies and their native twins

Each proof-visible kernel has an @[extern] twin that calls the reference body. A @[csimp] lemma selects the twin during compilation; its borrow annotations match the C entry point. Keeping one Lean body prevents the two models from drifting apart. As with Array.zipWith, buffer operations truncate to the shorter input; tensor callers already have matching lengths by their shapes. The C implementation's agreement with these models remains an FFI trust boundary.

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferAdd (left right : FloatArray) : FloatArray

Proof-visible packed floating-point addition.

@[extern torchlean_float_array_add]

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferAddNative (left right : FloatArray) : FloatArray

Native packed floating-point addition, compiled to one C loop.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferAdd_eq_native : floatBufferAdd = floatBufferAddNative

Compile packed floating-point addition to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferSub (left right : FloatArray) : FloatArray

Proof-visible packed floating-point subtraction.

@[extern torchlean_float_array_sub]

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferSubNative (left right : FloatArray) : FloatArray

Native packed floating-point subtraction, compiled to one C loop.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferSub_eq_native : floatBufferSub = floatBufferSubNative

Compile packed floating-point subtraction to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferMul (left right : FloatArray) : FloatArray

Proof-visible packed floating-point multiplication.

@[extern torchlean_float_array_mul]

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferMulNative (left right : FloatArray) : FloatArray

Native packed floating-point multiplication, compiled to one C loop.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferMul_eq_native : floatBufferMul = floatBufferMulNative

Compile packed floating-point multiplication to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferDiv (left right : FloatArray) : FloatArray

Proof-visible packed floating-point division.

@[extern torchlean_float_array_div]

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferDivNative (left right : FloatArray) : FloatArray

Native packed floating-point division, compiled to one C loop.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferDiv_eq_native : floatBufferDiv = floatBufferDivNative

Compile packed floating-point division to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.byteFloatBufferAdd (left : ByteArray) (right : FloatArray) : FloatArray

Proof-visible fused byte promotion and floating-point addition.

@[extern torchlean_byte_float_array_add]

def TorchLean.Tensor.Internal.Elab.Impl.byteFloatBufferAddNative (left : ByteArray) (right : FloatArray) : FloatArray

Native fused byte promotion and floating-point addition.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.byteFloatBufferAdd_eq_native : byteFloatBufferAdd = byteFloatBufferAddNative

Compile fused byte/float addition to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.floatByteBufferAdd (left : FloatArray) (right : ByteArray) : FloatArray

Proof-visible fused floating-point and promoted-byte addition.

@[extern torchlean_float_byte_array_add]

def TorchLean.Tensor.Internal.Elab.Impl.floatByteBufferAddNative (left : FloatArray) (right : ByteArray) : FloatArray

Native fused floating-point and promoted-byte addition.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatByteBufferAdd_eq_native : floatByteBufferAdd = floatByteBufferAddNative

Compile fused float/byte addition to one native loop.

def TorchLean.Tensor.Internal.Elab.Impl.nativeAdd {shape : Shape} (left right : Rep Float shape) : Rep Float shape

Add two packed Float tensors in one preallocated native loop.

Lean evaluation uses the ordinary packed-array model. Generated code calls torchlean_float_array_add.

def TorchLean.Tensor.Internal.Elab.Impl.nativeSub {shape : Shape} (left right : Rep Float shape) : Rep Float shape

Subtract two packed Float tensors in one preallocated native loop.

def TorchLean.Tensor.Internal.Elab.Impl.nativeMul {shape : Shape} (left right : Rep Float shape) : Rep Float shape

Multiply two packed Float tensors in one preallocated native loop.

def TorchLean.Tensor.Internal.Elab.Impl.nativeDiv {shape : Shape} (left right : Rep Float shape) : Rep Float shape

Divide two packed Float tensors in one preallocated native loop.

def TorchLean.Tensor.Internal.Elab.Impl.nativePromoteLeftAdd {shape : Shape} (left : Rep UInt8 shape) (right : Rep Float shape) : Rep Float shape

Promote packed bytes and add them to packed floats in one native output loop.

The proof-visible definition is the canonical promoted pointwise operation.

def TorchLean.Tensor.Internal.Elab.Impl.nativePromoteRightAdd {shape : Shape} (left : Rep Float shape) (right : Rep UInt8 shape) : Rep Float shape

Add packed floats to promoted packed bytes in one native output loop.

Operand order remains explicit so IEEE exceptional behavior matches scalar Float addition exactly.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeAdd_data {shape : Shape} (left right : Rep Float shape) : (nativeAdd left right).data = Array.zipWith (fun (x1 x2 : Float) => x1 + x2) left.data right.data

The ordinary array observation of packed addition is pointwise addition.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeSub_data {shape : Shape} (left right : Rep Float shape) : (nativeSub left right).data = Array.zipWith (fun (x1 x2 : Float) => x1 - x2) left.data right.data

The ordinary array observation of packed subtraction is pointwise subtraction.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeMul_data {shape : Shape} (left right : Rep Float shape) : (nativeMul left right).data = Array.zipWith (fun (x1 x2 : Float) => x1 * x2) left.data right.data

The ordinary array observation of packed multiplication is pointwise multiplication.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeDiv_data {shape : Shape} (left right : Rep Float shape) : (nativeDiv left right).data = Array.zipWith (fun (x1 x2 : Float) => x1 / x2) left.data right.data

The ordinary array observation of packed division is pointwise division.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativePromoteLeftAdd_data {shape : Shape} (left : Rep UInt8 shape) (right : Rep Float shape) : (nativePromoteLeftAdd left right).data = Array.zipWith (fun (x : UInt8) (y : Float) => x.toFloat + y) left.data right.data

The ordinary array observation of byte/float addition includes promotion.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativePromoteRightAdd_data {shape : Shape} (left : Rep Float shape) (right : Rep UInt8 shape) : (nativePromoteRightAdd left right).data = Array.zipWith (fun (x : Float) (y : UInt8) => x + y.toFloat) left.data right.data

The ordinary array observation of float/byte addition includes promotion.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeAdd_apply {shape : Shape} (left right : Rep Float shape) (coordinate : Coord shape) : (nativeAdd left right).get coordinate = left.get coordinate + right.get coordinate

Native packed addition has the canonical coordinate semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeSub_apply {shape : Shape} (left right : Rep Float shape) (coordinate : Coord shape) : (nativeSub left right).get coordinate = left.get coordinate - right.get coordinate

Native packed subtraction has the canonical coordinate semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeMul_apply {shape : Shape} (left right : Rep Float shape) (coordinate : Coord shape) : (nativeMul left right).get coordinate = left.get coordinate * right.get coordinate

Native packed multiplication has the canonical coordinate semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeDiv_apply {shape : Shape} (left right : Rep Float shape) (coordinate : Coord shape) : (nativeDiv left right).get coordinate = left.get coordinate / right.get coordinate

Native packed division has the canonical coordinate semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativePromoteLeftAdd_apply {shape : Shape} (left : Rep UInt8 shape) (right : Rep Float shape) (coordinate : Coord shape) : (nativePromoteLeftAdd left right).get coordinate = (left.get coordinate).toFloat + right.get coordinate

Fused byte/float addition has the canonical promoted semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Elab.Impl.nativePromoteRightAdd_apply {shape : Shape} (left : Rep Float shape) (right : Rep UInt8 shape) (coordinate : Coord shape) : (nativePromoteRightAdd left right).get coordinate = left.get coordinate + (right.get coordinate).toFloat

Fused float/byte addition has the canonical promoted semantics.