VeriFast solution for Challenge 5 (linked_list.rs)

[btj]

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 and may also have unknown unsoundnesses, since it is a non-foundational tool (unlike e.g. RefinedRust.)

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.

[celinval]

Hi @btj, may I ask what was the motivation behind the diff? We do ask people to refrain from making changes to the existing code, so it would be nice to understand the motivation behind it. Thanks!

[btj]

Well, the challenge says "The solution cannot impact the runtime logic of the standard library" so I figured that changes that
'obviously' don't affect the generated machine code might be OK. Here are the most important changes I made and the motivation:

• Marked Node::new, Node::into_element, and pop_front_node as unsafe because for non-unsafe functions, VeriFast enforces RustBelt semantic well-typedness and for these non-public functions this would unnecessarily complicate the proof. As a result, I had to move some calls of these functions into unsafe blocks as well.

• Replaced a few instances where the code moved a Box's content out of the box with Box::into_inner. Examples: Node::into_element, remove_current, ExtractIf::next. The MIR generated for this code breaks the Box abstraction and would require a lot of special-case logic in VeriFast to handle.

• Made some implicit lifetime parameters explicit because I need to refer to them in the proof (e.g. pop_front_node, iter, cursor_front_mut, cursor_back_mut, extract_if)

• In pop_front_node, replaced

  let node = Box::from_raw_in(node.as_ptr(), &self.alloc);
  self.head = node.next;
  

  by

  self.head = (*node.as_ptr()).next;
  let node_ = Box::from_raw_in(node.as_ptr(), &self.alloc);
  

  because the former dereferences a Box; the latter is significantly simpler to reason about (but on closer thought, it might not be hard to add support for this).

• Moved some alloc.clone() calls into a separate clone_allocator function assumed to be correct because clone is a trait function, the call's semantic well-typedness is not sufficient to verify the call sites, and VeriFast does not yet support attaching special-case specs to particular trait implementations.

• Replaced some higher-order patterns (in particular: Option::map and Option::unwrap_or_else) by first-order equivalents; VeriFast does not yet support reasoning about closures.

• Enclosed some expressions in braces so as to be able to insert ghost commands

• Factored some subexpressions out into lets so as to be able to insert ghost commands

• Replaced some calls of NonNull::from, which VeriFast does not yet support, by NonNull::new_unchecked.

• Replaced some calls of mem::take by mem::replace because VeriFast does not yet support referring to a type's default value.

• In split_off, I made the following changes:

  • Replaced the use of iter() with manual iteration; this is much easier to reason about.
  • Replaced the for loops by loop loops; for now, VeriFast supports only loop loops.

• In LinkedList::drop:

  • Moved struct DropGuard and the accompanying impl block to the toplevel; VeriFast does not yet support local items.
  • Replaced the while loop by a loop loop.

• In next, replaced &*node.as_ptr() by node.as_ptr(), i.e. the subsequent few lines of code use a raw pointer instead of a shared reference. This is much easier to reason about because of the aliasing restrictions.

• Still in next, replaced self.len -= 1 by let len = self.len; self.len = len - 1, so that I could insert a ghost command between the load and the store.

• In move_next, replaced self.current = current.as_ref().next; by self.current = (*current.as_ptr()).next;, again to avoid the complexity of shared references. I made an analogous change in move_prev, remove_current, and ExtractIf::next.

• In move_prev, replaced list.len() by list.len. len() is a non-unsafe function and semantic well-typedness is not sufficient for this call site.

• I notice now that two as_list functions are not present in my solution but are present in main. But they are not present in the commit pointed to from the challenge. So apparently as_list was added after the challenge was created.

• In remove_current, replaced self.current? by a match so that I could insert ghost code onto the None path.

• In ExtractIf::next, I moved a FnMut call into a separate function that I assumed to be correct, because VeriFast does not yet support FnMut calls.

• In assert_covariance, moved some nested functions to the toplevel because VeriFast does not yet support nested functions.

• At the bottom of the file, made some impl lifetime parameters explicit because VeriFast currently requires an impl block's parameter list to be identical to the struct's parameter list.

Unless I overlooked something, the remaining changes have been eliminated by recent VeriFast improvements so they are no longer relevant. See the new version of the diff; this version of the proof was done with VeriFast 25.01, released today.