Skip to content

VeriFast solution for Challenge 5 (linked_list.rs) #238

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 12 commits into from
Aug 20, 2025
Merged

VeriFast solution for Challenge 5 (linked_list.rs) #238

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
10df662
Refinement-checked linked_list.rs proof
btj Jun 3, 2025
dee31cd
Patch the linked_list.rs proof
btj Jun 3, 2025
f2a3e42
Add a README giving a tour of the proof
btj Jun 5, 2025
171911b
README: Mention allocator unsoundness
btj Jul 5, 2025
31d55fc
Merge branch 'main' into verifast-linked-list
btj Jul 6, 2025
0bbc27c
README.md: Mention target architecture caveat
btj Jul 6, 2025
84296da
Merge branch 'main' into verifast-linked-list
btj Jul 23, 2025
b96760a
Merge branch 'main' into verifast-linked-list
btj Aug 6, 2025
e9fd0e4
README.md: VeriFast soundness includes std specs
btj Aug 7, 2025
b12bb9b
Merge branch 'main' into verifast-linked-list
btj Aug 9, 2025
a4b9577
Close Challenge 5
btj Aug 12, 2025
eac968c
Merge branch 'main' into verifast-linked-list
btj Aug 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/verifast-negative.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,16 +30,16 @@ jobs:
- name: Install VeriFast
run: |
cd ~
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
# https://github.com/verifast/verifast/attestations/4911733
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
tar xf verifast-25.02-linux.tar.gz
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
# https://github.com/verifast/verifast/attestations/8998468
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
tar xf verifast-25.07-linux.tar.gz

- name: Install the Rust toolchain used by VeriFast
run: rustup toolchain install nightly-2024-11-23
run: rustup toolchain install nightly-2025-04-09

- name: Run VeriFast Verification
run: |
export PATH=~/verifast-25.02/bin:$PATH
export PATH=~/verifast-25.07/bin:$PATH
cd verifast-proofs
bash check-verifast-proofs-negative.sh
12 changes: 6 additions & 6 deletions .github/workflows/verifast.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,17 +27,17 @@ jobs:
- name: Install VeriFast
run: |
cd ~
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
# https://github.com/verifast/verifast/attestations/4911733
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
tar xf verifast-25.02-linux.tar.gz
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
# https://github.com/verifast/verifast/attestations/8998468
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
tar xf verifast-25.07-linux.tar.gz

- name: Install the Rust toolchain used by VeriFast
run: rustup toolchain install nightly-2024-11-23
run: rustup toolchain install nightly-2025-04-09

- name: Run VeriFast Verification
run: |
export PATH=~/verifast-25.02/bin:$PATH
export PATH=~/verifast-25.07/bin:$PATH
cd verifast-proofs
bash check-verifast-proofs.sh

Expand Down
584 changes: 584 additions & 0 deletions verifast-proofs/alloc/collections/linked_list.rs/README.md
View file
Open in desktop

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion verifast-proofs/alloc/collections/linked_list.rs/original/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// verifast_options{skip_specless_fns}
// verifast_options{skip_specless_fns ignore_unwind_paths}

#![no_std]
#![allow(internal_features)]
Expand All @@ -12,6 +12,7 @@
#![feature(exact_size_is_empty)]
#![feature(hasher_prefixfree_extras)]
#![feature(box_into_inner)]
#![feature(try_trait_v2)]

#![stable(feature = "rust1", since = "1.0.0")]

Expand Down
3 changes: 2 additions & 1 deletion verifast-proofs/alloc/collections/linked_list.rs/verified/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// verifast_options{skip_specless_fns}
// verifast_options{skip_specless_fns ignore_unwind_paths}

#![no_std]
#![allow(internal_features)]
Expand All @@ -12,6 +12,7 @@
#![feature(exact_size_is_empty)]
#![feature(hasher_prefixfree_extras)]
#![feature(box_into_inner)]
#![feature(try_trait_v2)]

#![stable(feature = "rust1", since = "1.0.0")]

Expand Down
Loading
Loading