You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
changed the title [-]Challenge 19: Verify the safety of `slice` iter functions - part 2[/-][+]Challenge 19: Verify the safety of RawVec[/+]on Apr 4, 2025
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:
Activity
[-]Challenge 19: Verify the safety of `slice` iter functions - part 2[/-][+]Challenge 19: Verify the safety of RawVec[/+]btj commentedon Jun 20, 2025
I'm having a go at this challenge with VeriFast. So far, I've verified (with the caveats mentioned below)
RawVecInner::current_memory
andRawVecInner::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 areq
orens
clause.-ignore_unwind_paths
: This proof ignores code that is reachable only when unwinding.-allow_assume
: This proof uses a number ofassume
ghost statements andassume_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:
Fourthly, unlike foundational tools such as RefinedRust, VeriFast has not itself been verified, so there are undoubtedly also unknown unsoundnesses.
btj commentedon Jul 7, 2025
I've now also verified
RawVecInner::new_in
andRawVecInner::try_allocate_in
. To make these proofs go through, I had to fix a bug in the data structure invariant.