Correctness of configured binary kernels

Every configured backend in Configured.Core.Runtime refines the same carrier-independent specification. The proofs depend only on the codec laws and the shared model-kernel theorems, not on the selected storage representation.

Total generic kernels

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericAdd_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : genericAdd left right = Spec.add left right

The width-generic addition backend implements the configured addition specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericSub_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : genericSub left right = Spec.sub left right

The width-generic subtraction backend implements the configured subtraction specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericMul_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : genericMul left right = Spec.mul left right

The width-generic multiplication backend implements the configured multiplication specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericDiv_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : genericDiv left right = Spec.div left right

The width-generic division backend implements the configured division specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericSqrt_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : genericSqrt value = Spec.sqrt value

The width-generic square-root backend implements the configured square-root specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericFma_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right addend : ExecFloat (Family format code plan)) : genericFma left right addend = Spec.fma left right addend

The width-generic fused multiply-add backend implements the configured FMA specification.

Word and fixed-limb arithmetic

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordAdd_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : wordAdd left right = Spec.add left right

The native-word addition backend implements the configured addition specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordSub_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : wordSub left right = Spec.sub left right

The native-word subtraction backend implements the configured subtraction specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordMul_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : wordMul left right = Spec.mul left right

The word or fixed-limb multiplication backend implements the configured specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordDiv_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : wordDiv left right = Spec.div left right

The word or fixed-limb division backend implements the configured specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordSqrt_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : wordSqrt value = Spec.sqrt value

The native-word square-root backend implements the configured square-root specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordFma_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right addend : ExecFloat (Family format code plan)) : wordFma left right addend = Spec.fma left right addend

The native-word fused multiply-add backend implements the configured FMA specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.fixedLimbSqrt_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : fixedLimbSqrt value = Spec.sqrt value

The fixed-limb square-root route implements the configured square-root specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.fixedLimbFma_eq_spec {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right addend : ExecFloat (Family format code plan)) : fixedLimbFma left right addend = Spec.fma left right addend

The fixed-limb fused multiply-add route implements the configured FMA specification.