Physical Tensor Storage

Storage α selects the physical buffer used by tensors with scalar type α. Arbitrary scalar types retain ordinary Array α storage. Float uses Lean's unboxed FloatArray runtime representation, while UInt8 uses ByteArray.

The toArray laws are the proof boundary: the kernel reasons about an ordinary array observation, while compiled code calls the specialized buffer operations directly. Selected pointwise, slice, and transpose operations also have proof-visible Lean definitions with native compiled replacements. The Lean theorems describe those definitions; agreement of the external C bodies is a native runtime boundary documented in docs/TRUST_BOUNDARIES.md.

@[irreducible, specialize #[]]

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

Run the tail-recursive engine used by nativeFinFoldl.

hBound and the callback's index proof are erased. The executable loop therefore carries only an unboxed bound, counter, and accumulator.

@[inline]

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

Fold over Fin length with a platform-native loop counter.

The caller supplies a native bound together with an erased proof that it represents the semantic length.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeFinFoldl_eq_fin_foldl {α : Type u} (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (step : α → Fin length → α) (initial : α) : nativeFinFoldl length bound hBound (fun (value : α) (index : USize) (hIndex : index.toNat < length) => step value ⟨index.toNat, hIndex⟩) initial = Fin.foldl length step initial

nativeFinFoldl computes exactly Fin.foldl.

Generated kernels can execute with an unboxed counter while proofs continue to reason about the standard finite enumeration.

theorem TorchLean.Tensor.Internal.Elab.Impl.nativeFinFoldl_eq_fin_foldl_of_eq {α : Type u} (length : ℕ) (bound : USize) (hBound : bound.toNat = length) (nativeStep : α → (index : USize) → index.toNat < length → α) (step : α → Fin length → α) (initial : α) (hStep : ∀ (value : α) (index : USize) (hIndex : index.toNat < length), nativeStep value index hIndex = step value ⟨index.toNat, hIndex⟩) : nativeFinFoldl length bound hBound nativeStep initial = Fin.foldl length step initial

A native callback computes the semantic finite fold when it agrees with the semantic callback at every represented index.

class TorchLean.Storage (α : Type u) : Type (u + 1)

Physical tensor storage for one scalar type.

The buffer operations are used by generated native kernels. toArray is their proof-facing observation and may allocate when explicitly evaluated; optimized code therefore stays on Buffer, get, uget, push, and appendSlice.

• Buffer : Type u

  Physical row-major scalar buffer.

• emptyWithCapacity : ℕ → Buffer α

  Allocate an empty buffer with room for the requested number of scalars.

• push : Buffer α → α → Buffer α

  Append one scalar.

• appendSlice : Buffer α → ℕ → ℕ → Buffer α → Buffer α

  Append a contiguous half-open source interval to an output buffer.

• foldl {β : Type u} : (β → α → β) → β → Buffer α → β

  Traverse the physical buffer in row-major order.

• size : Buffer α → ℕ

  Number of scalar entries in the buffer.

• copyAt (source : Buffer α) (index : USize) : index.toNat < size source → Buffer α → Buffer α

  Copy one physical entry from a source buffer into an output buffer.

  Unlike push output (uget source index ...), this primitive does not expose the scalar at the caller boundary. Generic arrays can therefore transfer an existing boxed object directly, while scalar arrays read and write their unboxed representation.

• gather (source : Buffer α) (length : ℕ) (bound : USize) : bound.toNat = length → (sourceIndices : (index : USize) → index.toNat < length → USize) → (∀ (index : USize) (hIndex : index.toNat < length), (sourceIndices index hIndex).toNat < size source) → Buffer α

  Build a buffer by gathering physical entries from one source buffer.

  The storage implementation owns the complete loop so backend selection happens once per tensor rather than once per copied scalar.

• gather_eq_nativeFinFoldl (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) : gather source length bound hBound sourceIndices hSourceIndices = Tensor.Internal.Elab.Impl.nativeFinFoldl length bound hBound (fun (output : Buffer α) (index : USize) (hIndex : index.toNat < length) => copyAt source (sourceIndices index hIndex) ⋯ output) (emptyWithCapacity length)

  Physical gathering is the storage-specific native finite loop.

• get (buffer : Buffer α) (index : ℕ) : index < size buffer → α

  Read one scalar using a natural-number index.

• uget (buffer : Buffer α) (index : USize) : index.toNat < size buffer → α

  Read one scalar using a platform-native index.

• toArray : Buffer α → Array α

  Observe the physical buffer as an ordinary logical array.

• ofArray : Array α → Buffer α

  Construct physical storage from an ordinary array.

• toArray_size (buffer : Buffer α) : (toArray buffer).size = size buffer

  Buffer observation preserves size.

• toArray_get (buffer : Buffer α) (index : ℕ) (hBuffer : index < size buffer) (hArray : index < (toArray buffer).size) : (toArray buffer)[index] = get buffer index hBuffer

  Buffer observation preserves natural-number reads.

• toArray_uget (buffer : Buffer α) (index : USize) (hBuffer : index.toNat < size buffer) (hArray : index.toNat < (toArray buffer).size) : (toArray buffer).uget index hArray = uget buffer index hBuffer

  Buffer observation preserves platform-native reads.

• toArray_emptyWithCapacity (capacity : ℕ) : toArray (emptyWithCapacity capacity) = Array.emptyWithCapacity capacity

  An empty physical buffer observes as an empty ordinary array.

• toArray_push (buffer : Buffer α) (value : α) : toArray (push buffer value) = (toArray buffer).push value

  Appending one scalar commutes with buffer observation.

• toArray_copyAt (source : Buffer α) (index : USize) (hBuffer : index.toNat < size source) (output : Buffer α) (hArray : index.toNat < (toArray source).size) : toArray (copyAt source index hBuffer output) = (toArray output).push ((toArray source).uget index hArray)

  Copying one physical entry commutes with buffer observation.

• toArray_appendSlice (source : Buffer α) (start stop : ℕ) (output : Buffer α) : toArray (appendSlice source start stop output) = toArray output ++ (toArray source).extract start stop

  Appending a source interval commutes with buffer observation.

• toArray_foldl {β : Type u} (step : β → α → β) (initial : β) (buffer : Buffer α) : foldl step initial buffer = Array.foldl step initial (toArray buffer)

  Row-major traversal agrees with folding the ordinary array observation.

• toArray_ofArray (values : Array α) : toArray (ofArray values) = values

  Converting from an ordinary array is inverse to observation.

• toArray_injective : Function.Injective toArray

  The ordinary array observation uniquely determines physical storage.

class TorchLean.Storage.Update (α : Type u) [storage : Storage α] : Type u

Copy-on-write replacement of one physical scalar.

Every Storage receives the ordinary-array fallback below, so defining a custom scalar storage does not require implementing this capability. Packed backends can override it to retain their native representation.

• set (buffer : Buffer α) (index : ℕ) : index < size buffer → α → Buffer α

  Replace one in-bounds physical entry.

• toArray_set (buffer : Buffer α) (index : ℕ) (hBuffer : index < size buffer) (value : α) : toArray (set buffer index hBuffer value) = (toArray buffer).set index value ⋯

  Physical replacement agrees with ordinary-array replacement.

@[instance_reducible, instance 100]

instance TorchLean.Storage.instUpdate (α : Type u) [storage : Storage α] : Update α

Universal update support for any storage.

This fallback round-trips through the logical array observation. Specialized packed storage overrides it below with native copy-on-write replacement.

theorem TorchLean.Storage.copyAt_eq_push_of_uget_eq {α : Type u} [storage : Storage α] (source : Buffer α) (index : USize) (hSource : index.toNat < size source) (output : Buffer α) (value : α) (hValue : uget source index hSource = value) : copyAt source index hSource output = push output value

Copying a physical entry is the same buffer update as pushing its observed scalar value.

Generated movement kernels use this theorem to reason about copyAt without exposing the scalar at the executable callback boundary.

def TorchLean.Storage.ofFn {α : Type u} [storage : Storage α] {length : ℕ} (values : Fin length → α) : Buffer α

Construct a physical buffer from a finite scalar function.

theorem TorchLean.Storage.fin_foldl_push_eq_array_ofFn {α : Type u} (length : ℕ) (values : Fin length → α) : Fin.foldl length (fun (output : Array α) (index : Fin length) => output.push (values index)) (Array.emptyWithCapacity length) = Array.ofFn values

Pushing finite-indexed values in order constructs Array.ofFn.

theorem TorchLean.Storage.toArray_finFoldl_push_eq_array_ofFn {α : Type u} [storage : Storage α] {length : ℕ} (capacity : ℕ) (values : Fin length → α) : toArray (Fin.foldl length (fun (output : Buffer α) (index : Fin length) => push output (values index)) (emptyWithCapacity capacity)) = Array.ofFn values

Observing finite pushes from any reserved capacity gives the corresponding ordinary function array.

theorem TorchLean.Storage.toArray_ofFn {α : Type u} [storage : Storage α] {length : ℕ} (values : Fin length → α) : toArray (ofFn values) = Array.ofFn values

Finite construction observes as the corresponding ordinary array.

theorem TorchLean.Storage.size_ofFn {α : Type u} [storage : Storage α] {length : ℕ} (values : Fin length → α) : size (ofFn values) = length

Finite construction creates exactly the requested number of scalars.

theorem TorchLean.Storage.size_eq_of_toArray_eq_ofFn {α : Type u} [storage : Storage α] {length : ℕ} (buffer : Buffer α) (values : Fin length → α) (hData : toArray buffer = Array.ofFn values) : size buffer = length

An Array.ofFn observation determines the physical buffer size.

theorem TorchLean.Storage.size_emptyWithCapacity {α : Type u} [storage : Storage α] (capacity : ℕ) : size (emptyWithCapacity capacity) = 0

Empty physical storage contains no scalar entries.

theorem TorchLean.Storage.size_push {α : Type u} [storage : Storage α] (buffer : Buffer α) (value : α) : size (push buffer value) = size buffer + 1

Appending one scalar increases physical storage length by one.

theorem TorchLean.Storage.size_ofArray {α : Type u} [storage : Storage α] (values : Array α) : size (ofArray values) = values.size

Constructing physical storage from an array preserves its length.

@[inline]

def TorchLean.appendArraySlice {α : Type u} (source : Array α) (start stop : ℕ) (output : Array α) : Array α

Append one contiguous ordinary-array interval to an output array.

theorem TorchLean.appendArraySlice_eq_append_extract {α : Type u} (source : Array α) (start stop : ℕ) (output : Array α) : appendArraySlice source start stop output = output ++ source.extract start stop

Ordinary-array slice traversal is extraction followed by append.

@[inline, specialize #[]]

def TorchLean.copyArrayAt {α : Type u} (source : Array α) (index : USize) (hIndex : index.toNat < source.size) (output : Array α) : Array α

Copy one ordinary-array entry without exposing its scalar at the caller boundary.

Specializing a scalar-valued callback can unbox and immediately rebox values such as Float32. Keeping the transfer inside this polymorphic primitive lets Lean's runtime retain and move the existing lean_object* instead.

@[specialize #[]]

def TorchLean.gatherArray {α : Type u} (source : Array α) (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 < source.size) : Array α

Gather ordinary-array entries without exposing their scalar values.

@[instance_reducible, inline, instance 100]

instance TorchLean.instArrayStorage (α : Type u) : Storage α

Ordinary polymorphic arrays are the universal tensor-storage fallback.

@[implemented_by ByteArray.emptyWithCapacity]

def TorchLean.Storage.Internal.byteBufferEmptyWithCapacity (capacity : ℕ) : ByteArray

Proof-visible model of the native empty ByteArray allocator.

Compiled code calls Lean's built-in scalar-array runtime primitive.

@[implemented_by ByteArray.push]

def TorchLean.Storage.Internal.byteBufferPush : ByteArray → UInt8 → ByteArray

Proof-visible model of native ByteArray.push.

@[implemented_by ByteArray.size]

def TorchLean.Storage.Internal.byteBufferSize : ByteArray → ℕ

Proof-visible model of native ByteArray.size.

@[inline]

unsafe def TorchLean.Storage.Internal.byteBufferCopyAtFast (source : ByteArray) (index : USize) (_hIndex : index.toNat < byteBufferSize source) (output : ByteArray) : ByteArray

Fast native transfer between byte buffers.

@[implemented_by TorchLean.Storage.Internal.byteBufferCopyAtFast]

def TorchLean.Storage.Internal.byteBufferCopyAt (source : ByteArray) (index : USize) (hIndex : index.toNat < byteBufferSize source) (output : ByteArray) : ByteArray

Proof-visible model of one native byte-buffer transfer.

@[inline]

unsafe def TorchLean.Storage.Internal.byteBufferGetFast (buffer : ByteArray) (index : ℕ) (_hIndex : index < byteBufferSize buffer) : UInt8

Runtime adapter from the proof-visible byte-buffer bound to ByteArray.get.

@[implemented_by TorchLean.Storage.Internal.byteBufferGetFast]

def TorchLean.Storage.Internal.byteBufferGet (buffer : ByteArray) (index : ℕ) : index < byteBufferSize buffer → UInt8

Proof-visible model of native natural-number ByteArray lookup.

@[inline]

unsafe def TorchLean.Storage.Internal.byteBufferSetFast (buffer : ByteArray) (index : ℕ) (_hIndex : index < byteBufferSize buffer) (value : UInt8) : ByteArray

Fast native replacement in a packed byte buffer.

@[implemented_by TorchLean.Storage.Internal.byteBufferSetFast]

def TorchLean.Storage.Internal.byteBufferSet (buffer : ByteArray) (index : ℕ) (hIndex : index < byteBufferSize buffer) (value : UInt8) : ByteArray

Proof-visible model of native byte-buffer replacement.

@[inline]

unsafe def TorchLean.Storage.Internal.byteBufferUGetFast (buffer : ByteArray) (index : USize) (_hIndex : index.toNat < byteBufferSize buffer) : UInt8

Runtime adapter from the proof-visible byte-buffer bound to ByteArray.uget.

@[implemented_by TorchLean.Storage.Internal.byteBufferUGetFast]

def TorchLean.Storage.Internal.byteBufferUGet (buffer : ByteArray) (index : USize) : index.toNat < byteBufferSize buffer → UInt8

Proof-visible model of native USize ByteArray lookup.

@[inline]

def TorchLean.Storage.Internal.byteBufferGather (source : ByteArray) (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 < byteBufferSize source) : ByteArray

Gather native byte-buffer entries in one storage-specific loop.

@[inline]

def TorchLean.Storage.Internal.byteBufferAppendSliceFast (source : ByteArray) (start stop : ℕ) (output : ByteArray) : ByteArray

Fast native implementation of contiguous byte-buffer copying.

Clamp before calling ByteArray.copySlice: its native allocator may reserve the requested length before clipping the source interval. The model follows Array.extract, including huge naturals.

@[implemented_by TorchLean.Storage.Internal.byteBufferAppendSliceFast]

def TorchLean.Storage.Internal.byteBufferAppendSlice (source : ByteArray) (start stop : ℕ) (output : ByteArray) : ByteArray

Proof-visible model of contiguous native ByteArray traversal.

The logical body exposes ordinary array extraction. Native code delegates the whole interval to Lean's built-in ByteArray.copySlice runtime primitive.

@[inline]

def TorchLean.Storage.Internal.byteBufferFoldlFast {β : Type u} (step : β → UInt8 → β) (initial : β) (buffer : ByteArray) : β

Fast native traversal of an unboxed byte buffer.

@[implemented_by TorchLean.Storage.Internal.byteBufferFoldlFast]

def TorchLean.Storage.Internal.byteBufferFoldl {β : Type u} (step : β → UInt8 → β) (initial : β) (buffer : ByteArray) : β

Proof-visible model of native ByteArray traversal.

The logical body exposes the ordinary array fold. Native code traverses the unboxed byte buffer directly.

@[irreducible, implemented_by FloatArray.emptyWithCapacity]

def TorchLean.Storage.Internal.floatBufferEmptyWithCapacity (capacity : ℕ) : FloatArray

Proof-visible model of the native empty FloatArray allocator.

Compiled code calls Lean's built-in scalar-array runtime primitive.

@[irreducible, implemented_by FloatArray.push]

def TorchLean.Storage.Internal.floatBufferPush : FloatArray → Float → FloatArray

Proof-visible model of native FloatArray.push.

@[irreducible, implemented_by FloatArray.size]

def TorchLean.Storage.Internal.floatBufferSize : FloatArray → ℕ

Proof-visible model of native FloatArray.size.

@[inline]

unsafe def TorchLean.Storage.Internal.floatBufferCopyAtFast (source : FloatArray) (index : USize) (_hIndex : index.toNat < floatBufferSize source) (output : FloatArray) : FloatArray

Fast native transfer between floating-point buffers.

@[implemented_by TorchLean.Storage.Internal.floatBufferCopyAtFast]

def TorchLean.Storage.Internal.floatBufferCopyAt (source : FloatArray) (index : USize) (hIndex : index.toNat < floatBufferSize source) (output : FloatArray) : FloatArray

Proof-visible model of one native floating-point-buffer transfer.

@[inline]

unsafe def TorchLean.Storage.Internal.floatBufferGetFast (buffer : FloatArray) (index : ℕ) (_hIndex : index < floatBufferSize buffer) : Float

Runtime adapter from the proof-visible float-buffer bound to FloatArray.get.

@[irreducible, implemented_by TorchLean.Storage.Internal.floatBufferGetFast]

def TorchLean.Storage.Internal.floatBufferGet (buffer : FloatArray) (index : ℕ) : index < floatBufferSize buffer → Float

Proof-visible model of native natural-number FloatArray lookup.

@[inline]

unsafe def TorchLean.Storage.Internal.floatBufferUGetFast (buffer : FloatArray) (index : USize) (_hIndex : index.toNat < floatBufferSize buffer) : Float

Runtime adapter from the proof-visible float-buffer bound to FloatArray.uget.

@[irreducible, implemented_by TorchLean.Storage.Internal.floatBufferUGetFast]

def TorchLean.Storage.Internal.floatBufferUGet (buffer : FloatArray) (index : USize) : index.toNat < floatBufferSize buffer → Float

Proof-visible model of native USize FloatArray lookup.

@[inline]

def TorchLean.Storage.Internal.floatBufferGather (source : FloatArray) (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 < floatBufferSize source) : FloatArray

Gather native floating-point-buffer entries in one storage-specific loop.

def TorchLean.Storage.Internal.floatBufferAppendSlice (source : FloatArray) (start stop : ℕ) (output : FloatArray) : FloatArray

Proof-visible model of contiguous native FloatArray traversal.

The logical body exposes ordinary array extraction.

@[extern torchlean_float_array_append_slice]

def TorchLean.Storage.Internal.floatBufferAppendSliceNative (source : FloatArray) (start stop : ℕ) (output : FloatArray) : FloatArray

Native implementation of contiguous packed floating-point copying.

The body calls the reference rather than restating it, so the rfl below cannot drift; compiled code replaces the whole thing with torchlean_float_array_append_slice.

@[csimp]

theorem TorchLean.Storage.Internal.floatBufferAppendSlice_eq_native : floatBufferAppendSlice = floatBufferAppendSliceNative

Compile packed floating-point slice appends to one native bulk-copy call.

Lean evaluation and proofs continue to unfold floatBufferAppendSlice; only generated code uses the external implementation.

@[inline]

def TorchLean.Storage.Internal.floatBufferFoldlFast {β : Type u} (step : β → Float → β) (initial : β) (buffer : FloatArray) : β

Fast native traversal of an unboxed floating-point buffer.

@[implemented_by TorchLean.Storage.Internal.floatBufferFoldlFast]

def TorchLean.Storage.Internal.floatBufferFoldl {β : Type u} (step : β → Float → β) (initial : β) (buffer : FloatArray) : β

Proof-visible model of native FloatArray traversal.

The logical body exposes the ordinary array fold. Native code traverses the unboxed floating-point buffer directly.

@[inline]

unsafe def TorchLean.Storage.Internal.floatBufferSetFast (buffer : FloatArray) (index : ℕ) (_hIndex : index < floatBufferSize buffer) (value : Float) : FloatArray

Fast native replacement in an unboxed floating-point buffer.

@[irreducible, implemented_by TorchLean.Storage.Internal.floatBufferSetFast]

def TorchLean.Storage.Internal.floatBufferSet (buffer : FloatArray) (index : ℕ) (hIndex : index < floatBufferSize buffer) (value : Float) : FloatArray

Proof-visible model of native floating-point-buffer replacement.

@[instance_reducible]

instance TorchLean.instUInt8Storage : Storage UInt8

UInt8 tensors use Lean's packed native byte-array representation.

@[instance_reducible]

instance TorchLean.instFloatStorage : Storage Float

Float tensors use Lean's unboxed native scalar-array representation.

@[instance_reducible]

instance TorchLean.instUInt8StorageUpdate : Storage.Update UInt8

Byte tensors replace entries directly in their packed native buffer.

@[instance_reducible]

instance TorchLean.instFloatStorageUpdate : Storage.Update Float

Float tensors replace entries directly in their unboxed native buffer.