Lowered Forward Evaluation: SSA Denotation Agreement

The main theorem denoteAllFrom_lowerForwardLetChain_eq_evalForwardLetChainVals states that running the IR evaluator over a lowered let-chain produces the same value vector as the typed evaluator. The proof is an induction over the chain: evalAt_eq_evalNode_of_lowerNode dispatches the one-node agreement to the per-operator lemmas, and the remaining lemmas here unfold one evaluation step on each side.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_of_lowerNode {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (node : Node α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure (lowerNode id node params ps).1) (hConst : P.constVals.get? id = (lowerNode id node params ps).2.constVals.get? id) (hLin : P.linearWB.get? id = (lowerNode id node params ps).2.linearWB.get? id) (hConv : P.convCfg.get? id = (lowerNode id node params ps).2.convCfg.get? id) (hLayerNorm : P.layerNorm.get? id = (lowerNode id node params ps).2.layerNorm.get? id) : G.evalAt (payloadOfParamStore P) input vals id = evalNode node params vals

Evaluating the IR node emitted by lowerNode agrees with evalNode on the source node, provided the graph holds that node at id and the parameter store agrees with the lowering at id.

def NN.Verification.Builtin.Proved.Correctness.lowerStep {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid : Spec.Shape} (node : Node α paramShapes inShape ss mid) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) : LoweredIR α

The lowering accumulator after appending the lowering of one node at the fresh id.

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardLetChain_let1 {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid out : Spec.Shape} (node : Node α paramShapes inShape ss mid) (gNext : ForwardLetChain α paramShapes inShape (ss ++ [mid]) out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) : lowerForwardLetChain (ForwardLetChain.let1 node gNext) params c = lowerForwardLetChain gNext params (lowerStep node params c)

Lowering a let1 chain lowers the head node and continues from the extended accumulator.

theorem NN.Verification.Builtin.Proved.Correctness.size_lt_lowerForwardLetChain_lowerStep {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid out : Spec.Shape} (node : Node α paramShapes inShape ss mid) (gNext : ForwardLetChain α paramShapes inShape (ss ++ [mid]) out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) : c.graph.nodes.size < (lowerForwardLetChain gNext params (lowerStep node params c)).graph.nodes.size

The id reserved by lowerStep stays in range after lowering the rest of the chain.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_lowerForwardLetChain_lowerStep_eq_evalNode {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid out : Spec.Shape} (node : Node α paramShapes inShape ss mid) (gNext : ForwardLetChain α paramShapes inShape (ss ++ [mid]) out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (hShapes : shapesOfVals vals = Ctx inShape ss) : (lowerForwardLetChain gNext params (lowerStep node params c)).graph.evalAt (payloadOfParamStore (lowerForwardLetChain gNext params (lowerStep node params c)).ps) input vals c.graph.nodes.size = evalNode node params vals

The node lowered by lowerStep evaluates like its source node inside the fully lowered graph: lowering the rest of the chain neither moves the node nor disturbs its payload entries.

theorem NN.Verification.Builtin.Proved.Correctness.denoteAllFrom_eq_bind_of_lt {α : Type} [TorchLean.Storage α] [Context α] (g : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (i : ℕ) (vals : Array (Spec.SomeTensor α)) (hi : i < g.nodes.size) : g.denoteAllFrom payload input i vals = do let v ← g.evalAt payload input vals i g.denoteAllFrom payload input (i + 1) (vals.push v)

One in-range step of denoteAllFrom: evaluate node i, push it, and continue at i + 1.

theorem NN.Verification.Builtin.Proved.Correctness.shapesOfVals_push_of_evalNode_ok {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {mid : Spec.Shape} (node : Node α paramShapes inShape ss mid) (params : TorchLean.TensorPack α paramShapes) (vals : Array (Spec.SomeTensor α)) (v : Spec.SomeTensor α) (hShapes : shapesOfVals vals = Ctx inShape ss) (hEval : evalNode node params vals = Except.ok v) : shapesOfVals (vals.push v) = Ctx inShape (ss ++ [mid])

Pushing a successfully evaluated node value extends the shape context by its output shape.

theorem NN.Verification.Builtin.Proved.Correctness.denoteAllFrom_lowerForwardLetChain_eq_evalForwardLetChainVals {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (g : ForwardLetChain α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (c : LoweredIR α) (x : TorchLean.Tensor α inShape) (vals : Array (Spec.SomeTensor α)) (hSize : vals.size = c.graph.nodes.size) (hShapes : shapesOfVals vals = Ctx inShape ss) : (lowerForwardLetChain g params c).graph.denoteAllFrom (payloadOfParamStore (lowerForwardLetChain g params c).ps) { shape := inShape, tensor := x } c.graph.nodes.size vals = evalForwardLetChainVals g params vals

denoteAllFrom for the lowered IR agrees with the forward-fragment evaluator that returns all intermediate values. Lowering preserves the full SSA value vector up to the current lowering point, not only the final output.