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

.gitignore

@@ -30,6 +30,12 @@ Cargo.lock
 /doc/mdbook-metrics/target
 *.png
 
+## Nix flake runtime artefacts
+/.rustup-fake/
+/.toolchain-wrapper/
+/kani-list.md
+/result
+
 ## Temporary files
 *~
 \#*

library/core/src/lib.rs

@@ -43,6 +43,7 @@
 //!   which do not trigger a panic can be assured that this function is never
 //!   called. The `lang` attribute is called `eh_personality`.
 
+#![cfg_attr(kani, recursion_limit = "256")]
 #![stable(feature = "core", since = "1.6.0")]
 #![doc(
     html_playground_url = "https://play.rust-lang.org/",

library/core/src/num/bignum.rs

@@ -335,6 +335,33 @@ macro_rules! define_bignum {
                 }
                 (self, borrow)
             }
+
+            /// Havoc the bignum to a nondeterministic value whose bit length is
+            /// bounded by `max_bits`. Used exclusively by Kani verification
+            /// stubs to avoid tracing through the full multi-limb arithmetic.
+            #[cfg(kani)]
+            #[doc(hidden)]
+            pub fn kani_size(&self) -> usize {
+                self.size
+            }
+
+            #[cfg(kani)]
+            #[doc(hidden)]
+            pub fn kani_havoc(&mut self, max_bits: usize) {
+                let digitbits = <$ty>::BITS as usize;
+                let cap_bits = $n * digitbits;
+                let bound = if max_bits > cap_bits { cap_bits } else { max_bits };
+                let sz: usize = crate::kani::any();
+                let max_sz = (bound + digitbits - 1) / digitbits;
+                crate::kani::assume(sz <= max_sz);
+                // Whole-array nondet; CBMC models this as a symbolic array
+                // without per-element loop unwinding. Skip the canonical-
+                // size mask and non-zero-top-limb constraints: dragon's
+                // safety stubs only depend on `size`, and adding those
+                // constraints would re-introduce per-limb reasoning.
+                self.size = sz;
+                self.base = crate::kani::any();
+            }
         }
 
         impl crate::cmp::PartialEq for $name {

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

@@ -124,6 +124,8 @@ functions.
 
 pub use self::decoder::{DecodableFloat, Decoded, FullDecoded, decode};
 use super::fmt::{Formatted, Part};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 
 pub mod decoder;
@@ -666,3 +668,309 @@ where
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Maximum digit buffer length we exercise. Small enough to verify fast, large
+    // enough to cover every branch in both targets (1, len == exp, len > exp,
+    // len < exp boundaries all become reachable).
+    const MAX_BUF_LEN: usize = 4;
+
+    // Reads every returned `Part` so that any uninitialized element would surface
+    // as a discriminant read on poisoned memory and trip Kani.
+    fn touch_parts(rendered: &[Part<'_>]) {
+        for part in rendered {
+            match *part {
+                Part::Zero(n) => {
+                    let _ = n;
+                }
+                Part::Num(v) => {
+                    let _ = v;
+                }
+                Part::Copy(bytes) => {
+                    // Force a real read of the slice header (ptr + len) and at
+                    // least one byte when non-empty.
+                    let _ = bytes.len();
+                    if !bytes.is_empty() {
+                        let _ = bytes[0];
+                    }
+                }
+            }
+        }
+    }
+
+    /// Proof for `digits_to_dec_str`.
+    ///
+    /// Rules out the following UB inside the function body:
+    ///   - `MaybeUninit::assume_init_ref` reading an uninitialized `Part<'a>`
+    ///     slot (every index covered by the `..N` slice returned in each of the
+    ///     six branches must have been written first).
+    ///   - Constructing an invalid `Part` value or an invalid `&[u8]` slice
+    ///     reference, which would be observed when `touch_parts` reads the
+    ///     enum discriminant and each variant payload.
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_digits_to_dec_str() {
+        // Symbolic buffer of length 1..=MAX_BUF_LEN. We back it with a fixed
+        // array and pick an arbitrary sub-slice via `any_slice_of_array`.
+        let buf_storage: [u8; MAX_BUF_LEN] = kani::any();
+        let buf: &[u8] = kani::slice::any_slice_of_array(&buf_storage);
+
+        // Honour the function's documented preconditions.
+        kani::assume(!buf.is_empty());
+        kani::assume(buf[0] > b'0');
+
+        // `parts` must have len >= 4. Use exactly 4 (the minimum) to keep the
+        // search space tight; the function never writes past index 3.
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+
+        // `exp: i16` is fully symbolic. The function admits any value in its
+        // domain. `frac_digits: usize` is bounded so that the symbolic state
+        // remains tractable while still covering the
+        // `frac_digits > buf.len()` / `frac_digits == 0` branches.
+        let exp: i16 = kani::any();
+        let frac_digits: usize = kani::any();
+        kani::assume(frac_digits <= 8);
+
+        let rendered = digits_to_dec_str(buf, exp, frac_digits, &mut parts_storage);
+        // The returned slice must be one of `..2`, `..3`, or `..4`.
+        assert!(rendered.len() >= 2 && rendered.len() <= 4);
+        touch_parts(rendered);
+    }
+
+    /// Proof for `digits_to_exp_str`.
+    ///
+    /// Rules out the following UB inside the function body:
+    ///   - `MaybeUninit::assume_init_ref` reading an uninitialized `Part<'a>`
+    ///     slot when the function returns `parts[..n + 2]`; every index in
+    ///     `0..n + 2` must have been initialized along the taken branch.
+    ///   - Constructing an invalid `Part::Num(u16)` from `-exp as u16` when
+    ///     `exp` was `i16::MIN` (the function compensates by casting through
+    ///     `i32` first; Kani sees the full domain of `exp`).
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_digits_to_exp_str() {
+        let buf_storage: [u8; MAX_BUF_LEN] = kani::any();
+        let buf: &[u8] = kani::slice::any_slice_of_array(&buf_storage);
+
+        kani::assume(!buf.is_empty());
+        kani::assume(buf[0] > b'0');
+
+        // `parts` must have len >= 6. The function writes at most six entries
+        // (`buf.len() > 1 || min_ndigits > 1` plus `min_ndigits > buf.len()`
+        // gives `n == 4`, then the trailing exponent pair brings the upper
+        // bound to `n + 2 == 6`).
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+
+        let exp: i16 = kani::any();
+        let min_ndigits: usize = kani::any();
+        kani::assume(min_ndigits <= 8);
+        let upper: bool = kani::any();
+
+        let rendered = digits_to_exp_str(buf, exp, min_ndigits, upper, &mut parts_storage);
+        // The returned slice is `parts[..n + 2]` with `n` in {1, 3, 4}, so the
+        // length is in {3, 5, 6}.
+        assert!(rendered.len() >= 3 && rendered.len() <= 6);
+        touch_parts(rendered);
+    }
+
+    // Stub digit-generation callback used by the public-wrapper proofs.
+    //
+    // The wrappers (`to_shortest_str`, `to_shortest_exp_str`, `to_exact_*_str`)
+    // accept any `FnMut(&Decoded, &'a mut [MaybeUninit<u8>]) -> (&'a [u8], i16)`
+    // that satisfies the documented preconditions of the helper it forwards to
+    // (`!buf.is_empty()`, `buf[0] > b'0'`). The shortest mode in particular
+    // requires the caller to provide a buffer with at least `MAX_SIG_DIGITS`
+    // bytes; the callback fills some prefix of it and returns that prefix.
+    //
+    // For verification we replace the real Grisu/Dragon callback with a stub
+    // that writes a single '1' digit. This keeps the proof focused on the
+    // wrapper's branching and `assume_init_ref` calls; the digit-generation
+    // strategies themselves are separate verification targets.
+    fn stub_format_shortest<'a>(
+        _decoded: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+    ) -> (&'a [u8], i16) {
+        buf[0] = MaybeUninit::new(b'1');
+        // SAFETY: index 0 was just initialised.
+        let s = unsafe { buf[..1].assume_init_ref() };
+        (s, 0_i16)
+    }
+
+    /// Proof for `to_shortest_str`, monomorphised to `f32`.
+    ///
+    /// Rules out UB across all four `FullDecoded` branches:
+    ///   - `Nan` and `Infinite` branches write one `Part::Copy` slot and
+    ///     `assume_init_ref` only that slot.
+    ///   - `Zero` branch writes one or two slots depending on `frac_digits`
+    ///     and assumes init of the matching prefix.
+    ///   - `Finite` branch delegates to the already-verified
+    ///     `digits_to_dec_str`. The stubbed callback satisfies its
+    ///     documented preconditions.
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_to_shortest_str_f32() {
+        let v: f32 = kani::any();
+        let frac_digits: usize = kani::any();
+        kani::assume(frac_digits <= 8);
+        let sign = if kani::any::<bool>() { Sign::Minus } else { Sign::MinusPlus };
+
+        let mut buf_storage: [MaybeUninit<u8>; MAX_SIG_DIGITS] =
+            [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS];
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+
+        let formatted = to_shortest_str::<f32, _>(
+            stub_format_shortest,
+            v,
+            sign,
+            frac_digits,
+            &mut buf_storage,
+            &mut parts_storage,
+        );
+
+        touch_parts(formatted.parts);
+    }
+
+    /// Proof for `to_shortest_exp_str`, monomorphised to `f32`.
+    ///
+    /// Same shape as `check_to_shortest_str_f32`. The Zero branch writes one
+    /// `Part::Copy` depending on whether `0` lies inside `dec_bounds`. The
+    /// Finite branch dispatches to either `digits_to_dec_str` (already
+    /// proven) or `digits_to_exp_str` (already proven) based on the
+    /// computed `vis_exp`.
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_to_shortest_exp_str_f32() {
+        let v: f32 = kani::any();
+        let dec_lo: i16 = kani::any();
+        let dec_hi: i16 = kani::any();
+        kani::assume(dec_lo <= dec_hi);
+        let upper: bool = kani::any();
+        let sign = if kani::any::<bool>() { Sign::Minus } else { Sign::MinusPlus };
+
+        let mut buf_storage: [MaybeUninit<u8>; MAX_SIG_DIGITS] =
+            [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS];
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+
+        let formatted = to_shortest_exp_str::<f32, _>(
+            stub_format_shortest,
+            v,
+            sign,
+            (dec_lo, dec_hi),
+            upper,
+            &mut buf_storage,
+            &mut parts_storage,
+        );
+
+        touch_parts(formatted.parts);
+    }
+
+    // Stubs for the `to_exact_*` callback shape.
+    //
+    // The real callbacks (`strategy::grisu::format_exact`, `strategy::dragon::
+    // format_exact`) either render at least one digit with `exp > limit` or
+    // return an empty buffer with `exp == limit` to signal "could not satisfy
+    // the limit". `to_exact_exp_str` ignores the empty case (it always calls
+    // `digits_to_exp_str` afterwards, which requires `!buf.is_empty()`).
+    // `to_exact_fixed_str` branches on `exp <= limit` and expects an empty
+    // buffer in that path. Two stubs handle the two contracts.
+
+    // Always returns one digit. Suitable for `to_exact_exp_str`.
+    fn stub_format_exact_nonempty<'a>(
+        _decoded: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        limit: i16,
+    ) -> (&'a [u8], i16) {
+        buf[0] = MaybeUninit::new(b'1');
+        // SAFETY: index 0 was just initialised.
+        let s = unsafe { buf[..1].assume_init_ref() };
+        // Ensure `exp > limit` for callers that branch on it.
+        (s, limit.saturating_add(1))
+    }
+
+    // Non-deterministically chooses between the "rendered" and "could not
+    // meet limit" outcomes. Suitable for `to_exact_fixed_str`, whose Finite
+    // branch needs both paths covered.
+    fn stub_format_exact_nondet<'a>(
+        _decoded: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        limit: i16,
+    ) -> (&'a [u8], i16) {
+        if kani::any::<bool>() {
+            // SAFETY: empty range, no element needs initialisation.
+            let empty = unsafe { buf[..0].assume_init_ref() };
+            (empty, limit)
+        } else {
+            buf[0] = MaybeUninit::new(b'1');
+            // SAFETY: index 0 was just initialised.
+            let s = unsafe { buf[..1].assume_init_ref() };
+            (s, limit.saturating_add(1))
+        }
+    }
+
+    /// Proof for `to_exact_exp_str`, monomorphised to `f32`.
+    ///
+    /// Branches: Nan/Infinite/Zero each `assume_init_ref` 1 or 3 slots
+    /// depending on `ndigits` and `upper`. Finite branch delegates to
+    /// `digits_to_exp_str` (already proven). `ndigits` is bounded so the
+    /// `buf.len() >= ndigits` precondition is trivially met.
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_to_exact_exp_str_f32() {
+        let v: f32 = kani::any();
+        let ndigits: usize = kani::any();
+        kani::assume(ndigits >= 1 && ndigits <= 8);
+        let upper: bool = kani::any();
+        let sign = if kani::any::<bool>() { Sign::Minus } else { Sign::MinusPlus };
+
+        let mut buf_storage: [MaybeUninit<u8>; MAX_SIG_DIGITS] =
+            [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS];
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+
+        let formatted = to_exact_exp_str::<f32, _>(
+            stub_format_exact_nonempty,
+            v,
+            sign,
+            ndigits,
+            upper,
+            &mut buf_storage,
+            &mut parts_storage,
+        );
+
+        touch_parts(formatted.parts);
+    }
+
+    /// Proof for `to_exact_fixed_str`, monomorphised to `f32`.
+    ///
+    /// Same shape as the other wrappers. The Finite branch has an extra
+    /// "rendered as zero after rounding" path that initialises 1 or 2 parts
+    /// depending on `frac_digits`. Uses a 256-byte buffer to satisfy the
+    /// `buf.len() >= maxlen` precondition for any `f32` exponent
+    /// (`estimate_max_buf_len` peaks around 133 for subnormal f32 inputs).
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_to_exact_fixed_str_f32() {
+        let v: f32 = kani::any();
+        let frac_digits: usize = kani::any();
+        kani::assume(frac_digits <= 8);
+        let sign = if kani::any::<bool>() { Sign::Minus } else { Sign::MinusPlus };
+
+        // 256 covers the worst-case `estimate_max_buf_len` for any f32 input.
+        let mut buf_storage: [MaybeUninit<u8>; 256] = [const { MaybeUninit::uninit() }; 256];
+        let mut parts_storage: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+
+        let formatted = to_exact_fixed_str::<f32, _>(
+            stub_format_exact_nondet,
+            v,
+            sign,
+            frac_digits,
+            &mut buf_storage,
+            &mut parts_storage,
+        );
+
+        touch_parts(formatted.parts);
+    }
+}