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
 *~
 \#*

docs/README.md

@@ -0,0 +1,29 @@
+# Notes
+
+Working notes for this fork. Not part of the upstream `doc/` mdBook.
+
+## Status
+
+Challenge 28 (flt2dec): **12 of 12 functions verified end-to-end via Kani**. PR not yet opened. Run `nix run .#verify -- flt2dec` from the repo root to reproduce. Verified:
+
+- `digits_to_dec_str`, `digits_to_exp_str`, `to_shortest_str`, `to_shortest_exp_str`, `to_exact_exp_str`, `to_exact_fixed_str` (the last four monomorphised to `f32`)
+- `grisu::format_shortest_opt` and `grisu::format_exact_opt` via the Loitsch-paper-derived stubs and a hoisted `round_and_weed`
+- `grisu::format_shortest` and `grisu::format_exact` (the two lifetime-laundering wrappers) via hand-written stubs of the inner `_opt` calls and the dragon fallback
+- `dragon::format_shortest` and `dragon::format_exact` via tightened `Decoded` inputs matching `decode_finite`'s real output shape (`minus=1`, `plus in {1,2}`), a stub of `div_rem_upto_16` that directly encodes the algorithm's `d < 10` digit-range invariant, a stub of `Big::is_zero` that avoids the 40-limb `iter().all` unwind, a call-counter on `stub_big_cmp` that bounds the digit-generation loop within `MAX_SIG_DIGITS`, and a release-profile build (`CARGO_PROFILE_DEV_DEBUG_ASSERTIONS=false`) so the harness verifies *release semantics* — the algorithm-correctness `debug_assert!` invariants are out of scope for Challenge 28's "no UB" safety mandate.
+
+## Reproducing locally
+
+- `nix run .#verify -- flt2dec` — Verifies the 6 public/helper functions (passes).
+- `nix run .#verify -- flt2dec-grisu-strategies` — Verifies the 2 grisu `_opt` functions (passes).
+- `nix run .#verify -- flt2dec-grisu-wrappers` — Verifies the 2 grisu wrapper functions (passes, sub-second each).
+- `nix run .#verify -- flt2dec-dragon-strategies` — Verifies the 2 dragon strategy functions (passes, ~10s).
+
+Set `VERIFY_MEMORY_MAX` to override the default 24 GiB systemd-cgroup memory cap.
+
+## Contents
+
+- [research/verify-rust-std-challenge-landscape.md](research/verify-rust-std-challenge-landscape.md) - Snapshot of open challenges, tools, and Kani usage conventions as of 2026-05-19.
+- [decisions/0001-target-flt2dec-helpers-first.md](decisions/0001-target-flt2dec-helpers-first.md) - Why Challenge 28's two private helpers were the first target.
+- [decisions/0002-nix-flake-for-local-kani.md](decisions/0002-nix-flake-for-local-kani.md) - Flake design for reproducible Kani runs on NixOS.
+- [decisions/0003-grisu-needs-contract-decomposition.md](decisions/0003-grisu-needs-contract-decomposition.md) - Why the six Grisu/Dragon strategy functions needed contract-based decomposition; partially superseded by ADR 0004.
+- [decisions/0004-dragon-stubs-too-loose-for-safety.md](decisions/0004-dragon-stubs-too-loose-for-safety.md) - Dragon strategy verification gap and the contract-decomposition path forward.

docs/decisions/0001-target-flt2dec-helpers-first.md

@@ -0,0 +1,27 @@
+# 0001. Target flt2dec private helpers first for Challenge 28
+
+Status: accepted
+
+## Context
+
+Challenge 28 (flt2dec, 5000 USD bounty) requires proving twelve safe functions whose bodies contain `unsafe` code. All twelve centre on the same property: `MaybeUninit::assume_init*` calls must be preceded by full initialization of the indices they cover, and any lifetime laundering must be sound. No competing PRs are filed as of 2026-05-19. See `docs/research/verify-rust-std-challenge-landscape.md` for the wider landscape.
+
+A single-session contribution cannot realistically cover all twelve. Picking which subset to tackle first determines whether the work compiles and verifies, and whether the resulting harnesses provide a usable template for the remaining functions.
+
+## Options considered
+
+- **Private helpers `digits_to_dec_str` and `digits_to_exp_str`** (chosen) - Both are concrete, non-generic, no loops, no calls into the grisu/dragon strategies. All `assume_init_ref` calls are local to the function bodies. Preconditions are visible as `assert!` statements at the top. Together they cover six branches and exercise every variant of the `Part` enum. Small enough to verify fast, complete enough to be a real contribution.
+- **Public wrappers `to_shortest_str` and `to_shortest_exp_str`** - These call the private helpers; verifying them would transitively verify the helpers, but generic type parameters (`T: DecodableFloat`, `F: FnMut(&Decoded, &mut [u8]) -> (usize, i16)`) complicate harness construction. The spec allows restricting generics to primitive types, but that adds noise.
+- **Strategy entry points `format_shortest` / `format_exact` in grisu/dragon** - The most algorithmically interesting targets and the deepest use of unsafe, but they contain loops requiring `#[kani::unwind(N)]` bounds and substantial domain reasoning about the digit-generation invariants. Out of scope for an opening contribution.
+
+## Decision
+
+Land harnesses for `digits_to_dec_str` and `digits_to_exp_str` first. They are simple enough that the harness pattern (symbolic bounded inputs, assumption of documented preconditions, full read-back of returned `&[Part<'a>]`) generalizes to every other target in the challenge.
+
+## Consequences
+
+- Two of twelve target functions get covered in this initial cut. The remaining ten require follow-up work that can reuse the same `verify` module structure.
+- The harnesses are not run locally - building Kani on NixOS would require a nix-shell with rustup, cbmc, and kissat, plus bypassing the Ubuntu setup script. The project CI (Kani workflow) is the authoritative verification path; we rely on it.
+- The chosen targets ship as a `#[cfg(kani)] mod verify` block appended to `library/core/src/num/flt2dec/mod.rs`. The function bodies are untouched, which keeps the change clean and reduces review friction.
+- A reviewer might ask why `frac_digits` is bounded to `<= 8` rather than fully symbolic. The answer is verification-time tractability; an unbounded `usize` would explore arithmetic paths like `frac_digits - buf.len() - minus_exp` overflow but blow up the search. A follow-up harness can address overflow paths separately.
+- The lifetime-laundering aspect of the challenge is implicitly covered: the returned `&[Part<'a>]` borrows from `buf` and `parts_storage`, and the harness reads every element while both are still live. There is no explicit transmute or pointer cast in these two functions, so no separate lifetime proof is needed.

docs/decisions/0002-nix-flake-for-local-kani.md

@@ -0,0 +1,34 @@
+# 0002. Nix flake for local Kani runs
+
+Status: accepted
+
+## Context
+
+verify-rust-std's `scripts/run-kani.sh` clones Kani from a pinned commit and builds it from source. The build needs nightly Rust (matching `rust-toolchain.toml`), CBMC, kissat, plus the assumption that the dev environment looks like a rustup-managed Ubuntu box. On NixOS none of those assumptions hold: there is no `/bin/bash`, no rustup, the apt-based dep installer (`scripts/setup/ubuntu/install_deps.sh`) does not run, and CBMC / kissat live in `/nix/store` rather than `/usr/bin`.
+
+Without local verification, contributors rely on the project's CI to learn whether harnesses compile and pass. That feedback loop is too slow for iteration. See `docs/decisions/0001-target-flt2dec-helpers-first.md`, which initially deferred local runs for exactly this reason.
+
+## Options considered
+
+- **Nix flake providing tools, run-kani.sh does the Kani build** (chosen) - Flake exposes a devShell with fenix-managed nightly Rust, cbmc, kissat, python3, jq, build basics. A `nix run .#verify -- <challenge>` app wraps `run-kani.sh` after applying a few targeted patches (rustup-layout shim, cargo +toolchain wrapper, /bin/bash shebang fixes). First run rebuilds Kani from source against the pinned commit; subsequent runs are seconds.
+- **Build Kani itself in Nix (custom derivation)** - Cleanest in theory: Kani becomes a reproducible Nix package. Rejected as out of scope for a contributor environment - Kani's build assumes rustup and pulls a specific CBMC version; packaging it correctly is non-trivial and would diverge from the upstream build process.
+- **Docker / OCI container** - Avoids NixOS quirks by running an Ubuntu environment. Rejected because it adds a layer of virtualization, slows iteration, and contradicts the user's existing Nix-first workflow.
+- **Defer to CI only** - Rejected: slow feedback loop, no ability to debug locally, harness errors only visible after pushing.
+
+## Decision
+
+Ship `flake.nix` with a `devShells.default` and `apps.verify`. Map challenge names to fully-qualified harness identifiers in the app's case statement. Patch around five NixOS-specific issues at runtime:
+
+1. `/bin/bash` shebang in `run-kani.sh` and friends - rewrite to `/usr/bin/env bash`.
+2. `env!("RUSTUP_TOOLCHAIN")` in `build-kani/src/main.rs` - export it from `rust-toolchain.toml`.
+3. `RUSTUP_HOME/toolchains/$TC/lib` rpath in `kani-compiler/build.rs` - synthesise a fake `$PWD/.rustup-fake` whose toolchain symlink points at the fenix sysroot.
+4. `cargo +<toolchain>` invocation by kani-driver - install a thin shim `cargo` in `$PWD/.toolchain-wrapper` that strips the leading `+` arg and forwards.
+5. `kani_build/` left half-built by a previous failed run trips the script's "is Kani up to date" check (which only inspects the git commit, not the binary) - detect and clean.
+
+## Consequences
+
+- `nix run .#verify -- flt2dec` runs end-to-end on NixOS. Both harnesses verify, 254 individual safety checks succeed, verification time around 1.5 seconds after Kani is built.
+- The two flt2dec helper functions (`digits_to_dec_str`, `digits_to_exp_str`) move from "harnesses-written" to "machine-verified" status. The challenge as a whole stays open: 10 functions remain.
+- CBMC / kissat versions in nixpkgs are newer than Kani's pinned versions (6.9.0 vs 6.7.1, 4.0.4 vs 4.0.1). Kani's version-check scripts use "newer is fine" comparisons, so the mismatch does not trip the apt fallback. Worth re-verifying if Kani's pinned versions change.
+- The first run of `nix run .#verify` takes 10-20 minutes (Kani builds from source). Subsequent runs are seconds. `kani_build/` is gitignored.
+- The flake is verify-rust-std-specific; it does not generalise to other Nix-on-Rust setups without adjustment.

docs/decisions/0003-grisu-needs-contract-decomposition.md

@@ -0,0 +1,40 @@
+# 0003. Grisu and Dragon strategies need contract decomposition
+
+Status: accepted
+
+## Context
+
+The remaining six Challenge 28 targets are the four Grisu and two Dragon strategy functions: `format_shortest_opt`, `format_shortest`, `format_exact_opt`, `format_exact` in `flt2dec::strategy::grisu`, plus `format_shortest`, `format_exact` in `flt2dec::strategy::dragon`. The `_opt` functions are the actual digit-generation algorithms (~290 lines of dense unsafe + arithmetic). The non-`_opt` versions are thin wrappers that launder a lifetime through `unsafe { &mut *(buf as *mut _) }` and fall back to Dragon when Grisu returns `None`.
+
+Whole-program Kani harnesses for the wrappers were attempted (see git history). Even with aggressive constraints (`mant <= 0xFF`, `plus <= 0x0F`, `exp` in `[-4, 4]`, `#[kani::unwind(32)]`, 12 GiB memory cap), CBMC OOM-killed during the bit-blast phase. The algorithm's nested loops over u64/u128 arithmetic produce a SAT formula that exceeds available memory at any input bound large enough to exercise the digit-generation loop.
+
+## Options considered
+
+- **Whole-program verification of the wrappers** (rejected) - Forces Kani to trace into `format_shortest_opt` / `format_exact_opt`. OOM at the first grisu harness even with tight bounds. The CBMC formula for the digit-generation main loop alone has hundreds of thousands of clauses; combined with the surrounding arithmetic, the in-memory formula exceeds 12-24 GiB.
+- **Stub the `_opt` functions in the wrapper harness via `#[kani::stub]`** (rejected for now) - Possible but `#[kani::stub]` needs the stub to live somewhere Kani can find it during std verification. Plumbing this in the std crate is not standard; existing verified files in this repo do not use `kani::stub`. Worth revisiting if contract decomposition turns out to be slower than expected.
+- **Contract-based decomposition** (chosen) - Add `#[ensures]` (and likely `#[requires]`, `#[modifies]`) contracts to `format_shortest_opt` / `format_exact_opt` / dragon's `format_shortest` / dragon's `format_exact`. Verify each `_opt` against its own contract with `#[kani::proof_for_contract(...)]` in isolation. Then verify the wrappers (`format_shortest`, `format_exact`) using the contracts as stubs via `#[kani::stub_for_contract(...)]`. The wrapper proofs become cheap because Kani never traces into the algorithm.
+- **Skip the strategies entirely** (rejected) - Half the challenge would remain unsolved. The contract path is the well-trodden Kani idiom for exactly this situation.
+
+## Decision
+
+Defer the six strategy functions to a follow-up using contract decomposition.
+
+For each algorithm function (`format_shortest_opt`, `format_exact_opt`, dragon's `format_shortest`, dragon's `format_exact`):
+
+1. Write a `#[requires]` contract capturing the documented preconditions (the `assert!`s at the top of the function body).
+2. Write an `#[ensures]` contract capturing the relevant well-encapsulation invariant: the returned `&[u8]` is either empty (signalling failure) or has `result.0[0] > b'0'`. Crucially, ensure that the function did not read uninitialised memory through the supplied `MaybeUninit` buffer.
+3. Write a `#[kani::proof_for_contract(path)]` harness that calls the function with symbolic inputs and trusts Kani to check the contract.
+4. Tighten the contract until the proof passes within memory budget. This may require splitting harnesses per branch of the algorithm.
+
+For each lifetime-laundering wrapper (`format_shortest`, `format_exact` in grisu):
+
+1. Write a `#[kani::proof]` harness annotated with `#[kani::stub_for_contract(format_shortest_opt)]` (and the dragon fallback). This replaces the call to the algorithm with its contract's stub, so Kani only verifies the unsafe reborrow.
+2. The harness should run in seconds, not minutes.
+
+## Consequences
+
+- The current branch lands six of twelve Challenge 28 functions verified, with a clear road map for the remaining six. PRs against verify-rust-std historically accept partial coverage if the approach generalises.
+- A reviewer can read this ADR plus `decisions/0001-target-flt2dec-helpers-first.md` to understand both the picked subset and the deferred portion.
+- The contract approach is the canonical Kani technique for verifying unsafe code that wraps algorithmically dense helpers. Adopting it here keeps the proofs maintainable.
+- A second `nix run .#verify -- flt2dec-grisu` invocation is wired up for the deferred harnesses; it currently OOMs but exists as a sentinel for the contract refactor.
+- Memory cap (12 GiB by default, override via `VERIFY_MEMORY_MAX`) was introduced for this experiment and stays. It protects the host from runaway CBMC instances regardless of which challenge is being verified.