Lowered Forward Evaluation: End-to-End Correctness #
theorem
NN.Verification.Builtin.Proved.Correctness.runForwardIR_eq_evalForward
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape outShape : Spec.Shape}
(p : ForwardProgram α paramShapes inShape outShape)
(params : TorchLean.TensorPack α paramShapes)
(x : TorchLean.Tensor α inShape)
:
Main lowering correctness theorem (verified forward fragment).
In words: lowering a first-order forward program p into the verifier IR and then
evaluating the lowered graph yields the same output as directly evaluating p with
evalForward.