completed programs roughly from 70 to 80

tasks/human_eval_007.rs

@@ -9,7 +9,87 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+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
+}
+
+spec fn is_subseq_of<A>(s: Seq<A>, sub: Seq<A>) -> bool {
+    exists|i: int| 0 <= i <= s.len() - sub.len() && s.subrange(i, #[trigger] (i + sub.len())) == sub
+}
+
+fn check_substring(s: &str, sub: &str) -> (result: bool)
+    ensures
+        result <==> is_subseq_of(s@, 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 filter_by_sub<'a>(strings: &Vec<&'a str>, sub: &str) -> (res: Vec<&'a str>)
+    ensures
+        [email protected](|s: &str| is_subseq_of(s@, sub@)) == res@,
+{
+    let mut res = Vec::new();
+    assert(res@ == Seq::<&str>::empty());
+    let mut n = 0;
+    for n in 0..strings.len()
+        invariant
+            [email protected](0, n as int).filter(|s: &str| is_subseq_of(s@, sub@)) == res@,
+            n <= strings.len(),
+    {
+        reveal(Seq::filter);
+        assert([email protected](0, n as int + 1).drop_last() == [email protected](0, n as int));
+        if check_substring(strings[n], sub) {
+            res.push(strings[n]);
+        }
+    }
+    assert([email protected](0, [email protected]() as int) == strings@);
+    res
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_012.rs

@@ -9,7 +9,41 @@ 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_034.rs

@@ -5,11 +5,188 @@ HumanEval/34
 /*
 ### VERUS BEGIN
 */
+use vstd::calc;
 use vstd::prelude::*;
+use vstd::seq_lib::lemma_multiset_commutative;
+use vstd::seq_lib::lemma_seq_contains_after_push;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+proof fn swap_preserves_multiset_helper(s: Seq<i32>, i: int, j: int)
+    requires
+        0 <= i < j < s.len(),
+    ensures
+        (s.take(j + 1)).to_multiset() =~= s.take(i).to_multiset().add(
+            s.subrange(i + 1, j).to_multiset(),
+        ).insert(s.index(j)).insert(s.index(i)),
+{
+    let fst = s.take(i);
+    let snd = s.subrange(i + 1, j);
+
+    assert((s.take(j + 1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add(
+        snd.to_multiset().insert(s.index(j)),
+    )) by {
+        assert(s.take(i + 1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by {
+            fst.to_multiset_ensures();
+            assert(fst.push(s.index(i)) =~= s.take(i + 1));
+        }
+        assert(s.subrange(i + 1, j + 1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by {
+            snd.to_multiset_ensures();
+            assert(snd.push(s.index(j)) =~= s.subrange(i + 1, j + 1));
+        }
+        lemma_multiset_commutative(s.take(i + 1), s.subrange(i + 1, j + 1));
+        assert(s.take(i + 1) + s.subrange(i + 1, j + 1) =~= s.take(j + 1));
+    }
+}
+
+// Helper lemma to prove that swapping two elements doesn't change the multiset
+proof fn swap_preserves_multiset(s1: Seq<i32>, s2: Seq<i32>, i: int, j: int)
+    requires
+        0 <= i < j < s1.len() == s2.len(),
+        forall|x: int| 0 <= x < s1.len() && x != i && x != j ==> s1.index(x) == s2.index(x),
+        s1.index(i) == s2.index(j),
+        s1.index(j) == s2.index(i),
+    ensures
+        s1.to_multiset() == s2.to_multiset(),
+{
+    calc! {
+        (==)
+        s1.to_multiset(); {
+            lemma_multiset_commutative(s1.take(j + 1), s1.skip(j + 1));
+            assert(s1 =~= s1.take(j + 1) + s1.skip(j + 1));
+        }
+        s1.take(j + 1).to_multiset().add(s1.skip(j + 1).to_multiset()); {
+            assert(s1.take(j + 1).to_multiset() =~= s2.take(j + 1).to_multiset()) by {
+                assert(s1.take(i) == s2.take(i));
+                assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j)));
+                swap_preserves_multiset_helper(s1, i, j);
+                swap_preserves_multiset_helper(s2, i, j);
+            }
+            assert(s1.skip(j + 1).to_multiset() =~= s2.skip(j + 1).to_multiset()) by {
+                assert(s1.skip(j + 1) =~= s2.skip(j + 1));
+            }
+        }
+        s2.take(j + 1).to_multiset().add(s2.skip(j + 1).to_multiset()); {
+            lemma_multiset_commutative(s2.take(j + 1), s2.skip(j + 1));
+            assert(s2 =~= s2.take(j + 1) + s2.skip(j + 1));
+        }
+        s2.to_multiset();
+    }
+}
+
+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 ghost old_sorted = sorted@;
+            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(old_sorted, sorted@, i as int, min_index as int);
+                assert(old_sorted.to_multiset() =~= [email protected]_multiset());
+            }
+        }
+        i += 1;
+    }
+    sorted
+}
+
+fn unique_sorted(s: Vec<i32>) -> (result: Vec<i32>)
+    requires
+        forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j],
+    ensures
+        forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j],
+        forall|i: int| #![auto] 0 <= i < result.len() ==> [email protected](result[i]),
+        forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> [email protected](s[i]),
+{
+    let mut result: Vec<i32> = vec![];
+    for i in 0..s.len()
+        invariant
+            forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j],
+            forall|k: int, l: int| 0 <= k < l < result.len() ==> result[k] < result[l],
+            forall|k: int|
+                #![trigger result[k]]
+                0 <= k < result.len() ==> (exists|m: int| 0 <= m < i && result[k] == s[m]),
+            forall|m: int| #![trigger s[m]] 0 <= m < i ==> [email protected](s[m]),
+    {
+        let ghost pre = result;
+        if result.len() == 0 || result[result.len() - 1] != s[i] {
+            assert(result.len() == 0 || result[result.len() - 1] < s[i as int]);
+            result.push(s[i]);
+            assert forall|m: int| #![trigger s[m]] 0 <= m < i implies [email protected](s[m]) by {
+                assert([email protected](s@[m]));
+                lemma_seq_contains_after_push(pre@, s@[i as int], s@[m]);
+            };
+        }
+        assert(forall|m: int|
+            #![trigger result@[m], pre@[m]]
+            0 <= m < pre.len() ==> [email protected](result@[m]) ==> [email protected](pre@[m])) by {
+            assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]);
+        }
+        assert([email protected](s[i as int])) by {
+            assert(result[result.len() - 1] == s[i as int]);
+        }
+    }
+    result
+}
+
+fn unique(s: Vec<i32>) -> (result: Vec<i32>)
+    ensures
+        forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j],
+        forall|i: int| #![auto] 0 <= i < result.len() ==> [email protected](result[i]),
+        forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> [email protected](s[i]),
+{
+    let sorted = sort_seq(&s);
+    assert(forall|i: int| #![auto] 0 <= i < sorted.len() ==> [email protected](sorted[i])) by {
+        assert(forall|i: int|
+            #![auto]
+            0 <= i < sorted.len() ==> [email protected]_multiset().contains(sorted[i])) by {
+            [email protected]_multiset_ensures();
+        }
+        assert(forall|i: int|
+            #![auto]
+            0 <= i < sorted.len() ==> [email protected]_multiset().contains(sorted[i]));
+        [email protected]_multiset_ensures();
+    }
+    assert(forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> [email protected](s[i])) by {
+        assert(forall|i: int| #![auto] 0 <= i < s.len() ==> [email protected]_multiset().contains(s[i])) by {
+            [email protected]_multiset_ensures();
+        }
+        assert(forall|i: int| #![auto] 0 <= i < s.len() ==> [email protected]_multiset().contains(s[i]));
+        [email protected]_multiset_ensures();
+    }
+    unique_sorted(sorted)
+}
 
 } // verus!
 fn main() {}