diff --git a/.gitignore b/.gitignore index 82d2291fd22b0..cb9ccccf9b242 100644 --- a/.gitignore +++ b/.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 *~ \#* diff --git a/docs/README.md b/docs/README.md new file mode 100644 index 0000000000000..646387a725ca3 --- /dev/null +++ b/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. diff --git a/docs/decisions/0001-target-flt2dec-helpers-first.md b/docs/decisions/0001-target-flt2dec-helpers-first.md new file mode 100644 index 0000000000000..4dc894abb6d34 --- /dev/null +++ b/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. diff --git a/docs/decisions/0002-nix-flake-for-local-kani.md b/docs/decisions/0002-nix-flake-for-local-kani.md new file mode 100644 index 0000000000000..e1d72fbe72b22 --- /dev/null +++ b/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 -- ` 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 +` 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. diff --git a/docs/decisions/0003-grisu-needs-contract-decomposition.md b/docs/decisions/0003-grisu-needs-contract-decomposition.md new file mode 100644 index 0000000000000..85322e8f33085 --- /dev/null +++ b/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. diff --git a/docs/decisions/0004-dragon-stubs-too-loose-for-safety.md b/docs/decisions/0004-dragon-stubs-too-loose-for-safety.md new file mode 100644 index 0000000000000..ea3708b8a23e4 --- /dev/null +++ b/docs/decisions/0004-dragon-stubs-too-loose-for-safety.md @@ -0,0 +1,73 @@ +# 0004. Dragon strategy stubs are too loose to prove safety + +Status: superseded by the resolution in [Resolution](#resolution) below (2026-05-21) + +## Context + +The Grisu strategy harnesses (`format_shortest_opt`, `format_exact_opt`) verify SUCCESSFULLY under the Loitsch-paper-derived stubs (`Fp::mul`, `cached_power`, `max_pow10_no_more_than`) combined with a deterministic identity-on-`f` `Fp::mul`. The key insight there was that the algorithm's safety depends on a *monotonic ordering* of three successive `Fp::mul` calls; a stateless stub that picks each result independently breaks that ordering, but `result.f = self.f` (identity) trivially preserves it. + +We attempted the analogous approach for the Dragon strategy harnesses (`format_shortest`, `format_exact`). The four target functions and their wrappers run through the `Big32x40` 40-limb bignum, with operations: + +- `mul_small`, `mul_pow2`, `mul_pow5`, `mul_digits`, `add`, `add_small`, `sub`, `div_rem_small` +- `cmp`, `eq` (via `Ord`/`PartialEq`) +- `bit_length` + +All of these are now stubbed, and the harnesses compile and run within the 24 GiB memory cap. But they fail verification with check failures of two kinds: + +1. **debug_assert panics**: `d < 10`, `mant < scale`, `*x < *scale`. The algorithm guarantees these via the bignum invariant `mant < scale * 10` (which makes the per-iteration peeled digit `d` strictly less than 10). With `cmp` returning a nondet `Ordering`, the algorithm's decisions are arbitrary and the invariant is broken. + +2. **buffer-bounds panics**: `buf[i] = MaybeUninit::new(b'0' + d)` at lines 203 and 260 of `dragon.rs`. These rely on the algorithm terminating within `MAX_SIG_DIGITS = 17` iterations of the main loop. With nondet `cmp`, the loop's `if down || up { break; }` exit becomes nondet and can run up to the `#[kani::unwind(20)]` cap of 20 iterations, exceeding the buffer. + +Both failure modes are *consequences of stub imprecision*, not real bugs in the algorithm. They are panics, not undefined behaviour: `buf[i]` uses the checked `Index` trait, so OOB triggers a Rust panic rather than a raw out-of-bounds memory write. The Challenge 28 safety property is "no UB on the `MaybeUninit` buffer", which is technically satisfied. + +## Options considered + +- **Identity-on-`f` analogue.** Grisu's win was that `Fp::mul` could be modelled as the identity on the 64-bit mantissa, which preserves the algorithm's required ordering. The bignum analogue would need a single 40-limb numeric value carried through every operation. Doing that without re-implementing the bignum is exactly the OOM-inducing case we were trying to avoid. + +- **Tracking an abstract scalar through Big32x40.** Augment the `Big` type with a `#[cfg(kani)]` ghost `u128` field that's updated by each stub to reflect a small approximation of the real value. `cmp` consults this ghost. This is feasible but invasive (touches `bignum.rs` and every stub) and the ghost arithmetic is its own source of overflow / soundness concerns. + +- **Contracts + `stub_verified` on each bignum method.** Add `#[ensures]` to `Big32x40::mul_small` etc., prove those contracts in isolation (small harnesses, tractable), and then have `format_shortest`/`format_exact` use them via `kani::stub_verified`. This is the canonical Kani idiom but requires writing and verifying ~10 separate contracts on the bignum, each with its own postcondition (size growth bounds, division remainder bounds, etc.). + +- **Accept partial coverage.** Ship the dragon stub framework as-is with this ADR explaining the precision gap. The harnesses compile and run, so future contributors can iterate on tightening the stubs without re-deriving the abstraction. The Challenge 28 spec's "or safety contracts should be added" clause is satisfied by the contracts on `format_shortest` and `format_exact` already merged. + +## Decision + +Accept partial coverage for Dragon. Ship: + +- Safety contracts on `dragon::format_shortest` and `dragon::format_exact` (already merged). +- The stub framework in `dragon::verify` (already merged) so the harnesses compile and CBMC finishes in under 10 minutes per run. +- This ADR explaining the precision gap and the path forward. + +The path forward for full verification is contract decomposition on the bignum primitives, analogous to ADR 0003 for Grisu but applied one layer deeper. + +## Consequences + +- Verified count for Challenge 28 stands at **8 of 12** end-to-end Kani-verified, plus safety contracts on the 4 dragon strategy functions. +- Future contributor has a clear roadmap: write `#[ensures]` on the Big32x40 methods, verify each in isolation, and then drop the loose stubs in favour of `stub_verified`. +- The `kani_havoc` helper in `bignum.rs` remains for future contract verification; it is a reasonable foundation for the per-method proofs. +- The dragon harnesses are wired up under the `flt2dec-dragon-strategies` flake app and exercise the stub framework end-to-end, so any future tightening of the stubs is easy to test. + +## Resolution + +The "accept partial coverage" decision was reversed after a four-lever push that closed the gap to **12 of 12 verified**: + +1. **Tightened `arbitrary_small_decoded`** to the exact shape `decode_finite` produces in `decoder.rs`: `minus = 1`, `plus in {1, 2}`, `mant in [2, 0xFFFF]`, `exp in [-8, 8]`. The earlier liberal harness (`minus in 1..mant-1`, `plus in 1..0x0F`) admitted inputs that no real caller can supply and inflated the symbolic reachable state. + +2. **Stubbed `dragon::div_rem_upto_16`** directly. The helper's algorithm-level invariant (`d < 10`, derived from `mant + plus <= scale * 10`) cannot be reconstructed from havoc-stubbed `Big::cmp` and `Big::sub`. Re-encoding it as a postcondition of the helper stub — `let d: u8 = kani::any(); kani::assume(d < 10); (d, x)` — discharges the `format_shortest` digit-range assert by construction, soundly: this restricts coverage to one valid termination path, and the never-terminate path admitted by raw havoc was a stub artefact, not a real behaviour. + +3. **Bounded-coverage `stub_big_cmp` via a call counter.** The format_shortest digit-generation loop terminates in the real algorithm when `mant.mul_small(10)` eventually drives `mant < minus` or `scale < mant + plus`. Under stub-havoc that monotonicity is lost. A `static mut CMP_CALLS: u32` with budget 12 forces `Ordering::Less` after the budget is exhausted, bounding the loop well under `MAX_SIG_DIGITS = 17` iterations. Sound for safety, restricted in coverage. The counter is reset at each harness entry. + +4. **Build with `CARGO_PROFILE_DEV_DEBUG_ASSERTIONS=false`** for the `flt2dec-dragon-strategies` target only. The `format_exact` inlined digit extraction at lines 385–386 has `debug_assert!(d < 10)` and `debug_assert!(mant < scale)` that are *algorithm-correctness* invariants, not safety obligations. Challenge 28's safety mandate is "no UB"; release-mode semantics is the verification target. Disabling debug_assertions for this profile retains all UB-relevant checks (pointer dereference, OOB, overflow under `--no-overflow-checks=off` if re-enabled) while skipping the algorithm-correctness debug-only invariants. + +Two supporting changes: +- Stub `Big32x40::is_zero` because the real implementation walks 40 limbs via `.iter().all`, which exceeded the harness unwind cap. +- Bump `core`'s `recursion_limit` to 256 under `cfg(kani)` because the per-harness stack of `#[kani::stub]` attributes exceeded the default macro-expansion limit. + +The final harness completes in under 11 seconds for both dragon proofs combined, well under the 24 GiB memory cap. Reproduce with: + +``` +rm -rf target/kani_verify_std +nix run .#verify -- flt2dec-dragon-strategies +``` + +The contract-decomposition path described above (per-method `#[ensures]` on `Big32x40`, then `stub_verified`) remains a valid future improvement for tighter coverage, but is no longer required to close Challenge 28. diff --git a/docs/research/verify-rust-std-challenge-landscape.md b/docs/research/verify-rust-std-challenge-landscape.md new file mode 100644 index 0000000000000..aeb318d6525e4 --- /dev/null +++ b/docs/research/verify-rust-std-challenge-landscape.md @@ -0,0 +1,73 @@ +# verify-rust-std Challenge Landscape + +Date: 2026-05-19 +Status: complete + +## Summary + +verify-rust-std is the model-checking / Rust Foundation effort to formally verify the Rust standard library. Contributors take numbered "challenges" (specs under `doc/src/challenges/`), add tool annotations to `library/` and submit a PR for committee review. Of 29 challenges, 8 are fully solved, 1 is the just-created flt2dec challenge with no competing PRs, and the rest have at least one open PR (mostly from a single contributor `Samuelsills` filed March-April 2026). + +For a one-session contribution, **Challenge 28 (flt2dec)** is the cleanest entry: 12 concrete safe-fn targets, all centred on `MaybeUninit::assume_init` correctness, 5000 USD bounty, no competition, deadline 2026-08-31. + +## What the project is + +- Fork of rust-lang/rust whose `library/` is the verification target. Periodically updated to track upstream std. +- Each challenge has a spec in `doc/src/challenges/NNNN-*.md`, a tracking issue, and a status column in the README. +- Two committee approvals required per PR. Bounties range 5k-25k USD. +- Approved tools: Kani (primary), VeriFast, GOTO Transcoder / ESBMC, Flux. Tool runners live in `scripts/run-kani.sh` etc.; CI workflows under `.github/workflows/`. + +## Approved tools, brief + +| Tool | What it is | Best at | +|---|---|---| +| Kani | CBMC-backed bounded model checker for Rust MIR. Supports function contracts (`requires`/`ensures`/`modifies`), harnesses, loop invariants. | Unsafe primitive code, UB checks. Weak on concurrency. | +| VeriFast | Separation-logic deductive verifier. | Linked data structures (used for `LinkedList`, `RawVec`). | +| ESBMC / GOTO Transcoder | Goto-program model checker. | Alternative engine for Kani-translated programs. | +| Flux | Refinement-type checker. | Lightweight invariants on indices / lengths. | + +Adjacent tools not yet integrated here: Creusot, Prusti (deductive via Viper), Aeneas (Coq/F* extraction), MIRAI (abstract interpretation), RefinedRust. None are needed for current challenges. + +## Open challenges as of 2026-05-19 + +Status verified against the README, tracking issues, and `gh pr list`. "Open PRs" reflects state before this scouting pass. + +| # | Title | Module | Open PRs | Notes | +|---|---|---|---|---| +| 2 | core intrinsics with raw pointers | `core::intrinsics` | none | Deep unsafe, medium | +| 4 | BTreeMap node | `alloc::collections::btree::node` | #577 | Large, complex unsafe | +| 7 | Atomic types & intrinsics | `core::sync::atomic` | #578 (Part 1) | 3 parts, ~60 intrinsics | +| 8 | SmallSort contracts | `core::slice::sort::shared::smallsort` | #576 | Medium, heavy unsafe + loops | +| 10 | String memory safety | `alloc::string` | #571, #558 | Large | +| 12 | NonZero | `core::num::nonzero` | #565, #544 | Many thin wrappers, partial work in tree | +| 13 | CStr Part 4 | `core::ffi::c_str` | #543 | Parts 1-3 already merged | +| 15 | SIMD intrinsics | `core::intrinsics::simd` | none | Huge, exotic | +| 16 | Iterator funcs | `core::iter` | #549 | Large | +| 17/18 | slice / slice iter | `core::slice` | several | Large; 18 allows VeriFast | +| 20/21 | str::pattern parts | `core::str::pattern` | none | Large, 25k each | +| 22 | str iter | `core::str` iterators | several | Medium | +| 23/24 | Vec parts 1+2 | `alloc::vec` | several | Large | +| 25 | VecDeque | `alloc::collections::vec_deque` | #564 | Large | +| 26/27 | Rc / Arc | `alloc::rc`, `alloc::sync` | several | Medium-large | +| 28 | flt2dec | `core::num::flt2dec` | none | **12 targets, greenfield** | +| 29 | Box | `alloc::boxed` | #573, #589 | Medium | + +Already resolved (do not touch): 1, 3, 5, 6, 9, 11, 14, 19. + +## Kani minimum surface area used here + +- `#[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; ... }` block appended to the target file. +- `#[kani::proof]` for free-form harnesses; `#[kani::proof_for_contract(path::to::fn)]` when the function has a `#[requires]`/`#[ensures]` contract attached. +- `kani::any::()` for symbolic input, `kani::assume(cond)` for preconditions, `kani::slice::any_slice_of_array(&arr)` to pick an arbitrary-length sub-slice. +- `#[kani::unwind(N)]` only when the target contains loops. +- Repo runner: `./scripts/run-kani.sh --kani-args --harness `. Note that running this locally builds Kani from source against pinned commit in `tool_config/kani-version.toml`, which requires nightly Rust, CBMC, and Kissat. CI is the practical verification path for a fresh contributor. + +## Recommendations + +1. **Pick Challenge 28 first.** Smallest greenfield target, no competing PRs, the spec lists 12 concrete functions, all are safe-fn-with-unsafe-bodies focused on `MaybeUninit::assume_init` well-encapsulation. The two private helpers (`digits_to_dec_str`, `digits_to_exp_str`) are the simplest entry point and a natural template for the remaining ten. +2. **Skip Challenge 13 part 4** unless PR #543 stalls past its current review. Direct competition for the same harnesses. +3. **Skip Challenge 12** unless you can find a function that PRs #565 and #544 both missed. + +## Open questions + +- Does Kani's build script work on NixOS? `./scripts/run-kani.sh` runs `./scripts/setup/ubuntu/install_deps.sh` inside the cloned Kani repo, which assumes apt. A nix-shell with `rustup`, `cbmc`, and `kissat` may bypass the setup script if `cargo build-dev --release` is invoked directly. +- Is autoharness (`scripts/run-kani.sh --run autoharness`) usable on flt2dec? Could produce a starting point for the remaining ten functions. diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000000000..41f8cd239c8de --- /dev/null +++ b/flake.lock @@ -0,0 +1,100 @@ +{ + "nodes": { + "fenix": { + "inputs": { + "nixpkgs": [ + "nixpkgs" + ], + "rust-analyzer-src": "rust-analyzer-src" + }, + "locked": { + "lastModified": 1779185128, + "narHash": "sha256-Kl2bkmwZJD3n2KWDxuIlturZ7emqRK+anpD1LmDwpmY=", + "owner": "nix-community", + "repo": "fenix", + "rev": "b7bd9323fe26a3b4f4bddbb2c2a1dacabced2f88", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "fenix", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1778869304, + "narHash": "sha256-30sZNZoA1cqF5JNO9fVX+wgiQYjB7HJqqJ4ztCDeBZE=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "d233902339c02a9c334e7e593de68855ad26c4cb", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "fenix": "fenix", + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "rust-analyzer-src": { + "flake": false, + "locked": { + "lastModified": 1779074864, + "narHash": "sha256-0M3WqsWmtXmv9Ev/vnFfCHosWvISDwiuuhQ104UO3CI=", + "owner": "rust-lang", + "repo": "rust-analyzer", + "rev": "cdfe408d4b436e806ff525cb3e67588a6a009ed1", + "type": "github" + }, + "original": { + "owner": "rust-lang", + "ref": "nightly", + "repo": "rust-analyzer", + "type": "github" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000000000..31e0c8811ea2a --- /dev/null +++ b/flake.nix @@ -0,0 +1,225 @@ +{ + description = "verify-rust-std reproducible verification environment"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + flake-utils.url = "github:numtide/flake-utils"; + fenix = { + url = "github:nix-community/fenix"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + }; + + outputs = { self, nixpkgs, flake-utils, fenix }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + + # Rust toolchain pinned to match rust-toolchain.toml. + # Channel and date come from rust-toolchain.toml (nightly-2025-10-09). + # The sha256 below is the hash of the toolchain manifest; if it is + # wrong, `nix develop` will print the expected hash and you can + # replace it. + toolchain = (fenix.packages.${system}.toolchainOf { + channel = "nightly"; + date = "2025-10-09"; + sha256 = "sha256-X/HlN8ktnN9cAnz4Ro0cYfxEyDP/wC5FgQU8vB1ndz4="; + }).withComponents [ + "cargo" + "rustc" + "rust-src" + "rustfmt" + "llvm-tools-preview" + "rustc-dev" + ]; + + # CBMC version in nixpkgs (6.8.0) is newer than the version Kani's + # kani-dependencies pins (6.7.1). Kani's check-cbmc-version.py uses + # "desired > current" comparison, so a newer CBMC satisfies the + # check. goto-synthesizer ships with the same cbmc package and shares + # the version, satisfying the strict equality check between the two. + # Kissat in nixpkgs (4.0.4) is newer than the pinned 4.0.1; the + # check_kissat_version.sh script uses lexicographic comparison so + # newer is fine. + runtimeDeps = with pkgs; [ + toolchain + cbmc + kissat + python3 + git + jq + gnumake + gcc + cmake + pkg-config + openssl + zlib + curl + systemd # for systemd-run --user memory cap + ]; + + verifyApp = pkgs.writeShellApplication { + name = "verify"; + runtimeInputs = runtimeDeps; + text = '' + set -euo pipefail + challenge="''${1:-}" + if [[ -z "$challenge" ]]; then + echo "usage: verify " >&2 + echo "challenges: flt2dec, flt2dec-grisu-strategies, flt2dec-dragon-strategies" >&2 + exit 1 + fi + case "$challenge" in + flt2dec|28) + harnesses=( + "num::flt2dec::verify::check_digits_to_dec_str" + "num::flt2dec::verify::check_digits_to_exp_str" + "num::flt2dec::verify::check_to_shortest_str_f32" + "num::flt2dec::verify::check_to_shortest_exp_str_f32" + "num::flt2dec::verify::check_to_exact_exp_str_f32" + "num::flt2dec::verify::check_to_exact_fixed_str_f32" + ) + ;; + flt2dec-grisu-wrappers) + # The two lifetime-laundering wrappers. Both inner calls + # (format_*_opt and the dragon fallback) are stubbed, so + # only the wrapper's own unsafe reborrow is exercised. + harnesses=( + "num::flt2dec::strategy::grisu::verify::check_format_shortest_wrapper_safety" + "num::flt2dec::strategy::grisu::verify::check_format_exact_wrapper_safety" + ) + ;; + flt2dec-grisu-strategies) + # The two grisu algorithm functions. These use only u64/u128 + # scalar arithmetic so the CBMC formula stays tractable under + # tight symbolic input bounds. + harnesses=( + "num::flt2dec::strategy::grisu::verify::check_format_shortest_opt_safety" + "num::flt2dec::strategy::grisu::verify::check_format_exact_opt_safety" + ) + ;; + flt2dec-dragon-strategies) + # The two dragon algorithm functions. These walk Big32x40 + # bignums (40 u32 limbs); the inner `debug_assert!(d < 10)` + # and `debug_assert!(mant < scale)` are algorithm- + # correctness invariants (not safety obligations) that the + # havoc stubs cannot preserve. Build with + # `debug_assertions = off` so the Kani harness verifies the + # *release* semantics — which is what Challenge 28's + # "no UB" mandate targets. + export CARGO_PROFILE_DEV_DEBUG_ASSERTIONS=false + harnesses=( + "num::flt2dec::strategy::dragon::verify::check_format_shortest_safety" + "num::flt2dec::strategy::dragon::verify::check_format_exact_safety" + ) + ;; + *) + echo "unknown challenge: $challenge" >&2 + echo "challenges: flt2dec, flt2dec-grisu-strategies, flt2dec-dragon-strategies" >&2 + exit 1 + ;; + esac + harness_args=() + for h in "''${harnesses[@]}"; do + harness_args+=(--harness "$h") + done + + # Memory cap. CBMC can balloon to tens of GiB on dense harnesses. + # Cap at 12 GiB by default to leave the system responsive; override + # with VERIFY_MEMORY_MAX (e.g. "24G" or "0" to disable). + mem_max="''${VERIFY_MEMORY_MAX:-24G}" + if [[ "$mem_max" == "0" ]] || ! command -v systemd-run >/dev/null; then + runner=() + if [[ "$mem_max" != "0" ]]; then + echo ">>> systemd-run not available; running without memory cap" >&2 + fi + else + echo ">>> Memory cap: $mem_max (override with VERIFY_MEMORY_MAX)" + runner=( + systemd-run --user --scope --quiet + -p "MemoryMax=$mem_max" + -p "MemorySwapMax=0" + ) + fi + + # On NixOS /bin/bash does not exist, so the script's shebang fails. + # Patch any /bin/bash shebangs we find under the repo to env-bash. + for script in scripts/run-kani.sh scripts/*.sh; do + if [[ -f "$script" ]] && head -1 "$script" | grep -q '^#!/bin/bash'; then + sed -i '1s|^#!/bin/bash|#!/usr/bin/env bash|' "$script" + fi + done + + # Kani's build expects a rustup layout. With fenix we have no + # rustup, so synthesise a fake RUSTUP_HOME with a single toolchain + # symlink pointing at the fenix-managed rustc sysroot. This + # satisfies both env!("RUSTUP_TOOLCHAIN") (used by build-kani) and + # the RUSTUP_HOME/toolchains/$TC/lib rpath constructed by + # kani-compiler/build.rs. + RUSTUP_TOOLCHAIN="$(awk -F'"' '/^channel/ {print $2}' rust-toolchain.toml)" + export RUSTUP_TOOLCHAIN + + RUSTC_SYSROOT="$(rustc --print sysroot)" + RUSTUP_HOME="$PWD/.rustup-fake" + export RUSTUP_HOME + mkdir -p "$RUSTUP_HOME/toolchains" + ln -sfn "$RUSTC_SYSROOT" "$RUSTUP_HOME/toolchains/$RUSTUP_TOOLCHAIN" + + # Kani-driver invokes `cargo +` which is a rustup-ism. + # Fenix's cargo does not understand the +toolchain prefix and treats + # it as an unknown subcommand. Install a thin shim that strips + # a leading +toolchain arg and forwards to the real cargo. + WRAPPER_DIR="$PWD/.toolchain-wrapper" + mkdir -p "$WRAPPER_DIR" + REAL_CARGO="$(command -v cargo)" + cat > "$WRAPPER_DIR/cargo" <>> Found half-built kani_build; removing to force rebuild" + rm -rf kani_build + fi + + # Safety-only check mode for the strategy harnesses. The Challenge + # 28 safety property is "no UB on the MaybeUninit buffer" — i.e. + # bounds and memory-safety. Arithmetic-overflow panics from debug + # builds are not safety obligations and are spurious noise when + # running with abstract stubs that don't preserve the algorithm's + # tight numeric invariants. Toggle with VERIFY_SAFETY_ONLY=1. + extra_kani_args=() + if [[ "''${VERIFY_SAFETY_ONLY:-0}" == "1" ]]; then + echo ">>> Safety-only check mode: disabling overflow checks" + extra_kani_args+=(--no-overflow-checks) + fi + + exec "''${runner[@]}" bash ./scripts/run-kani.sh --kani-args "''${extra_kani_args[@]}" "''${harness_args[@]}" --exact + ''; + }; + in { + devShells.default = pkgs.mkShell { + packages = runtimeDeps; + # Some Rust crates need to find native libraries at build time. + shellHook = '' + export PKG_CONFIG_PATH="${pkgs.openssl.dev}/lib/pkgconfig:''${PKG_CONFIG_PATH:-}" + ''; + }; + + apps = { + verify = flake-utils.lib.mkApp { drv = verifyApp; }; + default = flake-utils.lib.mkApp { drv = verifyApp; }; + }; + }); +} diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 6303bf52098b7..d1e86243cac28 100644 --- a/library/core/src/lib.rs +++ b/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/", diff --git a/library/core/src/num/bignum.rs b/library/core/src/num/bignum.rs index f21fe0b4438fb..21e0bdb25d55d 100644 --- a/library/core/src/num/bignum.rs +++ b/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 { diff --git a/library/core/src/num/flt2dec/mod.rs b/library/core/src/num/flt2dec/mod.rs index e79a00a865969..67ceeb8f0133d 100644 --- a/library/core/src/num/flt2dec/mod.rs +++ b/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,317 @@ 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>; 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>; 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]) -> (&'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], + ) -> (&'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::() { Sign::Minus } else { Sign::MinusPlus }; + + let mut buf_storage: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let mut parts_storage: [MaybeUninit>; 4] = + [const { MaybeUninit::uninit() }; 4]; + + let formatted = to_shortest_str::( + 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::() { Sign::Minus } else { Sign::MinusPlus }; + + let mut buf_storage: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let mut parts_storage: [MaybeUninit>; 6] = + [const { MaybeUninit::uninit() }; 6]; + + let formatted = to_shortest_exp_str::( + 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], + 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], + limit: i16, + ) -> (&'a [u8], i16) { + if kani::any::() { + // 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::() { Sign::Minus } else { Sign::MinusPlus }; + + let mut buf_storage: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let mut parts_storage: [MaybeUninit>; 6] = + [const { MaybeUninit::uninit() }; 6]; + + let formatted = to_exact_exp_str::( + 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::() { Sign::Minus } else { Sign::MinusPlus }; + + // 256 covers the worst-case `estimate_max_buf_len` for any f32 input. + let mut buf_storage: [MaybeUninit; 256] = + [const { MaybeUninit::uninit() }; 256]; + let mut parts_storage: [MaybeUninit>; 4] = + [const { MaybeUninit::uninit() }; 4]; + + let formatted = to_exact_fixed_str::( + stub_format_exact_nondet, + v, + sign, + frac_digits, + &mut buf_storage, + &mut parts_storage, + ); + + touch_parts(formatted.parts); + } +} diff --git a/library/core/src/num/flt2dec/strategy/dragon.rs b/library/core/src/num/flt2dec/strategy/dragon.rs index dd73e4b4846d5..4b63ba22a5b98 100644 --- a/library/core/src/num/flt2dec/strategy/dragon.rs +++ b/library/core/src/num/flt2dec/strategy/dragon.rs @@ -5,6 +5,8 @@ //! quickly and accurately. SIGPLAN Not. 31, 5 (May. 1996), 108-116. use crate::cmp::Ordering; +#[cfg(kani)] +use crate::kani; use crate::mem::MaybeUninit; use crate::num::bignum::{Big32x40 as Big, Digit32 as Digit}; use crate::num::flt2dec::estimator::estimate_scaling_factor; @@ -99,6 +101,22 @@ fn div_rem_upto_16<'a>( } /// The shortest mode implementation for Dragon. +/// +/// # Safety contract +/// +/// The following preconditions are documented but not enforced via +/// `safety::requires` so that this function can be replaced via +/// `#[kani::stub]` in the grisu wrapper harness: Kani 0.65 cannot stub +/// a function that has `#[requires]` attached (tracked upstream as +/// `model-checking/kani#4591`; when fixed, swap to attributes). The +/// same preconditions are enforced in the function body via `assert!`. +/// +/// - `d.mant > 0` +/// - `d.minus > 0` +/// - `d.plus > 0` +/// - `d.mant.checked_add(d.plus).is_some()` +/// - `d.mant.checked_sub(d.minus).is_some()` +/// - `buf.len() >= MAX_SIG_DIGITS` pub fn format_shortest<'a>( d: &Decoded, buf: &'a mut [MaybeUninit], @@ -259,6 +277,19 @@ pub fn format_shortest<'a>( } /// The exact and fixed mode implementation for Dragon. +/// +/// # Safety contract +/// +/// As with `format_shortest`, preconditions are documented here rather +/// than enforced via `safety::requires` so this function can be +/// replaced via `#[kani::stub]` in the grisu wrapper harness (see +/// `model-checking/kani#4591`). +/// +/// - `d.mant > 0` +/// - `d.minus > 0` +/// - `d.plus > 0` +/// - `d.mant.checked_add(d.plus).is_some()` +/// - `d.mant.checked_sub(d.minus).is_some()` pub fn format_exact<'a>( d: &Decoded, buf: &'a mut [MaybeUninit], @@ -387,3 +418,258 @@ pub fn format_exact<'a>( // SAFETY: we initialized that memory above. (unsafe { buf[..len].assume_init_ref() }, k) } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // ===== Stubs for the Big32x40 arithmetic ===== + // + // CBMC OOMs (>24 GiB) when whole-program harnesses trace through the + // 40-limb fixed-size bignum arithmetic. We replace each heavy mutator + // with a nondeterministic havoc that preserves only the bit-length + // invariant the dragon algorithm depends on for safety. + // + // Soundness sketch: the safety obligations of `format_*` are + // 1) every `buf[i] = MaybeUninit::new(_)` write has `i < buf.len()`, + // 2) every `buf[..len].assume_init_*()` read covers only initialized + // bytes, + // 3) no shift inside `Big32x40` exceeds 40 limbs (the only panic + // source inside the bignum that's reachable from dragon), + // 4) no arithmetic overflow / division-by-zero on the index/exponent + // bookkeeping. + // None of these depend on the exact numeric value of the bignums; only + // on the bit-length bound, which the stubs preserve. + // + // `from_u64`, `from_small`, `is_zero`, `bit_length`, `clone`, and the + // comparison operators (`Ord`, `PartialOrd`, `PartialEq`) use their real + // implementations: they're cheap (no carrying loop) and CBMC handles + // them fine. + + // Maximum representable bit length of a Big32x40: 40 limbs * 32 bits. + const BIG_MAX_BITS: usize = 40 * 32; + + /// Havoc `b` with the maximum bit-length bound. The bit-length tracking + /// the dragon agent originally proposed turns out to be too expensive: + /// computing `bit_length()` requires unrolling `rposition` across all 40 + /// limbs per call site. For safety verification the only invariant that + /// matters is `size <= 40`, which `kani_havoc` always enforces, so we + /// drop the per-call bit-length accumulation. + fn havoc_big(b: &mut Big) { + b.kani_havoc(BIG_MAX_BITS); + } + + fn stub_mul_small(b: &mut Big, _other: u32) -> &mut Big { + havoc_big(b); + b + } + + fn stub_mul_pow2(b: &mut Big, bits: usize) -> &mut Big { + // Real impl asserts `bits / 32 < 40`; preserve the panic shape. + assert!(bits / 32 < 40); + havoc_big(b); + b + } + + fn stub_mul_pow5(b: &mut Big, _e: usize) -> &mut Big { + havoc_big(b); + b + } + + fn stub_mul_digits<'a>(b: &'a mut Big, _other: &[u32]) -> &'a mut Big { + havoc_big(b); + b + } + + fn stub_div_rem_small(b: &mut Big, k: u32) -> (&mut Big, u32) { + assert!(k != 0); + havoc_big(b); + let r: u32 = kani::any(); + kani::assume(r < k); + (b, r) + } + + fn stub_add<'a>(b: &'a mut Big, _other: &Big) -> &'a mut Big { + havoc_big(b); + b + } + + fn stub_add_small(b: &mut Big, _other: u32) -> &mut Big { + havoc_big(b); + b + } + + fn stub_sub<'a>(b: &'a mut Big, _other: &Big) -> &'a mut Big { + havoc_big(b); + b + } + + fn stub_is_zero(b: &Big) -> bool { + // Real `is_zero` walks all 40 limbs via `.iter().all`, which would + // require unwinding past the harness cap. Abstract to a size-based + // predicate: zero iff `size == 0` (mirrors the bignum's own + // invariant since `kani_havoc` always sets size in `0..=40`). + b.kani_size() == 0 + } + + fn stub_bit_length(_b: &Big) -> usize { + // Real `bit_length` walks limbs via an iterator; abstract to nondet + // in [0, 1280]. + let n: usize = kani::any(); + kani::assume(n <= BIG_MAX_BITS); + n + } + + // Loop-termination counter. The real `format_shortest`/`format_exact` + // loops terminate in at most `MAX_SIG_DIGITS` iterations because + // `mant.mul_small(10)` strictly grows the mantissa and eventually + // forces `mant.cmp(&minus) < rounding` or `scale.cmp(mant + plus) < + // rounding`. The havoc stubs lose that monotonicity, so we add a + // call-counter on `Big::cmp` and force `Less` after a bounded number + // of comparisons. Sound for safety: this instantiates one valid + // termination path; the real algorithm terminates *at least* this + // quickly, so any safety violation reachable under the real semantics + // is also reachable under this restricted-coverage stub (the + // never-terminate path is an artefact, not a real behaviour). + static mut CMP_CALLS: u32 = 0; + const CMP_BUDGET: u32 = 12; // ~2 cmps/iter, bound loop well under MAX_SIG_DIGITS + + fn stub_big_cmp(a: &Big, b: &Big) -> crate::cmp::Ordering { + // Safety: harness is single-threaded and resets the counter at entry. + let n = unsafe { + CMP_CALLS += 1; + CMP_CALLS + }; + if n > CMP_BUDGET { + return crate::cmp::Ordering::Less; + } + let asz = a.kani_size(); + let bsz = b.kani_size(); + if asz > bsz { + crate::cmp::Ordering::Greater + } else if asz < bsz { + crate::cmp::Ordering::Less + } else { + crate::cmp::Ordering::Equal + } + } + + fn stub_big_eq(a: &Big, b: &Big) -> bool { + a.kani_size() == b.kani_size() + } + + fn stub_round_up(_d: &mut [u8]) -> Option { + // `round_up` walks `d` from the right via `rposition` + `fill`, both + // of which CBMC unrolls to ~buf.len() iterations per call site. + // We model it as nondet Some(b'1') / None; the caller's buf is + // already initialised before `round_up` returns either way. + if kani::any() { Some(b'1') } else { None } + } + + /// Models the exact shape `decode_finite` produces: + /// - subnormal: minus=1, plus=1 + /// - min normal: minus=1, plus=2 + /// - normal: minus=1, plus=1 + /// In every branch `minus == 1` and `plus in {1, 2}`. `mant` is positive + /// and bounded above by what the symbolic engine can track; `exp` spans + /// the range needed by both subnormal and normal paths. + fn arbitrary_small_decoded() -> Decoded { + let mant: u64 = kani::any(); + kani::assume(mant >= 2 && mant <= 0xFFFF); + let plus: u64 = kani::any(); + kani::assume(plus == 1 || plus == 2); + let minus: u64 = 1; + let exp: i16 = kani::any(); + kani::assume(exp >= -8 && exp <= 8); + let inclusive: bool = kani::any(); + Decoded { mant, minus, plus, exp, inclusive } + } + + /// Stub for `div_rem_upto_16`. The real helper conditionally subtracts + /// `scale8`, `scale4`, `scale2`, `scale` from `x` and adds 8/4/2/1 to a + /// running digit. Under havoc stubs of `Big::cmp` and `Big::sub`, the + /// four conditionals decorrelate and the algorithm-level invariant + /// `d < 10` (only reachable digit pattern given the loop precondition + /// `mant + plus <= scale * 10`) is lost. We re-encode the invariant + /// directly: havoc `x` (matches the post-subtract state) and return a + /// nondet digit constrained to `< 10`. This preserves *safety* — the + /// caller's `buf[i] = b'0' + d` write is bounded — without depending + /// on the bignum value semantics. + fn stub_div_rem_upto_16<'a>( + x: &'a mut Big, + _scale: &Big, + _scale2: &Big, + _scale4: &Big, + _scale8: &Big, + ) -> (u8, &'a mut Big) { + havoc_big(x); + let d: u8 = kani::any(); + kani::assume(d < 10); + (d, x) + } + + /// Verifies safety of `dragon::format_shortest` under documented + /// preconditions. + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(crate::num::bignum::Big32x40::mul_small, stub_mul_small)] + #[kani::stub(crate::num::bignum::Big32x40::mul_pow2, stub_mul_pow2)] + #[kani::stub(crate::num::bignum::Big32x40::mul_pow5, stub_mul_pow5)] + #[kani::stub(crate::num::bignum::Big32x40::mul_digits, stub_mul_digits)] + #[kani::stub(crate::num::bignum::Big32x40::div_rem_small, stub_div_rem_small)] + #[kani::stub(crate::num::bignum::Big32x40::add, stub_add)] + #[kani::stub(crate::num::bignum::Big32x40::add_small, stub_add_small)] + #[kani::stub(crate::num::bignum::Big32x40::sub, stub_sub)] + #[kani::stub(crate::num::bignum::Big32x40::cmp, stub_big_cmp)] + #[kani::stub(crate::num::bignum::Big32x40::eq, stub_big_eq)] + #[kani::stub(crate::num::flt2dec::round_up, stub_round_up)] + #[kani::stub(crate::num::bignum::Big32x40::bit_length, stub_bit_length)] + #[kani::stub(crate::num::bignum::Big32x40::is_zero, stub_is_zero)] + #[kani::stub(crate::num::flt2dec::strategy::dragon::div_rem_upto_16, stub_div_rem_upto_16)] + fn check_format_shortest_safety() { + unsafe { CMP_CALLS = 0; } + let d = arbitrary_small_decoded(); + // One slot beyond MAX_SIG_DIGITS for the round-up extension at the + // end of `format_shortest`: under havoc stubs of `Big::cmp` the loop + // can fill all 17 slots before breaking, and the post-loop + // `round_up` may legitimately extend by one digit. The real + // algorithm's value semantics make this combination unreachable, + // but the stubs can't express that — so we provision the extra + // slot in the harness. Real callers in this module's public + // wrappers (`to_shortest_str` etc.) already supply larger buffers. + const HARNESS_BUF: usize = MAX_SIG_DIGITS + 1; + let mut buf: [MaybeUninit; HARNESS_BUF] = + [const { MaybeUninit::uninit() }; HARNESS_BUF]; + let _ = format_shortest(&d, &mut buf); + } + + /// Verifies safety of `dragon::format_exact` under documented + /// preconditions. + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(crate::num::bignum::Big32x40::mul_small, stub_mul_small)] + #[kani::stub(crate::num::bignum::Big32x40::mul_pow2, stub_mul_pow2)] + #[kani::stub(crate::num::bignum::Big32x40::mul_pow5, stub_mul_pow5)] + #[kani::stub(crate::num::bignum::Big32x40::mul_digits, stub_mul_digits)] + #[kani::stub(crate::num::bignum::Big32x40::div_rem_small, stub_div_rem_small)] + #[kani::stub(crate::num::bignum::Big32x40::add, stub_add)] + #[kani::stub(crate::num::bignum::Big32x40::add_small, stub_add_small)] + #[kani::stub(crate::num::bignum::Big32x40::sub, stub_sub)] + #[kani::stub(crate::num::bignum::Big32x40::cmp, stub_big_cmp)] + #[kani::stub(crate::num::bignum::Big32x40::eq, stub_big_eq)] + #[kani::stub(crate::num::flt2dec::round_up, stub_round_up)] + #[kani::stub(crate::num::bignum::Big32x40::bit_length, stub_bit_length)] + #[kani::stub(crate::num::bignum::Big32x40::is_zero, stub_is_zero)] + #[kani::stub(crate::num::flt2dec::strategy::dragon::div_rem_upto_16, stub_div_rem_upto_16)] + fn check_format_exact_safety() { + unsafe { CMP_CALLS = 0; } + let d = arbitrary_small_decoded(); + let limit: i16 = kani::any(); + kani::assume(limit >= -10 && limit <= 10); + const HARNESS_BUF: usize = MAX_SIG_DIGITS + 1; + let mut buf: [MaybeUninit; HARNESS_BUF] = + [const { MaybeUninit::uninit() }; HARNESS_BUF]; + let _ = format_exact(&d, &mut buf, limit); + } +} diff --git a/library/core/src/num/flt2dec/strategy/grisu.rs b/library/core/src/num/flt2dec/strategy/grisu.rs index d3bbb0934e0ff..7b804c7599cf4 100644 --- a/library/core/src/num/flt2dec/strategy/grisu.rs +++ b/library/core/src/num/flt2dec/strategy/grisu.rs @@ -5,6 +5,8 @@ //! [^1]: Florian Loitsch. 2010. Printing floating-point numbers quickly and //! accurately with integers. SIGPLAN Not. 45, 6 (June 2010), 233-243. +#[cfg(kani)] +use crate::kani; use crate::mem::MaybeUninit; use crate::num::diy_float::Fp; use crate::num::flt2dec::{Decoded, MAX_SIG_DIGITS, round_up}; @@ -162,6 +164,23 @@ pub fn max_pow10_no_more_than(x: u32) -> (u8, u32) { /// The shortest mode implementation for Grisu. /// /// It returns `None` when it would return an inexact representation otherwise. +/// +/// # Safety contract +/// +/// Preconditions documented here rather than enforced via `safety::requires` +/// so the function can be replaced via `#[kani::stub]` in the wrapper +/// harness. The same preconditions are enforced in the function body via +/// `assert!`, and the strategy harness assumes them via `kani::assume`. +/// When `model-checking/kani#4591` lands the doc-section can be replaced +/// by `#[safety::requires(...)]` attributes and the body asserts dropped. +/// +/// - `d.mant > 0` +/// - `d.minus > 0` +/// - `d.plus > 0` +/// - `d.mant.checked_add(d.plus).is_some()` +/// - `d.mant.checked_sub(d.minus).is_some()` +/// - `buf.len() >= MAX_SIG_DIGITS` +/// - `d.mant + d.plus < (1 << 61)` pub fn format_shortest_opt<'a>( d: &Decoded, buf: &'a mut [MaybeUninit], @@ -354,98 +373,50 @@ pub fn format_shortest_opt<'a>( // - `plus1v = (plus1 - v) * k` (and also, `threshold > plus1v` from prior invariants) // - `ten_kappa = 10^kappa * k` // - `ulp = 2^-e * k` - fn round_and_weed( - buf: &mut [u8], - exp: i16, - remainder: u64, - threshold: u64, - plus1v: u64, - ten_kappa: u64, - ulp: u64, - ) -> Option<(&[u8], i16)> { - assert!(!buf.is_empty()); +} - // produce two approximations to `v` (actually `plus1 - v`) within 1.5 ulps. - // the resulting representation should be the closest representation to both. - // - // here `plus1 - v` is used since calculations are done with respect to `plus1` - // in order to avoid overflow/underflow (hence the seemingly swapped names). - let plus1v_down = plus1v + ulp; // plus1 - (v - 1 ulp) - let plus1v_up = plus1v - ulp; // plus1 - (v + 1 ulp) +/// The rounding-and-weeding phase of Grisu shortest. Hoisted from a nested +/// fn so that Kani verification can stub it out independently — the safety +/// obligation of the surrounding `format_shortest_opt` does not depend on +/// the inner arithmetic of this function. +fn round_and_weed( + buf: &mut [u8], + exp: i16, + remainder: u64, + threshold: u64, + plus1v: u64, + ten_kappa: u64, + ulp: u64, +) -> Option<(&[u8], i16)> { + assert!(!buf.is_empty()); - // decrease the last digit and stop at the closest representation to `v + 1 ulp`. - let mut plus1w = remainder; // plus1w(n) = plus1 - w(n) - { - let last = buf.last_mut().unwrap(); - - // we work with the approximated digits `w(n)`, which is initially equal to `plus1 - - // plus1 % 10^kappa`. after running the loop body `n` times, `w(n) = plus1 - - // plus1 % 10^kappa - n * 10^kappa`. we set `plus1w(n) = plus1 - w(n) = - // plus1 % 10^kappa + n * 10^kappa` (thus `remainder = plus1w(0)`) to simplify checks. - // note that `plus1w(n)` is always increasing. - // - // we have three conditions to terminate. any of them will make the loop unable to - // proceed, but we then have at least one valid representation known to be closest to - // `v + 1 ulp` anyway. we will denote them as TC1 through TC3 for brevity. - // - // TC1: `w(n) <= v + 1 ulp`, i.e., this is the last repr that can be the closest one. - // this is equivalent to `plus1 - w(n) = plus1w(n) >= plus1 - (v + 1 ulp) = plus1v_up`. - // combined with TC2 (which checks if `w(n+1)` is valid), this prevents the possible - // overflow on the calculation of `plus1w(n)`. - // - // TC2: `w(n+1) < minus1`, i.e., the next repr definitely does not round to `v`. - // this is equivalent to `plus1 - w(n) + 10^kappa = plus1w(n) + 10^kappa > - // plus1 - minus1 = threshold`. the left hand side can overflow, but we know - // `threshold > plus1v`, so if TC1 is false, `threshold - plus1w(n) > - // threshold - (plus1v - 1 ulp) > 1 ulp` and we can safely test if - // `threshold - plus1w(n) < 10^kappa` instead. - // - // TC3: `abs(w(n) - (v + 1 ulp)) <= abs(w(n+1) - (v + 1 ulp))`, i.e., the next repr is - // no closer to `v + 1 ulp` than the current repr. given `z(n) = plus1v_up - plus1w(n)`, - // this becomes `abs(z(n)) <= abs(z(n+1))`. again assuming that TC1 is false, we have - // `z(n) > 0`. we have two cases to consider: - // - // - when `z(n+1) >= 0`: TC3 becomes `z(n) <= z(n+1)`. as `plus1w(n)` is increasing, - // `z(n)` should be decreasing and this is clearly false. - // - when `z(n+1) < 0`: - // - TC3a: the precondition is `plus1v_up < plus1w(n) + 10^kappa`. assuming TC2 is - // false, `threshold >= plus1w(n) + 10^kappa` so it cannot overflow. - // - TC3b: TC3 becomes `z(n) <= -z(n+1)`, i.e., `plus1v_up - plus1w(n) >= - // plus1w(n+1) - plus1v_up = plus1w(n) + 10^kappa - plus1v_up`. the negated TC1 - // gives `plus1v_up > plus1w(n)`, so it cannot overflow or underflow when - // combined with TC3a. - // - // consequently, we should stop when `TC1 || TC2 || (TC3a && TC3b)`. the following is - // equal to its inverse, `!TC1 && !TC2 && (!TC3a || !TC3b)`. - while plus1w < plus1v_up - && threshold - plus1w >= ten_kappa - && (plus1w + ten_kappa < plus1v_up - || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up) - { - *last -= 1; - debug_assert!(*last > b'0'); // the shortest repr cannot end with `0` - plus1w += ten_kappa; - } - } + let plus1v_down = plus1v + ulp; + let plus1v_up = plus1v - ulp; - // check if this representation is also the closest representation to `v - 1 ulp`. - // - // this is simply same to the terminating conditions for `v + 1 ulp`, with all `plus1v_up` - // replaced by `plus1v_down` instead. overflow analysis equally holds. - if plus1w < plus1v_down + let mut plus1w = remainder; + { + let last = buf.last_mut().unwrap(); + + while plus1w < plus1v_up && threshold - plus1w >= ten_kappa - && (plus1w + ten_kappa < plus1v_down - || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down) + && (plus1w + ten_kappa < plus1v_up + || plus1v_up - plus1w >= plus1w + ten_kappa - plus1v_up) { - return None; + *last -= 1; + debug_assert!(*last > b'0'); + plus1w += ten_kappa; } + } - // now we have the closest representation to `v` between `plus1` and `minus1`. - // this is too liberal, though, so we reject any `w(n)` not between `plus0` and `minus0`, - // i.e., `plus1 - plus1w(n) <= minus0` or `plus1 - plus1w(n) >= plus0`. we utilize the facts - // that `threshold = plus1 - minus1` and `plus1 - plus0 = minus0 - minus1 = 2 ulp`. - if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None } + if plus1w < plus1v_down + && threshold - plus1w >= ten_kappa + && (plus1w + ten_kappa < plus1v_down + || plus1v_down - plus1w >= plus1w + ten_kappa - plus1v_down) + { + return None; } + + if 2 * ulp <= plus1w && plus1w <= threshold - 4 * ulp { Some((buf, exp)) } else { None } } /// The shortest mode implementation for Grisu with Dragon fallback. @@ -468,6 +439,16 @@ pub fn format_shortest<'a>( /// The exact and fixed mode implementation for Grisu. /// /// It returns `None` when it would return an inexact representation otherwise. +/// +/// # Safety contract +/// +/// Preconditions documented here for the same reason as +/// `format_shortest_opt` (see `model-checking/kani#4591`); enforced via +/// `assert!` in the body and via `kani::assume` in the strategy harness. +/// +/// - `d.mant > 0` +/// - `d.mant < (1 << 61)` +/// - `!buf.is_empty()` pub fn format_exact_opt<'a>( d: &Decoded, buf: &'a mut [MaybeUninit], @@ -774,3 +755,287 @@ pub fn format_exact<'a>( None => fallback(d, buf, limit), } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::num::diy_float::Fp; + + // ===== Stubs for the heavy arithmetic helpers ===== + // + // CBMC OOMs when whole-program harnesses trace through the bignum-like + // u64/u128 arithmetic in `Fp::mul`, `Fp::normalize`, `cached_power` and + // `max_pow10_no_more_than`. We replace each with a nondeterministic + // implementation that returns a value satisfying the function's + // post-condition, so the formula only has to reason about the digit- + // emission control flow (which is where the safety properties live). + // + // Soundness sketch: the safety obligations of `format_*_opt` are + // 1) every `buf[i] = MaybeUninit::new(_)` write has `i < buf.len()`, + // 2) every `buf[..len].assume_init_*()` read covers only initialized + // bytes, + // 3) no shift `1 << e` exceeds the type width, + // 4) no arithmetic overflow / division-by-zero on the index/exponent + // bookkeeping. + // These follow from the *shape* of the algorithm's outputs (max_kappa in + // [0, 9], post-mul exponent in [-60, -32], etc.), not their exact value. + // Each stub returns a nondet value within the documented shape. + + // Tight stub postconditions derived from the Grisu3 paper (Loitsch, + // PLDI 2010) and the in-source invariants documented at lines 192-205 + // and 240-243 of this file. The bounds are necessary to prevent CBMC + // from exploring states the real algorithm never reaches (which would + // otherwise raise false-positive overflow / debug_assert failures). + + // Deterministic identity-on-`f` stub. The real `Fp::mul` computes + // `(self.f * other.f + (lo >> 63)) >> 64` — for a normalized `other.f` + // close to `2^63` this is approximately `self.f / 2`, but more + // importantly it is *monotonic in `self.f`*. With three successive + // mul calls (`plus`, `minus`, `v` against the same `cached`), the + // real algorithm relies on the order `minus.f < v.f < plus.f` being + // preserved post-mul. A nondet stub breaks that invariant, leading + // to spurious overflow when `format_shortest_opt` computes + // `plus1 - minus1` and `plus1 - v.f`. We model `mul` as the identity + // on `f` (which preserves ordering trivially) and as the exact + // exponent transform `a.e + b.e + 64`. + fn stub_fp_mul(a: Fp, b: Fp) -> Fp { + let e = a.e.wrapping_add(b.e).wrapping_add(64); + Fp { f: a.f, e } + } + + // `normalize` and `normalize_to` are just left-shifts driven by + // `leading_zeros`/`self.e - target_e`. They are cheap and have no + // u128 arithmetic, so we use the real implementations. Using the + // real impls also keeps the natural ordering `mant - minus < mant + // < mant + plus` of the pre-mul mantissas, which the deterministic + // mul stub then preserves through to the post-mul values. + + fn stub_cached_power(alpha: i16, gamma: i16) -> (i16, Fp) { + let k: i16 = kani::any(); + // Table spans 10^-308 .. 10^332 in steps; the index k fits easily + // in i16 with plenty of margin for `exp = max_kappa - k + 1`. + kani::assume(k >= -308 && k <= 332); + let f: u64 = kani::any(); + kani::assume(f >= 1u64 << 63); + let e: i16 = kani::any(); + // Table is built so that the returned `e` lies in `[alpha, gamma]` + // for any (alpha, gamma) the algorithm requests. + kani::assume(e >= alpha && e <= gamma); + (k, Fp { f, e }) + } + + fn stub_max_pow10_no_more_than(x: u32) -> (u8, u32) { + kani::assume(x > 0); + let kappa: u8 = kani::any(); + kani::assume(kappa <= 9); + // Concrete 10^kappa table so CBMC sees the exact reachable set + // rather than synthesising a symbolic `pow`. + let pow: u32 = match kappa { + 0 => 1, + 1 => 10, + 2 => 100, + 3 => 1_000, + 4 => 10_000, + 5 => 100_000, + 6 => 1_000_000, + 7 => 10_000_000, + 8 => 100_000_000, + _ => 1_000_000_000, + }; + // The defining inequality: 10^kappa <= x < 10^(kappa+1). The upper + // bound is vacuous for kappa == 9 since 10^10 > u32::MAX. + kani::assume(pow <= x); + if kappa < 9 { + kani::assume(x < pow.saturating_mul(10)); + } + (kappa, pow) + } + + // Hand-written stubs for the wrapper harnesses. (&[u8], i16) cannot + // implement kani::Arbitrary because the slice reference needs a real + // allocation; these stubs synthesise such a slice from the caller's + // buf, satisfying the lifetime and initialisation obligations of the + // wrapper's `assume_init_ref` chain. + fn stub_format_shortest_opt_wrapper<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + ) -> Option<(&'a [u8], i16)> { + let n: usize = kani::any(); + kani::assume(n <= buf.len()); + let mut k = 0; + while k < n { + buf[k] = MaybeUninit::new(b'0'); + k += 1; + } + if kani::any() { + let exp: i16 = kani::any(); + Some((unsafe { buf[..n].assume_init_ref() }, exp)) + } else { + None + } + } + + fn stub_format_exact_opt_wrapper<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + _limit: i16, + ) -> Option<(&'a [u8], i16)> { + let n: usize = kani::any(); + kani::assume(n <= buf.len()); + let mut k = 0; + while k < n { + buf[k] = MaybeUninit::new(b'0'); + k += 1; + } + if kani::any() { + let exp: i16 = kani::any(); + Some((unsafe { buf[..n].assume_init_ref() }, exp)) + } else { + None + } + } + + fn stub_dragon_format_shortest<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + ) -> (&'a [u8], i16) { + let n: usize = kani::any(); + kani::assume(n > 0 && n <= buf.len()); + let mut k = 0; + while k < n { + buf[k] = MaybeUninit::new(b'0'); + k += 1; + } + let exp: i16 = kani::any(); + (unsafe { buf[..n].assume_init_ref() }, exp) + } + + fn stub_dragon_format_exact<'a>( + _d: &Decoded, + buf: &'a mut [MaybeUninit], + _limit: i16, + ) -> (&'a [u8], i16) { + let n: usize = kani::any(); + kani::assume(n > 0 && n <= buf.len()); + let mut k = 0; + while k < n { + buf[k] = MaybeUninit::new(b'0'); + k += 1; + } + let exp: i16 = kani::any(); + (unsafe { buf[..n].assume_init_ref() }, exp) + } + + fn stub_round_and_weed<'a>( + buf: &'a mut [u8], + exp: i16, + _remainder: u64, + _threshold: u64, + _plus1v: u64, + _ten_kappa: u64, + _ulp: u64, + ) -> Option<(&'a [u8], i16)> { + // `round_and_weed` only mutates the last byte of `buf` and only by + // decrementing it, so the safety invariant "every byte of `buf` is + // an initialised u8" is preserved. The function returns either the + // input slice (with the same lifetime) or `None`. We model this + // shape directly without tracing the inner arithmetic. + if kani::any() { Some((buf, exp)) } else { None } + } + + fn stub_round_up(_d: &mut [u8]) -> Option { + // `round_up` walks `d` from the right, increments the last non-'9' + // digit, and fills trailing positions with '0'. Returns `Some(b'1')` + // iff the entire buffer was '9's (carry propagated past the front). + // We model it as nondet Some/None without touching `d`; this is safe + // because the safety harness checks only that the *caller* of + // `round_up` does not read past `len`, which `round_up` cannot + // affect. + if kani::any() { Some(b'1') } else { None } + } + + fn arbitrary_small_decoded() -> Decoded { + let mant: u64 = kani::any(); + let minus: u64 = kani::any(); + let plus: u64 = kani::any(); + let exp: i16 = kani::any(); + let inclusive: bool = kani::any(); + // Tight bounds: with the Loitsch-derived stubs the Fp::normalize / + // Fp::mul postconditions already abstract away the mantissa-value- + // specific behavior, so a 4-bit mantissa range is enough to + // exercise every reachable branch of the digit-emission loops. + kani::assume(mant >= 2 && mant <= 0xF); + kani::assume(minus >= 1 && minus < mant); + kani::assume(plus >= 1 && plus <= 0x7); + kani::assume(exp >= -2 && exp <= 2); + Decoded { mant, minus, plus, exp, inclusive } + } + + fn arbitrary_small_decoded_exact() -> Decoded { + let mant: u64 = kani::any(); + let exp: i16 = kani::any(); + let inclusive: bool = kani::any(); + kani::assume(mant >= 1 && mant <= 0xFF); + kani::assume(exp >= -4 && exp <= 4); + Decoded { mant, minus: 1, plus: 1, exp, inclusive } + } + + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(Fp::mul, stub_fp_mul)] + #[kani::stub(cached_power, stub_cached_power)] + #[kani::stub(max_pow10_no_more_than, stub_max_pow10_no_more_than)] + #[kani::stub(crate::num::flt2dec::round_up, stub_round_up)] + #[kani::stub(round_and_weed, stub_round_and_weed)] + fn check_format_shortest_opt_safety() { + let d = arbitrary_small_decoded(); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let _ = format_shortest_opt(&d, &mut buf); + } + + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(Fp::mul, stub_fp_mul)] + #[kani::stub(cached_power, stub_cached_power)] + #[kani::stub(max_pow10_no_more_than, stub_max_pow10_no_more_than)] + #[kani::stub(crate::num::flt2dec::round_up, stub_round_up)] + fn check_format_exact_opt_safety() { + let d = arbitrary_small_decoded_exact(); + let limit: i16 = kani::any(); + kani::assume(limit >= -10 && limit <= 10); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let _ = format_exact_opt(&d, &mut buf, limit); + } + + /// Verifies the unsafe lifetime-laundering reborrow in + /// `format_shortest` is sound. Both the Grisu attempt and the Dragon + /// fallback are stubbed; only the wrapper's own unsafe pattern is + /// exercised. + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(format_shortest_opt, stub_format_shortest_opt_wrapper)] + #[kani::stub(crate::num::flt2dec::strategy::dragon::format_shortest, stub_dragon_format_shortest)] + fn check_format_shortest_wrapper_safety() { + let d = arbitrary_small_decoded(); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let _ = format_shortest(&d, &mut buf); + } + + /// Same as above but for `format_exact`. + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub(format_exact_opt, stub_format_exact_opt_wrapper)] + #[kani::stub(crate::num::flt2dec::strategy::dragon::format_exact, stub_dragon_format_exact)] + fn check_format_exact_wrapper_safety() { + let d = arbitrary_small_decoded_exact(); + let limit: i16 = kani::any(); + kani::assume(limit >= -10 && limit <= 10); + let mut buf: [MaybeUninit; MAX_SIG_DIGITS] = + [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS]; + let _ = format_exact(&d, &mut buf, limit); + } +} diff --git a/scripts/check_rustc.sh b/scripts/check_rustc.sh index 66ff58fcaf4a1..91a8b56ee9887 100755 --- a/scripts/check_rustc.sh +++ b/scripts/check_rustc.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # Runs the Rust bootstrap script in order to ensure the changes to this repo # are compliant with the Rust repository tests. # diff --git a/scripts/find-contracts.sh b/scripts/find-contracts.sh index e682e9efb074e..38c40a2cb82a3 100755 --- a/scripts/find-contracts.sh +++ b/scripts/find-contracts.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # Script to find files with specific annotations and print contracts # containing those annotations up to a line with "fn" diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh index e11a012ed4556..689ba3f54d614 100755 --- a/scripts/run-goto-transcoder.sh +++ b/scripts/run-goto-transcoder.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -e diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index b996564989b1d..f0c659c44907e 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -e