Correctness of direct arbitrary-width exact-dyadic posit arithmetic

The direct-packing kernels agree with the rational specification. Addition, subtraction, multiplication, square root, and FMA are related through the exact-dyadic implementation. Division uses the quotient-prefix refinement directly. Executable definitions are in Direct.Runtime.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.add_eq_dyadic {format : Format} (left right : Model format) : add left right = DyadicArithmetic.add left right

Direct arbitrary-width addition equals the shared exact-dyadic implementation.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sub_eq_dyadic {format : Format} (left right : Model format) : sub left right = DyadicArithmetic.sub left right

Direct arbitrary-width subtraction equals the shared exact-dyadic implementation.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.mul_eq_dyadic {format : Format} (left right : Model format) : mul left right = DyadicArithmetic.mul left right

Direct arbitrary-width multiplication equals the shared exact-dyadic implementation.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sqrt_eq_dyadic {format : Format} (value : Model format) : sqrt value = DyadicArithmetic.sqrt value

Direct arbitrary-width square root equals squared-boundary rounding.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.fma_eq_dyadic {format : Format} (left right addend : Model format) : fma left right addend = DyadicArithmetic.fma left right addend

Direct arbitrary-width FMA equals the shared exact-dyadic implementation.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.add_eq_spec {format : Format} (left right : Model format) : add left right = Spec.add left right

Direct arbitrary-width addition refines the reference rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sub_eq_spec {format : Format} (left right : Model format) : sub left right = Spec.sub left right

Direct arbitrary-width subtraction refines the reference rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.mul_eq_spec {format : Format} (left right : Model format) : mul left right = Spec.mul left right

Direct arbitrary-width multiplication refines the reference rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.div_eq_spec {format : Format} (left right : Model format) : div left right = Spec.div left right

Direct arbitrary-width division refines the reference rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.sqrt_eq_spec {format : Format} (value : Model format) : sqrt value = Spec.sqrt value

Direct arbitrary-width square root refines the reference rational specification.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicArithmetic.fma_eq_spec {format : Format} (left right addend : Model format) : fma left right addend = Spec.fma left right addend

Direct arbitrary-width FMA refines the single-rounding specification.