TensorBridge

Computable, row-major conversions between TensorArray.Tensor and Spec.Tensor.

Why we have this file:

• Spec.Tensor is the spec representation (functional, shape-indexed).
• TensorArray.Tensor is an array-backed representation that is convenient for IO and external interfaces (CSV/NPY/etc).

This bridge gives explicit, easy-to-audit conversions:

• flatten / unflatten between Spec.Tensor and a flat row-major list,
• plus shape list conversions (Shape ↔ List Nat) to connect the typed and runtime views.

Why “row-major”?

Our spec tensor datatype is a nested dim tree: outer dimensions are modeled as functions Fin n → .... Our flatten recursion iterates outer indices first and then recurses inward, so the last axis varies fastest (the conventional row-major / C-order layout for matrices and images when you think of the outer dimension as “rows”).

We could have picked a different order, but we need one consistent convention for interop (CSV/NPY, torch tensor serialization, etc.). Row-major matches the contiguous layout assumptions used in many toolchains, so it’s a practical default.

Notes for proofs

We don’t want “conversion code” to be a place where meaning quietly changes. So we prove the basic round-trip facts:

• flattening after unflattening gives you the original list, and
• unflattening after flattening gives you the original tensor.

Those lemmas let us move between the functional spec view and the array/list view without handwaving.

Example file: NN.Examples.Advanced.Tensor.TensorBridge.

References / analogies:

• Row-major ("C-order") is the default contiguous layout in many toolchains (NumPy/PyTorch) and is a common convention for serialization. This file fixes a single convention so interop is auditably well-defined.
• PyTorch docs (intuition for the operations we mirror here, not the semantics):
  • torch.flatten: https://pytorch.org/docs/stable/generated/torch.flatten.html
  • torch.Tensor.reshape: https://pytorch.org/docs/stable/generated/torch.Tensor.reshape.html
  • torch.Tensor.view: https://pytorch.org/docs/stable/generated/torch.Tensor.view.html
  • torch.Tensor.contiguous: https://pytorch.org/docs/stable/generated/torch.Tensor.contiguous.html
• NumPy docs (C-order / reshape conventions):
  • numpy.reshape: https://numpy.org/doc/stable/reference/generated/numpy.reshape.html

def TensorBridge.shapeToList : Spec.Shape → List ℕ

Convert a Shape to a runtime list of dimensions.

def TensorBridge.listToShape : List ℕ → Spec.Shape

Convert a runtime list of dimensions to a Shape.

theorem TensorBridge.shapeToList_listToShape_involutive (s : Spec.Shape) : listToShape (shapeToList s) = s

Shape conversion is involutive (applying it twice gives the original).

theorem TensorBridge.listToShape_shapeToList_involutive (shape : List ℕ) : shapeToList (listToShape shape) = shape

List-to-shape conversion is involutive.

def TensorBridge.flatten {α : Type} {shape : List ℕ} : Spec.Tensor α (listToShape shape) → List α

Flatten a Spec.Tensor of list-shape to row-major list.

theorem TensorBridge.flatten_length {α : Type} {shape : List ℕ} (t : Spec.Tensor α (listToShape shape)) : (flatten t).length = TensorArray.shapeProd shape

Length of flatten is exactly the product of dimensions.

theorem TensorBridge.length_take_drop_mul {α : Type} (xs : List α) {n k : ℕ} (h : xs.length = n * k) (i : Fin n) : (List.take k (List.drop (↑i * k) xs)).length = k

A block slice of size k has length k when the full list has length n*k.

def TensorBridge.unflatten {α : Type} (shape : List ℕ) (xs : List α) : xs.length = TensorArray.shapeProd shape → Spec.Tensor α (listToShape shape)

Unflatten a row-major list into a Spec.Tensor of list-shape.

theorem TensorBridge.flatMap_drop_take_eq {α : Type} (n k : ℕ) (xs : List α) (h : xs.length = n * k) : List.flatMap (fun (i : Fin n) => List.take k (List.drop (↑i * k) xs)) (List.finRange n) = xs

Reconstruct a list by concatenating its k-sized blocks.

theorem TensorBridge.flatten_unflatten {α : Type} {shape : List ℕ} (xs : List α) (h : xs.length = TensorArray.shapeProd shape) : flatten (unflatten shape xs h) = xs

Flatten after unflatten returns the original list.

theorem TensorBridge.unflatten_flatten {α : Type} {shape : List ℕ} (t : Spec.Tensor α (listToShape shape)) {h : (flatten t).length = TensorArray.shapeProd shape} : unflatten shape (flatten t) h = t

Unflatten after flatten returns the original tensor (for any valid length proof).

def TensorBridge.toTensor {α : Type} {shape : List ℕ} : TensorArray.Tensor α shape → Spec.Tensor α (listToShape shape)

Convert from TensorArray.Tensor to Spec.Tensor.

def TensorBridge.toTensorArray {α : Type} {shape : List ℕ} : Spec.Tensor α (listToShape shape) → TensorArray.Tensor α shape

Convert from Spec.Tensor to TensorArray.Tensor.

theorem TensorBridge.to_tensor_array_to_tensor {α : Type} {shape : List ℕ} (t : TensorArray.Tensor α shape) : toTensorArray (toTensor t) = t

Converting to tensor and back preserves the original tensor array.

theorem TensorBridge.to_tensor_to_tensor_array {α : Type} {shape : List ℕ} (t : Spec.Tensor α (listToShape shape)) : toTensor (toTensorArray t) = t

Converting to tensor array and back preserves the original tensor.

def TensorBridge.tensorArrayEquivTensor (α : Type) (shape : List ℕ) : TensorArray.Tensor α shape ≃ Spec.Tensor α (listToShape shape)

A definable equivalence between the two tensor representations.