Proof contracts for explicit conversion and mixed arithmetic

The preparation theorems compose the supplied decoder, exact-domain operations, and destination quantization relation. They establish one quantizer call on successful preparation and preserve preparation failures. Numerical preservation by ExactMap, the arithmetic instances and the context-dependent addition and subtraction hooks is left to family-specific laws.

Runtime-only clients may import Conversion.Runtime, and FloatLib.Floats.ExecFloat exports both execution and these contracts.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_inexact (first second : ConversionStatus) : (first.merge second).inexact = (first.inexact || second.inexact)

The merged inexact flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_overflow (first second : ConversionStatus) : (first.merge second).overflow = (first.overflow || second.overflow)

The merged overflow flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_underflow (first second : ConversionStatus) : (first.merge second).underflow = (first.underflow || second.underflow)

The merged underflow flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_saturated (first second : ConversionStatus) : (first.merge second).saturated = (first.saturated || second.saturated)

The merged saturation flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_wrapped (first second : ConversionStatus) : (first.merge second).wrapped = (first.wrapped || second.wrapped)

The merged wrapping flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_mapped_special (first second : ConversionStatus) : (first.merge second).mappedSpecial = (first.mappedSpecial || second.mappedSpecial)

The merged special-value flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_invalid (first second : ConversionStatus) : (first.merge second).invalid = (first.invalid || second.invalid)

The merged invalid flag is raised exactly when either input raised it.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.empty_merge (status : ConversionStatus) : { }.merge status = status

An empty first status contributes no flags.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_empty (status : ConversionStatus) : status.merge { } = status

An empty second status contributes no flags.

theorem FloatLib.Floats.ExecFloat.ConversionStatus.merge_assoc (first second third : ConversionStatus) : (first.merge second).merge third = first.merge (second.merge third)

Status accumulation is associative, so grouping a successful pipeline is irrelevant.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.map_success {α : Type u} {β : Type v} (f : α → β) (value : α) (status : ConversionStatus) : map f (success value status) = success (f value) status

Mapping a successful outcome transforms only its value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.map_failure {α : Type u} {β : Type v} (f : α → β) (reason : ConversionFailure) : map f (failure reason) = failure reason

Mapping a failed outcome preserves its failure reason.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.bind_success {α : Type u} {β : Type v} (value : α) (status : ConversionStatus) (next : α → ConversionOutcome β) : (success value status).bind next = match next value with | success nextValue nextStatus => success nextValue (status.merge nextStatus) | failure reason => failure reason

Binding a successful outcome runs the continuation and accumulates successful status.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.bind_failure {α : Type u} {β : Type v} (reason : ConversionFailure) (next : α → ConversionOutcome β) : (failure reason).bind next = failure reason

Binding a failed outcome does not run the continuation.

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.bind_success_empty {α : Type u} {β : Type v} (value : α) (next : α → ConversionOutcome β) : (success value).bind next = next value

Binding a successful outcome that carries no flags applies the continuation.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.value?_success {α : Type u} (value : α) (status : ConversionStatus) : (success value status).value? = some value

Extracting the value of a successful outcome returns that value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.value?_failure {α : Type u} (reason : ConversionFailure) : (failure reason).value? = none

A failed outcome contains no successful value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.status?_success {α : Type u} (value : α) (status : ConversionStatus) : (success value status).status? = some status

Extracting status from a successful outcome returns its stored flags.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.status?_failure {α : Type u} (reason : ConversionFailure) : (failure reason).status? = none

A failed outcome contains no successful status.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.failure?_success {α : Type u} (value : α) (status : ConversionStatus) : (success value status).failure? = none

A successful outcome contains no failure reason.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.failure?_failure {α : Type u} (reason : ConversionFailure) : (failure reason).failure? = some reason

Extracting failure information returns the stored reason.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.map_id {α : Type u} (outcome : ConversionOutcome α) : map id outcome = outcome

Mapping the identity function leaves an outcome unchanged.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.map_comp {α : Type u} {β : Type v} (f : α → β) {γ : Type w} (g : β → γ) (outcome : ConversionOutcome α) : map g (map f outcome) = map (g ∘ f) outcome

Success-value maps compose without changing status or failure information.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.value?_map {α : Type u} {β : Type v} (f : α → β) (outcome : ConversionOutcome α) : (map f outcome).value? = Option.map f outcome.value?

Extracting a value after map agrees with mapping the extracted option.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.status?_map {α : Type u} {β : Type v} (f : α → β) (outcome : ConversionOutcome α) : (map f outcome).status? = outcome.status?

Mapping a successful value does not alter its status.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.failure?_map {α : Type u} {β : Type v} (f : α → β) (outcome : ConversionOutcome α) : (map f outcome).failure? = outcome.failure?

Mapping a successful value does not alter a failure reason.

theorem FloatLib.Floats.ExecFloat.ConversionOutcome.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (outcome : ConversionOutcome α) (next : α → ConversionOutcome β) (last : β → ConversionOutcome γ) : (outcome.bind next).bind last = outcome.bind fun (value : α) => (next value).bind last

Grouping consecutive successful binds does not change values, failures, or accumulated flags.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactDecoder.run_natural (value : ℕ) : run value = Numerics.NumericalValue.finite value

Decoding a natural number for conversion produces that exact finite value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactDecoder.run_integer (value : ℤ) : run value = Numerics.NumericalValue.finite value

Decoding an integer for conversion produces that exact finite value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactDecoder.run_rational (value : ℚ) : run value = Numerics.NumericalValue.finite value

Decoding a rational for conversion introduces no rounding.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactDecoder.run_dyadic (value : Numerics.Dyadic) : run value = Numerics.NumericalValue.finite value

Decoding a dyadic value for conversion preserves its exact binary representation.

theorem FloatLib.Floats.ExecFloat.ExactDecoder.decodeTo_eq {Source : Type u} {SourceExact : Type v} {TargetExact : Type w} [ExactDecoder Source SourceExact] [embedding : ExactMap SourceExact TargetExact] (value : Source) : decodeTo value = Numerics.NumericalValue.map ExactMap.map (run value)

decodeTo is exact decoding followed by the selected finite-value embedding.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactDecoder.decodeTo_self {Source : Type u} {SourceExact : Type v} [ExactDecoder Source SourceExact] (value : Source) : decodeTo value = run value

Decoding into the source's own exact domain performs no semantic transformation.

theorem FloatLib.Floats.ExecFloat.Quantizer.spec_quantize {Destination : Type u} {Exact : Type v} [self : Quantizer Destination Exact] (context : Context Destination) (value : Numerics.NumericalValue Exact) : spec context value (quantize context value)

The executable destination quantizer satisfies its declared relation.

theorem FloatLib.Floats.ExecFloat.spec_convert {Source : Type u} {target : Type v} {SourceExact : Type w} {TargetExact : Type x} [ExactDecoder Source SourceExact] [ExactMap SourceExact TargetExact] [quantizer : Quantizer target TargetExact] {Mode : Type} [RoundingModes target Mode] (value : Source) (mode : Mode) (context : Quantizer.Context target) : Quantizer.spec context (ExactDecoder.decodeTo value) (convert value mode context)

Generic conversion satisfies the destination's declared quantization relation in the context it uses. For a call without context, that context is ModeContext.context for its mode.

theorem FloatLib.Floats.ExecFloat.spec_cast {F : Type u} [Numerics.EncodedFormat F] {target : Type v} {SourceExact : Type w} {TargetExact : Type x} [ExactDecoder (ExecFloat F) SourceExact] [ExactMap SourceExact TargetExact] [quantizer : Quantizer target TargetExact] {Mode : Type} [RoundingModes target Mode] (value : ExecFloat F) (mode : Mode) (context : Quantizer.Context target) : Quantizer.spec context (ExactDecoder.decodeTo value) (value.cast mode context)

ExecFloat conversion satisfies the destination's declared relation in the context it uses.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.requireFinite_finite {Exact : Type u} (position : InputPosition) (value : Exact) : requireFinite position (Numerics.NumericalValue.finite value) = Except.ok value

A finite observation passes through preparation unchanged.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.requireFinite_infinity {Exact : Type u} (position : InputPosition) (negative : Bool) : requireFinite position (Numerics.NumericalValue.infinity negative) = Except.error (ConversionFailure.infinity position negative)

Infinity is rejected at the supplied operand position.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.requireFinite_exceptional {Exact : Type u} (position : InputPosition) (value : Numerics.ExceptionalValue) : requireFinite position (Numerics.NumericalValue.exceptional value) = Except.error (ConversionFailure.exceptional position value)

An exceptional observation is rejected at the supplied operand position.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.prepareDiv_finite_of_is_zero {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (left right : Exact) (hright : Numerics.ExactZero.isZero right) : prepareDiv (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Except.error ConversionFailure.divisionByZero

Finite exact division rejects any denominator satisfying the domain's zero predicate.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.prepareDiv_finite_of_not_is_zero {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (left right : Exact) (hright : ¬Numerics.ExactZero.isZero right) : prepareDiv (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Except.ok (Numerics.NumericalValue.finite (left / right))

Finite exact division applies the domain's / when the denominator is not zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.prepareDiv_finite_eq_error_iff {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (left right : Exact) : prepareDiv (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Except.error ConversionFailure.divisionByZero ↔ Numerics.ExactZero.isZero right

Finite exact division reports division by zero exactly for declared-zero denominators.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.quantizePrepared_ok {Destination : Type u} {Exact : Type v} [quantizer : Quantizer Destination Exact] (context : Quantizer.Context Destination) (value : Numerics.NumericalValue Exact) : quantizePrepared context (Except.ok value) = Quantizer.run context value

A successfully prepared exact observation is passed to the destination quantizer.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.quantizePrepared_error {Destination : Type u} {Exact : Type v} [quantizer : Quantizer Destination Exact] (context : Quantizer.Context Destination) (reason : ConversionFailure) : quantizePrepared context (Except.error reason) = ConversionOutcome.failure reason

A preparation failure reaches the public outcome unchanged.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.preparedSpec_ok {Destination : Type u} {Exact : Type v} [quantizer : Quantizer Destination Exact] (context : Quantizer.Context Destination) (value : Numerics.NumericalValue Exact) (outcome : ConversionOutcome Destination) : PreparedSpec context (Except.ok value) outcome ↔ Quantizer.spec context value outcome

On successful preparation, PreparedSpec is the destination relation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Conversion.preparedSpec_error {Destination : Type u} {Exact : Type v} [quantizer : Quantizer Destination Exact] (context : Quantizer.Context Destination) (reason : ConversionFailure) (outcome : ConversionOutcome Destination) : PreparedSpec context (Except.error reason) outcome ↔ outcome = ConversionOutcome.failure reason

On preparation failure, PreparedSpec requires the same public failure.

theorem FloatLib.Floats.ExecFloat.Conversion.preparedSpec_quantizePrepared {Destination : Type u} {Exact : Type v} [quantizer : Quantizer Destination Exact] (context : Quantizer.Context Destination) (prepared : Except ConversionFailure (Numerics.NumericalValue Exact)) : PreparedSpec context prepared (quantizePrepared context prepared)

Preparation followed by the executable quantizer satisfies PreparedSpec.

theorem FloatLib.Floats.ExecFloat.ExactExpression.operand_eq_ok_of_decodeTo_eq_finite {Source : Type u} {SourceExact : Type v} {Exact : Type w} [ExactDecoder Source SourceExact] [ExactMap SourceExact Exact] (index : ℕ) (source : Source) (value : Exact) (hdecode : ExactDecoder.decodeTo source = Numerics.NumericalValue.finite value) : operand index source = Except.ok value

A finite decoded operand enters an exact expression unchanged.

theorem FloatLib.Floats.ExecFloat.ExactExpression.operand_eq_error_of_decodeTo_eq_infinity {Source : Type u} {SourceExact : Type v} {Exact : Type w} [ExactDecoder Source SourceExact] [ExactMap SourceExact Exact] (index : ℕ) (source : Source) (negative : Bool) (hdecode : ExactDecoder.decodeTo source = Numerics.NumericalValue.infinity negative) : operand index source = Except.error (ConversionFailure.infinity (InputPosition.operand index) negative)

A decoded infinity identifies the numbered operand that made the expression invalid.

theorem FloatLib.Floats.ExecFloat.ExactExpression.operand_eq_error_of_decodeTo_eq_exceptional {Source : Type u} {SourceExact : Type v} {Exact : Type w} [ExactDecoder Source SourceExact] [ExactMap SourceExact Exact] (index : ℕ) (source : Source) (value : Numerics.ExceptionalValue) (hdecode : ExactDecoder.decodeTo source = Numerics.NumericalValue.exceptional value) : operand index source = Except.error (ConversionFailure.exceptional (InputPosition.operand index) value)

A decoded exceptional value identifies the numbered operand that caused rejection.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.toPrepared_ok {Exact : Type u} (value : Exact) : toPrepared (Except.ok value) = Except.ok (Numerics.NumericalValue.finite value)

A successful exact expression becomes a finite input to the sole quantization step.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.toPrepared_error {Exact : Type u} (reason : ConversionFailure) : toPrepared (Except.error reason) = Except.error reason

An exact-expression failure is preserved before quantization.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.div_of_is_zero {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (numerator denominator : Exact) (hdenominator : Numerics.ExactZero.isZero denominator) : div numerator denominator = Except.error ConversionFailure.divisionByZero

Checked exact division rejects any denominator satisfying the domain's zero predicate.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.div_zero {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (numerator : Exact) : div numerator 0 = Except.error ConversionFailure.divisionByZero

Checked exact division reports division by canonical zero.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.div_of_not_is_zero {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (numerator denominator : Exact) (hdenominator : ¬Numerics.ExactZero.isZero denominator) : div numerator denominator = Except.ok (numerator / denominator)

Checked exact division applies the exact domain's / when the denominator is nonzero.

The premise uses the exact domain's declared zero proposition. A domain such as SignedRat can therefore recognize several zero representations and prove a bridge from that proposition to its numerical meaning.

@[simp]

theorem FloatLib.Floats.ExecFloat.ExactExpression.div_eq_error_iff {Exact : Type u} [Zero Exact] [self : Numerics.ExactZero Exact] [Div Exact] (numerator denominator : Exact) : div numerator denominator = Except.error ConversionFailure.divisionByZero ↔ Numerics.ExactZero.isZero denominator

Checked exact division reports division by zero exactly for declared-zero denominators.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_roundOnce {target : Type w} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [quantizer : Quantizer target Exact] (expression : ExactExpression Exact) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context expression.toPrepared (roundOnce expression mode context)

An exact expression followed by one quantization satisfies the destination's declared relation in the context used, or returns the expression's failure unchanged.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionProof.roundOnce_ok {target : Type w} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [quantizer : Quantizer target Exact] (value : Exact) (mode : Mode) (context : Quantizer.Context target) : roundOnce (Except.ok value) mode context = Quantizer.run context (Numerics.NumericalValue.finite value)

A successful expression goes to the quantizer as one finite exact value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ConversionProof.roundOnce_error {target : Type w} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [quantizer : Quantizer target Exact] (reason : ConversionFailure) (mode : Mode) (context : Quantizer.Context target) : roundOnce (Except.error reason) mode context = ConversionOutcome.failure reason

An exact-expression failure bypasses the destination quantizer unchanged.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_addAs {Left : Type u} {Right : Type v} {target : Type w} {LeftExact : Type x} {RightExact : Type y} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [ExactDecoder Left LeftExact] [ExactMap LeftExact Exact] [ExactDecoder Right RightExact] [ExactMap RightExact Exact] [Add Exact] [quantizer : Quantizer target Exact] (left : Left) (right : Right) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context (Conversion.prepareBinary (Quantizer.addExact context) (ExactDecoder.decodeTo left) (ExactDecoder.decodeTo right)) (addAs left right mode context)

The context's addition hook followed by one quantization satisfies the composed relation.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_subAs {Left : Type u} {Right : Type v} {target : Type w} {LeftExact : Type x} {RightExact : Type y} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [ExactDecoder Left LeftExact] [ExactMap LeftExact Exact] [ExactDecoder Right RightExact] [ExactMap RightExact Exact] [Sub Exact] [quantizer : Quantizer target Exact] (left : Left) (right : Right) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context (Conversion.prepareBinary (Quantizer.subExact context) (ExactDecoder.decodeTo left) (ExactDecoder.decodeTo right)) (subAs left right mode context)

The context's subtraction hook followed by one quantization satisfies the composed relation.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_mulAs {Left : Type u} {Right : Type v} {target : Type w} {LeftExact : Type x} {RightExact : Type y} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [ExactDecoder Left LeftExact] [ExactMap LeftExact Exact] [ExactDecoder Right RightExact] [ExactMap RightExact Exact] [Mul Exact] [quantizer : Quantizer target Exact] (left : Left) (right : Right) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context (Conversion.prepareBinary (fun (x1 x2 : Exact) => x1 * x2) (ExactDecoder.decodeTo left) (ExactDecoder.decodeTo right)) (mulAs left right mode context)

Exact multiplication followed by one quantization satisfies the composed relational contract.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_divAs {Left : Type u} {Right : Type v} {target : Type w} {LeftExact : Type x} {RightExact : Type y} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] [ExactDecoder Left LeftExact] [ExactMap LeftExact Exact] [ExactDecoder Right RightExact] [ExactMap RightExact Exact] [Zero Exact] [Numerics.ExactZero Exact] [Div Exact] [quantizer : Quantizer target Exact] (left : Left) (right : Right) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context (Conversion.prepareDiv (ExactDecoder.decodeTo left) (ExactDecoder.decodeTo right)) (divAs left right mode context)

Exact division followed by one quantization satisfies the composed relational contract.

theorem FloatLib.Floats.ExecFloat.ConversionProof.preparedSpec_fmaAs {Left : Type u} {Right : Type v} {target : Type w} {LeftExact : Type x} {RightExact : Type y} {Exact : Type z} {Mode : Type} [RoundingModes target Mode] {Addend : Type a} {AddendExact : Type b} [ExactDecoder Left LeftExact] [ExactMap LeftExact Exact] [ExactDecoder Right RightExact] [ExactMap RightExact Exact] [ExactDecoder Addend AddendExact] [ExactMap AddendExact Exact] [Mul Exact] [Add Exact] [quantizer : Quantizer target Exact] (left : Left) (right : Right) (addend : Addend) (mode : Mode) (context : Quantizer.Context target) : Conversion.PreparedSpec context (Conversion.prepareFmaWith (Quantizer.addExact context) (ExactDecoder.decodeTo left) (ExactDecoder.decodeTo right) (ExactDecoder.decodeTo addend)) (fmaAs left right addend mode context)

Exact fused multiply-add followed by one quantization satisfies the composed contract.