Correctness

TorchLean→IR correctness helpers.

This file contains no correctness theorem itself. It provides the two executable bridges that the lowering theorems under NN.Verification.Builtin.Proved (in particular Proved.Correctness.runForwardIR_eq_evalForward) are stated about:

• convert a verifier ParamStore into an IR Payload for NN.IR.Graph.denote;
• evaluate a LoweredIR graph on a concrete input.

def NN.Verification.Builtin.payloadOfParamStore {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) : IR.Payload α

Convert a verifier ParamStore into an IR Payload for NN.IR.Graph.denote.

This is the bridge between the CROWN/LiRPA parameter representation used by the verification pipeline and the executable IR semantics.

def NN.Verification.Builtin.runForwardIR {α : Type} [TorchLean.Storage α] [Context α] {inShape outShape : Spec.Shape} (c : LoweredIR α) (x : TorchLean.Tensor α inShape) : Except String (TorchLean.Tensor α outShape)

Evaluate a LoweredIR forward graph on an input tensor, returning a shape-checked tensor.