Structural Nodes

Structural correctness facts for IR nodes that do not lower to ordinary executable operators.

The first node of a compiled graph is the distinguished input, but the recursive buildFrom loop starts after that input node. If buildFrom ever encounters another .input node while compiling the tail, successful compilation is impossible. We keep that fact as a named theorem so the top-level semantic-equivalence proof can dispatch to it directly.

This file also contains the correctness lemma for .detach. Although .detach appears in the IR as a node, it does not change the tensor value at the spec layer, and the compiled lowering is just the identity function with a shape check.

Build note: structural nodes look simple, but they sit on the boundary between graph control flow and tensor semantics. The .input case is an impossible-success proof, while .detach is a value identity proof wrapped in parent and shape checks. These boundary cases should stay small and separate from numeric operator proofs.

theorem Runtime.Autograd.Compiled.buildFrom_denoteAllFrom_input_impossible {α : 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) (hN : g.getNode i = Except.ok n) (hk : n.kind = NN.IR.OpKind.input) (hi : i < g.nodes.size) (hBuild : IRExec.buildFrom g payload inShape i ⟨ss, gd⟩ = Except.ok st') : g.denoteAllFrom payload (NN.IR.DVal.mk inShape x) i (denoteAllState inShape ⟨ss, gd⟩ x) = Except.ok (denoteAllState inShape st' x)

The recursive compiler cannot successfully compile an .input node in the graph tail.

theorem Runtime.Autograd.Compiled.buildFrom_denoteAllFrom_detach {α : 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) (hN : g.getNode i = Except.ok n) (hk : n.kind = NN.IR.OpKind.detach) (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 .detach lowering.