Add proof of LinkedList::unlink_node

Author: btj

.github/workflows/verifast.yml

@@ -27,16 +27,16 @@ jobs:
       - name: Install VeriFast
         run: |
           cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/24.12/verifast-24.12-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/3689894
-          echo '51bebf990f31666abcd3675000e7714ef79b417390e930953ef25383e8d59421  verifast-24.12-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-24.12-linux.tar.gz
+          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
 
       - name: Install the Rust toolchain used by VeriFast
         run: rustup toolchain install nightly-2024-11-23
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-24.12/bin:$PATH
+          export PATH=~/verifast-25.02/bin:$PATH
           cd verifast-proofs
           mysh check-verifast-proofs.mysh

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

@@ -0,0 +1,29 @@
+// verifast_options{skip_specless_fns}
+
+#![no_std]
+#![allow(internal_features)]
+#![allow(incomplete_features)]
+#![feature(allocator_api)]
+#![feature(staged_api)]
+#![feature(rustc_attrs)]
+#![feature(dropck_eyepatch)]
+#![feature(specialization)]
+#![feature(extend_one)]
+#![feature(exact_size_is_empty)]
+#![feature(hasher_prefixfree_extras)]
+#![feature(box_into_inner)]
+
+#![stable(feature = "rust1", since = "1.0.0")]
+
+extern crate alloc as std;
+
+#[stable(feature = "rust1", since = "1.0.0")]
+pub use std::alloc as alloc;
+#[stable(feature = "rust1", since = "1.0.0")]
+pub use std::boxed as boxed;
+
+trait SpecExtend<I> {
+    fn spec_extend(&mut self, iter: I);
+}
+
+pub mod linked_list;