Using Verus from unverified client code

[tjhance]

Typically, we haven't thought much about the question of calling into verified code from trusted client code. The answer is usually just "well, the client has to obey the specifications, or there aren't any guarantees." In the Rust ecosystem, we can tell a slightly cleaner story.

Consider a function like:

fn vec_index_lookup_fast<T>(v: &Vec<T>, i: usize) -> &T {
    requires(0 <= i && i < v.len());
    // ... look up v[i] without doing a run-time bounds check on i
}

Naturally, such a function is easy to use in Verus, which will check that the precondition holds at each call-site. However, this code is not safe to call from vanilla rust code. Not only would it be logically nonsense to call vec_index_lookup_fast with an out-of-bounds index, it would be memory unsafe and undefined behavior. In normal Rust, this function would have to be marked unsafe, although here, that really means something more like “safety is dependent on the context of the caller code.“

Of course, that concept of context-dependent safety is exactly what the requires clause captures. In some sense, Rust's unsafe (the keyword on a fn declaration) is the same thing as having a precondition, except that the precondition is written in English. Conversely, Rust requires that any function without the unsafe keyword be memory safe if called from any context.

Proposal

When Verus exports code to be callable by vanilla Rust code, it should be marked unsafe unless it meets all the following criteria:

• It has no preconditions
• It has no #[proof] arguments
• It would be allowed to panic, though
• All input parameters have the most general possible assumptions about them given their types, except we can assume that any input function parameters are also "safe" in the same manner:
  • Function arguments might unwind when called
  • However, we may assume that the function argument has a precondition allowing to be called with any arguments
• Maybe some others ...

Likewise, an exported trait will need to be marked unsafe unless it meets some carefully chosen criteria.

For this to really work, we do need to work how to handle encapsulated invariants, i.e., we need to be able to have a type T with some private, internal invariants, which clients of T don't have to know about as long as they don't break modularity. (Without that feature, the exported functions would have a bunch of boilerplate requires/ensures like foo.well_formed()). Also, such a feature would generally reduce boilerplate, although it's probably something for a separate discussion.

[tjhance]

One more quick note:

In our goals document we say that we "don't support unsafe code" but I feel this undersells Verus a little. It's more accurate to say Verus doesn't require you to write the unsafe keyword, but in fact Verus lets you easily write code that would have required the unsafe keyword in vanilla Rust.

The Rust "idiom" is that developers who use unsafe code should encapsulate the uses of unsafe and produce memory-safe APIs, and Verus will enable users to effectively do exactly that, except the code that would have been unsafe is now verified. So I think we should lean into idea.

[jaybosamiya]

While I do believe that the core discussion (around whether exported stuff should be marked unsafe or not) makes sense, I would argue that (quoting directly from the goals doc) "We do not intend to verify unsafe Rust code (instead, verification will rely on Rust's type safety, as ensured by Rust's type checker)" is indeed correct.

We do not support code with the unsafe keyword. Indeed, we can support some (or even many) cases where Rust would otherwise require unsafe but Verus's ability to verify code is not sufficient to handle all cases where Rust might need unsafe (eg: std::mem::transmute, raw pointer dereferences, etc.). Note that the use of unsafe in Rust is not just restricted to memory safety, but instead a non-trivial number of other invariants that are assumed to be held by rustc while compiling a program. If any of those assumptions are falsified, then overall type safety can break down, and since our verification assumes Rust's type checker is ensuring type safety, we cannot allow the use of the unsafe keyword.

[tjhance]

I think you might be underestimating the number of use-cases for unsafe that Verus will have equivalents for.

• We already have a small library (pervasive/ptr.rs) that wraps around a "raw pointer" and uses proof state to verify access. It is safe to use because of its preconditions, but if the same library were written in vanilla Rust, it would absolutely need unsafe annotations.
• I don't see why we can't verify transmute. The nontrivial other invariants of a type can be represented by #[proof] variables. To show that a transmute is allowed, the user would provide the proof state and show some kind of byte-representation-equivalence.

We don't need to claim that we verify all unsafe code. But I think claiming that "We do not intend to verify unsafe Rust code" misses the fact that we have verified algorithms which fundamentally require unsafe annotations if written in vanilla rust (like the node replication algorithm, or Rc).

[parno]

FWIW, historically, Dafny imposed many of the conditions in your Proposal list on Main; i.e., it wouldn't produce an executable unless the Dafny Main method met those conditions. A problem that arose was around ghost variables. For example, we might want to pass in a ghost variable representing the state of the file system at the start of the program, or the values of the command-line arguments, both in support of writing specs about the effect of the program w.r.t. those non-Dafny items. It may be that those things are more necessary at the entry point of a program than they are for a library exposing an API to a larger program though.

[tjhance]

I think there are a handful of issues here.

One, is the fact that the functions which are not memory-safe on all inputs should be marked unsafe by the established conventions of Rust.

We should respect that convention (I don't write the rules!) That means, if Verus is showing memory safety, but only subject to some precondition, the function should be marked unsafe.

Second, though, it is conceivable that a function be memory safe in all cases, but only "logically safe" in some cases. It's possible that developers would still like to expose the function as not-unsafe in that case. In that case, we should expect them to prove it memory safe. They can always do that, for example, by moving the "logical precondition" into an implication in the postcondition.

Third, there's the issue you brought up about external devices, and the question of what guarantees you provide in the case that the external device isn't what's expected. I think we should aim to provide memory safety still (veribetrkv's memory safety, for example, didn't depend on assumptions about the disk persisting data, because those assumptions were "outside the program logic"). This is a super important question, but I think this is part of a different discussion about the next iteration of the iron* methodology. (When I wrote this discussion up, I was thinking about "normal libraries")

[utaal]

This came up when @gz and @matthias-brun were integrating a verified code fragment (a page table implementation) in a larger unverified code base. The outer code base was calling the verified function with arguments that violated its precondition, causing what should have been an impossible stack overflow.

@gz suggests that it may be nice to mark some functions as "entry points" to the verified code base which would emit runtime assertions to check their pre-conditions. We probably cannot directly generate runtime checks for preconditions (they may contain quantifiers, and they often contain spec-only abstract data structures and functions).
The solution of making functions that don't satisfy the criteria listed by @tjhance unsafe to unverified code would probably have caught this. One can always write a wrapper function that adds runtime assertions for the preconditions (in the same spirit of what's suggested by #105 (reply in thread)); then that function would not need to be unsafe to unverified code anymore. We may want to add language facilities for this (possibly just by supporting the assert! macro in "entry point" functions that are allowed to panic).

[utaal]

We may want the feature that allows assert! in entry point functions to also be generally available as an optional weakening of the postcondition (that's infectious on all the callers): this code either panics or satisfies the postcondition; in some cases a user may decide they are okay with accepting a crash (but still be guaranteed no silent corruption) in case of e.g. an arithmetic overflow, in exchange for not having to set up invariants for value bounds.

[parno]

FWIW, Dafny includes a similar feature called expect.

In our case, if we use assert! for a similar feature, then I think your suggestion of it being "infectious on all the callers" is important, since I can easily imagine developers confusing assert!() with assert(). We can hope that the infectious annotations cause them to notice something odd going on if they meant to write assert().

[parno]

Looks like Dafny is also looking at automating wrappers for extern functions:
dafny-lang/dafny#2712

[utaal]

We are considering marking all functions with a precondition unsafe, so that unverified callers would need to wrap calls in unsafe. This would work, but it would mean that we lose the type system's ability to control use of unsafe features inside verified code. This may not matter, but we'd want to make sure that we don't plan to use it.

This is achievable with multiple versions of the verus! macro, but if we move to a single pass with a rust ghost code feature then we may not get to make changes using different "modes" of the macro.

[tchajed]

One reason why preconditions are needed is a struct invariant, which can be maintained in a completely safe way by ensuring it from each constructor and preserving it in each method, with the struct fields private. It would be nice if this pattern did not need to be marked unsafe. This would also be solved by exposing only a subset type that consists of the struct together with its invariant to the unverified code.

[Chris-Hawblitzel]

I'd like to be more precise about which functions are actually unsafe to call under which conditions. Consider the following scenario. Suppose someone has implemented a binary search function in safe Rust. Then they decide to verify the function by adding a requires that the input is sorted and that the search key is in the input, and they add an ensures that the return value is the index of the key. They don't change the executable implementation in any way. It would be unfortunate, at this point, to force the function to be marked unsafe just because it has now been formally verified.

At the very least, I'd like projects to be able to opt in to using unsafe-but-verified code. If a project doesn't use any unsafe library code, I think it should be able to export a safe API, even if that API has requires clauses.

But more generally, it would be good to have a story for when it's possible to wrap unsafe operations in a safe API, which is common in Rust. For example, we could have an unsafe Vec index operation that requires the index to be in bounds, which would be unsafe to export to unverified code. But if this is wrapped in code that performs a run-time check (e.g. it's in a loop from 0 to the Vec's len() - 1), then we should be able to encapsulate the unsafe operation in an unsafe block inside an otherwise safe function:

fn my_safe_fn(v: &Vec<u8>) {
    for i in 0..v.len() {
        unsafe { unsafe_vec_access(v, i); }
    }
}

We could say that since my_safe_fn has no requires clauses and it satisfies the preconditions of unsafe_vec_access, it can safely wrap the unsafe block, so that my_safe_fn doesn't need to be marked unsafe.

The difficulty is that functions may have additional requires clauses needed for correctness but not for type safety, and we somehow have to distinguish these:

fn my_safe_fn(v: &Vec<u8>, x: &OtherStuff)
    requires correctness_of(x)
{
    for i in 0..v.len() {
        unsafe { unsafe_vec_access(v, i); }
    }
}

Here's a proposal. Suppose we have an uninterpreted global boolean flag ONLY_CHECK_TYPE_SAFETY. Then we say that in order for a safe function to use an unsafe block, the safe function's requires clauses have to be equivalent to true in the case where ONLY_CHECK_TYPE_SAFETY = true. (I.e. ONLY_CHECK_TYPE_SAFETY has to imply the requires clauses.) For example, this would satisfy this constraint:

fn my_safe_fn(v: &Vec<u8>, x: &OtherStuff)
    requires !ONLY_CHECK_TYPE_SAFETY ==> correctness_of(x)
{
    for i in 0..v.len() {
        unsafe { unsafe_vec_access(v, i); }
    }
}

I'd expect that most code would ignore ONLY_CHECK_TYPE_SAFETY, but for code that needs to wrap an unsafe block inside a safe function, it could be a way out.

[tjhance]

Under this proposal will you need to use an unsafe block to call something like pptr.take(...)?

[tjhance]

How does arithmetic overflow and stuff like that work? I assume it doesn't get checked in the "only check type safety" mode?

[tjhance]

The way I think about the problem is like this: for any given function, there's some bare minimum 'requires' clause that needs to be satisfied for the call to be type safe (and this condition is trivial for non-unsafe functions). Usually, we have other conditions in mind that are needed for further functional-correctness guarantees. In principle, you could write the specification like this:

fn stuff()
    requires bare_minimum_for_type_safety,
    ensures stuff_I_usually_expect ==> postcondition_I_care_about,

The problem with actual coding this way is that we usually want Verus to actually check that stuff_I_usually_expect actually holds, otherwise diagnostics get annoying when you don't know if you actually have the postcondition.

My read on Chris's proposal is that it solves this problem by letting you have two requires clauses which are "multiplexed" by the ONLY_CHECK_TYPE_SAFETY variable. That way you can toggle the requires clause between bare_minimum_for_type_safety and stuff_I_usually_expect via this global variable.

Let me propose something slightly different ... optional named requires clauses.

fn stuff()
    requires[hard] bare_minimum_for_type_safety,
    requires[soft] stuff_I_usually_expect
    ensures[soft] postcondition_I_care_about,

In principle you could use any names you want, but we'd have some idiomatic names for type-safety & functional-correctness, here hard and soft.

The idea is that if Verus is doing hard checking it's check the hard condition by default, and if it's doing soft checking it'd check the soft condition by default ... but you could alway toggle which one you use at the call-site. If you're doing type-safety reasoning, which requires some difficult functional-correctness reasoning from a subcomponent, you could e.g., opt-in to the 'soft' conditions.

[jaybosamiya]

I like the idea of the two kinds of requires clauses, with the minor comment that I would expect one to be a subset of the other (i.e., base_minimum_for... should always be checked), so it is less of a toggle between "hard" and "soft".

[jcp19]

Just a tiny remark, using terms like 'soft' and 'hard' may be misleading to new users who have used other verification tools in the past. In particular, they may assume requires[soft] to be a soft constraint and may confuse it with a recommends clause.

Also, riffing on @jaybosamiya's idea of having some sort of subset relation between the checks, we could have requires[recommended] (not suggesting this particular syntax, it is ugly) and have a third mode where all recommends clauses are also checked..

[tjhance]

It's been a while since I've written down my mental model for safe/unsafe, which I've refined a bit over the past year, so I think it's time for an update.

In Rust terms, an API is considered 'safe' if for any client code that calls into the API while satisfying rustc's type system and not using any additional 'unsafe' code, there won't be any UB. The key question is, how can we determine if an API to a Verus-verified codebase is safe?

To first approximation, the answer is: We can say that some API is safe if all of its preconditions are trivially 'true', and its implementation is verified with Verus.

One way to think about this is to imagine running Verus on the client code. Since the API only has trivially true preconditions,
and the client code doesn't have any postconditions or 'unsafe' features, Verus should pass automatically. (Here, I'm ignoring things that like integer overflow, which Verus does check but which don't matter for UB safety.) In other words, if we believe that Verus is correct, then we argue that an API is memory safe by making a meta-argument that Verus will pass when run on the client code. This is conceptually useful for making the characterization of a safe API precise.

Handling invariants

Now, one problem is that lots of types need internal invariants ('well-formedness predicates') which ordinarily would show up in the preconditions. I believe this will be resolved by implementing something similar to the type invariants discussed here: #962. This allows the verified code to rely on type invariants without having to add explicit preconditions. Even when we consider the possibility of temporarily-broken type invariants, the unverified client code will not be able to break them.

To be explicit, a function with this signature can be marked 'safe':

fn f()
  requires true,
  opens_invariants any,

(This happens to be the default signature.)

This is not the weakest possible signature (that would be opens_invariants none). However, the hypothetical client code is not able to able to open invariants, since that requires a special Verus feature, so Verus would always allow the client to call f. Under this perspective, open_local_invariant or open_atomic_invariant are 'conceptually unsafe', in the sense that we require Verus to check that they are used correctly. Again, the salient point is that the client code can't open an invariant.

Higher-order executable functions

Higher-order executable functions are a bit of a snag in this picture. Right now, the Verus model is to explicitly model the preconditions and postconditions as part of the FnOnce trait. Therefore, calling a function object would be 'unsafe' under this perspective, since the precondition might be nontrivial.

More explicitly, Verus treats the FnOnce trait as if it had the following precondition & postcondition:

pub trait FnOnce<Args: Tuple> {
    type Output;

    extern "rust-call" fn call_once(self, args: Args) -> (output: Self::Output)
        requires call_requires(self, args),
        opens_invariants any,
        ensures ...
}

Of course, in Rust, calling a function is safe. Functions marked 'unsafe fn' do not even implement the FnOnce trait. So the way we treat functions currently is at a mismatch with the idea that a safe function should be one with no preconditions.

Now, one option to resolve this would be to walk this back and remove the notion of call_requires. However, this would likely to be too limiting since there are plenty of applications for a 'requires' clause on a closure.

Another option would be to have a check that an API doesn't expose any function types with nontrivial preconditions. (It's actually pretty hard to expose a closure type. You either need to use 'dyn' or an existential type. Regardless, it can be done.) This is a bit of a wart, but I don't really see a reason it would be unsound. It would make things tricky if we ever support dyn.

Conclusion

Now that we have a decently concrete plan for type invariants, I think we can basically nail down what it means for a Verus-verified API to be safe. An API is safe if:

• Every non-unsafe function (except the builtin FnOnce::call) has a trivial 'requires' clause (with no restrictions on 'ensures' or 'opens_invariants')
• Any type with a type invariant has private fields
• Any closure types that are exposed have a trivial precondition