Einsum reports

This module reports checked axes, contraction work, generated loops, and the correctness chain for concrete einsum certificates.

Optimization descriptions are reconstructed from current shapes, scalar instances, and planning policies. This report does not inspect the supplied kernel body or record which optimizations its elaborator actually selected; those descriptions are not an execution trace.

def TorchLean.Tensor.Internal.Report.Impl.concreteEinsumReport (checked scalarType : Lean.Expr) (correctnessTheorem : String) : Lean.MetaM (Option String)

Decode a concrete einsum certificate into its axis analysis, semantic stages, generated loops, and correctness chain.