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, 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.

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