TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Operation.Status

Status-bearing numerical operation contracts #

Status-bearing operations differ in their concrete result structures: IEEE arithmetic returns exception flags, checked integer operations may report overflow, and quantizers may report saturation. These contracts express correctness in terms of result and status projections, without imposing a common runtime wrapper.

source
def FloatLib.Numerics.Operation.WithStatus1 (A : NumericalSystem) (B : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → Outcome) (value : Outcome → B.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → Status → Prop) :
Prop

Complete semantics of a unary operation whose concrete result carries a code and status.

Instances For
    source
    def FloatLib.Numerics.Operation.WithStatus2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → Outcome) (value : Outcome → C.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → Status → Prop) :
    Prop

    Complete semantics of a two-input operation whose result carries a code and status.

    Instances For
      source
      def FloatLib.Numerics.Operation.WithStatus3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → C.Code → Outcome) (value : Outcome → D.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar → Status → Prop) :
      Prop

      Complete semantics of a three-input operation whose result carries a code and status.

      Instances For
        source
        def FloatLib.Numerics.Operation.WithStatusFinite1 (A : NumericalSystem) (B : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → Outcome) (value : Outcome → B.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → Status → Prop) :
        Prop

        Finite semantics of a unary status-bearing operation.

        Instances For
          source
          def FloatLib.Numerics.Operation.WithStatusFinite2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → Outcome) (value : Outcome → C.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → C.Scalar → Status → Prop) :
          Prop

          Finite semantics of a two-input status-bearing operation.

          Instances For
            source
            def FloatLib.Numerics.Operation.WithStatusFinite3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → C.Code → Outcome) (value : Outcome → D.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → C.Scalar → D.Scalar → Status → Prop) :
            Prop

            Finite semantics of a three-input status-bearing operation.

            Instances For