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

This PR adds a VeriFast proof that the LinkedList APIs enumerated in
Challenge 5 have the properties enumerated in the Challenge.

Note that VeriFast has some [known
unsoundnesses](https://github.com/verifast/verifast/blob/master/tests/rust/README.md)
and may also have unknown unsoundnesses, since it is a non-foundational
tool (unlike e.g. [RefinedRust](https://plv.mpi-sws.org/refinedrust/).)

*Addendum, 2025-01-23*: Note, in particular, that VeriFast 24.12 ignores
unwind paths, and, if the `-ignore_unwind_paths` flag is specified on
the command line, so does VeriFast 25.01. The 25.01 version of the proof
specifies `-ignore_unwind_paths`. So neither version of the proof
verifies unwind paths.

Note also that I made some minor changes to the code of linked_list.rs.
A diff is at
`verifast-proofs/alloc/collections/linked_list.code-changes.diff`.

Note, furthermore, that this proof uses a few `assume` statements.
Incorrect use of `assume` statements can of course lead to unsoundness.

This PR is based on the solution that I announced originally in the #29
thread; since then, I have resolved some VeriFast unsoundnesses and made
some other improvements (such as bringing down the verification time for
linked_list.rs significantly). I will be happy to produce a new VeriFast
release and either update this PR or submit a new one to use the new
VeriFast release if that is desired.

See some more details in the #29 thread.

Note: the VeriFast tool application issue (#213) is still open; it
should probably be resolved before this PR is accepted. I'm submitting
this PR at this point to inform the creation of the tool PR.

Resolves #29.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: btj

doc/src/challenges/0005-linked-list.md

@@ -1,10 +1,11 @@
 # Challenge 5: Verify functions iterating over inductive data type: `linked_list`
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *2024/07/01*
-- **End date:** *2025/04/10*
+- **End date:** *2025/08/12*
 - **Reward:** *5,000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

verifast-proofs/alloc/collections/linked_list.rs/README.md

@@ -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/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")]