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.

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

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

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