Add bounded memory-safety harnesses for core::num::flt2dec (challenge #28)

[MavenRain]

The wrapper harnesses did not establish safety of Grisu's digit generators, and Dragon needed direct generator proofs. This revision adds those harnesses with symbolic buffer lengths, removes digit-index assumptions and forced termination models, and restores Dragon's production digit extraction. Grisu's existing rounding helpers move to module scope with unchanged signatures and bodies so they can be proved separately. Both Grisu generators now return their rounding state to one final call per mode; their generator statements, stopping conditions, and rounding arguments are preserved.

Verification remains incomplete. Revision ee24d41d retains full positive finite-float coverage. All six helper contracts and the comparison and bit-scan equivalence proofs passed on df8bbbbd; all 65 estimator equivalence cases passed on c108d774. Grisu exact passed every positive finite f32 input on 49acde40, including subnormals, with symbolic buffer lengths and limits. Full f64 verification and the other generator families remain unfinished. Current CI uses 57 batches. Current CI, full f32 Grisu exact result.

Functions	Harness scope
Six string-assembly functions in flt2dec/mod.rs	Existing bounded harnesses check their own bodies with symbolic formatting inputs.
grisu::format_shortest, grisu::format_exact	Wrapper harnesses check the slice reborrow, with their callees modeled as opaque.
grisu::format_shortest_opt, grisu::format_exact_opt	Real generator bodies, with symbolic buffer lengths 17 through 32 and 1 through 32 respectively.
dragon::format_shortest, dragon::format_exact	Real generator bodies, with symbolic buffer lengths 17 through 32 and 0 through 32 respectively.

Each generator has four f32 groups and 32 f64 groups. Their union covers every positive finite nonzero input bit pattern through the real decoder, including subnormals. Each group keeps six exponent bits and all significand bits symbolic. Exact-mode limits remain arbitrary i16 values. The harnesses check output bounds and buffer identity, retain real digit writes and uninitialized-memory checks, and include boundary and multi-digit covers. All generator loops remain in the real code.

Four additional f64 probes cover [1, 2) with all 52 significand bits symbolic and the same buffer bounds and checks. They diagnose verification cost without replacing any full-domain harness. The two Dragon probes now check the actual estimator arguments against the proved model, assert that the result is zero, and return a literal zero to simplify symbolic expansion. An incorrect estimate fails that assertion. These revised probes are pending. Full verification requires all 144 generator harnesses, six contracts, the comparison and bit-scan equivalence proofs, and all 65 estimator equivalence cases.

The compositional proofs cover these dependencies:

• Bigint comparisons: constant-index models preserve exact Big::cmp and Big::is_zero results. An independent proof covers every size 0 through 40 and arbitrary limb contents, including inactive limbs. The adapters assert the same size bounds. No comparison or termination decision is arbitrary. Passing equivalence proof.
• Bit scans: fixed shifts and comparisons model u32::leading_zeros and u64::leading_zeros. Their separate CI proof compares the models against the real methods for every input, including zero. All 29 checks and six boundary covers passed in 0.36 seconds. The models add no input assumptions. Passing proof.
• Exponent estimation: the model evaluates the original arithmetic at each bit-count leaf, exposing equal decimal exponents to simplification before Dragon's bigint scaling. Every call asserts a nonzero mantissa. Its independent checks partition mantissa - 1 into all 65 possible bit lengths. Their union covers every nonzero u64 mantissa, with every i16 exponent retained. All 65 cases passed with all 133 intended boundary covers reachable. No float-generator input group changed. Equivalence results.
• Power-of-ten expansion: a Kani-only identity call exposes exponent bits common to each existing Dragon input partition before executing the original multiplication body. Each replacement asserts that its encoded exponent equals the actual call argument. An incorrect encoding fails verification. The full generator proofs must discharge these new checks; their inputs, buffer bounds, and loop checks are unchanged. These results are pending.
• Grisu exact rounding: the numeric contract executes real possibly_round with every permitted input prefix and uninitialized padding. It checks buffer identity and every returned byte, and bounds growth by one byte and available capacity. The adapter asserts the byte predicate on the actual caller buffer before invoking the contract. The independent proof composes round_up and passed with zero failures among 1,695 checks, five of six covers satisfied, and one duplicate cover unreachable. Passing proof.
• Grisu shortest rounding: the scalar contract takes the final digit and numeric state, quantifies the other permitted prefix bytes inside its proof, and executes real round_and_weed with uninitialized padding. The adapter checks every actual prefix byte before invoking it. The precondition retains arithmetic ranges and the stopping condition before decrementing to zero, encoded by up to eight saturating additions. Every generator call must establish it. The revised proof checks length, exponent, buffer identity, and initialization, with zero failures among 1,226 checks and five of seven covers satisfied in 159.03 seconds. Two covers were unreachable. Passing proof.
• Carry rounding: round_up preserves the carry result while overapproximating output bytes within the initialized prefix. Passing proof.
• Division: div_2pow10 preserves bigint storage size and unused zero limbs for sizes 0 through 40 and powers 0 through 32. It composes Big::div_rem_small, which checks the real limb loop for every valid storage size and nonzero u32 divisor. That proof composes a scalar FullOps::full_div_rem contract with borrow < divisor and a bounded remainder. Mutable contracts permit writes only to the limb array; Arbitrary is unrestricted and storage validity is an explicit precondition. Power-of-ten proof, limb-loop proof, scalar proof.

Both Grisu rounding contracts have empty write sets. Their adapters overapproximate output byte values only within the proved initialized prefix, leaving unused padding uninitialized. Both proofs quantify prefix bytes internally after their adapters check the actual prefix; shortest rounding additionally preserves the actual final digit as a scalar input.

Grisu exact mode's integral loop takes at most ten iterations. Its fractional loop stops by iteration 18 because err reaches 10^18, exceeding the largest maxerr, 2^59. Exact rounding retains unwind 33; shortest rounding uses unwind nine because its checked precondition permits at most eight decrements. All unwinding assertions remain enabled. There are no index assumptions or forced loop exits.

CI has 57 focused jobs: thirty-six generator batches, six contracts, two simple equivalence proofs, nine estimator-case batches, and four probes. Each uses one Kani worker. Generator batches select at most four harnesses with 60 minutes per proof; equivalence batches select at most eight with 30 minutes per proof. Probes receive 60 minutes and helper contracts retain 30 minutes. Each job therefore has at most four hours of proof budgets, leaving setup and instrumentation time within GitHub's six-hour job limit. The longer generator allowance follows successful full-range Grisu exact proofs taking 27 to 30 minutes and a timeout in f64 group 31. Static checks confirm every required target is selected exactly once and the other existing jobs are unchanged. GitHub Actions limits. Helper/equivalence jobs use 12 object bits; generators and probes use 14. Only the probes select CBMC's pointer-read caching and whole-array encoding options. No verification checks are disabled.

With one shared exact-rounding call, the [1, 2) Grisu exact probe passed with zero failures among 1,168 checks and four of five covers satisfied in 1,647.77 seconds. One cover was unreachable. This result covers the real generator, symbolic buffer lengths, and arbitrary formatting limits within that probe's numeric range. Passing generator probe. The shared-call shortest probe completed symbolic expansion but hit the 30-minute solver timeout. The revised scalar summary is intended to reduce its remaining cost. Dragon and full-domain generator verification are still incomplete. Shortest timeout.

Formatting, whitespace, and complete CI-selection checks passed locally. Static comparisons confirmed both moved rounding helpers are unchanged and both generator extractions preserve their public signatures, statements, conditions, and all rounding arguments. The shortest extraction also preserves where the initialized slice is constructed and the argument evaluation order. These are static preservation checks, not formal equivalence proofs. No local Kani proof or Rust build ran. The upstream Rust Tests and SIMD-model workflows passed on 0bbe5517; current-revision validation remains required. Upstream tests, SIMD-model tests. The PR also fixes serial proof-log parsing and trusts the existing CBMC Homebrew tap in macOS setup.

[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.

[MavenRain]

@tautschnig when you or another committee member have review bandwidth, would you
be able to take a first look at three challenge solutions I have open? All
three are complete and CI-green:

• Add bounded memory-safety harnesses for core::num::flt2dec (challenge #28) #601: challenge Add new templates for issues #28 (core::num::flt2dec), 12 target functions
• Verify iter adapter unsafe methods + safe abstractions (challenge #16) #602: challenge Challenge 2: Verify the memory safery of core intrinsics using raw pointers #16 (core::iter adapters)
• Verify the safety of slice functions (challenge #17) #603: challenge Add runtime implementation of requires and ensures #17 (slice), 37 functions

Each passes the required CI checks (the Kani verify-std suite across partitions,
autoharness on macOS and Ubuntu, the Kani metrics / list / analyzer jobs,
upstream_test, goto-transcoder, and Flux) and has no conflicts with main, with the
honest coverage caveats written into each PR description. Since a merge needs
approvals from two committee members, they are really just waiting on a first
reviewer. No urgency at all; I mostly want to make sure they are on the radar
rather than lost in the queue. I'd be happy to address any feedback whenever you get to
them. Thank you.

[feliperodri]

Verdict: REQUEST_CHANGES

The PR is not vacuous in the cfg-swap sense (0 cfg(not(kani)), confirmed), and several harnesses are genuinely sound. But it has two blocking soundness/coverage defects that mirror the exact failure modes flagged in the competing PRs #596 and #606.

Proof inventory (10 proofs, 12 required functions)

Required function	Proof	Status
digits_to_dec_str (mod)	check_digits_to_dec_str	sound (bounded)
digits_to_exp_str (mod)	check_digits_to_exp_str	sound (bounded)
to_shortest_str (mod)	check_to_shortest_str	sound
to_shortest_exp_str (mod)	check_to_shortest_exp_str	sound
to_exact_exp_str (mod)	check_to_exact_exp_str	sound
to_exact_fixed_str (mod)	check_to_exact_fixed_str	sound
grisu::format_shortest	check_format_shortest	wrapper only (OK)
grisu::format_exact	check_format_exact	wrapper only (OK)
grisu::format_shortest_opt	—	NOT VERIFIED
grisu::format_exact_opt	—	NOT VERIFIED
dragon::format_shortest	check_format_shortest_stub	assume-the-conclusion
dragon::format_exact	check_format_exact_stub	sound

BLOCKER 1 — Two required functions are never verified (same as #606, doubled)

grisu::format_shortest_opt and grisu::format_exact_opt are on the challenge's required list, and the challenge states each "should be proven unconditionally safe, or safety contracts should be added." They get neither.

• check_format_shortest stubs the real body out: #[kani::stub(format_shortest_opt, stub_format_shortest_opt)] (grisu.rs, grisu_verify), where stub_format_shortest_opt just writes one arbitrary digit.
• check_format_exact does the same: #[kani::stub(format_exact_opt, stub_format_exact_opt)].
• No other harness targets either function.

These *_opt functions ARE the hard Grisu digit-generation code — the loops at grisu.rs:271 and grisu.rs:323 that this very PR modified with #[cfg(kani)] assume(i < MAX_SIG_DIGITS). Because the functions are stubbed everywhere, those added assumes are dead code — they never execute under any proof, and the loops that write digits into the scratch buffer are never model-checked. This is precisely the "compiling out format_exact_opt" defect that sank #606, here applied to both *_opt functions.

Direction: add harnesses that call format_shortest_opt / format_exact_opt directly (unstubbed), or add safety contracts on them. The lifetime-laundering wrappers being green does not cover the digit-emission unsafe inside the _opt bodies.

BLOCKER 2 — dragon::format_shortest: assume-the-conclusion + forced termination (same as #596/#606)

In check_format_shortest_stub the target is dragon::format_shortest, which the diff modified to add, at the top of the digit loop and again before the round-up carry write:

#[cfg(kani)]
crate::kani::assume(i < MAX_SIG_DIGITS);
buf[i] = MaybeUninit::new(b'0' + d);   // dragon.rs ~209 and ~266

The function asserts buf.len() >= MAX_SIG_DIGITS (dragon.rs:123) and the proof supplies buf: [MaybeUninit<u8>; MAX_SIG_DIGITS]. So assume(i < MAX_SIG_DIGITS) is identically assume(i < buf.len()) — the exact memory-safety obligation for buf[i] = ..., asserted immediately before the write. That is textbook assume-the-conclusion on an internal loop variable (not an input precondition).

It is compounded by forced termination: the proof havoc-stubs every bignum op including the comparison that drives the loop break (s_cmp → nondeterministic Ordering, s_is_zero → any()). With real termination destroyed, nothing constrains i except the assume itself; under #[kani::unwind(19)] the loop would otherwise write buf[18] into a 17-element buffer, and the assume(i < 17) is exactly what prevents it. This is the same mechanism as #596's CMP_BUDGET early-exit stub. The digit loop's buffer safety is therefore verified by assuming buffer safety — it proves nothing and would not catch a real off-by-one in the digit count.

The author's framing ("bounds the DIGIT COUNT, an input-precision property; safety follows from the separate assert!") is the sophisticated form of the antipattern: the digit-count theorem is assumed, not proven, on an internal index, while all arithmetic that could constrain that index is havoced. Contrast with dragon::format_exact (check_format_exact_stub), which is sound precisely because its bound is structural — for i in 0..len with len clamped to buf.len(), so no digit-count assume is needed. format_shortest needs a real argument (loop contract, or not stubbing the comparison, or a proven bound), not assume(i < buf.len()).

Non-blocking issues

• std runtime-logic change. dragon::format_exact was refactored from the inline 8-4-2-1 subtraction block to a call to div_rem_upto_16(...) (dragon.rs:361). It is behavior-preserving (the helper already exists at dragon.rs:73 and format_shortest already used it), but CLAUDE.md/general-rules forbid changing std runtime logic — verification code should be additive/gated. Prefer verifying the original body or making the extraction upstream-first.
• Bounded buffer length. mod.rs check_digits_to_dec_str/check_digits_to_exp_str fix PROOF_BUFLEN = 4 (symbolic content, fixed length). The to_exact_* proofs justify PROOF_EXACT_BUFLEN = 1024 well via estimate_max_buf_len ≤ 828; the digits_to_* fixed length is asserted to lose no path coverage but is not as rigorously argued. Minor.
• 0 contracts (T7). No contracts are added anywhere; harness-local precondition assumes are used instead. Fine for the sound harnesses, but it means the two missing _opt functions have no fallback contract either.

Creditable, sound work

The six mod.rs proofs verify the string-assembly functions with symbolic content and full-range exp/frac_digits; the two Grisu wrapper proofs correctly isolate the lifetime-laundering reborrow by modelling both callees as opaque; dragon::format_exact is soundly verified with structural bounds and a value-contract stub for div_rem_upto_16. The recursion_limit bump and bignum::kani_any over-approximating constructor are benign.

Required before approval: (1) genuinely verify grisu::format_shortest_opt and grisu::format_exact_opt (or add contracts); (2) remove the assume(i < MAX_SIG_DIGITS) assume-the-conclusion in dragon::format_shortest and establish the digit-loop bound without assuming the buffer index; (3) revert or upstream the format_exact body refactor.

[MavenRain]

Thanks for the careful review, @feliperodri. Both blockers were correct. This push removes every in-body assume and every dragon stub, restores the upstream format_exact body, and replaces the strategy-level harnesses. It also documents, with numbers, what a direct proof of the two grisu _opt functions runs into, because that is the one item I could not close in the way you asked, and I would rather show the wall than paper over it.

Shape of the PR now. git diff main is exactly two files, +347/-0: an appended #[cfg(kani)] pub mod *_verify block in flt2dec/mod.rs and in strategy/grisu.rs. strategy/dragon.rs, lib.rs and bignum.rs are byte-identical to main again (the recursion_limit bump, bignum::kani_any, every in-body #[cfg(kani)] assume, the whole stub-based dragon module, and the div_rem_upto_16 refactor are gone).

(2) dragon::format_shortest: the assume(i < MAX_SIG_DIGITS) is gone, and so is the stub-based module around it. I tried to replace it with the real thing: format_shortest / format_exact with every Big32x40 operation unstubbed, inputs = the exact decode() image, d.exp bounded to [-8, 8] so the operands stay a few limbs long, headroom or minimum buffers, unwind(41) and then unwind(20). Nothing converges: format_exact (17-byte) times out at 45 min (unwind 41) and 40 min (unwind 20), and even format_exact with a 1-byte buffer times out at 25 min. The digit loop is the cheap part; the cost is the scaling prelude (mul_pow10 under a symbolic k keeps every POW5TO* branch live) plus the value-dependent debug_assert!(mant < scale) / debug_assert!(d < 10), which with debug assertions live make the proof a numerical-correctness obligation on estimate_scaling_factor and the bignum products. The digit-loop bound itself is real (minus grows x10 per iteration against a fixed scale with scale / minus < 2^54 + 2 < 10^17, so the down break fires within 18 digits), but I do not have a proof artifact for it, and I would rather ship no dragon harness than a stubbed one whose termination rests on an assume. Loop contracts on the digit loop are the route I see; see (1) below.

(3) format_exact body refactor: reverted. dragon::format_exact is upstream's inline 8-4-2-1 block again and dragon.rs carries no PR changes at all.

(1) grisu::format_shortest_opt / format_exact_opt: partially, and here is exactly where it stops.

• format_exact_opt is now called directly, unstubbed, over its full documented precondition (0 < mant < 2^61, exp in the decoder range, arbitrary limit) with a 1-byte buffer: check_format_exact_opt_buf1, 0 of 488 checks failed, ~12 s. It exercises the len clamp, the exp <= limit early path (possibly_round with len == 0), the first digit of both digit loops, and the real cached_power / Fp::mul / possibly_round arithmetic (the value-dependent debug_assert!s are discharged from real values). With any longer buffer len is symbolic, every unrolled digit iteration stays live with its own possibly_round instance, and CBMC stops with too many addressed objects ... 2^12 under the repository's --object-bits 12 (17-byte/unwind-20: 13.1M SSA steps; 8-byte/unwind-9: still over the cap; 1-byte: 63k steps).
• format_shortest_opt: a direct, unstubbed harness over the exact decode() image (even mant in [2, 2^54], plus == 2 only at the minimum normal value, exp in [-1076, 970]; the exact image matters, an arbitrary plus == 2 trips round_and_weed's debug_assert!(*last > b'0')) produces a 4.7M-step program with ~120k verification conditions at unwind(20); cadical times out at 30 min, kissat at 45 min, and restricting exp to a window that pins cached_power to one table entry does not shrink the formula at all (same 4.7M steps, then out of memory during bit-blasting). The digit loops are bounded only by the arithmetic (up to 17 digits), round_and_weed is a nested function so it cannot be stubbed or contracted separately, and with debug_assert! live its *last > b'0' makes the proof a numerical-correctness obligation over the three 64x64-bit Fp products. So the reachable options are (a) loop contracts on the two digit loops (invariants inside the upstream body, #[cfg_attr(kani, kani::loop_invariant(...))]), or (b) hoisting round_and_weed out of the body so it can carry a contract and be verified on its own; both touch upstream code, so I would like your steer before doing either. Until then format_shortest_opt is covered only through the wrapper proof (check_format_shortest, both callees opaque), which I know is not what the challenge asks for.

Non-blocking items.

• PROOF_BUFLEN: the digits_to_dec_str / digits_to_exp_str harnesses now use a symbolic length in 1..=4 (any_digits). Every length-dependent branch in those two functions compares against a small value (buf.len() == 1, exp < buf.len(), frac_digits > buf.len() - exp), so the range reaches every branch, including the buf.len() == 1 path of digits_to_exp_str that a fixed length of 4 could not reach. A longer buffer only lengthens a Part::Copy slice. (0/146 and 0/120 checks.)
• The wrapper stubs' None arms now dirty buf[0] before returning, so the wrapper's reuse of buf on the None path is exercised against a modified buffer.
• Contracts: still none; every harness uses harness-local preconditions.

Local results (model-checking/kani @ 415ca503, the pinned commit, verify-std with debug assertions live, one harness at a time):

• flt2dec_verify (mod.rs): check_to_exact_fixed_str 0/307, check_to_exact_exp_str 0/225, check_to_shortest_exp_str 0/292, check_to_shortest_str 0/228, check_digits_to_exp_str 0/120, check_digits_to_dec_str 0/146 (all in one 45 s invocation)
• grisu_verify: check_format_shortest 0/61, check_format_exact 0/52, check_format_exact_opt_buf1 0/488 (15 unreachable) (one 46 s invocation)
• Attempted and NOT shipped (log kept locally): grisu format_shortest_opt direct (32-byte, exact decode() image): cadical timeout 30 min, kissat timeout 45 min, exp-window variants same 4.7M-step formula then out of memory; grisu format_exact_opt with 17-byte or 8-byte buffer: CBMC "too many addressed objects" under --object-bits 12; dragon format_exact 17-byte: timeout 45 min (unwind 41) and 40 min (unwind 20); dragon format_exact 1-byte: timeout 25 min; dragon format_shortest 24-byte: no verdict within budget.

[feliperodri]

Thanks @MavenRain. Reviewed Challenge 28 with our vacuity tooling. Sound (no cfg body swaps, no T7, no assume-the-conclusion), but doesn't meet criteria:

1. Coverage: 7/12 effective, not 12/12 as claimed. dragon.rs is not modified — dragon::format_shortest and dragon::format_exact have NO harness. grisu::format_shortest_opt isn't directly proved (PR body: "covered here through the wrapper proofs below (both callees modelled as opaque)"). check_format_exact_opt_buf1 uses buf length 1 concretely, pruning most digit-loop paths.
2. PR body discrepancy: mentions kani::assume(i < MAX_SIG_DIGITS), but no such assume exists in the diff.
3. No contracts (0 requires/ensures), no proof_for_contract.

Between the three open Challenge 28 solutions we're prioritizing #596 (12/12, sound). This needs actual harnesses for dragon (2 fns) and format_shortest_opt with symbolic buf length.