diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs
index b8ba40c..3922afa 100644
--- a/tasks/human_eval_007.rs
+++ b/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
+ s1@.subrange(0, i as int) =~= s2@.subrange(0, i as int),
+ i <= s1_len == s2_len == s1@.len() == s2@.len(),
+ {
+ let c = s1.get_char(i);
+ if c != s2.get_char(i) {
+ return false;
+ }
+ assert(s1@.subrange(0, i + 1) == s1@.subrange(0, i as int).push(c));
+ assert(s1@.subrange(0, i as int).push(c) == s2@.subrange(0, i as int).push(c));
+ assert(s2@.subrange(0, i as int).push(c) == s2@.subrange(0, i + 1));
+ }
+ assert(s1@ == s1@.subrange(0, s1_len as int));
+ assert(s2@ == s2@.subrange(0, s2_len as int));
+ true
+}
+
+spec fn is_subseq_of(s: Seq, sub: Seq) -> 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(s@.subrange(0, (0 + sub@.len()) as int) == sub@);
+ return true;
+ }
+ for i in 0..s_len - sub_len + 1
+ invariant
+ forall|j: int| 0 <= j < i ==> s@.subrange(j, #[trigger] (j + sub@.len())) != sub@,
+ i <= s_len - sub_len + 1,
+ sub_len == sub@.len() <= s_len == s@.len(),
+ sub_len > 0,
+ {
+ if string_eq(sub, s.substring_char(i, i + sub_len)) {
+ assert(0 <= i <= s@.len() - sub@.len());
+ assert(s@.subrange(i as int, i + sub@.len()) == sub@);
+ return true;
+ }
+ }
+ false
+}
+
+fn filter_by_sub<'a>(strings: &Vec<&'a str>, sub: &str) -> (res: Vec<&'a str>)
+ ensures
+ strings@.filter(|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
+ strings@.subrange(0, n as int).filter(|s: &str| is_subseq_of(s@, sub@)) == res@,
+ n <= strings.len(),
+ {
+ reveal(Seq::filter);
+ assert(strings@.subrange(0, n as int + 1).drop_last() == strings@.subrange(0, n as int));
+ if check_substring(strings[n], sub) {
+ res.push(strings[n]);
+ }
+ }
+ assert(strings@.subrange(0, strings@.len() as int) == strings@);
+ res
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_012.rs b/tasks/human_eval_012.rs
index 4a6722d..57ee646 100644
--- a/tasks/human_eval_012.rs
+++ b/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>) -> (result: Option<&Vec>)
+ 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 = &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() {}
diff --git a/tasks/human_eval_014.rs b/tasks/human_eval_014.rs
index 9d5d1e5..ae23a14 100644
--- a/tasks/human_eval_014.rs
+++ b/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) -> (prefixes: Vec>)
+ 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![];
+ 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() {}
diff --git a/tasks/human_eval_034.rs b/tasks/human_eval_034.rs
index a7c6bdb..9d96386 100644
--- a/tasks/human_eval_034.rs
+++ b/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, 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, s2: Seq, 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) -> (ret: Vec)
+ 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) -> (result: Vec)
+ 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 = 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) -> (result: Vec)
+ 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() {}
diff --git a/tasks/human_eval_035.rs b/tasks/human_eval_035.rs
index db151d6..5b4a5d9 100644
--- a/tasks/human_eval_035.rs
+++ b/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) -> (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() {}
diff --git a/tasks/human_eval_037.rs b/tasks/human_eval_037.rs
index 99af6b8..f438baa 100644
--- a/tasks/human_eval_037.rs
+++ b/tasks/human_eval_037.rs
@@ -9,7 +9,159 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// code taken from sort_third (033)
+spec fn count(s: Seq, x: T) -> int
+ decreases s.len(),
+{
+ if s.len() == 0 {
+ 0
+ } else {
+ count(s.skip(1), x) + if s[0] == x {
+ 1int
+ } else {
+ 0int
+ }
+ }
+}
+
+// This function defines what it means for two sequences to be
+// permutations of each other: for every value `x`, each of the two
+// sequences has the same number of instances of `x`.
+spec fn permutes(s1: Seq, s2: Seq) -> bool {
+ forall|x: T| count(s1, x) == count(s2, x)
+}
+
+// This lemma establishes the effect of an `update` operation on the
+// result of a `count`. That is, it gives a closed-form
+// (non-recursive) description of what happens to `count(s, x)` when
+// `s` is updated to `s.update(i, v)`.
+proof fn lemma_update_effect_on_count(s: Seq, i: int, v: T, x: T)
+ requires
+ 0 <= i < s.len(),
+ ensures
+ count(s.update(i, v), x) == if v == x && s[i] != x {
+ count(s, x) + 1
+ } else if v != x && s[i] == x {
+ count(s, x) - 1
+ } else {
+ count(s, x)
+ },
+ decreases s.len(),
+{
+ if s.len() == 0 {
+ return ;
+ }
+ if i == 0 {
+ assert(s.update(i, v) =~= seq![v] + s.skip(1));
+ assert(s.update(i, v).skip(1) =~= s.skip(1));
+ } else {
+ assert(s.update(i, v) =~= seq![s[0]] + s.skip(1).update(i - 1, v));
+ assert(s.update(i, v).skip(1) =~= s.skip(1).update(i - 1, v));
+ lemma_update_effect_on_count(s.skip(1), i - 1, v, x);
+ }
+}
+
+// This lemma proves that if you swap elements `i` and `j` of sequence `s`,
+// you get a permutation of `s`.
+proof fn lemma_swapping_produces_a_permutation(s: Seq, i: int, j: int)
+ requires
+ 0 <= i < s.len(),
+ 0 <= j < s.len(),
+ ensures
+ permutes(s.update(i, s[j]).update(j, s[i]), s),
+{
+ assert forall|x: T| #[trigger] count(s.update(i, s[j]).update(j, s[i]), x) == count(s, x) by {
+ lemma_update_effect_on_count(s, i, s[j], x);
+ lemma_update_effect_on_count(s.update(i, s[j]), j, s[i], x);
+ }
+}
+
+#[verifier::loop_isolation(false)]
+fn sort_pred(l: Vec, p: Vec) -> (l_prime: Vec)
+ requires
+ l.len() == p.len(),
+ ensures
+ l_prime.len() == l.len(),
+ forall|i: int| 0 <= i < l.len() && !p[i] ==> l_prime[i] == l[i],
+ forall|i: int, j: int|
+ #![auto]
+ 0 <= i < j < l.len() && p[i] && p[j] ==> l_prime[i] <= l_prime[j],
+ permutes(l_prime@, l@),
+{
+ let ghost old_l = l@;
+ let l_len = l.len();
+ let mut pos_replace: usize = 0;
+ let mut l_prime: Vec = l;
+ while pos_replace < l_len
+ invariant
+ l_len == l.len() == l_prime.len(),
+ forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i],
+ permutes(l_prime@, l@),
+ forall|i: int, j: int|
+ #![auto]
+ 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i] <= l_prime[j],
+ {
+ if p[pos_replace] {
+ let mut pos_cur: usize = pos_replace;
+ let mut pos: usize = pos_replace;
+ while pos < l_len
+ invariant
+ l_len == l.len() == l_prime.len(),
+ pos_replace <= pos,
+ pos_replace <= pos_cur < l_len,
+ p[pos_replace as int],
+ p[pos_cur as int],
+ forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i],
+ permutes(l_prime@, l@),
+ forall|i: int|
+ #![auto]
+ pos_replace <= i < pos && p[i] ==> l_prime[pos_cur as int] <= l_prime[i],
+ forall|i: int, j: int|
+ #![auto]
+ 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i]
+ <= l_prime[j],
+ {
+ if p[pos] && l_prime[pos] < l_prime[pos_cur] {
+ pos_cur = pos;
+ }
+ pos = pos + 1;
+ }
+ proof {
+ lemma_swapping_produces_a_permutation(l_prime@, pos_replace as int, pos_cur as int);
+ }
+ let v1 = l_prime[pos_replace];
+ let v2 = l_prime[pos_cur];
+ l_prime.set(pos_replace, v2);
+ l_prime.set(pos_cur, v1);
+ }
+ pos_replace = pos_replace + 1;
+ }
+ l_prime
+}
+
+#[verifier::loop_isolation(false)]
+fn sort_even(l: Vec) -> (result: Vec)
+ ensures
+ l.len() == result.len(),
+ permutes(result@, l@),
+ forall|i: int| 0 <= i < l.len() && i % 2 == 1 ==> result[i] == l[i],
+ forall|i: int, j: int|
+ #![auto]
+ 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> result[i] <= result[j],
+{
+ let mut p: Vec = vec![];
+ for i in 0..l.len()
+ invariant
+ p.len() == i,
+ forall|j: int| 0 <= j < i ==> p[j] == (j % 2 == 0),
+ {
+ p.push(i % 2 == 0);
+ }
+ assert(forall|i: int, j: int|
+ #![auto]
+ 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> p[i] && p[j]);
+ sort_pred(l, p)
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_043.rs b/tasks/human_eval_043.rs
index 37830cc..e32fc3b 100644
--- a/tasks/human_eval_043.rs
+++ b/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() {}
diff --git a/tasks/human_eval_049.rs b/tasks/human_eval_049.rs
index 3756e13..81321d9 100644
--- a/tasks/human_eval_049.rs
+++ b/tasks/human_eval_049.rs
@@ -9,7 +9,43 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn modp_rec(n: nat, p: nat) -> nat
+ decreases n,
+{
+ if n == 0 {
+ 1nat % p
+ } else {
+ (modp_rec((n - 1) as nat, p) * 2) % p
+ }
+}
+
+fn modmul(a: u32, b: u32, p: u32) -> (mul: u32)
+ by (nonlinear_arith)
+ requires
+ p > 0,
+ ensures
+ mul == ((a as int) * (b as int)) % (p as int),
+{
+ (((a as u64) * (b as u64)) % (p as u64)) as u32
+}
+
+#[verifier::loop_isolation(false)]
+fn modp(n: u32, p: u32) -> (r: u32)
+ by (nonlinear_arith)
+ requires
+ p > 0,
+ ensures
+ r == modp_rec(n as nat, p as nat),
+{
+ let mut r = 1u32 % p;
+ for i in 0..n
+ invariant
+ r == modp_rec(i as nat, p as nat),
+ {
+ r = modmul(r, 2, p);
+ }
+ r
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_050.rs b/tasks/human_eval_050.rs
index 71023ab..c97fca3 100644
--- a/tasks/human_eval_050.rs
+++ b/tasks/human_eval_050.rs
@@ -9,7 +9,96 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn encode_char_spec(c: int) -> int
+ recommends
+ 65 <= c <= 90,
+{
+ (c - 65 + 5) % 26 + 65
+}
+
+fn encode_char(c: u8) -> (r: u8)
+ requires
+ 65 <= c <= 90,
+ ensures
+ r == encode_char_spec(c as int),
+ 65 <= r <= 90,
+{
+ (c - 65 + 5) % 26 + 65
+}
+
+spec fn decode_char_spec(c: int) -> int
+ recommends
+ 65 <= c <= 90,
+{
+ (c - 65 + 26 - 5) % 26 + 65
+}
+
+fn decode_char(c: u8) -> (r: u8)
+ requires
+ 65 <= c <= 90,
+ ensures
+ r == decode_char_spec(c as int),
+ 65 <= r <= 90,
+{
+ (c - 65 + 26 - 5) % 26 + 65
+}
+
+proof fn opposite_encode_decode(c: int)
+ requires
+ 65 <= c <= 90,
+ ensures
+ encode_char_spec(decode_char_spec(c)) == c,
+ decode_char_spec(encode_char_spec(c)) == c,
+{
+}
+
+#[verifier::loop_isolation(false)]
+fn encode_shift(s: &Vec) -> (t: Vec)
+ requires
+ forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90,
+ ensures
+ s.len() == t.len(),
+ forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == encode_char_spec(s[i] as int),
+ forall|i: int| #![auto] 0 <= i < t.len() ==> decode_char_spec(t[i] as int) == s[i],
+{
+ let mut t: Vec = vec![];
+ for i in 0..s.len()
+ invariant
+ t.len() == i,
+ forall|j: int| #![auto] 0 <= j < i ==> t[j] == encode_char_spec(s[j] as int),
+ forall|j: int| #![auto] 0 <= j < i ==> decode_char_spec(t[j] as int) == s[j],
+ {
+ t.push(encode_char(s[i]));
+ proof {
+ opposite_encode_decode(s[i as int] as int);
+ }
+ }
+ t
+}
+
+#[verifier::loop_isolation(false)]
+fn decode_shift(s: &Vec) -> (t: Vec)
+ requires
+ forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90,
+ ensures
+ s.len() == t.len(),
+ forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == decode_char_spec(s[i] as int),
+ forall|i: int| #![auto] 0 <= i < t.len() ==> encode_char_spec(t[i] as int) == s[i],
+{
+ let mut t: Vec = vec![];
+ for i in 0..s.len()
+ invariant
+ t.len() == i,
+ forall|j: int| #![auto] 0 <= j < i ==> t[j] == decode_char_spec(s[j] as int),
+ forall|j: int| #![auto] 0 <= j < i ==> encode_char_spec(t[j] as int) == s[j],
+ {
+ t.push(decode_char(s[i]));
+ proof {
+ opposite_encode_decode(s[i as int] as int);
+ }
+ }
+ t
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_054.rs b/tasks/human_eval_054.rs
index 1c44e12..e894030 100644
--- a/tasks/human_eval_054.rs
+++ b/tasks/human_eval_054.rs
@@ -5,11 +5,92 @@ HumanEval/54
/*
### VERUS BEGIN
*/
+use vstd::hash_set::HashSetWithView;
use vstd::prelude::*;
+use vstd::std_specs::hash::axiom_u8_obeys_hash_table_key_model;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+broadcast use axiom_u8_obeys_hash_table_key_model;
+
+fn hash_set_from(s: &Vec) -> (res: HashSetWithView)
+ ensures
+ forall|i: int| #![auto] 0 <= i < s.len() ==> res@.contains(s[i]),
+ forall|x: int|
+ 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> #[trigger] s@.contains(x as u8),
+{
+ let mut res: HashSetWithView = HashSetWithView::new();
+ for i in 0..s.len()
+ invariant
+ forall|j: int| #![auto] 0 <= j < i ==> res@.contains(s[j]),
+ forall|x: int|
+ 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> (exists|j: int|
+ 0 <= j < i && s[j] == x),
+ {
+ res.insert(s[i]);
+ }
+ res
+}
+
+proof fn implies_contains(s0: Seq, s1: Seq, hs1: Set)
+ requires
+ forall|i: int| #![trigger s0[i]] 0 <= i < s0.len() ==> 0 <= s0[i] < 256,
+ forall|x: int|
+ 0 <= x < 256 ==> #[trigger] hs1.contains(x as u8) ==> #[trigger] s1.contains(x as u8),
+ ensures
+ forall|i: int|
+ #![auto]
+ 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) ==> s1.contains(s0[i]),
+{
+ assert forall|i: int|
+ #![auto]
+ 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) implies s1.contains(s0[i]) by {
+ let x = s0[i];
+ assert(0 <= x < 256);
+ assert(hs1.contains(x as u8));
+ assert(s1.contains(x as u8));
+ };
+}
+
+#[verifier::loop_isolation(false)]
+fn same_chars(s0: &Vec, s1: &Vec) -> (same: bool)
+ ensures
+ same <==> (forall|i: int| #![auto] 0 <= i < s0.len() ==> s1@.contains(s0[i])) && (forall|
+ i: int,
+ |
+ #![auto]
+ 0 <= i < s1.len() ==> s0@.contains(s1[i])),
+{
+ let hs0 = hash_set_from(s0);
+ let hs1 = hash_set_from(s1);
+
+ proof {
+ implies_contains(s0@, s1@, hs1@);
+ implies_contains(s1@, s0@, hs0@);
+ }
+
+ let mut contains_s0 = true;
+ for i in 0..s0.len()
+ invariant
+ contains_s0 <==> forall|j: int| #![auto] 0 <= j < i ==> s1@.contains(s0[j]),
+ {
+ if !hs1.contains(&s0[i]) {
+ contains_s0 = false;
+ assert(!s1@.contains(s0[i as int]));
+ }
+ }
+ let mut contains_s1 = true;
+ for i in 0..s1.len()
+ invariant
+ contains_s1 <==> forall|j: int| #![auto] 0 <= j < i ==> s0@.contains(s1[j]),
+ {
+ if !hs0.contains(&s1[i]) {
+ contains_s1 = false;
+ assert(!s0@.contains(s1[i as int]));
+ }
+ }
+ contains_s0 && contains_s1
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_068.rs b/tasks/human_eval_068.rs
index b6b971f..d2e3e58 100644
--- a/tasks/human_eval_068.rs
+++ b/tasks/human_eval_068.rs
@@ -9,7 +9,54 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn pluck_smallest_even(nodes: &Vec) -> (result: Vec)
+ requires
+ nodes@.len() <= u32::MAX,
+ ensures
+ result@.len() == 0 || result@.len() == 2,
+ result@.len() == 0 ==> forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] % 2 != 0,
+ result@.len() == 2 ==> {
+ let node = result@[0];
+ let index = result@[1];
+ &&& 0 <= index < nodes@.len()
+ &&& nodes@[index as int] == node
+ &&& node % 2 == 0
+ &&& forall|i: int|
+ 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> node <= nodes@[i] && forall|i: int|
+ 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > node
+ },
+{
+ let mut smallest_even: Option = None;
+ let mut smallest_index: Option = None;
+
+ for i in 0..nodes.len()
+ invariant
+ 0 <= i <= nodes@.len(),
+ nodes@.len() <= u32::MAX,
+ smallest_even.is_none() == smallest_index.is_none(),
+ smallest_index.is_none() ==> forall|j: int| 0 <= j < i ==> nodes@[j] % 2 != 0,
+ smallest_index.is_some() ==> {
+ &&& 0 <= smallest_index.unwrap() < i as int
+ &&& nodes@[smallest_index.unwrap() as int] == smallest_even.unwrap()
+ &&& smallest_even.unwrap() % 2 == 0
+ &&& forall|j: int|
+ 0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j]
+ &&& forall|j: int|
+ 0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j]
+ > smallest_even.unwrap()
+ },
+ {
+ 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() {}
diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs
index 21b837c..3e5db36 100644
--- a/tasks/human_eval_070.rs
+++ b/tasks/human_eval_070.rs
@@ -5,11 +5,167 @@ HumanEval/70
/*
### VERUS BEGIN
*/
+use vstd::calc;
use vstd::prelude::*;
+use vstd::seq_lib::lemma_multiset_commutative;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+proof fn swap_preserves_multiset_helper(s: Seq, 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, s2: Seq, 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) -> (ret: Vec)
+ 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
+}
+
+// returns (sorted, strange). Also returning sorted solely to have access to it for writing postcondition
+fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec))
+ ensures
+ s@.to_multiset() == (ret.0)@.to_multiset(),
+ s@.len() == (ret.0)@.len() == (ret.1)@.len(),
+ forall|i: int|
+ 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2),
+ forall|i: int|
+ 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index(
+ s@.len() - (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() == s@.len(),
+ strange@.len() == i,
+ forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2),
+ forall|j: int|
+ 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index(
+ sorted@.len() - (j / 2) - 1,
+ ),
+ decreases sorted.len() - i,
+ {
+ 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) -> (ret: Vec)
+ ensures
+ s@.len() == ret@.len(),
+{
+ let (_, strange) = strange_sort_list_helper(s);
+ strange
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_072.rs b/tasks/human_eval_072.rs
index 921035d..1429940 100644
--- a/tasks/human_eval_072.rs
+++ b/tasks/human_eval_072.rs
@@ -9,7 +9,126 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// i and j are ends of the subrange - exclusive
+proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int)
+ requires
+ 0 <= i <= j <= s.len(),
+ ensures
+ spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)),
+ decreases j - i,
+{
+ if (i < j) {
+ assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by {
+ assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1));
+ }
+ lemma_increasing_sum_params(s, i, j - 1);
+ }
+}
+
+proof fn lemma_increasing_sum(s: Seq)
+ ensures
+ forall|i: int, j: int|
+ #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))]
+ 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)),
+{
+ assert forall|i: int, j: int|
+ #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))]
+ 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) by {
+ if (0 <= i <= j <= s.len()) {
+ lemma_increasing_sum_params(s, i, j);
+ }
+ }
+}
+
+spec fn spec_sum(s: Seq) -> int {
+ s.fold_left(0, |x: int, y| x + y)
+}
+
+fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool)
+ ensures
+ ret <==> spec_sum(qs@) <= w,
+{
+ let mut sum: u32 = 0;
+ for i in 0..qs.len()
+ invariant
+ sum == spec_sum(qs@.subrange(0, i as int)),
+ i <= qs.len(),
+ sum <= w,
+ {
+ proof {
+ assert(spec_sum(qs@.subrange(0, i + 1)) <= spec_sum(qs@)) by {
+ assert(qs@ == qs@.subrange(0, qs@.len() as int));
+ lemma_increasing_sum(qs@);
+ }
+ assert(spec_sum(qs@.subrange(0, i as int)) + qs[i as int] == spec_sum(
+ qs@.subrange(0, i + 1),
+ )) by {
+ assert(qs@.subrange(0, i + 1).drop_last() == qs@.subrange(0, i as int));
+ }
+ }
+ let sum_opt = sum.checked_add(qs[i]);
+ if sum_opt.is_none() {
+ assert(spec_sum(qs@.subrange(0, i + 1)) > u32::MAX >= w);
+ return false;
+ } else {
+ sum = sum_opt.unwrap();
+ if sum > w {
+ assert(spec_sum(qs@.subrange(0, i + 1)) > w);
+ return false;
+ }
+ }
+ }
+ assume(sum == spec_sum(qs@));
+ true
+}
+
+fn palindrome(qs: &Vec) -> (ret: bool)
+ ensures
+ ret <==> qs@ =~= qs@.reverse(),
+{
+ let mut ret = true;
+ let mut i: usize = 0;
+ while i < qs.len() / 2
+ invariant
+ i <= qs@.len() / 2,
+ ret <==> qs@.subrange(0, i as int) =~= qs@.subrange(
+ qs@.len() - i,
+ qs@.len() as int,
+ ).reverse(),
+ {
+ // reveal_with_fuel(Seq::reverse, 5); // VERUS BUG on uncomment. file issue
+ assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last()
+ =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse());
+ assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange(
+ qs@.len() - i,
+ qs@.len() as int,
+ ).reverse().push(qs@.index(qs@.len() - (i + 1))));
+ if qs[i] != qs[qs.len() - i - 1] {
+ ret = false;
+ }
+ i += 1;
+ }
+ let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int);
+ let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int);
+ proof {
+ if (qs.len() % 2) == 1 {
+ assert(qs@ =~= fst_half + qs@.subrange(
+ (qs@.len() / 2) as int,
+ qs@.len() - qs@.len() / 2,
+ ) + snd_half);
+ } else {
+ assert(qs@ =~= fst_half + snd_half);
+ }
+ }
+ ret
+}
+
+fn will_it_fly(qs: &Vec, w: u32) -> (ret: bool)
+ ensures
+ ret <==> qs@ =~= qs@.reverse() && spec_sum(qs@) <= w,
+{
+ palindrome(qs) && sum_lesser_than_limit(qs, w)
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_073.rs b/tasks/human_eval_073.rs
index ba70ee6..59c2166 100644
--- a/tasks/human_eval_073.rs
+++ b/tasks/human_eval_073.rs
@@ -9,7 +9,49 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn zip_halves(v: Seq) -> (ret: Seq<(T, T)>) {
+ v.take((v.len() / 2) as int).zip_with(v.skip(((v.len() + 1) / 2) as int).reverse())
+}
+
+spec fn diff(s: Seq<(i32, i32)>) -> int {
+ s.fold_left(
+ 0,
+ |acc: int, x: (i32, i32)|
+ if (x.0 != x.1) {
+ acc + 1
+ } else {
+ acc
+ },
+ )
+}
+
+fn smallest_change(v: Vec) -> (change: usize)
+ requires
+ v@.len() < usize::MAX,
+ ensures
+ change == diff(zip_halves(v@)),
+{
+ let mut ans: usize = 0;
+ let ghost zipped = Seq::<(i32, i32)>::empty();
+ for i in 0..v.len() / 2
+ invariant
+ ans <= i <= v@.len() / 2 < usize::MAX,
+ ans == diff(zipped),
+ zipped =~= zip_halves(v@).take(i as int),
+ {
+ proof {
+ let ghost pair = (v[i as int], v[v.len() - i - 1]);
+ let ghost zipped_old = zipped;
+ zipped = zipped.push(pair);
+ assert(zipped.drop_last() =~= zipped_old);
+ }
+ if v[i] != v[v.len() - i - 1] {
+ ans += 1;
+ }
+ }
+ assert(zip_halves(v@).take((v@.len() / 2) as int) =~= zip_halves(v@));
+ ans
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_074.rs b/tasks/human_eval_074.rs
index eeaaecf..3e5c3f7 100644
--- a/tasks/human_eval_074.rs
+++ b/tasks/human_eval_074.rs
@@ -9,7 +9,88 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_sum(s: Seq) -> int {
+ s.fold_left(0, |x: int, y| x + y)
+}
+
+// i and j are ends of the subrange - exclusive
+proof fn lemma_increasing_sum(s: Seq, i: int, j: int)
+ requires
+ 0 <= i <= j <= s.len(),
+ ensures
+ spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)),
+ decreases j - i,
+{
+ if (i < j) {
+ assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by {
+ assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1));
+ }
+ lemma_increasing_sum(s, i, j - 1);
+ }
+}
+
+spec fn total_str_len(strings: Seq<&str>) -> int {
+ spec_sum(strings.map_values(|s: &str| s@.len()))
+}
+
+fn checked_total_str_len(lst: &Vec<&str>) -> (ret: Option)
+ ensures
+ ret.is_some() <==> total_str_len(lst@) <= usize::MAX,
+ ret.is_some() <==> ret.unwrap() == total_str_len(lst@),
+{
+ let ghost lens = Seq::::empty();
+ let mut sum: usize = 0;
+ for i in 0..lst.len()
+ invariant
+ sum == lst@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left(
+ 0,
+ |x: int, y| x + y,
+ ),
+ spec_sum(lens) == sum,
+ lens =~= lst@.map_values(|s: &str| s@.len()).take(i as int),
+ lens =~= lst@.take(i as int).map_values(|s: &str| s@.len()),
+ {
+ let x = lst[i].unicode_len();
+ proof {
+ assert(lens.push(x as nat).drop_last() == lens);
+ lens = lens.push(x as nat);
+ assert(lens =~= lst@.map_values(|s: &str| s@.len()).take(i + 1));
+
+ lemma_increasing_sum(lst@.map_values(|s: &str| s@.len()), i + 1, lst@.len() as int);
+ assert(total_str_len(lst@) >= spec_sum(lens)) by {
+ assert(lst@.map_values(|s: &str| s@.len()) =~= lst@.map_values(
+ |s: &str| s@.len(),
+ ).take(lst@.len() as int));
+ }
+ if x + sum > usize::MAX {
+ assert(sum.checked_add(x).is_none());
+ assert(total_str_len(lst@) > usize::MAX);
+ }
+ }
+ sum = sum.checked_add(x)?;
+ assert(lst@.take(i + 1).map_values(|s: &str| s@.len()).drop_last() == lst@.take(
+ i as int,
+ ).map_values(|s: &str| s@.len()));
+ }
+ assert(lst@ == lst@.subrange(0, lst.len() as int));
+ return Some(sum);
+}
+
+fn total_match<'a>(lst1: Vec<&'a str>, lst2: Vec<&'a str>) -> (ret: Option>)
+ ensures
+ ret.is_some() <== total_str_len(lst1@) <= usize::MAX && total_str_len(lst2@) <= usize::MAX,
+ ret.is_some() ==> ret.unwrap() == if total_str_len(lst1@) <= total_str_len(lst2@) {
+ lst1
+ } else {
+ lst2
+ },
+{
+ if checked_total_str_len(&lst1)? <= checked_total_str_len(&lst2)? {
+ Some(lst1)
+ } else {
+ Some(lst2)
+ }
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_075.rs b/tasks/human_eval_075.rs
index 4bf4540..dcbb5d6 100644
--- a/tasks/human_eval_075.rs
+++ b/tasks/human_eval_075.rs
@@ -5,11 +5,130 @@ HumanEval/75
/*
### VERUS BEGIN
*/
+use vstd::arithmetic::mul::*;
use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_prime(p: int) -> bool {
+ p > 1 && forall|k: int| 1 < k < p ==> #[trigger] (p % k) != 0
+}
+
+fn prime(p: u32) -> (ret: bool)
+ ensures
+ ret <==> spec_prime(p as int),
+{
+ if p <= 1 {
+ return false;
+ }
+ for k in 2..p
+ invariant
+ forall|j: int| 1 < j < k ==> #[trigger] (p as int % j) != 0,
+ k <= p,
+ {
+ if p % k == 0 {
+ return false;
+ }
+ }
+ true
+}
+
+fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option)
+ ensures
+ ret.is_some() ==> ret.unwrap() == x * y * z,
+ ret.is_none() ==> x * y * z > u32::MAX,
+{
+ // x,y,z == 0 done separately to invoke lemma_mul_increases which requires x > 0
+ if (x == 0 || y == 0 || z == 0) {
+ assert(0 == x * y * z);
+ return Some(0);
+ }
+ assert(x > 0 && y > 0 && z > 0);
+ let prod2 = x.checked_mul(y);
+ if prod2.is_some() {
+ let prod3 = prod2.unwrap().checked_mul(z);
+ if prod3.is_some() {
+ let ans = prod3.unwrap();
+ assert(ans == x * y * z);
+ Some(ans)
+ } else {
+ assert(x * y * z > u32::MAX);
+ None
+ }
+ } else {
+ broadcast use group_mul_properties;
+
+ assert(x * y * z >= y * z);
+ None
+ }
+}
+
+fn is_multiply_prime(x: u32) -> (ans: bool)
+ requires
+ x > 1,
+ ensures
+ ans <==> exists|a: int, b: int, c: int|
+ spec_prime(a) && spec_prime(b) && spec_prime(c) && x == a * b * c,
+{
+ let mut a = 1;
+ while a < x
+ invariant
+ forall|i: int, j: int, k: int|
+ (spec_prime(i) && spec_prime(j) && spec_prime(k) && i <= a && j <= x && k <= x)
+ ==> x != i * j * k,
+ a <= x,
+ decreases x - a,
+ {
+ a += 1;
+ if prime(a) {
+ let mut b = 1;
+ while b < x
+ invariant
+ forall|j: int, k: int|
+ (spec_prime(j) && spec_prime(k) && j <= b && k <= x) ==> x != (a as int) * j
+ * k,
+ spec_prime(a as int),
+ a <= x,
+ b <= x,
+ decreases x - b,
+ {
+ b += 1;
+ if prime(b) {
+ let mut c = 1;
+ while c < x
+ invariant
+ forall|k: int| (spec_prime(k) && k <= c as int) ==> x != a * b * k,
+ spec_prime(a as int),
+ spec_prime(b as int),
+ a <= x,
+ b <= x,
+ c <= x,
+ decreases x - c,
+ {
+ c += 1;
+ let prod = checked_mul_thrice(a, b, c);
+ if prime(c) && prod.is_some() && x == prod.unwrap() {
+ return true;
+ }
+ }
+ }
+ }
+ }
+ }
+ assert(forall|i: int, j: int, k: int|
+ i <= x && j <= x && k <= x && spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j
+ * k);
+ // prove that that even if the factors are not in the range [2, x], the product is still not equal to x
+ assert forall|i: int, j: int, k: int|
+ spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j * k by {
+ if (i > 1 && j > 1 && k > 1 && (i > x || j > x || k > x)) {
+ broadcast use group_mul_properties;
+
+ assert(i * j * k > x);
+ }
+ }
+ false
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_076.rs b/tasks/human_eval_076.rs
index 3a5559e..3d5ad48 100644
--- a/tasks/human_eval_076.rs
+++ b/tasks/human_eval_076.rs
@@ -5,11 +5,42 @@ HumanEval/76
/*
### VERUS BEGIN
*/
+use vstd::arithmetic::logarithm::log;
+use vstd::arithmetic::power::pow;
use vstd::prelude::*;
-
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// note that the order of paramters is reverse in exec fn ilog and spec fn log
+#[verifier::external_fn_specification]
+pub fn ex_ilog(x: u32, base: u32) -> (ret: u32)
+ requires
+ x > 0,
+ base > 1,
+ ensures
+ ret == log(base as int, x as int),
+{
+ x.ilog(base)
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_checked_pow(x: u32, exp: u32) -> (ret: Option)
+ ensures
+ ret.is_some() <==> ret.unwrap() == pow(x as int, exp as nat),
+ ret.is_none() <==> pow(x as int, exp as nat) > u32::MAX,
+{
+ x.checked_pow(exp)
+}
+
+fn is_simple_power(x: u32, n: u32) -> (ret: bool)
+ requires
+ x > 0,
+ n > 1,
+ ensures
+ ret <==> x == pow(n as int, log(n as int, x as int) as nat),
+{
+ let maybe_x = n.checked_pow(x.ilog(n));
+ return maybe_x.is_some() && maybe_x.unwrap() == x;
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_077.rs b/tasks/human_eval_077.rs
index 957a9bb..bcb8d8a 100644
--- a/tasks/human_eval_077.rs
+++ b/tasks/human_eval_077.rs
@@ -5,11 +5,139 @@ HumanEval/77
/*
### VERUS BEGIN
*/
+use vstd::arithmetic::mul::*;
+use vstd::math::abs;
use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+proof fn lemma_cube_increases_helper(i: int)
+ ensures
+ i >= 0 ==> (i * i * i) <= (i + 1) * (i + 1) * (i + 1),
+{
+ broadcast use group_mul_properties;
+
+ if (i > 0) {
+ assert((i + 1) * (i + 1) * (i + 1) == i * i * i + 3 * i * i + 3 * i + 1);
+ assert(i * i * i + 3 * i * i + 3 * i + 1 > i * i * i);
+ }
+}
+
+proof fn lemma_cube_increases_params(i: int, j: int)
+ ensures
+ 0 <= i <= j ==> (i * i * i) <= (j * j * j),
+ decreases j - i,
+{
+ // base case
+ if (i == j) {
+ }
+ // inductive case
+ else if (i < j) {
+ lemma_cube_increases_params(i, j - 1);
+ lemma_cube_increases_helper(j - 1);
+
+ }
+}
+
+proof fn lemma_cube_increases()
+ ensures
+ forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j),
+{
+ assert forall|i: int, j: int|
+ 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j) by {
+ lemma_cube_increases_params(i, j);
+ }
+}
+
+fn checked_cube(x: i32) -> (ret: Option)
+ requires
+ x >= 0,
+ ensures
+ ret.is_some() ==> ret.unwrap() == x * x * x,
+ ret.is_none() ==> x * x * x > i32::MAX,
+{
+ //x == 0 done separately to invoke lemma_mul_increases which requires x > 0
+ if x == 0 {
+ return Some(0);
+ }
+ let sqr = x.checked_mul(x);
+ if sqr.is_some() {
+ let cube = sqr.unwrap().checked_mul(x);
+ if cube.is_some() {
+ let ans = cube.unwrap();
+ assert(ans == x * x * x);
+ Some(ans)
+ } else {
+ assert(x * x * x > i32::MAX);
+ None
+ }
+ } else {
+ assert(x > 0);
+ assert(x * x > i32::MAX);
+ proof {
+ lemma_mul_increases(x as int, x * x);
+ }
+ assert(x * x * x >= x * x);
+ None
+ }
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_abs(x: i32) -> (ret: i32)
+ requires
+ x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1
+
+ ensures
+ ret == abs(x as int),
+{
+ x.abs()
+}
+
+fn is_cube(x: i32) -> (ret: bool)
+ requires
+ x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1
+
+ ensures
+ ret <==> exists|i: int| 0 <= i && abs(x as int) == #[trigger] (i * i * i),
+{
+ let x_abs = x.abs();
+
+ // dealing with cases where the the cube is not greater than the number
+ if x_abs == 0 {
+ assert(abs(x as int) == 0 * 0 * 0);
+ return true;
+ } else if (x_abs == 1) {
+ assert(abs(x as int) == 1 * 1 * 1);
+ return true;
+ }
+ assert(-1 > x || x > 1);
+ let mut i = 2;
+ while i < x_abs
+ invariant
+ forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j),
+ 2 <= i <= abs(x as int) == x_abs,
+ {
+ let prod = checked_cube(i);
+ if prod.is_some() && prod.unwrap() == x.abs() {
+ return true;
+ }
+ i += 1;
+ }
+ assert(forall|j: int| 2 <= j ==> abs(x as int) != #[trigger] (j * j * j)) by {
+ assert(forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j));
+
+ assert(forall|j: int| i <= j ==> abs(x as int) < #[trigger] (j * j * j)) by {
+ assert(abs(x as int) < #[trigger] (i * i * i)) by {
+ broadcast use group_mul_properties;
+
+ assert(i <= i * i <= i * i * i);
+ }
+ lemma_cube_increases();
+ assert(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j));
+ }
+ }
+ false
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_080.rs b/tasks/human_eval_080.rs
index 0185958..cdae840 100644
--- a/tasks/human_eval_080.rs
+++ b/tasks/human_eval_080.rs
@@ -9,7 +9,44 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn three_distinct_spec(s: Seq, i: int) -> bool
+ recommends
+ 0 < i && i + 1 < s.len(),
+{
+ (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1])
+}
+
+fn three_distinct(s: &Vec, i: usize) -> (is: bool)
+ requires
+ 0 < i && i + 1 < s.len(),
+ ensures
+ is <==> three_distinct_spec(s@, i as int),
+{
+ (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1])
+}
+
+spec fn happy_spec(s: Seq) -> bool {
+ s.len() >= 3 && (forall|i: int| 0 < i && i + 1 < s.len() ==> three_distinct_spec(s, i))
+}
+
+#[verifier::loop_isolation(false)]
+fn is_happy(s: &Vec) -> (happy: bool)
+ ensures
+ happy <==> happy_spec(s@),
+{
+ if s.len() < 3 {
+ return false;
+ }
+ for i in 1..(s.len() - 1)
+ invariant
+ forall|j: int| 0 < j < i ==> three_distinct_spec(s@, j),
+ {
+ if !three_distinct(s, i) {
+ return false;
+ }
+ }
+ return true;
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_134.rs b/tasks/human_eval_134.rs
index f0a371a..727ff34 100644
--- a/tasks/human_eval_134.rs
+++ b/tasks/human_eval_134.rs
@@ -9,7 +9,39 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+pub uninterp spec fn is_alphabetic(c: char) -> (result: bool);
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(is_alphabetic)]
+pub fn ex_is_alphabetic(c: char) -> (result: bool)
+ ensures
+ result <==> (c.is_alphabetic()),
+{
+ c.is_alphabetic()
+}
+
+pub uninterp spec fn is_whitespace(c: char) -> (result: bool);
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(is_whitespace)]
+pub fn ex_is_whitespace(c: char) -> (result: bool)
+ ensures
+ result <==> (c.is_whitespace()),
+{
+ c.is_whitespace()
+}
+
+fn check_if_last_char_is_a_letter(txt: &str) -> (result: bool)
+ ensures
+ result <==> (txt@.len() > 0 && txt@.last().is_alphabetic() && (txt@.len() == 1
+ || txt@.index(txt@.len() - 2).is_whitespace())),
+{
+ let len = txt.unicode_len();
+ if len == 0 {
+ return false;
+ }
+ txt.get_char(len - 1).is_alphabetic() && (len == 1 || txt.get_char(len - 2).is_whitespace())
+}
} // verus!
fn main() {}
diff --git a/tasks/human_eval_136.rs b/tasks/human_eval_136.rs
index 04fda7e..cd5c489 100644
--- a/tasks/human_eval_136.rs
+++ b/tasks/human_eval_136.rs
@@ -9,7 +9,46 @@ use vstd::prelude::*;
verus! {
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn largest_smallest_integers(arr: &Vec) -> (res: (Option, Option))
+ ensures
+ ({
+ let a = res.0;
+ let b = res.1;
+ &&& a.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] >= 0
+ &&& a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0
+ &&& a.is_some() ==> forall|i: int|
+ 0 <= i < arr@.len() && arr@[i] < 0 ==> arr@[i] <= a.unwrap()
+ &&& b.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] <= 0
+ &&& b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0
+ &&& b.is_some() ==> forall|i: int|
+ 0 <= i < arr@.len() && arr@[i] > 0 ==> arr@[i] >= b.unwrap()
+ }),
+{
+ let mut i: usize = 0;
+ let mut a = None;
+ let mut b = None;
+
+ while i < arr.len()
+ invariant
+ 0 <= i <= arr@.len(),
+ a.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] >= 0,
+ a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0,
+ a.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] < 0 ==> arr@[j] <= a.unwrap(),
+ b.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] <= 0,
+ b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0,
+ b.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] > 0 ==> arr@[j] >= b.unwrap(),
+ decreases arr.len() - i,
+ {
+ if arr[i] < 0 && (a.is_none() || arr[i] >= a.unwrap()) {
+ a = Some(arr[i]);
+ }
+ if arr[i] > 0 && (b.is_none() || arr[i] <= b.unwrap()) {
+ b = Some(arr[i]);
+ }
+ i = i + 1;
+ }
+ (a, b)
+}
} // verus!
fn main() {}