A generic, formally verified roundtrip theorem for IEEE 754 float-to-decimal conversion algorithms in Lean 4.
The main theorem: For ANY algorithm that produces a decimal in the acceptance interval, the roundtrip holds:
theorem generic_full_roundtrip (alg : DecimalConversionAlgorithm)
(x : F64) (hfin : x.isFinite) :
(Decimal.parse (Decimal.format (alg.convert x hfin))).map Decimal.toF64 = some xThis covers all algorithms in the Schubfach/shortest-decimal family:
- Ryu (Adams, PLDI 2018)
- Dragonbox/zmij (Jeon, 2020)
- Schubfach (Giulietti, 2022)
- Grisu-Exact (Jeon, 2020)
- Errol (Andrysco et al., POPL 2016)
- Any future algorithm satisfying the interface
All proofs checked by Lean's kernel. No native_decide. No sorry. No axioms.
Supports F64 (binary64) with all five IEEE 754 rounding modes, and F32 (binary32) with RNE.
| Mode | F64 | F32 |
|---|---|---|
| Round-to-nearest-even (RNE) | Fully proven | Fully proven |
| Round-toward-zero (RTZ) | Fully proven | — |
| Round-ties-to-away (RNA) | Fully proven | — |
| Round-toward-positive (RTP) | Fully proven | — |
| Round-toward-negative (RTN) | Fully proven | — |
All entries marked "Fully proven" have zero sorrys, zero axioms, kernel-only trust base.
"Shortest" is irrelevant for correctness. The roundtrip property only requires:
- The algorithm produces a decimal whose rational value is in the acceptance interval — the set of rationals that round to the input float
- The decimal is well-formed (no trailing zeros)
The acceptance interval soundness (schubfach_interval_correct, ~1,100 lines) proves that ANY rational in the interval rounds back to the original float. The format/parse roundtrip (format_parse_roundtrip, ~450 lines) proves that string formatting is lossless. The generic theorem composes these two facts — the algorithm-specific search procedure is abstracted away.
"Shortest" (whether scale-minimal or digit-minimal) is a quality property affecting human readability, not a correctness property. All algorithms listed above are correct; they differ in search strategy, tie-breaking, and optimality guarantees.
structure DecimalConversionAlgorithm where
convert : (x : F64) → x.isFinite → Decimal
well_formed : ∀ x hfin, (convert x hfin).WellFormed
in_interval : ∀ x hfin, x.toRat ≠ 0 →
(schubfachInterval x hfin).contains (convert x hfin).toRat
zero_digits : ∀ x hfin, x.toRat = 0 → (convert x hfin).digits = 0
zero_sign : ∀ x hfin, x.toRat = 0 → (convert x hfin).sign = x.signTo verify a new algorithm, provide these five obligations. The roundtrip theorem follows automatically.
ShortestDecimal/
├── IEEE754/ # IEEE 754 float models
│ ├── Float64.lean # F64 structure (sign, biasedExp, mantissa)
│ ├── Float32.lean # F32 structure (binary32)
│ ├── Classify.lean # F64 float classification
│ ├── Classify32.lean # F32 float classification
│ ├── Value.lean # F64 → ℚ rational interpretation
│ ├── Value32.lean # F32 → ℚ rational interpretation
│ ├── RoundToNearest.lean # ℚ → F64 rounding (RNE)
│ ├── RoundToNearest32.lean # ℚ → F32 rounding (RNE)
│ ├── RoundTowardZero.lean # ℚ → F64 rounding (RTZ)
│ ├── RoundTiesAway.lean # ℚ → F64 rounding (RNA)
│ ├── RoundTowardPos.lean # ℚ → F64 rounding (RTP)
│ ├── RoundTowardNeg.lean # ℚ → F64 rounding (RTN)
│ ├── RoundProof.lean # RNE(toRat(x)) = x for F64
│ ├── RoundProof32.lean # RNE(toRat(x)) = x for F32
│ ├── RoundProofRTZ.lean # RTZ(toRat(x)) = x for F64
│ ├── RoundProofRNA.lean # RNA(toRat(x)) = x for F64
│ ├── RoundProofRTP.lean # RTP(toRat(x)) = x for F64
│ └── RoundProofRTN.lean # RTN(toRat(x)) = x for F64
├── Decimal/ # Decimal representation
│ ├── Decimal.lean # Decimal type + toRat/toF64
│ ├── Format.lean # Decimal → String (scientific notation)
│ └── Parse.lean # String → Decimal parser
├── Interval/ # Acceptance interval
│ ├── Interval.lean # RNE interval for F64 (~1,150 lines)
│ ├── Interval32.lean # RNE interval for F32
│ ├── IntervalRTZ.lean # RTZ interval for F64
│ ├── IntervalRNA.lean # RNA interval for F64
│ ├── IntervalRTP.lean # RTP interval for F64
│ ├── IntervalRTN.lean # RTN interval for F64
│ └── CeilHelper.lean # Shared ceiling/floor lemmas
├── Roundtrip/ # String roundtrip
│ └── FormatParse.lean # parse(format(d)) = d (~450 lines)
├── Generic/ # Algorithm-independent interface
│ ├── Algorithm.lean # DecimalConversionAlgorithm (F64/RNE)
│ ├── Algorithm32.lean # DecimalConversionAlgorithm32 (F32/RNE)
│ ├── AlgorithmRTZ.lean # F64/RTZ algorithm interface
│ ├── AlgorithmRNA.lean # F64/RNA algorithm interface
│ ├── AlgorithmRTP.lean # F64/RTP algorithm interface
│ ├── AlgorithmRTN.lean # F64/RTN algorithm interface
│ ├── Roundtrip.lean # generic_full_roundtrip (F64/RNE)
│ ├── Roundtrip32.lean # generic_full_roundtrip32 (F32/RNE)
│ ├── RoundtripRTZ.lean # generic roundtrip (F64/RTZ)
│ ├── RoundtripRNA.lean # generic roundtrip (F64/RNA)
│ ├── RoundtripRTP.lean # generic roundtrip (F64/RTP)
│ └── RoundtripRTN.lean # generic roundtrip (F64/RTN)
└── Examples/
└── RyuInstance.lean # Example: Ryu instantiation sketch
~7,848 lines of Lean. Zero sorrys. Zero axioms. Kernel-only trust base.
lake build # ~20 min first build (fetches Mathlib)- Define your algorithm as a Lean function:
myAlg : (x : F64) → x.isFinite → Decimal - Prove well-formedness: the output has no trailing zeros
- Prove interval membership: for non-zero x, the output's
toRatis inschubfachInterval x hfin - Handle zero: output has
digits = 0and matching sign - Instantiate
DecimalConversionAlgorithmand get the roundtrip theorem for free
See ryu-lean4 for a concrete example.
The roundtrip proof decomposes into three independent layers:
Layer 1: Acceptance Interval Soundness (schubfach_interval_correct)
"Any rational in [u·2^e₂, w·2^e₂] rounds to x under RNE"
~1,100 lines. The hardest proof. Algorithm-independent.
Layer 2: String Format/Parse Roundtrip (format_parse_roundtrip)
"parse(format(d)) = d for well-formed Decimals"
~450 lines. 8-layer proof. Completely independent of IEEE 754.
Layer 3: Generic Composition (generic_full_roundtrip)
"in_interval + well_formed → roundtrip"
~30 lines. Composes Layer 1 and Layer 2.
The generic theorem is 30 lines because all the hard work is in the layers.
- ryu-lean4 — Verified Ryu algorithm instantiation (~3,230 lines). Proves the Ryu-specific search (
findDigits) produces output in the acceptance interval. - nickelean — Verified JSON serialization for Nickel, using this library + ryu-lean4.
- Nadezhin verify-todec — Partial ACL2 verification of Schubfach's mathematical lemmas (precision sufficiency).
- Flocq — Coq library for floating-point arithmetic (Boldo, Melquiond). Formalizes rounding but not decimal conversion.
- Adams, "Ryū: fast float-to-string conversion", PLDI 2018 (paper)
- Jeon, "Dragonbox: A New Floating-Point Binary-to-Decimal Conversion Algorithm", 2020 (paper)
- Giulietti, "The Schubfach way to render doubles", 2022 (paper)
- Loitsch, "Printing floating-point numbers quickly and accurately with integers", PLDI 2010 (paper)
- Andrysco et al., "Printing floating-point numbers: a faster, always correct method", POPL 2016 (paper)
- Champagne Gareau & Lemire, "How (Not) to Convert Binary Numbers to Decimal", 2026 (arXiv)
MIT