Shape-Changing IR Evaluation

Local semantics for the shape-oriented IR nodes emitted by PyTorch/ONNX import paths. These facts pin the executable IR evaluator to the corresponding typed tensor operations.

inductive NN.Verification.Builtin.Proved.Correctness.IRStep.ShapeOperation : Spec.Shape → Spec.Shape → Type

Shape-changing unary operations with statically typed output tensors.

• reshape (inShape outShape : Spec.Shape) (hsize : inShape.size = outShape.size) : ShapeOperation inShape outShape

  Reshape between shapes with equal element counts.

• flatten (s : Spec.Shape) : ShapeOperation s (Spec.Shape.dim s.size Spec.Shape.scalar)

  Flatten a tensor to one dimension.

• broadcastTo (s₁ s₂ : Spec.Shape) (witness : s₁.CanBroadcastTo s₂) : ShapeOperation s₁ s₂

  Broadcast to a compatible target shape.

• sum (s : Spec.Shape) : ShapeOperation s Spec.Shape.scalar

  Sum every coordinate to a scalar.

def NN.Verification.Builtin.Proved.Correctness.IRStep.ShapeOperation.toOpKind {inShape outShape : Spec.Shape} : ShapeOperation inShape outShape → IR.OpKind

IR opcode represented by a typed shape operation.

def NN.Verification.Builtin.Proved.Correctness.IRStep.ShapeOperation.denote {α : Type} [TorchLean.Storage α] [Context α] {inShape outShape : Spec.Shape} (op : ShapeOperation inShape outShape) (x : TorchLean.Tensor α inShape) : TorchLean.Tensor α outShape

Typed denotation of a shape operation.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_shapeOperation_eq {α : Type} [TorchLean.Storage α] [Context α] {inShape outShape : Spec.Shape} (op : ShapeOperation inShape outShape) (x : TorchLean.Tensor α inShape) : (unaryGraphOut op.toOpKind inShape outShape).evalAt { } { shape := inShape, tensor := x } #[{ shape := inShape, tensor := x }] 1 = Except.ok { shape := outShape, tensor := op.denote x }

Evaluate any typed shape operation in its canonical two-node graph.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_reshape_eq {α : Type} [TorchLean.Storage α] [Context α] {inShape outShape : Spec.Shape} (x : TorchLean.Tensor α inShape) (hsize : inShape.size = outShape.size) : (unaryGraphOut (IR.OpKind.reshape inShape outShape) inShape outShape).evalAt { } { shape := inShape, tensor := x } #[{ shape := inShape, tensor := x }] 1 = Except.ok { shape := outShape, tensor := x.reshapeSpec hsize }

Local IR semantics for reshape when the element counts match.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_flatten_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraphOut (IR.OpKind.flatten s) s (Spec.Shape.dim s.size Spec.Shape.scalar)).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := Spec.Shape.dim s.size Spec.Shape.scalar, tensor := x.flattenSpec }

Local IR semantics for flatten.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_broadcastTo_eq {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ : Spec.Shape} (x : TorchLean.Tensor α s₁) (cb : s₁.CanBroadcastTo s₂) : (unaryGraphOut (IR.OpKind.broadcastTo s₁ s₂) s₁ s₂).evalAt { } { shape := s₁, tensor := x } #[{ shape := s₁, tensor := x }] 1 = Except.ok { shape := s₂, tensor := TorchLean.Tensor.broadcastTo cb x }

Local IR semantics for broadcastTo when the shapes are broadcast compatible.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_sum_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraphOut IR.OpKind.sum s Spec.Shape.scalar).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := Spec.Shape.scalar, tensor := TorchLean.Tensor.scalar x.sumSpec }

Local IR semantics for reduction to a scalar sum.