Concrete pack and unpack checking

The packing pattern has a fixed leading region, one *, and a fixed trailing region. Inputs may have different ranks because * captures an arbitrary middle shape. A checked plan records the common fixed shapes and proves that every component decomposes as

leadingShape ++ starShape ++ trailingShape.

The same CheckedPack certificate serves both directions. checkPack rejects an empty input family and obtains the fixed shapes from its first tensor. checkUnpack obtains them from the packed tensor, resolves requested star shapes, and therefore also represents the strict empty-metadata case when the packed axis has length zero.

Requested unpack dimensions are integers so -1 can denote one inferred dimension. Every other dimension must be nonnegative. Resolution rejects multiple inferred dimensions, non-divisible residual lengths, underdetermined zero products, and metadata whose segment lengths do not exactly partition the packed axis.

def TorchLean.Tensor.Internal.Check.packFixedRank (pattern : Syntax.PackPattern) : ℕ

The number of fixed axes surrounding * in a packing pattern.

def TorchLean.Tensor.Internal.Check.packStarShape (pattern : Syntax.PackPattern) (inputShape : Shape) : Shape

The middle shape captured by * in one component.

Checked components have enough dimensions for both fixed regions. The subtraction therefore removes exactly those regions.

structure TorchLean.Tensor.Internal.Check.CheckedPack : Type

A pack/unpack shape plan with exactly the invariants used by semantics.

leadingShape and trailingShape are explicit because strict unpacking may produce an empty component family, from which the fixed dimensions cannot be recovered. Component star shapes, segment lengths, metadata, offsets, and the packed output shape remain deterministic derived values.

• pattern : Syntax.PackPattern

  Parsed packing pattern shared by pack and unpack.

• inputShapes : List Shape

  Shapes of the unpacked components, in segment order.

• leadingShape : Shape

  Fixed dimensions preceding every component's star region.

• trailingShape : Shape

  Fixed dimensions following every component's star region.

• leading_rank : List.length self.leadingShape = self.pattern.before.length

  The stored leading shape has the rank written before *.

• trailing_rank : List.length self.trailingShape = self.pattern.after.length

  The stored trailing shape has the rank written after *.

• input_shapes (component : Fin self.inputShapes.length) : self.inputShapes.get component = self.leadingShape ++ packStarShape self.pattern (self.inputShapes.get component) ++ self.trailingShape

  Every component decomposes into the shared prefix, its star region, and suffix.

def TorchLean.Tensor.Internal.Check.CheckedPack.starShape (checked : CheckedPack) (component : Fin checked.inputShapes.length) : Shape

The middle shape represented by one checked component.

def TorchLean.Tensor.Internal.Check.CheckedPack.metadata (checked : CheckedPack) : List Shape

Pack metadata in component order.

def TorchLean.Tensor.Internal.Check.CheckedPack.segmentLengths (checked : CheckedPack) : List ℕ

Flattened lengths of all packed middle regions.

def TorchLean.Tensor.Internal.Check.CheckedPack.packedAxisLength (checked : CheckedPack) : ℕ

The length of the concatenated packed axis.

def TorchLean.Tensor.Internal.Check.CheckedPack.output (checked : CheckedPack) : Shape

Shape of the packed tensor.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.metadata_length (checked : CheckedPack) : checked.metadata.length = checked.inputShapes.length

Pack metadata has one entry for every input component.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.segmentLengths_length (checked : CheckedPack) : checked.segmentLengths.length = checked.inputShapes.length

Segment lengths have one entry for every input component.

def TorchLean.Tensor.Internal.Check.CheckedPack.componentSegmentEquiv (checked : CheckedPack) : Fin checked.inputShapes.length ≃ Fin checked.segmentLengths.length

Match each input component with its metadata segment.

The two lists have equal length by construction. Naming this equivalence keeps the dependent component-to-segment transport identical in checking, semantics, and lowering.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.componentSegmentEquiv_val (checked : CheckedPack) (component : Fin checked.inputShapes.length) : ↑(checked.componentSegmentEquiv component) = ↑component

Matching a component with its metadata segment preserves its position in the component list.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.metadata_get (checked : CheckedPack) (component : Fin checked.metadata.length) : checked.metadata[↑component] = checked.starShape (Fin.cast ⋯ component)

Metadata at a component index is its checked star shape.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.segmentLengths_get (checked : CheckedPack) (segment : Fin checked.segmentLengths.length) : checked.segmentLengths[↑segment] = (checked.starShape (Fin.cast ⋯ segment)).size

A segment length is the row-major size of its metadata shape.

@[simp]

theorem TorchLean.Tensor.Internal.Check.CheckedPack.segmentLength_eq_star_size (checked : CheckedPack) (component : Fin checked.inputShapes.length) : checked.segmentLengths[↑component] = (checked.starShape component).size

The segment selected by an input component has the row-major size of that component's star region.

theorem TorchLean.Tensor.Internal.Check.CheckedPack.segmentLengths_get_componentSegmentEquiv (checked : CheckedPack) (component : Fin checked.inputShapes.length) : checked.segmentLengths.get (checked.componentSegmentEquiv component) = (checked.starShape component).size

Looking up the metadata segment selected for a component yields the size of that component's star region.

theorem TorchLean.Tensor.Internal.Check.CheckedPack.metadata_eq_ofFn (checked : CheckedPack) : checked.metadata = List.ofFn fun (component : Fin checked.inputShapes.length) => checked.starShape component

Pack metadata is exactly the checked star-shape family in input order.

This extensional form is useful when clients consume metadata through finite component indices rather than list lookup.

theorem TorchLean.Tensor.Internal.Check.CheckedPack.input_size_eq_flattened (checked : CheckedPack) (component : Fin checked.inputShapes.length) : (checked.inputShapes.get component).size = (checked.leadingShape ++ (checked.starShape component).size :: checked.trailingShape).size

Flattening the star region into one axis preserves every component's number of scalar entries.

theorem TorchLean.Tensor.Internal.Check.CheckedPack.input_size_eq_segment (checked : CheckedPack) (component : Fin checked.inputShapes.length) : (checked.inputShapes.get component).size = (checked.leadingShape ++ checked.segmentLengths.get (checked.componentSegmentEquiv component) :: checked.trailingShape).size

Reshaping one input component to its checked segment shape preserves the number of entries.

def TorchLean.Tensor.Internal.Check.Pack.Impl.checkPackComponents (pattern : Syntax.PackPattern) (leadingShape trailingShape : Shape) : List Shape → ℕ → Result Unit

Validate rank and fixed-prefix/suffix agreement for every component in a pack family.

def TorchLean.Tensor.Internal.Check.Pack.Impl.certifyPackComponents (pattern : Syntax.PackPattern) (inputShapes : List Shape) (leadingShape trailingShape : Shape) : Result CheckedPack

Bundle validated component decompositions into the dependent CheckedPack certificate consumed by semantics and lowering.

def TorchLean.Tensor.Internal.Check.checkPack (pattern : Syntax.PackPattern) (inputShapes : List Shape) : Result CheckedPack

Check a nonempty family of tensor shapes for packing.

The first component determines fixed leading and trailing dimensions. Every other component must agree at those positions, while its star region may have any finite shape, including an empty shape or zero dimensions.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Check.RequestedShapes : Type

Integer star shapes accepted by the public unpack checker.

def TorchLean.Tensor.Internal.Check.Pack.Impl.requestedShapeProduct (requestedShape : List ℤ) : ℕ

Compute one fully specified requested star-shape size.

def TorchLean.Tensor.Internal.Check.Pack.Impl.requestedKnownFactor (requestedShape : List ℤ) : ℕ

Multiply the known factors of a requested shape, treating -1 as unknown.

def TorchLean.Tensor.Internal.Check.Pack.Impl.requestedInferredCount (requestedShapes : RequestedShapes) : ℕ

Count inferred -1 dimensions across the complete unpack request.

def TorchLean.Tensor.Internal.Check.Pack.Impl.resolveRequestedShapesWith (inferred : ℕ) (requestedShapes : RequestedShapes) : List Shape

Replace the unique inferred dimension by its resolved natural-number value.

def TorchLean.Tensor.Internal.Check.Pack.Impl.firstInvalidRequestedDimension? : RequestedShapes → Option ℤ

Find the first unpack dimension smaller than the permitted sentinel -1.

def TorchLean.Tensor.Internal.Check.resolveUnpackShapes (span : Syntax.Span) (packedAxisLength : ℕ) (requestedShapes : RequestedShapes) : Result (List Shape)

Resolve requested unpack metadata against one concrete packed-axis length.

The result contains only natural-number shapes. Success guarantees computationally that their products sum to the packed-axis length; the subsequent checked plan turns that equality into the segment partition used by semantics.

def TorchLean.Tensor.Internal.Check.checkUnpack (pattern : Syntax.PackPattern) (packedShape : Shape) (requestedShapes : RequestedShapes) : Result CheckedPack

Check strict unpack metadata against a concrete packed tensor shape.

Unlike the reference implementation's backend-deferred failures, every segment bound and reshape size is validated before tensor execution.