Verify core::num::flt2dec memory safety (challenge #28)#601
Open
MavenRain wants to merge 2 commits into
Open
Conversation
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>
a7ae3ea to
e4e3297
Compare
…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>
98db9cd to
e104d40
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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_strstrategy/grisu.rs:format_exact_opt,format_shortest_opt,format_exact,format_shorteststrategy/dragon.rs:format_exact,format_shortestApproach
assume_initover written cells,buf[i]in-bounds) is independent of the bignum/
Fpvalues, so the arithmetic isabstracted by sound stubs;
cmp/is_zeroare nondeterministic so everycontrol-flow path is explored. The
format_exact/format_shortestwrappersare proven by stubbing their callees, which are themselves verified.
MAX_SIG_DIGITSby 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 harnessesconstrain
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 realf64) and is what makes the assumesound.
Caveats for review (transparency)
theorem; the rest is unconditional. The
assumebounds 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 thebound to the concrete
max_kappa) or to discuss proving the theorem ifpreferred.
grisu::format_shortest_optadditionally assumesFp::mul's documented outputinvariants (ordering
minus ≤ v ≤ plus, normalized-mantissa bounds) that thecost-reducing stub would otherwise havoc.
-C debug-assertions=off(thedebug_assert!s aredigit-correctness, not memory safety). Please advise on the preferred CI
wiring.