Issue #784: CI: extend the unsafe_crates job - Miri daily, Kani and fuzzing, failures reported and the checks documented

Open and answer this issue on GitHub.

ready · opened 2026-10-24 · updated 2026-10-24 · 0 comments

What this is about

Every unsafe the toolchain needs lives in a crate of its own under crates/unsafe/ (ADR-218): byte-blocks, c-boundary, c-text, checked-text, child-usage, crc32c, file-ring, low-bits, polled, proven-index, ref-or-box, shared-bytes, tether, text-key. Each one is its own workspace, and crates/nikaia-std forbids unsafe_code. So these crates are the only place where memory safety depends on hand-written reasoning instead of the compiler. Each crate’s README states that reasoning for every unsafe.

The owner’s goal is reliability that people outside the project can see. A check that runs only on someone’s machine does not count. It has to run in CI, regularly, and it has to be documented where readers look. The owner asked for Miri, and for fuzzing and Kani where they make sense and are possible, all built into the existing workflow rather than a second one.

Today

• The unsafe_crates job of .github/workflows/nikaia.yml runs scripts/check-unsafe-crates.sh on every crate:
  • fmt --check, test and clippy -D warnings, with and without --all-features;
  • cargo +nightly miri test --all-features under Stacked Borrows and again under Tree Borrows (nightly is installed in the job; ADR-001 D1’s one build toolchain stands, because Miri only checks the crates’ tests).
• It runs when scripts/ci-changes.sh sets unsafe: on a change to crates/unsafe/ or to the script, on workflow_dispatch, and on the weekly schedule (17 3 * * 1, which runs the whole workflow on main). On a push to develop it gates promote.
• The scheduled runs of 2026-10-05, -10-12 and -10-19 succeeded, and the one of 2026-09-28 was cancelled. A failed scheduled run notifies nobody.
• Fuzzing: nothing. There is no fuzz/ directory, and cargo-fuzz is not installed anywhere in CI.
• Kani: nothing. Kani is mentioned only in ADR-359 and ADR-361, as a prover compared with Nikaia’s own. No crate has a #[cfg(kani)] harness.
• Outside the repository’s ADRs and crate READMEs, nothing says which checks the unsafe code passes.

Why that is not enough

• Nightly Miri moves. It gains UB checks, and Tree Borrows changes. A crate that passed last week can fail today without any change of ours. A weekly run that tells nobody finds this late, or not at all.
• The tests only check the cases someone wrote. The arguments in the READMEs hold for every input. Fuzzing tries many more inputs than the tests do. Kani checks every input up to a bound.
• What is not written down is not visible. A reader of the website cannot tell that the unsafe code is checked, or how.

Decision (taken here)

• One workflow. Everything below goes into nikaia.yml, next to the existing job. There is no second workflow.
• Jobs: unsafe_crates stays as it is (Miri and the stable checks). Beside it come unsafe_kani and unsafe_fuzz, under the same condition (needs.changes.outputs.unsafe). All three gate promote on a push, as unsafe_crates does today.
• Daily: a second cron in the same workflow (e.g. 41 2 * * *). ci-changes.sh sees which cron fired (github.event.schedule) and turns on only unsafe for the daily one. The weekly one keeps turning on everything. So drift in nightly Miri or in Kani shows within a day, and the daily run costs only the three unsafe jobs.
• Two fuzz budgets. A run that gates promote has to mean the same on every run. On a push, each target runs a fixed number of runs (-runs=) with a fixed seed and no cached corpus. The daily run uses a larger budget, keeps the corpus between runs with actions/cache, and its findings do not wait for the next push. The budget is a number of runs, never a time.
• Miri: the existing script, plus -Zmiri-many-seeds=0..8 for the crates with threads or atomics (shared-bytes, tether). polled and file-ring stay outside Miri, as ADR-218 states (epoll and io_uring); neither fuzzing nor Kani can reach them either.
• Kani where the unsafe rests on arithmetic or a bit layout that a bounded check can cover completely. Not where it rests on the kernel or on C (c-boundary, child-usage, polled, file-ring), and not on the SIMD paths, which Kani’s models of the intrinsics do not cover reliably:
  • proven-index: under the stated precondition, the unchecked index or arithmetic gives the same result as the checked one and is never UB. One harness per operation and integer width.
  • low-bits: the bzhi path equals x & ((1 << n) - 1) for every x and every n. If Kani does not model bzhi, check the portable path and keep the equality as a fuzz target.
  • ref-or-box: building one and reading it back returns the same variant and the same address, for both sides. Option<RefOrBox<A, B>> is one word.
  • checked-text: for every byte string up to a bound (e.g. 8 bytes), it accepts exactly when std::str::from_utf8 does, and the text read back equals the input.
  • text-key: the bytes read back are the key’s own, for each key type the crate knows.
• Fuzzing with cargo-fuzz (libFuzzer, nightly), compared with a safe reference wherever one exists:
  • checked-text: arbitrary bytes, compared with std::str::from_utf8;
  • c-text: arbitrary bytes with a zero byte appended; the length and the bytes read back must equal the input up to the first zero;
  • byte-blocks: arbitrary 64-byte blocks and sets, the vector path against a scalar loop;
  • crc32c: arbitrary words, the crc32 path against the table-driven path;
  • low-bits: arbitrary (x, n), against the mask;
  • shared-bytes and tether: an arbitrary sequence of operations (make, clone, slice, drop), checked against a plain Vec<u8> model.
• A failed scheduled run is reported. It opens one tracking issue, or comments on it if it is already open. The next green scheduled run closes it.
• Documented for readers outside the project. A page lists each unsafe crate and which checks run on it in CI: Miri under Stacked Borrows and Tree Borrows, Kani with its bound, the fuzz targets with their budgets. It gives the reason for each check that is left out. It links the latest run. ADR-218 says the same in short.
• Not here: sanitizers and cargo deny. They can get their own issue if someone wants them.

To build

1. Daily cron:
   • add 41 2 * * * beside 17 3 * * 1 in nikaia.yml;
   • pass github.event.schedule to ci-changes.sh: the daily cron sets only unsafe=true, the weekly one keeps all;
   • print rustc +nightly -V in the log of unsafe_crates, so a drift can be dated.
   • Test: a workflow_dispatch still turns everything on. Check the cron branch of ci-changes.sh locally by setting the variable by hand.
2. Miri seeds: in check-unsafe-crates.sh, add -Zmiri-many-seeds=0..8 for shared-bytes and tether, under both aliasing models.
   • Test: the script passes locally and in unsafe_crates.
3. Kani:
   • write the harnesses as #[cfg(kani)] mod proofs in each crate named above;
   • declare cfg(kani) in each crate’s [lints.rust] unexpected_cfgs, so clippy stays clean;
   • add --kani to check-unsafe-crates.sh, so a contributor runs it the same way as CI;
   • add the job unsafe_kani to nikaia.yml, with the Kani version pinned (cargo install --locked kani-verifier@<v>, cargo kani setup), and add it to promote’s needs;
   • state the bound of each harness in the crate’s README, next to the argument it checks.
   • Test: each harness passes. Weaken one precondition in a scratch change and see Kani produce a counterexample; do not commit that change.
4. Fuzzing:
   • write the targets in crates/unsafe/<crate>/fuzz/, a crate of its own outside the crate’s workspace, so the workspace and its Cargo.lock stay as they are;
   • add --fuzz RUNS to check-unsafe-crates.sh;
   • add the job unsafe_fuzz to nikaia.yml and to promote’s needs. On a push it runs -runs=100000 -seed=1 with no cache. On the daily cron it runs -runs=1000000 with the corpus cached per target. A crash uploads the reproducing input as an artifact.
   • Test: each target runs its budget clean. Break the reference comparison in a scratch change and see the target find it; do not commit that change.
5. Failure reporting: a step at the end of the scheduled run (issues: write, if: github.event_name == 'schedule'). On a failure in any job, it opens “unsafe crates: scheduled check failing” (label ready), or comments on it if it is already open, with the run link, the failing job and the nightly version. On a green run, it closes that issue.
   • Test: a workflow_dispatch input that forces a failure opens the issue, and the next green run closes it.
6. Documentation:
   • a page in guide/ (and on the website, where the guide is published), “How the unsafe code is checked”, with the per-crate table from the decision above and a link to the workflow’s runs;
   • a link to it from README.md;
   • in ADR-218, in D2 or the consequences, name Kani and fuzzing beside Miri, and say which crates each one covers and why the others are left out;
   • in scripts/ci-changes.sh, say what the daily cron turns on.
7. No version raise: this is CI, crates outside nikaia-std, the guide and a note in an ADR that decides nothing new for the language.

Back to Open Issues