add verus humaneval

.gitignore

@@ -7,3 +7,5 @@ clover_mbpp/exp_results_k_10.log
 clover_mbpp/clover_mbpp_results.json
 *.swp
 **/tmp/
+target/
+*.code-workspace

dataset/verus_humaneval/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "verus_humaneval"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

dataset/verus_humaneval/Notes.md

@@ -0,0 +1,6 @@
+# HumanEval to Verus Compatibility Notes
+
+Features that are not supported by Verus are reported here.
+
+- 0: `f32::abs` is not supported.
+- 43: iterator `enumerate` is not supported, but you can use `for` loop to achieve the same effect.

dataset/verus_humaneval/src/_rust_0.rs

@@ -0,0 +1,61 @@
+fn main() {}
+use vstd::{prelude::*};
+/*
+ Check if in given list of numbers, are any two numbers closer to each other than
+    given threshold.
+
+*/
+verus! {
+fn has_close_elements(numbers: Vec<f32>, threshold: f32) -> (r: bool)
+    ensures
+        r == (exists |i: int, j: int| 0 <= i < numbers.len() && 0 <= j < numbers.len() && i != j && (numbers[i] - numbers[j]).abs() < threshold)
+{
+    for i in 0..numbers.len() {
+        for j in 1..numbers.len() {
+            if i != j {
+                let distance: f32 = numbers[i] - numbers[j];
+
+                if distance.abs() < threshold {
+                    return true;
+                }
+            }
+        }
+    }
+
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_has_close_elements() {
+        assert_eq!(
+            has_close_elements(vec![11.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.3),
+            true
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.05),
+            false
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 5.9, 4.0, 5.0], 0.95),
+            true
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 5.9, 4.0, 5.0], 0.8),
+            false
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 3.0, 4.0, 5.0, 2.0], 0.1),
+            true
+        );
+        assert_eq!(has_close_elements(vec![1.1, 2.2, 3.1, 4.1, 5.1], 1.0), true);
+        assert_eq!(
+            has_close_elements(vec![1.1, 2.2, 3.1, 4.1, 5.1], 0.5),
+            false
+        );
+    }
+}

dataset/verus_humaneval/src/main.rs

@@ -0,0 +1 @@
+fn main () {}

dataset/verus_humaneval/src/rust_3.rs

@@ -0,0 +1,77 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+    You're given a list of deposit and withdrawal operations on a bank account that starts with
+    zero balance. Your task is to detect if at any point the balance of account fallls below zero, and
+    at that point function should return True. Otherwise it should return False.
+*/
+
+
+verus! {
+// spec fn sum(v: Vec<i32>, start: int, end: int) -> (r: int)
+//     recommends 0 <= start && start <= end && end <= v.len(),
+//     decreases end - start
+// {
+//     if start == end {
+//         0
+//     } else {
+//         v[start] + sum(v, start + 1, end)
+//     }
+// }
+spec fn sum(v: Vec<i32>, start: int, len: nat) -> (r: int)
+    recommends 0 <= start && start + len <= v.len(),
+    decreases len
+{
+    if len == 0 {
+        0
+    } else {
+        sum(v, start, (len - 1) as nat) + v[start + len as int - 1]
+    }
+}
+
+fn below_zero(operations: Vec<i32>) -> (r: bool)
+    requires
+        forall|i: int| 0 <= i < operations.len() ==> -0x1fff_ffff <= #[trigger] operations[i] <= 0x1fff_ffff,
+        forall|i: int| 0 <= i <= operations.len() ==> -0x1fff_ffff <= #[trigger] sum(operations, 0, i as nat) <= 0x1fff_ffff,
+    ensures
+        r == (exists |i: int| 0 <= i <= operations.len() && #[trigger] sum(operations, 0, i as nat) < 0),
+{
+    let mut balance: i32 = 0;
+    for n in 0..operations.len()
+        invariant
+            0 <= n <= operations.len(),
+            balance == sum(operations, 0, n as nat),
+            forall|i: int| 0 <= i <= n ==> #[trigger] sum(operations, 0, i as nat) >= 0,
+            // overflow checks
+            -0x1fff_ffff <= balance <= 0x1fff_ffff,
+            forall|i: int| 0 <= i < operations.len() ==> -0x1fff_ffff <= #[trigger] operations[i] <= 0x1fff_ffff,
+            forall|i: int| 0 <= i <= operations.len() ==> -0x1fff_ffff <= #[trigger] sum(operations, 0, i as nat) <= 0x1fff_ffff,
+    {
+        let op = operations[n];
+        assert(-0x1fff_ffff <= operations[n as int] <= 0x1fff_ffff);
+        balance = balance + op;
+        assert(balance == sum(operations, 0, (n + 1) as nat));
+        assert(-0x1fff_ffff <= balance <= 0x1fff_ffff);
+        if balance < 0 {
+            return true;
+        }
+    }
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_below_zero() {
+        assert_eq!(below_zero(vec![]), false);
+        assert_eq!(below_zero(vec![1, 2, -3, 1, 2, -3]), false);
+        assert_eq!(below_zero(vec![1, 2, -4, 5, 6]), true);
+        assert_eq!(below_zero(vec![1, -1, 2, -2, 5, -5, 4, -4]), false);
+        assert_eq!(below_zero(vec![1, -1, 2, -2, 5, -5, 4, -5]), true);
+        assert_eq!(below_zero(vec![1, -2, 2, -2, 5, -5, 4, -4]), true);
+    }
+}

dataset/verus_humaneval/src/rust_31.rs

@@ -0,0 +1,66 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return true if a given number is IsPrime, and false otherwise.
+*/
+
+verus! {
+// reference: https://github.com/verus-lang/verus/blob/55b24eea93ad3dc907a4219e8b58a2f5f3f43afb/source/rust_verify/example/rw2022_script.rs#L36C1-L69C2
+
+spec fn divides(factor: nat, candidate: nat) -> bool {
+    candidate % factor == 0
+}
+
+spec fn IsPrime(candidate: nat) -> bool {
+    1 < candidate &&
+    forall|factor: nat| 1 < factor < candidate ==> !divides(factor, candidate)
+}
+
+fn is_prime(n: u32) -> (result: bool)
+    requires
+        1 < n,
+    ensures
+        result == IsPrime(n as nat),
+{
+    if n < 2 {
+        return false;
+    }
+    for k in 2..n
+        invariant
+            1 < k <= n,
+            forall|smallerfactor: nat|
+                1 < smallerfactor < k ==> !divides(smallerfactor, n as nat),
+    {
+        assert(1 < k < n);
+        if n % k == 0 {
+            assert(divides(k as nat, n as nat));
+            assert(!IsPrime(n as nat));
+            return false;
+        }
+    }
+    return true;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_is_prime() {
+        assert!(is_prime(6) == false);
+        assert!(is_prime(101) == true);
+        assert!(is_prime(11) == true);
+        assert!(is_prime(13441) == true);
+        assert!(is_prime(61) == true);
+        assert!(is_prime(4) == false);
+        assert!(is_prime(1) == false);
+        assert!(is_prime(5) == true);
+        assert!(is_prime(11) == true);
+        assert!(is_prime(17) == true);
+        assert!(is_prime(5 * 17) == false);
+        assert!(is_prime(11 * 7) == false);
+        assert!(is_prime(13441 * 19) == false);
+    }
+}

dataset/verus_humaneval/src/rust_35.rs

@@ -0,0 +1,39 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return maximum element in the list.
+*/
+
+verus! {
+fn maximum(nmbs: Vec<i32>) -> (r: i32)
+    requires
+        nmbs.len() > 0,
+    ensures
+        forall|i: int| 0 <= i < nmbs.len() ==> nmbs[i] <= r,
+        exists|i: int| 0 <= i < nmbs.len() && r == nmbs[i],
+{
+    let mut max = nmbs[0];
+    for i in 1..nmbs.len()
+        invariant
+            forall|j: int| 0 <= j < i ==> nmbs[j] <= max,
+            exists|j: int| 0 <= j < i && max == nmbs[j],
+    {
+        if nmbs[i] > max {
+            max = nmbs[i];
+        }
+    }
+    max
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_maximum() {
+        assert!(maximum(vec![1, 2, 3]) == 3);
+        assert!(maximum(vec![5, 3, -5, 2, -3, 3, 9, 0, 124, 1, -10]) == 124);
+    }
+}

dataset/verus_humaneval/src/rust_43.rs

@@ -0,0 +1,59 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+    pairs_sum_to_zero takes a list of integers as an input.
+    it returns True if there are two distinct elements in the list that
+    sum to zero, and False otherwise.
+*/
+
+verus! {
+fn pairs_sum_to_zero(l: Vec<i32>) -> (r: bool)
+    requires
+        forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+    ensures
+        r == (exists |i: int, j: int| 0 <= i < j < l.len() && l[i as int] + l[j as int] == 0)
+{
+    for i in 0..l.len()
+        invariant
+            0 <= i <= l.len(),
+            forall|i_: int, j_: int| 0 <= i_ < i && i_ < j_ < l.len() ==> l[i_ as int] + l[j_ as int] != 0,
+            // overflow check
+            forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+    {
+        for j in i + 1..l.len()
+            invariant
+                i < j <= l.len(),
+                forall|j_: int| i < j_ < j ==> l[i as int] + l[j_ as int] != 0,
+                // overflow check
+                forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+        {
+            assert(-0x1000_0000 <= l[i as int] <= 0x1000_0000);
+            assert(-0x1000_0000 <= l[j as int] <= 0x1000_0000);
+            if l[i] + l[j] == 0 {
+                return true;
+            }
+        }
+    }
+
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_pairs_sum_to_zero() {
+        assert!(pairs_sum_to_zero(vec![1, 3, 5, 0]) == false);
+        assert!(pairs_sum_to_zero(vec![1, 3, -2, 1]) == false);
+        assert!(pairs_sum_to_zero(vec![1, 2, 3, 7]) == false);
+        assert!(pairs_sum_to_zero(vec![2, 4, -5, 3, 5, 7]) == true);
+        assert!(pairs_sum_to_zero(vec![1]) == false);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 3, 2, 30]) == true);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 3, 2, 31]) == true);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 4, 2, 30]) == false);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 4, 2, 31]) == false);
+    }
+}

dataset/verus_humaneval/src/rust_49.rs

@@ -0,0 +1,54 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return 2^n modulo p (be aware of numerics).
+*/
+
+verus! {
+spec fn Modp(n: nat, p: nat) -> nat
+    decreases n
+{
+    if n == 0 {
+        1
+    } else {
+        (Modp((n - 1) as nat, p) * 2) % p
+    }
+}
+
+fn modp(n: u32, p: u32) -> (result: u32)
+    requires
+        p > 0,
+        p <= 0x1000_0000,
+    ensures
+        result == Modp(n as nat, p as nat),
+{
+    let mut res = 1;
+    let mut i = 0;
+    while i < n
+        invariant
+            i <= n, 0 < p <= 0x1000_0000, res <= 0x1000_0000,
+            res == Modp(i as nat, p as nat),
+    {
+        res = (res * 2) % p;
+        i = i + 1;
+    }
+    res
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_modp() {
+        assert!(modp(3, 5) == 3);
+        assert!(modp(1101, 101) == 2);
+        assert!(modp(0, 101) == 1);
+        assert!(modp(3, 11) == 8);
+        assert!(modp(100, 101) == 1);
+        assert!(modp(30, 5) == 4);
+        assert!(modp(31, 5) == 3);
+    }
+}