Merge branch 'main' of https://github.com/JetBrains-Research/verified…

…-cogen

.gitignore

@@ -20,4 +20,8 @@ run_nagini.py
 /tmp
 results
 results/*
+/log_tries/
+/log_tries/*
 .direnv
+scripts/processed
+scripts/processed/*

.gitmodules

@@ -5,3 +5,7 @@
 [submodule "benches/HumanEval-Dafny"]
 	path = benches/HumanEval-Dafny
 	url = https://github.com/JetBrains-Research/HumanEval-Dafny
+
+[submodule "benches/HumanEval-Nagini"]
+	path = benches/HumanEval-Nagini
+	url = https://github.com/JetBrains-Research/HumanEval-Nagini

benches/HumanEval-RustBench/000-has_close_elements.rs

@@ -0,0 +1,69 @@
+use vstd::math::abs;
+use vstd::prelude::*;
+use vstd::slice::*;
+
+verus! {
+fn has_close_elements(numbers: &[i64], threshold: i64) -> (result: bool)
+    // post-conditions-start
+    ensures
+        result == exists|i: int, j: int|
+            0 <= i < j < [email protected]() && abs(numbers[i] - numbers[j]) < threshold,
+    // post-conditions-end
+{
+    // impl-start
+    if threshold <= 0 {
+        // assert-start
+        assert(forall|i: int, j: int|
+            0 <= i < j < [email protected]() ==> abs(numbers[i] - numbers[j]) >= 0 >= threshold);
+        // assert-end
+        return false;
+    }
+    let max_minus_threshold: i64 = i64::MAX - threshold;
+    let numbers_len: usize = numbers.len();
+    for x in 0..numbers_len
+        // invariants-start
+        invariant
+            max_minus_threshold == i64::MAX - threshold,
+            numbers_len == [email protected](),
+            forall|i: int, j: int|
+                0 <= i < j < [email protected]() && i < x ==> abs(numbers[i] - numbers[j]) >= threshold,
+        // invariants-end
+    {
+        let numbers_x: i64 = *slice_index_get(numbers, x);
+        for y in x + 1..numbers_len
+            // invariants-start
+            invariant
+                max_minus_threshold == i64::MAX - threshold,
+                numbers_len == [email protected](),
+                x < [email protected](),
+                numbers_x == numbers[x as int],
+                forall|i: int, j: int|
+                    0 <= i < j < [email protected]() && i < x ==> abs(numbers[i] - numbers[j])
+                        >= threshold,
+                forall|j: int| x < j < y ==> abs(numbers_x - numbers[j]) >= threshold,
+            // invariants-end
+        {
+            let numbers_y = *slice_index_get(numbers, y);
+            if numbers_x > numbers_y {
+                if numbers_y > max_minus_threshold {
+                    return true;
+                }
+                if numbers_x < numbers_y + threshold {
+                    return true;
+                }
+            } else {
+                if numbers_x > max_minus_threshold {
+                    return true;
+                }
+                if numbers_y < numbers_x + threshold {
+                    return true;
+                }
+            }
+        }
+    }
+    false
+    // impl-end
+}
+
+}
+fn main() {}

benches/HumanEval-RustBench/001-separate-paren-groups.rs

@@ -0,0 +1,188 @@
+use vstd::prelude::*;
+
+verus! {
+pub open spec fn nesting_level(input: Seq<char>) -> int
+    decreases input.len(),
+{
+    // impl-start
+    if input.len() == 0 {
+        0
+    } else {
+        let prev_nesting_level = nesting_level(input.drop_last());
+        let c = input.last();
+        if c == '(' {
+            prev_nesting_level + 1
+        } else if c == ')' {
+            prev_nesting_level - 1
+        } else {
+            prev_nesting_level
+        }
+    }
+    // impl-end
+}
+
+pub open spec fn is_paren_char(c: char) -> bool {
+    c == '(' || c == ')'
+}
+pub open spec fn is_balanced_group(input: Seq<char>) -> bool {
+    &&& input.len() > 0
+    &&& nesting_level(input) == 0
+    &&& forall|i| 0 <= i < input.len() ==> is_paren_char(#[trigger] input[i])
+    &&& forall|i| 0 < i < input.len() ==> nesting_level(#[trigger] input.take(i)) > 0
+}
+pub open spec fn is_sequence_of_balanced_groups(input: Seq<char>) -> bool {
+    &&& nesting_level(input) == 0
+    &&& forall|i| 0 < i < input.len() ==> nesting_level(#[trigger] input.take(i)) >= 0
+}
+
+pub open spec fn vecs_to_seqs<T>(s: Seq<Vec<T>>) -> Seq<Seq<T>> {
+    s.map(|_i, ss: Vec<T>| ss@)
+}
+
+pub open spec fn remove_nonparens(s: Seq<char>) -> Seq<char> {
+    s.filter(|c| is_paren_char(c))
+}
+proof fn lemma_remove_nonparens_maintained_by_push(s: Seq<char>, pos: int)
+    // pre-conditions-start
+    requires
+        0 <= pos < s.len(),
+    // pre-conditions-end
+    // post-conditions-start
+    ensures
+        ({
+            let s1 = remove_nonparens(s.take(pos as int));
+            let s2 = remove_nonparens(s.take((pos + 1) as int));
+            if is_paren_char(s[pos]) {
+                s2 == s1.push(s[pos])
+            } else {
+                s2 == s1
+            }
+        }),
+    // post-conditions-end
+    decreases pos,
+{
+    // impl-start
+    reveal(Seq::filter);
+    assert(s.take((pos + 1) as int).drop_last() =~= s.take(pos as int)); // assert-line
+    if pos != 0 {
+        lemma_remove_nonparens_maintained_by_push(s, pos - 1);
+    }
+    // impl-end
+}
+fn separate_paren_groups(input: &Vec<char>) -> (groups: Vec<Vec<char>>)
+    // pre-conditions-start
+    requires
+        is_sequence_of_balanced_groups(input@),
+    // pre-conditions-end
+    // post-conditions-start
+    ensures
+        forall|i: int|
+            #![trigger groups[i]]
+            0 <= i < groups.len() ==> is_balanced_group(groups[i]@),
+        vecs_to_seqs(groups@).flatten() == remove_nonparens(input@),
+    // post-conditions-end
+{
+    // impl-start
+    let mut groups: Vec<Vec<char>> = Vec::new();
+    let mut current_group: Vec<char> = Vec::new();
+    let input_len = input.len();
+    let ghost mut ghost_groups: Seq<Seq<char>> = Seq::empty();
+    // assert-start
+    proof {
+        assert(vecs_to_seqs(groups@) =~= ghost_groups);
+        assert(remove_nonparens([email protected](0)) =~= Seq::<char>::empty());
+        assert(ghost_groups.flatten() + current_group@ =~= Seq::<char>::empty());
+    }
+    // assert-end
+    let mut current_nesting_level: usize = 0;
+    for pos in 0..input_len
+        // invariants-start
+        invariant
+            input_len == input.len(),
+            ghost_groups == vecs_to_seqs(groups@),
+            ghost_groups.flatten() + current_group@ == remove_nonparens([email protected](pos as int)),
+            forall|i: int|
+                #![trigger groups[i]]
+                0 <= i < ghost_groups.len() ==> is_balanced_group(ghost_groups[i]),
+            current_nesting_level == nesting_level([email protected](pos as int)),
+            current_nesting_level == nesting_level(current_group@),
+            current_nesting_level <= pos,
+            [email protected]() == 0 <==> current_nesting_level == 0,
+            forall|i| 0 <= i < [email protected]() ==> is_paren_char(#[trigger] current_group@[i]),
+            forall|i|
+                0 < i < [email protected]() ==> nesting_level(#[trigger] [email protected](i))
+                    > 0,
+            is_sequence_of_balanced_groups(input@),
+        // invariants-end
+    {
+        let ghost prev_group = current_group@;
+        let ghost prev_groups = ghost_groups;
+        let c = input[pos];
+        proof {
+            assert([email protected]((pos + 1) as int) == [email protected](pos as int).push(c)); // assert-line
+            assert([email protected]((pos + 1) as int).drop_last() == [email protected](pos as int)); // assert-line
+            lemma_remove_nonparens_maintained_by_push(input@, pos as int);
+        }
+        if c == '(' {
+            current_nesting_level = current_nesting_level + 1;
+            current_group.push('(');
+            assert([email protected]_last() == prev_group); // assert-line
+            // assert-start
+            assert(ghost_groups.flatten() + current_group@ =~= (ghost_groups.flatten()
+                + prev_group).push('('));
+            ));
+            // assert-end
+            // assert-start
+            assert(forall|i|
+                0 < i < prev_group.len() ==> #[trigger] [email protected](i) == prev_group.take(
+                    i,
+                ));
+            // assert-end
+        } else if c == ')' {
+            current_nesting_level = current_nesting_level - 1;
+            current_group.push(')');
+            assert([email protected]_last() == prev_group); // assert-line
+            // assert-start
+            assert(ghost_groups.flatten() + current_group@ =~= (ghost_groups.flatten()
+                + prev_group).push(')'));
+            // assert-end
+            // assert-start
+            assert(forall|i|
+                0 < i < prev_group.len() ==> #[trigger] [email protected](i) == prev_group.take(
+                    i,
+                ));
+            // assert-end
+            if current_nesting_level == 0 {
+                proof {
+                    ghost_groups = ghost_groups.push(current_group@);
+                    // assert-start
+                    assert(vecs_to_seqs([email protected](current_group)) =~= vecs_to_seqs(groups@).push(
+                        current_group@,
+                    ));
+                    // assert-end
+                    assert(ghost_groups.drop_last() == prev_groups); // assert-line
+                    // assert-start
+                    assert(ghost_groups.flatten() =~= prev_groups.flatten() + current_group@) by {
+                        prev_groups.lemma_flatten_and_flatten_alt_are_equivalent();
+                        ghost_groups.lemma_flatten_and_flatten_alt_are_equivalent();
+                    }
+                    // assert-end
+                }
+                groups.push(current_group);
+                current_group = Vec::<char>::new();
+                // assert-start
+                assert(ghost_groups.flatten() + current_group@ =~= remove_nonparens(
+                    [email protected]((pos + 1) as int),
+                ));
+                // assert-end
+            }
+        }
+    }
+    assert([email protected](input_len as int) =~= input@); // assert-line
+    assert(ghost_groups.flatten() + current_group@ == ghost_groups.flatten()); // assert-line
+    groups
+    // impl-end
+}
+
+}
+fn main() {}