Tensor Shape-Erasure Boundary

Conversions between statically shape-indexed TensorPack values and arrays of existentially packaged Spec.SomeTensor values. Runtime tapes and heterogeneous external data use the erased representation; typed computation should recover a TensorPack immediately after crossing that boundary.

def TorchLean.TensorPack.toShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → Array (Spec.SomeTensor α)

Erase the individual tensor shapes in a typed pack into a runtime array.

def TorchLean.TensorPack.toIndexedShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} : TensorPack α ss → ℕ → Array (ℕ × Spec.SomeTensor α)

Tag each shape-erased tensor with its runtime index, beginning at start.

def TorchLean.TensorPack.ofShapeErasedArray {α : Type} [Storage α] (values : Array (Spec.SomeTensor α)) (start : ℕ := 0) {shapes : List Spec.Shape} : Except String (TensorPack α shapes)

Recover a statically shape-indexed pack from a prefix of a shape-erased runtime array.

start selects the first array entry to consume. The conversion checks every stored shape and fails if the array is too short or an entry has the wrong shape. Entries after the requested pack are intentionally ignored, which supports recovering a typed prefix of a larger runtime context.