Refinement-checked linked_list.rs proof

Bumps VeriFast to 25.06

Author: btj

.github/workflows/verifast-negative.yml

@@ -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.06/verifast-25.06-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/7473259
+          echo '7081408d99853620a79fbfc3767f367d6f6ccfdaf26a63b1f30a382489aacb5a  verifast-25.06-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.06-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
         run: rustup toolchain install nightly-2024-11-23
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.06/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -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.06/verifast-25.06-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/7473259
+          echo '7081408d99853620a79fbfc3767f367d6f6ccfdaf26a63b1f30a382489aacb5a  verifast-25.06-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.06-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
         run: rustup toolchain install nightly-2024-11-23
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.06/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs.sh
 

verifast-proofs/alloc/collections/linked_list.rs/original/lib.rs

@@ -1,4 +1,4 @@
-// verifast_options{skip_specless_fns}
+// verifast_options{skip_specless_fns ignore_unwind_paths}
 
 #![no_std]
 #![allow(internal_features)]
@@ -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")]
 

verifast-proofs/alloc/collections/linked_list.rs/verified/lib.rs

@@ -1,4 +1,4 @@
-// verifast_options{skip_specless_fns}
+// verifast_options{skip_specless_fns ignore_unwind_paths}
 
 #![no_std]
 #![allow(internal_features)]
@@ -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")]