TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Square

Once-rounded posit squares #

The model square reuses exact dyadic multiplication. The public configured square reuses the selected certified multiplication kernel, including its packed carriers and width-generic fallback. Neither entry point adds a rounding step.

source
@[inline]
def FloatLib.Floats.Formats.Posit.Model.square {format : Format} (value : Model format) :
Model format

Square by exact multiplication followed by one standardized posit rounding. NaR propagates.

Instances For
    source
    theorem FloatLib.Floats.Formats.Posit.Model.square_eq_spec {format : Format} (value : Model format) :
    value.square = Spec.mul value value

    Model squaring refines the exact rational multiplication specification.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.square_of_toRat {format : Format} (value : Model format) (q : ℚ) (hvalue : value.toRat? = some q) :
    value.square = roundRat format (q * q)

    The exact rational square is rounded once for every finite posit.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.Posit.Model.square_nar {format : Format} :
    (nar format).square = nar format

    Not-a-Real propagates through squaring.

    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.square {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [Backend.PolicyFor (Formats.Posit.Configured.Family format code plan)] [Mul (Formats.Posit.Configured.Family format code plan)] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
    ExecFloat (Formats.Posit.Configured.Family format code plan)

    Square using the selected certified posit multiplication, with one final rounding.

    Instances For
      source
      theorem FloatLib.Floats.ExecFloat.Posit.square_eq_mul {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [Backend.PolicyFor (Formats.Posit.Configured.Family format code plan)] [Mul (Formats.Posit.Configured.Family format code plan)] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
      square value = value.mul value

      Public squaring uses the same certified multiplication call as value * value.

      source
      theorem FloatLib.Floats.ExecFloat.Posit.square_eq_spec {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [Backend.PolicyFor (Formats.Posit.Configured.Family format code plan)] [Mul (Formats.Posit.Configured.Family format code plan)] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
      square value = Spec.mul value value

      Squaring preserves the selected multiplication capability's reference result.