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

[qinheping]

Link to PR: #30 Link to challenge: 0005-linked-list.md

[bp7968h]

Hi @qinheping and @feliperodri , can I please give this a try, thank you.

[bp7968h]

Hi @carolynzech, @celinval, @qinheping, @feliperodri; I've been working on the challenge to verify the memory safety for this challenge. Below is the code I have written so far to prove that undefined behavior doesn't exists for clear function in LinkedList:

use kani;

#[cfg(kani)]
#[kani::proof]
fn unbounded_check_for_clear() {
    let size: i8 = kani::any();
    let mut size_copy: i8 = size.clone();
    let mut list: LinkedList<i8> = LinkedList::new();

    // create a arbitraty size linkedlist
    loop {
        if size_copy == 0 {
            break;
        }

        list.push_back(size_copy);

        match size_copy.is_positive() {
            true => size_copy -= 1,
            false => size_copy += 1,
        }
    }
    // check if the original kani produced size aligns with the linked list
    assert_eq!(list.contains(&size), true);
    assert_eq!(list.len(), size.abs().try_into().unwrap());

    // clear all the items
    list.clear();

    //check again
    assert_eq!(list.contains(&size), false);
    assert_eq!(list.len(), 0);
    assert!(list.is_empty());
}

I have some confusions:

• Whether my approach to proving memory safety is correct.
• Do we necessarily need to have contracts or proof harness are ok as well.
• Any suggestion on specifying preconditions.
• And am I going in the right direction, any suggestions or learning material to lookup as an example is very much appreciated.

thank you for your time and help.