Refinement of unary binary squaring

Each single-operand kernel equals the corresponding multiplication kernel on equal operands. The multiplication proofs then supply correct rounding and the complete result encoding, including NaN signs and payloads.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.finite_eq_mul {fmt : FloatFormat} (x : Model fmt) : finite? x = FiniteKernel.mulRuntime? x x

Finite squaring with one decode equals the finite product mulRuntime? x x.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.generic_eq_mul {fmt : FloatFormat} (x : Model fmt) : generic x = MulBackend.generic x x

Generic squaring equals generic multiplication of x by itself.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.binary32_eq_mul (x : NativeBinary32.Value) : binary32? x = NativeBinary32.mulFiniteWord? x x

Binary32 squaring agrees with NativeBinary32.mulFiniteWord? x x.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.smallWord_eq_mul {fmt : FloatFormat} (x : Model fmt) : smallWord x = NativeSmallWordMul.mulNormalWord x x

One-word squaring agrees with mulNormalWord x x, decline sentinel included.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.twoWord_eq_mul {fmt : FloatFormat} (x : Model fmt) : twoWord? x = NativeTwoWordMul.mulNormal? x x

Two-word squaring agrees with NativeTwoWordMul.mulNormal? x x.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.pair_eq_mul {fmt : FloatFormat} (x : Model fmt) : pair? x = NativePair.mulNormalLimb? x x

Fixed-pair squaring agrees with the four-limb product mulNormalLimb? x x.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.dispatch_eq_mul {fmt : FloatFormat} (x : Model fmt) : dispatch x = MulBackend.word x x

Squaring dispatch agrees with the multiplication dispatcher on x * x, branch by branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.SquareBackend.dispatch_eq_spec {fmt : FloatFormat} (x : Model fmt) : dispatch x = Spec.mul x x

Binary squaring is the once-rounded exact product, with multiplication's encoding policy.