Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Sign up
Appearance settings

Commit f66ba41

Browse files
btjfeliperodri
andauthored
VeriFast solution for challenge 19 (RawVec) (model-checking#422)
Adds a VeriFast solution for challenge 19 (RawVec). Note: this proof does not prove semantic well-typedness of the non-`unsafe` RawVecInner methods listed in the challenge, because they do not satisfy any meaningful kind of semantic well-typedness; see the discussion at model-checking#283. Resolves model-checking#283 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
1 parent 80da01f commit f66ba41

File tree

10 files changed

+3946
-3
lines changed

10 files changed

+3946
-3
lines changed

‎doc/src/challenges/0019-rawvec.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
1-
# Challenge 25: Verify the safety of `RawVec` functions
1+
# Challenge 19: Verify the safety of `RawVec` functions
22

3-
- **Status:** Open
3+
- **Status:** Resolved
44
- **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
55
- **Start date:** *2025年03月07日*
6-
- **End date:** *2025-10-17*
6+
- **End date:** *2025-08-12*
77
- **Reward:** *10000 USD*
8+
- **Contributors:** [Bart Jacobs](https://github.com/btj)
89

910
-------------------
1011

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# Partial verification of RawVec with VeriFast
2+
3+
With certain [caveats](#caveats), this proof proves functional correctness as well as [soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of RawVec associated functions `new_in`, `with_capacity_in`, `try_reserve`, `try_reserve_exact`, and `drop`, as well as functional correctness of RawVec associated functions `into_box`, `from_raw_parts_in`, `from_nonnull_in`, `ptr`, and `capacity`, RawVecInner associated functions `new_in`, `with_capacity_in`, `try_allocate_in`, `from_raw_parts_in`, `from_nonnull_in`, `ptr`, `non_null`, `capacity`, `current_memory`, `try_reserve`, `try_reserve_exact`, `needs_to_grow`, `set_ptr_and_cap`, `grow_amortized`, `grow_exact`, `shrink`, `shrink_unchecked`, and `deallocate`, and functions `capacity_overflow`, `new_cap`, `finish_grow`, `handle_error`, `alloc_guard`, and `layout_array`.
4+
5+
## Caveats
6+
7+
First of all, this proof was performed with the following VeriFast command-line flags:
8+
- `-skip_specless_fns`: VeriFast ignores the functions that do not have a `req` or `ens` clause.
9+
- `-ignore_unwind_paths`: This proof ignores code that is reachable only when unwinding.
10+
- `-allow_assume`: This proof uses a number of `assume` ghost statements and `assume_correct` clauses. These must be carefully audited.
11+
12+
Secondly, since VeriFast uses the `rustc` frontend, which assumes a particular target architecture, VeriFast's results hold only for the used Rust toolchain's target architecture. When VeriFast reports "0 errors found" for a Rust program, it always reports the targeted architecture as well (e.g. `0 errors found (2149 statements verified) (target: x86_64-unknown-linux-gnu (LP64))`).
13+
14+
Thirdly, VeriFast has a number of [known unsoundnesses](https://github.com/verifast/verifast/issues?q=is%3Aissue+is%3Aopen+label%3Aunsoundness) (reasons why VeriFast might in some cases incorrectly accept a program), including the following:
15+
- VeriFast does not yet fully verify compliance with Rust's [pointer aliasing rules](https://doc.rust-lang.org/reference/behavior-considered-undefined.html).
16+
- VeriFast does not yet properly verify compliance of custom type interpretations with Rust's [variance](https://doc.rust-lang.org/reference/subtyping.html#variance) rules.
17+
18+
Fourthly, unlike foundational tools such as [RefinedRust](https://plv.mpi-sws.org/refinedrust/), VeriFast has not itself been verified, so there are undoubtedly also unknown unsoundnesses. Such unsoundnesses might exist in VeriFast's [symbolic execution engine](https://github.com/model-checking/verify-rust-std/issues/213#issuecomment-2531006855) [itself](https://github.com/model-checking/verify-rust-std/issues/213#issuecomment-2534922580) or in its [prelude](https://github.com/verifast/verifast/tree/master/bin/rust) (definitions and axioms automatically imported at the start of every verification run) or in the [specifications](https://github.com/verifast/verifast/blob/master/bin/rust/std/lib.rsspec) it uses for the Rust standard library functions called by the program being verified.
Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// verifast_options{skip_specless_fns}
2+
3+
#![allow(dead_code)]
4+
#![no_std]
5+
#![allow(internal_features)]
6+
#![allow(incomplete_features)]
7+
#![feature(allocator_api)]
8+
#![feature(staged_api)]
9+
#![feature(rustc_attrs)]
10+
#![feature(dropck_eyepatch)]
11+
#![feature(specialization)]
12+
#![feature(extend_one)]
13+
#![feature(exact_size_is_empty)]
14+
#![feature(hasher_prefixfree_extras)]
15+
#![feature(box_into_inner)]
16+
#![feature(try_trait_v2)]
17+
#![feature(optimize_attribute)]
18+
#![feature(temporary_niche_types)]
19+
#![feature(ptr_internals)]
20+
#![feature(try_reserve_kind)]
21+
#![feature(ptr_alignment_type)]
22+
#![feature(sized_type_properties)]
23+
#![feature(std_internals)]
24+
#![feature(alloc_layout_extra)]
25+
#![feature(nonnull_provenance)]
26+
#![feature(panic_internals)]
27+
28+
#![stable(feature = "rust1", since = "1.0.0")]
29+
30+
extern crate alloc as std;
31+
32+
#[stable(feature = "rust1", since = "1.0.0")]
33+
pub use std::alloc as alloc;
34+
#[stable(feature = "rust1", since = "1.0.0")]
35+
pub use std::boxed as boxed;
36+
#[stable(feature = "rust1", since = "1.0.0")]
37+
pub use std::collections as collections;
38+
39+
pub mod raw_vec;

0 commit comments

Comments
(0)

AltStyle によって変換されたページ (->オリジナル) /