Verify core::num::flt2dec memory safety (challenge #28)

[MavenRain]

Towards #524 (challenge #28: core::num::flt2dec).

What this proves

Kani harnesses for all 12 target functions, proving each unsafe block touches
only initialized, in-bounds memory:

• flt2dec/mod.rs: digits_to_dec_str, digits_to_exp_str,
  to_shortest_str,
  to_shortest_exp_str, to_exact_exp_str, to_exact_fixed_str
• strategy/grisu.rs: format_exact_opt, format_shortest_opt,
  format_exact,
  format_shortest
• strategy/dragon.rs: format_exact, format_shortest

Approach

• The buffer-safety obligation (assume_init over written cells, buf[i]
  in-bounds) is independent of the bignum/Fp values, so the arithmetic is
  abstracted by sound stubs; cmp/is_zero are nondeterministic so every
  control-flow path is explored. The format_exact/format_shortest wrappers
  are proven by stubbing their callees, which are themselves verified.
• The shortest-mode loops have no explicit index guard; they terminate within
  MAX_SIG_DIGITS by the Grisu/Loitsch digit-count theorem (Loitsch, PLDI'10;
  Errol, POPL'16, Thm 5). CBMC cannot derive this number-theoretic bound, so it
  is cited as a cfg(kani) assume(i < MAX_SIG_DIGITS). The harnesses
  constrain
  inputs to the exact decode() image (minus == 1, plus ∈ {1,2},
  mant ≤ 2^54), which is the functions' true precondition (they are internal,
  only reached via decode() on a real f64) and is what makes the assume
  sound.

Caveats for review (transparency)

• The two shortest-mode proofs are conditional on the cited digit-count
  theorem; the rest is unconditional. The assume bounds the digit count
  (an input-precision property); buffer safety follows via the separate
  assert!(buf.len() >= MAX_SIG_DIGITS). Happy to strengthen this (e.g. tie the
  bound to the concrete max_kappa) or to discuss proving the theorem if
  preferred.
• grisu::format_shortest_opt additionally assumes Fp::mul's documented output
  invariants (ordering minus ≤ v ≤ plus, normalized-mantissa bounds) that the
  cost-reducing stub would otherwise havoc.
• Harnesses require -C debug-assertions=off (the debug_assert!s are
  digit-correctness, not memory safety). Please advise on the preferred CI
  wiring.

[MavenRain]

Quick status update for reviewers: this PR is now fully green on every check
(Kani verify-std partitions 1 to 4, autoharness on both macOS and Ubuntu, Kani
Metrics / List / Analyzer, upstream_test, VeriFast, goto-transcoder, Flux, and
Build Book), and it is mergeable against current main.

One item from the original description is now resolved. The "Caveats for review"
note asking how to wire -C debug-assertions=off into CI no longer applies.
The harnesses were reworked (commit c02f4fd) to discharge the value-dependent
debug_assert!s by stubbing div_rem_upto_16 to its value contract (it returns
a digit below 10 with the remainder havoced), so they now pass under both
autoharness (debug-assertions ON) and verify-std (debug-assertions off) with no
special CI flags. There is nothing left to wire up on that front.

The challenge is otherwise uncontested and all 12 target functions are proven.
Happy to address any review feedback, including the strengthening I offered for
the digit-count assume (tying it to the concrete max_kappa rather than to
MAX_SIG_DIGITS) if that form is preferred. Thanks for taking a look whenever
you have a chance.