Binary Matrix Product Enclosures

The runtime and certificate semantics share a flat coordinate map for batch broadcasting and vector promotion. Each product is enclosed by its four endpoint products, then accumulated in the same order as the value evaluator. Empty contractions and empty output shapes need no positivity assumptions.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.binaryMatmulBox_encloses (dims : IR.OpContracts.MatmulDims) {left right : FlatBox ℝ} {x y : Val} (hx : EnclosesBox left x) (hy : EnclosesBox right y) : EnclosesBox (binaryMatmulBox dims left right) { n := dims.outShape.size, v := IR.Graph.matmulFlat dims x.v y.v }

The executable binary interval contraction encloses the shared real value contraction.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibpBinaryMatmul_encloses {leftShape rightShape : Spec.Shape} {left right B : FlatBox ℝ} {x y v : Val} (hx : EnclosesBox left x) (hy : EnclosesBox right y) (hB : ibpBinaryMatmul? leftShape rightShape left right = some B) (hv : evalBinaryMatmul? leftShape rightShape x y = some v) : EnclosesBox B v

Successful binary value and interval transfers have the same layout and are enclosed.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.binary_matmul_node_encloses {nodes : Array Node} {ps : ParamStore ℝ} {cert : Array (Option (FlatBox ℝ))} {inputs : Std.HashMap ℕ Val} {vals : Array (Option Val)} {k : ℕ} {B : FlatBox ℝ} {v : Val} (hkKind : nodes[k]!.kind = IR.OpKind.matmul) (hUnary : IR.unaryParent? nodes[k]!.parents = none) (hcertStep : certStepNode? nodes ps cert k = some B) (hvalStep : evalNode? nodes ps inputs vals k = some v) (hpe : ParentsEnclosed nodes cert vals k) : EnclosesBox B v

Binary matmul's local certificate step preserves both parent enclosures.