TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Util.DecimalRounding

Rounding JSON decimals into binary formats #

A JSON number is an exact decimal mantissa / 10^exponent. Reading it through JsonNumber.toFloat and then casting to binary32 rounds twice, and the first rounding is not directed. The helpers here round the exact decimal once, in the requested direction, directly into binary32 or binary64.

Certificate parsers use .down for lower endpoints and .up for upper endpoints, so the parsed box contains the decimal box that the artifact states. Transcript entries that must equal a replayed value use .nearest.

source
def NN.Verification.Util.DecimalRounding.roundDecimal (fmt : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (n : Lean.JsonNumber) :
FloatLib.Floats.Formats.BinaryInterchange.Model fmt

Round an exact JSON decimal once into fmt.

Instances For
    source
    def NN.Verification.Util.DecimalRounding.binary (fmt : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (n : Lean.JsonNumber) :
    FloatLib.Floats.ExecFloat.Binary fmt.expWidth fmt.fracWidth fmt.encoding fmt.exponentBias ⋯ ⋯ ⋯ ⋯

    Round an exact JSON decimal once into the executable format fmt.

    Instances For
      source
      def NN.Verification.Util.DecimalRounding.float (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (n : Lean.JsonNumber) :
      Float

      Round an exact JSON decimal once into host binary64.

      Instances For
        source
        def NN.Verification.Util.DecimalRounding.numbers? (n : ℕ) (j : Lean.Json) :
        Option (Fin n → Lean.JsonNumber)

        Read a JSON array of exactly n numbers.

        Instances For
          source
          def NN.Verification.Util.DecimalRounding.numberMatrix? (rows cols : ℕ) (j : Lean.Json) :
          Option (Fin rows → Fin cols → Lean.JsonNumber)

          Read a JSON rows × cols matrix of numbers.

          Instances For
            source
            def NN.Verification.Util.DecimalRounding.vector? (fmt : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (n : ℕ) (j : Lean.Json) :
            Option (TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary fmt.expWidth fmt.fracWidth fmt.encoding fmt.exponentBias ⋯ ⋯ ⋯ ⋯) [n])

            Read a length-n JSON vector, rounding every entry once into fmt with mode.

            Instances For
              source
              def NN.Verification.Util.DecimalRounding.matrix? (fmt : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat) (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (rows cols : ℕ) (j : Lean.Json) :
              Option (TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary fmt.expWidth fmt.fracWidth fmt.encoding fmt.exponentBias ⋯ ⋯ ⋯ ⋯) [rows, cols])

              Read a rows × cols JSON matrix, rounding every entry once into fmt with mode.

              Instances For