Proof-producing einsum output fusion #
This module recognizes a scalar-register contraction immediately consumed by an output append. It emits the fused loop together with an equality proof to the ordinary tiled append.
def
TorchLean.Tensor.Internal.Elab.Impl.fuseNativeFinSumPush
(tileWidth : ℕ)
(output rawTile emittedTile : Lean.Expr)
(finalizers : List Lean.Expr)
:
Fuse a scalarized tiled contraction with the output-buffer append that immediately consumes it.
When finalizers is nonempty, each lane function is applied only after its
scalar accumulator is complete. Leading generated lets remain outside the
fused call. The returned certificate identifies the direct append with the
original tiled push expression.