completed programs extracted from !11 #34

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

parno merged 1 commit into secure-foundations:main from edwin1729:reviewed

Aug 11, 2025

tasks/human_eval_012.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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]
+<= 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
+<= 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() {}
@@ Expand Down @@

tasks/human_eval_014.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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]
+<= i < prefix.len() ==> prefix@.index(i) == prefix@.subrange(
+,
+                prefix.len() as int,
+            ).index(i));
+        assert(prefix@ == prefix@.subrange(0, 0));
+        assert(forall|i: int|
+            #![auto]
+<= 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]
+<= 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]
+<= 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() {}
@@ Expand Down @@

tasks/human_eval_034.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
+<= 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
+<= 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|
+<= 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]]
+<= 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]]
+<= 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]
+<= i < sorted.len() ==> sorted@.to_multiset().contains(sorted[i])) by {
+                sorted@.to_multiset_ensures();
+            }
+            assert(forall|i: int|
+                #![auto]
+<= 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() {}
@@ Expand Down @@

tasks/human_eval_035.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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() {}
@@ Expand Down @@

tasks/human_eval_043.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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|
+<= 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
+<= 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
+<= i < j <= nums.len(),
+                    forall|u: int, v: int|
+<= 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() {}
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

completed programs extracted from !11 #34

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!