TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.IR.ShapeContracts

IR Shape Contract Facts #

Closed facts for the graph-level shape contracts used by NN.IR.Infer.

These used to live as an IO regression test. They are pure Lean computations, so the useful artifact is a theorem: the same shape checker that protects runtime IR paths rejects malformed nodes and accepts the intended scalar-broadcast case.

source
def NN.Proofs.IR.ShapeContracts.chwSmall :
Spec.Shape
Instances For
    source
    def NN.Proofs.IR.ShapeContracts.node (kind : IR.OpKind) (outShape : Spec.Shape) :
    IR.Node
    Instances For
      source
      def NN.Proofs.IR.ShapeContracts.rejects (x : Except String Spec.Shape) :
      Bool
      Instances For