Certified contiguous output partitions

This module proves the general array theorem used by task-parallel einsum output generation. A partition may contain any number of adjacent chunks. Folding their arrays together in source order reconstructs the original finite function exactly.

structure TorchLean.Tensor.Internal.Elab.Impl.CertifiedFlatBuffer {α : Type u} [storage : Storage α] (length : ℕ) (values : Fin length → α) : Type u

One named physical output buffer together with its complete finite-function semantics.

Generated sequential kernels name this record as one auxiliary definition. Executable code projects produce, while certificates project toArray_produce; neither side needs to unfold the complete native loop.

• produce : Unit → Storage.Buffer α

  Produce the complete physical output buffer.

• toArray_produce : Storage.toArray (self.produce ()) = Array.ofFn values

  Observing the produced buffer gives the complete finite function.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.flatRange {α : Type u} (total start length : ℕ) (hRange : start + length ≤ total) (values : Fin total → α) : Fin length → α

Select a contiguous subrange of a finite function.

The range proof is erased. At runtime this adds start to the local index and reads the corresponding value.

structure TorchLean.Tensor.Internal.Elab.Impl.CertifiedFlatPart {α : Type u} [storage : Storage α] (total start length : ℕ) (hRange : start + length ≤ total) (values : Fin total → α) : Type u

One named parallel chunk together with its exact finite-function semantics.

Generated code names this record as one auxiliary definition. Executable code projects produce, while certificates project toArray_produce; neither side needs to unfold the named chunk body.

• produce : Unit → Storage.Buffer α

  Produce the physical buffer for this contiguous range.

• toArray_produce : Storage.toArray (self.produce ()) = Array.ofFn (flatRange total start length hRange values)

  Observing the produced buffer gives exactly the selected range.

inductive TorchLean.Tensor.Internal.Elab.Impl.OrderedFlatPartition {α : Type u} [storage : Storage α] (total : ℕ) (values : Fin total → α) : ℕ → List (Unit → Storage.Buffer α) → Prop

An ordered list of chunk producers covering the interval from start through total.

Each producer returns exactly one contiguous physical-buffer range, and the recursive index ensures that adjacent ranges have no gap or overlap. The final constructor requires the accumulated start to equal total, so the partition is complete.

• done {α : Type u} [storage : Storage α] {total : ℕ} {values : Fin total → α} : OrderedFlatPartition total values total []

  The empty suffix completes a partition once its start reaches total.

• next {α : Type u} [storage : Storage α] {total : ℕ} {values : Fin total → α} {start length : ℕ} {parts : List (Unit → Storage.Buffer α)} (part : Unit → Storage.Buffer α) (hRange : start + length ≤ total) (hPart : Storage.toArray (part ()) = Array.ofFn (flatRange total start length hRange values)) (tail : OrderedFlatPartition total values (start + length) parts) : OrderedFlatPartition total values start (part :: parts)

  Prepend one certified contiguous producer to a partition of the remaining interval.

@[inline]

def TorchLean.Tensor.Internal.Elab.Impl.appendBuffer {α : Type u} [storage : Storage α] (source output : Storage.Buffer α) : Storage.Buffer α

Append a complete physical source buffer to a physical output buffer.

theorem TorchLean.Tensor.Internal.Elab.Impl.toArray_appendBuffer {α : Type u} [storage : Storage α] (source output : Storage.Buffer α) : Storage.toArray (appendBuffer source output) = Storage.toArray output ++ Storage.toArray source

Observing a complete physical-buffer append gives ordinary array append.

theorem TorchLean.Tensor.Internal.Elab.Impl.appendBuffer_empty {α : Type u} [storage : Storage α] (source : Storage.Buffer α) : appendBuffer source (Storage.emptyWithCapacity 0) = source

Appending to a fresh empty physical buffer returns the source buffer.

theorem TorchLean.Tensor.Internal.Elab.Impl.OrderedFlatPartition.foldl_append_eq_array_ofFn {α : Type u} [storage : Storage α] {total start : ℕ} {values : Fin total → α} {parts : List (Unit → Storage.Buffer α)} (partition : OrderedFlatPartition total values start parts) (initial : Storage.Buffer α) (hStart : start ≤ total) (hInitial : Storage.toArray initial = Array.ofFn (flatRange total 0 start ⋯ values)) : Storage.toArray (List.foldl (fun (output : Storage.Buffer α) (part : Unit → Storage.Buffer α) => appendBuffer (part ()) output) initial parts) = Array.ofFn values

Appending every producer in an ordered partition after an existing prefix reconstructs the complete finite-function array.