Configured comparison semantics

Configured predicates preserve the complete model result, including flags. The numerical theorems connect both quiet and signaling operations to exact extended-real order.

theorem FloatLib.Floats.ExecFloat.Binary.compareQuiet_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : compareQuiet predicate x y = Formats.BinaryInterchange.Model.Comparison.quiet predicate (toModel x) (toModel y)

Quiet comparison preserves the model's answer and all five flags.

theorem FloatLib.Floats.ExecFloat.Binary.compareSignaling_eq_model {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : compareSignaling predicate x y = Formats.BinaryInterchange.Model.Comparison.signaling predicate (toModel x) (toModel y)

Signaling comparison preserves the model's answer and all five flags.

theorem FloatLib.Floats.ExecFloat.Binary.compareQuiet_value_of_toEReal? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} {a b : EReal} (hx : (toModel x).toEReal? = some a) (hy : (toModel y).toEReal? = some b) : (compareQuiet predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate (some (compare a b))

Configured quiet predicates use exact extended-real order on non-NaN operands.

theorem FloatLib.Floats.ExecFloat.Binary.compareSignaling_value_of_toEReal? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) {x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)} {a b : EReal} (hx : (toModel x).toEReal? = some a) (hy : (toModel y).toEReal? = some b) : (compareSignaling predicate x y).value = Numerics.IEEEComparison.Predicate.accepts predicate (some (compare a b))

Configured signaling predicates use the same exact numerical order.

theorem FloatLib.Floats.ExecFloat.Binary.compareQuiet_invalid_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (compareQuiet predicate x y).status.invalid = true ↔ (toModel x).isSNaN = true ∨ (toModel y).isSNaN = true

Quiet configured comparison raises invalid precisely for signaling NaNs.

theorem FloatLib.Floats.ExecFloat.Binary.compareSignaling_invalid_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (predicate : Formats.BinaryInterchange.Model.Comparison.Predicate) (x y : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) : (compareSignaling predicate x y).status.invalid = true ↔ (toModel x).isNaN = true ∨ (toModel y).isNaN = true

Signaling configured comparison raises invalid precisely for NaNs.