More tasks completed (#12)

* Complete 098
* Complete 100
* Complete 102
* Complete 127
* Complete 130
* Complete 135
* Complete 138
* Complete 150
* Complete 152
* Complete 157
* Complete 159
* Complete 161
* Complete 163

---------

Co-authored-by: Bryan Parno <parno@cmu.edu>

tasks/human_eval_098.rs

@@ -6,10 +6,52 @@ HumanEval/98
 ### VERUS BEGIN
 */
 use vstd::prelude::*;
+use vstd::set::group_set_axioms;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+broadcast use group_set_axioms;
+
+spec fn spec_is_upper_vowel(c: char) -> bool {
+    c == 'A' || c == 'E' || c == 'I' || c == 'O' || c == 'U'
+}
+
+fn is_upper_vowel(c: char) -> (is: bool)
+    ensures
+        is <==> spec_is_upper_vowel(c),
+{
+    c == 'A' || c == 'E' || c == 'I' || c == 'O' || c == 'U'
+}
+
+#[verifier::loop_isolation(false)]
+fn count_upper(s: &[char]) -> (cnt: usize)
+    ensures
+        cnt == Set::new(|i: int| 0 <= i < s.len() && i % 2 == 0 && spec_is_upper_vowel(s[i])).len(),
+{
+    let ghost mut found = set![];
+    let mut cnt = 0;
+    for i in 0..s.len()
+        invariant
+            found.len() <= i,
+            found.finite(),
+            cnt == found.len(),
+            found =~= Set::new(|j: int| 0 <= j < i && j % 2 == 0 && spec_is_upper_vowel(s[j])),
+    {
+        if i % 2 == 0 && is_upper_vowel(s[i]) {
+            cnt = cnt + 1;
+            proof {
+                assert(!(0 <= i < i && i % 2 == 0 && spec_is_upper_vowel(s[i as int]))) by {
+                    assert(!(0 <= i < i));
+                };
+                assert(found.insert(i as int).len() == found.len() + 1) by {
+                    assert(!found.contains(i as int));
+                }
+                found = found.insert(i as int);
+            }
+        }
+    }
+    cnt
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_100.rs

@@ -9,7 +9,30 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn make_a_pile(n: usize) -> (pile: Vec<usize>)
+    requires
+        n + (2 * n) <= usize::MAX,
+    ensures
+        pile.len() == n,
+        n > 0 ==> pile[0] == n,
+        forall|i: int| #![trigger pile[i]] 1 <= i < n ==> pile[i] == pile[i - 1] + 2,
+{
+    if n == 0 {
+        return vec![];
+    }
+    let mut pile = vec![n];
+    for i in 1..n
+        invariant
+            pile.len() == i,
+            pile[i - 1] + (2 * (n - i)) <= usize::MAX,
+            forall|j: int| #![trigger pile[j]] 1 <= j < i ==> pile[j] == pile[j - 1] + 2,
+            n > 0 ==> pile[0] == n,
+    {
+        let prev = pile[i - 1];
+        pile.push(prev + 2);
+    }
+    pile
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_102.rs

@@ -9,7 +9,26 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn choose_num(x: u32, y: u32) -> (ret: i32)
+    requires
+        x <= i32::MAX && y <= i32::MAX,
+    ensures
+        ret != -1 ==> {
+            x <= ret <= y && ret % 2 == 0 && (forall|i: int|
+                #![trigger i % 2]
+                (x <= i <= y && i % 2 == 0) ==> i <= ret)
+        },
+        (ret == -1) <==> forall|i: int| #![trigger i % 2] x <= i <= y ==> i % 2 == 1,
+{
+    if x > y || (x == y && y % 2 == 1) {
+        return -1;
+    }
+    (if y % 2 == 0 {
+        y
+    } else {
+        y - 1
+    }) as i32
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_127.rs

@@ -5,11 +5,91 @@ HumanEval/127
 /*
 ### VERUS BEGIN
 */
+use vstd::math;
 use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn min(a: i32, b: i32) -> (m: i32)
+    ensures
+        m == math::min(a as int, b as int),
+{
+    if a < b {
+        a
+    } else {
+        b
+    }
+}
+
+fn max(a: i32, b: i32) -> (m: i32)
+    ensures
+        m == math::max(a as int, b as int),
+{
+    if a > b {
+        a
+    } else {
+        b
+    }
+}
+
+spec fn spec_prime_helper(num: int, limit: int) -> bool {
+    forall|j: int| 2 <= j < limit ==> (#[trigger] (num % j)) != 0
+}
+
+spec fn spec_prime(num: int) -> bool {
+    num >= 2 && spec_prime_helper(num, num)
+}
+
+fn is_prime_2(num: u64) -> (result: bool)
+    requires
+        num >= 2,
+    ensures
+        result <==> spec_prime(num as int),
+{
+    let mut i = 2;
+    let mut result = true;
+    while i < num
+        invariant
+            2 <= i <= num,
+            result <==> spec_prime_helper(num as int, i as int),
+    {
+        if num % i == 0 {
+            result = false;
+        }
+        i += 1;
+    }
+    result
+}
+
+fn is_prime(num: i64) -> (is: bool)
+    requires
+        num >= 0,
+    ensures
+        is <==> (num >= 2 && spec_prime(num as int)),
+{
+    num >= 2 && is_prime_2(num as u64)
+}
+
+fn intersection(a: (i32, i32), b: (i32, i32)) -> (result: &'static str)
+    requires
+        a.0 <= a.1 && b.0 <= b.1,
+    ensures
+        result == "YES" || result == "NO",
+        result == "YES" <==> {
+            let left = math::max(a.0 as int, b.0 as int);
+            let right = math::min(a.1 as int, b.1 as int);
+            left <= right && spec_prime(right - left + 1)
+        },
+{
+    let sect_start = max(a.0, b.0);
+    let sect_end = min(a.1, b.1);
+
+    if sect_start < sect_end && is_prime(sect_end as i64 - sect_start as i64 + 1) {
+        "YES"
+    } else {
+        "NO"
+    }
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_130.rs

@@ -9,7 +9,93 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_tri(n: nat) -> nat
+    decreases
+            if n % 2 == 0 {
+                0
+            } else {
+                n
+            },
+{
+    if n == 1 {
+        3
+    } else if n % 2 == 0 {
+        1 + n / 2
+    } else {
+        spec_tri((n - 1) as nat) + spec_tri((n - 2) as nat) + spec_tri(n + 1)
+    }
+}
+
+fn checked_add_three(a: Option<u32>, b: Option<u32>, c: Option<u32>) -> (r: Option<u32>)
+    ensures
+        r.is_some() && a.is_some() && b.is_some() && c.is_some() ==> r.unwrap() == a.unwrap()
+            + b.unwrap() + c.unwrap(),
+        a.is_none() || b.is_none() || c.is_none() ==> r.is_none(),
+        !(a.is_none() || b.is_none() || c.is_none()) && r.is_none() ==> a.unwrap() + b.unwrap()
+            + c.unwrap() > u32::MAX,
+{
+    a?.checked_add(b?)?.checked_add(c?)
+}
+
+#[verifier::loop_isolation(false)]
+fn tri(n: u32) -> (result: Vec<Option<u32>>)
+    requires
+        n + 1 <= u32::MAX,
+    ensures
+        result.len() == n + 1,
+        forall|i: int|
+            #![trigger result[i]]
+            0 <= i < result.len() ==> {
+                (result[i].is_some() ==> result[i].unwrap() == spec_tri(i as nat)) && (
+                result[i].is_none() ==> spec_tri(i as nat) > u32::MAX)
+            },
+{
+    if n == 0 {
+        vec![Some(1)]
+    } else {
+        let mut result: Vec<Option<u32>> = vec![Some(1), Some(3)];
+        let mut i = 2;
+        while i <= n
+            invariant
+                2 <= i <= n + 1,
+                result.len() == i,
+                forall|j: int|
+                    #![trigger result[j]]
+                    0 <= j < i ==> ((result[j].is_some() ==> result[j].unwrap() == spec_tri(
+                        j as nat,
+                    )) && (result[j].is_none() ==> spec_tri(j as nat) > u32::MAX)),
+        {
+            if i % 2 == 0 {
+                result.push(Some(1 + (i / 2)));
+                assert(result[i as int].unwrap() == spec_tri(i as nat));
+            } else {
+                assert((i + 1) / 2 + 1 == (i + 3) / 2);
+                let cur = checked_add_three(
+                    result[i as usize - 2],
+                    result[i as usize - 1],
+                    Some((i + 1) / 2 + 1),
+                );
+                proof {
+                    if result[i - 2].is_some() && result[i - 1].is_some() {
+                        assert(result[i - 2].unwrap() == spec_tri((i - 2) as nat));
+                        assert(result[i - 1].unwrap() == spec_tri((i - 1) as nat));
+                        assert((i + 3) / 2 == spec_tri((i + 1) as nat));
+                    } else {
+                        assert(cur.is_none());
+                    }
+                    assert(cur.is_some() ==> cur.unwrap() == spec_tri(i as nat));
+                }
+                result.push(cur);
+                assert(result[i as int].is_some() ==> result[i as int].unwrap() == spec_tri(
+                    i as nat,
+                ));
+            }
+            i += 1;
+        }
+        assert(result.len() == n + 1);
+        result
+    }
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_135.rs

@@ -9,7 +9,32 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+#[verifier::loop_isolation(false)]
+fn can_arrange(arr: &Vec<i32>) -> (pos: i32)
+    requires
+        forall|i: int, j: int| 0 <= i < j < arr.len() ==> arr[i] != arr[j],
+        arr.len() + 1 < i32::MAX,
+    ensures
+        pos == -1 ==> forall|i: int| #![trigger arr[i]] 1 <= i < arr.len() ==> arr[i] >= arr[i - 1],
+        pos >= 0 ==> 1 <= pos < arr.len() && arr[pos as int] < arr[pos - 1],
+        pos >= 0 ==> forall|i: int| #![trigger arr[i]] pos < i < arr.len() ==> arr[i] >= arr[i - 1],
+{
+    if arr.len() == 0 {
+        return -1;
+    }
+    let mut pos = -1;
+    for i in 1..arr.len()
+        invariant
+            pos == -1 ==> forall|j: int| #![trigger arr[j]] 1 <= j < i ==> arr[j] >= arr[j - 1],
+            pos >= 0 ==> 1 <= pos < i && arr[pos as int] < arr[pos - 1],
+            pos >= 0 ==> forall|j: int| #![trigger arr[j]] pos < j < i ==> arr[j] >= arr[j - 1],
+    {
+        if arr[i] < arr[i - 1] {
+            pos = i as i32;
+        }
+    }
+    pos
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_138.rs

@@ -9,7 +9,12 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn is_equal_to_sum_even(n: u32) -> (b: bool)  // 2 + 2 + 2 + (n - 6)
+    ensures
+        b <==> n % 2 == 0 && n >= 8,
+{
+    n % 2 == 0 && n >= 8
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_150.rs

@@ -9,7 +9,46 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_prime_helper(num: int, limit: int) -> bool {
+    forall|j: int| 2 <= j < limit ==> (#[trigger] (num % j)) != 0
+}
+
+spec fn spec_prime(num: int) -> bool {
+    num >= 2 && spec_prime_helper(num, num)
+}
+
+fn is_prime(num: u32) -> (result: bool)
+    requires
+        num >= 2,
+    ensures
+        result <==> spec_prime(num as int),
+{
+    let mut i = 2;
+    let mut result = true;
+    while i < num
+        invariant
+            2 <= i <= num,
+            result <==> spec_prime_helper(num as int, i as int),
+    {
+        if num % i == 0 {
+            result = false;
+        }
+        i += 1;
+    }
+    result
+}
+
+fn x_or_y(n: u32, x: i32, y: i32) -> (result: i32)
+    ensures
+        spec_prime(n as int) ==> result == x,
+        !spec_prime(n as int) ==> result == y,
+{
+    if n >= 2 && is_prime(n) {
+        x
+    } else {
+        y
+    }
+}
 
 } // verus!
 fn main() {}