Packing correctness for configured standard operations

Every decoding theorem states that decoding a configured result recovers the single descriptor-model operation used to compute it. Results with status := true keep all five indicators, and the projection theorems value_remainder through value_nextDown state that their value is the configured operation without status.

The arithmetic properties are proved for the descriptor-model operations. These theorems transport their results through the storage codec, giving the same equations for values and exception flags with every storage plan.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (remainder dividend divisor) = (toModel dividend).remainder (toModel divisor)

Decoding configured IEEE remainder gives the descriptor-model remainder.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : toModel (remainder dividend divisor true) = (Binary.toModel dividend).remainder (Binary.toModel divisor) true

Decoding configured remainder preserves its value, status indicators, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_roundToIntegral {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)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (roundToIntegral value mode) = (toModel value).roundToIntegral mode

Decoding configured integral rounding gives integral rounding in the descriptor model.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_roundToIntegral {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)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (roundToIntegral value mode true) = (Binary.toModel value).roundToIntegral mode true

Configured integral rounding preserves the model value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_scale {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)) (n : ℤ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (scale value n mode) = (toModel value).scale n mode

Decoding configured power-of-two scaling gives descriptor-model scaling.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_scale {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)) (n : ℤ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toModel (scale value n mode true) = (Binary.toModel value).scale n mode true

Configured power-of-two scaling preserves the model value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.binaryExponentInt_eq {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)) : binaryExponentInt value = (toModel value).binaryExponentInt

The integer exponent query is the descriptor-model query on the decoded value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_binaryExponent {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 (binaryExponent value) = (toModel value).binaryExponent

Decoding configured binaryExponent gives the descriptor-model leading binary exponent.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_binaryExponent {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 (binaryExponent value true) = (Binary.toModel value).binaryExponent true

Configured binaryExponent preserves the model value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_copySign {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (magnitude signSource : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (copySign magnitude signSource).toModel = (toModel magnitude).copySign (toModel signSource)

Decoding configured sign copying gives descriptor-model sign copying.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_abs {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)) : (abs value).toModel = (toModel value).abs

Decoding configured absolute value gives descriptor-model absolute value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_nextUp {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 (nextUp value) = (toModel value).nextUp

Decoding the configured upward neighbor gives the descriptor-model upward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_nextUp {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 (nextUp value true) = (Binary.toModel value).nextUp true

The configured upward neighbor preserves the model value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_nextDown {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 (nextDown value) = (toModel value).nextDown

Decoding the configured downward neighbor gives the descriptor-model downward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.IEEEOutcome.toModel_nextDown {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 (nextDown value true) = (Binary.toModel value).nextDown true

The configured downward neighbor preserves the model value, status, and ternary value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_minNum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (minNum left right).toModel = (toModel left).minNum (toModel right)

Decoding configured minNum gives descriptor-model minNum.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toModel_maxNum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (maxNum left right).toModel = (toModel left).maxNum (toModel right)

Decoding configured maxNum gives descriptor-model maxNum.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (remainder dividend divisor true).value = remainder dividend divisor

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_roundToIntegral {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)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (roundToIntegral value mode true).value = roundToIntegral value mode

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_scale {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)) (n : ℤ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : (scale value n mode true).value = scale value n mode

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_binaryExponent {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)) : (binaryExponent value true).value = binaryExponent value

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

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_nextUp {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)) : (nextUp value true).value = nextUp value

The configured upward neighbor with status := true delivers the upward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.value_nextDown {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)) : (nextDown value true).value = nextDown value

The configured downward neighbor with status := true delivers the downward neighbor.

@[simp]

theorem FloatLib.Floats.ExecFloat.Binary.toInt?_eq_none_iff {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)) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode) : toInt? value mode = none ↔ isFinite value = false

The integer value is absent exactly for the values that are not finite.