Native shaped tensor storage

Rep α shape stores one contiguous row-major buffer selected by Storage α. Its proof field certifies that the buffer length is exactly Shape.size shape, while its coordinate-function view supplies the mathematical observation semantics. The size proof does not establish exclusive ownership or verify an external storage implementation; native copy-on-write behavior belongs to the backend.

structure TorchLean.Tensor.Internal.Rep (α : Type u) (s : Shape) [storage : Storage α] : Type u

A contiguous row-major tensor whose storage length is certified by its shape.

The proof is erased by code generation. At runtime a tensor is therefore its selected native buffer, rather than a coordinate closure or a second semantic representation.

• buffer : Storage.Buffer α

  Contiguous row-major scalar storage.

• size_eq : Storage.size self.buffer = s.size

  The storage has exactly one entry for every coordinate of the shape.

def TorchLean.Tensor.Internal.Rep.castShape {α : Type u} [Storage α] {sourceShape targetShape : Shape} (h : sourceShape = targetShape) (tensor : Rep α sourceShape) : Rep α targetShape

Transport a tensor along an equality of its static shape.

@[inline]

def TorchLean.Tensor.Internal.Rep.getFlat {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) (i : Fin s.size) : α

Read one row-major entry from a tensor's native storage.

@[inline]

def TorchLean.Tensor.Internal.Rep.getFlatUSize {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) (i : USize) (h : i.toNat < s.size) : α

Read one row-major entry using a platform-native array index.

The explicit bound is the same safety certificate carried by Fin in getFlat. This form is used by generated kernels whose index arithmetic has already been proved to fit USize, avoiding boxed natural-number indexing in the scalar loop.

theorem TorchLean.Tensor.Internal.Rep.getFlatUSize_eq_getFlat {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) (i : USize) (h : i.toNat < s.size) : x.getFlatUSize i h = x.getFlat ⟨i.toNat, h⟩

Platform-native and finite flat reads agree at the same row-major position.

Generic arrays satisfy this definitionally. Specialized storage proves it through the common ordinary-array observation.

theorem TorchLean.Tensor.Internal.Rep.getFlatUSize_congr {α : Type u} [Storage α] {s : Shape} (x : Rep α s) {i j : USize} (h : i = j) (hi : i.toNat < s.size) (hj : j.toNat < s.size) : x.getFlatUSize i hi = x.getFlatUSize j hj

Changing a native flat index along an equality does not change the observed tensor entry. The two bounds proofs may differ because their types mention the index; proof irrelevance removes that distinction after the indices agree.

@[inline]

def TorchLean.Tensor.Internal.Rep.get {α : Type u} [Storage α] {s : Shape} (x : Rep α s) (i : Coord s) : α

Read the entry at a multidimensional coordinate.

@[inline]

def TorchLean.Tensor.Internal.Rep.setFlat {α : Type u} [storage : Storage α] [update : Storage.Update α] {s : Shape} (x : Rep α s) (i : Fin s.size) (value : α) : Rep α s

Replace one row-major entry while preserving the tensor's static shape.

Packed storage performs a native copy-on-write update. Other storage types use the universal array-backed update capability supplied by Storage.Update.

@[inline]

def TorchLean.Tensor.Internal.Rep.set {α : Type u} [Storage α] [Storage.Update α] {s : Shape} (x : Rep α s) (i : Coord s) (value : α) : Rep α s

Replace the entry at a statically valid multidimensional coordinate.

@[inline]

def TorchLean.Tensor.Internal.Rep.modify {α : Type u} [Storage α] [Storage.Update α] {s : Shape} (x : Rep α s) (i : Coord s) (f : α → α) : Rep α s

Transform the entry at one statically valid coordinate.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instCoeFunForallCoord {α : Type u} [Storage α] {s : Shape} : CoeFun (Rep α s) fun (x : Rep α s) => Coord s → α

A tensor acts as its coordinate observation function in statements and proofs.

def TorchLean.Tensor.Internal.Rep.format {α : Type u} [Repr α] (shape : Shape) : (Coord shape → α) → Std.Format

Render a tensor as shape-aware nested lists, with rank-zero tensors rendered as their scalar value.

The recursion follows the coordinate type itself, so it works uniformly at every rank and renders a zero-length axis as an empty list.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instRepr {α : Type u} [Storage α] {shape : Shape} [Repr α] : Repr (Rep α shape)

Print a tensor as a scalar or shape-aware nested row-major lists.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instToStringOfRepr {α : Type u} [Storage α] {shape : Shape} [Repr α] : ToString (Rep α shape)

Use the ordinary shape-aware tensor rendering in strings and interpolations.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instReprForall {α : Type u} [Storage α] {componentCount : ℕ} {shapes : Fin componentCount → Shape} [Repr α] : Repr ((component : Fin componentCount) → Rep α (shapes component))

Print a finite dependent tensor family in component order.

This includes the result type returned by unpack; each component retains its own statically checked shape and uses the ordinary tensor representation.

def TorchLean.Tensor.Internal.Rep.ofFlatFn {α : Type u} [storage : Storage α] {s : Shape} (values : Fin s.size → α) : Rep α s

Build a tensor from a row-major function.

Construction reserves the requested capacity, then appends values in increasing flat-index order. Allocation and buffer reuse depend on the selected storage backend.

@[inline]

def TorchLean.Tensor.Internal.Rep.ofFlatNativeFn {α : Type u} [storage : Storage α] {s : Shape} (nativeValues : (index : USize) → index.toNat < s.size → α) (values : Fin s.size → α) (_hValues : ∀ (index : USize) (hIndex : index.toNat < s.size), nativeValues index hIndex = values ⟨index.toNat, hIndex⟩) : Rep α s

Build a tensor with a platform-native flat-index loop when its static size fits USize, and retain the universal finite-index construction otherwise.

The native and semantic callbacks are connected by an erased certificate. Ordinary executable tensor shapes therefore use unboxed loop counters and native storage reads, while the representation remains total for arbitrary mathematical shapes.

def TorchLean.Tensor.Internal.Rep.ofArray {α : Type u} [storage : Storage α] {s : Shape} (values : Array α) (hSize : values.size = s.size) : Rep α s

Build a tensor from an ordinary row-major array of the certified size.

theorem TorchLean.Tensor.Internal.Rep.mk_eq_ofFlatFn {α : Type u} [storage : Storage α] {s : Shape} (values : Fin s.size → α) (buffer : Storage.Buffer α) (hSize : Storage.size buffer = s.size) (hData : Storage.toArray buffer = Array.ofFn values) : { buffer := buffer, size_eq := hSize } = ofFlatFn values

Rebuilding a tensor from a buffer equal to Array.ofFn values gives the canonical flat-function tensor.

This theorem lets verified native builders replace their certified output buffer without exposing proof-field equality to generated code.

theorem TorchLean.Tensor.Internal.Rep.ofFlatNativeFn_eq_ofFlatFn {α : Type u} [storage : Storage α] {s : Shape} (nativeValues : (index : USize) → index.toNat < s.size → α) (values : Fin s.size → α) (hValues : ∀ (index : USize) (hIndex : index.toNat < s.size), nativeValues index hIndex = values ⟨index.toNat, hIndex⟩) : ofFlatNativeFn nativeValues values hValues = ofFlatFn values

Native flat construction has the ordinary finite-index tensor semantics.

def TorchLean.Tensor.Internal.Rep.ofFn {α : Type u} [Storage α] {s : Shape} (values : Coord s → α) : Rep α s

Build a native tensor by evaluating a coordinate function once per entry.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.getFlat_ofFlatFn {α : Type u} [storage : Storage α] {s : Shape} (values : Fin s.size → α) (i : Fin s.size) : (ofFlatFn values).getFlat i = values i

Reading a generated tensor at a flat index returns the generated value.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.get_ofFlatFn {α : Type u} [Storage α] {s : Shape} (values : Fin s.size → α) (i : Coord s) : (ofFlatFn values).get i = values i.linearize

Reading a flat-generated tensor linearizes the requested coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.get_ofFn {α : Type u} [Storage α] {s : Shape} (values : Coord s → α) (i : Coord s) : (ofFn values).get i = values i

Reading a generated tensor at a coordinate returns the generated value.

def TorchLean.Tensor.Internal.Rep.data {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) : Array α

Observe the native buffer as an ordinary array.

theorem TorchLean.Tensor.Internal.Rep.data_injective {α : Type u} [storage : Storage α] {s : Shape} : Function.Injective data

The ordinary-array observation uniquely determines a shaped tensor.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instDecidableEq {α : Type u} [storage : Storage α] [DecidableEq α] {s : Shape} : DecidableEq (Rep α s)

Executable tensors have decidable elementwise equality whenever their scalar type does.

The comparison uses the storage's certified ordinary-array observation. Equality of those observations determines equality of the native buffers, while the size certificates are proof-irrelevant.

@[inline]

def TorchLean.Tensor.Internal.Rep.foldl {α β : Type u} [storage : Storage α] {s : Shape} (step : β → α → β) (initial : β) (x : Rep α s) : β

Traverse tensor entries in physical row-major order without materializing the ordinary array observation.

theorem TorchLean.Tensor.Internal.Rep.foldl_eq_data_foldl {α β : Type u} [storage : Storage α] {s : Shape} (step : β → α → β) (initial : β) (x : Rep α s) : foldl step initial x = Array.foldl step initial x.data

Native tensor traversal agrees with folding the proof-facing observation.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.data_ofArray {α : Type u} [storage : Storage α] {s : Shape} (values : Array α) (hSize : values.size = s.size) : (ofArray values hSize).data = values

Observing a tensor built from an ordinary array returns that array.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.getFlat_ofArray {α : Type u} [storage : Storage α] {s : Shape} (values : Array α) (hSize : values.size = s.size) (index : Fin s.size) : (ofArray values hSize).getFlat index = values[↑index]

Flat lookup into a tensor built from an ordinary array reads that array.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.get_ofArray {α : Type u} [Storage α] {s : Shape} (values : Array α) (hSize : values.size = s.size) (coordinate : Coord s) : (ofArray values hSize).get coordinate = values[↑coordinate.linearize]

Coordinate lookup into an array-built tensor uses row-major linearization.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.data_size {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) : x.data.size = s.size

The proof-facing ordinary array observation has the statically known tensor size. Evaluating data may convert specialized storage, so native kernels use buffer, getFlat, and getFlatUSize instead.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.data_getFlat {α : Type u} [storage : Storage α] {s : Shape} (x : Rep α s) (index : Fin s.size) : x.data[↑index] = x.getFlat index

Reading the array observation agrees with native flat tensor lookup.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.getFlat_setFlat_self {α : Type u} [storage : Storage α] [update : Storage.Update α] {s : Shape} (x : Rep α s) (i : Fin s.size) (value : α) : (x.setFlat i value).getFlat i = value

Reading a flat entry immediately after replacing it returns the new value.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.get_set_self {α : Type u} [Storage α] [Storage.Update α] {s : Shape} (x : Rep α s) (i : Coord s) (value : α) : (x.set i value).get i = value

Reading a coordinate immediately after replacing it returns the new value.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.get_modify_self {α : Type u} [Storage α] [Storage.Update α] {s : Shape} (x : Rep α s) (i : Coord s) (f : α → α) : (x.modify i f).get i = f (x.get i)

Reading a coordinate after modifying it returns the transformed old value.

theorem TorchLean.Tensor.Internal.Rep.ext {α : Type u} [storage : Storage α] {s : Shape} {x y : Rep α s} (h : ∀ (i : Coord s), x.get i = y.get i) : x = y

Two native tensors are equal when all of their coordinate observations agree.

theorem TorchLean.Tensor.Internal.Rep.ext_iff {α : Type u} [storage : Storage α] {s : Shape} {x y : Rep α s} : x = y ↔ ∀ (i : Coord s), x.get i = y.get i