Challenge 28 (flt2dec): Kani's uninitialized-memory checker cannot analyze the `MaybeUninit` prefixes

[kanapitsas]

Filing this in the spirit of #656 — a gap that comes from tool limits rather than
from missing harnesses — because it affects what the three open Challenge 28 PRs
(#596, #601, #606) can claim about initialization. As of 2026-09-02 all three
remain open with changes requested.

The obligation

The challenge states its central obligation as:

This challenge is thus centered around proving well-encapsulation, which here
mainly means showing that calls to variants of assume_init() are only performed
on fully-initialized structures [...]

The unsafe sites in library/core/src/num/flt2dec/ consist mainly of
assume_init on prefixes. grep -n unsafe over the module returns
buf[..i].assume_init_ref(), buf[..i].assume_init_mut(),
buf[len - 1].assume_init() and parts[..n].assume_init_ref(), plus the two
lifetime-laundering reborrows in grisu.

Kani's built-in mechanism does not support these MaybeUninit shapes

Kani's built-in detector for reads of uninitialized memory is enabled by
-Z uninit-checks
(kani#3300; without instrumentation such a read yields a symbolic value rather
than an error, kani#920).

Measured on macOS 26.5.2 / arm64, Kani 0.67.0, on the four shapes that matter.
Case A is the positive control: it shows the flag itself works, so B/C/D are not
an invocation mistake.

Case A — empty harness:

#[kani::proof]
fn preuve() { let x: u8 = kani::any(); kani::assert(x == x, "trivial"); }

Case B — scalar MaybeUninit:

use std::mem::MaybeUninit;
#[kani::proof]
fn preuve() {
    let mut m = MaybeUninit::<u8>::uninit();
    m.write(7);
    let v = unsafe { m.assume_init() };
    kani::assert(v == 7, "ecrit");
}

Case C — array of MaybeUninit:

use std::mem::MaybeUninit;
#[kani::proof]
fn preuve() {
    let mut buf = [MaybeUninit::<u8>::uninit(); 4];
    buf[0] = MaybeUninit::new(7);
    let v = unsafe { buf[0].assume_init() };
    kani::assert(v == 7, "ecrit");
}

Case D — the shape flt2dec actually uses:

#![feature(maybe_uninit_slice)]
use std::mem::MaybeUninit;
#[kani::proof]
fn preuve() {
    let mut buf = [MaybeUninit::<u8>::uninit(); 4];
    buf[0] = MaybeUninit::new(7);
    let s: &[u8] = unsafe { buf[..1].assume_init_ref() };
    kani::assert(s[0] == 7, "ecrit");
}

Each run with cargo kani --harness preuve -Z uninit-checks:

case	result under -Z uninit-checks
A (positive control)	VERIFICATION:- SUCCESSFUL
B	VERIFICATION:- FAILED — "Interaction between raw pointers and unions is not yet supported."
C	VERIFICATION:- FAILED — "Checking memory initialization of type [std::mem::MaybeUninit; 4] is not supported. Cannot determine layout for a type that contains union of type std::mem::MaybeUninit as a field."
D	internal compiler error in kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs, pointing at kani#3300 (possibly the same instrumentation path as kani#3881)

So the built-in checker cannot traverse the MaybeUninit shapes used by these
functions. A custom logical encoding may still establish the property, but a
successful ordinary harness does not get this check automatically.

The flag is not enabled anywhere in this repository

grep -rn "uninit-checks" . over verify-rust-std at ad7590c returns no match.
scripts/run-kani.sh:87 passes:

-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing

What that means in practice

A mutant on the exact shape of dragon::format_shortest — a loop writing buf[i],
then returning buf[..i] — where the returned prefix is widened by one byte, so
that assume_init_ref covers a byte that was never written:

harness	mutant buf[..i] -> buf[..i + 1]
plain, with this repo's flags	VERIFICATION:- SUCCESSFUL (mutant survives)
plain, with -Z uninit-checks	does not compile (case D above)

Reading a never-written byte through assume_init_ref is real UB and is the
precise fault the challenge exists to catch, yet this mutant verifies clean.

This is not a criticism of the three open PRs. It means that claims based only
on executing or touching the returned value do not automatically discharge the
initialization obligation. A custom witness has to be checked at every relevant
assume_init* boundary, independently of the other blockers already raised in
review.

One workaround that does kill the mutant

The property can be encoded in the value domain instead, with no flag: pre-fill
the buffer with a symbolic byte constrained outside the ASCII digit range, then
assert that every returned byte is an ASCII digit. A byte that was never written
still carries the sentinel, so the assertion fails.

let s: u8 = kani::any();
kani::assume(s > b'9');            // sentinel outside the digit domain
// ... pre-fill buf with `s`, then call the function under proof ...
// assert every returned byte is in b'0'..=b'9'

On a final-return mutant this gives SUCCESSFUL for the unmutated code and
FAILED for the mutant, in about 1 second each. It is not sufficient as a final
postcondition alone: a too-wide intermediate assume_init_mut can consume the
sentinel and overwrite it before return. A second measured mutant does exactly
that; the return-only check passes, while the same check placed immediately
before assume_init_mut fails. The viable direction is therefore a boundary
witness at every assume_init*, plus an argument that the function's behaviour
does not depend on the fill value. I mention it only as a possible direction,
not as a finished proposal.

Suggestion

Either scope the obligation explicitly for Challenge 28 the way #656 does for
Challenge 12, so that reviewers and contributors agree on what a Kani solution
can and cannot claim, or state which of the accepted tools is expected to carry
the initialization part.

Happy to open a PR with the four measurement cases as a small standalone
reproducer if that would be useful.