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.