Slice / gather / split operator bounds

This file provides IBP and affine transfer rules for a small subset of indexing-like operations:

• Slice: extract a contiguous range [start, stop) from a flattened vector,
• Gather: select entries by static indices (List Nat), and
• Split: split a flattened vector into a list of parts.

Important limitation: this does not model tensor-valued index dtypes inside the differentiable graph (i.e. no PyTorch-style LongTensor indexing/gather/scatter driven by data tensors).

def NN.MLTheory.CROWN.Operators.Slice.getDimScalarFn {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Fin n → Spec.Tensor α Spec.Shape.scalar

View a (.dim n .scalar) tensor as its underlying Fin n → Tensor α .scalar function.

def NN.MLTheory.CROWN.Operators.Slice.ibpSlice? {α : Type} [Context α] (xB : FlatBox α) (start stop : ℕ) : Option (FlatBox α)

IBP for Slice: extract elements [start, stop) from a flattened vector. Slice is a linear operation, so bounds propagate exactly.

def NN.MLTheory.CROWN.Operators.Slice.ibpGather? {α : Type} [Context α] (xB : FlatBox α) (indices : List ℕ) : Option (FlatBox α)

IBP for Gather: index into a vector using integer indices.

For input $x$ and a concrete index vector, the output satisfies $y_j=x_{\mathrm{indices}[j]}$. This is a permutation or selection.

def NN.MLTheory.CROWN.Operators.Slice.ibpSplit? {α : Type} [Context α] (xB : FlatBox α) (splitSizes : List ℕ) : Option (List (FlatBox α))

IBP for Split: split a vector into multiple parts. Returns a list of FlatBoxes, one for each split.

def NN.MLTheory.CROWN.Operators.Slice.ibpSplit?.buildSplits {α : Type} [Context α] (xB : FlatBox α) (flo fhi : Fin xB.dim → Spec.Tensor α Spec.Shape.scalar) (remaining : List ℕ) (offset : ℕ) : List (FlatBox α)

def NN.MLTheory.CROWN.Operators.Slice.affSlice? {α : Type} [Context α] {inDim outDim : ℕ} (start sliceSize : ℕ) (aff : AffineVec α inDim outDim) : Option (AffineVec α inDim sliceSize)

Affine bounds for Slice: extract a subvector of an affine form.

If the input represents $y=Ax+c$, slicing selects the corresponding rows of $A$ and entries of $c$.

def NN.MLTheory.CROWN.Operators.Slice.affGather? {α : Type} [Context α] {inDim outDim : ℕ} (indices : List ℕ) (aff : AffineVec α inDim outDim) : Option (AffineVec α inDim indices.length)

Affine bounds for Gather: permute/select rows of affine form.

def NN.MLTheory.CROWN.Operators.Slice.derivSlice? {α : Type} [Context α] (dB : FlatBox α) (start stop : ℕ) : Option (FlatBox α)

Derivative bounds for Slice: derivatives just slice through.

def NN.MLTheory.CROWN.Operators.Slice.derivGather? {α : Type} [Context α] (dB : FlatBox α) (indices : List ℕ) : Option (FlatBox α)

Derivative bounds for Gather: derivatives follow the same indexing.

def NN.MLTheory.CROWN.Operators.Slice.ibpConcat {α : Type} [Context α] (boxes : List (FlatBox α)) : FlatBox α

Concatenate multiple FlatBoxes into one.