Real IR node equations for the finite vector linear/ReLU fragment.

theorem NN.Verification.Cert.FiniteArtifact.evalNode_input {n : ℕ} (payload : IR.Payload ℝ) (x : TorchLean.Tensor ℝ [n]) (values : Array (Spec.SomeTensor ℝ)) : IR.Graph.evalNode payload { shape := [n], tensor := x } values 0 { id := 0, parents := #[], kind := IR.OpKind.input, outShape := [n] } = Except.ok { shape := [n], tensor := x }

The real IR evaluator returns a vector input at its declared shape.

theorem NN.Verification.Cert.FiniteArtifact.evalNode_linear {n m : ℕ} (payload : IR.Payload ℝ) (input : Spec.SomeTensor ℝ) (values : Array (Spec.SomeTensor ℝ)) (id parent : ℕ) (x : TorchLean.Tensor ℝ [n]) (weights : TorchLean.Tensor ℝ [m, n]) (bias : TorchLean.Tensor ℝ [m]) (hp : values[parent]? = some { shape := [n], tensor := x }) (hw : payload.linear? id = some { outDim := m, inDim := n, W := weights, b := bias }) : IR.Graph.evalNode payload input values id { id := id, parents := #[parent], kind := IR.OpKind.linear, outShape := [m] } = Except.ok { shape := [m], tensor := (Spec.matVecMulSpec weights x).addSpec bias }

A unary vector linear node applies the payload's exact-real affine map.

theorem NN.Verification.Cert.FiniteArtifact.evalNode_relu {n : ℕ} (payload : IR.Payload ℝ) (input : Spec.SomeTensor ℝ) (values : Array (Spec.SomeTensor ℝ)) (id parent : ℕ) (x : TorchLean.Tensor ℝ [n]) (hp : values[parent]? = some { shape := [n], tensor := x }) : IR.Graph.evalNode payload input values id { id := id, parents := #[parent], kind := IR.OpKind.relu, outShape := [n] } = Except.ok { shape := [n], tensor := Activation.reluSpec x }

A unary vector ReLU node uses the same real activation as the decoded program.