Implementation tracking: issue #10. Float literals, addition, subtraction,
multiplication, float(...) and integer/bool, float and mixed true division connect
to the same kernel-reducible binary64 core on both interpreter surfaces.
The float_lab real extracted artifact has kernel proofs, differential rows
and script transcripts. This is not complete float-language support:
remaining operators, constructor protocols, NaN behavior outside ordinary
arithmetic, hashing and identity are still language-coverage work.
LeanModels.Python.Float64 stores a 64-bit word, not Lean's native Float.
Classification, exact rational decoding, nearest-even rational rounding and
decimal rendering use kernel-reducible integer operations. The source oracle
is CPython 3.9 on the binary64 platforms used by the regression suite.
Rounding keeps the sign separate from the nonnegative numerator and positive denominator. It selects the binary scale from the exact ratio, clamps the smallest unit to 2^-1074, rounds the significand to nearest with even ties, and handles carry into the next exponent. This preserves negative zero at zero and underflow, and distinguishes the largest finite value from overflow.
Integer true division rounds the ratio directly. It must not first convert
both operands to floats: 10**400 / 10**400 is 1.0 in CPython even though
converting either operand alone overflows. Float64.divideInt distinguishes
division by zero from a ratio whose rounded result overflows. Interpreter
adapters must retain their distinct Python exception classes and messages.
Mixed integer/float division is different: CPython first converts the integer,
then divides the two floats. 10**400 / 0.0 therefore raises the conversion
OverflowError, not ZeroDivisionError. The core provides conversion plus
float division separately, and retains that evaluation order. A
finite float quotient can overflow to infinity without raising the integer
division overflow exception. A nonzero finite denominator and infinite
numerator produce signed infinity; a finite numerator and infinite denominator
produce signed zero. Both signs use the operands' sign XOR, including signed
zero and subnormal inputs. A zero denominator raises ZeroDivisionError even
when the numerator is infinite or NaN. Mixed integer conversion still happens
first, including overflow with an infinite or NaN operand. NaN inputs are
quieted in place, preserving payload and sign, with the left operand winning
when both are NaN. Infinity divided by infinity uses CPython 3.9's pinned
canonical negative quiet-NaN word, after the zero-denominator and
mixed-conversion checks. The legacy Float64.divideFinite helper name is
retained; the NaN-aware wrapper shares its determined infinity cases without a
second interpreter path.
Addition, subtraction and multiplication compute with exact rational operands
and round once to nearest-even binary64. Mixed integer/Boolean operands are
converted to binary64 first, including their conversion overflow; consequently
9007199254740993 + 1.0 is 9007199254740992.0 and 10**400 * 0.0 raises
OverflowError rather than returning zero. Cancellation returns positive
zero, except that the IEEE same-sign zero rules preserve negative zero in
-0.0 + -0.0 and -0.0 - 0.0. Multiplication preserves the sign XOR through
zero and underflow. Float overflow produces signed infinity. Nonindeterminate infinity operations are admitted. For binary +, -, and
*, NaN inputs are quieted in place, preserving the payload and sign; when
both operands are NaN, the left operand wins. Invalid inf - inf, opposite-sign
inf + inf, and inf * 0 use CPython 3.9's pinned canonical negative quiet-NaN
word. True division, floor division, remainder, and divmod use the same
quieting rule, with zero-denominator errors taking priority.
Float ordering and mixed float/integer comparison use the exact decoded value. They do not round the integer: 9007199254740992.0 is strictly less than 9007199254740993 even though converting that integer to binary64 loses the distinction. Numerical NaN comparisons are false. Integer conversion truncates toward zero, while exact-integral conversion is available for future dictionary key normalization; neither conversion claims an answer for an infinity or NaN.
Decimal rendering computes the exact midpoints to the adjacent binary64 values, including the narrower lower interval at powers of two and the virtual finite successor of the largest finite value. Endpoint inclusion follows the significand's parity. It searches up to 17 significant digits, chooses the closest admissible decimal with even ties, and selects fixed or scientific notation from the resulting decimal exponent. Signed zero, infinities and NaNs have separate representations.
The reference describes binary64 representation and shortest round-trip display in the CPython 3.9 floating-point tutorial. The implementation is checked against the actual pinned interpreter, not just a reading of that explanation.
Float //, % and divmod share a pure binary64 quotient/remainder worker.
Mixed integer/Boolean operands convert before the arithmetic, retaining
conversion overflow even when the other operand is NaN or the divisor is zero.
All-integer/Boolean operations keep their existing arbitrary-precision path.
The remainder starts with the exact magnitude remainder, with the numerator's
sign. The quotient then uses binary64-rounded subtraction and division, not
the mathematical floor of the original rational ratio: 1.0 // 0.1 is 9.0.
A nonzero remainder with the wrong sign is corrected by rounded addition of
the divisor, alongside rounded subtraction of one from the quotient. The
quotient is snapped to an integral binary64 value after these corrections.
Zero remainders take the divisor's sign; zero quotients take the true quotient's
sign. Finite operands can produce an infinite quotient without an exception.
A finite numerator with an infinite divisor has a determined result, including
the opposite-sign correction to quotient -1.0 and an infinite remainder.
An infinite numerator produces the pinned canonical negative quiet NaN. NaN
operands are quieted in place, with the left operand winning when both are NaN;
zero-divisor exceptions come first after mixed conversion. //, % and
divmod preserve their distinct CPython messages and common exception class,
including ArithmeticError/ZeroDivisionError handlers. The source
oracle is CPython 3.9's float operation sequence, with differential checks
against the actual pinned interpreter; this is not an exact-rational shortcut.
The extractor records a float literal/default as an unsigned decimal binary64
word using struct.pack, without evaluating a program expression. Ingestion
validates 0 <= bits < 2^64; boundary JSON uses
{"t":"float","bits":"<unsigned decimal word>"} and rejects an invalid
word rather than truncating it. Const.float, Val.float and RVal.float
preserve the word through reflection, thaw/freeze and heap-boundary proofs.
The typed proof surface supplies PyFloat (definitionally Float64) and exact
ToVal marshalling, so artifact theorem statements need not expose Val.
Both interpreters share the numeric adapters in Semantics.lean. Truthiness,
unary signs, abs, int, scalar/container rendering, bare %s/%r/finite
%d, f-string conversions and exact mixed comparisons are wired. int(nan)
and int(inf) retain their distinct exception classes/messages. Integer true
division and float division have distinct zero-division messages, and the
ArithmeticError handler relation covers both plus OverflowError.
Finite numeric sorted/max/min use the shared exact order. NaN comparisons
with </<=/>/>= are false, but ordering NaNs inside containers refuses:
the insertion-sort implementation cannot claim CPython's results for a
non-total order. NaN equality and non-finite float dictionary/set keys
(including nested tuple keys) also refuse. Finite float keys use Python's
numeric equality, including equality with equal integers and signed zeros,
through the same linear key relation as other scalar keys. Existing float
attributes remain loud rather than
fabricating missing-attribute exceptions. Other float arithmetic must not fall
into an integer-only TypeError.
The monadic itertools.count frame now admits immediate integer, Boolean, and
binary64 start/step values, including NaNs and infinities. It keeps the first
value's CPython subtype (for example, count(True, 2) yields True, 3, 5) and
advances with the shared numeric addition worker, so mixed integer/float
stepping preserves binary64 rounding and NaN payload/sign propagation. The proof
Both interpreter surfaces use the value-carrying frame for these finite rows;
invalid nonnumeric arguments and excessive positional arity retain their
faithful exceptions.
The new value forms add scalar proof cases without changing existing theorem
statements. float_lab proves concrete results against its extracted Python
file by kernel reduction, including augmented assignment and mixed rounding.
It also proves cancellation for every finite binary64 input via the shared
arithmetic lemma. This does not claim general symbolic float automation;
the global walker has no numeric-literal shortcuts.
NaN introduces an additional object-identity issue: its numerical comparison is false, but container element comparison can shortcut on object identity. An immediate value representation must not fabricate the answer when that identity is unavailable. Dictionary key normalization also must preserve the equality of finite floats with equal integers and signed zeros. These cases remain in scope; refusing an unresolved case is not an exclusion or a reason to weaken an existing theorem.
Broader float arithmetic outside +, -, *, //, %, and divmod,
remaining constructor protocols, formatting specifications, methods, hashing
and identity remain language-coverage work. Undefined or
platform-dependent numerical details require an explicit model/oracle
parameter when they cannot be decided from the admitted state.
float() returns positive zero. One positional argument preserves an existing
binary64 word, converts an integer or Boolean with nearest-even rounding (and
the integer-conversion overflow exception), or parses a decimal string.
Decimal strings admit signs, a decimal point, signed exponents and underscores
strictly between digits. Unicode decimal digits and surrounding whitespace
use the pinned CPython 3.9 Unicode 13.0.0 inventory; ASCII control characters
are not broadened to Unicode isspace. inf and infinity are case-insensitive.
Decimal overflow produces signed infinity, underflow produces signed zero,
and finite results use the same exact rational rounding as arithmetic. ASCII
bytes use the same parser and preserve the bytes-specific ValueError
rendering; non-ASCII bytes and NaN payload spellings remain loud. Canonical
case-insensitive nan, -NaN, and +nAn forms preserve CPython's quiet-NaN
word and explicit sign bit.
Malformed strings raise the repr-rendered ValueError when the shared
string renderer can decide its message exactly. Quote selection traverses
the structural code-point list, keeping error rendering kernel-reducible.
Unresolved Unicode repr and payload spellings such as nan(1) remain explicit
unfinished work. Heap containers and instances without an admitted __float__
protocol now take CPython's ordinary non-numeric TypeError; custom object
conversion protocols remain unfinished. Existing NaN words are preserved without selecting
a new payload. Positional arity and immediate nonnumeric type errors retain
CPython's exception classes and messages; keyword construction stays loud
until its evaluation and positional-only protocol are modeled.
lake build LeanModels.Python.Float64Tests checks closed kernel proofs for
rounding, signed zero, subnormal ties, numerical equality, conversions,
division, arithmetic and decimal parsing. The closed numeric-arithmetic
checks have empty axiom reports; native execution is not a proof tactic.
Text parsing, the general finite-cancellation lemma and artifact proofs use
only Lean's standard propext, Classical.choice and Quot.sound, not native
computation or new axioms.
python3.9 harness/float64_test.py compares the core against CPython's bit
patterns, repr, integer and float division, addition/subtraction/
multiplication, unary negation, mixed comparisons, conversions and exception
messages in a single Lean
process. Decimal parsing tests also compare the complete Unicode decimal-zero
inventory against the pinned unicodedata, every decimal digit block,
Unicode whitespace, malformed syntax, extreme exponents and rounding ties.
It covers every finite exponent field at selected fraction
boundaries, both signs, arbitrary-size integer ratios, subnormal and overflow
ties, non-finite bit patterns and deterministic random samples. This is a
numeric-core test, not the language-level differential harness. NaN-payload
refusals are counted separately from successful numerical matches.