completed programs roughly from 70 to 80

tasks/human_eval_007.rs

@@ -9,7 +9,101 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>)
+    ensures
+        [email protected]() <= [email protected](),
+        forall|s: &str| [email protected](s) ==> [email protected](s),
+        forall|s: &str|
+            [email protected](s) ==> exists|i: int|
+                0 <= i <= [email protected]() - [email protected]() && [email protected](
+                    i,
+                    #[trigger] (i + [email protected]()),
+                ) == substring@,
+{
+    let mut res = Vec::new();
+    let mut i: usize = 0;
+
+    for i in 0..strings.len()
+        invariant
+            0 <= i && i <= [email protected](),
+            [email protected]() <= i,
+            forall|s: &str| [email protected](s) ==> [email protected](s),
+            forall|s: &str|
+                [email protected](s) ==> exists|i: int|
+                    0 <= i <= [email protected]() - [email protected]() && [email protected](
+                        i,
+                        #[trigger] (i + [email protected]()),
+                    ) == substring@,
+    {
+        if check_substring(strings[i], substring) {
+            let ghost res_old = res;
+            res.push(strings[i]);
+
+            assert([email protected]() == strings[i as int]);
+            assert([email protected]_last() == res_old@);
+            assert(forall|s: &str|
+                [email protected](s) <==> [email protected](s) || s == strings[i as int]);
+        }
+    }
+    res
+}
+
+fn check_substring(s: &str, sub: &str) -> (result: bool)
+    ensures
+        result <==> exists|i: int|
+            0 <= i <= [email protected]() - [email protected]() && [email protected](i, #[trigger] (i + [email protected]())) == sub@,
+{
+    let s_len = s.unicode_len();
+    let sub_len = sub.unicode_len();
+    if (s_len < sub_len) {
+        return false;
+    }
+    if sub_len == 0 {
+        assert([email protected](0, (0 + [email protected]()) as int) == sub@);
+        return true;
+    }
+    for i in 0..s_len - sub_len + 1
+        invariant
+            forall|j: int| 0 <= j < i ==> [email protected](j, #[trigger] (j + [email protected]())) != sub@,
+            i <= s_len - sub_len + 1,
+            sub_len == [email protected]() <= s_len == [email protected](),
+            sub_len > 0,
+    {
+        if string_eq(sub, s.substring_char(i, i + sub_len)) {
+            assert(0 <= i <= [email protected]() - [email protected]());
+            assert([email protected](i as int, i + [email protected]()) == sub@);
+            return true;
+        }
+    }
+    false
+}
+
+fn string_eq(s1: &str, s2: &str) -> (result: bool)
+    ensures
+        result <==> s1@ == s2@,
+{
+    let s1_len = s1.unicode_len();
+    let s2_len = s2.unicode_len();
+    if s1_len != s2_len {
+        return false;
+    }
+    for i in 0..s1_len
+        invariant
+            [email protected](0, i as int) =~= [email protected](0, i as int),
+            i <= s1_len == s2_len == [email protected]() == [email protected](),
+    {
+        let c = s1.get_char(i);
+        if c != s2.get_char(i) {
+            return false;
+        }
+        assert([email protected](0, i + 1) == [email protected](0, i as int).push(c));
+        assert([email protected](0, i as int).push(c) == [email protected](0, i as int).push(c));
+        assert([email protected](0, i as int).push(c) == [email protected](0, i + 1));
+    }
+    assert(s1@ == [email protected](0, s1_len as int));
+    assert(s2@ == [email protected](0, s2_len as int));
+    true
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_012.rs

@@ -9,7 +9,42 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn longest(strings: &Vec<Vec<u8>>) -> (result: Option<&Vec<u8>>)
+    ensures
+        match result {
+            None => strings.len() == 0,
+            Some(s) => {
+                forall|i: int|
+                    #![auto]
+                    0 <= i < strings.len() ==> s.len() >= strings[i].len() && exists|i: int|
+                        #![auto]
+                        (0 <= i < strings.len() && s == strings[i] && (forall|j: int|
+                            #![auto]
+                            0 <= j < i ==> strings[j].len() < s.len()))
+            },
+        },
+{
+    if strings.len() == 0 {
+        return None;
+    }
+    let mut result: &Vec<u8> = &strings[0];
+    let mut pos = 0;
+
+    for i in 1..strings.len()
+        invariant
+            0 <= pos < i,
+            result == &strings[pos as int],
+            exists|i: int| 0 <= i < strings.len() && strings[i] == result,
+            forall|j: int| #![auto] 0 <= j < i ==> strings[j].len() <= result.len(),
+            forall|j: int| #![auto] 0 <= j < pos ==> strings[j].len() < result.len(),
+    {
+        if result.len() < strings[i].len() {
+            result = &strings[i];
+            pos = i;
+        }
+    }
+    Some(result)
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_014.rs

@@ -9,7 +9,53 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn all_prefixes(s: &Vec<u8>) -> (prefixes: Vec<Vec<u8>>)
+    ensures
+        prefixes.len() == s.len(),
+        forall|i: int| #![auto] 0 <= i < s.len() ==> prefixes[i]@ == [email protected](0, i + 1),
+{
+    let mut prefixes: Vec<Vec<u8>> = vec![];
+    let mut prefix = vec![];
+    assert(forall|i: int|
+        #![auto]
+        0 <= i < prefix.len() ==> [email protected](i) == [email protected](
+            0,
+            prefix.len() as int,
+        ).index(i));
+
+    assert(prefix@ == [email protected](0, 0));
+    assert(forall|i: int|
+        #![auto]
+        0 <= i < prefix.len() ==> [email protected](i) == [email protected](0, prefix.len() as int).index(i));
+    assert(prefix@ == [email protected](0, 0));
+    for i in 0..s.len()
+        invariant
+            prefixes.len() == i,
+            prefix.len() == i,
+            forall|j: int| #![auto] 0 <= j < i ==> prefixes[j]@ == [email protected](0, j + 1),
+            prefix@ == [email protected](0, i as int),
+            prefix@ == [email protected](0, i as int),
+    {
+        let ghost pre_prefix = prefix;
+        prefix.push(s[i]);
+        assert([email protected](0, i as int) == pre_prefix@ && [email protected](0, i as int)
+            == [email protected](0, i as int));
+        assert([email protected](0, i as int) == [email protected](0, i as int));
+        assert(prefix[i as int] == [email protected](0, i + 1).index(i as int));
+
+        assert(forall|j: int|
+            #![auto]
+            0 <= j < i + 1 ==> [email protected](j) == [email protected](0, (i + 1) as int).index(j));
+        assert(prefix@ == [email protected](0, (i + 1) as int));
+        assert(forall|j: int|
+            #![auto]
+            0 <= j < i + 1 ==> [email protected](j) == [email protected](0, (i + 1) as int).index(j));
+        assert(prefix@ == [email protected](0, (i + 1) as int));
+
+        prefixes.push(prefix.clone());
+    }
+    return prefixes;
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_068.rs

@@ -9,7 +9,51 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn pluck_smallest_even(nodes: &Vec<u32>) -> (result: Vec<u32>)
+    requires
+        [email protected]() <= u32::MAX,
+        forall|i: int| 0 <= i < [email protected]() ==> nodes@[i] >= 0,
+    ensures
+        [email protected]() == 0 || [email protected]() == 2,
+        [email protected]() == 2 ==> 0 <= result@[1] < [email protected]() && nodes@[result@[1] as int]
+            == result@[0],
+        [email protected]() == 2 ==> result@[0] % 2 == 0,
+        [email protected]() == 2 ==> forall|i: int|
+            0 <= i < [email protected]() && nodes@[i] % 2 == 0 ==> result@[0] <= nodes@[i],
+        [email protected]() == 2 ==> forall|i: int|
+            0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > result@[0],
+        [email protected]() == 0 ==> forall|i: int| 0 <= i < [email protected]() ==> nodes@[i] % 2 != 0,
+{
+    let mut smallest_even: Option<u32> = None;
+    let mut smallest_index: Option<u32> = None;
+
+    for i in 0..nodes.len()
+        invariant
+            0 <= i <= [email protected](),
+            [email protected]() <= u32::MAX,
+            smallest_even.is_none() == smallest_index.is_none(),
+            smallest_index.is_some() ==> 0 <= smallest_index.unwrap() < i as int,
+            smallest_index.is_some() ==> nodes@[smallest_index.unwrap() as int]
+                == smallest_even.unwrap(),
+            smallest_even.is_some() ==> smallest_even.unwrap() % 2 == 0,
+            smallest_even.is_some() ==> forall|j: int|
+                0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j],
+            smallest_index.is_some() ==> forall|j: int|
+                0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j]
+                    > smallest_even.unwrap(),
+            smallest_index.is_none() ==> forall|j: int| 0 <= j < i ==> nodes@[j] % 2 != 0,
+    {
+        if nodes[i] % 2 == 0 && (smallest_even.is_none() || nodes[i] < smallest_even.unwrap()) {
+            smallest_even = Some(nodes[i]);
+            smallest_index = Some((i as u32));
+        }
+    }
+    if smallest_index.is_none() {
+        Vec::new()
+    } else {
+        vec![smallest_even.unwrap(), smallest_index.unwrap()]
+    }
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_070.rs

@@ -9,8 +9,109 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
-
+// returns (sorted, strange). Also returning sorted solely to have access to it for writing postcondition
+fn strange_sort_list_helper(s: &Vec<i32>) -> (ret: (Vec<i32>, Vec<i32>))
+    ensures
+        [email protected]_multiset() == (ret.0)@.to_multiset(),
+        [email protected]() == (ret.0)@.len() == (ret.1)@.len(),
+        forall|i: int|
+            0 <= i < [email protected]() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2),
+        forall|i: int|
+            0 <= i < [email protected]() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index(
+                [email protected]() - (i - 1) / 2 - 1,
+            ),
+{
+    let sorted = sort_seq(s);
+    let mut strange = Vec::new();
+    let mut i: usize = 0;
+    while i < sorted.len()
+        invariant
+            i <= sorted.len() == [email protected](),
+            [email protected]() == i,
+            forall|j: int| 0 <= j < i && j % 2 == 0 ==> [email protected](j) == [email protected](j / 2),
+            forall|j: int|
+                0 < j < i && j % 2 == 1 ==> [email protected](j) == [email protected](
+                    [email protected]() - (j / 2) - 1,
+                ),
+    {
+        if i % 2 == 0 {
+            strange.push(sorted[i / 2]);
+        } else {
+            let r = (i - 1) / 2;
+            strange.push(sorted[s.len() - r - 1]);
+        }
+        i += 1;
+    }
+    (sorted, strange)
+}
+
+fn strange_sort_list(s: &Vec<i32>) -> (ret: Vec<i32>)
+    ensures
+        [email protected]() == [email protected](),
+{
+    let (_, strange) = strange_sort_list_helper(s);
+    strange
+}
+
+fn sort_seq(s: &Vec<i32>) -> (ret: Vec<i32>)
+    ensures
+        forall|i: int, j: int| 0 <= i < j < [email protected]() ==> [email protected](i) <= [email protected](j),
+        [email protected]() == [email protected](),
+        [email protected]_multiset() == [email protected]_multiset(),
+{
+    let mut sorted = s.clone();
+    let mut i: usize = 0;
+    while i < sorted.len()
+        invariant
+            i <= sorted.len(),
+            forall|j: int, k: int| 0 <= j < k < i ==> [email protected](j) <= [email protected](k),
+            [email protected]_multiset() == [email protected]_multiset(),
+            forall|j: int, k: int|
+                0 <= j < i <= k < [email protected]() ==> [email protected](j) <= [email protected](k),
+            [email protected]() == [email protected](),
+    {
+        let mut min_index: usize = i;
+        let mut j: usize = i + 1;
+        while j < sorted.len()
+            invariant
+                i <= min_index < j <= sorted.len(),
+                forall|k: int| i <= k < j ==> [email protected](min_index as int) <= [email protected](k),
+        {
+            if sorted[j] < sorted[min_index] {
+                min_index = j;
+            }
+            j += 1;
+        }
+        if min_index != i {
+            let curr_val = sorted[i];
+            let min_val = sorted[min_index];
+            sorted.set(i, min_val);
+            sorted.set(min_index, curr_val);
+            proof {
+                // swap_preserves_multiset([email protected]_values(|x| x as int), i as int, min_index as int);
+                assume([email protected]_multiset() == [email protected]_multiset());
+            }
+        }
+        i += 1;
+    }
+    sorted
+}
+
+// #[verifier::external_body]
+// // Helper lemma to prove that swapping two elements doesn't change the multiset
+// proof fn swap_preserves_multiset(s: Seq<int>, i: int, j: int)
+//     requires 0 <= i < s.len() && 0 <= j < s.len()
+//     ensures s.to_multiset() == s.update(i, s.index(j)).update(j, s.index(i)).to_multiset()
+// {
+//     let s_new = s.update(i, s.index(j)).update(j, s.index(i));
+//     assert(s.to_multiset().count(s.index(i)) == s_new.to_multiset().count(s.index(i)));
+//     assert(s.to_multiset().count(s.index(j)) == s_new.to_multiset().count(s.index(j)));
+//     assert forall|x: int| s.to_multiset().count(x) == s_new.to_multiset().count(x) by {
+//         if x != s.index(i) && x != s.index(j) {
+//             assert(s.to_multiset().count(x) == s_new.to_multiset().count(x));
+//         }
+//     }
+// }
 } // verus!
 fn main() {}