Partial functions / changes to recommends checking

[utaal]

From a discussion with @jonhnet, and from discussions at the [Verus all-hands] and with @Chris-Hawblitzel.

@jonhnet has reported frustration with the fact that the lack of hard requires on spec functions can hide issues/mistakes when writing them and till later, when one has to investigate a proof failure caused by a malformed spec function that could have been caught by a requires a-la Dafny.

At the retreat, we discussed a proposal of introducing partial functions (with requires) but only in user code (and not in the standard library). The primary concern here is "function coloring", where each function that calls a partial function must also be partial (modulo more complex designs that allow to total-ize a partial function). The other complication is FnSpecs (now likely renamed to something like spec_fn): should they also be partial? E.g. Seq::new_req(n, |i:int| requires 0<= i < n foo(i)).

At the retreat, we were wondering if the poor experience has been due to recommends being unreliable so far, in such a way that incentivizes ignoring the recommends failures.

We are considering defaulting to the behavior of spec(checked) (which checks recommends for the bodies of the spec functions) and allow users to opt-out for larger functions with e.g. spec(unchecked).

[utaal]

@Chris-Hawblitzel asked @jonhnet to experimentally add (checked) to all the functions in Verisplinter to evaluate the potential performance impact of implementing partial functions (requires) or an always-on recommends check.

These are @jonhnet's results:

I did a spec(checked) experiment on the VeruSplinter code base and discussed with @utaal.

High order bits. First, the latency cost:

unchecked: μ=7.84 σ=0.06
checked: μ=13.69 σ=0.14
cost: 5.9s 74.7%

Next, the usability cost: I set out to try fixing all 84 recommends failures that came up. I only made it a few fns in before realizing it was a fool's errand without ensures on spec fns. So I think I can't really lean into the world of spec(checked)-always (which I want!) until I have spec ensures -- and perhaps also a way to call a proof fn to complete a check in hairier cases.

[utaal]

Some new results from the experiment by @jonhnet:

Usability: When I started, we had 475 spec fns. I sedded them all to spec(checked) and propagated recommends as if they were requires. When it got frustrating, I gave up by commenting the (checked) out again. I finished with 26 such termination points remaining. IIRC, they're mostly cases where I needed to invoke some other lemma (what used to be an ensures on an underlying definition in Dafny). I did not bother trying to construct the recommends by contraption for those cases; it seemed like more boilerplate than it was worth.

The performance data is more interesting now that all the checks (those ~450 that survive) pass:
unchecked: μ=5.74 σ=0.14
checked: μ=5.74 σ=0.21
cost: -0.0s -0.0%

Wow! There's simply no evident cost to turning on spec(checked) always!

In collecting this data I noticed that my early measurements were going faster; I think it took a while to literally "warm up" the CPU and hit the thermal limits.

Conclusion: I am happy with the spec(checked) lifestyle. I think 'spec' should mean 'spec(checked)'.

We should add an attribute to locally disable checking, which I will use heavily until we have better support for spec-ensures and spec-lemma-calls, and which may retain occasional use beyond. (edited)

[utaal]

I re-ran things to see if the parallelism was potentially hiding the additional cost:

Pre-checked (commit 39101faa1afc79bffd0283bc9d1f0d7d748723f3):

$ verus --time --expand-errors --multiple-errors 1 --num-threads 1 src/bundle.rs

total-time:            8133 ms

verify-crate-time-breakdown
    total verify-time:           6525 ms   (1 threads)
    total air-time:               403 ms   (1 threads)
    total smt-time:              5066 ms   (1 threads)
        total smt-init:              1148 ms   (1 threads)
        total smt-run:               3918 ms   (1 threads)

After-checked (commit 4b39f8083e73ae82ed773efa8adb1a2c158e8038):

$ verus --time --expand-errors --multiple-errors 1 --num-threads 1 src/bundle.rs

total-time:            8457 ms

verify-crate-time-breakdown
    total verify-time:           6836 ms   (1 threads)
    total air-time:               436 ms   (1 threads)
    total smt-time:              5278 ms   (1 threads)
        total smt-init:              1567 ms   (1 threads)
        total smt-run:               3711 ms   (1 threads)

The times are very repeatable on my machine. The cost seems indeed small: a couple hundred ms at most (3%).

[utaal]

This is subsumed by the proposals in #764.