Packing correctness for configured binary arithmetic

The decoding bridge theorems toModel_add through toModel_sqrt and their IEEEOutcome.toModel_add through IEEEOutcome.toModel_sqrt companions state that decoding a configured result recovers the single descriptor-model operation used to compute it, with the same rounding direction and, for the outcomes, the same flags and ternary value. They let proofs transfer results from the model without depending on the configured storage plan. toModel_hAdd, toModel_hSub, toModel_hMul, toModel_hDiv, toModel_neg, and toModel_execFloat_sqrt do the same for the notation +, -, *, /, unary -, and the generic ExecFloat.sqrt, so simp turns a goal about toModel (a + b) into one about Model.add. The projection theorems value_add through value_sqrt mirror the model's: the value of an operation with status := true is the value of the same operation without it.

A nearest-even call without status runs the format's selected capability. A capability certifies its kernels against its own reference operation, so the value theorems take the instance argument ExecFloat.Capability.HasSpec cap Configured.Spec.add (and its siblings): the selected capability's reference is the configured model operation. Instance search proves it for every capability instance in the library, generic, automatic, and first-order binary32 and binary64, since each declares that reference. A custom capability whose reference operation is only propositionally the model operation must declare the instance itself. A capability with another reference operation gets neither the decoding nor the projection theorems, because its default call and its status := true call can then deliver different values.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_ofModel {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (outcome : Formats.BinaryInterchange.Model.IEEEOutcome format) : (ofModel outcome).toModel = outcome

Repacking and then decoding a model outcome preserves its value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.value_bind {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} (outcome : IEEEOutcome) (next : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) → IEEEOutcome) : (outcome.bind next).value = (next outcome.value).value

bind delivers the value of its second step.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.status_bind {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} (outcome : IEEEOutcome) (next : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) → IEEEOutcome) : (outcome.bind next).status = outcome.status.union (next outcome.value).status

bind raises every flag that either step raised.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.ternary_bind {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} (outcome : IEEEOutcome) (next : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan) → IEEEOutcome) : (outcome.bind next).ternary = (next outcome.value).ternary

bind keeps the ternary value of its second step.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_ofRat {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (q : ℚ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (ofRat q mode) = Formats.BinaryInterchange.Model.ofRat format q mode

Decoding a rounded rational gives the model rounding with the same direction.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_ofRat {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (q : ℚ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (ofRat q mode true) = Formats.BinaryInterchange.Model.ofRat format q mode true

Decoding a rounded rational with status := true preserves the flags and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_ofRat {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (q : ℚ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (ofRat q mode true).value = ofRat q mode

Rounding a rational with status := true delivers the value of the same rounding.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (add left right mode) = (toModel left).add (toModel right) mode

Decoding configured addition gives model addition with the same rounding mode.

The nearest-even call runs the selected ExecFloat.Add capability, so the theorem asks, as an instance argument, that its reference operation be Configured.Spec.add, the configured model operation. Instance search proves this for every capability the library declares. A custom capability whose reference is only propositionally that operation must declare the instance, and one with another reference operation does not satisfy the theorem.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sub (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sub] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sub left right mode) = (toModel left).sub (toModel right) mode

Decoding configured subtraction gives model subtraction with the same rounding mode.

As for toModel_add, the nearest-even call runs the selected ExecFloat.Sub capability, whose reference operation the instance argument fixes to Configured.Spec.sub.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Mul (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.mul] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (mul left right mode) = (toModel left).mul (toModel right) mode

Decoding configured multiplication gives model multiplication with the same rounding mode.

As for toModel_add, the nearest-even call runs the selected ExecFloat.Mul capability, whose reference operation the instance argument fixes to Configured.Spec.mul.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Div (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.div] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (div left right mode) = (toModel left).div (toModel right) mode

Decoding configured division gives model division with the same rounding mode.

As for toModel_add, the nearest-even call runs the selected ExecFloat.Div capability, whose reference operation the instance argument fixes to Configured.Spec.div.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_fma {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Fma (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.fma] (left right addend : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (fma left right addend mode) = (toModel left).fma (toModel right) (toModel addend) mode

Decoding configured FMA gives model FMA with the same rounding mode.

As for toModel_add, the nearest-even call runs the selected ExecFloat.Fma capability, whose reference operation the instance argument fixes to Configured.Spec.fma.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sqrt] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sqrt value mode) = (toModel value).sqrt mode

Decoding configured square root gives model square root with the same rounding mode.

As for toModel_add, the nearest-even call runs the selected ExecFloat.Sqrt capability, whose reference operation the instance argument fixes to Configured.Spec.sqrt.

Operator notation

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_hAdd {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (left + right) = (toModel left).add (toModel right)

Decoding a configured sum left + right gives nearest-even model addition.

+ runs the selected ExecFloat.Add capability, so, as for toModel_add, the theorem asks that its reference operation be Configured.Spec.add, which instance search proves for every capability the library declares.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_hSub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sub (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sub] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (left - right) = (toModel left).sub (toModel right)

Decoding a configured difference left - right gives nearest-even model subtraction.

- runs the selected ExecFloat.Sub capability, whose reference operation the instance argument fixes to Configured.Spec.sub.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_hMul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Mul (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.mul] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (left * right) = (toModel left).mul (toModel right)

Decoding a configured product left * right gives nearest-even model multiplication.

* runs the selected ExecFloat.Mul capability, whose reference operation the instance argument fixes to Configured.Spec.mul.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_hDiv {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Div (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.div] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (left / right) = (toModel left).div (toModel right)

Decoding a configured quotient left / right gives nearest-even model division.

/ runs the selected ExecFloat.Div capability, whose reference operation the instance argument fixes to Configured.Spec.div.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_neg {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (-value) = (toModel value).neg

Decoding a configured negation -value gives model negation.

Negation goes through the storage codec rather than a selected capability, so the theorem has no instance argument.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_execFloat_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sqrt] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel value.sqrt = (toModel value).sqrt

Decoding the generic square root ExecFloat.sqrt value gives nearest-even model square root.

value.sqrt on a configured value is ExecFloat.Binary.sqrt, covered by toModel_sqrt. This theorem covers the format-generic call, which runs the selected ExecFloat.Sqrt capability with reference operation Configured.Spec.sqrt.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Add (Formats.BinaryInterchange.Configured.Family format code plan)] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (add left right mode true) = (Binary.toModel left).add (Binary.toModel right) mode true

Decoding configured addition preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Sub (Formats.BinaryInterchange.Configured.Family format code plan)] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sub left right mode true) = (Binary.toModel left).sub (Binary.toModel right) mode true

Decoding configured subtraction preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Mul (Formats.BinaryInterchange.Configured.Family format code plan)] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (mul left right mode true) = (Binary.toModel left).mul (Binary.toModel right) mode true

Decoding configured multiplication preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Div (Formats.BinaryInterchange.Configured.Family format code plan)] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (div left right mode true) = (Binary.toModel left).div (Binary.toModel right) mode true

Decoding configured division preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_fma {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Fma (Formats.BinaryInterchange.Configured.Family format code plan)] (left right addend : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (fma left right addend mode true) = (Binary.toModel left).fma (Binary.toModel right) (Binary.toModel addend) mode true

Decoding configured FMA preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (sqrt value mode true) = (Binary.toModel value).sqrt mode true

Decoding configured square root preserves the model result, flags, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (add left right mode true).value = add left right mode

Configured addition with status := true delivers the value of configured addition.

Like toModel_add, it takes the instance argument HasSpec cap Configured.Spec.add, which instance search proves for every capability the library declares.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sub (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sub] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (sub left right mode true).value = sub left right mode

Configured subtraction with status := true delivers the value of configured subtraction.

Like toModel_sub, it takes the instance argument HasSpec cap Configured.Spec.sub.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Mul (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.mul] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (mul left right mode true).value = mul left right mode

Configured multiplication with status := true delivers the value of configured multiplication.

Like toModel_mul, it takes the instance argument HasSpec cap Configured.Spec.mul.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Div (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.div] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (div left right mode true).value = div left right mode

Configured division with status := true delivers the value of configured division.

Like toModel_div, it takes the instance argument HasSpec cap Configured.Spec.div.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_fma {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Fma (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.fma] (left right addend : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (fma left right addend mode true).value = fma left right addend mode

Configured FMA with status := true delivers the value of configured FMA.

Like toModel_fma, it takes the instance argument HasSpec cap Configured.Spec.fma.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] [cap : Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sqrt] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (sqrt value mode true).value = sqrt value mode

Configured square root with status := true delivers the value of configured square root.

Like toModel_sqrt, it takes the instance argument HasSpec cap Configured.Spec.sqrt.