TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Square

Squaring configured binary values #

Word and model carriers transport the unary square kernel through their lossless codec. Byte tables, two-word carriers, and limb carriers keep their selected multiplication kernel. Both routes agree with configured multiplication.

source
@[inline]
def FloatLib.Floats.ExecFloat.Binary.square {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format (Formats.BinaryInterchange.Configured.Code plan) plan)] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan (Formats.BinaryInterchange.Configured.Code plan)) :
Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan (Formats.BinaryInterchange.Configured.Code plan)

Square with one nearest-even rounding, retaining the descriptor's full encoding policy.

Instances For
    source
    theorem FloatLib.Floats.ExecFloat.Binary.square_eq_spec {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format (Formats.BinaryInterchange.Configured.Code plan) plan)] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan (Formats.BinaryInterchange.Configured.Code plan)) :
    value.square = Formats.BinaryInterchange.Configured.Spec.mul value value

    Configured squaring agrees with the certified multiplication specification.

    source
    theorem FloatLib.Floats.ExecFloat.Binary.square_eq_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format (Formats.BinaryInterchange.Configured.Code plan) plan)] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan (Formats.BinaryInterchange.Configured.Code plan)) :
    value.square = mul value value

    Squaring preserves the complete result of the selected multiplication capability.

    source
    @[simp]
    theorem FloatLib.Floats.ExecFloat.Binary.toModel_square {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format (Formats.BinaryInterchange.Configured.Code plan) plan)] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan (Formats.BinaryInterchange.Configured.Code plan)) :
    value.square.toModel = value.toModel.square

    Decoding a configured square gives the model square of the decoded value.