Certified native array slices

Contiguous tensor blocks can be copied with Array.foldl rather than recomputing a source index for every scalar. These helpers retain Array.ofFn as their independent semantic reference.

def TorchLean.Tensor.Internal.Elab.Impl.rectangularIndex (rowCount rowLength : ℕ) (row : Fin rowCount) (column : Fin rowLength) : Fin (rowCount * rowLength)

Flatten one row and column index into a rectangular row-major index.

theorem TorchLean.Tensor.Internal.Elab.Impl.fin_foldl_append_rows_eq_array_ofFn {α : Type u} (rowCount rowLength : ℕ) (values : Fin (rowCount * rowLength) → α) : Fin.foldl rowCount (fun (output : Array α) (row : Fin rowCount) => output ++ Array.ofFn fun (column : Fin rowLength) => values (rectangularIndex rowCount rowLength row column)) (Array.emptyWithCapacity (rowCount * rowLength)) = Array.ofFn values

Appending fixed-width rows in finite-index order reconstructs their flattened finite function.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfSlices {α : Type u} [storage : Storage α] (rowCount rowLength sourceStride sourceOffset : ℕ) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Storage.Buffer α) : Storage.Buffer α

Build a physical buffer by appending one fixed-width source slice per row.

For Float, appendSlice traverses the unboxed FloatArray directly.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfSlices_toArray {α : Type u} [storage : Storage α] (rowCount rowLength sourceStride sourceOffset : ℕ) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Storage.Buffer α) (values : Fin (rowCount * rowLength) → α) (hRanges : ∀ (row : Fin rowCount), ↑row * sourceStride + sourceOffset + rowLength ≤ Storage.size source) (hValues : ∀ (row : Fin rowCount) (column : Fin rowLength), Storage.get source (↑row * sourceStride + sourceOffset + ↑column) ⋯ = values (rectangularIndex rowCount rowLength row column)) : Storage.toArray (nativeBufferOfSlices rowCount rowLength sourceStride sourceOffset rowBound hRowBound source) = Array.ofFn values

The physical slice builder observes as Array.ofFn when each copied source row agrees with the corresponding semantic row.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeBufferOfSlices_size {α : Type u} [storage : Storage α] (rowCount rowLength sourceStride sourceOffset : ℕ) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Storage.Buffer α) (values : Fin (rowCount * rowLength) → α) (hRanges : ∀ (row : Fin rowCount), ↑row * sourceStride + sourceOffset + rowLength ≤ Storage.size source) (hValues : ∀ (row : Fin rowCount) (column : Fin rowLength), Storage.get source (↑row * sourceStride + sourceOffset + ↑column) ⋯ = values (rectangularIndex rowCount rowLength row column)) : Storage.size (nativeBufferOfSlices rowCount rowLength sourceStride sourceOffset rowBound hRowBound source) = rowCount * rowLength

The physical slice builder produces exactly the requested scalar count.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfSlices {α : Type u} [storage : Storage α] {shape sourceShape : Shape} (rowCount rowLength sourceStride sourceOffset : ℕ) (hShapeSize : rowCount * rowLength = shape.size) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Rep α sourceShape) (values : Fin shape.size → α) (hRanges : ∀ (row : Fin rowCount), ↑row * sourceStride + sourceOffset + rowLength ≤ sourceShape.size) (hValues : ∀ (row : Fin rowCount) (column : Fin rowLength), source.getFlat ⟨↑row * sourceStride + sourceOffset + ↑column, ⋯⟩ = values (Fin.cast hShapeSize (rectangularIndex rowCount rowLength row column))) : Rep α shape

Build a shaped tensor by copying a fixed-width source slice for each row.

The shape equality and row certificates erase, leaving only the source array, four static index constants, and the native outer loop.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeTensorOfSlices_correct {α : Type u} [storage : Storage α] {shape sourceShape : Shape} (rowCount rowLength sourceStride sourceOffset : ℕ) (hShapeSize : rowCount * rowLength = shape.size) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Rep α sourceShape) (values : Fin shape.size → α) (hRanges : ∀ (row : Fin rowCount), ↑row * sourceStride + sourceOffset + rowLength ≤ sourceShape.size) (hValues : ∀ (row : Fin rowCount) (column : Fin rowLength), source.getFlat ⟨↑row * sourceStride + sourceOffset + ↑column, ⋯⟩ = values (Fin.cast hShapeSize (rectangularIndex rowCount rowLength row column))) : nativeTensorOfSlices rowCount rowLength sourceStride sourceOffset hShapeSize rowBound hRowBound source values hRanges hValues = Rep.ofFlatFn values

The native tensor slice builder equals its ordinary finite-function tensor.