Challenge 28: Safety of float to decimal conversion module

[AlexLB99]

#523

Runbook Link

Will add once runbook link is up

[MavenRain]

I'd like to claim challenge #28 (core::num::flt2dec). PR:

It adds Kani harnesses for all 12 target functions (the 6 flt2dec/mod.rs entry points and the 6 Grisu/Dragon strategy functions), proving each assume_init/indexing unsafe block touches only initialized, in-bounds memory. Bignum/Fp arithmetic is abstracted via sound stubbing; the two shortest-mode functions' loop bounds are discharged by citing the Grisu/Loitsch <=17-digit theorem as an assume under the exact decode() precondition (details and caveats in the PR).