SemanticEquivalenceCommon

Shared helper lemmas for the semantic equivalence proof in NN.Runtime.Autograd.Compiled.IRExec.Correctness.

This module contains correctness infrastructure used by the end-to-end semantic equivalence proof. We keep these lemmas separate from ...Correctness.Common because they are specific to the recursive buildFrom proof shape rather than generally useful per-op infrastructure.

Reading map:

• denoteAllState_nil: base case table lemma for the empty compiled prefix.
• permuteDVal_eq_applySwapsTensor (+ helper): connects IR permutation semantics to the runtime swap-based implementation.
• buildFrom_denoteAllFrom_{unary,binary}_exact: convenience wrappers that package the standard semantic equivalence proof pattern once a nodeData closure has been constructed.

These helpers exist because the main correctness proof is expensive to elaborate. They keep the recursive theorem from re-solving the same typed-context and dynamic-value facts for every operator. When a new proof starts to repeat parent lookup, DVal casting, or tail-of-graph preservation steps, it usually belongs here.

Maintenance note: add focused, well-named lemmas here instead of adding another large tactic block to the recursive proof.

Correctness (Semantic Equivalence Helpers)

These lemmas are shared by the branch-by-branch proof in Correctness.SemanticEquivalence.

@[simp]

theorem Runtime.Autograd.Compiled.denoteAllState_nil {α : Type} [Context α] {inShape : Spec.Shape} (x : Spec.Tensor α inShape) : denoteAllState inShape ⟨[], Proofs.Autograd.Algebra.GraphData.nil⟩ x = #[NN.IR.DVal.mk inShape x]

Base case: evaluating the empty compiled prefix yields the singleton table containing just the input.

theorem Runtime.Autograd.Compiled.applySwapsTensor_eq_foldl_applySwapDepth {α : Type} [Context α] {s : Spec.Shape} (t : Spec.Tensor α s) (swaps : List ℕ) : List.foldl (fun (acc : NN.IR.DVal α) (d : ℕ) => NN.IR.Graph.applySwapDepth acc d) (NN.IR.DVal.mk s t) swaps = NN.IR.DVal.mk (IRExec.swapShapeBySwaps s swaps) (IRExec.applySwapsTensor swaps t)

Relate the IR permutation lowering (applySwapDepth folded over swap depths) to applySwapsTensor.

This is used to connect NN.IR.Graph.permuteDVal to the runtime implementation used by the compiler-generated node.

theorem Runtime.Autograd.Compiled.permuteDVal_eq_applySwapsTensor {α : Type} [Context α] {sIn : Spec.Shape} (t : Spec.Tensor α sIn) (perm : List ℕ) (expected : Spec.Shape) (swaps : List ℕ) (hPerm : sIn.permute? perm = some expected) (hSwaps : NN.IR.Graph.swapDepthsForPerm perm sIn.rank = Except.ok swaps) : NN.IR.Graph.permuteDVal (NN.IR.DVal.mk sIn t) perm = Except.ok (NN.IR.DVal.mk (IRExec.swapShapeBySwaps sIn swaps) (IRExec.applySwapsTensor swaps t))

Specialize NN.IR.Graph.permuteDVal to the swap-based implementation used by this compiler.

Given a successful permute? witness and computed swap depths, permuteDVal returns the tensor produced by applySwapsTensor with the expected final shape.

theorem Runtime.Autograd.Compiled.buildFrom_denoteAllFrom_unary_exact {α : 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) (hi : i < g.nodes.size) (τ : Spec.Shape) (nodeData : Proofs.Autograd.Algebra.NodeData α Unit ([inShape] ++ ss) τ) (hTail : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) (i + 1) (denoteAllState inShape ⟨ss ++ [τ], gd.snoc nodeData⟩ x) = Except.ok (denoteAllState inShape st' x)) (hEval : g.evalAt payload (NN.IR.DVal.mk inShape x) (denoteAllState inShape ⟨ss, gd⟩ x) i = Except.ok (NN.IR.DVal.mk τ (nodeData.forward (gd.eval (Proofs.Autograd.Algebra.TList.cons x Proofs.Autograd.Algebra.TList.nil) ()) ()))) : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) i (denoteAllState inShape ⟨ss, gd⟩ x) = Except.ok (denoteAllState inShape st' x)

Semantic Equivalence lemma for a unary op compilation step (already-compiled nodeData).

This packages the common pattern for unary operators: compile the node, compute its forward value, push it onto the value table, and appeal to the inductive hypothesis for the tail.

theorem Runtime.Autograd.Compiled.buildFrom_denoteAllFrom_binary_exact {α : 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) (hi : i < g.nodes.size) (τ : Spec.Shape) (nodeData : Proofs.Autograd.Algebra.NodeData α Unit ([inShape] ++ ss) τ) (hTail : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) (i + 1) (denoteAllState inShape ⟨ss ++ [τ], gd.snoc nodeData⟩ x) = Except.ok (denoteAllState inShape st' x)) (hEval : g.evalAt payload (NN.IR.DVal.mk inShape x) (denoteAllState inShape ⟨ss, gd⟩ x) i = Except.ok (NN.IR.DVal.mk τ (nodeData.forward (gd.eval (Proofs.Autograd.Algebra.TList.cons x Proofs.Autograd.Algebra.TList.nil) ()) ()))) : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) i (denoteAllState inShape ⟨ss, gd⟩ x) = Except.ok (denoteAllState inShape st' x)

Semantic Equivalence lemma for a binary op compilation step (already-compiled nodeData).

This is the two-parent analogue of buildFrom_denoteAllFrom_unary_exact.

theorem Runtime.Autograd.Compiled.dval_fst_eq_of_eq_mk {α : Type} [Context α] {v : NN.IR.DVal α} {s : Spec.Shape} {t : Spec.Tensor α s} (h : v = NN.IR.DVal.mk s t) : v.fst = s

If a dynamic value v is definitionally a dependent pair ⟨s, t⟩, then extracting its second component requires a transport across the (propositional) shape equality.

This lemma packages the standard Sigma-transport pattern used throughout the semantic equivalence proof: when v = DVal.mk s t, transporting v.snd across the induced shape equality yields t.

theorem Runtime.Autograd.Compiled.dval_snd_cast_of_eq_mk {α : Type} [Context α] {v : NN.IR.DVal α} {s : Spec.Shape} {t : Spec.Tensor α s} (h : v = NN.IR.DVal.mk s t) : ⋯ ▸ v.snd = t

Transport the tensor component of a dynamic value across the induced shape equality.

We spell this as a separate theorem (rather than using by simpa ... inside the statement) so that the module system does not need to elaborate a tactic block in a public header.

Boolean Shape Equality Helpers

The IR evaluator uses boolean equality/inequality checks on Shape (via BEq Shape) in a few places. For example, evalAt's .conv2d case checks a computed output shape against the node's declared outShape using != (rather than a propositional ≠) because it is part of the runtime error-reporting path.

In the proof layer we frequently have a propositional equality s = t and need to discharge such boolean guards. Since BEq Shape is defined as an explicit structural test (Shape.areEqual) and we do not globally assume LawfulBEq Shape, we prove the small bridge lemmas locally here.

theorem Runtime.Autograd.Compiled.shape_areEqual_refl (s : Spec.Shape) : s.areEqual s = true

Reflexivity of the explicit structural boolean equality test Shape.areEqual.

theorem Runtime.Autograd.Compiled.shape_beq_refl (s : Spec.Shape) : (s == s) = true

Reflexivity of BEq Shape (==).

theorem Runtime.Autograd.Compiled.shape_bne_refl (s : Spec.Shape) : (s != s) = false

Reflexivity of boolean inequality (!=) on shapes.

theorem Runtime.Autograd.Compiled.shape_bne_eq_false_of_eq {s t : Spec.Shape} (h : s = t) : (s != t) = false

Propositional shape equality implies the boolean inequality guard s != t is false.