Extended static checking

[Chris-Hawblitzel]

At previous meetings, we've discussed having an extended static checking mode for Verus (by "extended static checking", I mean using formal verification techniques to check some properties of code, but not guaranteeing 100% soundness). The goal of this mode would be to make it easier to apply lightweight checking of some properties to existing Rust code without having to check all the properties that Verus currently checks. For example, users might want to check a few of their own hand-written preconditions, but not check arithmetic overflows or out-of-bounds array accesses. Such users might view errors about potential arithmetic overflows or potential out-of-bounds array accesses as spurious (false positives). Even if these users eventually decide that they want to prove the absence of arithmetic overflows and out-of-bounds array accesses, they might not want to worry about these properties immediately when starting to use Verus.

Here are some examples of checks that Verus performs that could be disabled or relaxed in an extended static checking mode:

• calls to external functions that lack a Verus declaration
• uses of other external items (traits, datatypes) without a Verus declaration
• preconditions of external functions that do have a Verus declaration (e.g. bounds checks of Vec accesses). In general, for such declarations, requires R, ensures E could be treated as requires true, ensures R ==> E to eliminate the check of R.
• arithmetic overflow and divide-by-zero
• uses of recursion and loops without decreases clauses (also: declarations of recursive types that violate strict positivity)
• verification of code generated by derive macros (for example, derive(Serialize) for serde)
• uses of unsupported features (for example, Verus currently rejects code that uses dbg! or println!)

I would guess that there are more such checks that could be added to this list.

I propose adding individual attributes to control each of these various checks, plus a few aggregate attributes to combine the individual attributes together in a convenient way. In order to control the individual attributes, I propose using something like Rust lint levels (allow, warn, deny, etc.), with each check being configured by one or more of the following levels:

• #[verifier::assume(...)
• #[verifier::assume_but_warn(...)
• #[verifier::allow(...)
• #[verifier::warn(...)
• #[verifier::warn_on_error(...), which would behave like recommends, warning only when there's a verification error in the function
• #[verifier::deny(...)

Here, assume is used for anything that could introduce unsoundness, while allow is used when soundness is maintained. Each check might only support a subset of the levels listed above. Here are some potential examples:

• verifier::assume(externals_available_without_declaration)
• verifier::assume_but_warn(externals_available_without_declaration)
• verifier::deny(externals_available_without_declaration)
• verifier::assume(externals_requires_as_ensures[vstd])
• verifier::assume(ignore_unsupported_features)
• verifier::assume(no_arith_overflow)
• verifier::allow(arith_overflow)
• verifier::warn(arith_overflow)
• verifier::warn_on_error(arith_overflow)
• verifier::deny(arith_overflow)

We could introduce aggregate configuration options as well. For example, verifier::assume(configure_for_minimal_checking) might expand to:

• verifier::assume(externals_available_without_declaration)
• verifier::assume(externals_requires_as_ensures[vstd])
• verifier::assume(ignore_unsupported_features)
• verifier::warn_on_error(arith_overflow)
• verifier::external_derive
• verifier::exec_allows_no_decreases_clause

As with existing configuration options like exec_allows_no_decreases_clause and loop_isolation, these could be configured for a whole crate, a whole module, a function, or perhaps individual expressions, and inner configurations (like on a function) would override outer configurations (like on a whole crate).

If people like this overall scheme with assume, allow, warn, etc., we could also consider renaming external_derive and exec_allows_no_decreases_clause to use this (for example, verifier::allow(exec_no_decreases_clause)).

The existing --no-cheating flag would check for uses of the options above. I don't know exactly what the policy should be, but certainly anything that assumes something potentially unsound should be prohibited by --no-cheating.

[jaybosamiya-ms]

My 2 cents:

I like that this uses allow, warn, etc. lint style things.

I would also suggest adding a the expect level that Rust allows too (equiv to allow but errors out if the lint was never triggered): this is super helpful when migrating things over to safer variants, since it allows the compiler to let you know when you can finally remove the allow that you had in your codebase before. I've found great help with this by placing expect for (as an example) clippy lints on regular Rust projects. Related: https://doc.rust-lang.org/rustc/lints/levels.html#expect

Also, I would suggest allowing reason = "..." similar to what Rust lint levels allow. Allowing this makes it easier to track things rather than via comments, since tooling can actually use this to show more precise suggestions (e.g., a project might say deny(whatever, reason = "we don't like whatever, use WHATEVER instead") and the error message can give a more precise error). Related: https://doc.rust-lang.org/rustc/lints/levels.html#:~:text=All%20lint%20attributes%20support%20an%20additional%20reason%20parameter

Finally, there is a 3rd point that I think is super helpful on real projects that Rust doesn't natively support but I've found great in practice: something like ratchet = N. So for example, #![allow(arith_overflow, ratchet = 15)] means that there are 15 places that Verus finds overflows in the codebase. It should error out if the number of times it finds it is not exactly 15. This allows the user to ratchet them down over time (or at least prevent them from introducing new overflows going forward). The reason you want it on exact count (rather than <= or something) is that you want to remind the user to reduce the ratchet count down too. Multiple of my projects implement this manually (e.g., slowly ratcheting down the number of transmutes in a very low-level library, or the number of globals in a project that we're trying to make usable in more places). Interestingly, expect then is just saying something like allow(.., ratchet > 0) (I am not suggesting introducing this >0 syntax though). Related reading about ratchet tests in general: https://qntm.org/ratchet

We don't need all of these in the first version of the implementation, but I'm just mentioning them because I like the idea of extended static checking, and giving people the way to actually support a controlled migration is a very useful idea. Things like expect and ratchets are very helpful in migrating over without a "stop the world" moment in the codebase.

[parno]

I think this generally sounds great, and I (like Jay) agree with integrating it in a lint-like style. I do think it will require some solid documentation to accompany it. For example, at first glance, I couldn't tell the difference between verifier::assume(no_arith_overflow) and verifier::allow(arith_overflow). Even now, my guess is that the former means assume(x + y <= u32::MAX), but I'm not sure which of the other possible meanings the latter activates.

we could also consider renaming external_derive and exec_allows_no_decreases_clause to use this

Yes, I think this would be a very good idea. Sticking with a consistent style is important as we add lots more configuration options.

I also like Jay's suggestion of supporting reason = "...".

[tjhance]

Summary of my perspective from the meeting last night

---

I think we can implement many of these in a principled way which retain concrete verification guarantees. Some of these can be viewed as relaxing certain restrictions that aren't required for Verus's proof system to remain sound.

For example, panics. Currently, x + y is implicitly specified as follows:

fn add(x: u8, y: u8) -> (z: u8)
    requires x + y <= 25
    ensures z == x + y;

But it could also be specified like this:

fn add(x: u8, y: u8) -> (z: u8)
    no_unwind when x + y <= 25
    ensures z == x.wrapping_add(y)

Likewise, Vec::index is specified like this:

fn index<T>(v: &Vec<T>, i: usize) -> (t: &T)
    requires 0 <= i < v.len()
    ensures t == v@[i]

But it could be specified like this:

fn index<T>(v: &Vec<T>, i: usize) -> (t: &T)
    no_unwind when 0 <= i < v.len()
    ensures 0 <= i < v.len() && t == v@[i]

So I propose that we implement these attributes by essentially switching the specifications of these common functions to the ones that allow (and specify) the panicking behavior. We can have a special attribute to tell Verus when the unwinding-variant of a function is sound. e.g.:

#[verifier::unwinds_when_requires_not_met]
fn index<T>(v: &Vec<T>, i: usize) -> (t: &T)
    requires 0 <= i < v.len()
    ensures t == v@[i]

With an attribute like allow(unwinding_stdlib_functions) or whatnot that tells Verus to use the unwinding-version of the spec for callers.

(Even for user crates, we could, in some cases, automatically apply the #[verifier::unwinds_when_requires_not_met] relaxation to user specs. Due to Rust metatheory, this is sound as long as the user code is entirely written in safe code (this also means no PPtr, PCell, etc.)

Guide level explanation I think we can explain the guarantees roughly like this:

By default, Verus prevents most (all?) sources of panics, e.g., when the developer writes x + y, Verus checks that x + y does not overflow. You can direct Verus to turn off these checks with the allow(arith_overflow) attribute.

Note that Verus will still consider all possible behaviors of a program in the presence of overflow and reason accordingly. For example, given a function with an arithmetic operation (x+y) and a postcondition, Verus will check that the postcondition holds even in executions where x+y overflows and returns a truncated integer.

Furthermore, the developer can always add no_unwind to a function to force Verus to check that the function cannot terminate in a panic. This will force Verus to ensure the function doesn't panic no matter the status of the lint levels in this crate or any dependent crates.

Hopefully this answers Byran's question about the difference between assume(no_arith_overflow) and allow(arith_overflow) under my interpretation. Specifically, if the user were to write:

fn test(x: u8, y: u8) {
    let z = x + y;
    assert(z == x + y);
}

Then this would:

• pass under assume(no_arith_overflow) (since it only considers executions where x+y does not overflow; i.e., x+y <= 255)
• fail under allow(arith_overflow) (since it considers, e.g., the execution wherex+y == 256 and z == 0, which can happen when Rust is run with the default release profile)

Naming

As I said, I think for attributes like 'allow(arith_overflow)' or 'allow(stdlib_panics)' or what have you, we don't need to treat these as soundness-violating at all.

We obviously need some kind of scary-sounding names for the soundness violating ones. "assume" is an obvious contendor, though I don't know if it actually makes all of the proposed attributes. Like, for assume_no_overflow, it makes sense, since this is applying a sweeping but still concrete and easy-to-state assumption to the code. But then we have ignore_unsupported_features which isn't even doing that, it's throwing the Rust semantics completely out the window. That's not to say I think it's a bad idea, just that I wouldn't know what to name it.

[tjhance]

(Even for user crates, we could, in some cases, automatically apply the #[verifier::unwinds_when_requires_not_met] relaxation to user specs. Due to Rust metatheory, this is sound as long as the user code is entirely written in safe code (this also means no PPtr, PCell, etc.)

I think this could potentially be a good way to handle derive code.