Unwinding signature #

For any exec-mode function, it is possible to specify whether that function may unwind. The allowed forms of the signature are:

• No signature (default) - This means the function may unwind.
• no_unwind - This means the function may not unwind.
• no_unwind when {boolean expression in the input arguments} - If the given condition holds, then the call is guaranteed to not unwind.
  • no_unwind when true is equivalent to no_unwind
  • no_unwind when false is equivalent to the default behavior

By default, a function is allowed to unwind. (Note, though, that Verus does rule out common sources of unwinding, such as integer overflow, even when the function signature technically allows unwinding.)

Example #

Suppose you want to write a function which takes an index, and that you want to specify:

• The function will execute normally if the index is in-bounds
• The function will unwind otherwise

You might write it like this:

fn get(&self, i: usize) -> (res: T)
    ensures i < self.len() && res == self[i]
    no_unwind when i < self.len()

This effectively says:

• If i < self.len(), then the function will not unwind.
• If the function returns normally, then i < self.len() (equivalently, if i >= self.len(), then the function must unwind).

Restrictions with invariants #

You cannot unwind when an invariant is open. This restriction is necessary because an unwinding operation does not necessarily abort a program. Rust allows a program to "catch" an unwind, for example, or there might be other threads to continue execution. As a result, Verus cannot permit the program to exit an invariant-block early without restoring the invariant, not even for unwinding.

This restriction is what enables Verus to rule out exception safety violations.

Drops #

If you implement Drop for a type, you are required to give it a signature of no_unwind.