unsafe { assume(claim) } - a Claim the Program Vouches For, a Fact Without a ProofStatus: Accepted
Date: October 20, 2026
Answers: how a program removes a check the compiler cannot prove, where the
person writing it knows the claim holds
Related: ADR-269 (an assert is a contract, proved where it
can be, checked where it cannot), ADR-306 (proved checks dropped
at the build’s request; an unchecked mode rejected),
ADR-361 (claims through loops), ADR-218 (unsafe
in a crate of its own), Part III 14.2 and 15.1
unsafe { assume(at < self.slots.len()) }
let s = self.slots[at] // no checkAn assert the compiler cannot prove is checked once where it stands; every
check after it that follows from it is gone. What is left is that one check.
Where the program’s author knows a claim holds - from an invariant over a whole
table, from the format of the input, from an argument the prover does not make -
the fastest programs in Rust (core::hint::assert_unchecked,
get_unchecked), C++ ([[assume]]) and C (__builtin_assume) drop that check
too, and the reader sees where.
assume(claim) inside unsafe is a fact from where it stands.assume(claim) and assume(claim; message: "…") are written only inside an
unsafe { … } block; outside one they are refused (NK1294). From where it
stands, the claim is a fact for the prover as a proved assert is: the checks
that follow from it are proved and dropped as the build’s optimization
switches say. The claim is read as an assert’s is (Part III 14.2): it changes
nothing, and a condition that could is NK1194. Data from outside the program
may be its subject, unlike an assert’s (NK1202): vouching for it is what
unsafe says.
Why. The person who knows the claim states it once, where the reader of the
program sees it, and the word unsafe marks the one place that has to be right.
A fact the prover takes is the same whether it was proved or vouched for, so
nothing else in the compiler changes.
In a build with remove-bounds-checks:off and remove-overflow-checks:off,
the default, an assume is checked as an assert is, and a false one stops
the program (A.2). In a build with either on, it is not checked: it lowers to
core::hint::assert_unchecked, and a false claim is undefined behaviour - the
program may read past the end of a buffer, or compute anything, without
stopping.
Why. The default build and every test then find a wrong assume the way
they find a wrong assert; only a build that asked for speed takes the risk,
and it asked for it twice, once in the source with unsafe and once in the
build. This is Rust’s assert_unchecked, checked in a debug build, with
Nikaia’s switches in place of debug assertions, which no Nikaia build has
(ADR-002 D5).
std assumes nothing, and every assume is listed.An assume in std’s Nikaia is refused (NK1295): std’s unsafe lives in
the small crates of ADR-218, each listed. nikaia check --asserts lists every
assume of the package, beside its asserts and the rules of its types.
Why. What a program relies on without proof has to be found in one place by
whoever reviews it, as SPARK lists every pragma Assume.
Where the claim is believed, its + - * are lowered as arithmetic that does
not overflow (Rust’s unchecked_add, unchecked_sub, unchecked_mul): a claim
whose arithmetic would overflow is false, and a believed false claim is
undefined behaviour already. Wrapping would make such a claim say something
else; widening would cost instructions the claim exists to save. A checked
claim keeps its checks.
-Ounchecked):
rejected by ADR-306 for changing what every program means unasked; an
assume changes it at one written place.assume without unsafe: nothing would mark the place that can break the
program silently.assert.assume would then be
found only as a corrupted result.trust, unsafe_trust_me): assume is the word SPARK,
Dafny, C++ and Rust’s assert_unchecked documentation use for the same thing.assume beside a call into C as
what unsafe is written for, and the code table gets NK1294 and NK1295.unsafe variant;
benches/brc measures both.