Proof contracts for transcendental approximations

These contracts state and prove accuracy claims about an approximation:

1. a real function value lies in a proved enclosure;
2. an executable result satisfies a proved absolute-error budget; and
3. an enclosure is narrow enough that both endpoints round to the same destination value.

When both endpoints round alike, monotonicity forces the enclosed function value to round there too. StableEnclosure.roundAt_eq_roundAt_lower proves this fact. Constructing an enclosure requires Lean proofs of both bounds; external numerical output alone does not supply them.

IEEE exceptional-value behavior and the sign of an exact zero remain separate bit-level obligations. roundAt is the finite real grid semantics.

ApproximationCertificateOn and CorrectlyRoundedCertificateOn restrict the finite-real guarantees to an explicit predicate on encoded inputs. For example, a logarithm certificate can use fun input ↦ 0 < toReal input; an exponential certificate can use a proved input range on which the result remains finite. Membership never replaces the obligation to prove output finiteness. Outside the domain these certificates make no claim, so exceptional-value and overflow behavior need separate specifications. The certificates without On apply to every finite input and are equivalent to the domain-restricted certificates with domain fun _ ↦ True.

References

• IEEE 754-2019, Section 9.2, recommended correctly rounded operations.
• F. de Dinechin, C. Lauter, and J.-M. Muller, “Fast and correctly rounded logarithms in double-precision,” RAIRO-Theoretical Informatics and Applications 41(1), 2007.
• S. Boldo and G. Melquiond, “Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq,” IEEE ARITH 2011.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure (f : ℝ → ℝ) (x : ℝ) : Type

A checked closed real enclosure of f x.

• lower : ℝ

  Proved lower endpoint.

• upper : ℝ

  Proved upper endpoint.

• lower_le : self.lower ≤ f x

  The lower endpoint does not exceed the exact value.

• le_upper : f x ≤ self.upper

  The exact value does not exceed the upper endpoint.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.ofRational {f : ℝ → ℝ} {x : ℝ} (interval : Numerics.RationalInterval) (hx : interval.Contains (f x)) : RealEnclosure f x

Use proved executable rational endpoints in a real-valued approximation contract.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.expRational (x : ℚ) (degree : ℕ) : RealEnclosure Real.exp ↑x

A Taylor enclosure whose rational endpoints are computed inside FloatLib.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.logRational (x : ℚ) (degree : ℕ) (hx : 0 < x) : RealEnclosure Real.log ↑x

A proved rational logarithm enclosure for a positive input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.mem_Icc {f : ℝ → ℝ} {x : ℝ} (enclosure : RealEnclosure f x) : f x ∈ Set.Icc enclosure.lower enclosure.upper

The exact function value belongs to its enclosure.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.lower_le_upper {f : ℝ → ℝ} {x : ℝ} (enclosure : RealEnclosure f x) : enclosure.lower ≤ enclosure.upper

Every proved enclosure has ordered endpoints.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.abs_sub_le_width {f : ℝ → ℝ} {x candidate : ℝ} (enclosure : RealEnclosure f x) (hcandidate : enclosure.lower ≤ candidate ∧ candidate ≤ enclosure.upper) : |candidate - f x| ≤ enclosure.upper - enclosure.lower

Any candidate lying in the same enclosure has absolute error at most its width.

This conservative bound is often sufficient for a first verified implementation. A sharper algorithm-specific proof can populate ApproximationCertificate directly.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.ofMonotone {f : ℝ → ℝ} (hf : Monotone f) (input : Interval.RInterval) {x : ℝ} (hx : x ∈ input) : RealEnclosure f x

Build an enclosure by monotonicity from a real input interval.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.outward {f : ℝ → ℝ} {x : ℝ} (rounder : Interval.Rounder) (enclosure : RealEnclosure f x) : RealEnclosure f x

Round a proved real enclosure outward with any sound endpoint rounder.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.exp (input : Interval.RInterval) {x : ℝ} (hx : x ∈ input) : RealEnclosure Real.exp x

Sound exponential enclosure on an input interval.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.sinh (input : Interval.RInterval) {x : ℝ} (hx : x ∈ input) : RealEnclosure Real.sinh x

Sound hyperbolic-sine enclosure on an input interval.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.sin (x : ℝ) : RealEnclosure Real.sin x

Enclose sine in [-1, 1] for every real argument.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.cos (x : ℝ) : RealEnclosure Real.cos x

Enclose cosine in [-1, 1] for every real argument.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.tanh (x : ℝ) : RealEnclosure Real.tanh x

Enclose hyperbolic tangent in [-1, 1] for every real argument.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.cosh (input : Interval.RInterval) {x : ℝ} (hx : x ∈ input) : RealEnclosure Real.cosh x

Sound hyperbolic-cosine enclosure on an input interval.

The upper endpoint uses the largest absolute endpoint because cosh is even and increases with absolute value.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.log (rounder : Interval.Rounder) (input : Interval.RInterval) {x : ℝ} (hpositive : 0 < input.lo) (hx : x ∈ input) : RealEnclosure Real.log x

Convert the existing proved logarithm interval into the common enclosure contract.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure.sqrt (rounder : Interval.Rounder) (input : Interval.RInterval) {x : ℝ} (hx : x ∈ input) : RealEnclosure Real.sqrt x

Convert the existing proved square-root interval into the common enclosure contract.

No sign hypothesis is needed: Real.sqrt is zero on negative arguments and monotone on all of ℝ.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.StableEnclosure (fmt : FloatFormat) (f : ℝ → ℝ) (x : ℝ) extends FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.RealEnclosure f x : Type

A proved enclosure whose endpoints select one nearest-even destination-grid value.

The inherited enclosure bounds and the endpoint-rounding equality are all proof obligations.

• lower : ℝ
• upper : ℝ
• lower_le : self.lower ≤ f x
• le_upper : f x ≤ self.upper
• endpoints_round_same : roundAt fmt self.lower = roundAt fmt self.upper

  Both enclosure endpoints round to the same finite-grid real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.StableEnclosure.roundAt_eq_roundAt_lower {fmt : FloatFormat} {f : ℝ → ℝ} {x : ℝ} (enclosure : StableEnclosure fmt f x) : roundAt fmt (f x) = roundAt fmt enclosure.lower

A stable enclosure determines the correctly rounded real value of the exact function.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CertifiedRoundedResult (fmt : FloatFormat) (f : ℝ → ℝ) (x : ℝ) extends FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.StableEnclosure fmt f x : Type

A finite encoded result backed by a stable real enclosure.

The final equality connects the stored result to the lower endpoint's rounded value. Together with stability, this proves correct nearest-even rounding of the exact function in finite real semantics.

• lower : ℝ
• upper : ℝ
• lower_le : self.lower ≤ f x
• le_upper : f x ≤ self.upper
• endpoints_round_same : roundAt fmt self.lower = roundAt fmt self.upper
• value : Model fmt

  Encoded result returned by an implementation.

• value_finite : self.value.isFinite = true

  The encoded result is finite, so toReal is its complete numerical magnitude.

• value_eq_lower_round : self.value.toReal = roundAt fmt self.lower

  The implementation selected the endpoint-certified rounded real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CertifiedRoundedResult.toReal_value_eq_roundAt {fmt : FloatFormat} {f : ℝ → ℝ} {x : ℝ} (result : CertifiedRoundedResult fmt f x) : result.value.toReal = roundAt fmt (f x)

The certified encoded result has the correctly rounded real value of f x.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.ApproximationCertificate (fmt : FloatFormat) (f : ℝ → ℝ) (approximation : Model fmt → Model fmt) (errorBudget : Model fmt → ℝ) : Prop

Whole-algorithm absolute-error contract for an executable unary approximation.

The fields require output finiteness and an error bound for every finite input.

• budget_nonnegative (input : Model fmt) : 0 ≤ errorBudget input

  Every advertised error budget is nonnegative.

• output_finite (input : Model fmt) : input.isFinite = true → (approximation input).isFinite = true

  Finite inputs in scope produce finite outputs.

• error_le (input : Model fmt) : input.isFinite = true → |(approximation input).toReal - f input.toReal| ≤ errorBudget input

  The decoded result satisfies the advertised real absolute-error budget.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificate (fmt : FloatFormat) (f : ℝ → ℝ) (implementation : Model fmt → Model fmt) : Prop

Whole-algorithm correctly-rounded finite-real contract.

Both components are propositions, so the certificate adds no runtime data.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificate.output_finite {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} (certificate : CorrectlyRoundedCertificate fmt f implementation) (input : Model fmt) : input.isFinite = true → (implementation input).isFinite = true

Finite inputs in scope produce finite outputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificate.toReal_eq_roundAt {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} (certificate : CorrectlyRoundedCertificate fmt f implementation) (input : Model fmt) : input.isFinite = true → (implementation input).toReal = roundAt fmt (f input.toReal)

At every finite input, the result equals nearest-even rounding of the exact real function.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.ApproximationCertificateOn (fmt : FloatFormat) (f : ℝ → ℝ) (approximation : Model fmt → Model fmt) (errorBudget : Model fmt → ℝ) (domain : Model fmt → Prop) : Prop

Absolute-error contract on an explicit domain of encoded inputs.

The domain can express mathematical restrictions, such as positivity for logarithms, and the range on which finite output is promised. Budgets must be nonnegative on the domain; output finiteness and accuracy are required for every finite input in that domain. In particular, merely restricting the mathematical domain does not discharge the output-finiteness obligation.

• budget_nonnegative (input : Model fmt) : domain input → 0 ≤ errorBudget input

  Every budget advertised on the domain is nonnegative.

• output_finite (input : Model fmt) : input.isFinite = true → domain input → (approximation input).isFinite = true

  Finite inputs in the domain produce finite outputs.

• error_le (input : Model fmt) : input.isFinite = true → domain input → |(approximation input).toReal - f input.toReal| ≤ errorBudget input

  The decoded result satisfies the budget at every finite input in the domain.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.ApproximationCertificateOn.mono {fmt : FloatFormat} {f : ℝ → ℝ} {approximation : Model fmt → Model fmt} {errorBudget : Model fmt → ℝ} {domain smallerDomain : Model fmt → Prop} (certificate : ApproximationCertificateOn fmt f approximation errorBudget domain) (hsub : ∀ (input : Model fmt), smallerDomain input → domain input) : ApproximationCertificateOn fmt f approximation errorBudget smallerDomain

Restrict an absolute-error certificate to a smaller domain.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.ApproximationCertificate.on_domain {fmt : FloatFormat} {f : ℝ → ℝ} {approximation : Model fmt → Model fmt} {errorBudget : Model fmt → ℝ} (certificate : ApproximationCertificate fmt f approximation errorBudget) (domain : Model fmt → Prop) : ApproximationCertificateOn fmt f approximation errorBudget domain

A whole-algorithm absolute-error certificate applies on any chosen domain.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.ApproximationCertificateOn.true_iff {fmt : FloatFormat} {f : ℝ → ℝ} {approximation : Model fmt → Model fmt} {errorBudget : Model fmt → ℝ} : (ApproximationCertificateOn fmt f approximation errorBudget fun (x : Model fmt) => True) ↔ ApproximationCertificate fmt f approximation errorBudget

The unrestricted domain gives the absolute-error contract for all finite inputs.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn (fmt : FloatFormat) (f : ℝ → ℝ) (implementation : Model fmt → Model fmt) (domain : Model fmt → Prop) : Prop

Correct nearest-even finite-real rounding on an explicit domain of encoded inputs.

Every finite input in the domain must produce a finite result with the stated rounded real value. This does not certify overflow, exceptional values, or the sign of zero: roundAt has no upper exponent bound, and those behaviors need separate bit-level specifications.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn.output_finite {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} {domain : Model fmt → Prop} (certificate : CorrectlyRoundedCertificateOn fmt f implementation domain) (input : Model fmt) : input.isFinite = true → domain input → (implementation input).isFinite = true

Finite inputs in the certified domain produce finite outputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn.toReal_eq_roundAt {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} {domain : Model fmt → Prop} (certificate : CorrectlyRoundedCertificateOn fmt f implementation domain) (input : Model fmt) : input.isFinite = true → domain input → (implementation input).toReal = roundAt fmt (f input.toReal)

At finite inputs in the domain, the result equals rounding of the exact real function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn.mono {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} {domain smallerDomain : Model fmt → Prop} (certificate : CorrectlyRoundedCertificateOn fmt f implementation domain) (hsub : ∀ (input : Model fmt), smallerDomain input → domain input) : CorrectlyRoundedCertificateOn fmt f implementation smallerDomain

Restrict a correctly-rounded certificate to a smaller domain.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn.of_certified_results {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} {domain : Model fmt → Prop} (results : (input : Model fmt) → input.isFinite = true → domain input → CertifiedRoundedResult fmt f input.toReal) (hvalue : ∀ (input : Model fmt) (hfinite : input.isFinite = true) (hdomain : domain input), (results input hfinite hdomain).value = implementation input) : CorrectlyRoundedCertificateOn fmt f implementation domain

Assemble a domain certificate from stable enclosures certifying the implementation's results.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificate.on_domain {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} (certificate : CorrectlyRoundedCertificate fmt f implementation) (domain : Model fmt → Prop) : CorrectlyRoundedCertificateOn fmt f implementation domain

A whole-algorithm correctly-rounded certificate applies on any chosen domain.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Contract.CorrectlyRoundedCertificateOn.true_iff {fmt : FloatFormat} {f : ℝ → ℝ} {implementation : Model fmt → Model fmt} : (CorrectlyRoundedCertificateOn fmt f implementation fun (x : Model fmt) => True) ↔ CorrectlyRoundedCertificate fmt f implementation

The unrestricted domain gives the correct-rounding contract for all finite inputs.