Certified row-major index specialization

Checked operations express source indices through compact row-major programs. This module partially evaluates those programs while elaborating a concrete operation and returns an equality certificate for the specialized arithmetic.

def TorchLean.Tensor.Internal.Elab.Impl.nativeLoopIndexBound (index hNativeBound hIndexBound : Lean.Expr) : Lean.MetaM Lean.Expr

Transport one loop-index bound from a checked shape to its concrete native counter bound before arithmetic certification.

def TorchLean.Tensor.Internal.Elab.Impl.rowMajorIndexSimpContext (extraDeclarations : Array Lean.Name := #[]) : Lean.MetaM Lean.Meta.Simp.Context

Build the shared simplifier for compact row-major index programs.

Callers may provide operation-specific definitions such as the compact reduction index. Coordinate semantics and proof fields remain opaque.

def TorchLean.Tensor.Internal.Elab.Impl.compileRowMajorIndex (index : Lean.Expr) (extraDeclarations : Array Lean.Name := #[]) : Lean.MetaM (Lean.Expr × Lean.Expr)

Partially evaluate a compact row-major index.

The returned proof is oriented from the specialized expression to the original program, ready to compose with its semantic correctness theorem.