diff --git a/.gitignore b/.gitignore index 776b95e..6edb45a 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,5 @@ results/* /log_tries/ /log_tries/* .direnv +scripts/processed +scripts/processed/* diff --git a/benches/HumanEval-RustBench/000-has_close_elements.rs b/benches/HumanEval-RustBench/000-has_close_elements.rs new file mode 100644 index 0000000..bc65e22 --- /dev/null +++ b/benches/HumanEval-RustBench/000-has_close_elements.rs @@ -0,0 +1,59 @@ +use vstd::math::abs; +use vstd::prelude::*; +use vstd::slice::*; + +verus! { +fn has_close_elements(numbers: &[i64], threshold: i64) -> (result: bool) + ensures + result == exists|i: int, j: int| + 0 <= i < j < numbers@.len() && abs(numbers[i] - numbers[j]) < threshold, +{ + if threshold <= 0 { + assert(forall|i: int, j: int| + 0 <= i < j < numbers@.len() ==> abs(numbers[i] - numbers[j]) >= 0 >= threshold); + return false; + } + let max_minus_threshold: i64 = i64::MAX - threshold; + let numbers_len: usize = numbers.len(); + for x in 0..numbers_len + invariant + max_minus_threshold == i64::MAX - threshold, + numbers_len == numbers@.len(), + forall|i: int, j: int| + 0 <= i < j < numbers@.len() && i < x ==> abs(numbers[i] - numbers[j]) >= threshold, + { + let numbers_x: i64 = *slice_index_get(numbers, x); + for y in x + 1..numbers_len + invariant + max_minus_threshold == i64::MAX - threshold, + numbers_len == numbers@.len(), + x < numbers@.len(), + numbers_x == numbers[x as int], + forall|i: int, j: int| + 0 <= i < j < numbers@.len() && i < x ==> abs(numbers[i] - numbers[j]) + >= threshold, + forall|j: int| x < j < y ==> abs(numbers_x - numbers[j]) >= threshold, + { + 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 +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/001-separate-paren-groups.rs b/benches/HumanEval-RustBench/001-separate-paren-groups.rs new file mode 100644 index 0000000..705368b --- /dev/null +++ b/benches/HumanEval-RustBench/001-separate-paren-groups.rs @@ -0,0 +1,155 @@ +use vstd::prelude::*; + +verus! { +pub open spec fn nesting_level(input: Seq) -> int + decreases input.len(), +{ + 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 + } + } +} + +pub open spec fn is_paren_char(c: char) -> bool { + c == '(' || c == ')' +} +pub open spec fn is_balanced_group(input: Seq) -> 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) -> 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(s: Seq>) -> Seq> { + s.map(|_i, ss: Vec| ss@) +} + +pub open spec fn remove_nonparens(s: Seq) -> Seq { + s.filter(|c| is_paren_char(c)) +} +proof fn lemma_remove_nonparens_maintained_by_push(s: Seq, pos: int) + requires + 0 <= pos < s.len(), + 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 + } + }), + decreases pos, +{ + reveal(Seq::filter); + assert(s.take((pos + 1) as int).drop_last() =~= s.take(pos as int)); + if pos != 0 { + lemma_remove_nonparens_maintained_by_push(s, pos - 1); + } +} +fn separate_paren_groups(input: &Vec) -> (groups: Vec>) + requires + is_sequence_of_balanced_groups(input@), + ensures + forall|i: int| + #![trigger groups[i]] + 0 <= i < groups.len() ==> is_balanced_group(groups[i]@), + vecs_to_seqs(groups@).flatten() == remove_nonparens(input@), +{ + let mut groups: Vec> = Vec::new(); + let mut current_group: Vec = Vec::new(); + let input_len = input.len(); + let ghost mut ghost_groups: Seq> = Seq::empty(); + proof { + assert(vecs_to_seqs(groups@) =~= ghost_groups); + assert(remove_nonparens(input@.take(0)) =~= Seq::::empty()); + assert(ghost_groups.flatten() + current_group@ =~= Seq::::empty()); + } + let mut current_nesting_level: usize = 0; + for pos in 0..input_len + invariant + input_len == input.len(), + ghost_groups == vecs_to_seqs(groups@), + ghost_groups.flatten() + current_group@ == remove_nonparens(input@.take(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(input@.take(pos as int)), + current_nesting_level == nesting_level(current_group@), + current_nesting_level <= pos, + current_group@.len() == 0 <==> current_nesting_level == 0, + forall|i| 0 <= i < current_group@.len() ==> is_paren_char(#[trigger] current_group@[i]), + forall|i| + 0 < i < current_group@.len() ==> nesting_level(#[trigger] current_group@.take(i)) + > 0, + is_sequence_of_balanced_groups(input@), + { + let ghost prev_group = current_group@; + let ghost prev_groups = ghost_groups; + let c = input[pos]; + proof { + assert(input@.take((pos + 1) as int) == input@.take(pos as int).push(c)); + assert(input@.take((pos + 1) as int).drop_last() == input@.take(pos as int)); + lemma_remove_nonparens_maintained_by_push(input@, pos as int); + } + if c == '(' { + current_nesting_level = current_nesting_level + 1; + current_group.push('('); + assert(current_group@.drop_last() == prev_group); + assert(ghost_groups.flatten() + current_group@ =~= (ghost_groups.flatten() + + prev_group).push('(')); + assert(forall|i| + 0 < i < prev_group.len() ==> #[trigger] current_group@.take(i) == prev_group.take( + i, + )); + } else if c == ')' { + current_nesting_level = current_nesting_level - 1; + current_group.push(')'); + assert(current_group@.drop_last() == prev_group); + assert(ghost_groups.flatten() + current_group@ =~= (ghost_groups.flatten() + + prev_group).push(')')); + assert(forall|i| + 0 < i < prev_group.len() ==> #[trigger] current_group@.take(i) == prev_group.take( + i, + )); + if current_nesting_level == 0 { + proof { + ghost_groups = ghost_groups.push(current_group@); + assert(vecs_to_seqs(groups@.push(current_group)) =~= vecs_to_seqs(groups@).push( + current_group@, + )); + assert(ghost_groups.drop_last() == prev_groups); + 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(); + } + } + groups.push(current_group); + current_group = Vec::::new(); + assert(ghost_groups.flatten() + current_group@ =~= remove_nonparens( + input@.take((pos + 1) as int), + )); + } + } + } + assert(input@.take(input_len as int) =~= input@); + assert(ghost_groups.flatten() + current_group@ == ghost_groups.flatten()); + groups +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/004-mean_absolute_derivation.rs b/benches/HumanEval-RustBench/004-mean_absolute_derivation.rs new file mode 100644 index 0000000..31daf3c --- /dev/null +++ b/benches/HumanEval-RustBench/004-mean_absolute_derivation.rs @@ -0,0 +1,332 @@ +use vstd::arithmetic::div_mod::{ + lemma_div_is_ordered, lemma_div_is_ordered_by_denominator, lemma_div_multiples_vanish, + lemma_fundamental_div_mod, lemma_fundamental_div_mod_converse, +}; +use vstd::arithmetic::mul::{ + lemma_mul_inequality, lemma_mul_is_distributive_add, lemma_mul_is_distributive_add_other_way, + lemma_mul_unary_negation, +}; +use vstd::prelude::*; + +verus! { +pub open spec fn sum(numbers: Seq) -> int { + numbers.fold_left(0, |acc: int, x| acc + x) +} +pub open spec fn mean(values: Seq) -> int + recommends + values.len() > 0, +{ + sum(values) / (values.len() as int) +} +pub open spec fn abs(n: int) -> int { + if n >= 0 { + n + } else { + -n + } +} +pub open spec fn spec_mean_absolute_deviation(numbers: Seq) -> int + recommends + numbers.len() > 0, +{ + let avg = mean(numbers); + sum(numbers.map(|_index, n: int| abs(n - avg))) / (numbers.len() as int) +} +proof fn lemma_sum_bound(numbers: Seq, min: int, max: int) + requires + forall|i| 0 <= i < numbers.len() ==> min <= #[trigger] numbers[i] <= max, + ensures + numbers.len() * min <= sum(numbers) <= numbers.len() * max, + decreases numbers.len(), +{ + if numbers.len() != 0 { + lemma_sum_bound(numbers.drop_last(), min, max); + lemma_mul_is_distributive_add_other_way(min, numbers.len() - 1, 1); + lemma_mul_is_distributive_add_other_way(max, numbers.len() - 1, 1); + } +} +proof fn lemma_sum_ratio_bound(numbers: Seq, denominator: int, min: int, max: int) + requires + forall|i| 0 <= i < numbers.len() ==> min <= #[trigger] numbers[i] <= max, + denominator >= numbers.len(), + denominator > 0, + min <= 0, + max >= 0, + ensures + min <= sum(numbers) / denominator <= max, +{ + lemma_sum_bound(numbers, min, max); + assert(denominator * min <= numbers.len() * min) by { + lemma_mul_unary_negation(denominator, -min); + lemma_mul_unary_negation(numbers.len() as int, -min); + lemma_mul_inequality(numbers.len() as int, denominator, -min); + } + assert(numbers.len() * max <= denominator * max) by { + lemma_mul_inequality(numbers.len() as int, denominator, max); + } + lemma_div_multiples_vanish(min, denominator); + lemma_div_multiples_vanish(max, denominator); + lemma_div_is_ordered(denominator * min, sum(numbers), denominator); + lemma_div_is_ordered(sum(numbers), denominator * max, denominator); +} +proof fn lemma_how_to_update_running_sum(s: Seq, i: int) + requires + 0 <= i < s.len(), + ensures + sum(s.take(i + 1)) == sum(s.take(i)) + s[i], +{ + let q1 = s.take(i); + let q2 = s.take(i + 1); + assert(q2.last() == s[i]); + assert(q2.drop_last() == q1); +} +proof fn lemma_how_to_add_then_divide(x: int, y: int, d: int) + requires + d > 0, + ensures + if (x % d) + (y % d) >= d { + &&& (x + y) / d == (x / d) + (y / d) + 1 + &&& (x + y) % d == (x % d) + (y % d) - d + } else { + &&& (x + y) / d == (x / d) + (y / d) + &&& (x + y) % d == (x % d) + (y % d) + }, +{ + lemma_fundamental_div_mod(x, d); + lemma_fundamental_div_mod(y, d); + lemma_mul_is_distributive_add(d, x / d, y / d); + if (x % d) + (y % d) >= d { + lemma_mul_is_distributive_add(d, (x / d) + (y / d), 1); + lemma_fundamental_div_mod_converse(x + y, d, (x / d) + (y / d) + 1, (x % d) + (y % d) - d); + } else { + lemma_fundamental_div_mod_converse(x + y, d, (x / d) + (y / d), (x % d) + (y % d)); + } +} +proof fn lemma_effect_of_dividing_by_two_or_more(x: int, d: int) + requires + d >= 2, + ensures + x > 0 ==> x / d < x, + x < 0 ==> x / d < 0, +{ + lemma_fundamental_div_mod(x, d); + if x > 0 { + lemma_div_is_ordered_by_denominator(x, 2, d); + } +} +fn divide_i32_by_u32(x: i32, d: u32) -> (qr: (i32, u32)) + requires + d > 0, + ensures + ({ + let (q, r) = qr; + q == x as int / d as int && r == x as int % d as int + }), +{ + if x >= 0 { + return ((x as u32 / d) as i32, x as u32 % d); + } + let neg_x: u32; + if x == i32::MIN { + if d == 1 { + return (x, 0); + } else { + neg_x = 0x80000000u32; + } + } else { + neg_x = (-x) as u32; + } + assert(neg_x == -x); + let neg_x_div_d = neg_x / d; + let neg_x_mod_d = neg_x % d; + assert(neg_x == d * neg_x_div_d + neg_x_mod_d) by { + lemma_fundamental_div_mod(neg_x as int, d as int); + } + assert(neg_x_div_d <= i32::MAX) by { + if x == i32::MIN { + lemma_mul_inequality(2, d as int, neg_x_div_d as int); + } + } + if neg_x_mod_d == 0 { + proof { + lemma_mul_unary_negation(d as int, neg_x_div_d as int); + assert(x == d * -neg_x_div_d); + lemma_fundamental_div_mod_converse(x as int, d as int, -(neg_x_div_d as int), 0int); + } + (-(neg_x_div_d as i32), 0u32) + } else { + proof { + lemma_mul_unary_negation(d as int, (neg_x_div_d + 1) as int); + lemma_mul_is_distributive_add(d as int, neg_x_div_d as int, 1); + assert(x == d as int * (-neg_x_div_d - 1) + (d - neg_x_mod_d) as int); + lemma_fundamental_div_mod_converse( + x as int, + d as int, + -(neg_x_div_d as int) - 1, + (d - neg_x_mod_d) as int, + ); + } + (-(neg_x_div_d as i32) - 1, d - neg_x_mod_d) + } +} +fn divide_i32_by_usize(x: i32, d: usize) -> (qr: (i32, usize)) + requires + d > 0, + ensures + ({ + let (q, r) = qr; + q == x as int / d as int && r == x as int % d as int + }), +{ + if d <= u32::MAX as usize { + let (q, r) = divide_i32_by_u32(x, d as u32); + (q, r as usize) + } else if x >= 0 { + assert(0 == x as int / d as int && x == x as int % d as int) by { + lemma_fundamental_div_mod_converse(x as int, d as int, 0, x as int); + } + (0, x as usize) + } else { + assert(-1 == x as int / d as int && d + x == x as int % d as int) by { + lemma_fundamental_div_mod_converse(x as int, d as int, -1, d + x); + } + let neg_x: usize = if x == i32::MIN { + 0x80000000usize + } else { + (-x) as usize + }; + (-1, d - neg_x) + } +} +fn compute_mean_of_i32s(numbers: &[i32]) -> (result: i32) + requires + numbers.len() > 0, + ensures + result == mean(numbers@.map(|_index, n: i32| n as int)), +{ + let ghost nums = numbers@.map(|_index, n: i32| n as int); + let mut quotient: i32 = 0; + let mut remainder: usize = 0; + let numbers_len: usize = numbers.len(); + for i in 0..numbers_len + invariant + quotient == sum(nums.take(i as int)) / numbers_len as int, + remainder == sum(nums.take(i as int)) % numbers_len as int, + numbers_len == numbers.len(), + nums == numbers@.map(|_index, n: i32| n as int), + { + let n = numbers[i]; + proof { + lemma_how_to_update_running_sum(nums, i as int); + lemma_sum_ratio_bound( + nums.take(i + 1), + numbers_len as int, + i32::MIN as int, + i32::MAX as int, + ); + lemma_how_to_add_then_divide(sum(nums.take(i as int)), n as int, numbers_len as int); + } + + let (q, r) = divide_i32_by_usize(n, numbers_len); + + if r >= numbers_len - remainder { + assert(q < i32::MAX) by { + lemma_effect_of_dividing_by_two_or_more(n as int, numbers_len as int); + } + remainder -= (numbers_len - r); + quotient += (q + 1); + } else { + remainder += r; + quotient += q; + } + } + assert(nums == nums.take(nums.len() as int)); + quotient +} +fn compute_absolute_difference(x: i32, y: i32) -> (z: u32) + ensures + z == abs(x - y), +{ + if x >= y { + if y >= 0 || x < 0 { + (x - y) as u32 + } else { + let neg_y: u32 = if y == i32::MIN { + 0x80000000u32 + } else { + (-y) as u32 + }; + x as u32 + neg_y + } + } else { + if x >= 0 || y < 0 { + (y - x) as u32 + } else { + let neg_x: u32 = if x == i32::MIN { + 0x80000000u32 + } else { + (-x) as u32 + }; + y as u32 + neg_x + } + } +} +pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) + requires + numbers.len() > 0, + ensures + result == spec_mean_absolute_deviation(numbers@.map(|_index, n: i32| n as int)), +{ + let numbers_mean: i32 = compute_mean_of_i32s(numbers); + let ghost deviations = numbers@.map(|_index, n: i32| n as int).map( + |_index, n: int| abs(n - numbers_mean), + ); + let mut quotient: u32 = 0; + let mut remainder: usize = 0; + let numbers_len: usize = numbers.len(); + for i in 0..numbers_len + invariant + quotient == sum(deviations.take(i as int)) / numbers_len as int, + remainder == sum(deviations.take(i as int)) % numbers_len as int, + numbers_len == numbers.len(), + numbers_mean == mean(numbers@.map(|_index, n: i32| n as int)), + deviations == numbers@.map(|_index, n: i32| n as int).map( + |_index, n: int| abs(n - numbers_mean), + ), + { + let n: u32 = compute_absolute_difference(numbers[i], numbers_mean); + proof { + lemma_how_to_update_running_sum(deviations, i as int); + lemma_sum_ratio_bound( + deviations.take(i + 1), + numbers_len as int, + u32::MIN as int, + u32::MAX as int, + ); + lemma_how_to_add_then_divide( + sum(deviations.take(i as int)), + n as int, + numbers_len as int, + ); + } + + let q: u32 = (n as usize / numbers_len) as u32; + let r: usize = n as usize % numbers_len; + + if r >= numbers_len - remainder { + assert(q < u32::MAX) by { + lemma_effect_of_dividing_by_two_or_more(n as int, numbers_len as int); + } + remainder -= (numbers_len - r); + quotient += (q + 1); + } else { + remainder += r; + quotient += q; + } + } + assert(deviations == deviations.take(deviations.len() as int)); + quotient +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/005-intersperse.rs b/benches/HumanEval-RustBench/005-intersperse.rs new file mode 100644 index 0000000..b3bfa03 --- /dev/null +++ b/benches/HumanEval-RustBench/005-intersperse.rs @@ -0,0 +1,105 @@ +use vstd::assert_seqs_equal; +use vstd::prelude::*; + +verus! { +pub open spec fn intersperse_spec(numbers: Seq, delimiter: u64) -> Seq + decreases numbers.len(), +{ + if numbers.len() <= 1 { + numbers + } else { + intersperse_spec(numbers.drop_last(), delimiter) + seq![delimiter, numbers.last()] + } +} +spec fn even(i: int) -> int { + 2 * i +} + +spec fn odd(i: int) -> int { + 2 * i + 1 +} +spec fn intersperse_quantified(numbers: Seq, delimiter: u64, interspersed: Seq) -> bool { + (if numbers.len() == 0 { + interspersed.len() == 0 + } else { + interspersed.len() == 2 * numbers.len() - 1 + }) && (forall|i: int| 0 <= i < numbers.len() ==> #[trigger] interspersed[even(i)] == numbers[i]) + && (forall|i: int| + 0 <= i < numbers.len() - 1 ==> #[trigger] interspersed[odd(i)] == delimiter) +} + +proof fn intersperse_spec_len(numbers: Seq, delimiter: u64) + ensures + numbers.len() > 0 ==> intersperse_spec(numbers, delimiter).len() == 2 * numbers.len() - 1, + decreases numbers.len(), +{ + if numbers.len() > 0 { + intersperse_spec_len(numbers.drop_last(), delimiter); + } +} +proof fn intersperse_quantified_is_spec(numbers: Seq, delimiter: u64, interspersed: Seq) + requires + intersperse_quantified(numbers, delimiter, interspersed), + ensures + interspersed == intersperse_spec(numbers, delimiter), + decreases numbers.len(), +{ + let is = intersperse_spec(numbers, delimiter); + if numbers.len() == 0 { + } else if numbers.len() == 1 { + assert(interspersed.len() == 1); + assert(interspersed[even(0)] == numbers[0]); + } else { + intersperse_quantified_is_spec( + numbers.drop_last(), + delimiter, + interspersed.take(interspersed.len() - 2), + ); + intersperse_spec_len(numbers, delimiter); + assert_seqs_equal!(is == interspersed, i => { + if i < is.len() - 2 { + } else { + if i % 2 == 0 { + assert(is[i] == numbers.last()); + assert(interspersed[even(i/2)] == numbers[i / 2]); + assert(i / 2 == numbers.len() - 1); + } else { + assert(is[i] == delimiter); + assert(interspersed[odd((i-1)/2)] == delimiter); + } + } + }); + } + assert(interspersed =~= intersperse_spec(numbers, delimiter)); +} +pub fn intersperse(numbers: Vec, delimiter: u64) -> (result: Vec) + ensures + result@ == intersperse_spec(numbers@, delimiter), +{ + if numbers.len() <= 1 { + numbers + } else { + let mut result = Vec::new(); + let mut index = 0; + while index < numbers.len() - 1 + invariant + numbers.len() > 1, + 0 <= index < numbers.len(), + result.len() == 2 * index, + forall|i: int| 0 <= i < index ==> #[trigger] result[even(i)] == numbers[i], + forall|i: int| 0 <= i < index ==> #[trigger] result[odd(i)] == delimiter, + { + result.push(numbers[index]); + result.push(delimiter); + index += 1; + } + result.push(numbers[numbers.len() - 1]); + proof { + intersperse_quantified_is_spec(numbers@, delimiter, result@); + } + result + } +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/007-filter_by_substring.rs b/benches/HumanEval-RustBench/007-filter_by_substring.rs new file mode 100644 index 0000000..06f0295 --- /dev/null +++ b/benches/HumanEval-RustBench/007-filter_by_substring.rs @@ -0,0 +1,92 @@ +use vstd::prelude::*; + +verus! { + +fn string_eq(s1: &str, s2: &str) -> (result: bool) + ensures + result <==> s1@ == s2@, +{ + let s1_len = s1.unicode_len(); + let s2_len = s2.unicode_len(); + if s1_len != s2_len { + return false; + } + for i in 0..s1_len + invariant + s1@.subrange(0, i as int) =~= s2@.subrange(0, i as int), + i <= s1_len == s2_len == s1@.len() == s2@.len(), + { + let c = s1.get_char(i); + if c != s2.get_char(i) { + return false; + } + assert(s1@.subrange(0, i + 1) == s1@.subrange(0, i as int).push(c)); + assert(s1@.subrange(0, i as int).push(c) == s2@.subrange(0, i as int).push(c)); + assert(s2@.subrange(0, i as int).push(c) == s2@.subrange(0, i + 1)); + } + assert(s1@ == s1@.subrange(0, s1_len as int)); + assert(s2@ == s2@.subrange(0, s2_len as int)); + true +} + +fn check_substring(s: &str, sub: &str) -> (result: bool) + ensures + result <==> exists|i: int| + 0 <= i <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@, +{ + let s_len = s.unicode_len(); + let sub_len = sub.unicode_len(); + if (s_len < sub_len) { + return false; + } + if sub_len == 0 { + assert(s@.subrange(0, (0 + sub@.len()) as int) == sub@); + return true; + } + for i in 0..s_len - sub_len + 1 + invariant + forall|j: int| 0 <= j < i ==> s@.subrange(j, #[trigger] (j + sub@.len())) != sub@, + i <= s_len - sub_len + 1, + sub_len == sub@.len() <= s_len == s@.len(), + sub_len > 0, + { + if string_eq(sub, s.substring_char(i, i + sub_len)) { + assert(0 <= i <= s@.len() - sub@.len()); + assert(s@.subrange(i as int, i + sub@.len()) == sub@); + return true; + } + } + false +} + +fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) + ensures + forall|i: int| + 0 <= i < strings@.len() && (exists|j: int| + 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( + j, + #[trigger] (j + substring@.len()), + ) == substring@) ==> res@.contains(#[trigger] (strings[i])), +{ + let mut res = Vec::new(); + for n in 0..strings.len() + invariant + forall|i: int| + 0 <= i < n && (exists|j: int| + 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( + j, + #[trigger] (j + substring@.len()), + ) == substring@) ==> res@.contains(#[trigger] (strings[i])), + { + if check_substring(strings[n], substring) { + let ghost res_old = res; + res.push(strings[n]); + assert(res@.last() == strings[n as int]); + assert(res@.drop_last() == res_old@); + } + } + res +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/008-sum_product.rs b/benches/HumanEval-RustBench/008-sum_product.rs new file mode 100644 index 0000000..f02906a --- /dev/null +++ b/benches/HumanEval-RustBench/008-sum_product.rs @@ -0,0 +1,55 @@ +use vstd::prelude::*; + +verus! { +pub open spec fn sum(numbers: Seq) -> int { + numbers.fold_left(0, |acc: int, x| acc + x) +} +pub open spec fn product(numbers: Seq) -> int { + numbers.fold_left(1, |acc: int, x| acc * x) +} +proof fn sum_bound(numbers: Seq) + ensures + sum(numbers) <= numbers.len() * u32::MAX, + decreases numbers.len(), +{ + if numbers.len() == 0 { + } else { + sum_bound(numbers.drop_last()); + } +} +fn sum_product(numbers: Vec) -> (result: (u64, Option)) + requires + numbers.len() < u32::MAX, + ensures + result.0 == sum(numbers@), + result.1 matches Some(v) ==> v == product(numbers@), +{ + let mut sum_value: u64 = 0; + let mut prod_value: Option = Some(1); + for index in 0..numbers.len() + invariant + numbers.len() < u32::MAX, + sum_value == sum(numbers@.take(index as int)), + prod_value matches Some(v) ==> v == product(numbers@.take(index as int)), + index <= numbers.len(), + index >= 0, + { + proof { + sum_bound(numbers@.take(index as int)); + assert(sum_value <= index * u32::MAX); + } + assert(numbers@.take(index as int + 1).drop_last() =~= numbers@.take(index as int)); + assert(numbers[index as int] == numbers@.take(index as int + 1).last()); + sum_value += numbers[index] as u64; + prod_value = + match prod_value { + Some(v) => v.checked_mul(numbers[index]), + None => None, + }; + } + assert(numbers@.take(numbers@.len() as int) =~= numbers@); + (sum_value, prod_value) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/009-rolling_max.rs b/benches/HumanEval-RustBench/009-rolling_max.rs new file mode 100644 index 0000000..b1203a5 --- /dev/null +++ b/benches/HumanEval-RustBench/009-rolling_max.rs @@ -0,0 +1,41 @@ +use vstd::prelude::*; + +verus! { + +spec fn seq_max(a: Seq) -> i32 + decreases a.len(), +{ + if a.len() == 0 { + i32::MIN + } else if a.last() > seq_max(a.drop_last()) { + a.last() + } else { + seq_max(a.drop_last()) + } +} + +fn rolling_max(numbers: Vec) -> (result: Vec) + ensures + result.len() == numbers.len(), + forall|i: int| 0 <= i < numbers.len() ==> result[i] == seq_max(numbers@.take(i + 1)), +{ + let mut max_so_far = i32::MIN; + let mut result = Vec::with_capacity(numbers.len()); + for pos in 0..numbers.len() + invariant + result.len() == pos, + max_so_far == seq_max(numbers@.take(pos as int)), + forall|i: int| 0 <= i < pos ==> result[i] == seq_max(numbers@.take(i + 1)), + { + let number = numbers[pos]; + if number > max_so_far { + max_so_far = number; + } + result.push(max_so_far); + assert(numbers@.take((pos + 1) as int).drop_last() =~= numbers@.take(pos as int)); + } + result +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/011-string_xor.rs b/benches/HumanEval-RustBench/011-string_xor.rs new file mode 100644 index 0000000..7a9cef4 --- /dev/null +++ b/benches/HumanEval-RustBench/011-string_xor.rs @@ -0,0 +1,48 @@ +use vstd::prelude::*; +use vstd::slice::*; + +verus! { +spec fn is_binary_digit(c: char) -> bool { + c == '0' || c == '1' +} +spec fn xor_char(a: char, b: char) -> (result: char) + recommends + is_binary_digit(a), + is_binary_digit(b), +{ + if a == b { + '0' + } else { + '1' + } +} + +fn string_xor(a: &[char], b: &[char]) -> (result: Vec) + requires + a@.len() == b@.len(), + forall|i: int| 0 <= i < a@.len() as int ==> is_binary_digit(#[trigger] a[i]), + forall|i: int| 0 <= i < b@.len() as int ==> is_binary_digit(#[trigger] b[i]), + ensures + result.len() == a@.len(), + forall|i: int| + 0 <= i < result.len() as int ==> #[trigger] result[i] == xor_char(a[i], b[i]), +{ + let a_len = a.len(); + let mut result = Vec::with_capacity(a_len); + #[verifier::loop_isolation(false)] + for pos in 0..a_len + invariant + result.len() == pos, + forall|i: int| 0 <= i < pos ==> #[trigger] result[i] == xor_char(a[i], b[i]), + { + if *slice_index_get(a, pos) == *slice_index_get(b, pos) { + result.push('0'); + } else { + result.push('1'); + } + } + result +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/012-longest.rs b/benches/HumanEval-RustBench/012-longest.rs new file mode 100644 index 0000000..e12aaab --- /dev/null +++ b/benches/HumanEval-RustBench/012-longest.rs @@ -0,0 +1,42 @@ +use vstd::prelude::*; + +verus! { + +fn longest(strings: &Vec>) -> (result: Option<&Vec>) + ensures + match result { + None => strings.len() == 0, + Some(s) => { + (forall|i: int| #![auto] 0 <= i < strings.len() ==> s.len() >= strings[i].len()) + && (exists|i: int| + #![auto] + (0 <= i < strings.len() && s == strings[i] && (forall|j: int| + #![auto] + 0 <= j < i ==> strings[j].len() < s.len()))) + }, + }, +{ + if strings.len() == 0 { + return None; + } + let mut result: &Vec = &strings[0]; + let mut pos = 0; + + for i in 1..strings.len() + invariant + 0 <= pos < i, + result == &strings[pos as int], + exists|i: int| 0 <= i < strings.len() && strings[i] == result, + forall|j: int| #![auto] 0 <= j < i ==> strings[j].len() <= result.len(), + forall|j: int| #![auto] 0 <= j < pos ==> strings[j].len() < result.len(), + { + if result.len() < strings[i].len() { + result = &strings[i]; + pos = i; + } + } + Some(result) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/014-all_prefixes.rs b/benches/HumanEval-RustBench/014-all_prefixes.rs new file mode 100644 index 0000000..56b977b --- /dev/null +++ b/benches/HumanEval-RustBench/014-all_prefixes.rs @@ -0,0 +1,54 @@ +use vstd::prelude::*; + +verus! { + +fn all_prefixes(s: &Vec) -> (prefixes: Vec>) + ensures + prefixes.len() == s.len(), + forall|i: int| #![auto] 0 <= i < s.len() ==> prefixes[i]@ == s@.subrange(0, i + 1), +{ + let mut prefixes: Vec> = vec![]; + let mut prefix = vec![]; + assert(forall|i: int| + #![auto] + 0 <= i < prefix.len() ==> prefix@.index(i) == prefix@.subrange( + 0, + prefix.len() as int, + ).index(i)); + + assert(prefix@ == prefix@.subrange(0, 0)); + assert(forall|i: int| + #![auto] + 0 <= i < prefix.len() ==> prefix@.index(i) == s@.subrange(0, prefix.len() as int).index(i)); + assert(prefix@ == s@.subrange(0, 0)); + for i in 0..s.len() + invariant + prefixes.len() == i, + prefix.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> prefixes[j]@ == s@.subrange(0, j + 1), + prefix@ == s@.subrange(0, i as int), + prefix@ == prefix@.subrange(0, i as int), + { + let ghost pre_prefix = prefix; + prefix.push(s[i]); + assert(pre_prefix@.subrange(0, i as int) == pre_prefix@ && prefix@.subrange(0, i as int) + == pre_prefix@.subrange(0, i as int)); + assert(prefix@.subrange(0, i as int) == s@.subrange(0, i as int)); + assert(prefix[i as int] == s@.subrange(0, i + 1).index(i as int)); + + assert(forall|j: int| + #![auto] + 0 <= j < i + 1 ==> prefix@.index(j) == prefix@.subrange(0, (i + 1) as int).index(j)); + assert(prefix@ == prefix@.subrange(0, (i + 1) as int)); + assert(forall|j: int| + #![auto] + 0 <= j < i + 1 ==> prefix@.index(j) == s@.subrange(0, (i + 1) as int).index(j)); + assert(prefix@ == s@.subrange(0, (i + 1) as int)); + + prefixes.push(prefix.clone()); + } + return prefixes; +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/023-strlen.rs b/benches/HumanEval-RustBench/023-strlen.rs new file mode 100644 index 0000000..a9e0d4e --- /dev/null +++ b/benches/HumanEval-RustBench/023-strlen.rs @@ -0,0 +1,14 @@ +use vstd::prelude::*; + +verus! { + +fn strlen(string: &Vec) -> (length: usize) + ensures + length + == string.len(), +{ + string.len() +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/024-largest-divisor.rs b/benches/HumanEval-RustBench/024-largest-divisor.rs new file mode 100644 index 0000000..e5f6108 --- /dev/null +++ b/benches/HumanEval-RustBench/024-largest-divisor.rs @@ -0,0 +1,85 @@ +use vstd::arithmetic::div_mod::{ + lemma_fundamental_div_mod, lemma_fundamental_div_mod_converse_div, +}; +use vstd::prelude::*; + +verus! { + +pub open spec fn mul(a: nat, b: nat) -> nat { + builtin::mul(a, b) +} +pub open spec fn divides(factor: nat, candidate: nat) -> bool { + exists|k: nat| mul(factor, k) == candidate +} +proof fn lemma_mod_zero(a: nat, b: nat) + requires + a > 0 && b > 0, + a % b == 0, + ensures + divides(b, a), +{ + lemma_fundamental_div_mod(a as int, b as int); + assert(mul(b, (a / b)) == a); +} +proof fn lemma_mod_zero_reversed(a: nat, b: nat) + requires + a > 0 && b > 0, + divides(b, a), + ensures + a % b == 0, +{ + let k_wit = choose|k: nat| mul(b, k) == a; + assert(k_wit == a / b) by { + lemma_fundamental_div_mod_converse_div(a as int, b as int, k_wit as int, 0 as int); + } + lemma_fundamental_div_mod(a as int, b as int); +} +proof fn lemma_one_divides_all() + ensures + forall|v: nat| divides(1 as nat, v), +{ + assert forall|v: nat| divides(1 as nat, v) by { + assert(mul(1 as nat, v) == v); + } +} +fn largest_divisor(n: u32) -> (ret: u32) + requires + n > 1, + ensures + divides(ret as nat, n as nat), + ret < n, + forall|k: u32| (0 < k < n && divides(k as nat, n as nat)) ==> ret >= k, +{ + let mut i = n - 1; + while i >= 2 + invariant + n > 0, + i < n, + forall|k: u32| i < k < n ==> !divides(k as nat, n as nat), + { + if n % i == 0 { + assert(divides(i as nat, n as nat)) by { + lemma_mod_zero(n as nat, i as nat); + } + return i; + } + i -= 1; + + assert forall|k: u32| i < k < n implies !divides(k as nat, n as nat) by { + if k == i + 1 { + assert(!divides(k as nat, n as nat)) by { + if (divides(k as nat, n as nat)) { + lemma_mod_zero_reversed(n as nat, k as nat); + } + } + } + } + } + assert(divides(1 as nat, n as nat)) by { + lemma_one_divides_all(); + } + 1 +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/030-get-positive.rs b/benches/HumanEval-RustBench/030-get-positive.rs new file mode 100644 index 0000000..18c71fb --- /dev/null +++ b/benches/HumanEval-RustBench/030-get-positive.rs @@ -0,0 +1,29 @@ +use vstd::prelude::*; + +verus! { + +fn get_positive(input: Vec) -> (positive_list: Vec) + ensures + positive_list@ == input@.filter(|x: i32| x > 0), +{ + let mut positive_list = Vec::::new(); + let input_len = input.len(); + assert(input@.take(0int).filter(|x: i32| x > 0) == Seq::::empty()); + for pos in 0..input_len + invariant + input_len == input.len(), + positive_list@ == input@.take(pos as int).filter(|x: i32| x > 0), + { + let n = input[pos]; + if n > 0 { + positive_list.push(n); + } + assert(input@.take((pos + 1) as int).drop_last() == input@.take(pos as int)); + reveal(Seq::filter); + } + assert(input@ == input@.take(input_len as int)); + positive_list +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/033-sort_third.rs b/benches/HumanEval-RustBench/033-sort_third.rs new file mode 100644 index 0000000..a946a36 --- /dev/null +++ b/benches/HumanEval-RustBench/033-sort_third.rs @@ -0,0 +1,120 @@ +use vstd::prelude::*; + +verus! { +spec fn count(s: Seq, x: T) -> int + decreases s.len(), +{ + if s.len() == 0 { + 0 + } else { + count(s.skip(1), x) + if s[0] == x { + 1int + } else { + 0int + } + } +} +spec fn permutes(s1: Seq, s2: Seq) -> bool { + forall|x: T| count(s1, x) == count(s2, x) +} +proof fn lemma_update_effect_on_count(s: Seq, i: int, v: T, x: T) + requires + 0 <= i < s.len(), + ensures + count(s.update(i, v), x) == if v == x && s[i] != x { + count(s, x) + 1 + } else if v != x && s[i] == x { + count(s, x) - 1 + } else { + count(s, x) + }, + decreases s.len(), +{ + if s.len() == 0 { + return ; + } + if i == 0 { + assert(s.update(i, v) =~= seq![v] + s.skip(1)); + assert(s.update(i, v).skip(1) =~= s.skip(1)); + } else { + assert(s.update(i, v) =~= seq![s[0]] + s.skip(1).update(i - 1, v)); + assert(s.update(i, v).skip(1) =~= s.skip(1).update(i - 1, v)); + lemma_update_effect_on_count(s.skip(1), i - 1, v, x); + } +} +proof fn lemma_swapping_produces_a_permutation(s: Seq, i: int, j: int) + requires + 0 <= i < s.len(), + 0 <= j < s.len(), + ensures + permutes(s.update(i, s[j]).update(j, s[i]), s), +{ + assert forall|x: T| #[trigger] count(s.update(i, s[j]).update(j, s[i]), x) == count(s, x) by { + lemma_update_effect_on_count(s, i, s[j], x); + lemma_update_effect_on_count(s.update(i, s[j]), j, s[i], x); + } +} +fn sort_third(l: Vec) -> (l_prime: Vec) + ensures + l_prime.len() == l.len(), + forall|i: int| 0 <= i < l.len() && i % 3 != 0 ==> l_prime[i] == l[i], + forall|i: int, j: int| + 0 <= i < j < l.len() && i % 3 == 0 && j % 3 == 0 ==> l_prime[i] <= l_prime[j], + permutes(l_prime@, l@), +{ + let ghost old_l = l@; + let l_len = l.len(); + let mut pos_being_set_to_smallest: usize = 0; + let mut l_prime: Vec = l; + while pos_being_set_to_smallest < l_len + invariant + l_len == l.len() == l_prime.len(), + pos_being_set_to_smallest % 3 == 0, + forall|i: int| 0 <= i < l_len && i % 3 != 0 ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int, j: int| + 0 <= i < pos_being_set_to_smallest && i < j < l_len && i % 3 == 0 && j % 3 == 0 + ==> l_prime[i] <= l_prime[j], + { + let mut pos_of_smallest_found_so_far: usize = pos_being_set_to_smallest; + let mut pos_during_scan_for_smallest: usize = pos_being_set_to_smallest; + while pos_during_scan_for_smallest < l_len + invariant + l_len == l.len() == l_prime.len(), + pos_being_set_to_smallest % 3 == 0, + pos_during_scan_for_smallest % 3 == 0, + pos_of_smallest_found_so_far % 3 == 0, + pos_being_set_to_smallest <= pos_during_scan_for_smallest, + pos_being_set_to_smallest <= pos_of_smallest_found_so_far < l_len, + forall|i: int| 0 <= i < l_len && i % 3 != 0 ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int| + pos_being_set_to_smallest <= i < pos_during_scan_for_smallest && i % 3 == 0 + ==> l_prime[pos_of_smallest_found_so_far as int] <= l_prime[i], + forall|i: int, j: int| + 0 <= i < pos_being_set_to_smallest && i < j < l_len && i % 3 == 0 && j % 3 == 0 + ==> l_prime[i] <= l_prime[j], + { + if l_prime[pos_during_scan_for_smallest] < l_prime[pos_of_smallest_found_so_far] { + pos_of_smallest_found_so_far = pos_during_scan_for_smallest; + } + pos_during_scan_for_smallest = pos_during_scan_for_smallest + 3; + } + proof { + lemma_swapping_produces_a_permutation( + l_prime@, + pos_being_set_to_smallest as int, + pos_of_smallest_found_so_far as int, + ); + } + let v1 = l_prime[pos_being_set_to_smallest]; + let v2 = l_prime[pos_of_smallest_found_so_far]; + l_prime.set(pos_being_set_to_smallest, v2); + l_prime.set(pos_of_smallest_found_so_far, v1); + pos_being_set_to_smallest = pos_being_set_to_smallest + 3; + } + l_prime +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/034-unique.rs b/benches/HumanEval-RustBench/034-unique.rs new file mode 100644 index 0000000..f4c8c90 --- /dev/null +++ b/benches/HumanEval-RustBench/034-unique.rs @@ -0,0 +1,183 @@ +use vstd::calc; +use vstd::prelude::*; +use vstd::seq_lib::lemma_multiset_commutative; +use vstd::seq_lib::lemma_seq_contains_after_push; + +verus! { + +proof fn swap_preserves_multiset_helper(s: Seq, i: int, j: int) + requires + 0 <= i < j < s.len(), + 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)), +{ + let fst = s.take(i); + let snd = s.subrange(i + 1, j); + + assert((s.take(j + 1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add( + snd.to_multiset().insert(s.index(j)), + )) by { + assert(s.take(i + 1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { + fst.to_multiset_ensures(); + assert(fst.push(s.index(i)) =~= s.take(i + 1)); + } + assert(s.subrange(i + 1, j + 1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { + snd.to_multiset_ensures(); + assert(snd.push(s.index(j)) =~= s.subrange(i + 1, j + 1)); + } + lemma_multiset_commutative(s.take(i + 1), s.subrange(i + 1, j + 1)); + assert(s.take(i + 1) + s.subrange(i + 1, j + 1) =~= s.take(j + 1)); + } +} +proof fn swap_preserves_multiset(s1: Seq, s2: Seq, i: int, j: int) + 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), + ensures + s1.to_multiset() == s2.to_multiset(), +{ + calc! { + (==) + s1.to_multiset(); { + lemma_multiset_commutative(s1.take(j + 1), s1.skip(j + 1)); + assert(s1 =~= s1.take(j + 1) + s1.skip(j + 1)); + } + s1.take(j + 1).to_multiset().add(s1.skip(j + 1).to_multiset()); { + assert(s1.take(j + 1).to_multiset() =~= s2.take(j + 1).to_multiset()) by { + assert(s1.take(i) == s2.take(i)); + assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j))); + swap_preserves_multiset_helper(s1, i, j); + swap_preserves_multiset_helper(s2, i, j); + } + assert(s1.skip(j + 1).to_multiset() =~= s2.skip(j + 1).to_multiset()) by { + assert(s1.skip(j + 1) =~= s2.skip(j + 1)); + } + } + s2.take(j + 1).to_multiset().add(s2.skip(j + 1).to_multiset()); { + lemma_multiset_commutative(s2.take(j + 1), s2.skip(j + 1)); + assert(s2 =~= s2.take(j + 1) + s2.skip(j + 1)); + } + s2.to_multiset(); + } +} + +fn sort_seq(s: &Vec) -> (ret: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), + ret@.len() == s@.len(), + s@.to_multiset() == ret@.to_multiset(), +{ + let mut sorted = s.clone(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len(), + forall|j: int, k: int| 0 <= j < k < i ==> sorted@.index(j) <= sorted@.index(k), + s@.to_multiset() == sorted@.to_multiset(), + forall|j: int, k: int| + 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), + sorted@.len() == s@.len(), + { + let mut min_index: usize = i; + let mut j: usize = i + 1; + while j < sorted.len() + invariant + i <= min_index < j <= sorted.len(), + forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), + { + if sorted[j] < sorted[min_index] { + min_index = j; + } + j += 1; + } + if min_index != i { + let ghost old_sorted = sorted@; + let curr_val = sorted[i]; + let min_val = sorted[min_index]; + sorted.set(i, min_val); + + sorted.set(min_index, curr_val); + + proof { + swap_preserves_multiset(old_sorted, sorted@, i as int, min_index as int); + assert(old_sorted.to_multiset() =~= sorted@.to_multiset()); + } + } + i += 1; + } + sorted +} + +fn unique_sorted(s: Vec) -> (result: Vec) + requires + forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j], + ensures + forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j], + forall|i: int| #![auto] 0 <= i < result.len() ==> s@.contains(result[i]), + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]), +{ + let mut result: Vec = vec![]; + for i in 0..s.len() + invariant + forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j], + forall|k: int, l: int| 0 <= k < l < result.len() ==> result[k] < result[l], + forall|k: int| + #![trigger result[k]] + 0 <= k < result.len() ==> (exists|m: int| 0 <= m < i && result[k] == s[m]), + forall|m: int| #![trigger s[m]] 0 <= m < i ==> result@.contains(s[m]), + { + let ghost pre = result; + if result.len() == 0 || result[result.len() - 1] != s[i] { + assert(result.len() == 0 || result[result.len() - 1] < s[i as int]); + result.push(s[i]); + assert forall|m: int| #![trigger s[m]] 0 <= m < i implies result@.contains(s[m]) by { + assert(pre@.contains(s@[m])); + lemma_seq_contains_after_push(pre@, s@[i as int], s@[m]); + }; + } + assert(forall|m: int| + #![trigger result@[m], pre@[m]] + 0 <= m < pre.len() ==> pre@.contains(result@[m]) ==> result@.contains(pre@[m])) by { + assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]); + } + assert(result@.contains(s[i as int])) by { + assert(result[result.len() - 1] == s[i as int]); + } + } + result +} + +fn unique(s: Vec) -> (result: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j], + forall|i: int| #![auto] 0 <= i < result.len() ==> s@.contains(result[i]), + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]), +{ + let sorted = sort_seq(&s); + assert(forall|i: int| #![auto] 0 <= i < sorted.len() ==> s@.contains(sorted[i])) by { + assert(forall|i: int| + #![auto] + 0 <= i < sorted.len() ==> sorted@.to_multiset().contains(sorted[i])) by { + sorted@.to_multiset_ensures(); + } + assert(forall|i: int| + #![auto] + 0 <= i < sorted.len() ==> s@.to_multiset().contains(sorted[i])); + s@.to_multiset_ensures(); + } + assert(forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> sorted@.contains(s[i])) by { + assert(forall|i: int| #![auto] 0 <= i < s.len() ==> s@.to_multiset().contains(s[i])) by { + s@.to_multiset_ensures(); + } + assert(forall|i: int| #![auto] 0 <= i < s.len() ==> sorted@.to_multiset().contains(s[i])); + sorted@.to_multiset_ensures(); + } + unique_sorted(sorted) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/035-max-element.rs b/benches/HumanEval-RustBench/035-max-element.rs new file mode 100644 index 0000000..5b6dda5 --- /dev/null +++ b/benches/HumanEval-RustBench/035-max-element.rs @@ -0,0 +1,26 @@ +use vstd::prelude::*; + +verus! { + +fn max_element(a: &Vec) -> (max: i32) + requires + a.len() > 0, + ensures + forall|i: int| 0 <= i < a.len() ==> a[i] <= max, + exists|i: int| 0 <= i < a.len() && a[i] == max, +{ + let mut max = a[0]; + for i in 1..a.len() + invariant + forall|j: int| 0 <= j < i ==> a[j] <= max, + exists|j: int| 0 <= j < i && a[j] == max, + { + if a[i] > max { + max = a[i]; + } + } + max +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/037-sort_even.rs b/benches/HumanEval-RustBench/037-sort_even.rs new file mode 100644 index 0000000..4cf1fe8 --- /dev/null +++ b/benches/HumanEval-RustBench/037-sort_even.rs @@ -0,0 +1,146 @@ +use vstd::prelude::*; + +verus! { +spec fn count(s: Seq, x: T) -> int + decreases s.len(), +{ + if s.len() == 0 { + 0 + } else { + count(s.skip(1), x) + if s[0] == x { + 1int + } else { + 0int + } + } +} +spec fn permutes(s1: Seq, s2: Seq) -> bool { + forall|x: T| count(s1, x) == count(s2, x) +} +proof fn lemma_update_effect_on_count(s: Seq, i: int, v: T, x: T) + requires + 0 <= i < s.len(), + ensures + count(s.update(i, v), x) == if v == x && s[i] != x { + count(s, x) + 1 + } else if v != x && s[i] == x { + count(s, x) - 1 + } else { + count(s, x) + }, + decreases s.len(), +{ + if s.len() == 0 { + return ; + } + if i == 0 { + assert(s.update(i, v) =~= seq![v] + s.skip(1)); + assert(s.update(i, v).skip(1) =~= s.skip(1)); + } else { + assert(s.update(i, v) =~= seq![s[0]] + s.skip(1).update(i - 1, v)); + assert(s.update(i, v).skip(1) =~= s.skip(1).update(i - 1, v)); + lemma_update_effect_on_count(s.skip(1), i - 1, v, x); + } +} +proof fn lemma_swapping_produces_a_permutation(s: Seq, i: int, j: int) + requires + 0 <= i < s.len(), + 0 <= j < s.len(), + ensures + permutes(s.update(i, s[j]).update(j, s[i]), s), +{ + assert forall|x: T| #[trigger] count(s.update(i, s[j]).update(j, s[i]), x) == count(s, x) by { + lemma_update_effect_on_count(s, i, s[j], x); + lemma_update_effect_on_count(s.update(i, s[j]), j, s[i], x); + } +} + +#[verifier::loop_isolation(false)] +fn sort_pred(l: Vec, p: Vec) -> (l_prime: Vec) + requires + l.len() == p.len(), + ensures + l_prime.len() == l.len(), + forall|i: int| 0 <= i < l.len() && !p[i] ==> l_prime[i] == l[i], + forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && p[i] && p[j] ==> l_prime[i] <= l_prime[j], + permutes(l_prime@, l@), +{ + let ghost old_l = l@; + let l_len = l.len(); + let mut pos_replace: usize = 0; + let mut l_prime: Vec = l; + while pos_replace < l_len + invariant + l_len == l.len() == l_prime.len(), + forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int, j: int| + #![auto] + 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i] <= l_prime[j], + { + if p[pos_replace] { + let mut pos_cur: usize = pos_replace; + let mut pos: usize = pos_replace; + while pos < l_len + invariant + l_len == l.len() == l_prime.len(), + pos_replace <= pos, + pos_replace <= pos_cur < l_len, + p[pos_replace as int], + p[pos_cur as int], + forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int| + #![auto] + pos_replace <= i < pos && p[i] ==> l_prime[pos_cur as int] <= l_prime[i], + forall|i: int, j: int| + #![auto] + 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i] + <= l_prime[j], + { + if p[pos] && l_prime[pos] < l_prime[pos_cur] { + pos_cur = pos; + } + pos = pos + 1; + } + proof { + lemma_swapping_produces_a_permutation(l_prime@, pos_replace as int, pos_cur as int); + } + let v1 = l_prime[pos_replace]; + let v2 = l_prime[pos_cur]; + l_prime.set(pos_replace, v2); + l_prime.set(pos_cur, v1); + } + pos_replace = pos_replace + 1; + } + l_prime +} + +#[verifier::loop_isolation(false)] +fn sort_even(l: Vec) -> (result: Vec) + ensures + l.len() == result.len(), + permutes(result@, l@), + forall|i: int| 0 <= i < l.len() && i % 2 == 1 ==> result[i] == l[i], + forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> result[i] <= result[j], +{ + let mut p: Vec = vec![]; + for i in 0..l.len() + invariant + p.len() == i, + forall|j: int| 0 <= j < i ==> p[j] == (j % 2 == 0), + { + p.push(i % 2 == 0); + } + assert(forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> p[i] && p[j]); + sort_pred(l, p) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/042-incr-list.rs b/benches/HumanEval-RustBench/042-incr-list.rs new file mode 100644 index 0000000..cf7de96 --- /dev/null +++ b/benches/HumanEval-RustBench/042-incr-list.rs @@ -0,0 +1,26 @@ +use vstd::prelude::*; + +verus! { + +fn incr_list(l: Vec) -> (result: Vec) + requires + forall|i: int| 0 <= i < l.len() ==> l[i] + 1 <= i32::MAX, + + ensures + result.len() == l.len(), + forall|i: int| 0 <= i < l.len() ==> #[trigger] result[i] == l[i] + 1, +{ + let mut result = Vec::with_capacity(l.len()); + for i in 0..l.len() + invariant + forall|i: int| 0 <= i < l.len() ==> l[i] + 1 <= i32::MAX, + result.len() == i, + forall|j: int| 0 <= j < i ==> #[trigger] result[j] == l[j] + 1, + { + result.push(l[i] + 1); + } + result +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/043-pairs-sum-to-zero.rs b/benches/HumanEval-RustBench/043-pairs-sum-to-zero.rs new file mode 100644 index 0000000..78381ce --- /dev/null +++ b/benches/HumanEval-RustBench/043-pairs-sum-to-zero.rs @@ -0,0 +1,41 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool) + requires + nums.len() >= 2, + forall|i: int, j: int| + 0 <= i < j < nums.len() ==> nums[i] + nums[j] <= i32::MAX && nums[i] + nums[j] + >= i32::MIN, + ensures + found <==> exists|i: int, j: int| 0 <= i < j < nums.len() && nums[i] + nums[j] == target, +{ + let mut i = 0; + + while i < nums.len() + invariant + 0 <= i <= nums.len(), + forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + { + let mut j = i + 1; + while j < nums.len() + invariant + 0 <= i < j <= nums.len(), + forall|u: int, v: int| + 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + forall|u: int| i < u < j ==> nums[i as int] + nums[u] != target, + { + if nums[i] + nums[j] == target { + return true; + } + j = j + 1; + } + i = i + 1; + } + false +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/045-triangle_area.rs b/benches/HumanEval-RustBench/045-triangle_area.rs new file mode 100644 index 0000000..1a745d9 --- /dev/null +++ b/benches/HumanEval-RustBench/045-triangle_area.rs @@ -0,0 +1,24 @@ +use vstd::prelude::*; + +verus! { + +fn triangle_area(a: u64, h: u64) -> (area: u64) + requires + a > 0, + h > 0, + a * h / 2 <= u64::MAX + , + ensures + area == a * h / 2, +{ + if a % 2 == 0 { + assert(a % 2 == 0 ==> (a / 2) * h == a * h / 2) by (nonlinear_arith); + (a / 2) * h + } else { + assert(a % 2 == 1 ==> (a / 2) * h + (h / 2) == a * h / 2) by (nonlinear_arith); + (a / 2) * h + (h / 2) + } +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/048-is-palindrome.rs b/benches/HumanEval-RustBench/048-is-palindrome.rs new file mode 100644 index 0000000..34fa1fc --- /dev/null +++ b/benches/HumanEval-RustBench/048-is-palindrome.rs @@ -0,0 +1,24 @@ +use vstd::prelude::*; + +verus! { + +fn is_palindrome(text: &str) -> (result: bool) + ensures + result == forall|i: int| + 0 <= i < text@.len() ==> #[trigger] text@[i] == text@[text@.len() - 1 - i], +{ + let text_len: usize = text.unicode_len(); + for pos in 0..text_len / 2 + invariant + text_len == text@.len(), + forall|i: int| 0 <= i < pos ==> #[trigger] text@[i] == text@[text_len - 1 - i], + { + if text.get_char(pos) != text.get_char(text_len - 1 - pos) { + return false; + } + } + true +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/049-modp.rs b/benches/HumanEval-RustBench/049-modp.rs new file mode 100644 index 0000000..836e338 --- /dev/null +++ b/benches/HumanEval-RustBench/049-modp.rs @@ -0,0 +1,44 @@ +use vstd::prelude::*; + +verus! { + +spec fn modp_rec(n: nat, p: nat) -> nat + decreases n, +{ + if n == 0 { + 1nat % p + } else { + (modp_rec((n - 1) as nat, p) * 2) % p + } +} + +fn modmul(a: u32, b: u32, p: u32) -> (mul: u32) + by (nonlinear_arith) + requires + p > 0, + ensures + mul == ((a as int) * (b as int)) % (p as int), +{ + (((a as u64) * (b as u64)) % (p as u64)) as u32 +} + +#[verifier::loop_isolation(false)] +fn modp(n: u32, p: u32) -> (r: u32) + by (nonlinear_arith) + requires + p > 0, + ensures + r == modp_rec(n as nat, p as nat), +{ + let mut r = 1u32 % p; + for i in 0..n + invariant + r == modp_rec(i as nat, p as nat), + { + r = modmul(r, 2, p); + } + r +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/050-encode_shift.rs b/benches/HumanEval-RustBench/050-encode_shift.rs new file mode 100644 index 0000000..9fa06a2 --- /dev/null +++ b/benches/HumanEval-RustBench/050-encode_shift.rs @@ -0,0 +1,97 @@ +use vstd::prelude::*; + +verus! { + +spec fn encode_char_spec(c: int) -> int + recommends + 65 <= c <= 90, +{ + (c - 65 + 5) % 26 + 65 +} + +fn encode_char(c: u8) -> (r: u8) + requires + 65 <= c <= 90, + ensures + r == encode_char_spec(c as int), + 65 <= r <= 90, +{ + (c - 65 + 5) % 26 + 65 +} + +spec fn decode_char_spec(c: int) -> int + recommends + 65 <= c <= 90, +{ + (c - 65 + 26 - 5) % 26 + 65 +} + +fn decode_char(c: u8) -> (r: u8) + requires + 65 <= c <= 90, + ensures + r == decode_char_spec(c as int), + 65 <= r <= 90, +{ + (c - 65 + 26 - 5) % 26 + 65 +} + +proof fn opposite_encode_decode(c: int) + requires + 65 <= c <= 90, + ensures + encode_char_spec(decode_char_spec(c)) == c, + decode_char_spec(encode_char_spec(c)) == c, +{ +} + +#[verifier::loop_isolation(false)] +fn encode_shift(s: &Vec) -> (t: Vec) + requires + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90, + ensures + s.len() == t.len(), + forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == encode_char_spec(s[i] as int), + forall|i: int| #![auto] 0 <= i < t.len() ==> decode_char_spec(t[i] as int) == s[i], +{ + let mut t: Vec = vec![]; + for i in 0..s.len() + invariant + t.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> t[j] == encode_char_spec(s[j] as int), + forall|j: int| #![auto] 0 <= j < i ==> decode_char_spec(t[j] as int) == s[j], + { + t.push(encode_char(s[i])); + proof { + opposite_encode_decode(s[i as int] as int); + } + } + t +} + +#[verifier::loop_isolation(false)] +fn decode_shift(s: &Vec) -> (t: Vec) + requires + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90, + ensures + s.len() == t.len(), + forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == decode_char_spec(s[i] as int), + forall|i: int| #![auto] 0 <= i < t.len() ==> encode_char_spec(t[i] as int) == s[i], +{ + let mut t: Vec = vec![]; + for i in 0..s.len() + invariant + t.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> t[j] == decode_char_spec(s[j] as int), + forall|j: int| #![auto] 0 <= j < i ==> encode_char_spec(t[j] as int) == s[j], + { + t.push(decode_char(s[i])); + proof { + opposite_encode_decode(s[i as int] as int); + } + } + t +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/052-below-threshold.rs b/benches/HumanEval-RustBench/052-below-threshold.rs new file mode 100644 index 0000000..0beb0b1 --- /dev/null +++ b/benches/HumanEval-RustBench/052-below-threshold.rs @@ -0,0 +1,21 @@ +use vstd::prelude::*; + +verus! { + +fn below_threshold(l: &[i32], t: i32) -> (result: bool) + ensures + result == forall|i: int| 0 <= i < l.len() ==> l[i] < t, +{ + for i in 0..l.len() + invariant + forall|j: int| 0 <= j < i ==> l[j] < t, + { + if l[i] >= t { + return false; + } + } + true +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/053-add.rs b/benches/HumanEval-RustBench/053-add.rs new file mode 100644 index 0000000..12a09ea --- /dev/null +++ b/benches/HumanEval-RustBench/053-add.rs @@ -0,0 +1,13 @@ +use vstd::prelude::*; + +verus! { + +fn add(x: i32, y: i32) -> (res: Option) + ensures + res.is_some() ==> res.unwrap() == x + y, +{ + x.checked_add(y) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/054-same-chars.rs b/benches/HumanEval-RustBench/054-same-chars.rs new file mode 100644 index 0000000..5ec16d8 --- /dev/null +++ b/benches/HumanEval-RustBench/054-same-chars.rs @@ -0,0 +1,89 @@ +use vstd::hash_set::HashSetWithView; +use vstd::prelude::*; +use vstd::std_specs::hash::axiom_u8_obeys_hash_table_key_model; + +verus! { + +broadcast use axiom_u8_obeys_hash_table_key_model; + +fn hash_set_from(s: &Vec) -> (res: HashSetWithView) + ensures + forall|i: int| #![auto] 0 <= i < s.len() ==> res@.contains(s[i]), + forall|x: int| + 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> #[trigger] s@.contains(x as u8), +{ + let mut res: HashSetWithView = HashSetWithView::new(); + for i in 0..s.len() + invariant + forall|j: int| #![auto] 0 <= j < i ==> res@.contains(s[j]), + forall|x: int| + 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> (exists|j: int| + 0 <= j < i && s[j] == x), + { + res.insert(s[i]); + } + res +} + +proof fn implies_contains(s0: Seq, s1: Seq, hs1: Set) + requires + forall|i: int| #![trigger s0[i]] 0 <= i < s0.len() ==> 0 <= s0[i] < 256, + forall|x: int| + 0 <= x < 256 ==> #[trigger] hs1.contains(x as u8) ==> #[trigger] s1.contains(x as u8), + ensures + forall|i: int| + #![auto] + 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) ==> s1.contains(s0[i]), +{ + assert forall|i: int| + #![auto] + 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) implies s1.contains(s0[i]) by { + let x = s0[i]; + assert(0 <= x < 256); + assert(hs1.contains(x as u8)); + assert(s1.contains(x as u8)); + }; +} + +#[verifier::loop_isolation(false)] +fn same_chars(s0: &Vec, s1: &Vec) -> (same: bool) + ensures + same <==> (forall|i: int| #![auto] 0 <= i < s0.len() ==> s1@.contains(s0[i])) && (forall| + i: int, + | + #![auto] + 0 <= i < s1.len() ==> s0@.contains(s1[i])), +{ + let hs0 = hash_set_from(s0); + let hs1 = hash_set_from(s1); + + proof { + implies_contains(s0@, s1@, hs1@); + implies_contains(s1@, s0@, hs0@); + } + + let mut contains_s0 = true; + for i in 0..s0.len() + invariant + contains_s0 <==> forall|j: int| #![auto] 0 <= j < i ==> s1@.contains(s0[j]), + { + if !hs1.contains(&s0[i]) { + contains_s0 = false; + assert(!s1@.contains(s0[i as int])); + } + } + let mut contains_s1 = true; + for i in 0..s1.len() + invariant + contains_s1 <==> forall|j: int| #![auto] 0 <= j < i ==> s0@.contains(s1[j]), + { + if !hs0.contains(&s1[i]) { + contains_s1 = false; + assert(!s0@.contains(s1[i as int])); + } + } + contains_s0 && contains_s1 +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/057-monotonic.rs b/benches/HumanEval-RustBench/057-monotonic.rs new file mode 100644 index 0000000..ec8fdcd --- /dev/null +++ b/benches/HumanEval-RustBench/057-monotonic.rs @@ -0,0 +1,37 @@ +use vstd::prelude::*; + +verus! { + +fn monotonic(l: Vec) -> (ret: bool) + ensures + ret <==> (forall|i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j)) || ( + forall|i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(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 ==> l@.index(i) <= l@.index(j), + decreasing <==> forall|i: int, j: int| + 0 <= i < j < n + 1 ==> l@.index(i) >= l@.index(j), + { + if l[n] < l[n + 1] { + decreasing = false; + } else if l[n] > l[n + 1] { + increasing = false; + } + n += 1; + } + increasing || decreasing +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/059-largest-prime-factor.rs b/benches/HumanEval-RustBench/059-largest-prime-factor.rs new file mode 100644 index 0000000..66de5cd --- /dev/null +++ b/benches/HumanEval-RustBench/059-largest-prime-factor.rs @@ -0,0 +1,62 @@ +use vstd::prelude::*; + +verus! { +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 +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/060-sum_to_n.rs b/benches/HumanEval-RustBench/060-sum_to_n.rs new file mode 100644 index 0000000..984e35b --- /dev/null +++ b/benches/HumanEval-RustBench/060-sum_to_n.rs @@ -0,0 +1,35 @@ +use vstd::prelude::*; + +verus! { + +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) + 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) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/062-derivative.rs b/benches/HumanEval-RustBench/062-derivative.rs new file mode 100644 index 0000000..b9748f6 --- /dev/null +++ b/benches/HumanEval-RustBench/062-derivative.rs @@ -0,0 +1,35 @@ +use vstd::prelude::*; + +verus! { + +fn derivative(xs: &Vec) -> (ret: Option>) + ensures + ret.is_some() ==> xs@.len() == 0 || xs@.map(|i: int, x| i * x).skip(1) + =~= ret.unwrap()@.map_values(|x| x as int), +{ + let mut ret = Vec::new(); + if xs.len() == 0 { + return Some(ret); + } + let mut i = 1; + while i < xs.len() + invariant + xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= ret@.map_values(|x| x as int), + 1 <= i <= xs.len(), + { + ret.push(xs[i].checked_mul(i)?); + + let ghost prods = xs@.map(|i: int, x| i * x); + assert(prods.subrange(1, i as int).push(prods.index(i as int)) =~= prods.subrange( + 1, + i + 1 as int, + )); + + i += 1; + } + assert(xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= xs@.map(|i: int, x| i * x).skip(1)); + Some(ret) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/063-fibfib.rs b/benches/HumanEval-RustBench/063-fibfib.rs new file mode 100644 index 0000000..b0f010c --- /dev/null +++ b/benches/HumanEval-RustBench/063-fibfib.rs @@ -0,0 +1,32 @@ +use vstd::prelude::*; + +verus! { + +spec fn spec_fibfib(n: nat) -> nat + decreases n, +{ + if (n == 0) { + 0 + } else if (n == 1) { + 0 + } else if (n == 2) { + 1 + } else { + spec_fibfib((n - 1) as nat) + spec_fibfib((n - 2) as nat) + spec_fibfib((n - 3) as nat) + } +} + +fn fibfib(x: u32) -> (ret: Option) + ensures + ret.is_some() ==> spec_fibfib(x as nat) == ret.unwrap(), +{ + match (x) { + 0 => Some(0), + 1 => Some(0), + 2 => Some(1), + _ => fibfib(x - 1)?.checked_add(fibfib(x - 2)?)?.checked_add(fibfib(x - 3)?), + } +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/064-vowel_count.rs b/benches/HumanEval-RustBench/064-vowel_count.rs new file mode 100644 index 0000000..b278f25 --- /dev/null +++ b/benches/HumanEval-RustBench/064-vowel_count.rs @@ -0,0 +1,57 @@ +use vstd::prelude::*; + +verus! { + +spec fn is_vowel(c: char) -> bool { + c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c == 'I' + || c == 'O' || c == 'U' +} + +spec fn vowels(s: Seq) -> Seq { + s.filter(|c| is_vowel(c)) +} + +fn vowels_count(s: &str) -> (ret: u32) + requires + s@.len() <= u32::MAX, + ensures + ret == vowels(s@).len() + if (s@.len() > 0 && (s@.last() == 'y' || s@.last() == 'Y')) { + 1int + + } else { + 0int + }, +{ + let mut ctr = 0; + let len = s.unicode_len(); + if len == 0 { + return ctr; + } + assert(len > 0); + let mut i = 0; + for i in 0..len + invariant + ctr == vowels(s@.subrange(0, i as int)).len(), + ctr <= i <= s@.len() == len <= u32::MAX, + ctr < u32::MAX || is_vowel(s@.last()), + { + let c = s.get_char(i); + reveal_with_fuel(Seq::filter, 2); + assert(s@.subrange(0, i + 1 as int).drop_last() =~= s@.subrange(0, i as int)); + if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c + == 'I' || c == 'O' || c == 'U') { + ctr += 1; + } + } + assert(ctr == vowels(s@).len()) by { + assert(s@.subrange(0, len as int) =~= s@); + } + let c = s.get_char(len - 1); + if (c == 'y' || c == 'Y') { + ctr += 1 + } + ctr +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/068-pluck.rs b/benches/HumanEval-RustBench/068-pluck.rs new file mode 100644 index 0000000..d5532fa --- /dev/null +++ b/benches/HumanEval-RustBench/068-pluck.rs @@ -0,0 +1,55 @@ +use vstd::prelude::*; + +verus! { + +fn pluck_smallest_even(nodes: &Vec) -> (result: Vec) + requires + nodes@.len() <= u32::MAX, + ensures + result@.len() == 0 || result@.len() == 2, + result@.len() == 0 ==> forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] % 2 != 0, + result@.len() == 2 ==> { + let node = result@[0]; + let index = result@[1]; + &&& 0 <= index < nodes@.len() + &&& nodes@[index as int] == node + &&& node % 2 == 0 + &&& forall|i: int| + 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> node <= nodes@[i] && forall|i: int| + 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > node + }, +{ + let mut smallest_even: Option = None; + let mut smallest_index: Option = None; + + for i in 0..nodes.len() + invariant + 0 <= i <= nodes@.len(), + nodes@.len() <= u32::MAX, + smallest_even.is_none() == smallest_index.is_none(), + smallest_index.is_none() ==> forall|j: int| 0 <= j < i ==> nodes@[j] % 2 != 0, + smallest_index.is_some() ==> { + &&& 0 <= smallest_index.unwrap() < i as int + &&& nodes@[smallest_index.unwrap() as int] == smallest_even.unwrap() + &&& smallest_even.unwrap() % 2 == 0 + &&& forall|j: int| + 0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j] + &&& forall|j: int| + 0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j] + > smallest_even.unwrap() + }, + { + if nodes[i] % 2 == 0 && (smallest_even.is_none() || nodes[i] < smallest_even.unwrap()) { + smallest_even = Some(nodes[i]); + smallest_index = Some((i as u32)); + } + } + if smallest_index.is_none() { + Vec::new() + } else { + vec![smallest_even.unwrap(), smallest_index.unwrap()] + } +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/070-strange_sort_list.rs b/benches/HumanEval-RustBench/070-strange_sort_list.rs new file mode 100644 index 0000000..bba839d --- /dev/null +++ b/benches/HumanEval-RustBench/070-strange_sort_list.rs @@ -0,0 +1,157 @@ +use vstd::calc; +use vstd::prelude::*; +use vstd::seq_lib::lemma_multiset_commutative; + +verus! { + +proof fn swap_preserves_multiset_helper(s: Seq, i: int, j: int) + requires + 0 <= i < j < s.len(), + 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)), +{ + let fst = s.take(i); + let snd = s.subrange(i + 1, j); + + assert((s.take(j + 1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add( + snd.to_multiset().insert(s.index(j)), + )) by { + assert(s.take(i + 1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { + fst.to_multiset_ensures(); + assert(fst.push(s.index(i)) =~= s.take(i + 1)); + } + assert(s.subrange(i + 1, j + 1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { + snd.to_multiset_ensures(); + assert(snd.push(s.index(j)) =~= s.subrange(i + 1, j + 1)); + } + lemma_multiset_commutative(s.take(i + 1), s.subrange(i + 1, j + 1)); + assert(s.take(i + 1) + s.subrange(i + 1, j + 1) =~= s.take(j + 1)); + } +} +proof fn swap_preserves_multiset(s1: Seq, s2: Seq, i: int, j: int) + 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), + ensures + s1.to_multiset() == s2.to_multiset(), +{ + calc! { + (==) + s1.to_multiset(); { + lemma_multiset_commutative(s1.take(j + 1), s1.skip(j + 1)); + assert(s1 =~= s1.take(j + 1) + s1.skip(j + 1)); + } + s1.take(j + 1).to_multiset().add(s1.skip(j + 1).to_multiset()); { + assert(s1.take(j + 1).to_multiset() =~= s2.take(j + 1).to_multiset()) by { + assert(s1.take(i) == s2.take(i)); + assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j))); + swap_preserves_multiset_helper(s1, i, j); + swap_preserves_multiset_helper(s2, i, j); + } + assert(s1.skip(j + 1).to_multiset() =~= s2.skip(j + 1).to_multiset()) by { + assert(s1.skip(j + 1) =~= s2.skip(j + 1)); + } + } + s2.take(j + 1).to_multiset().add(s2.skip(j + 1).to_multiset()); { + lemma_multiset_commutative(s2.take(j + 1), s2.skip(j + 1)); + assert(s2 =~= s2.take(j + 1) + s2.skip(j + 1)); + } + s2.to_multiset(); + } +} + +fn sort_seq(s: &Vec) -> (ret: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), + ret@.len() == s@.len(), + s@.to_multiset() == ret@.to_multiset(), +{ + let mut sorted = s.clone(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len(), + forall|j: int, k: int| 0 <= j < k < i ==> sorted@.index(j) <= sorted@.index(k), + s@.to_multiset() == sorted@.to_multiset(), + forall|j: int, k: int| + 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), + sorted@.len() == s@.len(), + { + let mut min_index: usize = i; + let mut j: usize = i + 1; + while j < sorted.len() + invariant + i <= min_index < j <= sorted.len(), + forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), + { + if sorted[j] < sorted[min_index] { + min_index = j; + } + j += 1; + } + if min_index != i { + let ghost old_sorted = sorted@; + let curr_val = sorted[i]; + let min_val = sorted[min_index]; + sorted.set(i, min_val); + + sorted.set(min_index, curr_val); + + proof { + swap_preserves_multiset(old_sorted, sorted@, i as int, min_index as int); + assert(old_sorted.to_multiset() =~= sorted@.to_multiset()); + } + } + i += 1; + } + sorted +} +fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) + ensures + s@.to_multiset() == (ret.0)@.to_multiset(), + s@.len() == (ret.0)@.len() == (ret.1)@.len(), + forall|i: int| + 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), + forall|i: int| + 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index( + s@.len() - (i - 1) / 2 - 1, + ), +{ + let sorted = sort_seq(s); + let mut strange = Vec::new(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len() == s@.len(), + strange@.len() == i, + forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2), + forall|j: int| + 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index( + sorted@.len() - (j / 2) - 1, + ), + { + if i % 2 == 0 { + strange.push(sorted[i / 2]); + } else { + let r = (i - 1) / 2; + strange.push(sorted[s.len() - r - 1]); + } + i += 1; + } + (sorted, strange) +} + +fn strange_sort_list(s: &Vec) -> (ret: Vec) + ensures + s@.len() == ret@.len(), +{ + let (_, strange) = strange_sort_list_helper(s); + strange +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/072-will_it_fly.rs b/benches/HumanEval-RustBench/072-will_it_fly.rs new file mode 100644 index 0000000..7becaf3 --- /dev/null +++ b/benches/HumanEval-RustBench/072-will_it_fly.rs @@ -0,0 +1,124 @@ +use vstd::prelude::*; + +verus! { +proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int) + requires + 0 <= i <= j <= s.len(), + ensures + spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + decreases j - i, +{ + 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_params(s, i, j - 1); + } +} + +proof fn lemma_increasing_sum(s: Seq) + ensures + forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), +{ + assert forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) by { + if (0 <= i <= j <= s.len()) { + lemma_increasing_sum_params(s, i, j); + } + } +} + +spec fn spec_sum(s: Seq) -> int { + s.fold_left(0, |x: int, y| x + y) +} + +fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) + ensures + ret <==> spec_sum(qs@) <= w, +{ + let mut sum: u32 = 0; + for i in 0..qs.len() + invariant + sum == spec_sum(qs@.subrange(0, i as int)), + i <= qs.len(), + sum <= w, + { + proof { + assert(spec_sum(qs@.subrange(0, i + 1)) <= spec_sum(qs@)) by { + assert(qs@ == qs@.subrange(0, qs@.len() as int)); + lemma_increasing_sum(qs@); + } + assert(spec_sum(qs@.subrange(0, i as int)) + qs[i as int] == spec_sum( + qs@.subrange(0, i + 1), + )) by { + assert(qs@.subrange(0, i + 1).drop_last() == qs@.subrange(0, i as int)); + } + } + let sum_opt = sum.checked_add(qs[i]); + if sum_opt.is_none() { + assert(spec_sum(qs@.subrange(0, i + 1)) > u32::MAX >= w); + return false; + } else { + sum = sum_opt.unwrap(); + if sum > w { + assert(spec_sum(qs@.subrange(0, i + 1)) > w); + return false; + } + } + } + assume(sum == spec_sum(qs@)); + true +} + +fn palindrome(qs: &Vec) -> (ret: bool) + ensures + ret <==> qs@ =~= qs@.reverse(), +{ + let mut ret = true; + let mut i: usize = 0; + while i < qs.len() / 2 + invariant + i <= qs@.len() / 2, + ret <==> qs@.subrange(0, i as int) =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse(), + { + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() + =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse().push(qs@.index(qs@.len() - (i + 1)))); + if qs[i] != qs[qs.len() - i - 1] { + ret = false; + } + i += 1; + } + let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int); + let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int); + proof { + if (qs.len() % 2) == 1 { + assert(qs@ =~= fst_half + qs@.subrange( + (qs@.len() / 2) as int, + qs@.len() - qs@.len() / 2, + ) + snd_half); + } else { + assert(qs@ =~= fst_half + snd_half); + } + } + ret +} + +fn will_it_fly(qs: &Vec, w: u32) -> (ret: bool) + ensures + ret <==> qs@ =~= qs@.reverse() && spec_sum(qs@) <= w, +{ + palindrome(qs) && sum_lesser_than_limit(qs, w) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/073-smallest_change.rs b/benches/HumanEval-RustBench/073-smallest_change.rs new file mode 100644 index 0000000..911e1b9 --- /dev/null +++ b/benches/HumanEval-RustBench/073-smallest_change.rs @@ -0,0 +1,50 @@ +use vstd::prelude::*; + +verus! { + +spec fn zip_halves(v: Seq) -> (ret: Seq<(T, T)>) { + v.take((v.len() / 2) as int).zip_with(v.skip(((v.len() + 1) / 2) as int).reverse()) +} + +spec fn diff(s: Seq<(i32, i32)>) -> int { + s.fold_left( + 0, + |acc: int, x: (i32, i32)| + if (x.0 != x.1) { + acc + 1 + } else { + acc + }, + ) +} + +fn smallest_change(v: Vec) -> (change: usize) + requires + v@.len() < usize::MAX, + ensures + change == diff(zip_halves(v@)), +{ + let mut ans: usize = 0; + let ghost zipped = Seq::<(i32, i32)>::empty(); + for i in 0..v.len() / 2 + invariant + ans <= i <= v@.len() / 2 < usize::MAX, + ans == diff(zipped), + zipped =~= zip_halves(v@).take(i as int), + { + proof { + let ghost pair = (v[i as int], v[v.len() - i - 1]); + let ghost zipped_old = zipped; + zipped = zipped.push(pair); + assert(zipped.drop_last() =~= zipped_old); + } + if v[i] != v[v.len() - i - 1] { + ans += 1; + } + } + assert(zip_halves(v@).take((v@.len() / 2) as int) =~= zip_halves(v@)); + ans +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/074-total_match.rs b/benches/HumanEval-RustBench/074-total_match.rs new file mode 100644 index 0000000..6858cf2 --- /dev/null +++ b/benches/HumanEval-RustBench/074-total_match.rs @@ -0,0 +1,87 @@ +use vstd::prelude::*; + +verus! { + +spec fn spec_sum(s: Seq) -> int { + s.fold_left(0, |x: int, y| x + y) +} +proof fn lemma_increasing_sum(s: Seq, i: int, j: int) + requires + 0 <= i <= j <= s.len(), + ensures + spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + decreases j - i, +{ + 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); + } +} + +spec fn total_str_len(strings: Seq<&str>) -> int { + spec_sum(strings.map_values(|s: &str| s@.len())) +} + +fn checked_total_str_len(lst: &Vec<&str>) -> (ret: Option) + ensures + ret.is_some() <==> total_str_len(lst@) <= usize::MAX, + ret.is_some() <==> ret.unwrap() == total_str_len(lst@), +{ + let ghost lens = Seq::::empty(); + let mut sum: usize = 0; + for i in 0..lst.len() + invariant + sum == lst@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( + 0, + |x: int, y| x + y, + ), + spec_sum(lens) == sum, + lens =~= lst@.map_values(|s: &str| s@.len()).take(i as int), + lens =~= lst@.take(i as int).map_values(|s: &str| s@.len()), + { + let x = lst[i].unicode_len(); + proof { + assert(lens.push(x as nat).drop_last() == lens); + lens = lens.push(x as nat); + assert(lens =~= lst@.map_values(|s: &str| s@.len()).take(i + 1)); + + lemma_increasing_sum(lst@.map_values(|s: &str| s@.len()), i + 1, lst@.len() as int); + assert(total_str_len(lst@) >= spec_sum(lens)) by { + assert(lst@.map_values(|s: &str| s@.len()) =~= lst@.map_values( + |s: &str| s@.len(), + ).take(lst@.len() as int)); + } + if x + sum > usize::MAX { + assert(sum.checked_add(x).is_none()); + assert(total_str_len(lst@) > usize::MAX); + } + } + sum = sum.checked_add(x)?; + assert(lst@.take(i + 1).map_values(|s: &str| s@.len()).drop_last() == lst@.take( + i as int, + ).map_values(|s: &str| s@.len())); + } + assert(lst@ == lst@.subrange(0, lst.len() as int)); + return Some(sum); +} + +fn total_match<'a>(lst1: Vec<&'a str>, lst2: Vec<&'a str>) -> (ret: Option>) + ensures + ret.is_some() <== total_str_len(lst1@) <= usize::MAX && total_str_len(lst2@) <= usize::MAX, + ret.is_some() ==> ret.unwrap() == if total_str_len(lst1@) <= total_str_len(lst2@) { + lst1 + } else { + lst2 + }, +{ + if checked_total_str_len(&lst1)? <= checked_total_str_len(&lst2)? { + Some(lst1) + } else { + Some(lst2) + } +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/075-is_multiply_prime.rs b/benches/HumanEval-RustBench/075-is_multiply_prime.rs new file mode 100644 index 0000000..388a121 --- /dev/null +++ b/benches/HumanEval-RustBench/075-is_multiply_prime.rs @@ -0,0 +1,121 @@ +use vstd::arithmetic::mul::*; +use vstd::prelude::*; + +verus! { + +spec fn spec_prime(p: int) -> bool { + p > 1 && forall|k: int| 1 < k < p ==> #[trigger] (p % k) != 0 +} + +fn prime(p: u32) -> (ret: bool) + ensures + ret <==> spec_prime(p as int), +{ + if p <= 1 { + return false; + } + for k in 2..p + invariant + forall|j: int| 1 < j < k ==> #[trigger] (p as int % j) != 0, + k <= p, + { + if p % k == 0 { + return false; + } + } + true +} + +fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option) + ensures + ret.is_some() ==> ret.unwrap() == x * y * z, + ret.is_none() ==> x * y * z > u32::MAX, +{ + if (x == 0 || y == 0 || z == 0) { + return Some(0); + } + assert(x > 0 && y > 0 && z > 0); + let prod2 = x.checked_mul(y); + if prod2.is_some() { + let prod3 = prod2.unwrap().checked_mul(z); + if prod3.is_some() { + let ans = prod3.unwrap(); + assert(ans == x * y * z); + Some(ans) + } else { + assert(x * y * z > u32::MAX); + None + } + } else { + broadcast use group_mul_properties; + + assert(x * y * z >= y * z); + None + } +} + +fn is_multiply_prime(x: u32) -> (ans: bool) + requires + x > 1, + ensures + ans <==> exists|a: int, b: int, c: int| + spec_prime(a) && spec_prime(b) && spec_prime(c) && x == a * b * c, +{ + let mut a = 1; + while a < x + invariant + forall|i: int, j: int, k: int| + (spec_prime(i) && spec_prime(j) && spec_prime(k) && i <= a && j <= x && k <= x) + ==> x != i * j * k, + a <= x, + { + a += 1; + if prime(a) { + let mut b = 1; + while b < x + invariant + forall|j: int, k: int| + (spec_prime(j) && spec_prime(k) && j <= b && k <= x) ==> x != (a as int) * j + * k, + spec_prime(a as int), + a <= x, + b <= x, + { + b += 1; + if prime(b) { + let mut c = 1; + while c < x + invariant + forall|k: int| (spec_prime(k) && k <= c as int) ==> x != a * b * k, + spec_prime(a as int), + spec_prime(b as int), + a <= x, + b <= x, + c <= x, + { + c += 1; + let prod = checked_mul_thrice(a, b, c); + if prime(c) && prod.is_some() && x == prod.unwrap() { + return true; + } + } + } + } + } + } + assert(forall|i: int, j: int, k: int| + i <= x && j <= x && k <= x && spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j + * k); + assert forall|i: int, j: int, k: int| + spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j * k by { + if (i > 1 && j > 1 && k > 1 && (i > x || j > x || k > x)) { + broadcast use group_mul_properties; + + assert(i * j * k > x); + } + } + false +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/076-is_simple_power.rs b/benches/HumanEval-RustBench/076-is_simple_power.rs new file mode 100644 index 0000000..2c18d2a --- /dev/null +++ b/benches/HumanEval-RustBench/076-is_simple_power.rs @@ -0,0 +1,37 @@ +use vstd::arithmetic::logarithm::log; +use vstd::arithmetic::power::pow; +use vstd::prelude::*; +verus! { +#[verifier::external_fn_specification] +pub fn ex_ilog(x: u32, base: u32) -> (ret: u32) + requires + x > 0, + base > 1, + ensures + ret == log(base as int, x as int), +{ + x.ilog(base) +} + +#[verifier::external_fn_specification] +pub fn ex_checked_pow(x: u32, exp: u32) -> (ret: Option) + ensures + ret.is_some() <==> ret.unwrap() == pow(x as int, exp as nat), + ret.is_none() <==> pow(x as int, exp as nat) > u32::MAX, +{ + x.checked_pow(exp) +} + +fn is_simple_power(x: u32, n: u32) -> (ret: bool) + requires + x > 0, + n > 1, + ensures + ret <==> x == pow(n as int, log(n as int, x as int) as nat), +{ + let maybe_x = n.checked_pow(x.ilog(n)); + return maybe_x.is_some() && maybe_x.unwrap() == x; +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/077-is_cube.rs b/benches/HumanEval-RustBench/077-is_cube.rs new file mode 100644 index 0000000..ca0fe21 --- /dev/null +++ b/benches/HumanEval-RustBench/077-is_cube.rs @@ -0,0 +1,131 @@ +use vstd::arithmetic::mul::*; +use vstd::math::abs; +use vstd::prelude::*; + +verus! { + +proof fn lemma_cube_increases_helper(i: int) + ensures + i >= 0 ==> (i * i * i) <= (i + 1) * (i + 1) * (i + 1), +{ + broadcast use group_mul_properties; + + if (i > 0) { + assert((i + 1) * (i + 1) * (i + 1) == i * i * i + 3 * i * i + 3 * i + 1); + assert(i * i * i + 3 * i * i + 3 * i + 1 > i * i * i); + } +} + +proof fn lemma_cube_increases_params(i: int, j: int) + ensures + 0 <= i <= j ==> (i * i * i) <= (j * j * j), + decreases j - i, +{ + if (i == j) { + } + else if (i < j) { + lemma_cube_increases_params(i, j - 1); + lemma_cube_increases_helper(j - 1); + + } +} + +proof fn lemma_cube_increases() + ensures + forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j), +{ + assert forall|i: int, j: int| + 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j) by { + lemma_cube_increases_params(i, j); + } +} + +fn checked_cube(x: i32) -> (ret: Option) + requires + x >= 0, + ensures + ret.is_some() ==> ret.unwrap() == x * x * x, + ret.is_none() ==> x * x * x > i32::MAX, +{ + if x == 0 { + return Some(0); + } + let sqr = x.checked_mul(x); + if sqr.is_some() { + let cube = sqr.unwrap().checked_mul(x); + if cube.is_some() { + let ans = cube.unwrap(); + assert(ans == x * x * x); + Some(ans) + } else { + assert(x * x * x > i32::MAX); + None + } + } else { + assert(x > 0); + assert(x * x > i32::MAX); + proof { + lemma_mul_increases(x as int, x * x); + } + assert(x * x * x >= x * x); + None + } +} + +#[verifier::external_fn_specification] +pub fn ex_abs(x: i32) -> (ret: i32) + requires + x != i32::MIN, + + ensures + ret == abs(x as int), +{ + x.abs() +} + +fn is_cube(x: i32) -> (ret: bool) + requires + x != i32::MIN, + + ensures + ret <==> exists|i: int| 0 <= i && abs(x as int) == #[trigger] (i * i * i), +{ + let x_abs = x.abs(); + if x_abs == 0 { + assert(abs(x as int) == 0 * 0 * 0); + return true; + } else if (x_abs == 1) { + assert(abs(x as int) == 1 * 1 * 1); + return true; + } + assert(-1 > x || x > 1); + let mut i = 2; + while i < x_abs + invariant + forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j), + 2 <= i <= abs(x as int) == x_abs, + { + let prod = checked_cube(i); + if prod.is_some() && prod.unwrap() == x.abs() { + return true; + } + i += 1; + } + assert(forall|j: int| 2 <= j ==> abs(x as int) != #[trigger] (j * j * j)) by { + assert(forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j)); + + assert(forall|j: int| i <= j ==> abs(x as int) < #[trigger] (j * j * j)) by { + assert(abs(x as int) < #[trigger] (i * i * i)) by { + broadcast use group_mul_properties; + + assert(i <= i * i <= i * i * i); + } + lemma_cube_increases(); + assert(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); + } + } + false +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/080-is_happy.rs b/benches/HumanEval-RustBench/080-is_happy.rs new file mode 100644 index 0000000..803cd6c --- /dev/null +++ b/benches/HumanEval-RustBench/080-is_happy.rs @@ -0,0 +1,45 @@ +use vstd::prelude::*; + +verus! { + +spec fn three_distinct_spec(s: Seq, i: int) -> bool + recommends + 0 < i && i + 1 < s.len(), +{ + (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1]) +} + +fn three_distinct(s: &Vec, i: usize) -> (is: bool) + requires + 0 < i && i + 1 < s.len(), + ensures + is <==> three_distinct_spec(s@, i as int), +{ + (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1]) +} + +spec fn happy_spec(s: Seq) -> bool { + s.len() >= 3 && (forall|i: int| 0 < i && i + 1 < s.len() ==> three_distinct_spec(s, i)) +} + +#[verifier::loop_isolation(false)] +fn is_happy(s: &Vec) -> (happy: bool) + ensures + happy <==> happy_spec(s@), +{ + if s.len() < 3 { + return false; + } + for i in 1..(s.len() - 1) + invariant + forall|j: int| 0 < j < i ==> three_distinct_spec(s@, j), + { + if !three_distinct(s, i) { + return false; + } + } + return true; +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/134-check_if_last_char_is_a_letter.rs b/benches/HumanEval-RustBench/134-check_if_last_char_is_a_letter.rs new file mode 100644 index 0000000..2d148e7 --- /dev/null +++ b/benches/HumanEval-RustBench/134-check_if_last_char_is_a_letter.rs @@ -0,0 +1,40 @@ +use vstd::prelude::*; + +verus! { + +pub spec fn is_alphabetic(c: char) -> (result: bool); + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(is_alphabetic)] +pub fn ex_is_alphabetic(c: char) -> (result: bool) + ensures + result <==> (c.is_alphabetic()), +{ + c.is_alphabetic() +} + +pub spec fn is_whitespace(c: char) -> (result: bool); + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(is_whitespace)] +pub fn ex_is_whitespace(c: char) -> (result: bool) + ensures + result <==> (c.is_whitespace()), +{ + c.is_whitespace() +} + +fn check_if_last_char_is_a_letter(txt: &str) -> (result: bool) + ensures + result <==> (txt@.len() > 0 && txt@.last().is_alphabetic() && (txt@.len() == 1 + || txt@.index(txt@.len() - 2).is_whitespace())), +{ + let len = txt.unicode_len(); + if len == 0 { + return false; + } + txt.get_char(len - 1).is_alphabetic() && (len == 1 || txt.get_char(len - 2).is_whitespace()) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/136-largest_smallest_integers.rs b/benches/HumanEval-RustBench/136-largest_smallest_integers.rs new file mode 100644 index 0000000..d6c8f66 --- /dev/null +++ b/benches/HumanEval-RustBench/136-largest_smallest_integers.rs @@ -0,0 +1,46 @@ +use vstd::prelude::*; + +verus! { + +fn largest_smallest_integers(arr: &Vec) -> (res: (Option, Option)) + ensures + ({ + let a = res.0; + let b = res.1; + &&& a.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] >= 0 + &&& a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0 + &&& a.is_some() ==> forall|i: int| + 0 <= i < arr@.len() && arr@[i] < 0 ==> arr@[i] <= a.unwrap() + &&& b.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] <= 0 + &&& b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0 + &&& b.is_some() ==> forall|i: int| + 0 <= i < arr@.len() && arr@[i] > 0 ==> arr@[i] >= b.unwrap() + }), +{ + let mut i: usize = 0; + let mut a = None; + let mut b = None; + + while i < arr.len() + invariant + 0 <= i <= arr@.len(), + a.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] >= 0, + a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0, + a.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] < 0 ==> arr@[j] <= a.unwrap(), + b.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] <= 0, + b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0, + b.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] > 0 ==> arr@[j] >= b.unwrap(), + { + if arr[i] < 0 && (a.is_none() || arr[i] >= a.unwrap()) { + a = Some(arr[i]); + } + if arr[i] > 0 && (b.is_none() || arr[i] <= b.unwrap()) { + b = Some(arr[i]); + } + i = i + 1; + } + (a, b) +} + +} +fn main() {} diff --git a/benches/HumanEval-RustBench/abs.rs b/benches/HumanEval-RustBench/abs.rs new file mode 100644 index 0000000..b33282e --- /dev/null +++ b/benches/HumanEval-RustBench/abs.rs @@ -0,0 +1,26 @@ +use vstd::prelude::*; + +verus! { + +fn abs(x: i32) -> (result: i32) + // pre-conditions-start + requires + x != i32::MIN, + // pre-conditions-end + // post-conditions-start + ensures + result >= 0, + result == x || result == -x, + // post-conditions-end +{ + // impl-start + if x < 0 { + -x + } else { + x + } + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/arithmetic_weird.rs b/benches/HumanEval-RustBench/arithmetic_weird.rs new file mode 100644 index 0000000..2ba2848 --- /dev/null +++ b/benches/HumanEval-RustBench/arithmetic_weird.rs @@ -0,0 +1,29 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn arithmetic_weird() -> (result: i32) + // post-conditions-start + ensures + result < 10 + // post-conditions-end +{ + // impl-start + let mut x = 0; + let mut y = 0; + while x <= 10 + // invariants-start + invariant + (x == 0 && y == 0) || y == 10 - x + 1 + // invariants-end + { + y = 10 - x; + x = x + 1; + } + y + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/array_append.rs b/benches/HumanEval-RustBench/array_append.rs new file mode 100644 index 0000000..3fe6e57 --- /dev/null +++ b/benches/HumanEval-RustBench/array_append.rs @@ -0,0 +1,33 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn array_append(a: Vec, b: i32) -> (result: Vec) + // post-conditions-start + ensures + result.len() == a.len() + 1, + forall|i: int| #![auto] 0 <= i && i < result.len() ==> result[i] == (if i < a.len() { a[i] } else { b }), + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == a[j], + // invariants-end + { + result.push(a[i]); + i = i + 1; + } + result.push(b); + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/array_concat.rs b/benches/HumanEval-RustBench/array_concat.rs new file mode 100644 index 0000000..102c16e --- /dev/null +++ b/benches/HumanEval-RustBench/array_concat.rs @@ -0,0 +1,47 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn array_concat(a: Vec, b: Vec) -> (result: Vec) + // post-conditions-start + ensures + result.len() == a.len() + b.len(), + forall|i: int| 0 <= i && i < a.len() ==> result[i] == a[i], + forall|i: int| 0 <= i && i < b.len() ==> result[i + a.len()] == b[i], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == a[j], + // invariants-end + { + result.push(a[i]); + i = i + 1; + } + let mut j = 0; + while j < b.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + 0 <= j && j <= b.len(), + result.len() == i + j, + forall|k: int| 0 <= k && k < i ==> result[k] == a[k], + forall|k: int| 0 <= k && k < j ==> result[k + i] == b[k], + // invariants-end + { + result.push(b[j]); + j = j + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/array_copy.rs b/benches/HumanEval-RustBench/array_copy.rs new file mode 100644 index 0000000..a51a4b5 --- /dev/null +++ b/benches/HumanEval-RustBench/array_copy.rs @@ -0,0 +1,32 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn array_copy(a: Vec) -> (result: Vec) + // post-conditions-start + ensures + result.len() == a.len(), + forall|i: int| 0 <= i && i < a.len() ==> result[i] == a[i], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == a[j], + // invariants-end + { + result.push(a[i]); + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/array_product.rs b/benches/HumanEval-RustBench/array_product.rs new file mode 100644 index 0000000..57fd41f --- /dev/null +++ b/benches/HumanEval-RustBench/array_product.rs @@ -0,0 +1,36 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn array_product(a: Vec, b: Vec) -> (result: Vec) by (nonlinear_arith) + // pre-conditions-start + requires + a.len() == b.len(), + // pre-conditions-end + // post-conditions-start + ensures + result.len() == a.len(), + forall|i: int| #![auto] 0 <= i && i < a.len() ==> result[i] == (a[i] as i64) * (b[i] as i64), + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| #![auto] 0 <= j && j < i ==> result[j] == (a[j] as i64) * (b[j] as i64), + // invariants-end + { + result.push(a[i] as i64 * b[i] as i64); + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/barrier.rs b/benches/HumanEval-RustBench/barrier.rs new file mode 100644 index 0000000..55d6b90 --- /dev/null +++ b/benches/HumanEval-RustBench/barrier.rs @@ -0,0 +1,53 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn barrier(arr: &[i32], p: usize) -> (result: bool) + // pre-conditions-start + requires + arr.len() > 0, + 0 <= p < arr.len(), + // pre-conditions-end + // post-conditions-start + ensures + result == forall|k: int, l: int| 0 <= k <= p && p < l < arr.len() ==> arr[k] < arr[l], + // post-conditions-end +{ + // impl-start + let mut i = 1; + let mut max: usize = 0; + while i <= p + // invariants-start + invariant + 0 <= i <= p + 1, + 0 <= max < i, + forall|k: int| 0 <= k < i ==> arr[max as int] >= arr[k], + // invariants-end + { + if arr[i] > arr[max] { + max = i; + } + i = i + 1; + } + + let mut result = true; + while i < arr.len() + // invariants-start + invariant + p < i <= arr.len(), + forall|k: int| 0 <= k <= p ==> arr[max as int] >= arr[k], + result == forall|k: int, l: int| 0 <= k <= p && p < l < i ==> arr[k] < arr[l], + // invariants-end + { + if arr[max] >= arr[i] { + result = false; + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/binary_search.rs b/benches/HumanEval-RustBench/binary_search.rs new file mode 100644 index 0000000..a6dbd25 --- /dev/null +++ b/benches/HumanEval-RustBench/binary_search.rs @@ -0,0 +1,44 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn binary_search(arr: &[i32], target: i32) -> (result: Option) + // pre-conditions-start + requires + forall|i: int, j: int| 0 <= i && i < j && j < arr.len() ==> arr[i] <= arr[j], + // pre-conditions-end + // post-conditions-start + ensures + match result { + Some(index) => arr[index as int] == target && arr.len() > 0 && index < arr.len(), + None => forall|i: int| 0 <= i && i < arr.len() ==> arr[i] != target, + }, + // post-conditions-end +{ + // impl-start + let mut low = 0; + let mut high = arr.len(); + while low < high + // invariants-start + invariant + low <= high && high <= arr.len(), + forall|i: int| 0 <= i && i < low ==> arr[i] < target, + forall|i: int| high <= i && i < arr.len() ==> arr[i] > target, + // invariants-end + { + let mid = low + (high - low) / 2; + if arr[mid] == target { + return Some(mid); + } else if arr[mid] < target { + low = mid; + } else { + high = mid; + } + } + None + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/binary_search_recursive.rs b/benches/HumanEval-RustBench/binary_search_recursive.rs new file mode 100644 index 0000000..d29748c --- /dev/null +++ b/benches/HumanEval-RustBench/binary_search_recursive.rs @@ -0,0 +1,46 @@ +use vstd::prelude::*; + +verus! { + +fn binary_search_recursive(v: &[i32], elem: i32, c: isize, f: isize) -> (p: isize) + // pre-conditions-start + requires + v.len() <= 100_000, + forall|i: int, j: int| 0 <= i < j < v.len() ==> v[i] <= v[j], + 0 <= c <= f + 1 <= v.len(), + forall|k: int| 0 <= k < c ==> v[k] <= elem, + forall|k: int| f < k < v.len() ==> v[k] > elem, + // pre-conditions-end + // post-conditions-start + ensures + -1 <= p < v.len(), + forall|u: int| 0 <= u <= p ==> v[u] <= elem, + forall|w: int| p < w < v.len() ==> v[w] > elem, + // post-conditions-end + decreases f - c + 1 +{ + // impl-start + if c == f + 1 { + return c as isize - 1; + } else { + let m = ((c + f) as usize / 2) as isize; + // assert-start + assert(m < v.len()) by { + assert(c <= f); + assert(f < v.len()) by { + assert(f + 1 <= v.len()); + }; + }; + // assert-end + if v[m as usize] <= elem { + return binary_search_recursive(v, elem, m + 1, f); + } else { + return binary_search_recursive(v, elem, c, m - 1); + } + } + // impl-end +} + + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/cubes.rs b/benches/HumanEval-RustBench/cubes.rs new file mode 100644 index 0000000..cdbec2b --- /dev/null +++ b/benches/HumanEval-RustBench/cubes.rs @@ -0,0 +1,52 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::external_body] +fn add(a: i32, b: i32) -> (result: i32) + ensures + result == a + b, +{ + a + b +} + +#[verifier::loop_isolation(false)] +fn cubes(len: usize) -> (result: Vec) by (nonlinear_arith) + // post-conditions-start + ensures + result.len() == len, + forall|i: int| 0 <= i && i < len ==> result[i] == i * i * i + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + + let mut c = 0; + let mut k = 1; + let mut m = 6; + + let mut n = 0; + while n < len + // invariants-start + invariant + 0 <= n && n <= len, + result.len() == n, + forall|i: int| 0 <= i && i < n ==> result[i] == i * i * i, + c == n * n * n, + k == 3 * n * n + 3 * n + 1, + m == 6 * n + 6, + // invariants-end + { + result.push(c); + + c = add(c, k); + k = add(k, m); + m = add(m, 6); + n = n + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/has_close_elements.rs b/benches/HumanEval-RustBench/has_close_elements.rs new file mode 100644 index 0000000..1ad9e52 --- /dev/null +++ b/benches/HumanEval-RustBench/has_close_elements.rs @@ -0,0 +1,65 @@ +use vstd::prelude::*; + +verus! { + +spec fn abs_spec(i: int) -> int { + if i < 0 { -i } else { i } +} + +fn abs(i: i32) -> (res: i32) + requires + i != i32::MIN, + ensures + i < 0 ==> res == -i, + i >= 0 ==> res == i +{ + if i < 0 { -i } else { i } +} + +#[verifier::loop_isolation(false)] +fn has_close_elements(numbers: &[i32], threshold: i32) -> (flag: bool) + // pre-conditions-start + requires + threshold > 0, + forall|i: int, j: int| 0 <= i && i < numbers.len() && 0 <= j && j < numbers.len() ==> numbers[i] - numbers[j] < i32::MAX && -(numbers[i] - numbers[j]) < i32::MAX + // pre-conditions-end + // post-conditions-start + ensures + flag == exists|i: int, j: int| 0 <= i && 0 <= j && i < numbers.len() && j < numbers.len() && i != j && abs_spec(numbers[i] - numbers[j]) < threshold + // post-conditions-end +{ + // impl-start + let mut flag = false; + let mut i = 0; + while i < numbers.len() + // invariants-start + invariant + 0 <= i && i <= numbers.len(), + flag == exists|i1: int, j1: int| 0 <= i1 && 0 <= j1 && i1 < i && j1 < numbers.len() && i1 != j1 && abs_spec(numbers[i1] - numbers[j1]) < threshold, + // invariants-end + { + let mut j = 0; + while j < numbers.len() + // invariants-start + invariant + 0 <= i && i < numbers.len(), + 0 <= j && j <= numbers.len(), + flag == exists|i1: int, j1: int| 0 <= i1 && 0 <= j1 && ((i1 < i && j1 < numbers.len()) || (i1 == i && j1 < j)) && i1 != j1 && abs_spec(numbers[i1] - numbers[j1]) < threshold, + // invariants-end + { + if i != j { + let distance = abs(numbers[i] - numbers[j]); + if distance < threshold { + flag = true; + } + } + j = j + 1; + } + i = i + 1; + } + flag + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/has_only_one_distinct_element.rs b/benches/HumanEval-RustBench/has_only_one_distinct_element.rs new file mode 100644 index 0000000..e58c64b --- /dev/null +++ b/benches/HumanEval-RustBench/has_only_one_distinct_element.rs @@ -0,0 +1,39 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn has_only_one_distinct_element(a: &[i32]) -> (result: bool) + // pre-conditions-start + // pre-conditions-end + // post-conditions-start + ensures + result ==> forall|i: int, j: int| 0 <= i < a.len() && 0 <= j < a.len() ==> a[i] == a[j], + !result ==> exists|i: int, j: int| 0 <= i < a.len() && 0 <= j < a.len() && a[i] != a[j], + // post-conditions-end +{ + // impl-start + if a.len() == 0 { + return true; + } + + let first = a[0]; + let mut i = 1; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int, l: int| 0 <= k < i && 0 <= l < i ==> a[k] == a[l], + // invariants-end + { + if a[i] != first { + return false; + } + i = i + 1; + } + true + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/index_wise_addition.rs b/benches/HumanEval-RustBench/index_wise_addition.rs new file mode 100644 index 0000000..82d4320 --- /dev/null +++ b/benches/HumanEval-RustBench/index_wise_addition.rs @@ -0,0 +1,62 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn index_wise_addition(a: &Vec>, b: &Vec>) -> (c: Vec>) + // pre-conditions-start + requires + a.len() == b.len(), + forall|i: int| #![auto] 0 <= i < a.len() ==> a[i].len() == b[i].len(), + forall|i: int| #![trigger a[i], b[i]] + 0 <= i < a.len() + ==> forall|j: int| 0 <= j < a[i].len() ==> a[i][j] + b[i][j] <= i32::MAX, + forall|i: int| #![trigger a[i], b[i]] + 0 <= i < a.len() + ==> forall|j: int| 0 <= j < a[i].len() ==> a[i][j] + b[i][j] >= i32::MIN, + // pre-conditions-end + // post-conditions-start + ensures + c.len() == a.len(), + forall|i: int| #![auto] 0 <= i < c.len() ==> c[i].len() == a[i].len(), + forall|i: int| #![trigger a[i], b[i], c[i]] + 0 <= i < c.len() + ==> forall|j: int| #![auto] 0 <= j < c[i].len() ==> c[i][j] == a[i][j] + b[i][j], + // post-conditions-end +{ + // impl-start + let mut c: Vec> = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + c.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> c[j].len() == a[j].len(), + forall|j: int| #![trigger a[j], b[j], c[j]] + 0 <= j < i + ==> forall|k: int| #![auto] 0 <= k < c[j].len() ==> c[j][k] == a[j][k] + b[j][k], + // invariants-end + { + let mut sub_c: Vec = Vec::new(); + let mut j = 0; + while j < a[i].len() + // invariants-start + invariant + 0 <= j <= a[i as int].len(), + sub_c.len() == j, + forall|k: int| #![auto] 0 <= k < j ==> sub_c[k] == a[i as int][k] + b[i as int][k], + // invariants-end + { + sub_c.push(a[i][j] + b[i][j]); + j = j + 1; + } + c.push(sub_c); + i = i + 1; + } + c + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/integer_square_root.rs b/benches/HumanEval-RustBench/integer_square_root.rs new file mode 100644 index 0000000..dd56c13 --- /dev/null +++ b/benches/HumanEval-RustBench/integer_square_root.rs @@ -0,0 +1,49 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::external_body] +fn add_one(n: i32) -> (result: i32) + ensures + result == n + 1, +{ + n + 1 +} + +#[verifier::external_body] +fn square(n: i32) -> (result: i32) + ensures + n * n == result, +{ + n * n +} + +fn integer_square_root(n: i32) -> (result: i32) + // pre-conditions-start + requires + n >= 1, + // pre-conditions-end + // post-conditions-start + ensures + 0 <= result * result, + result * result <= n, + n < (result + 1) * (result + 1) + // post-conditions-end +{ + // impl-start + let mut result = 0; + while square(add_one(result)) <= n + // invariants-start + invariant + 0 <= result, + 0 <= result * result <= n + // invariants-end + { + result = add_one(result); + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/intersperse.rs b/benches/HumanEval-RustBench/intersperse.rs new file mode 100644 index 0000000..8cdcadb --- /dev/null +++ b/benches/HumanEval-RustBench/intersperse.rs @@ -0,0 +1,38 @@ +use vstd::prelude::*; + +verus! { + +fn intersperse(numbers: &[i32], delim: i32) -> (res: Vec) + // post-conditions-start + ensures + numbers.len() == 0 ==> res.len() == 0, + numbers.len() != 0 ==> res.len() == 2 * numbers.len() - 1, + forall|i: int| 0 <= i && i < res.len() && i % 2 == 0 ==> res[i] == numbers[i / 2], + forall|i: int| 0 <= i && i < res.len() && i % 2 == 1 ==> res[i] == delim + // post-conditions-end +{ + // impl-start + let mut res = Vec::new(); + if numbers.len() != 0 { + let mut i = 0; + while i + 1 < numbers.len() + // invariants-start + invariant + 0 <= i && i < numbers.len(), + res.len() == 2 * i, + forall|j: int| 0 <= j && j < res.len() && j % 2 == 0 ==> res[j] == numbers[j / 2], + forall|j: int| 0 <= j && j < res.len() && j % 2 == 1 ==> res[j] == delim + // invariants-end + { + res.push(numbers[i]); + res.push(delim); + i += 1; + } + res.push(numbers[i]); + } + res + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/is_non_prime.rs b/benches/HumanEval-RustBench/is_non_prime.rs new file mode 100644 index 0000000..436b237 --- /dev/null +++ b/benches/HumanEval-RustBench/is_non_prime.rs @@ -0,0 +1,35 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn is_non_prime(n: u32) -> (result: bool) + // pre-conditions-start + requires + n >= 2, + // pre-conditions-end + // post-conditions-start + ensures + result == exists|k: int| 2 <= k < n && #[trigger] (n as int % k) == 0, + // post-conditions-end +{ + // impl-start + let mut i = 2; + while i < n + // invariants-start + invariant + 2 <= i <= n, + forall|k: int| 2 <= k < i ==> #[trigger] (n as int % k) != 0, + // invariants-end + { + if n % i == 0 { + return true; + } + i = i + 1; + } + false + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/is_sorted.rs b/benches/HumanEval-RustBench/is_sorted.rs new file mode 100644 index 0000000..f4f632a --- /dev/null +++ b/benches/HumanEval-RustBench/is_sorted.rs @@ -0,0 +1,39 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn is_sorted(lst: &[i32]) -> (result: bool) + // pre-conditions-start + requires + lst.len() >= 1, + // pre-conditions-end + // post-conditions-start + ensures + result <== forall|i: int, j: int| 0 <= i && i < j && j < lst.len() ==> lst[i] <= lst[j], + !result ==> exists|i: int, j: int| 0 <= i && i < j && j < lst.len() && lst[i] > lst[j], + // post-conditions-end +{ + // impl-start + let mut result = true; + let mut i = 0; + while i + 1 < lst.len() + // invariants-start + invariant + 0 <= i && i < lst.len(), + result <== forall|k: int, l: int| 0 <= k < l < i ==> lst[k] <= lst[l], + !result ==> exists|k: int, l: int| 0 <= k < l < i && lst[k] > lst[l], + // invariants-end + { + if lst[i] > lst[i + 1] { + result = false; + break; + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/largest_prime_factor.rs b/benches/HumanEval-RustBench/largest_prime_factor.rs new file mode 100644 index 0000000..d67982d --- /dev/null +++ b/benches/HumanEval-RustBench/largest_prime_factor.rs @@ -0,0 +1,66 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn is_prime(n: u32) -> (result: bool) + // pre-conditions-start + requires + n >= 2, + // pre-conditions-end + // post-conditions-start + ensures + result ==> (forall|k: int| 2 <= k < n ==> #[trigger] (n as int % k) != 0), + !result ==> exists|k: int| 2 <= k < n && #[trigger] (n as int % k) == 0, + // post-conditions-end +{ + // impl-start + let mut i = 2; + let mut result = true; + while i < n + // invariants-start + invariant + 2 <= i <= n, + result ==> forall|k: int| 2 <= k < i ==> #[trigger] (n as int % k) != 0, + !result ==> exists|k: int| 2 <= k < i && #[trigger] (n as int % k) == 0, + // invariants-end + { + if n % i == 0 { + result = false; + } + i = i + 1; + } + result + // impl-end +} + +spec fn is_prime_pred(n: u32) -> bool { + forall|k: int| 2 <= k < n ==> #[trigger] (n as int % k) != 0 +} + +#[verifier::loop_isolation(false)] +fn largest_prime_factor(n: u32) -> (result: u32) + requires + 2 <= n <= u32::MAX - 1, + ensures + 1 <= result <= n, + result == 1 || (result > 1 && is_prime_pred(result)) +{ + let mut largest = 1; + let mut i = 2; + while i <= n + invariant + 2 <= i <= n + 1, + 1 <= largest < i, + largest == 1 || (largest > 1 && is_prime_pred(largest)), + { + if n % i == 0 && is_prime(i) { + largest = i; + } + i = i + 1; + } + largest +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/last_position.rs b/benches/HumanEval-RustBench/last_position.rs new file mode 100644 index 0000000..d509291 --- /dev/null +++ b/benches/HumanEval-RustBench/last_position.rs @@ -0,0 +1,38 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn last_position(a: &[i32], elem: i32) -> (result: usize) + // pre-conditions-start + requires + 0 < a.len() < 100_000, + exists|i: int| 0 <= i < a.len() && a[i] == elem, + // pre-conditions-end + // post-conditions-start + ensures + 0 <= result < a.len(), + forall|i: int| result < i < a.len() ==> a[i] != elem, + a[result as int] == elem, + // post-conditions-end +{ + // impl-start + let mut i = a.len() as isize - 1; + while i >= 0 + // invariants-start + invariant + 0 <= i + 1 <= a.len() as isize, + forall|k: int| i < k < a.len() ==> a[k] != elem, + // invariants-end + { + if a[i as usize] == elem { + return i as usize; + } + i = i - 1; + } + a.len() + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/max_array.rs b/benches/HumanEval-RustBench/max_array.rs new file mode 100644 index 0000000..c9c6127 --- /dev/null +++ b/benches/HumanEval-RustBench/max_array.rs @@ -0,0 +1,38 @@ +use vstd::prelude::*; + +verus! { + +fn max_array(nums: &[i32]) -> (idx: usize) + // pre-conditions-start + requires + nums.len() >= 1, + // pre-conditions-end + // post-conditions-start + ensures + 0 <= idx && idx < nums.len(), + forall|i: int| 0 <= i && i < nums.len() ==> nums[i] <= nums[idx as int], + // post-conditions-end +{ + // impl-start + let mut idx = 0; + + let mut i = 1; + while i < nums.len() + // invariants-start + invariant + 0 < i <= nums.len(), + 0 <= idx && idx < i, + forall|j: int| 0 <= j && j < i ==> nums[j] <= nums[idx as int], + // invariants-end + { + if nums[i] > nums[idx] { + idx = i; + } + i = i + 1; + } + idx + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/max_dafny_lsp.rs b/benches/HumanEval-RustBench/max_dafny_lsp.rs new file mode 100644 index 0000000..46bfacc --- /dev/null +++ b/benches/HumanEval-RustBench/max_dafny_lsp.rs @@ -0,0 +1,48 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn max_dafny_lsp(a: &[i32]) -> (x: usize) + // pre-conditions-start + requires + a.len() > 0, + // pre-conditions-end + // post-conditions-start + ensures + 0 <= x < a.len(), + forall|k: int| 0 <= k < a.len() ==> a[k] <= a[x as int], + // post-conditions-end +{ + // impl-start + let mut x = 0; + let mut y = a.len() - 1; + + let ghost mut m = 0; + while x != y + // invariants-start + invariant + 0 <= x <= y < a.len(), + m == x || m == y, + forall|i: int| 0 <= i < x ==> a[i] <= a[m], + forall|i: int| y < i < a.len() ==> a[i] <= a[m], + // invariants-end + { + if a[x] <= a[y] { + x = x + 1; + proof { + m = y as int; + } + } else { + y = y - 1; + proof { + m = x as int; + } + } + } + x + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/remove_duplicates.rs b/benches/HumanEval-RustBench/remove_duplicates.rs new file mode 100644 index 0000000..358b266 --- /dev/null +++ b/benches/HumanEval-RustBench/remove_duplicates.rs @@ -0,0 +1,66 @@ +use vstd::prelude::*; + +verus! { + +spec fn in_array(a: Seq, x: i32) -> bool { + exists|i: int| 0 <= i < a.len() && a[i] == x +} + +fn in_array_exec(a: &Vec, x: i32) -> (result: bool) + // post-conditions-start + ensures + result == in_array(a@, x), + // post-conditions-end +{ + // impl-start + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int| 0 <= k < i ==> a[k] != x, + // invariants-end + { + if a[i] == x { + return true; + } + i = i + 1; + } + false + // impl-end +} + +#[verifier::loop_isolation(false)] +fn remove_duplicates(a: &[i32]) -> (result: Vec) + // pre-conditions-start + requires + a.len() >= 1, + // pre-conditions-end + // post-conditions-start + ensures + forall|i: int| #![auto] 0 <= i < result.len() ==> in_array(a@, result[i]), + forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] != result[j], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int| #![auto] 0 <= k < result.len() ==> in_array(a@, result[k]), + forall|k: int, l: int| 0 <= k < l < result.len() ==> result[k] != result[l], + // invariants-end + { + if !in_array_exec(&result, a[i]) { + result.push(a[i]); + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/remove_element.rs b/benches/HumanEval-RustBench/remove_element.rs new file mode 100644 index 0000000..58fa4d6 --- /dev/null +++ b/benches/HumanEval-RustBench/remove_element.rs @@ -0,0 +1,50 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn remove_element(a: &[i32], pos: usize) -> (result: Vec) + // pre-conditions-start + requires + 0 <= pos < a.len(), + // pre-conditions-end + // post-conditions-start + ensures + result.len() == a.len() - 1, + forall|i: int| 0 <= i < pos ==> result[i] == a[i], + forall|i: int| pos <= i < result.len() ==> result[i] == a[i + 1], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < pos + // invariants-start + invariant + 0 <= i <= pos, + forall|k: int| 0 <= k < i ==> result[k] == a[k], + result.len() == i, + // invariants-end + { + result.push(a[i]); + i = i + 1; + } + + while i + 1 < a.len() + // invariants-start + invariant + pos <= i < a.len(), + result.len() == i, + forall|k: int| 0 <= k < pos ==> result[k] == a[k], + forall|k: int| pos <= k < i ==> result[k] == a[k + 1], + // invariants-end + { + result.push(a[i + 1]); + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/remove_elements.rs b/benches/HumanEval-RustBench/remove_elements.rs new file mode 100644 index 0000000..bc7f28f --- /dev/null +++ b/benches/HumanEval-RustBench/remove_elements.rs @@ -0,0 +1,62 @@ +use vstd::prelude::*; + +verus! { + +spec fn in_array(a: Seq, x: i32) -> bool { + exists|i: int| 0 <= i < a.len() && a[i] == x +} + +fn in_array_exec(a: &Vec, x: i32) -> (result: bool) + // post-conditions-start + ensures + result == in_array(a@, x), + // post-conditions-end +{ + // impl-start + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int| 0 <= k < i ==> a[k] != x, + // invariants-end + { + if a[i] == x { + return true; + } + i = i + 1; + } + false + // impl-end +} + +#[verifier::loop_isolation(false)] +fn remove_elements(a: &Vec, b: &Vec) -> (c: Vec) + // post-conditions-start + ensures + forall|k: int| #![auto] 0 <= k < c.len() ==> in_array(a@, c[k]) && !in_array(b@, c[k]), + forall|i: int, j: int| 0 <= i < j < c.len() ==> c[i] != c[j], + // post-conditions-end +{ + // impl-start + let mut c: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int| #![auto] 0 <= k < c.len() ==> in_array(a@, c[k]) && !in_array(b@, c[k]), + forall|i: int, j: int| 0 <= i < j < c.len() ==> c[i] != c[j], + // invariants-end + { + if !in_array_exec(b, a[i]) && !in_array_exec(&c, a[i]) { + c.push(a[i]); + } + i = i + 1; + } + c + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/replace.rs b/benches/HumanEval-RustBench/replace.rs new file mode 100644 index 0000000..828c617 --- /dev/null +++ b/benches/HumanEval-RustBench/replace.rs @@ -0,0 +1,35 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn replace(a: &mut Vec, x: i32, y: i32) + // post-conditions-start + ensures + a.len() == old(a).len(), + forall|k: int| 0 <= k < old(a).len() && old(a)[k] == x ==> a[k] == y, + forall|k: int| 0 <= k < old(a).len() && old(a)[k] != x ==> a[k] == old(a)[k], + // post-conditions-end +{ + // impl-start + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + a.len() == old(a).len(), + forall|k: int| 0 <= k < i && old(a)[k] == x ==> a[k] == y, + forall|k: int| 0 <= k < i && old(a)[k] != x ==> a[k] == old(a)[k], + forall|k: int| i <= k < a.len() ==> a[k] == old(a)[k], + // invariants-end + { + if a[i] == x { + a.set(i, y); + } + i = i + 1; + } + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/replace_chars.rs b/benches/HumanEval-RustBench/replace_chars.rs new file mode 100644 index 0000000..3d7acbe --- /dev/null +++ b/benches/HumanEval-RustBench/replace_chars.rs @@ -0,0 +1,31 @@ +use vstd::prelude::*; + +verus! { + +fn replace_chars(s: &[char], old: char, new: char) -> (result: Vec) + // post-conditions-start + ensures + result.len() == s.len(), + forall|i: int| 0 <= i && i < result.len() ==> result[i] == (if s[i] == old { new } else { s[i] }), + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < s.len() + // invariants-start + invariant + 0 <= i && i <= s.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == (if s[j] == old { new } else { s[j] }), + // invariants-end + { + result.push(if s[i] == old { new } else { s[i] }); + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/reverse.rs b/benches/HumanEval-RustBench/reverse.rs new file mode 100644 index 0000000..151741d --- /dev/null +++ b/benches/HumanEval-RustBench/reverse.rs @@ -0,0 +1,31 @@ +use vstd::prelude::*; + +verus! { + +fn reverse(a: &[i32]) -> (result: Vec) + // post-conditions-start + ensures + result.len() == a.len(), + forall|i: int| 0 <= i && i < result.len() ==> result[i] == a[a.len() - 1 - i], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == a[a.len() - 1 - j] + // invariants-end + { + result.push(a[a.len() - 1 - i]); + i += 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/rolling_max.rs b/benches/HumanEval-RustBench/rolling_max.rs new file mode 100644 index 0000000..78c979b --- /dev/null +++ b/benches/HumanEval-RustBench/rolling_max.rs @@ -0,0 +1,50 @@ +use vstd::prelude::*; + +verus! { + +spec fn seq_max(a: Seq) -> i32 + decreases a.len(), +{ + if a.len() == 0 { + i32::MIN + } else if a.last() > seq_max(a.drop_last()) { + a.last() + } else { + seq_max(a.drop_last()) + } +} + +fn rolling_max(numbers: Vec) -> (result: Vec) + // post-conditions-start + ensures + result.len() == numbers.len(), + forall|i: int| 0 <= i < numbers.len() ==> result[i] == seq_max(numbers@.take(i + 1)), + // post-conditions-end +{ + // impl-start + let mut max_so_far = i32::MIN; + let mut result = Vec::with_capacity(numbers.len()); + let mut pos = 0; + while pos < numbers.len() + // invariants-start + invariant + 0 <= pos <= numbers.len(), + result.len() == pos, + max_so_far == seq_max(numbers@.take(pos as int)), + forall|i: int| 0 <= i < pos ==> result[i] == seq_max(numbers@.take(i + 1)), + pos < numbers.len() ==> numbers@.take((pos + 1) as int).drop_last() =~= numbers@.take(pos as int) + // invariants-end + { + let number = numbers[pos]; + if number > max_so_far { + max_so_far = number; + } + result.push(max_so_far); + pos += 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/smallest_list_length.rs b/benches/HumanEval-RustBench/smallest_list_length.rs new file mode 100644 index 0000000..18979bb --- /dev/null +++ b/benches/HumanEval-RustBench/smallest_list_length.rs @@ -0,0 +1,38 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn smallest_list_length(lists: Vec>) -> (result: usize) + // pre-conditions-start + requires + lists.len() > 0, + // pre-conditions-end + // post-conditions-start + ensures + exists|i: int| #![auto] 0 <= i < lists.len() && result == lists[i].len(), + forall|i: int| #![auto] 0 <= i < lists.len() ==> result <= lists[i].len(), + // post-conditions-end +{ + // impl-start + let mut result = lists[0].len(); + let mut i = 1; + while i < lists.len() + // invariants-start + invariant + 0 <= i <= lists.len(), + forall|j: int| #![auto] 0 <= j < i ==> result <= lists[j].len(), + exists|j: int| #![auto] 0 <= j < i && result == lists[j].len(), + // invariants-end + { + if lists[i].len() < result { + result = lists[i].len(); + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/smallest_missing_number.rs b/benches/HumanEval-RustBench/smallest_missing_number.rs new file mode 100644 index 0000000..c177665 --- /dev/null +++ b/benches/HumanEval-RustBench/smallest_missing_number.rs @@ -0,0 +1,46 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn smallest_missing_number(s: &[i32]) -> (v: i32) + // pre-conditions-start + requires + forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j], + forall|i: int| 0 <= i < s.len() ==> s[i] >= 0, + s.len() <= 100_000, + // pre-conditions-end + // post-conditions-start + ensures + 0 <= v, + forall|i: int| 0 <= i < s.len() ==> s[i] != v, + forall|k: int| 0 <= k < v && s[k] != v ==> exists|j: int| 0 <= j < s.len() && s[j] == k, + // post-conditions-end +{ + // impl-start + let mut v = 0; + let mut i = 0; + while i < s.len() + // invariants-start + invariant + 0 <= i <= s.len(), + 0 <= v <= i, + forall|k: int| 0 <= k < i ==> s[k] != v, + forall|k: int| 0 <= k < v && s[k] != v ==> exists|j: int| 0 <= j < i && s[j] == k, + // invariants-end + { + if s[i] > v { + break; + } else { + if s[i] == v { + v = v + 1; + } + } + i = i + 1; + } + v + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/string_xor.rs b/benches/HumanEval-RustBench/string_xor.rs new file mode 100644 index 0000000..be3d979 --- /dev/null +++ b/benches/HumanEval-RustBench/string_xor.rs @@ -0,0 +1,40 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn string_xor(a: &[char], b: &[char]) -> (result: Vec) + // pre-conditions-start + requires + a.len() == b.len(), + forall|i: int| 0 <= i && i < a.len() ==> a[i] == '0' || a[i] == '1', + forall|i: int| 0 <= i && i < b.len() ==> b[i] == '0' || b[i] == '1', + // pre-conditions-end + // post-conditions-start + ensures + result.len() == a.len(), + forall|i: int| 0 <= i && i < result.len() ==> (result[i] == '0' || result[i] == '1'), + forall|i: int| 0 <= i && i < result.len() ==> result[i] == (if a[i] == b[i] { '0' } else { '1' }) + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + result.len() == i, + forall|j: int| 0 <= j && j < i ==> result[j] == (if a[j] == b[j] { '0' } else { '1' }) + // invariants-end + { + let bit = if a[i] == b[i] { '0' } else { '1' }; + result.push(bit); + i += 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/two_sum.rs b/benches/HumanEval-RustBench/two_sum.rs new file mode 100644 index 0000000..6707924 --- /dev/null +++ b/benches/HumanEval-RustBench/two_sum.rs @@ -0,0 +1,57 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn two_sum(nums: &[i32], target: i32) -> (result: (usize, usize)) + // pre-conditions-start + requires + nums.len() >= 2, + exists|i: int, j: int| 0 <= i < j < nums.len() && nums[i] + nums[j] == target, + forall|i: int, j: int| + 0 <= i < nums.len() && 0 <= j < nums.len() + ==> nums[i] + nums[j] <= i32::MAX + && nums[i] + nums[j] >= i32::MIN, + // pre-conditions-end + // post-conditions-start + ensures + ({ let (i, j) = result; 0 <= i < nums.len() }), + ({ let (i, j) = result; 0 <= j < nums.len() }), + ({ let (i, j) = result; i != j }), + ({ let (i, j) = result; nums[i as int] + nums[j as int] == target }) + // post-conditions-end +{ + // impl-start + let mut i = 0; + + while i < nums.len() + // invariants-start + invariant + 0 <= i <= nums.len(), + forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + exists|u: int, v: int| i <= u < v < nums.len() && nums[u] + nums[v] == target, + // invariants-end + { + let mut j = i + 1; + while j < nums.len() + // invariants-start + invariant + 0 <= i < j <= nums.len(), + forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + exists|u: int, v: int| i <= u < v < nums.len() && nums[u] + nums[v] == target, + forall|u: int| i < u < j ==> nums[i as int] + nums[u] != target, + // invariants-end + { + if nums[i] + nums[j] == target { + return (i, j); + } + j = j + 1; + } + i = i + 1; + } + (0, 0) + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/two_way_sort.rs b/benches/HumanEval-RustBench/two_way_sort.rs new file mode 100644 index 0000000..207ad10 --- /dev/null +++ b/benches/HumanEval-RustBench/two_way_sort.rs @@ -0,0 +1,67 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::external_body] +fn swap(a: &mut Vec, i: usize, j: usize) + // pre-conditions-start + requires + 0 <= i < j < old(a).len(), + // pre-conditions-end + // post-conditions-start + ensures + a[i as int] == old(a)[j as int], + a[j as int] == old(a)[i as int], + forall|k: int| 0 <= k < a.len() && k != i && k != j ==> a[k] == old(a)[k], + a.len() == old(a).len(), + a@.to_multiset() =~~= old(a)@.to_multiset(), + // post-conditions-end +{ + // impl-start + let tmp = a[i]; + a.set(i, a[j]); + a.set(j, tmp); + // impl-end +} + +#[verifier::loop_isolation(false)] +fn two_way_sort(a: &mut Vec) + // pre-conditions-start + requires + old(a).len() <= 100_000, + // pre-conditions-end + // post-conditions-start + ensures + a.len() == old(a).len(), + a@.to_multiset() == old(a)@.to_multiset(), + forall|i: int, j: int| 0 <= i < j < a.len() ==> !a[i] || a[j], + // post-conditions-end +{ + // impl-start + let mut i = 0isize; + let mut j = a.len() as isize - 1; + while i <= j + // invariants-start + invariant + 0 <= i <= j + 1 <= a.len(), + forall|k: int| 0 <= k < i ==> !a[k], + forall|k: int| j < k < a.len() ==> a[k], + a.len() == old(a).len(), + a@.to_multiset() == old(a)@.to_multiset(), + // invariants-end + { + if !a[i as usize] { + i = i + 1; + } else if a[j as usize] { + j = j - 1; + } else { + swap(a, i as usize, j as usize); + i = i + 1; + j = j - 1; + } + } + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/unique.rs b/benches/HumanEval-RustBench/unique.rs new file mode 100644 index 0000000..f066cc7 --- /dev/null +++ b/benches/HumanEval-RustBench/unique.rs @@ -0,0 +1,43 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn unique(a: &[i32]) -> (result: Vec) + // pre-conditions-start + requires + forall|i: int, j: int| + #![trigger a[i], a[j]] + 0 <= i && i < j && j < a.len() ==> a[i] <= a[j], + // pre-conditions-end + // post-conditions-start + ensures + forall|i: int, j: int| + #![trigger result[i], result[j]] + 0 <= i && i < j && j < result.len() ==> result[i] < result[j], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i && i <= a.len(), + forall|i: int, j: int| 0 <= i && i < j && j < a.len() ==> a[i] <= a[j], + forall|i: int, j: int| 0 <= i && i < j && j < result.len() ==> #[trigger] result[i] < #[trigger] result[j], + result.len() == 0 || i == a.len() || result[result.len() - 1] <= a[i as int] + // invariants-end + { + if result.len() == 0 || result[result.len() - 1] != a[i] { + assert(result.len() == 0 || result[result.len() - 1] < a[i as int]); // assert-line + result.push(a[i]); + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/benches/HumanEval-RustBench/unique_better.rs b/benches/HumanEval-RustBench/unique_better.rs new file mode 100644 index 0000000..8d61865 --- /dev/null +++ b/benches/HumanEval-RustBench/unique_better.rs @@ -0,0 +1,46 @@ +use vstd::prelude::*; + +verus! { + +#[verifier::loop_isolation(false)] +fn unique_better(a: &[i32]) -> (result: Vec) + // pre-conditions-start + requires + forall|i: int, j: int| + #![trigger a[i], a[j]] + 0 <= i && i < j && j < a.len() ==> a[i] <= a[j], + // pre-conditions-end + // post-conditions-start + ensures + forall|i: int, j: int| + #![trigger result[i], result[j]] + 0 <= i && i < j && j < result.len() ==> result[i] < result[j], + // post-conditions-end +{ + // impl-start + let mut result: Vec = Vec::new(); + let mut i = 0; + while i < a.len() + // invariants-start + invariant + 0 <= i <= a.len(), + forall|k: int, l: int| + #![trigger result[k], result[l]] + 0 <= k && k < l && l < result.len() ==> result[k] < result[l], + forall|k: int| + #![trigger result[k]] + 0 <= k && k < result.len() ==> exists|m: int| 0 <= m < i && result[k] == a[m], + // invariants-end + { + if result.len() == 0 || result[result.len() - 1] != a[i] { + assert(result.len() == 0 || result[result.len() - 1] < a[i as int]); // assert-line + result.push(a[i]); + } + i = i + 1; + } + result + // impl-end +} + +fn main() {} +} diff --git a/flake.nix b/flake.nix index 9416483..a8eb780 100644 --- a/flake.nix +++ b/flake.nix @@ -7,10 +7,15 @@ inherit inputs; systems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ]; - devShell.packages = pkgs: with pkgs; [ - poetry - dafny - ]; - formatter = pkgs: with pkgs; [ nixpkgs-fmt ]; + devShell = pkgs: { + packages = pkgs: (with pkgs; [ + poetry + dafny + ]) ++ (pkgs.lib.optionals pkgs.stdenv.isDarwin (with pkgs.darwin.apple_sdk.frameworks; [ + AppKit + pkgs.libiconv + ])); + }; + formatter = pkgs: pkgs.nixpkgs-fmt; }; } diff --git a/scripts/process_files.fish b/scripts/process_files.fish new file mode 100644 index 0000000..ac09d27 --- /dev/null +++ b/scripts/process_files.fish @@ -0,0 +1,5 @@ +set VERUS_TASKS_DIR "/Users/Stanislav.Alekseev/Projects/human-eval-verus/tasks" + +for f in $VERUS_TASKS_DIR/*.rs + python process_verus_task.py $f +end diff --git a/scripts/process_verus_task.py b/scripts/process_verus_task.py new file mode 100644 index 0000000..05d0a4a --- /dev/null +++ b/scripts/process_verus_task.py @@ -0,0 +1,46 @@ +from sys import argv +from pathlib import Path + +dafny_files = Path( + "/Users/Stanislav.Alekseev/Projects/verified-cogen/benches/HumanEval-Dafny" +).glob("*.dfy") +dafny_files = [x.stem for x in dafny_files] +# print(dafny_files) + +with open(argv[1]) as task_file: + code = task_file.read() + if "TODO" in code: + exit(1) + else: + import re + + # Remove single-line comments + code = re.sub(r"//.*", "", code) + + code = re.sub(r"^\s+\n", "", code, flags=re.MULTILINE) + + # Remove multi-line comments + code = re.sub(r"/\*[\s\S]*?\*/", "", code, flags=re.MULTILINE) + + code = re.sub(r"^\s+", "", code) + code = re.sub(r"\s+$", "", code) + + code += "\n" + + # Create 'processed' folder if it doesn't exist + + processed_dir = Path("processed") + processed_dir.mkdir(exist_ok=True) + + number = Path(argv[1]).stem[-3:] + print(number) + result_name = None + for file in dafny_files: + if file.startswith(number): + result_name = file + + assert result_name is not None + # Save processed code to file in 'processed' folder + output_file = processed_dir / f"{result_name}.rs" + if not output_file.exists(): + output_file.write_text(code) diff --git a/run_validating.sh b/scripts/run_validating.sh similarity index 100% rename from run_validating.sh rename to scripts/run_validating.sh diff --git a/run_with_houdini.sh b/scripts/run_with_houdini.sh similarity index 100% rename from run_with_houdini.sh rename to scripts/run_with_houdini.sh