You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Challenge 28: Safety of float to decimal conversion module #524
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).
Activity
MavenRain commentedon Jun 15, 2026
I'd like to claim challenge #28 (
core::num::flt2dec). PR:It adds Kani harnesses for all 12 target functions (the 6
flt2dec/mod.rsentry points and the 6 Grisu/Dragon strategy functions), proving eachassume_init/indexing unsafe block touches only initialized, in-bounds memory. Bignum/Fparithmetic is abstracted via sound stubbing; the two shortest-mode functions' loop bounds are discharged by citing the Grisu/Loitsch <=17-digit theorem as anassumeunder the exactdecode()precondition (details and caveats in the PR).