Challenge 28 (flt2dec): 12 of 12 functions verified via Kani

[gui-wf]

Challenge 28 (flt2dec): 12 of 12 functions verified via Kani

Opening as draft to invite collaborative review on two deviations from the established verify-rust-std pattern (called out under "Design decisions reviewers may question" below). All 12 functions verify end-to-end under Kani 0.65; the deviations are about how the proofs are structured, not whether they pass.

The PR adds Kani harnesses under library/core/src/num/flt2dec/** and two #[cfg(kani)]-only helpers under library/core/src/num/bignum.rs. No production runtime logic changes apart from one small refactor in dragon::format_exact that consolidates a byte-identical inlined block into a call to the existing div_rem_upto_16 helper.

What's verified

flt2dec (module root):

• digits_to_dec_str, digits_to_exp_str
• to_shortest_str, to_shortest_exp_str, to_exact_exp_str, to_exact_fixed_str (monomorphised to f32, per the spec's "primitive types only" clause for generic T).

flt2dec::strategy::grisu:

• format_shortest_opt, format_exact_opt
• format_shortest, format_exact (the lifetime-laundering wrappers).

flt2dec::strategy::dragon:

• format_shortest, format_exact.

Verification approach

• Public helpers and the four to_*_str functions. Direct Kani proofs over symbolic Decoded and digit-buffer inputs. No stubs; the CBMC formula is small enough that the harnesses finish in ~2 seconds combined.
• grisu::format_shortest_opt / format_exact_opt. Stubs derived from the Loitsch PLDI 2010 paper: Fp::mul as identity on the mantissa (preserves the algorithm's required monotonic ordering of three successive multiplications), cached_power and max_pow10_no_more_than as range-bounded havoc. round_and_weed is hoisted to a free function so it can be reasoned about separately.
• grisu::format_shortest / format_exact wrappers. Hand-written buf-synthesizing stubs for the inner _opt call and the dragon fallback. Only the wrapper's own unsafe reborrow is exercised; this is the actual unsafe surface the wrappers add over their callees.
• dragon::format_shortest / format_exact. Three levers: (1) tightened the symbolic Decoded input to match decode_finite's real output shape (minus = 1, plus in {1, 2}); (2) stubbed div_rem_upto_16 to return (d, x) with kani::assume(d < 10), encoding the helper's algorithmic invariant mant + plus <= scale * 10 => d < 10 (Burger and Dybvig, 1996) directly; (3) bounded the digit-generation loop via a CMP_CALLS static counter on the Big::cmp stub. A small refactor in format_exact consolidates a byte-identical inlined digit-extraction block into a call to the existing div_rem_upto_16 helper, so both dragon entry points share the same stubbed extraction routine. Both proofs combined finish in under 11 seconds.

Design decisions

These two are off-pattern compared to merged work in this repo (a precedent survey of merged PRs found zero prior use of doc-comment safety contracts, and zero kani::stub plus kani::assume-postcondition stubs - only stub_verified plus proven #[ensures], per the transmute_unchecked_wrapper family in library/core/src/intrinsics/mod.rs). Each is explained below with the reasoning; happy to iterate on either.

• Doc-comment # Safety contract sections instead of #[safety::requires]. Blocked by Kani upstream issue model-checking/kani#4591 (open, assigned, milestone Contracts): Kani 0.65 cannot apply #[kani::stub] to a function that carries #[requires], with a "Failed to find contract closure" compile error. All four contracted functions (format_shortest_opt, format_exact_opt, dragon::format_shortest, dragon::format_exact) are stubbed by at least one other harness in this PR, so the two attributes cannot coexist. Reproduced locally: dropping the doc block and adding #[safety::requires(d.mant > 0)] etc. to format_exact_opt fails to compile the core crate. Preconditions remain enforced at runtime via assert! in the function body, and the strategy harnesses encode them via kani::assume. When Rewrite the coercion code to be more readable, more sound, and to reborrow when needed. rust-lang/rust#4591 lands, the migration is mechanical: drop the doc block, drop the body assert!s, add the attributes. Each of the four contract blocks references the upstream issue in-line.
• stub_div_rem_upto_16 encoding d < 10 as kani::assume. Sound for the Challenge 28 safety mandate (no UB on the MaybeUninit buffer): the assumed postcondition matches the helper's actual algorithmic invariant mant + plus <= scale * 10 => d < 10, proved by Burger and Dybvig (1996). The canonical alternative would be #[kani::stub_verified] with a proven #[ensures] (the transmute_unchecked_wrapper pattern). Deriving d < 10 automatically through that path requires per-method #[ensures] on the entire Big32x40 API plus a separately tractable proof for each; the kani_havoc / kani_size helpers added in bignum.rs are designed to support that follow-up. The current stub is the smallest change that closes the dragon harnesses; happy to invest in stub_verified if reviewers prefer it as a follow-up before merge.
• CMP_CALLS static counter on stub_big_cmp. Bounds the digit-generation loop to fewer than MAX_SIG_DIGITS = 17 iterations. The unbounded path admitted by raw havoc is a stub artefact - the real algorithm terminates monotonically as mant.mul_small(10) drives the comparison - not a real algorithmic behaviour. Sound for safety, restricted in coverage. Counter is reset on each harness entry.
• Production-code changes. Three, all conservative:
  • #[cfg_attr(kani, recursion_limit = "256")] in library/core/src/lib.rs - the per-harness stack of #[kani::stub] attributes exceeded the default macro-expansion limit. cfg(kani)-gated, zero impact on production builds.
  • kani_havoc / kani_size helpers in library/core/src/num/bignum.rs - #[cfg(kani)]-gated.
  • One small refactor in dragon::format_exact: an inlined digit-extraction block that was byte-identical to the existing div_rem_upto_16 helper is now a call to that helper. The two blocks were copy-paste duplicates; consolidating them deduplicates code regardless of verification, and incidentally lets the Kani harness stub one extraction routine for both format_shortest and format_exact. No behavioural change in any build mode.

Test plan

Reproduce from the repo root after building Kani per scripts/setup/install_deps.sh:

• scripts/run-kani.sh (runs every harness in the workspace; the new flt2dec harnesses are:)
  • num::flt2dec::verify::check_digits_to_dec_str, check_digits_to_exp_str
  • num::flt2dec::verify::check_to_shortest_str, check_to_shortest_exp_str, check_to_exact_exp_str, check_to_exact_fixed_str
  • num::flt2dec::strategy::grisu::verify::check_format_shortest_opt_safety, check_format_exact_opt_safety
  • num::flt2dec::strategy::grisu::verify::check_format_shortest_wrapper_safety, check_format_exact_wrapper_safety
  • num::flt2dec::strategy::dragon::verify::check_format_shortest_safety, check_format_exact_safety
• All twelve harnesses pass on the upstream Verify std library and Verify std library using autoharness workflows.

References

• Burger and Dybvig, Printing Floating-Point Numbers Quickly and Accurately, PLDI 1996 - the Dragon4 algorithm and the mant + plus <= scale * 10 => d < 10 invariant.
• Loitsch, Printing Floating-Point Numbers Quickly and Accurately with Integers, PLDI 2010 - the Grisu family and the monotonic-ordering property exploited by the identity-on-f Fp::mul stub.
• model-checking/kani#4591 - upstream blocker for #[safety::requires] plus #[kani::stub] coexistence.

[Copilot]

Pull request overview

This PR adds Kani verification coverage for Challenge 28’s flt2dec targets, along with Kani-only helpers and a small Dragon digit-extraction refactor to support the proofs.

Changes:

• Adds Kani harnesses for flt2dec formatting helpers and Grisu/Dragon strategy functions.
• Introduces Kani-only bignum havoc helpers and a Kani-only recursion-limit adjustment.
• Normalizes several script shebangs and adds Nix-related generated artifacts to .gitignore.

Reviewed changes

Copilot reviewed 9 out of 10 changed files in this pull request and generated 8 comments.

Show a summary per file

File	Description
library/core/src/num/flt2dec/mod.rs	Adds wrapper and digit-rendering Kani harnesses.
library/core/src/num/flt2dec/strategy/grisu.rs	Adds Grisu contracts, hoists round_and_weed, and adds Grisu Kani harnesses/stubs.
library/core/src/num/flt2dec/strategy/dragon.rs	Adds Dragon contracts, refactors digit extraction through div_rem_upto_16, and adds Dragon Kani harnesses/stubs.
library/core/src/num/bignum.rs	Adds Kani-only bignum helper methods for verification stubs.
library/core/src/lib.rs	Adds a Kani-only recursion-limit attribute.
scripts/run-kani.sh	Switches shebang to /usr/bin/env bash.
scripts/run-goto-transcoder.sh	Switches shebang to /usr/bin/env bash.
scripts/find-contracts.sh	Switches shebang to /usr/bin/env bash.
scripts/check_rustc.sh	Switches shebang to /usr/bin/env bash.
.gitignore	Ignores Nix/runtime verification artifacts.

[gui-wf]

Bounds documented as a new # Kani verification scope doc-section on format_shortest and format_exact in 5698c1e. Deliberately not a safety contract: the havoc stubs of Big32x40 decouple the proof's safety conclusion (no UB on buf[i] = b'0' + d) from the concrete mantissa/exponent values, so the narrow bounds are a CBMC-tractability choice rather than a precondition the real function imposes on its callers. Treating them as # Safety contract entries would incorrectly imply real callers (which feed decode_finite's full output range) must respect them.

[gui-wf]

Bounds documented as # Kani verification scope on format_shortest_opt in 5698c1e (same framing as the dragon comments - explicitly not a safety contract). stub_fp_mul is an identity on the mantissa, so the safety conclusion is independent of the specific Fp values; the narrow symbolic range is a CBMC-tractability choice rather than a precondition the real function imposes.

[gui-wf]

Bounds documented as # Kani verification scope on format_exact_opt in 5698c1e. Same justification as format_shortest_opt: the identity-on-f stub_fp_mul decouples the safety conclusion from the concrete Fp values, so the narrow symbolic range is a verification-time efficiency choice rather than a precondition.

[Copilot]

Pull request overview

Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.

Suppressed comments (5)

library/core/src/num/flt2dec/strategy/dragon.rs:690

• This mutable-static access also needs a // SAFETY: justification.

        unsafe {

library/core/src/num/flt2dec/mod.rs:843

• This overlooks the conditional DecodableFloat for f16 implementation at library/core/src/num/flt2dec/decoder.rs:48-53. The challenge permits limiting generic T to primitive types, but f16 is also a supported primitive when target_has_reliable_f16; add cfg-gated f16 harnesses for all four generic formatter targets.

    /// Same structure as the `f32` sibling: the wrapper's buffer
    /// precondition is `buf.len() >= MAX_SIG_DIGITS`, independent of float
    /// bitwidth. Only `decode::<f64>` and `min_pos_norm_value::<f64>` differ
    /// at the monomorphised IR; covering both primitives addresses
    /// Challenge 28's "primitive types" generic-T scope.

library/core/src/num/flt2dec/strategy/dragon.rs:550

• Use the repository's // SAFETY: marker for this unsafe access so the justification is recognized consistently.

        // Safety: harness is single-threaded and resets the counter at entry.

library/core/src/num/flt2dec/strategy/dragon.rs:658

• This mutable-static access needs a // SAFETY: comment explaining why concurrent access cannot occur.

This issue also appears on line 690 of the same file.

        unsafe {

library/core/src/num/flt2dec/strategy/grisu.rs:469

• The documented verification range is stale: the harness below assumes limit >= -10 && limit <= 10, not -8..=8. Keep the scope description aligned with the actual proof.

/// The proof in `verify::check_format_exact_opt_safety` exercises this
/// function on the symbolic subdomain `mant in 1..=0xFF`, `exp in -4..=4`,
/// `minus == 1`, `plus == 1`, with `limit in -8..=8`. Same justification
/// as `format_shortest_opt`: the identity-on-`f` `stub_fp_mul` decouples
/// the safety conclusion from concrete `Fp` values.

[feliperodri]

Summary

PR #596 adds harnesses for all 12 Challenge 28 target functions (mapping confirmed below) and passes CI. Triage of the soundness checklist is mixed: the six flt2dec/mod.rs wrapper proofs are genuinely sound and well-constructed, but the six strategy proofs — which cover the hardest unsafe code (the digit-emission loops that actually write the buffer) — depend on stubs that under-approximate the real behavior and so do not establish the very property the challenge is about (assume_init on fully-initialized buffers / lifetime-laundering safety across the real iteration space). Copilot independently flagged the same core issues.

Function coverage (12/12 have a harness)

• mod.rs: digits_to_dec_str, digits_to_exp_str, to_shortest_str (f32/f64), to_shortest_exp_str (f32/f64), to_exact_exp_str (f32/f64), to_exact_fixed_str (f32/f64)
• grisu: format_shortest_opt, format_exact_opt, format_shortest, format_exact
• dragon: format_shortest, format_exact

Checklist triage: 0 #[cfg(not(kani))] body-swaps (clean); 0 #[requires]/#[ensures] attributes — the "safety contracts" are prose doc comments only, so there are no decorative machine-checked contracts and no autoharness dependency (flt2dec is absent from the --include-pattern allowlist in .github/workflows/kani.yml, which is fine because explicit #[kani::proof] harnesses are used). I confirmed the documented preconditions (d.mant > 0, buf.len() >= MAX_SIG_DIGITS, etc.) genuinely exist as assert! in the upstream bodies (dragon.rs format_shortest L17-22; grisu.rs format_shortest_opt L5-11), so assuming them in harnesses is legitimate (checklist item 2 OK).

Strengths (credit)

• The 6 mod.rs wrapper proofs are sound. They run the real digits_to_dec_str/digits_to_exp_str bodies with symbolic buffers and exp/frac_digits, and pass the digit-generation callback as a generic F argument (stub_format_shortest etc.) — this is legitimate because the wrappers are generic over the callback, not a #[kani::stub] swap of real code. touch_parts forces a discriminant + payload read of every returned Part, so an uninitialized MaybeUninit<Part> slot would surface as UB. These are non-vacuous. f64 monomorphizations were added in the follow-up commit, closing the primitive-type coverage gap.
• The grisu wrapper harnesses (check_format_*_wrapper_safety) correctly isolate the unsafe reborrow, stubbing the callees — acceptable modular reasoning provided the callees are separately verified.
• The write-up is unusually transparent about its abstractions.

Blocking concerns

1. (FATAL for dragon proofs) CMP_BUDGET forces early loop termination — the buffer-write safety is never exercised. dragon.rs stub_big_cmp (diff L727-745) increments a static counter and returns Ordering::Less after 12 calls (CMP_BUDGET = 12, L725). At ~2 comparisons per digit iteration this forces the digit-emission loop to stop after ~6 writes, but dragon's real loop can emit up to MAX_SIG_DIGITS == 17 digits. The writes buf[i] = b'0' + d at indices 6..17 — exactly the assume_init/bounds obligation the challenge targets — are never reached. The in-code justification ("the real algorithm terminates at least this quickly, so any safety violation reachable under real semantics is also reachable") is asserted, not proven, and is dubious for shortest mode. This is a classic under-approximation: it can only miss bugs, not find them. Copilot raised this verbatim (dragon.rs:547). This must be replaced with an abstraction that covers comparisons through the full MAX_SIG_DIGITS boundary (e.g. a nondeterministic-but-eventually-terminating model, or #[kani::unwind]-bounded real cmp on abstracted sizes) before the dragon functions can be considered verified.

2. stub_fp_mul deterministic identity + tiny domains under-approximate grisu. grisu.rs stub_fp_mul (diff L1134-1137) models Fp::mul as identity-on-f, and arbitrary_small_decoded restricts mant to 2..=0xF, exp to -2..=2 (L1290-1305). The overflow-sensitive arithmetic in format_shortest_opt/round_and_weed (plus1 - minus1, threshold - plus1w, 2 * ulp) is precisely where real Fp magnitudes matter; a deterministic identity on a 4-bit mantissa never stresses it. Copilot flagged the same narrowness (grisu.rs:989, 998; dragon.rs:611). The author documented these as a "Kani verification scope" note and explicitly declined to broaden them, arguing the stubs decouple safety from values — but that argument is only valid if the stubs over-approximate, and both #1 and #2 do the opposite.

3. Non-kani std runtime code was modified. Two refactors change the shipped std source (not gated by #[cfg(kani)]):

• dragon.rs format_exact: the inlined subtract-ladder was replaced by a call to div_rem_upto_16 (diff L575-605). I confirmed the helper is logically byte-identical, so it is functionally equivalent — but per CLAUDE.md / general-rules.md this repo must not alter std runtime logic; such changes belong upstream in rust-lang/rust first.
• grisu.rs round_and_weed was hoisted from a nested fn to a module-level fn (diff L930-1058), changing structure/visibility of real code purely to enable stubbing.
  Even though both preserve behavior, they should be justified/minimized or split out, and reviewers here are typically strict about touching library/ runtime code.

Non-blocking issues

• bignum.rs kani_havoc (diff L33-47): the size <= ceil(max_bits/digitbits) bound constrains limb count, not bit length, when max_bits isn't limb-aligned (Copilot, bignum.rs:356). Latent only because it is always called with the limb-aligned BIG_MAX_BITS, but the doc comment ("bit length bounded by max_bits") is inaccurate.
• stub_round_up (dragon diff L751-773) hard-codes None for d.len() >= MAX_SIG_DIGITS; this is entangled with the same forced-termination assumption in #1 and should be revisited alongside it.
• The doc comments' "when kani#4591 lands, swap to #[safety::requires]" plan is reasonable, but until then the preconditions are only assumed, not verified as contracts.

Direction

The mod.rs half is essentially done. To close out the strategy half: (a) remove the CMP_BUDGET early-exit and instead bound the loop with #[kani::unwind] over real (size-abstracted) comparisons so all reachable buf[i] writes up to MAX_SIG_DIGITS are checked; (b) make stub_fp_mul/stub_cached_power over-approximate (nondet within documented post-condition shape) rather than a fixed identity, and widen the Decoded domains toward the real decode_finite output — or explicitly encode the narrow domains as verified preconditions; (c) move the two std-body refactors upstream or gate/justify them. Until the strategy-function loops are exercised across their real iteration range, six of the twelve required functions are not soundly verified.