Decouple context management from while loops

[jonhnet]

Right now, while loops do some sort of "context management" that causes them to forget the entire context from outside the loop. In practice, this means the user must "rediscover" all these facts and write them down as invariants, even though they're typically immutable facts. This is really surprising, because "invariants", intuitively, are statements that don't change about variables that are changing.

I'm proposing this change because I just spent half an hour verifying a simple while loop. Most of the time was spent stumbling along "rediscovering" two facts that were in my requires and a third fact that I learned in a method call before the loop began. This behavior is extremely counterintuitive and wastes a lot of the scarcest resource: developer cycles.

The proposed benefit of the current policy is to crop context to enable more complicated methods to verify faster. Given that I've encountered this many times in functions that contain not much more than a single while loop, I'm paying all the price and getting none of the benefit. Right now we have an existing strategy to cull context manually: break a loop into another fn. Much of the cost of that strategy is "discovering" the invariants (now requires) of the inner fn. Why don't we pay-as-we-go?

Or if we want a lighter-weight way to crop context, let's add an explicit block scoped construct. So if I want today's behavior, I'd say:

fn foo()
requires a();
{
    len = get_len();
    clean_context
        requires a(),
           len == len_property(),
    {
        while i < len
        invariant forall |j| 0<=j<i ==> bar(j)
        {
             i += 1;
        }
    }
}

This decouples the mysterious behavior. The non-invariant declarations that are being explicitly punched through the context boundary are declared as requires for the clean_context block. And the invariants of the while loop are proper invariants about actual variables. Most importantly, it's a pay-as-you-go proof-performance-management tool which I will henceforth almost entirely simply ignore.

[tjhance]

This sounds like a good topic for the verus meeting tomorrow. I'm going to convert this to a discussion.

[Chris-Hawblitzel]

I'd prefer to wait on the discussion. I have an upcoming pull request on this.

[Chris-Hawblitzel]

#1010 is now merged, so you can put #![verifier::spinoff_loop(false)] at the root of the crate if you want the default to be not to spin off a query for while loops.

[parno]

Given #1010, should we close this discussion?

[utaal]

cc @jonhnet

[jonhnet]

When it was working it was an improvement, but I've experienced a few cases where I still have to put silly things into the while loop invariant list. It might be worth having @Chris-Hawblitzel look over my shoulder to see if I'm holding it wrong or if something else is still broken.