Certified loops used by generated einsum kernels #
Literal einsums execute concrete traversals with USize counters whenever
the corresponding semantic length fits every Lean target. This module keeps
the loop implementation and its correctness theorems separate from syntax
elaboration.
Each optimized primitive has a theorem identifying it with the standard
Fin.foldl, Array.ofFn, or row-major coordinate operation used by the
mathematical lowering. The proof arguments erase during code generation, so
the generated loop carries only its native bound, counter, and accumulator.
Recombining a native quotient and remainder recovers the original index.
This theorem is kept out of the global simplifier. The einsum compiler uses it only for row-major indices that it generated itself.
Converting a native sum to Nat preserves a certified nonwrapping sum.
Converting a native product to Nat preserves a certified nonwrapping
product.
Native subtraction respects certified operand values when the subtrahend is no larger than the minuend.
A native strict comparison transports to the corresponding natural-number comparison when both operand values are certified.
The false branch of a native strict comparison transports to the corresponding natural-number lower bound when both operand values are certified.
Decode and immediately re-encode a native row-major coordinate before adding an invariant index base.
Decode and immediately re-encode a native row-major coordinate with a stride before adding an invariant index base.
This is the form produced for a flattened contraction coordinate inside an operand whose contracted axes are not the final physical dimensions.
Native remainder decoding agrees with the remainder coordinate of a finite row-major product index.
Projecting the state of a finite fold is equivalent to folding the projected state whenever one step commutes with the projection.
Fold over a tensor shape in row-major coordinate order.
This definition is the proof-level reference for generated loop nests. The einsum compiler emits the same recursion directly, choosing a native counter independently for each concrete axis.
Instances For
Converting a row-major product coordinate to USize exposes the native
multiplication and addition used to construct it.
The semantic certificate retains Fin.mkDivMod; generated indices use the
equivalent word-sized arithmetic.
Fixed-width blocks followed by a tail enumerate exactly the original finite
index interval. The theorem changes only loop nesting; it preserves the order
in which step observes indices.
The recursive coordinate fold is exactly the standard flat finite fold.
This theorem supplies the arbitrary-rank certificate for generated output loops. In particular, the empty shape executes once and any zero-length axis executes no leaves.
Projecting the state of a row-major coordinate fold is equivalent to folding the projected state when every coordinate update commutes with the projection.
Pushing entries through the row-major coordinate fold constructs the standard flat function array.
Observing a physical-buffer coordinate fold gives the standard flat function array.
A one-axis output loop observes directly as its row-major function array.
This specialized certificate avoids normalizing the recursive coordinate fold
when a tiled output compiler already emits the single Fin.foldl explicitly.
Transport a certified one-axis physical-buffer loop directly to its ordinary array observation.