Certified parallel output assembly

Large concrete einsums may compute any ordered partition of the outer output axis concurrently. This module proves that task execution followed by source-order assembly produces the same row-major array as sequential traversal.

Parallelism never enters a scalar contraction. Every output value therefore uses the original reduction order, including for floating-point scalars.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.parallelBuffer {α : Type u} [storage : Storage α] : List (Unit → Storage.Buffer α) → Storage.Buffer α

Run an arbitrary number of independent physical-buffer producers and append their results in source order.

The first producer runs on the calling thread and may reserve capacity for the complete result. Every remaining producer enters Lean's task pool before the first chunk is evaluated.

theorem TorchLean.Tensor.Internal.Elab.Impl.parallelBuffer_eq_foldl {α : Type u} [storage : Storage α] (parts : List (Unit → Storage.Buffer α)) : parallelBuffer parts = List.foldl (fun (output : Storage.Buffer α) (part : Unit → Storage.Buffer α) => appendBuffer (part ()) output) (Storage.emptyWithCapacity 0) parts

Task execution has the same value as evaluating and appending all chunk producers sequentially.

theorem TorchLean.Tensor.Internal.Elab.Impl.coordinateFoldl_push_outerRange_eq_array_ofFn {α : Type u} [storage : Storage α] (outer start count : ℕ) (shape : Shape) (hRange : start + count ≤ outer) (values : Fin (Shape.size (outer :: shape)) → α) : Storage.toArray (coordinateFoldl (count :: shape) (fun (output : Storage.Buffer α) (coordinate : Coord (count :: shape)) => Storage.push output (values (Coord.linearize (⟨start + ↑coordinate.1, ⋯⟩, coordinate.2)))) (Storage.emptyWithCapacity (count * shape.size))) = Array.ofFn (flatRange (Shape.size (outer :: shape)) (start * shape.size) (count * shape.size) ⋯ values)

Folding one contiguous range of the outer axis constructs the corresponding contiguous range of the full row-major output.

theorem TorchLean.Tensor.Internal.Elab.Impl.parallelBuffer_toArray_eq_array_ofFn {α : Type u} [storage : Storage α] {total : ℕ} {values : Fin total → α} {parts : List (Unit → Storage.Buffer α)} (partition : OrderedFlatPartition total values 0 parts) : Storage.toArray (parallelBuffer parts) = Array.ofFn values

Any certified ordered partition, evaluated through parallelBuffer, reconstructs the original finite-function array.