Linear Algebra IR Evaluation

Local semantics for matrix multiplication nodes accepted by the shared IR importer.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_matmul_eq {α : Type} [TorchLean.Storage α] [Context α] {leftShape rightShape outShape : Spec.Shape} (op : MatmulOperation leftShape rightShape outShape) (left : TorchLean.Tensor α leftShape) (right : TorchLean.Tensor α rightShape) : (binaryGraphOut IR.OpKind.matmul leftShape rightShape outShape).evalAt { } { shape := leftShape, tensor := left } #[{ shape := leftShape, tensor := left }, { shape := rightShape, tensor := right }] 2 = Except.ok { shape := outShape, tensor := op.denote left right }

Evaluate any supported matrix multiplication in its canonical three-node graph.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_matmul_of_getNode {α : Type} [TorchLean.Storage α] [Context α] {inShape leftShape rightShape outShape : Spec.Shape} {ss : List Spec.Shape} (op : MatmulOperation leftShape rightShape outShape) (leftIdx : Idx (Ctx inShape ss) leftShape) (rightIdx : Idx (Ctx inShape ss) rightShape) (g : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (i : ℕ) (node : IR.Node) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : g.getNode i = pure node) (hKind : node.kind = IR.OpKind.matmul) (hParents : node.parents = #[leftIdx.id, rightIdx.id]) (hOut : node.outShape = outShape) : g.evalAt payload input vals i = do let left ← getVal vals leftIdx let right ← getVal vals rightIdx pure { shape := outShape, tensor := op.denote left right }

Evaluate a typed matrix multiplication node in an arbitrary lowered graph.