Certified native flat pullbacks

This module compiles a certified output-to-source flat map into one native output loop and direct source-buffer reads. Rearrangement, repetition, and other shape-only transformations use this operation-independent lowering.

The generated term carries its pointwise equality to Rep.pullFlat. Concrete portable output sizes use USize counters. Source reads use native indices only when their bounds can also be certified; otherwise they retain bounded Fin reads. Symbolic output sizes use the general lowering.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativePullFlat? (outputShape sourceTensor flatMap : Lean.Expr) (nativeSourceDimensions? : Option (List Lean.Expr) := none) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Compile one flat pullback to a certified native tensor fill when the output length is a portable concrete value.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativeTransform? (checked hAxes inputFlatMap sourceTensor reference hSemanticReference : Lean.Expr) (hasPrecedingTransform : Bool) (concreteChecked? : Option Check.CheckedTransform := none) : Lean.Elab.TermElabM (Option Lean.Expr)

Compile a checked rearrangement or repeat, including any preceding shape-only chain, to one certified native output loop.