Verified contraction-loop generation

The contraction compiler is organized as certified native-index normalization, loop-invariant motion, scalar-register lowering, flat coordinate traversal, and arbitrary-rank coordinate folds; this module is the last of those stages and is what importers of the contraction compiler name.

This module compiles arbitrary-rank coordinate folds and sums to certified native loops. Concrete, symbolic, flattened, and compile-time-unrolled axes all share the same finite-fold correctness boundary.

def TorchLean.Tensor.Internal.Elab.Impl.compileCoordinateFold (lengths : List Lean.Expr) (step initial reference : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Compile a statically shaped coordinate-state fold into verified native loops.

The loop nest is constructed directly from the reflected dimension list. Tiny literal axes are expanded within a fixed code-size budget. Other concrete lengths that fit every Lean target use unboxed USize counters; symbolic or oversized lengths retain Fin.foldl. Every optimized loop carries a proof that it equals the corresponding standard fold. Simplification then cancels coordinate wrappers and a final pass floats staged index bases out of inner loops.

def TorchLean.Tensor.Internal.Elab.Impl.compileCoordinateSum (lengths : List Lean.Expr) (values initial reference : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Compile a statically shaped coordinate sum into verified native loops.

This wrapper instantiates the general state-fold compiler with scalar addition, then transports its certificate to Semantics.coordinateSum.