Shape-Erased Tensors

SomeTensor stores a TorchLean.Tensor together with the shape that indexes its type. It is the sole general shape-erasure boundary for tensors in TorchLean. Runtime collections use it when they must contain tensors of different shapes, including autograd tapes, graph interpreters, and certificate checkers.

Backend-specific resources are not alternative tensor wrappers. For example, the CUDA tape keeps an opaque device buffer together with runtime shape and allocation metadata; operation-polymorphic programs similarly package references owned by a monad rather than tensor values.

structure Spec.SomeTensor (α : Type) [TorchLean.Storage α] : Type

A tensor paired with the shape that indexes its type.

• shape : Shape

  The runtime shape of the tensor.

• tensor : TorchLean.Tensor α self.shape

  The tensor value, indexed by its stored shape.

def Spec.SomeTensor.ofTensor {α : Type} [TorchLean.Storage α] {shape : Shape} (tensor : TorchLean.Tensor α shape) : SomeTensor α

Package a statically shaped tensor for shape-erased storage.

@[simp]

theorem Spec.SomeTensor.shape_ofTensor {α : Type} [TorchLean.Storage α] {shape : Shape} (tensor : TorchLean.Tensor α shape) : (ofTensor tensor).shape = shape

Packing a tensor records its static shape as the runtime shape.

@[simp]

theorem Spec.SomeTensor.tensor_ofTensor {α : Type} [TorchLean.Storage α] {shape : Shape} (tensor : TorchLean.Tensor α shape) : (ofTensor tensor).tensor = tensor

Packing and unpacking a tensor returns it unchanged, since the recorded shape matches.

def Spec.SomeTensor.cast {α : Type} [TorchLean.Storage α] {shape : Shape} (value : SomeTensor α) (h : value.shape = shape) : TorchLean.Tensor α shape

Cast the stored tensor after checking its runtime shape.

@[simp]

theorem Spec.SomeTensor.cast_self {α : Type} [TorchLean.Storage α] (value : SomeTensor α) (h : value.shape = value.shape) : value.cast h = value.tensor

Casting to the shape already recorded returns the stored tensor.

@[simp]

theorem Spec.SomeTensor.ofTensor_cast {α : Type} [TorchLean.Storage α] (value : SomeTensor α) {shape : Shape} (h : value.shape = shape) : ofTensor (value.cast h) = value

Repacking a tensor after a successful shape cast recovers the original value.

@[simp]

theorem Spec.SomeTensor.ofTensor_castShape {α : Type} [TorchLean.Storage α] {shape shape' : Shape} (tensor : TorchLean.Tensor α shape) (h : shape = shape') : ofTensor (tensor.castShape h) = ofTensor tensor

Erasing a tensor's shape after transport recovers the original shape-erased value.

def Spec.SomeTensor.swapAdjacentAtDepth {α : Type} [TorchLean.Storage α] (value : SomeTensor α) (depth : ℕ) : SomeTensor α

Swap two adjacent axes at depth, retaining the resulting shape in the package.