Permutation Operators

Semantic-preservation lemmas for permutation-style operators in the IR-to-compiled-runtime bridge.

This file covers the IR .permute perm node kind. The compiler lowers a permutation to a swap-depth program (a list of axis swaps). The proof below mirrors that lowering: it validates the permutation witness and computed swaps, constructs the compiled forward closure in terms of applySwapsTensor, then rewrites the IR evaluator's permuteDVal to the same swap-based implementation via permuteDVal_eq_applySwapsTensor.

Build note: permutation proofs are slow because a permutation changes both tensor data and the type level shape. The proof therefore has to relate a dynamic IR permutation to the compiled swap program while keeping casts proof-irrelevant. The swap-program lemmas should stay small and avoid redoing permutation arithmetic inside the compiler branch proof.

theorem Runtime.Autograd.Compiled.buildFrom_denoteAllFrom_permute {α : Type} [Context α] [DecidableEq Spec.Shape] (g : NN.IR.Graph) (payload : NN.IR.Payload α) {inShape : Spec.Shape} {ss : List Spec.Shape} (gd : Proofs.Autograd.Algebra.GraphData α Unit [inShape] ss) (i : ℕ) (st' : IRExec.State α inShape) (x : Spec.Tensor α inShape) (n : NN.IR.Node) (perm : List ℕ) (hN : g.getNode i = Except.ok n) (hk : n.kind = NN.IR.OpKind.permute perm) (hi : i < g.nodes.size) (hBuild : IRExec.buildFrom g payload inShape i ⟨ss, gd⟩ = Except.ok st') (ih : ∀ (st1 : IRExec.State α inShape), IRExec.buildFrom g payload inShape (i + 1) st1 = Except.ok st' → g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) (i + 1) (denoteAllState inShape st1 x) = Except.ok (denoteAllState inShape st' x)) : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) i (denoteAllState inShape ⟨ss, gd⟩ x) = Except.ok (denoteAllState inShape st' x)

Semantic-preservation lemma for .permute perm lowering.