unsafe Only Where a Switch or the Program Says SoStatus: Accepted
Date: October 22, 2026
Answers: when the Rust the compiler writes holds unsafe, and through what
Related: ADR-306 (a proved check is dropped at the build’s
request; D18, D19), ADR-314 D5 (a proved negation),
ADR-376 (unsafe { assume(…) }), ADR-218 (every
unsafe topic is a small crate of its own), ADR-377 (a vector
load proved inside)
A program asks for speed with remove-bounds-checks:on and
remove-overflow-checks:on; then a check the compiler proves is not written.
Where that check stood, the emitted Rust needs unsafe to say what the proof
says: an index without its test, a + that does not overflow, a shift whose
count is below the width. A program that does not ask keeps every check and
needs none. The rule was kept in the code, decision by decision, but written
nowhere as a rule, and two of the dropped checks did not follow it: a proved
shift wrote <T>::unchecked_shl into the program itself, without an
assertion and above the Rust version the emitted manifest promises, and a
proved negation wrote wrapping_neg, which tells the optimiser nothing.
Other languages: Rust’s -C overflow-checks and debug-assertions switch
checks off without changing what the source says, and its unchecked forms
are unsafe at the call. Swift’s -Ounchecked drops checks by a switch and
makes a failed one undefined behaviour. Ada/SPARK proves checks and removes
the proved ones with -gnatp-like switches; the source stays the same.
remove-* switch off, the emitted code holds only the unsafe the program writes.The program’s own unsafe is unsafe { assume(…) } (ADR-376, checked in
such a build) and a foreign call (extern). Nothing the compiler adds to make
a check go away is written in that build, so a program that does not ask for
speed has every check and no unsafe it did not write.
nikaia_std::proven.An index, a cut, a run read as an array, a slot written, a +, -, *, a
shift and a negation proved to stay inside their type are written as
unsafe { nikaia_std::proven::read(…) } (cut, array, slot, write,
add, sub, mul, shl, shr, neg), from the proven-index crate
(ADR-218). Each asserts the dropped check where debug assertions are on, and
tells the optimiser what the proof says where they are off; a wrong proof is
then undefined behaviour, as a believed assume is. The emitter writes no
unchecked_* and no get_unchecked of its own; the arithmetic inside a
believed assume is the program’s unsafe (ADR-376 D4), not a dropped check.
One program with each kind of dropped check is lowered with the switches off
(no unsafe at all) and on (each unsafe a nikaia_std::proven:: call).
A new kind of dropped check is added to it.
unsafe at all, the checks written as wrapping_* or masks
(ADR-306 D10 before D19): the optimiser then does not learn what the proof
says, and a proved index has no such form.unsafe written where it is needed, in whatever form (as before): two
kinds of check escaped the assertion and the version floor unnoticed.unsafe in every build, a check kept only where unproved: a program
that asks for no speed would carry unsafe it never asked for.unsafe; with them on, grep proven:: lists every dropped
check.proven-index holds every operation a proof licenses, each with its
argument in its README, under Miri.