Challenge 28 (flt2dec): 12 of 12 functions verified via Kani

[gui-wf]

Challenge 28 (flt2dec): 12 of 12 functions verified via Kani

Opening as draft to invite collaborative review on three deviations from the established verify-rust-std pattern (called out explicitly under "Design decisions reviewers may question" below). All 12 functions verify end-to-end under Kani 0.65; the deviations are about how the proofs are structured, not whether they pass.

Closes Challenge 28 by verifying all 12 listed functions end-to-end under Kani 0.65. Reproduce with nix run .#verify -- flt2dec, ... flt2dec-grisu-strategies, ... flt2dec-grisu-wrappers, and ... flt2dec-dragon-strategies from the repo root. The work is partitioned into four flake targets to keep each CBMC run tractable (the dragon run depends on a release profile, and the grisu strategy run is the only target above one minute). Branch: challenge-28-flt2dec-helpers.

What's verified

flt2dec (module root):

• digits_to_dec_str, digits_to_exp_str
• to_shortest_str, to_shortest_exp_str, to_exact_exp_str, to_exact_fixed_str (monomorphised to f32, per the spec's "primitive types only" clause for generic T).

flt2dec::strategy::grisu:

• format_shortest_opt, format_exact_opt
• format_shortest, format_exact (the lifetime-laundering wrappers).

flt2dec::strategy::dragon:

• format_shortest, format_exact.

Verification approach

• Public helpers and the four to_*_str functions. Direct Kani proofs over symbolic Decoded / digit-buffer inputs. No stubs; the CBMC formula is small enough that the harnesses finish in ~2 seconds combined.
• grisu::format_shortest_opt / format_exact_opt. Stubs derived from the Loitsch PLDI 2010 paper: Fp::mul as identity on the mantissa (preserves the algorithm's required monotonic ordering of three successive multiplications), cached_power and max_pow10_no_more_than as range-bounded havoc. round_and_weed is hoisted to a free function so it can be reasoned about separately.
• grisu::format_shortest / format_exact wrappers. Hand-written buf-synthesizing stubs for the inner _opt call and the dragon fallback. Only the wrapper's own unsafe reborrow is exercised; this is the actual unsafe surface the wrappers add over their callees.
• dragon::format_shortest / format_exact. Four levers, documented in ADR 0004's Resolution section: (1) tightened the symbolic Decoded input to match decode_finite's real output shape (minus = 1, plus in {1, 2}); (2) stubbed div_rem_upto_16 to return (d, x) with kani::assume(d < 10), encoding the helper's algorithmic invariant directly; (3) bounded the digit-generation loop via a CMP_CALLS static counter on stub_big_cmp; (4) built the dragon target with CARGO_PROFILE_DEV_DEBUG_ASSERTIONS=false. Both proofs combined finish in under 11 seconds.

Design decisions reviewers may question

Three of these are off-pattern compared to merged work in this repo (a precedent survey of merged PRs found zero prior use of doc-comment safety contracts, zero kani::stub plus kani::assume-postcondition stubs - only stub_verified plus proven #[ensures], per the transmute_unchecked_wrapper family in library/core/src/intrinsics/mod.rs - and zero CARGO_PROFILE_* overrides). Each is explained below with the reasoning; happy to iterate on any.

• Doc-comment # Safety contract sections instead of #[safety::requires]. Blocked by Kani upstream issue model-checking/kani#4591 (open, assigned, milestone Contracts): Kani 0.65 cannot apply #[kani::stub] to a function that carries #[requires], with a "Failed to find contract closure" compile error. All four contracted functions (format_shortest_opt, format_exact_opt, dragon::format_shortest, dragon::format_exact) are stubbed by at least one other harness in this PR, so the two attributes cannot coexist. Reproduced locally in a worktree spike: dropping the doc block and adding #[safety::requires(d.mant > 0)] etc. to format_exact_opt fails to compile the core crate. Preconditions remain enforced at runtime via assert! in the function body, and the strategy harnesses encode them via kani::assume. When Rewrite the coercion code to be more readable, more sound, and to reborrow when needed. rust-lang/rust#4591 lands, the migration is mechanical: drop the doc block, drop the body assert!s, add the attributes. Each of the four contract blocks now references the upstream issue in-line.
• stub_div_rem_upto_16 encoding d < 10 as kani::assume. Sound for the Challenge 28 safety mandate (no UB on the MaybeUninit buffer): the assumed postcondition matches the helper's actual algorithmic invariant mant + plus <= scale * 10 => d < 10, proved by Burger and Dybvig (1996). The canonical alternative would be #[kani::stub_verified] with a proven #[ensures] (the transmute_unchecked_wrapper pattern). Deriving d < 10 automatically through that path requires per-method #[ensures] on the entire Big32x40 API plus a separately tractable proof for each; ADR 0004's Resolution and closing paragraph documents this as the next-iteration path, and the kani_havoc/kani_size helpers in bignum.rs are designed to support it. The current stub is the smallest change that closes the dragon harnesses; happy to invest in stub_verified if reviewers prefer it as a follow-up before merge.
• CMP_CALLS static counter on stub_big_cmp. Bounds the digit-generation loop to fewer than MAX_SIG_DIGITS = 17 iterations. The unbounded path admitted by raw havoc is a stub artefact - the real algorithm terminates monotonically as mant.mul_small(10) drives the comparison - not a real algorithmic behaviour. Sound for safety, restricted in coverage. Counter is reset on each harness entry.
• CARGO_PROFILE_DEV_DEBUG_ASSERTIONS=false for the dragon target only. Challenge 28's mandate is "no UB" (dangling/misaligned pointers, intrinsic-driven UB, mutating immutable bytes, producing invalid values). The debug_assert!(d < 10) and debug_assert!(mant < scale) in dragon.rs are algorithm-correctness invariants - they hold in the real algorithm by the bignum invariant - not safety obligations. Release-mode is what users run, and all UB-relevant CBMC checks (pointer dereference, OOB, overflow) remain enabled. The setting is scoped to the single flt2dec-dragon-strategies flake target via an environment variable; it does not affect the other three targets or any library code outside that target's verification build.
• Production-code changes. Two, both #[cfg(kani)]-gated: #[cfg_attr(kani, recursion_limit = "256")] in library/core/src/lib.rs (the per-harness stack of #[kani::stub] attributes exceeded the default macro-expansion limit), and kani_havoc / kani_size helpers in library/core/src/num/bignum.rs. Zero impact on production semantics; cargo's release builds compile these out entirely.

Test plan

• nix run .#verify -- flt2dec (6 functions, ~2s)
• nix run .#verify -- flt2dec-grisu-strategies (2 functions, ~7 min)
• nix run .#verify -- flt2dec-grisu-wrappers (2 functions, ~0.3s)
• nix run .#verify -- flt2dec-dragon-strategies (2 functions, ~10s)
• Default memory cap: 24 GiB. Override with VERIFY_MEMORY_MAX (e.g. VERIFY_MEMORY_MAX=0 to disable).

References

• docs/decisions/0001-target-flt2dec-helpers-first.md - why the two private helpers were the first target.
• docs/decisions/0002-nix-flake-for-local-kani.md - flake design for reproducible Kani runs.
• docs/decisions/0003-grisu-needs-contract-decomposition.md - why the strategy functions needed contract decomposition.
• docs/decisions/0004-dragon-stubs-too-loose-for-safety.md - dragon precision gap and the four-lever resolution that closed it.
• Burger and Dybvig, Printing Floating-Point Numbers Quickly and Accurately, PLDI 1996 - the Dragon4 algorithm and the d < 10 invariant.
• Loitsch, Printing Floating-Point Numbers Quickly and Accurately with Integers, PLDI 2010 - the Grisu family and the monotonic-ordering property exploited by the identity-on-f Fp::mul stub.
• model-checking/kani#4591 - upstream blocker for #[safety::requires] plus #[kani::stub] coexistence.