Learn · All the Ways It Can Break

growing

Assumptions Spend the Proof Domain

Every assumption removes executions, and every loop needs enough unwinding to reach its exit.

formal-methods, kani, assumptions, loop-unwinding, vacuity, learn

You will constrain a symbolic length, retain evidence that the largest intended case is reachable, set and justify an unwind bound, and distinguish a successful assertion from a complete loop proof.

Model the valid call domain

The function indexes a four-element array, so len < values.len()= is a real precondition. It excludes invalid calls rather than inconvenient valid calls.

rust code/all-the-ways-it-can-break/numeric-kani/numeric.rs#bounded-loop numeric.rs The cover condition asks whether the full-length case remains reachable after assumptions. The unwind bound permits four iterations and the exit check.

Run it:

cargo kani --harness prefix_sum_matches_reference

Read both the verification summary and the cover result. The reference sum is not an independent implementation if it shares the same loop body, so the specimen uses a library iterator expression as a compact differential oracle.

An unwinding assertion checks that a bounded loop has been unrolled far enough for every admitted execution to exit. Kani enables these checks by default; see its attribute reference.

Vacuity — find the harness that proves too little.

Count the backedge, then demand completeness

An unwind number is not simply the largest input. It bounds loop unfolding in the verifier. Off-by-one behavior depends on the loop shape, so derive the number from the maximum backedge traversals and the final exit test, then let the unwinding assertion challenge the derivation.

Disabling unwinding checks changes the result: it can turn “all admitted loop executions exit within this bound” into “no failure appears in these prefixes.” That may be a useful bug-finding mode, but it is not the same proof and must be reported differently.

Assumptions need witnesses

List every assumption beside the public claim. Add cover! conditions for boundary partitions such as empty, full, minimum, maximum, and each protocol mode. A cover condition is reachability evidence, not a safety assertion; read its result explicitly. It helps detect an empty or accidentally narrowed domain, but it does not prove the covered state is correct.

At scale, reduce symbolic data only with a reason tied to the property. Replacing four arbitrary bytes with four zeros is not optimization; it deletes the value dimension of the theorem.

Lessons

assume removes executions from the proof domain.
Preconditions justify assumptions; verifier convenience does not.
Cover conditions expose unreachable intended partitions but do not prove safety.
Loop unwinding needs a completeness check as well as a numerical bound.
Disabling unwinding checks weakens the verdict and must change its wording.

Practice

Retrieval. Why does the four-iteration loop use unwind five?
Discrimination. What does assume(false); assert!(dangerous()) prove?
Transfer. Prove a bounded linear search returns only an index containing the key and covers both found and absent cases.

Worked answers

Four body executions are followed by one loop-condition evaluation that establishes exit.
Nothing about dangerous(); no execution reaches the assertion.
Use a fixed array, symbolic key and length, assume only the valid length bound, assert returned-index validity, and add separate cover conditions for Some and None.

References

Kani. Harness attributes. — proof, unwind, solver, and related bounds
Kani. Library reference. — assume and cover!

← A Harness Turns Values Symbolic A Contract Can Replace an Implementation →

kani::assume(condition) tells the verifier to ignore executions where the condition is false. That is exactly right for a function precondition and dangerous when used merely to make verification finish. assume(false) makes every later assertion vacuously safe because no execution reaches it. Loops add a different boundary. Kani unwinds them finitely and, by default, checks that the chosen bound reaches the loop exit for every admitted input. The four-element prefix-sum specimen uses an unwind value of five: up to four body executions plus the final condition check that exits the loop.