Add Kani proof harnesses establishing the memory safety of all 12
  safe-functions-with-unsafe-bodies in core::num::flt2dec: the 6 formatting
  entry points (flt2dec/mod.rs) and the 6 Grisu/Dragon strategy functions
  (flt2dec/strategy/{grisu,dragon}.rs).

  Each unsafe block (MaybeUninit::assume_init_* and slice indexing) is proven
  to touch only initialized, in-bounds memory. The bignum/Fp arithmetic is
  abstracted via sound stubbing -- buffer safety is independent of the numeric
  values, and value inspection (cmp/is_zero) is made nondeterministic so all
  control-flow paths are explored.

  The shortest-mode functions (grisu::format_shortest_opt,
  dragon::format_shortest)
  have an implicit loop bound; their digit index is bounded by the Grisu/Loitsch
  digit-count theorem (a 53-bit-precision f64 has <= MAX_SIG_DIGITS = 17
  significant decimal digits), cited as a cfg(kani) assume because CBMC cannot
  derive it from the unwound arithmetic. The harnesses use the tight decode()
  precondition (the functions are internal and only ever receive a decode()
  result for a real f64), which is what makes that assume sound.

  All added annotations are cfg(kani) verification-only and compile out of normal
  builds. Harnesses require -C debug-assertions=off.

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

…ition-2 OOM)

  - Remove concrete dragon::check_format_exact: full unstubbed bignum (unwind 50)
    exhausted CBMC memory in the verify-std partition (ran ~6h, cancelled).
    format_exact buffer safety is already proven by check_format_exact_stub.
  - Run autoharness with debug-assertions off: the flt2dec harnesses stub the
    bignum/Fp arithmetic, making std debug_assert! digit-correctness checks
    (d<10, mant<scale) unprovable. Those are not memory-safety properties and are
    already dead in the verify-std job (--prove-safety-only). Keeps the two jobs
    consistent; monotonic (only removes checks).

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>

…ition-2 OOM)

  - Remove concrete dragon::check_format_exact: full unstubbed bignum (unwind 50)
    exhausted CBMC memory in the verify-std partition (ran ~6h, cancelled).
    format_exact buffer safety is already proven by check_format_exact_stub.
  - Run autoharness with debug-assertions off: the flt2dec harnesses stub the
    bignum/Fp arithmetic, making std debug_assert! digit-correctness checks
    (d<10, mant<scale) unprovable. Those are not memory-safety properties and are
    already dead in the verify-std job (--prove-safety-only). Keeps the two jobs
    consistent; monotonic (only removes checks).

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>