completed programs extract from !11

see original commits at secure-foundations#11

coauthored by @WeetHet

Author: edwin1729

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]@ == s@.subrange(0, i + 1),
+{
+    let mut prefixes: Vec<Vec<u8>> = vec![];
+    let mut prefix = vec![];
+    assert(forall|i: int|
+        #![auto]
+        0 <= i < prefix.len() ==> prefix@.index(i) == prefix@.subrange(
+            0,
+            prefix.len() as int,
+        ).index(i));
+
+    assert(prefix@ == prefix@.subrange(0, 0));
+    assert(forall|i: int|
+        #![auto]
+        0 <= i < prefix.len() ==> prefix@.index(i) == s@.subrange(0, prefix.len() as int).index(i));
+    assert(prefix@ == s@.subrange(0, 0));
+    for i in 0..s.len()
+        invariant
+            prefixes.len() == i,
+            prefix.len() == i,
+            forall|j: int| #![auto] 0 <= j < i ==> prefixes[j]@ == s@.subrange(0, j + 1),
+            prefix@ == s@.subrange(0, i as int),
+            prefix@ == prefix@.subrange(0, i as int),
+    {
+        let ghost pre_prefix = prefix;
+        prefix.push(s[i]);
+        assert(pre_prefix@.subrange(0, i as int) == pre_prefix@ && prefix@.subrange(0, i as int)
+            == pre_prefix@.subrange(0, i as int));
+        assert(prefix@.subrange(0, i as int) == s@.subrange(0, i as int));
+        assert(prefix[i as int] == s@.subrange(0, i + 1).index(i as int));
+
+        assert(forall|j: int|
+            #![auto]
+            0 <= j < i + 1 ==> prefix@.index(j) == prefix@.subrange(0, (i + 1) as int).index(j));
+        assert(prefix@ == prefix@.subrange(0, (i + 1) as int));
+        assert(forall|j: int|
+            #![auto]
+            0 <= j < i + 1 ==> prefix@.index(j) == s@.subrange(0, (i + 1) as int).index(j));
+        assert(prefix@ == s@.subrange(0, (i + 1) as int));
+
+        prefixes.push(prefix.clone());
+    }
+    return prefixes;
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_034.rs

@@ -5,11 +5,190 @@ 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 < ret@.len() ==> ret@.index(i) <= ret@.index(j),
+        ret@.len() == s@.len(),
+        s@.to_multiset() == ret@.to_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 ==> sorted@.index(j) <= sorted@.index(k),
+            s@.to_multiset() == sorted@.to_multiset(),
+            forall|j: int, k: int|
+                0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k),
+            sorted@.len() == s@.len(),
+        decreases (sorted.len() - i),
+    {
+        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 ==> sorted@.index(min_index as int) <= sorted@.index(k),
+            decreases (sorted.len() - j),
+        {
+            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() =~= sorted@.to_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() ==> s@.contains(result[i]),
+        forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(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 ==> result@.contains(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 result@.contains(s[m]) by {
+                assert(pre@.contains(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() ==> pre@.contains(result@[m]) ==> result@.contains(pre@[m])) by {
+            assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]);
+        }
+        assert(result@.contains(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() ==> s@.contains(result[i]),
+        forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]),
+{
+    let sorted = sort_seq(&s);
+    assert(forall|i: int| #![auto] 0 <= i < sorted.len() ==> s@.contains(sorted[i])) by {
+        assert(forall|i: int|
+            #![auto]
+            0 <= i < sorted.len() ==> sorted@.to_multiset().contains(sorted[i])) by {
+            sorted@.to_multiset_ensures();
+        }
+        assert(forall|i: int|
+            #![auto]
+            0 <= i < sorted.len() ==> s@.to_multiset().contains(sorted[i]));
+        s@.to_multiset_ensures();
+    }
+    assert(forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> sorted@.contains(s[i])) by {
+        assert(forall|i: int| #![auto] 0 <= i < s.len() ==> s@.to_multiset().contains(s[i])) by {
+            s@.to_multiset_ensures();
+        }
+        assert(forall|i: int| #![auto] 0 <= i < s.len() ==> sorted@.to_multiset().contains(s[i]));
+        sorted@.to_multiset_ensures();
+    }
+    unique_sorted(sorted)
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_035.rs

@@ -9,7 +9,25 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn max_element(a: &Vec<i32>) -> (max: i32)
+    requires
+        a.len() > 0,
+    ensures
+        forall|i: int| 0 <= i < a.len() ==> a[i] <= max,
+        exists|i: int| 0 <= i < a.len() && a[i] == max,
+{
+    let mut max = a[0];
+    for i in 1..a.len()
+        invariant
+            forall|j: int| 0 <= j < i ==> a[j] <= max,
+            exists|j: int| 0 <= j < i && a[j] == max,
+    {
+        if a[i] > max {
+            max = a[i];
+        }
+    }
+    max
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_043.rs

@@ -9,7 +9,42 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+#[verifier::loop_isolation(false)]
+fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool)
+    requires
+        nums.len() >= 2,
+        forall|i: int, j: int|
+            0 <= i < j < nums.len() ==> nums[i] + nums[j] <= i32::MAX && nums[i] + nums[j]
+                >= i32::MIN,
+    ensures
+        found <==> exists|i: int, j: int| 0 <= i < j < nums.len() && nums[i] + nums[j] == target,
+{
+    let mut i = 0;
+
+    while i < nums.len()
+        invariant
+            0 <= i <= nums.len(),
+            forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target,
+        decreases nums.len() - i,
+    {
+        let mut j = i + 1;
+        while j < nums.len()
+            invariant
+                0 <= i < j <= nums.len(),
+                forall|u: int, v: int|
+                    0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target,
+                forall|u: int| i < u < j ==> nums[i as int] + nums[u] != target,
+            decreases nums.len() - j,
+        {
+            if nums[i] + nums[j] == target {
+                return true;
+            }
+            j = j + 1;
+        }
+        i = i + 1;
+    }
+    false
+}
 
 } // verus!
 fn main() {}