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.

[carolynzech]

Hi @bp7968h. We're glad you're excited about the challenge! Kani is a bounded model checker, while this challenge explicitly requires unbounded proofs. Kani has been working on extending our support for unbounded proofs with loop invariants, but we do not yet have support for inductive data structures.
To complete this challenge, you would need to use a proof tool that can handle unbounded proofs. Note, however, that said tool would need to first be accepted as a valid verification tool through our tool application. To get started, I would recommend looking into other Rust verification tools to get a sense of which verification tool might help complete this challenge.

[btj]

I'm having a go at this with VeriFast: linked_list.rs Just got started; only verified push_front so far.

[btj]

Update: I am making good progress on this challenge. So far, I have verified soundness of LinkedList::{new, push_front, pop_front, drop, clear, iter, cursor_front_mut, cursor_back_mut}, Iter::next, CursorMut::{move_next, move_prev, current, remove_current}. Challenge function contains has no unsafe blocks and accesses the data structure only through verified functions iter and next, so its safety follows from the soundness of the verified functions. Challenge functions remove, retain, and retain_mut have no unsafe blocks and access the data structure only through verified functions cursor_front_mut, cursor_back_mut, move_next, move_prev, current, and remove_current. TODO: verify split_off and extract_if, as well as some proof obligations about the type interpretations. Note: I changed the code slightly in a few places:

• Commented out the stability attributes, because rustc (which VeriFast uses internally) errors out on them.
• Replaced a few instances of box dereferencing magic, which is not yet supported by VeriFast, with Box::into_inner
• Replaced some higher-order patterns (in particular: Option::map) 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

[btj]

Update: I now verified split_off and extract_if as well. (This again required a few changes to the code, such as wrapping the FnMut call in an unverified helper function (because VeriFast does not yet support trait associated types).) Therefore, I have now verified safety of all functions required by the challenge (as well as their transitive callees). I am now proving some properties of the type interpretations, such as compliance with the Send trait. Then I need to do a bit of work on VeriFast so that it (more) properly checks the "not mutating immutable bytes" requirement. (The other requirements (no accesses of dangling or misaligned pointers, no reading from uninitialized memory, no producing invalid values) should already be taken care of (with the usual caveat that VeriFast is non-foundational so there may be unknown bugs that cause unsoundness).)

[btj]

Update: VeriFast now verifies that non-mut let bindings are not mutated, and that memory to which a shared reference exists is not mutated. I believe that linked_list.rs, verified with the newly released VeriFast 24.12, is a solution to this challenge, in that this proof verifies the stated properties (modulo any unknown unsoundnesses in the tool) of the stated code (with a few very minor modifications applied).

I guess the next step is to get VeriFast accepted as a tool. See a completed tool application form at verifast-tool-application.txt.

[carolynzech]

@btj Thanks for all of your work so far! Could you please open an issue with your tool application instead? It's easier for us to provide feedback that way. See #108 for an example.

[btj]

OK; I opened #213 .