Constants

Constant-node correctness for the IR -> compiled runtime bridge.

The IR .const s node reads an external payload entry and appends that value to the execution table. This file proves that the compiled GraphData node produced by buildFrom appends exactly the same tensor as the IR denotational evaluator.

Keeping this proof outside the recursive semantic-equivalence theorem matters for readability: the top-level theorem should read as a dispatcher over named semantic cases, not as a long script that re-proves every operator branch inline.

Build note: .const is semantically straightforward but proof-intensive because the value arrives through the payload table and must be re-packed as a typed compiled node. Named payload lookup facts keep this proof focused instead of turning it into a long simp script.

Main definitions

• buildFrom_denoteAllFrom_const: semantic-preservation step for .const.

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