Correctness of configured posit backends

Every configured backend is proved equal to the independent exact operation in Configured.Spec. The proofs cover the representation-independent exact-dyadic and two-limb kernels as well as the direct packed-storage entry points.

Representation-independent backends

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicAdd_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : dyadicAdd left right = Spec.add left right

Exact-dyadic addition refines configured posit addition.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicSub_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : dyadicSub left right = Spec.sub left right

Exact-dyadic subtraction refines configured posit subtraction.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicMul_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : dyadicMul left right = Spec.mul left right

Exact-dyadic multiplication refines configured posit multiplication.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicDiv_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : dyadicDiv left right = Spec.div left right

Rational-free dyadic division refines configured posit division.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicSqrt_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : dyadicSqrt value = Spec.sqrt value

Rational-free dyadic square root refines configured posit square root.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.dyadicFma_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right addend : ExecFloat (Family format code plan)) : dyadicFma left right addend = Spec.fma left right addend

Exact-dyadic fused multiply-add refines configured posit FMA.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbAdd_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : nativeLimbAdd heligible left right = Spec.add left right

Two-limb-rounded addition refines configured posit addition.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbSub_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : nativeLimbSub heligible left right = Spec.sub left right

Two-limb-rounded subtraction refines configured posit subtraction.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbMul_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format code plan)) : nativeLimbMul heligible left right = Spec.mul left right

Two-limb-rounded multiplication refines configured posit multiplication.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.nativeLimbFma_eq_spec {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (heligible : Model.NativeLimb.Eligible format) (left right addend : ExecFloat (Family format code plan)) : nativeLimbFma heligible left right addend = Spec.fma left right addend

Two-limb-rounded fused multiply-add refines configured posit FMA.

Direct native-word storage

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordAdd_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : storedNativeWordAdd heligible left right = Spec.add left right

Direct packed-storage addition refines configured posit addition.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordSub_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : storedNativeWordSub heligible left right = Spec.sub left right

Direct packed-storage subtraction refines configured posit subtraction.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordMul_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : storedNativeWordMul heligible left right = Spec.mul left right

Direct packed-storage multiplication refines configured posit multiplication.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordDiv_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right : ExecFloat (Family format (Code plan) plan)) : storedNativeWordDiv heligible left right = Spec.div left right

Direct packed-storage division refines configured posit division.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordSqrt_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (value : ExecFloat (Family format (Code plan) plan)) : storedNativeWordSqrt heligible value = Spec.sqrt value

Direct packed-storage square root refines configured posit square root.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeWordFma_eq_spec {format : Format} {plan : StoragePlan format} [NativeCode format plan] (heligible : Model.NativeWord.Eligible format) (left right addend : ExecFloat (Family format (Code plan) plan)) : storedNativeWordFma heligible left right addend = Spec.fma left right addend

Direct packed-storage FMA refines configured posit FMA.

Direct two-limb storage

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbAdd_eq_spec {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbAdd width_le heligible left right = Spec.add left right

Direct two-limb packed addition refines configured posit addition.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbSub_eq_spec {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbSub width_le heligible left right = Spec.sub left right

Direct two-limb packed subtraction refines configured posit subtraction.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbMul_eq_spec {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbMul width_le heligible left right = Spec.mul left right

Direct two-limb packed multiplication refines configured posit multiplication.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbDiv_eq_spec {format : Format} (width_le : format.bits ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbDiv width_le left right = Spec.div left right

Direct pair decoding followed by the shared quotient-prefix kernel refines configured division.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbSqrt_eq_spec {format : Format} (width_le : format.bits ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbSqrt width_le value = Spec.sqrt value

Direct two-limb packed square root refines configured posit square root.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.storedNativeLimbFma_eq_spec {format : Format} (width_le : format.bits ≤ 128) (heligible : Model.NativeLimb.Eligible format) (left right addend : ExecFloat (Family format (Code (StoragePlan.pair width_le)) (StoragePlan.pair width_le))) : storedNativeLimbFma width_le heligible left right addend = Spec.fma left right addend

Direct two-limb packed FMA refines configured posit FMA.