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.

theorem TorchLean.Tensor.Internal.Elab.Impl.ite_eq_of_branch_eq {α : Type u} (condition : Prop) [Decidable condition] (thenValue elseValue expected : α) (hThen : condition → thenValue = expected) (hElse : ¬condition → elseValue = expected) : (if condition then thenValue else elseValue) = expected

Combine branch-local equality proofs for a generated runtime decision.

Native segmented kernels use this theorem to assemble arbitrary-length decision trees while keeping each leaf's semantic certificate local.

theorem TorchLean.Tensor.Internal.Elab.Impl.dite_eq_of_branch_eq {α : Type u} (condition : Prop) [Decidable condition] (thenValue : condition → α) (elseValue : ¬condition → α) (expected : α) (hThen : ∀ (proof : condition), thenValue proof = expected) (hElse : ∀ (proof : ¬condition), elseValue proof = expected) : (if proof : condition then thenValue proof else elseValue proof) = expected

Combine proof-dependent branches that both compute the same semantic value.

The branch evidence erases in generated native code, while each branch may use it to certify subtraction, bounds, or direct buffer reads.

fin_foldl_push_eq_array_ofFn is not restated here. It is proved once in NN.Tensor.Internal.Representation.Storage, which this file imports, and it used to have an exact second copy at this spot. The uses below spell out the Storage. prefix rather than opening the namespace, so a reader can see at a glance that the lemma comes from the storage layer.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeArrayOfFn {α : Type u} (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (values : (index : USize) → index.toNat < length → α) : Array α

Fill one array in increasing native-index order.

The callback's bound proof is erased, so the executable builder contains one allocation and one USize loop.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeArrayOfFn_eq_array_ofFn {α : Type u} (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⟩) : nativeArrayOfFn length bound hBound nativeValues = Array.ofFn values

The native array builder equals Array.ofFn whenever its native callback agrees pointwise with the semantic finite-index function.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeArrayOfFn_size {α : Type u} (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (values : (index : USize) → index.toNat < length → α) : (nativeArrayOfFn length bound hBound values).size = length

The native builder produces the statically requested number of entries.

@[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.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeBufferGather {α : Type u} [storage : Storage α] (source : Storage.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 < Storage.size source) : Storage.Buffer α

Fill a physical buffer by copying entries from another buffer.

The source-index callback never exposes α. Generic arrays can therefore retain and transfer existing boxed values, while specialized scalar arrays perform direct unboxed reads and writes.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferGather_toArray {α : Type u} [storage : Storage α] (source : Storage.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 < Storage.size source) (values : Fin length → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < length), Storage.uget source (sourceIndices index hIndex) ⋯ = values ⟨index.toNat, hIndex⟩) : Storage.toArray (nativeBufferGather source length bound hBound sourceIndices hSourceIndices) = Array.ofFn values

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

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferGather_size {α : Type u} [storage : Storage α] (source : Storage.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 < Storage.size source) : Storage.size (nativeBufferGather source length bound hBound sourceIndices hSourceIndices) = length

The native 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.