Certified native two-dimensional transpose

This module gives the common two-axis rearrange permutation tiled native implementations for packed FloatArray and ordinary polymorphic Array storage. Their proof-visible definitions are ordinary row-major Array.ofFn terms; compiled execution uses native tiled loops.

theorem TorchLean.Tensor.Internal.Elab.Impl.transpose2DIndexValue_lt (rows columns index : ℕ) (hIndex : index < columns * rows) : index / rows + columns * (index % rows) < rows * columns

The quotient/remainder transpose address is inside the source rectangle.

def TorchLean.Tensor.Internal.Elab.Impl.transpose2DIndex (rows columns : ℕ) : Fin (columns * rows) → Fin (rows * columns)

Source index selected by a row-major two-dimensional transpose.

def TorchLean.Tensor.Internal.Elab.Impl.transpose2DShapeIndex (rows columns : ℕ) : Fin (Shape.size [columns, rows]) → Fin (Shape.size [rows, columns])

Shape-indexed form of transpose2DIndex used by tensor pullbacks.

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferTranspose2D (source : FloatArray) (rows columns : ℕ) (hSize : source.data.size = rows * columns) : FloatArray

Proof-visible model of the packed two-dimensional transpose.

The source-size certificate is erased. It supplies the bounds needed by the ordinary finite-array model used in correctness proofs.

def TorchLean.Tensor.Internal.Elab.Impl.arrayBufferTranspose2D {α : Type u} (source : Array α) (rows columns : ℕ) (hSize : source.size = rows * columns) : Array α

Proof-visible model of the ordinary-array two-dimensional transpose.

The native implementation transfers retained object pointers directly. This model states the same operation solely in terms of ordinary array indexing.

@[extern torchlean_float_array_transpose2d]

def TorchLean.Tensor.Internal.Elab.Impl.floatBufferTranspose2DNative (source : FloatArray) (rows columns : ℕ) (hSize : source.data.size = rows * columns) : FloatArray

Native packed two-dimensional transpose, compiled to one tiled C loop.

@[extern torchlean_array_transpose2d]

def TorchLean.Tensor.Internal.Elab.Impl.arrayBufferTranspose2DNative {α : Type u} (source : Array α) (rows columns : ℕ) (hSize : source.size = rows * columns) : Array α

Native ordinary-array two-dimensional transpose, compiled to one tiled C loop.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferTranspose2D_eq_native : floatBufferTranspose2D = floatBufferTranspose2DNative

Use the tiled native packed transpose only in generated code.

@[csimp]

theorem TorchLean.Tensor.Internal.Elab.Impl.arrayBufferTranspose2D_eq_native : @arrayBufferTranspose2D = @arrayBufferTranspose2DNative

Use the tiled native ordinary-array transpose only in generated code.

theorem TorchLean.Tensor.Internal.Elab.Impl.floatBufferTranspose2D_size (source : FloatArray) (rows columns : ℕ) (hSize : source.data.size = rows * columns) : (floatBufferTranspose2D source rows columns hSize).data.size = columns * rows

The packed transpose has exactly the transposed scalar count.

theorem TorchLean.Tensor.Internal.Elab.Impl.arrayBufferTranspose2D_size {α : Type u} (source : Array α) (rows columns : ℕ) (hSize : source.size = rows * columns) : (arrayBufferTranspose2D source rows columns hSize).size = columns * rows

The ordinary-array transpose has exactly the transposed scalar count.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeFloatTranspose2D (rows columns : ℕ) (source : Rep Float [rows, columns]) : Rep Float [columns, rows]

Transpose a rank-two packed floating-point tensor without scalar callbacks.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.nativeArrayTranspose2D {α : Type u} (rows columns : ℕ) (source : Rep α [rows, columns]) : Rep α [columns, rows]

Transpose a rank-two ordinary-array tensor without scalar callbacks.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeFloatTranspose2D_correct (rows columns : ℕ) (source : Rep Float [rows, columns]) : nativeFloatTranspose2D rows columns source = Rep.pullFlat (transpose2DShapeIndex rows columns) source

The native rank-two transpose implements the ordinary flat pullback.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeArrayTranspose2D_correct {α : Type u} (rows columns : ℕ) (source : Rep α [rows, columns]) : nativeArrayTranspose2D rows columns source = Rep.pullFlat (transpose2DShapeIndex rows columns) source

The native ordinary-array transpose implements the flat pullback.