Certified native finite loops

Generated tensor kernels use these primitives when a static traversal length fits every Lean target. The executable loops carry USize counters, while their theorems identify the results with standard Fin.foldl and Array.ofFn semantics.

This module is operation-independent. Rearrangement, repetition, reduction, packing, unpacking, and einsum all share the same traversal boundary.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfFn {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (values : (index : USize) → index.toNat < length → α) : Storage.Buffer α

Fill the physical buffer selected for α in increasing native-index order.

The storage dictionary is specialized at each scalar type. For Float, this loop therefore allocates and pushes directly into an unboxed FloatArray.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfFn_toArray {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (nativeValues : (index : USize) → index.toNat < length → α) (values : Fin length → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < length), nativeValues index hIndex = values ⟨index.toNat, hIndex⟩) : Storage.toArray (nativeBufferOfFn length bound hBound nativeValues) = Array.ofFn values

The native physical-buffer builder observes as Array.ofFn when its callback agrees with the semantic finite-index function.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfFn_size {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (values : (index : USize) → index.toNat < length → α) : Storage.size (nativeBufferOfFn length bound hBound values) = length

The native physical-buffer builder creates the requested scalar count.

theorem TorchLean.Storage.toArray_gather {α : Type u} [storage : Storage α] (source : Buffer α) (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (sourceIndices : (index : USize) → index.toNat < length → USize) (hSourceIndices : ∀ (index : USize) (hIndex : index.toNat < length), (sourceIndices index hIndex).toNat < size source) (values : Fin length → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < length), uget source (sourceIndices index hIndex) ⋯ = values ⟨index.toNat, hIndex⟩) : toArray (gather source length bound hBound sourceIndices hSourceIndices) = Array.ofFn values

The storage gather observes as Array.ofFn when every copied source entry agrees with the semantic finite-index function.

theorem TorchLean.Storage.size_gather {α : Type u} [storage : Storage α] (source : Buffer α) (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (sourceIndices : (index : USize) → index.toNat < length → USize) (hSourceIndices : ∀ (index : USize) (hIndex : index.toNat < length), (sourceIndices index hIndex).toNat < size source) : size (gather source length bound hBound sourceIndices hSourceIndices) = length

The storage gather creates the requested scalar count.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfCopyFn {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (nativeStep : Storage.Buffer α → (index : USize) → index.toNat < length → Storage.Buffer α) : Storage.Buffer α

Fill a physical buffer with an executable update callback.

Unlike nativeBufferOfFn, the callback returns the updated physical buffer instead of a scalar. Movement kernels can therefore copy boxed objects or unboxed native entries without materializing a scalar at the callback ABI.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfCopyFn_toArray {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (nativeStep : Storage.Buffer α → (index : USize) → index.toNat < length → Storage.Buffer α) (values : Fin length → α) (hStep : ∀ (output : Storage.Buffer α) (index : USize) (hIndex : index.toNat < length), nativeStep output index hIndex = Storage.push output (values ⟨index.toNat, hIndex⟩)) : Storage.toArray (nativeBufferOfCopyFn length bound hBound nativeStep) = Array.ofFn values

A physical-update buffer fill observes as Array.ofFn when every update is the corresponding semantic push.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfCopyFn_size {α : Type u} [storage : Storage α] (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (nativeStep : Storage.Buffer α → (index : USize) → index.toNat < length → Storage.Buffer α) (values : Fin length → α) (hStep : ∀ (output : Storage.Buffer α) (index : USize) (hIndex : index.toNat < length), nativeStep output index hIndex = Storage.push output (values ⟨index.toNat, hIndex⟩)) : Storage.size (nativeBufferOfCopyFn length bound hBound nativeStep) = length

A physical-update buffer fill creates the requested scalar count.