Refinement of format-parameterized binary arithmetic

The executable model operations agree with the independent descriptor-aware specifications for every validated FloatFormat.

These theorems connect the arithmetic dispatchers to the format's specifications before a result is transported to configured storage. Each dispatcher proof covers its optimized backends and generic fallback.

The Internal.Directed.add_eq family and its status counterparts state that each kernel computes the public operation with the same options, so proofs that unfold a kernel can return to the public form.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.add_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.add y = Spec.add x y

Public addition agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.sub_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.sub y = Spec.sub x y

Public subtraction agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.mul_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.mul y = Spec.mul x y

Public multiplication agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.div_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.div y = Spec.div x y

Public division agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.sqrt_eq_spec {fmt : FloatFormat} (x : Model fmt) : x.sqrt = Spec.sqrt x

Public square root agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.fma_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : x.fma y z = Spec.fma x y z

Public FMA agrees with its descriptor-aware specification for every FloatFormat.

Kernels of the public operations

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.add_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : add mode x y = x.add y mode

The directed addition kernel computes add in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.sub_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : sub mode x y = x.sub y mode

The directed subtraction kernel computes sub in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.mul_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : mul mode x y = x.mul y mode

The directed multiplication kernel computes mul in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.div_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x y : Model fmt) : div mode x y = x.div y mode

The directed division kernel computes div in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.sqrt_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x : Model fmt) : sqrt mode x = x.sqrt mode

The directed square-root kernel computes sqrt in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Directed.fma_eq {fmt : FloatFormat} (mode : IEEERoundingMode) (x y z : Model fmt) : fma mode x y z = x.fma y z mode

The directed FMA kernel computes fma in every rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.add_eq {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : add x y mode = x.add y mode true

The status addition kernel is add with status := true.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.sub_eq {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : sub x y mode = x.sub y mode true

The status subtraction kernel is sub with status := true.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.mul_eq {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : mul x y mode = x.mul y mode true

The status multiplication kernel is mul with status := true.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.div_eq {fmt : FloatFormat} (x y : Model fmt) (mode : IEEERoundingMode) : div x y mode = x.div y mode true

The status division kernel is div with status := true.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.sqrt_eq {fmt : FloatFormat} (x : Model fmt) (mode : IEEERoundingMode) : sqrt x mode = x.sqrt mode true

The status square-root kernel is sqrt with status := true.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.fma_eq {fmt : FloatFormat} (x y z : Model fmt) (mode : IEEERoundingMode) : fma x y z mode = x.fma y z mode true

The status FMA kernel is fma with status := true.