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.

Contiguous copying reuses TorchLean.appendArraySlice and appendArraySlice_eq_append_extract from the storage layer.

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.nativeArrayOfSlices {α : Type u} (rowCount rowLength sourceStride sourceOffset : ℕ) (rowBound : USize) (hRowBound : rowBound.toNat = rowCount) (source : Array α) : Array α

Build an array by appending one fixed-width source slice for each row.

The executable path uses an unboxed outer counter and the runtime array slice fold. Source range proofs remain confined to the correctness theorem.

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

The native slice builder equals Array.ofFn when every extracted row agrees with the corresponding finite-function row.

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

The native slice builder produces the requested flattened size.

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