unwinding

[tjhance]

I want to address a few pain points in Verus today. I've brought these up before but am ready to take another crack at it.

• Most of Verus's messaging is that code is proved panic-free. This isn't entirely true, mostly because of the possibility of OOMs.
• We have a mechanism for specifying unwinding behavior, but it's mostly unused, and not tied to our messaging really at all.
• If you do want to use the unwind-specifications, it's often impossible, because of the possibility of OOMs.
• Verus doesn't have a mechanism for panics in general. We only allow specifying unwinds, but not panic aborts. (This is because unwinding has safety-relevant interactions with invariants.)

So in practice, people use no_unwind if they need to use invariants; otherwise, they use the default signature, which is unwind, so they aren't actually proving anything about unwinding, but in practice they're still 99%-proving unwinding anyway.

---

Regarding the unwinding and OOMs: it does seem like we need to assume that it is possible for allocating functions like Box::new to unwind. At least, the question isn't settled enough to definitely say that Box::new will never unwind. I asked on the rust zulip about this and got a few possibilities:

• set_alloc_error_hook (which is unstable)
• handle_alloc_error (stable) (requires a no_std environment. "questionably sound" according to ralf.)
• The docs for GlobalAlloc say that, "It’s undefined behavior if global allocators unwind. This restriction may be lifted in the future, but currently a panic from any of these functions may lead to memory unsafety." Apparently, if this restriction is actually lifted, it could mean unwinding from within user-defined global allocators.

Even so, a lot of users are working in systems where they have full control over their builds, so they could potentially ensure none of these things in the case. Since these setups are presumably rare, it's somewhat annoying that you have to deal with the possibility.

And of course, it's definitely possible for OOM to abort, anyway, even if it doesn't unwind.

---

We have the machinery we need to give precise specs for these situations. We just need to commit to a system that actually feels coherent and documentable. I think to start, we should acknowledge that: (i) most people want to prove panic-freedom, but this is mostly about their own errors (like index-out-of-bound errors or unwrap errors). (ii) most people are probably working in environments where some kind of panic or abort is the right behavior for OOM or other rare system events.

So: I think we need some kind of flag for these sorts of unusual events. I'll propose two to start:

• uninterp spec fn oom_event() -> bool
• uninterp spec fn rare_system_event() -> bool

The first would be for functions that might allocate, e.g.,

assume_specification<T> [Box<T>::new]()
   may_unwind when oom_event()

The second one is something of a catch-all for similar situations that might come up in the future. I have a feeling that people wrapping external code might want to use it.

Now, the default specification, instead of may_unwind will be:

may_unwind when oom_event()

In other words, the default specification will be, "this function won't unwind, unless OOM occurs", the theory being that most people would say panicking is the expected behavior in such a case.

Of course, if the user is a no-panic hardliner, they might use the spec no_unwind.

Some users looking for weaker guarantees could also assume the events away; this is riskier than using the unwind spec, since if they're wrong, they could get UB instead of just a panic. But a user might be able to assume the allocator doesn't unwind if they know that nobody's configuring an OOM hook, for example.

Finally, this would allow us to actually give a specification to panic!. It would have the spec of may_unwind, and people still wouldn't be able to call panic! unless they explicitly marked their own function may_unwind.

---

This is how I imagine the documentation looking: (this is a good practice that the rust team uses for RFCs, we should do it more)

proposed guide level explanation

Verus, by default, verifies that your code doesn't panic except as a result of OOM, a condition which many users will consider to be outside of their control. However, you can configure this however you want; you could set a more lenient specification that allows panicking under any condition you set, or you could set a stringent specification that forbids panicking entirely. The latter isn't practical in most situations, except may make sense in highly constrained environments where you're avoiding dynamic memory allocation entirely.

To be specific, Verus's "default" specification actually looks like this:

use vstd::error_conditions::*;

fn foo()
    may_abort when oom_event()
    may_unwind when oom_event() && unwindable_allocator()

In other words:

• The function can only abort when an OOM event occurs
• The function can only unwind when an OOM event occurs AND the allocator is set up to unwind on an OOM event.

FAQ:

I want Verus to check that my function won't panic for ANY reason, not even OOM.

You'll want to write a specification like this:

fn foo()
    no_abort
    no_unwind

I want Verus to let my function panic whenever I want.

fn foo()
    may_abort
    may_unwind
{
    panic!("hi");
}

I'm using assume_specification to wrap a third-party systems library. I think it can probably panic in some obscure error conditions, and I want to bubble up the panic. I still want to show that are no panics from MY code. Can I handle this in a principled way?

We recommend rare_system_event() for this purpose.

assume_specification[ open_device_driver ]()
    may_abort when rare_system_event()

Then you can declare that your own verified functions only panic when this rare event occurs:

fn foo()
    may_abort when rare_system_event()
{
    open_device_driver();
}

You can also declare your own error name:

uninterp spec fn driver_error_event() -> bool;

assume_specification[ open_device_driver ]()
    may_abort when driver_error_event()

I'd like to assume that the allocator never unwinds.

This is a reasonble assumption to make; today, this is only possible with certain unstable Rust features or no_std environments. If you control the entire build, you can make sure this assumption is upheld.

To declare the assumption to Verus, [... need to figure out how to deal with these kind of config assumptions]

[bsdinis]

A couple of loose thoughts on this. Generally really supportive of this, very big pain point on this. (From here on in, I'll talk about no_unwind, but everything applies the same with no_abort).

I wonder if we can have a single keyword unwinds_if <bool>, where by default it is assumed it unwinds (matching current behaviour).

I think the dual language problem is that client code should be able to assume/admit that a function call does not unwind.

Library code has an interest in being as accurate as possible (e.g., reporting something may unwind on OOM). However, application code may not really care about OOMs. For instance, something being pushed to a Vec, which is expected to be very small, and where (because we are the end application) we know panic == abort.