Lowered Forward Evaluation: Node Shape Preservation

theorem NN.Verification.Builtin.Proved.Correctness.evalNode_ok_shape_of_hShapes {α : 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) (vals : Array (Spec.SomeTensor α)) (hShapes : shapesOfVals vals = Ctx inShape ss) {v : Spec.SomeTensor α} : evalNode node params vals = Except.ok v → v.shape = out

If node evaluation succeeds under a consistent shapesOfVals invariant, the resulting dynamic value has the expected output shape.

This is a small “shape preservation” lemma used in the main lowering pass-correctness proof.

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.