BatchNorm IR Evaluation

The IR represents inference-time BatchNorm by a channel axis and a channel count. This file states the payload contract for that representation without fixing the tensor rank or choosing a layout. After shape inference identifies the channel axis, evaluation decomposes the input into leading axes, the channel axis, and trailing axes, then applies Spec.batchNormInference independently to each leading slice.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalBatchNorm_eq {α : Type} [TorchLean.Storage α] [Context α] (id channelAxis channels : ℕ) (params : IR.BatchNormEvalParams α) (x : Spec.SomeTensor α) (leading spatial : Spec.Shape) (hInfer : IR.OpContracts.inferBatchNormEvalOutShape channelAxis channels x.shape = Except.ok x.shape) (hChannels : params.c = channels) (hLeading : Spec.Shape.ofList (List.take channelAxis x.shape.toList) = leading) (hSpatial : Spec.Shape.ofList (List.drop (channelAxis + 1) x.shape.toList) = spatial) (hInput : x.shape = leading.concat (Spec.Shape.dim params.c spatial)) : IR.Graph.evalBatchNorm (singletonBatchNormEvalPayload id params) id channelAxis channels x = Except.ok (Spec.SomeTensor.ofTensor (TorchLean.Tensor.mapLeading leading (fun (sample : TorchLean.Tensor α (Spec.Shape.concat [params.c] spatial)) => Spec.batchNormInference sample params.mean params.var params.gamma params.beta params.eps) (hInput ▸ x.tensor)))

Evaluation of inference-time BatchNorm at an arbitrary channel axis.

The conditional on the right is the checked cast from the dynamically shaped IR value to the typed tensor expected by Spec.batchNormInference. For every shape accepted by inferBatchNormEvalOutShape, this equality records the complete payload-backed computation.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalBatchNorm_missing_payload {α : Type} [TorchLean.Storage α] [Context α] (payload : IR.Payload α) (id channelAxis channels : ℕ) (x : Spec.SomeTensor α) (hInfer : IR.OpContracts.inferBatchNormEvalOutShape channelAxis channels x.shape = Except.ok x.shape) (hMissing : payload.batchNormEval? id = none) : IR.Graph.evalBatchNorm payload id channelAxis channels x = Except.error (toString "IR eval: missing batch_norm_eval payload for node " ++ toString id)

A missing BatchNorm payload is rejected before normalization is evaluated.