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

Author: alex28sh

.git-blame-ignore-revs

@@ -0,0 +1 @@
+40ba9a26ce77a4720a5a2ee00007c8c5acb4ea1c

.gitignore

@@ -27,3 +27,4 @@ scripts/processed
 scripts/processed/*
 *dump.txt
 **/.verus-log
+.env

benches/HumanEval-RustBench/008-sum_product.rs

@@ -12,9 +12,11 @@ spec fn product(numbers: Seq<u32>) -> (result:int) {
 // pure-end
 
 proof fn sum_bound(numbers: Seq<u32>)
+    // post-conditions-start
     ensures
         sum(numbers) <= numbers.len() * u32::MAX,
     decreases numbers.len(),
+    // post-conditions-end
 {
     // impl-start
     if numbers.len() == 0 {

benches/HumanEval-RustBench/009-rolling_max.rs

@@ -2,7 +2,7 @@ use vstd::prelude::*;
 
 verus! {
 
-spec fn seq_max(a: Seq<i32>) -> i32
+spec fn seq_max(a: Seq<i32>) -> (ret: i32)
     decreases a.len(),
 {
     if a.len() == 0 {

benches/HumanEval-RustBench/011-string_xor.rs

@@ -2,7 +2,7 @@ use vstd::prelude::*;
 use vstd::slice::*;
 
 verus! {
-spec fn is_binary_digit(c: char) -> bool {
+spec fn is_binary_digit(c: char) -> (ret: bool) {
     c == '0' || c == '1'
 }
 // pure-end

benches/HumanEval-RustBench/034-unique.rs

@@ -6,12 +6,16 @@ use vstd::seq_lib::lemma_seq_contains_after_push;
 verus! {
 
 proof fn swap_preserves_multiset_helper(s: Seq<i32>, i: int, j: int)
+    // pre-conditions-start
     requires
         0 <= i < j < s.len(),
+    // pre-conditions-end
+    // post-conditions-start
     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)),
+    // post-conditions-end
 {
     // impl-start
     let fst = s.take(i);
@@ -36,13 +40,17 @@ proof fn swap_preserves_multiset_helper(s: Seq<i32>, i: int, j: int)
 // pure-end
 
 proof fn swap_preserves_multiset(s1: Seq<i32>, s2: Seq<i32>, i: int, j: int)
+    // pre-conditions-start
     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),
+    // pre-conditions-end
+    // post-conditions-start
     ensures
         s1.to_multiset() == s2.to_multiset(),
+    // post-conditions-end
 {
     // impl-start
     calc! {

benches/HumanEval-RustBench/074-total_match.rs

@@ -8,18 +8,24 @@ spec fn spec_sum(s: Seq<nat>) -> (ret: int) {
 // pure-end
 
 proof fn lemma_increasing_sum(s: Seq<nat>, i: int, j: int)
+    // pre-conditions-start
     requires
         0 <= i <= j <= s.len(),
+    // pre-conditions-end
+    // post-conditions-start
     ensures
         spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)),
     decreases j - i,
+    // post-conditions-end
 {
+    // impl-start
     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);
     }
+    // impl-end
 }
 // pure-end
 

benches/HumanEval-RustBench/additional/largest_prime_factor.rs

@@ -34,7 +34,7 @@ fn is_prime(n: u32) -> (result: bool)
     // impl-end
 }
 
-spec fn is_prime_pred(n: u32) -> bool {
+spec fn is_prime_pred(n: u32) -> (ret: bool) {
     forall|k: int| 2 <= k < n ==> #[trigger] (n as int % k) != 0
 }
 

benches/HumanEval-RustBench/additional/remove_duplicates.rs

@@ -2,7 +2,7 @@ use vstd::prelude::*;
 
 verus! {
 
-spec fn in_array(a: Seq<i32>, x: i32) -> bool {
+spec fn in_array(a: Seq<i32>, x: i32) -> (ret: bool) {
     exists|i: int| 0 <= i < a.len() && a[i] == x
 }
 

benches/HumanEval-RustBench/additional/remove_elements.rs

@@ -2,7 +2,7 @@ use vstd::prelude::*;
 
 verus! {
 
-spec fn in_array(a: Seq<i32>, x: i32) -> bool {
+spec fn in_array(a: Seq<i32>, x: i32) -> (ret: bool) {
     exists|i: int| 0 <= i < a.len() && a[i] == x
 }
 

benches/HumanEval-RustBench/additional/rolling_max.rs

@@ -2,7 +2,7 @@ use vstd::prelude::*;
 
 verus! {
 
-spec fn seq_max(a: Seq<i32>) -> i32
+spec fn seq_max(a: Seq<i32>) -> (ret: i32)
     decreases a.len(),
 {
     if a.len() == 0 {

benches/HumanEval-RustBench/text-descriptions/000-has_close_elements.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `has_close_elements`: Check if in given list of numbers, are any two numbers closer to each other than given threshold.

benches/HumanEval-RustBench/text-descriptions/001-separate-paren-groups.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `separate_paren_groups`: Input to this function is a string containing multiple groups of nested parentheses. Your goal is to separate those group into separate strings and return the list of those. Separate groups are balanced (each open brace is properly closed) and not nested within each other Ignore any spaces in the input string.

benches/HumanEval-RustBench/text-descriptions/002-truncate.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `truncate_number`: Given a positive floating point number, it can be decomposed into and integer part (largest integer smaller than given number) and decimals (leftover part always smaller than 1). Return the decimal part of the number.

benches/HumanEval-RustBench/text-descriptions/003-below_zero.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `below_zero`: 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.

benches/HumanEval-RustBench/text-descriptions/004-mean_absolute_derivation.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `mean_absolute_deviation`: For a given list of input numbers, calculate Mean Absolute Deviation around the mean of this dataset. Mean Absolute Deviation is the average absolute difference between each element and a centerpoint (mean in this case): MAD = average | x - x_mean |

benches/HumanEval-RustBench/text-descriptions/005-intersperse.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `intersperse`: Insert a number 'delimeter' between every two consecutive elements of input list `numbers'

benches/HumanEval-RustBench/text-descriptions/006-parse_nested_parens.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `parse_nested_parens`: Input to this function is a string represented multiple groups for nested parentheses separated by spaces. For each of the group, output the deepest level of nesting of parentheses. E.g. (()()) has maximum two levels of nesting while ((())) has three.

benches/HumanEval-RustBench/text-descriptions/007-filter_by_substring.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `filter_by_substring`: Filter an input list of strings only for ones that contain given substring

benches/HumanEval-RustBench/text-descriptions/008-sum_product.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `sum_product`: For a given list of integers, return a tuple consisting of a sum and a product of all the integers in a list. Empty sum should be equal to 0 and empty product should be equal to 1.

benches/HumanEval-RustBench/text-descriptions/009-rolling_max.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `rolling_max`: From a given list of integers, generate a list of rolling maximum element found until given moment in the sequence.

benches/HumanEval-RustBench/text-descriptions/010-is_palindrome.txt

@@ -1,4 +1,4 @@
-You have to write 2 functions in dafny, using the given helper functions
+You have to write 2 functions in verus, using the given helper functions
 The descriptions are as follows:
 function `is_palindrome`: Test if given string is a palindrome
 function `make_palindrome`: Find the shortest palindrome that begins with a supplied string. Algorithm idea is simple: - Find the longest postfix of supplied string that is a palindrome. - Append to the end of the string reverse of a string prefix that comes before the palindromic suffix.

benches/HumanEval-RustBench/text-descriptions/011-string_xor.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `string_xor`: Input are two strings a and b consisting only of 1s and 0s. Perform binary XOR on these inputs and return result also as a string.

benches/HumanEval-RustBench/text-descriptions/012-longest.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `longest`: Out of list of strings, return the longest one. Return the first one in case of multiple strings of the same length. Return None in case the input list is empty.

benches/HumanEval-RustBench/text-descriptions/013-greatest_common_divisor.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `greatest_common_divisor`: Return a greatest common divisor of two integers a and b

benches/HumanEval-RustBench/text-descriptions/014-all_prefixes.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `all_prefixes`: Return list of all prefixes from shortest to longest of the input string

benches/HumanEval-RustBench/text-descriptions/016-count_distinct_characters.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `count_distinct_characters`: Given a string, find out how many distinct characters (regardless of case) does it consist of

benches/HumanEval-RustBench/text-descriptions/018-how_many_times.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `how_many_times`: Find how many times a given substring can be found in the original string. Count overlaping cases.

benches/HumanEval-RustBench/text-descriptions/020-find_closest_elements.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `find_closest_elements`: From a supplied list of numbers (of length at least two) select and return two that are the closest to each other and return them in order (smaller number, larger number).

benches/HumanEval-RustBench/text-descriptions/021-rescale_to_unit.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `rescale_to_unit`: Given list of numbers (of at least two elements), apply a linear transform to that list, such that the smallest number will become 0 and the largest will become 1

benches/HumanEval-RustBench/text-descriptions/023-strlen.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `strlen`: Return length of given string

benches/HumanEval-RustBench/text-descriptions/024-largest-divisor.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `largest_divisor`: For a given number n, find the largest number that divides n evenly, smaller than n

benches/HumanEval-RustBench/text-descriptions/025-factorize.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `factorize`: Return list of prime factors of given integer in the order from smallest to largest. Each of the factors should be listed number of times corresponding to how many times it appeares in factorization. Input number should be equal to the product of all factors

benches/HumanEval-RustBench/text-descriptions/026-remove_duplicates.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `remove_duplicates`: From a list of integers, remove all elements that occur more than once. Keep order of elements left the same as in the input.

benches/HumanEval-RustBench/text-descriptions/027-flip_case.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `flip_case`: For a given string, flip lowercase characters to uppercase and uppercase to lowercase.

benches/HumanEval-RustBench/text-descriptions/029-filter_by_prefix.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `filter_by_prefix`: Filter an input list of strings only for ones that start with a given prefix.

benches/HumanEval-RustBench/text-descriptions/030-get-positive.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `get_positive`: Return only positive numbers in the list.

benches/HumanEval-RustBench/text-descriptions/031-is-prime.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `is_prime`: Return true if a given number is prime, and false otherwise.

benches/HumanEval-RustBench/text-descriptions/033-sort_third.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `sort_third`: This function takes a list l and returns a list l' such that l' is identical to l in the indicies that are not divisible by three, while its values at the indicies that are divisible by three are equal to the values of the corresponding indicies of l, but sorted.

benches/HumanEval-RustBench/text-descriptions/034-unique.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `unique`: Return sorted unique elements in a list

benches/HumanEval-RustBench/text-descriptions/035-max-element.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `max_element`: Return maximum element in the list.

benches/HumanEval-RustBench/text-descriptions/036-fizz_buzz.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `fizz_buzz`: Return the number of times the digit 7 appears in integers less than n which are divisible by 11 or 13.

benches/HumanEval-RustBench/text-descriptions/037-sort_even.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `sort_even`: This function takes a list l and returns a list l' such that l' is identical to l in the odd indicies, while its values at the even indicies are equal to the values of the even indicies of l, but sorted.

benches/HumanEval-RustBench/text-descriptions/040-triples-sum-to-zero.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `triples_sum_to_zero`: triples_sum_to_zero takes a list of integers as an input. it returns True if there are three distinct elements in the list that sum to zero, and False otherwise.

benches/HumanEval-RustBench/text-descriptions/041-car_race_collision.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `car_race_collision`: Imagine a road that's a perfectly straight infinitely long line. n cars are driving left to right; simultaneously, a different set of n cars are driving right to left. The two sets of cars start out being very far from each other. All cars move in the same speed. Two cars are said to collide when a car that's moving left to right hits a car that's moving right to left. However, the cars are infinitely sturdy and strong; as a result, they continue moving in their trajectory as if they did not collide. This function outputs the number of such collisions.

benches/HumanEval-RustBench/text-descriptions/042-incr-list.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `incr_list`: Return list with elements incremented by 1.

benches/HumanEval-RustBench/text-descriptions/043-pairs-sum-to-zero.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `pairs_sum_to_zero`: 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.

benches/HumanEval-RustBench/text-descriptions/045-triangle_area.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `triangle_area`: Given length of a side and high return area for a triangle.

benches/HumanEval-RustBench/text-descriptions/046-fib4.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `fib4`: The Fib4 number sequence is a sequence similar to the Fibbonacci sequnece that's defined as follows: fib4(0) -> 0 fib4(1) -> 0 fib4(2) -> 2 fib4(3) -> 0 fib4(n) -> fib4(n-1) + fib4(n-2) + fib4(n-3) + fib4(n-4). Please write a function to efficiently compute the n-th element of the fib4 number sequence. Do not use recursion.

benches/HumanEval-RustBench/text-descriptions/048-is-palindrome.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `is_palindrome`: Checks if given string is a palindrome

benches/HumanEval-RustBench/text-descriptions/048-is_palindrome.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `is_palindrome`: Checks if given string is a palindrome

benches/HumanEval-RustBench/text-descriptions/049-modp.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `modp`: Return 2^n modulo p (be aware of numerics).

benches/HumanEval-RustBench/text-descriptions/050-encode_shift.txt

@@ -1,4 +1,4 @@
-You have to write 2 functions in dafny, using the given helper functions
+You have to write 2 functions in verus, using the given helper functions
 The descriptions are as follows:
 function `encode_shift`: returns encoded string by shifting every character by 5 in the alphabet.
 function `decode_shift`: takes as input string encoded with encode_shift function. Returns decoded string.

benches/HumanEval-RustBench/text-descriptions/051-remove-vowels.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `remove_vowels`: remove_vowels is a function that takes string and returns string without vowels.

benches/HumanEval-RustBench/text-descriptions/052-below-threshold.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `below_threshold`: Return True if all numbers in the list l are below threshold t.

benches/HumanEval-RustBench/text-descriptions/053-add.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `add`: Add two numbers x and y

benches/HumanEval-RustBench/text-descriptions/054-same-chars.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `same_chars`: Check if two words have the same characters.

benches/HumanEval-RustBench/text-descriptions/055-fib.txt

@@ -1,3 +1,3 @@
-You have to write 1 function in dafny, using the given helper functions
+You have to write 1 function in verus, using the given helper functions
 The description is as follows:
 function `fib`: Return n-th Fibonacci number.