Challenge 5: Verify functions iterating over inductive data type: linked_list

  • Status: Open
  • Tracking Issue: #29
  • Start date: 2024/07/01
  • End date: 2025/04/10
  • Reward: 5,000 USD

Goal

Verify the memory safety of alloc::collections::linked_list functions that iterate over its internal inductive-defined data type.

Details

The internal representations of linked_list are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions.

Success Criteria

The memory safety of the following public functions that iterating over the internal inductive data type must be verified:

FunctionLocation
clearalloc::collections::linked_list
containsalloc::collections::linked_list
split_offalloc::collections::linked_list
removealloc::collections::linked_list
retainalloc::collections::linked_list
retain_mutalloc::collections::linked_list
extract_ifalloc::collections::linked_list

The verification must be unbounded---it must hold for linked lists of arbitrary shape.

It is OK to assume that the generic type T of the proofs is primitive types, e.g., i32, u32, bool, etc.

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors ref:

  • Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
  • Reading from uninitialized memory except for padding or unions.
  • Mutating immutable bytes.
  • Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.