Challenge 28: Verify flt2dec safety with Kani

[v3risec]

Summary

This PR solves Challenge 28 by adding Kani verification for functions in core::num::flt2dec, including the formatter layer and the Dragon/Grisu digit-generation strategies.

All verification-only code is gated behind #[cfg(kani)].

Verification Coverage Report (12/12 Verified)

Target	Coverage
digits_to_dec_str	harness_digits_to_dec_str verifies symbolic digit buffers, exponent placement, fractional padding, and all returned Part prefixes.
digits_to_exp_str	harness_digits_to_exp_str verifies symbolic exponents, significant-digit padding, e/E cases, and returned Part initialization.
to_shortest_str	Per-primitive harnesses for f16 when available, f32, and f64; covers NaN, infinity, zero, finite inputs, signs, symbolic fractional padding, and initialized formatter output.
to_shortest_exp_str	Per-primitive harnesses cover NaN, infinity, zero, finite inputs, symbolic decimal/exponential bounds, signs, and formatter composition.
to_exact_exp_str	Per-primitive harnesses cover symbolic ndigits > 0, non-finite and finite paths, and exact formatter output.
to_exact_fixed_str	Per-primitive harnesses cover symbolic fixed precision, including the empty digit result used when fixed precision rounds to zero.
grisu::format_shortest_opt	Verifies shortest-mode digit writes, initialized prefixes, assume_init_mut call sites, and the round_and_weed contract.
grisu::format_shortest	Verifies the unsafe lifetime-laundering fallback wrapper using initialized-output stubs for the optimized and Dragon paths.
grisu::format_exact_opt	Verifies exact/fixed-mode digit writes, integral/fractional loops, possibly_round, initialized prefixes, and carry append bounds.
grisu::format_exact	Verifies the exact/fixed fallback wrapper and buffer reuse discipline.
dragon::format_shortest	Verifies shortest-mode buffer writes, the MAX_SIG_DIGITS returned-slice bound, round_up, and initialized output.
dragon::format_exact	Verifies exact/fixed output initialization and write bounds over representative bounded buffers while abstracting Big integer arithmetic.

Verification Approach

For the formatter layer in mod.rs, the digit-generation callback is modeled by small symbolic functions that return initialized digit prefixes. This is valid because the to_* functions are generic over the digit-generation strategy: their safety depends on the callback contract that it returns an initialized slice from the provided scratch buffer. Dragon and Grisu are verified separately against that same contract.

For Grisu, the expensive scaling and arithmetic portions are abstracted where they are not needed for memory safety. The stubs preserve the bounds used by the real algorithm, such as cached-power exponent ranges, power-of-ten bounds, digit values in 0..10, and maximum digit counts. The real buffer writes, loop structure, prefix initialization checks, and unsafe conversions remain visible to Kani.

For Dragon, Big integer operations are stubbed because proving Big32x40 arithmetic is orthogonal to this challenge and causes the normal proof to time out. The stubs over-approximate control flow through nondeterministic comparisons, zero checks, and digit extraction, while preserving the safety-relevant fact that extracted digits are decimal digits. This lets Kani check the actual buffer writes and returned slices without requiring a full numerical proof.

The Grisu shortest rounding helper is given a Kani contract and verified with #[kani::proof_for_contract]; format_shortest_opt then uses #[kani::stub_verified]. The Kani-only version returns a boolean acceptance result rather than a borrowed slice because Kani cannot conveniently synthesize arbitrary verified-stub results containing borrowed slice lifetimes. The caller still owns and returns the already-initialized digit slice.

Verification Tradeoffs

Running the full algorithms without abstraction inlines cached-power selection, DiyFp multiplication, Big integer arithmetic, and nested digit loops. That path does not finish in a practical CI budget.

The proof cuts are limited to arithmetic facts that are not safety-critical:

• shortest-mode digit count is bounded by MAX_SIG_DIGITS;
• Grisu exact mode can generate at most 10 integral digits plus 18 fractional digits, with one possible carry byte;
• cached powers satisfy the exponent and normalization bounds expected by Grisu;
• digit-extraction helpers return one decimal digit.

These assumptions do not initialize buffers or skip unsafe call sites. The initialized-prefix assertions read the prefix before each assume_init_*; if a path exposes an unwritten byte, Kani fails.

Scope Assumptions

• This PR proves memory safety and absence of the challenge-listed UB.
• Generic formatter proofs are limited to primitive float types, as allowed by the challenge.
• Kani-only abstractions are behind #[cfg(kani)] and do not affect normal library behavior.

Notes

• The fallback wrappers in Grisu are verified separately from the optimized and Dragon implementations so the lifetime-laundering pattern is checked directly.
• Conventional stubs are used only where the real computation is safe Rust arithmetic or already outside the unsafe boundary being proved.
• The formatter harnesses use symbolic inputs for signs, precision, exponent bounds, and non-finite/finite classes to avoid only testing happy paths.

Verification

All added Challenge 28 harnesses pass locally with Kani.

Resolves #524

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.