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 : ℕ) : 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 ℕ) : FlatBox α

IBP for Gather: index into a vector using integer indices. Given input x and indices i, output[j] = x[indices[j]]. Since indices are concrete, this is a permutation/selection.

def NN.MLTheory.CROWN.Operators.Slice.ibpSplit {α : Type} [Context α] (xB : FlatBox α) (splitSizes : List ℕ) : 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 : ℕ) (aff : AffineVec α inDim outDim) (sliceSize : ℕ) : AffineVec α inDim sliceSize

Affine bounds for Slice: extract subvector of affine form. If aff represents y = A·x + c, then slice just selects rows of A and c.

def NN.MLTheory.CROWN.Operators.Slice.affGather {α : Type} [Context α] {inDim outDim : ℕ} (indices : List ℕ) (aff : AffineVec α inDim outDim) : 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 : ℕ) : FlatBox α

Derivative bounds for Slice: derivatives just slice through.

def NN.MLTheory.CROWN.Operators.Slice.derivGather {α : Type} [Context α] (dB : FlatBox α) (indices : List ℕ) : 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.

theorem NN.MLTheory.CROWN.Operators.Slice.Theorems.ibp_slice_dim {α : Type} [Context α] (xB : FlatBox α) (start stop : ℕ) (hvalid : start < stop ∧ stop ≤ xB.dim) : (ibpSlice xB start stop).dim = stop - start

Slice output dimension matches stop - start for valid inputs.

theorem NN.MLTheory.CROWN.Operators.Slice.Theorems.ibp_slice_returns_box {α : Type} [Context α] (xB : FlatBox α) (start stop : ℕ) : ∃ (dim : ℕ) (lo : Spec.Tensor α (Spec.Shape.dim dim Spec.Shape.scalar)) (hi : Spec.Tensor α (Spec.Shape.dim dim Spec.Shape.scalar)), ibpSlice xB start stop = { dim := dim, lo := lo, hi := hi }

Slice produces valid FlatBox structure.

theorem NN.MLTheory.CROWN.Operators.Slice.Theorems.ibp_gather_dim {α : Type} [Context α] (xB : FlatBox α) (indices : List ℕ) : (ibpGather xB indices).dim = indices.length

Gather output dimension equals indices length.

theorem NN.MLTheory.CROWN.Operators.Slice.Theorems.ibp_split_returns_list {α : Type} [Context α] (xB : FlatBox α) (splitSizes : List ℕ) (box : FlatBox α) : box ∈ ibpSplit xB splitSizes → ∃ (dim : ℕ) (lo : Spec.Tensor α (Spec.Shape.dim dim Spec.Shape.scalar)) (hi : Spec.Tensor α (Spec.Shape.dim dim Spec.Shape.scalar)), box = { dim := dim, lo := lo, hi := hi }

Split produces list of valid FlatBoxes.

theorem NN.MLTheory.CROWN.Operators.Slice.Theorems.ibp_concat_dim {α : Type} [Context α] (boxes : List (FlatBox α)) : (ibpConcat boxes).dim = List.foldl (fun (acc : ℕ) (b : FlatBox α) => acc + b.dim) 0 boxes ∨ (ibpConcat boxes).dim = 0

Concat output dimension is sum of input dimensions.