wrote some programs

tasks/human_eval_053.rs

@@ -9,7 +9,12 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+fn add (x: i32, y: i32) -> (res: Option<i32>)
+    ensures
+        res.is_some() ==> res.unwrap() == x + y
+{
+    x.checked_add(y)
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_055.rs

@@ -9,7 +9,32 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_fib(n: nat) -> nat 
+    decreases n
+{
+    if (n == 0){
+        0
+    } else if (n == 1) {
+        1
+    } else {
+        spec_fib((n - 1) as nat) + spec_fib((n - 2) as nat)
+    }
+}
+
+fn fib(n: u32) -> (ret: Option<u32>)
+    ensures
+        ret.is_some() ==> ret.unwrap() == spec_fib(n as nat)
+{
+    match n {
+        0 => Some(0),
+        1 => Some(1),
+        _ => {
+            let n1 = fib(n - 1)?;
+            let n2 = fib(n - 2)?;
+            n1.checked_add(n2)
+        }
+    }
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_056.rs

@@ -9,7 +9,53 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_bracketing_helper(brackets: Seq<char>) -> (int, bool) {
+    brackets.fold_left((0, true), |p: (int, bool), c| {
+        let (x, b) = p;
+        match (c) {
+            '<' => (x + 1, b),
+            '>' => (x - 1 , b && x == 0),
+            _ => (x, b),
+        }
+    })
+}
+
+spec fn spec_bracketing(brackets: Seq<char>) -> bool {
+    let p = spec_bracketing_helper(brackets);
+    p.1 && p.0 == 0
+}
+
+fn correct_bracketing(brackets: &str) -> (ret: bool)
+    requires
+        [email protected]() <= i32::MAX
+        [email protected]() >= i32::MIN
+    ensures
+        ret <==> spec_bracketing(brackets@)
+{
+    let mut i = 0;
+    let mut b = true;
+    let mut stack_size: i32 = 0;
+
+    while i < brackets.unicode_len()
+        invariant
+            (stack_size as int, b) == spec_bracketing_helper([email protected](0, i as int)),
+            stack_size <=  i <=  [email protected]() <= i32::MAX,
+            stack_size >= -i >= [email protected]() >= i32::MIN,
+    {
+        let c = brackets.get_char(i);
+        let ghost prev = spec_bracketing_helper([email protected](0, i as int));
+        if (c == '<') {
+            stack_size += 1;
+        } else if (c == '>') {
+            b = b && stack_size == 0;
+            stack_size -= 1;
+        }
+        assert([email protected](0, i+1 as int).drop_last() =~= [email protected](0, i as int));
+        i += 1;
+    }
+    assert(brackets@ =~= [email protected](0, i as int));
+    b && stack_size == 0
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_057.rs

@@ -9,8 +9,35 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
-
+fn monotonic(l: Vec<i32>) -> (ret: bool)
+    ensures
+        ret <==> forall |i: int, j: int| 0 <= i < j < [email protected]() ==> [email protected](i) <= [email protected](j) ||
+                 forall |i: int, j: int| 0 <= i < j < [email protected]() ==> [email protected](i) >= [email protected](j)
+{
+    if l.len() == 0 || l.len() == 1 {
+        return true;
+    }
+
+    let mut increasing = true;
+    let mut decreasing = true;
+
+    let mut n = 0;
+    while n < l.len() - 1 
+        invariant
+            l.len() > 1,
+            n <= l.len() - 1,
+            increasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> [email protected](i) <= [email protected](j),
+            decreasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> [email protected](i) >= [email protected](j),
+    {
+        if l[n] < l[n + 1] {
+            decreasing = false;
+        } else if l[n] > l[n + 1] {
+            increasing = false;
+        }
+        n += 1;
+    }
+    increasing || decreasing
+}
 } // verus!
 fn main() {}
 

tasks/human_eval_059.rs

@@ -8,8 +8,57 @@ HumanEval/59
 use vstd::prelude::*;
 
 verus! {
-
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+// Note that according to the canonical solution 1 is treated as a possible largest prime. We'll stick to this
+
+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 {
+    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 largest_prime_factor(n: u32) -> (largest: u32)
+    requires n >= 2,
+    ensures 
+        1 <= largest <= n,
+        spec_prime(largest as int),
+{
+    let mut largest = 1;
+    let mut j = 1;
+    while j < n
+        invariant 
+            1 <= largest <= j <= n,
+            spec_prime(largest as int),
+
+    {
+        j += 1;
+        let flag = is_prime(j);
+        if n % j == 0 && flag {
+            largest = if largest > j { largest } else { j };
+        }
+    }
+    largest
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_060.rs

@@ -9,7 +9,34 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_sum_to_n(n: nat) -> nat
+    decreases n
+{
+    if (n == 0) {
+        0
+    } else {
+        n + spec_sum_to_n((n-1) as nat)
+    }
+}
+
+fn sum_to_n(n: u32) -> (sum: Option<u32>)
+    ensures
+        sum.is_some() ==> sum.unwrap() == spec_sum_to_n(n as nat),
+{
+    let mut res: u32 = 0;
+    let mut sum: u32 = 0;
+    let mut i: u32 = 0;
+    while i < n
+        invariant
+            i <= n,
+            res == spec_sum_to_n(i as nat),
+            res <= u32::MAX,
+    {
+        i += 1;
+        res = i.checked_add(res)?;
+    }
+    Some(res)
+}
 
 } // verus!
 fn main() {}

tasks/human_eval_061.rs

@@ -9,7 +9,53 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn spec_bracketing_helper(brackets: Seq<char>) -> (int, bool) {
+    brackets.fold_left((0, true), |p: (int, bool), c| {
+        let (x, b) = p;
+        match (c) {
+            '(' => (x + 1, b),
+            ')' => (x - 1 , b && x == 0),
+            _ => (x, b),
+        }
+    })
+}
+
+spec fn spec_bracketing(brackets: Seq<char>) -> bool {
+    let p = spec_bracketing_helper(brackets);
+    p.1 && p.0 == 0
+}
+
+fn correct_bracketing(brackets: &str) -> (ret: bool)
+    requires
+        [email protected]() <= i32::MAX
+        [email protected]() >= i32::MIN
+    ensures
+        ret <==> spec_bracketing(brackets@)
+{
+    let mut i = 0;
+    let mut b = true;
+    let mut stack_size: i32 = 0;
+
+    while i < brackets.unicode_len()
+        invariant
+            (stack_size as int, b) == spec_bracketing_helper([email protected](0, i as int)),
+            stack_size <=  i <=  [email protected]() <= i32::MAX,
+            stack_size >= -i >= [email protected]() >= i32::MIN,
+    {
+        let c = brackets.get_char(i);
+        let ghost prev = spec_bracketing_helper([email protected](0, i as int));
+        if (c == '(') {
+            stack_size += 1;
+        } else if (c == ')') {
+            b = b && stack_size == 0;
+            stack_size -= 1;
+        }
+        assert([email protected](0, i+1 as int).drop_last() =~= [email protected](0, i as int));
+        i += 1;
+    }
+    assert(brackets@ =~= [email protected](0, i as int));
+    b && stack_size == 0
+}
 
 } // verus!
 fn main() {}