Challenge 19: Verify the safety of RawVec

[thanhnguyen-aws]

Runbook Link

https://model-checking.github.io/verify-rust-std/challenges/0019-rawvec.html

[btj]

I'm having a go at this challenge with VeriFast. So far, I've verified (with the caveats mentioned below) RawVecInner::current_memory and RawVecInner::deallocate, using this data structure invariant.

Caveats

First of all, I'm performing this proof with the following VeriFast command-line flags:

• -skip_specless_fns: VeriFast ignores the functions that do not have a req or ens clause.
• -ignore_unwind_paths: This proof ignores code that is reachable only when unwinding.
• -allow_assume: This proof uses a number of assume ghost statements and assume_correct clauses. These must be carefully audited.

Secondly, since VeriFast uses the rustc frontend, which assumes a particular target architecture, VeriFast's results apply only to the target architecture of the Rust toolchain being used.

Thirdly, VeriFast has a number of known unsoundnesses (reasons why VeriFast might in some cases incorrectly accept a program), including the following:

• VeriFast does not yet fully verify compliance with Rust's pointer aliasing rules.
• VeriFast does not yet properly verify compliance of custom type interpretations with Rust's variance rules.
• The current specifications for the allocation APIs do not prevent an allocated block from outliving its allocator. As a result, the proof does not apply if an allocator other than the global allocator is used.

Fourthly, unlike foundational tools such as RefinedRust, VeriFast has not itself been verified, so there are undoubtedly also unknown unsoundnesses.

[btj]

I've now also verified RawVecInner::new_in and RawVecInner::try_allocate_in. To make these proofs go through, I had to fix a bug in the data structure invariant.

[btj]

I've now verified all functions listed in the challenge against functional correctness specifications that should be sufficient for verifying Vec and VecDeque on top of them. I also verified semantic well-typedness of the non-unsafe RawVec methods listed in the challenge.

I did not, however, verify any kind of semantic well-typedness for the non-unsafe RawVecInner methods listed in the challenge. This is because it is not clear to me what kind of semantic well-typedness they would satisfy:

• RawVecInner::grow_exact causes UB if called with len and additional arguments such that len + additional is less than the current capacity. Indeed, in that case it calls Allocator::grow with a new_layout that is smaller than old_layout, which violates a safety precondition.
• RawVecInner::grow_exact and RawVecInner::grow_amortized both cause UB if called with an elem_layout different from the one used to initially allocate the buffer, because in that case grow is called with an old_layout that does not fit the allocated block, which violates a safety precondition.
• Since RawVecInner::try_reserve and RawVecInner::try_reserve_exact call RawVecInner::grow_amortized and RawVecInner::grow_exact, they also cause UB if called with an elem_layout different from the one used to initially allocate the buffer.
• Furthermore, these methods cause UB if called with an elem_layout where the size is not a multiple of the alignment. This is because Layout::repeat is used (in layout_array) to compute the allocation's layout when allocating, which includes padding to ensure alignment of array elements, but simple multiplication is used (in current_memory) to compute the old allocation's layout when resizing or deallocating, which would cause the layout used to resize or deallocate to not fit the allocated block, which violates a safety precondition.

@thanhnguyen-aws Please advise? I would suggest that the requirement to verify semantic well-typedness of the non-unsafe RawVecInner methods be dropped from the challenge. Or should I try to have unsafe keywords added to these methods upstream? (They are private to the module, so it's mostly an academic exercise, I guess?)

[btj]

I started working on a PR to add the missing unsafe modifiers to these RawVecInner methods.