Correctness

TorchLean→IR correctness helpers.

This file does not (yet) contain a full lowering-correctness theorem for arbitrary TorchLean.Programs (the current embedding is higher-order). It provides the small, reusable bridges needed by concrete model-correctness theorems:

• 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.castTensor {α : Type} [TorchLean.Storage α] [Context α] {s s' : Spec.Shape} (h : s = s') (t : TorchLean.Tensor α s) : TorchLean.Tensor α s'

Cast a tensor across a proved shape equality.

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.