Correctness of exact-dyadic posit arithmetic

These theorems prove that exact-dyadic addition, subtraction, multiplication, division, square root, and fused multiply-add equal the independent rational Model.Spec operations. The executable definitions live in Dyadic.Runtime.

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

Exact-dyadic addition refines the reference rational specification.

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

Exact-dyadic subtraction refines the reference rational specification.

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

Exact-dyadic multiplication refines the reference rational specification.

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

Exact-dyadic cross-multiplied division refines the rational specification.

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

Exact-dyadic squared-comparison square root refines the rational specification.

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

Exact-dyadic fused multiply-add refines the reference rational specification.