I recently read about the concept of library-level invariants and language-level invariants. It happens to me that there may be some gaps between the SAFETY requirements and how verification community writes their specifications.
In short, someone may think that SAFETY documentation serves as good sources to write soundness specifications of unsafe functions. However, the concept of library-level invariants make this wrong:
impl<T, A> Vec<T, A> {
pub fn split_off(&mut self, at: usize) -> Self {
// ...
let mut other = Vec::with_capacity_in(other_len, self.allocator().clone());
// Unsafely `set_len` and copy items to `other`.
unsafe {
self.set_len(at);
other.set_len(other_len);
ptr::copy_nonoverlapping(self.as_ptr().add(at), other.as_mut_ptr(), other.len());
}
other
}
}
This is the std implementation of Vec::split_off, but it violates the SAFETY documentation of Vec::set_len, which requires all new elements to be initialized. However, this is indeed sound, and should be verified. As a result, it's hard to write a good pre-condition for the Vec::set_len to make the above code verifiable and verified.
I wrote a note to fully explain my questions here, and I also come up with a solution for this problem.
Yes, this is a typical example of code that puts self into a state where its library invariant temporarily does not hold, but is still sound because it very carefully puts self back into a consistent state before passing control back to other code. And furthermore, this function lives in the same module as set_len, so it can make use of properties of set_len that are not stable guaranteed down downstream code.
The same code in a different crate would arguably be unsound, and require us to adjust the set_len documentation.
In my opinion, the way to solve that is to understand that when creating a module in Rust, you are creating distinct items as wrappers of the public items, you are not making those items visible publicly.
Foo, foo, Bar, and bar viewed from the private scope
Foo and foo viewed from the public scope (you can think of them as "transparent" or "inline" wrappers of their associated items above at a semantic level, you can't express that in Rust syntax)
When documenting a public API, you are documenting the public scope, not the private scope. This means that the private scope specification may be different from the public scope documentation, however the private spec should imply the public spec for the wrappers to be correct.
In the Vec case, we have that the public Vec is a refinement type of the private Vec (which is just a bunch of fields). In particular the safety invariant of Vec is the type invariant of the public Vec. The private Vec has a type invariant which is just the composition of the safety invariant of its fields, in particular ptr, len, and cap are unrelated (e.g. you don't need the first len items of ptr to satisfy their safety invariant).
In the Vec::set_len() case, the public spec would be something like:
Precondition:
self must satisfy the safety invariant of Vec<T>
new_len <= capacity
Elements between self.len() and new_len must satisfy the safety invariant for T
Postcondition:
self satisfies its safety invariant
self.len() == new_len
Elements between 0 and new_len were not modified
The private specification would be:
Precondition: nothing
Postcondition: If the precondition of the public spec holds, then the postcondition of the public spec holds (but this could be refined even more to match the implementation of set_len())
In my understanding, "being sound" is quite clear, which is related to the undefined behaviors listed in the rust nomicon (although it is not comprehensive, but that is off topic). If a different crate just set_len and copy_nonoverlapping, there is indeed no undefined behavior. I admit that this pattern is unsound-prone, but I do think it is sound.
I am not very aware of what's the possible adjustment to the set_len documentation. Could you clarify it a bit more?
Is this specification capable to compose the soundness verification of Vec::split_off? Since the pre-condition of the public spec is not held, the postcondition is a nop in my understanding?
We could document that it is okay to use set_len even if the elements at old_len..new_len are not initialized, as long as you don't call any Vec operations (except for a few that are fine) while the elements remain uninitialized.
OK I understand. Yes this is a feasible adjustment.
But even with this new SAFETY documentation, it is still hard to write a high-quality pre-condition for Vec::set_len, unless we move the initialization requirements to the pre-condition to other safe methods in Vec? If so, the SAFETY documentation is still inconsistent with soundness specifications.
It was a bit of a shortcut. Here's a better private specification:
Precondition: nothing
Postcondition:
self.len == new_len
self.ptr and self.cap are not modified
Elements between 0 and new_len are not modified (we could say 0 to cap if needed)
Note that you can always use the implementation of set_len() as its private specification (which kinds of amount of not doing modular verification, but for trivial functions like set_len() that's often the most appropriate choice).
If we insert a v.get(new_len - 1) between the set_len and copy_nonoverlapping, then it is definitely unsound. However, unless there is a pre-condition for the safe function Vec::get, this unsoundness can not be detected by verification
Also note that if your verification tool does not support private specs, you can usually modify your source code:
mod vec {
#[invariant = ...] // safety invariant
#[repr(transparent)] // this has limitations
pub struct Vec<T>(Vec_<T>);
struct Vec_<T> { ... } // no invariant
impl<T> Vec<T> {
#[requires(...)] #[ensures(...)] // public spec
#[inline(always)] // this may have limitations
pub unsafe fn set_len(&mut self, new_len: usize) {
// Proving this implementation is equivalent to proving that
// the private spec implies the public spec.
self.0.set_len(new_len)
}
}
impl<T> Vec_<T> {
#[ensures(...)] // private spec (no requires: safe function)
fn set_len(&mut self, new_len: usize) {
self.len = new_len;
}
}
}
There's 2 interpretations to your question with 2 different answers:
You try to call the public Vec::get(). In that case you need to build a public Vec from your private Vec_. For that you need to prove the Vec invariant, which you can't. So your verification tool will prevent you from calling the public Vec::get().
You try to call the private Vec_::get() which could be more lenient, like only requiring that particular element to satisfy its validity invariant (other elements may be invalid, and that element doesn't even need to be safe) besides being able to read that element through ptr (and possibly only that element). You still need to prove the element to satisfy the validity invariant, which you can't (unless the validity invariant is trivial, like it would be for Vec_<MaybeUninit<T>>::get()). So again your verification tool will prevent you from calling the private Vec::get().
OK, I think I understand. Then for internal Vec_, the safety-ness is completely reversed from the public Vec_. Since the public Vec_ has safe get and unsafe set_len, while the internal Vec_ has unsafe get (since we have pre-conditions) and safe set_len (as you posted in your snippet). This is quite interesting. Following your thoughts, when wrapping the internal methods with public methods, for unsafe wrapper set_len, the pre-condition flows to the type invariants of public Vec. For safe wrapper set_len, the unsafe internal set_len gets its pre-condition from the type invariants of public Vec. This does work. But does this mean that if we want to add soundness verification for std in the future, the whole logics need large rewrite? (like to add unsafe blocks at every Vec::get usage inside Vec) or we can add a third modifier lib_unsafe that means unsafe internal but safe external? This may make Rust more complicated and hard to learn.
Anyway, one little pity is that third-party crates can no longer use set_len-then-init approach due to the public pre-conditions.
I would build it by having some sort of predicate that represents a consistent, safe Vec -- the library invariant. set_len would have a spec which represents that after set_len was called, the Vec is not in a consistent state any more; its library invariant is temporarily violated. Therefore, the default precondition of get (that all arguments satisfy their library invariant) is not satisfied, and the verifier can reject this call to get without get having a special precondition.
(IOW: even safe functions have preconditions. The difference to unsafe functions is that the preconditions are entirely expressed by their argument types: the function is safe to call if all arguments satisfy their library invariant.)
Yes, this makes sense. But there is still a little bit inconsistency. Let's say the library has two invariants i1, i2, i3. Unsafe function foo1 breaks i1, but that states can be observed by safe function bar1, bar2 (like Vec::set_len() and Vec::len()), while unsafe function foo2 breaks i2, but that states can be observed by safe function bar3. Then in the type-invariant-based verification approach, both bar1, bar2, and bar3 have special pre-conditions, but the SAFETY documentation is in foo1 and foo2.
I'm not completely following what you said because some parts don't "type check" like there's no such thing as "public Vec_", it's either "public Vec" or "private Vec_". But after fixing such typos, then the underlying content sounds good to me.
No, we should definitely not rewrite code to verify it. The verification tools should be able to support existing code out of the box. There are many ways to do it, but the most simple one is:
A function call uses the private version if it can (essentially when the caller is in the private scope itself).
The tool should provide a way to distinguish public and private specs. Today it's usually private specs that are written. The public specs are inferred for safe functions based on types only (no logic spec). One could imagine #[pub_requires(...)] #[pub_ensures(...)] for public specs. Private specs need to imply public specs.
There's definitely a gap today regarding contracts, mostly because they focus on the standard library (in contrast to any crates) and on soundness (in contrast to any property like correctness). The first means they don't deal with dependencies since the standard library has none. The second means there's no notion of public contracts since they come from safety invariants (type interpretation).
Then for current contract design, is it able to prove the soundness of Vec::split_off? (BTW, I was thinking that safety contracts have been abandoned since I could not see any mention to contracts in 2026 project goals, I'm not expected to find it in Zulip chat )
Maybe the answer is that for calls inside a crate, you should verify them like the implementation of what was called was inlined into the caller, and only verify the publicly-exported things for soundness.
One thing that bothers me about the example in the OP is that the safety precondition violation is entirely unnecessary. You could just call other.set_len after the copy_nonoverlapping rather than before it.
In general, I think it's preferable, rather than trying to reason about weird things that the standard library does internally, to simply write it in a way that's easier to verify. Doing so is usually possible without losing performance, and it might potentially even make the code faster (because code that's easier for verification tools to reason about can also be code that's easier for compilers to reason about).
It crosses my mind that once we have &own/&move references, this code wouldn't even need "its own" unsafe, because it could be written efficiently in terms of other primitives, one which shortens a vector and produces an &own to the elements that fall off the end, and one which extends/collects a vector from an &own.
It also crosses my mind that it would be nice if implementing this as self.drain(q..).collect() would be as fast (in optimized builds) as the unsafe version, as such optimisations would be useful in speeding up things other than split_off, but that the unsafe version would nonetheless be useful for debug builds. (Currently, the drain+collect technique is slower.)
That's not a viable approach for most modular verification tools (probably all static ones). It might be fine for short functions (like I said for set_len where the specification is essentially the implementation) but not for complex functions.
Actually people usually do the opposite (in modular verification). They will give specifications to parts of a function (that would have made more sense to be its own function). See the trick in A case study with Aeneas and jxl-rs | Jonathan Protzenko
)