Executable IR Lowering

Connects the verification IR to its forward executor:

1. lower a TorchLean Program to NN.IR.Graph and a verifier ParamStore;
2. convert the parameter store to an IR Payload; and
3. lower the IR graph to Runtime.Autograd.IRExec.ForwardGraph.

The returned LoweredIR remains available for verification. The accompanying forward graph runs that same IR artifact; it is not the differentiable graph returned by nn.lowerToTypedGraph.

This function composes two executable lowerings. It does not strengthen the broad program-to-IR pass with the theorem for NN.Verification.Builtin.Proved.ForwardProgram.

@[noinline]

def NN.Verification.Builtin.lowerForwardExecutable {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (model : Runtime.Autograd.Model.Program α (paramShapes ++ [inShape]) outShape) (params : TorchLean.TensorPack α paramShapes) : Except String (LoweredIR α × Runtime.Autograd.IRExec.ForwardGraph α)

Lower a TorchLean forward model with one distinguished input to shared IR and its forward-executable graph.

Success establishes that both checked lowerings accepted the concrete program and payload. Use a named lowering theorem when a claim also requires equality with a source evaluator.