Shape Erasure

Bridge lemmas between the proved typed context (TensorPack) and the runtime tape representation (Spec.SomeTensor stored in Arrays).

The conversion preserves order and stores each erased shape in the resulting SomeTensor.

theorem TorchLean.TensorPack.mem_toIndexedShapeErasedArray_lt {α : Type} [Storage α] {ss : List Spec.Shape} (ts : TensorPack α ss) (start : ℕ) {pid : ℕ} {pg : Spec.SomeTensor α} : (pid, pg) ∈ ts.toIndexedShapeErasedArray start → pid < start + ss.length

Every (pid, tensor) produced by toIndexedShapeErasedArray ts start satisfies pid < start + ss.length.

This is bookkeeping used to prove runtime backward only references earlier nodes.

@[simp]

theorem TorchLean.TensorPack.toShapeErasedArray_cast {α : Type} [Storage α] {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : TensorPack α ss₁) : (cast h xs).toShapeErasedArray = xs.toShapeErasedArray

toShapeErasedArray ignores type-level casts of the shape list.

@[simp]

theorem TorchLean.TensorPack.size_toShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} (xs : TensorPack α ss) : xs.toShapeErasedArray.size = ss.length

toShapeErasedArray has the same size as the underlying shape list.

theorem TorchLean.TensorPack.ofShapeErasedArray_surround {α : Type} [Storage α] (suffix pref : Array (Spec.SomeTensor α)) {ss : List Spec.Shape} (xs : TensorPack α ss) : ofShapeErasedArray (pref ++ xs.toShapeErasedArray ++ suffix) pref.size = Except.ok xs

Recovering a typed pack ignores array entries before and after its encoded segment.

@[simp]

theorem TorchLean.TensorPack.ofShapeErasedArray_append_toShapeErasedArray {α : Type} [Storage α] (pref : Array (Spec.SomeTensor α)) {ss : List Spec.Shape} (xs : TensorPack α ss) : ofShapeErasedArray (pref ++ xs.toShapeErasedArray) pref.size = Except.ok xs

Recovering a typed pack after an untouched array prefix and shape erasure is lossless.

@[simp]

theorem TorchLean.TensorPack.ofShapeErasedArray_toShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} (xs : TensorPack α ss) : ofShapeErasedArray xs.toShapeErasedArray 0 = Except.ok xs

Recovering the expected typed pack immediately after shape erasure is lossless.

theorem TorchLean.TensorPack.toShapeErasedArray_split {α : Type} [Storage α] {left right : List Spec.Shape} (xs : TensorPack α (left ++ right)) : xs.toShapeErasedArray = xs.split.1.toShapeErasedArray ++ xs.split.2.toShapeErasedArray

Splitting a typed context splits its erased array at the same boundary.

theorem TorchLean.TensorPack.ofShapeErasedArray_toShapeErasedArray_prefix {α : Type} [Storage α] {left right : List Spec.Shape} (xs : TensorPack α (left ++ right)) : ofShapeErasedArray xs.toShapeErasedArray 0 = Except.ok xs.split.1

Recover just the typed input prefix of a complete runtime context.

Shape-erasing conversions

The lemmas below show that these conversions preserve length and order and interact well with TorchLean.TensorPack.snoc and TorchLean.TensorPack.get. They are used later to relate runtime node ids to positions in the typed proof context Γ ++ ss.

@[simp]

theorem TorchLean.TensorPack.toShapeErasedArray_snoc {α : Type} [Storage α] {ss : List Spec.Shape} {τ : Spec.Shape} (xs : TensorPack α ss) (t : Tensor α τ) : (xs.snoc t).toShapeErasedArray = xs.toShapeErasedArray.push (Spec.SomeTensor.ofTensor t)

toShapeErasedArray commutes with appending a value.

theorem TorchLean.TensorPack.toShapeErasedArray_cons {α : Type} [Storage α] {s : Spec.Shape} {ss : List Spec.Shape} (x : Tensor α s) (xs : TensorPack α ss) : (cons x xs).toShapeErasedArray = #[Spec.SomeTensor.ofTensor x] ++ xs.toShapeErasedArray

toShapeErasedArray of a cons context is array cons/append of the head element.

theorem TorchLean.TensorPack.get_toShapeErasedArray {α : Type} [Storage α] {ss : List Spec.Shape} (xs : TensorPack α ss) (i : Fin ss.length) : let arr := xs.toShapeErasedArray; arr[↑i] = Spec.SomeTensor.ofTensor (xs.get i)

Array lookup through toShapeErasedArray corresponds to TorchLean.TensorPack.get after erasing the result's shape from its type.

This is the key lemma that lets us connect runtime indexing (arr[i]) to proof indexing (get xs i).