1.2 "the proof is in the printf"

This release turns Żmij from a shortest-conversion library into a full floating-point formatter: scientific, fixed, general and hexadecimal notation with a caller-specified precision, long double support covering the x87 80-bit and IEEE binary128 formats, and a std::to_chars-style API. The conversion is now backed by machine-checked Lean 4 proofs.

New Features & API

Precision formatting

• Added write_scientific, write_fixed and write_general, which format with a given precision and match printf's %e, %f and %g, including the default of 6 for a negative precision, %g's notation rule and its trailing-zero removal (#111, #145).

Hexadecimal floats

• Added write_hex, which emits printf %a-style hexadecimal floating point in its shortest form (e.g. -0x1.8p+1) or with a given number of fractional hex digits, correctly rounded (ties to even).

long double

• Added long double support for the x87 80-bit extended and IEEE binary128 formats, in every notation; where long double is double the calls forward. to_decimal(long double) returns a dec_fp<uint128_t>.

std::to_chars-style API

• Added zmij-to-chars.h, which covers the whole floating-point to_chars surface: all three overload forms (shortest, with a format, and with a format and precision) for float, double and long double, over all four chars_format values including hex. The to_chars_result it returns is usable in C++14, where std::to_chars would need C++17, and it is several times faster and smaller than common standard library implementations.

constexpr

• zmij::write is now usable in constant expressions for float and double where std::is_constant_evaluated is available.
• Added ZMIJ_USE_CONSTEXPR, which can be set to 0 to opt out of C++14 relaxed constexpr table generation.

Other

• Added to_decimal overloads for float (#144) and long double, and made dec_fp a template over the significand type.
• Added long_double_buffer_size and the buffer_sizes<Float> trait, which gives the exact buffer size for each format: shortest, scientific, fixed and hex.
• Extended the C API with zmij_write_scientific, zmij_write_fixed, zmij_write_general and zmij_write_hex, each with an _f float variant and matching buffer-size constants, ordered like the C++ header.
• Added minimal CMake install support (#149, thanks @miyanyan) and the ZMIJ_TEST and ZMIJ_EXAMPLE options for skipping the tests and example (#153, thanks @miyanyan).

Formal Verification

The proofs live alongside the tests, build with lake, and contain no sorry.

• Core.lean proves, independently of any algorithm or format, that an exact Schubfach-like selection rule yields a shortest, correctly rounded decimal. Zmij.lean and ZmijPrecision.lean show that Żmij's shortest and fixed-precision binary64 paths implement it, and YY.lean does the same for yy, with YY128.lean and YY80.lean discharging its per-format obligations at IEEE binary128 and the x87 80-bit format.
• Carrying the proof to the wide formats exposed a limitation of yy: packing drops four fractional bits, leaving margin enough to decide every tie at binary64 but not at binary128. Żmij runs yy only above binary64 and now resolves those ties a nibble finer, against the full 64 low bits of the power of ten.

Performance & Code Size

On an Apple M5 Max, float conversion is about 23% faster than in 1.1, and double conversion is 1-4% faster depending on the input:

conversion	1.1	1.2	faster by
float, mixed values	4.82ns	3.72ns	23%
double, mixed values	4.05ns	4.00ns	1%
double, geographic coordinates	3.79ns	3.62ns	4%
double, values in fixed notation	3.86ns	3.81ns	1.5%

• Selected the float fixed/exponential layout from one shuffle table indexed by a clamped decimal exponent instead of branching on it. Floats reach the fixed range often enough that the branch mispredicted, and that cost more than the emit itself; this is most of the 23%.
• Dropped the leading '0' on the float fixed path by shifting in the register rather than storing eight digits and memmoving them back over themselves (based on #151, thanks @IRainman).
• Folded the exponent-shift lookup into a single load. On arm64 the old offset made the lookup pay for an add at the head of the kernel's dependency chain.
• Set extra_shift to 9 so that extra_shift + 1 reuses the base-10 digit-extraction constant, dropping a few immediate moves.
• Scaled subnormals with one multiply instead of a loop.
• Brought the C implementation up to date with the C++ one: the branchless SSE4.1 fixed-notation path, the optional precomputed exponent-string table, and loading constants through a single base pointer.

Measured with test/abtest.py.

Build & Tests

• Fixed the build with older GCC, which rejected the ZMIJ_SPLAT64 initializer on at least 5.3.1 and 6.3.0 (#148, thanks @patrickbkr).
• Split the tests so that the public-API suite runs against the C implementation too.

Breaking Changes

• C: zmij_write_double and zmij_write_float are now zmij_write and zmij_write_f, following libc's sqrt/sqrtf convention and leaving _l free for long double. They return a char* past the last character written instead of a size_t, matching the C++ API.
• C: zmij_float_buffer_size is 17 rather than 16, agreeing with C++'s float_buffer_size.
• C++: dec_fp is now a class template, so spell it dec_fp<>, and its sig field is unsigned.

New Contributors

• @patrickbkr: first contribution in #148
• @miyanyan: first contribution in #149

Thanks also to @IRainman for continued contributions, and to @Pure-Happiness, @ruema, @jsouquie and everyone else who reported issues.

Full Changelog: v1.1...v1.2