diff --git a/tasks/human_eval_001.rs b/tasks/human_eval_001.rs index 80045ca..3718c65 100644 --- a/tasks/human_eval_001.rs +++ b/tasks/human_eval_001.rs @@ -263,4 +263,3 @@ def check(candidate): assert candidate('( ) (( )) (( )( ))') == ['()', '(())', '(()())'] */ - diff --git a/tasks/human_eval_003c.rs b/tasks/human_eval_003c.rs index 72abb78..2e6c0c4 100644 --- a/tasks/human_eval_003c.rs +++ b/tasks/human_eval_003c.rs @@ -1,9 +1,7 @@ - /* ### ID HumanEval/3 */ - /* ### VERUS BEGIN */ @@ -13,34 +11,40 @@ verus! { // This function is part of the specification pub open spec fn sum(s: Seq) -> int - decreases s.len() + decreases s.len(), { - if s.len() == 0 { 0 } else { s[0] + sum(s.skip(1)) } + if s.len() == 0 { + 0 + } else { + s[0] + sum(s.skip(1)) + } } // This function is also part of the specification -pub open spec fn first_n(s: Seq, n: int) -> Seq -{ +pub open spec fn first_n(s: Seq, n: int) -> Seq { s.take(n).map(|_idx, j: i32| j as int) } // This function is used by the proof pub open spec fn sum_other_way(s: Seq) -> int - decreases s.len() + decreases s.len(), { - if s.len() == 0 { 0 } else { s.last() + sum_other_way(s.drop_last()) } + if s.len() == 0 { + 0 + } else { + s.last() + sum_other_way(s.drop_last()) + } } proof fn lemma_sum_equals_sum_other_way(s: Seq) ensures sum(s) == sum_other_way(s), - decreases s.len() + decreases s.len(), { if s.len() == 1 { assert(sum(s.skip(1)) == 0); assert(sum_other_way(s.drop_last()) == 0); - } - else if s.len() > 1 { + } else if s.len() > 1 { let ss = s.skip(1); lemma_sum_equals_sum_other_way(ss); assert(sum_other_way(ss) == ss.last() + sum_other_way(ss.drop_last())); @@ -52,7 +56,8 @@ proof fn lemma_sum_equals_sum_other_way(s: Seq) fn below_zero(operations: Vec) -> (result: bool) ensures - result <==> exists |i: int| 0 <= i <= operations@.len() && #[trigger] sum(first_n(operations@, i)) < 0, + result <==> exists|i: int| + 0 <= i <= operations@.len() && #[trigger] sum(first_n(operations@, i)) < 0, { let mut s = 0i32; let mut num_overflows: usize = 0; @@ -63,9 +68,11 @@ fn below_zero(operations: Vec) -> (result: bool) max_plus == i32::MAX + 1, s >= 0, s + num_overflows * max_plus == sum(first_n(operations@, k as int)), - forall |i: int| 0 <= i <= k ==> #[trigger] sum(first_n(operations@, i)) >= 0, + forall|i: int| 0 <= i <= k ==> #[trigger] sum(first_n(operations@, i)) >= 0, { - assert(sum(first_n(operations@, k as int)) + operations@[k as int] == sum(first_n(operations@, k + 1))) by { + assert(sum(first_n(operations@, k as int)) + operations@[k as int] == sum( + first_n(operations@, k + 1), + )) by { let q1 = first_n(operations@, k as int); let q2 = first_n(operations@, k + 1); assert(q2.last() == operations@[k as int] as int); @@ -78,12 +85,10 @@ fn below_zero(operations: Vec) -> (result: bool) if s > i32::MAX - op { s += op - i32::MAX - 1; num_overflows += 1; - } - else { + } else { s += op; } - } - else { + } else { s += op; if s < 0 { if num_overflows == 0 { @@ -98,7 +103,6 @@ fn below_zero(operations: Vec) -> (result: bool) } } // verus! - fn main() {} /* @@ -159,4 +163,3 @@ def check(candidate): assert candidate([1, -2, 2, -2, 5, -5, 4, -4]) == True */ - diff --git a/tasks/human_eval_004.rs b/tasks/human_eval_004.rs index d97fdd6..48cb1da 100644 --- a/tasks/human_eval_004.rs +++ b/tasks/human_eval_004.rs @@ -5,16 +5,20 @@ HumanEval/4 /* ### VERUS BEGIN */ +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::*; -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}; verus! { // NOTE: We use i32 rather than float because of lack of support for float in Verus. - /// Trusted specification functions - // Specification for what it means to sum a sequence of numbers pub open spec fn sum(numbers: Seq) -> int { numbers.fold_left(0, |acc: int, x| acc + x) @@ -23,28 +27,30 @@ pub open spec fn sum(numbers: Seq) -> int { // Specification for what it means to compute the mean of a sequence of numbers pub open spec fn mean(values: Seq) -> int recommends - values.len() > 0 + values.len() > 0, { sum(values) / (values.len() as int) } // Specification for what it means to compute the absolute value of a number -pub open spec fn abs(n: int) -> int -{ - if n >= 0 { n } else { -n } +pub open spec fn abs(n: int) -> int { + if n >= 0 { + n + } else { + -n + } } // Specification for what it means to compute the mean absolute deviation of a sequence of numbers pub open spec fn spec_mean_absolute_deviation(numbers: Seq) -> int recommends - numbers.len() > 0 + numbers.len() > 0, { let avg = mean(numbers); sum(numbers.map(|_index, n: int| abs(n - avg))) / (numbers.len() as int) } /// Lemmas used in proving correctness - // This lemma establishes that if every element of a sequence of // numbers `numbers` is between `min` and `max` inclusive, then their // sum is between `numbers.len() * min` and `numbers.len() * max` @@ -63,7 +69,6 @@ proof fn lemma_sum_bound(numbers: Seq, min: int, max: int) } } - // This lemma establishes that if every element of a sequence of // numbers `numbers` is between `min` and `max` inclusive, and if // certain other conditions apply, then their sum divided by @@ -100,9 +105,9 @@ proof fn lemma_sum_ratio_bound(numbers: Seq, denominator: int, min: int, ma // the `i`th element. proof fn lemma_how_to_update_running_sum(s: Seq, i: int) requires - 0 <= i < s.len() + 0 <= i < s.len(), ensures - sum(s.take(i + 1)) == sum(s.take(i)) + s[i] + sum(s.take(i + 1)) == sum(s.take(i)) + s[i], { let q1 = s.take(i); let q2 = s.take(i + 1); @@ -123,7 +128,7 @@ proof fn lemma_how_to_add_then_divide(x: int, y: int, d: int) } 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); @@ -131,8 +136,7 @@ proof fn lemma_how_to_add_then_divide(x: int, y: int, d: int) 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 { + } else { lemma_fundamental_div_mod_converse(x + y, d, (x / d) + (y / d), (x % d) + (y % d)); } } @@ -154,7 +158,6 @@ proof fn lemma_effect_of_dividing_by_two_or_more(x: int, d: int) } /// Subroutines used by target function - // This function divides an `i32` by a `u32` and returns the quotient // and remainder. You need this because Verus doesn't support using // the `/` and `%` operator on negative numbers. And even if it did, @@ -174,25 +177,23 @@ fn divide_i32_by_u32(x: i32, d: u32) -> (qr: (i32, u32)) if x >= 0 { return ((x as u32 / d) as i32, x as u32 % d); } - // When `x` is negative, compute `-x` as a `u32`. This is a bit // tricky because of the special case `i32::MIN`. + let neg_x: u32; if x == i32::MIN { if d == 1 { // If `x == i32::MIN` and `d == 1`, the algorithm below // won't work, so we special-case it here. return (x, 0); - } - else { + } else { // For the special case `x == i32::MIN`, we can't negate // it (because `-i32::MIN` isn't a valid `i32`). But we // can just directly assign the constant value of // `-i32::MIN` to a `u32`. neg_x = 0x80000000u32; } - } - else { + } else { neg_x = (-x) as u32; } assert(neg_x == -x); @@ -214,7 +215,6 @@ fn divide_i32_by_u32(x: i32, d: u32) -> (qr: (i32, u32)) lemma_mul_inequality(2, d as int, neg_x_div_d as int); } } - // There are two cases to consider. Case 1 is when `(-x) % d == // 0`. Case 2 is when it's positive. @@ -225,18 +225,22 @@ fn divide_i32_by_u32(x: i32, d: u32) -> (qr: (i32, u32)) 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 { + } 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); + 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) } } - + // This function divides an `i32` by a `usize` and returns the // quotient and remainder. You need this because Verus doesn't support // using the `/` and `%` operator on negative numbers. And even if it @@ -262,26 +266,27 @@ fn divide_i32_by_usize(x: i32, d: usize) -> (qr: (i32, usize)) // // (3) `d > u32::MAX` and `x < 0`, so we know that the // quotient and remainder are `-1` and `d + x`. - 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 { + } 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 { + } 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); } - // The remainder is `d + x`, but we can't directly add those // two values because we can't cast them to the same type. So instead // we compute `-x` then use subtraction to compute `d - (-x)`. - let neg_x: usize = if x == i32::MIN { 0x80000000usize } else { (-x) as usize }; + + let neg_x: usize = if x == i32::MIN { + 0x80000000usize + } else { + (-x) as usize + }; (-1, d - neg_x) } } @@ -307,7 +312,6 @@ fn compute_mean_of_i32s(numbers: &[i32]) -> (result: i32) // `quotient` and `remainder`. At the end of the loop, we return // `quotient` since it's the overall sum divided by the length of // the slice. - let ghost nums = numbers@.map(|_index, n: i32| n as int); let mut quotient: i32 = 0; let mut remainder: usize = 0; @@ -337,7 +341,12 @@ fn compute_mean_of_i32s(numbers: &[i32]) -> (result: i32) 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_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); } @@ -352,13 +361,11 @@ fn compute_mean_of_i32s(numbers: &[i32]) -> (result: i32) } remainder -= (numbers_len - r); quotient += (q + 1); - } - else { + } else { remainder += r; quotient += q; } } - assert(nums == nums.take(nums.len() as int)); quotient } @@ -371,25 +378,29 @@ fn compute_absolute_difference(x: i32, y: i32) -> (z: u32) 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 }; + } else { + let neg_y: u32 = if y == i32::MIN { + 0x80000000u32 + } else { + (-y) as u32 + }; x as u32 + neg_y } - } - else { + } else { if x >= 0 || y < 0 { (y - x) as u32 - } - else { - let neg_x: u32 = if x == i32::MIN { 0x80000000u32 } else { (-x) as u32 }; + } else { + let neg_x: u32 = if x == i32::MIN { + 0x80000000u32 + } else { + (-x) as u32 + }; y as u32 + neg_x } } } /// Target function - pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) requires numbers.len() > 0, @@ -397,7 +408,9 @@ pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) 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 ghost deviations = numbers@.map(|_index, n: i32| n as int).map( + |_index, n: int| abs(n - numbers_mean), + ); // The natural way to compute the mean absolute deviation is to // first compute the sum and then divide by the length. But this @@ -424,7 +437,9 @@ pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) 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)), + 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); @@ -444,8 +459,17 @@ pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) 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); + 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; @@ -460,13 +484,11 @@ pub fn mean_absolute_deviation(numbers: &[i32]) -> (result: u32) } remainder -= (numbers_len - r); quotient += (q + 1); - } - else { + } else { remainder += r; quotient += q; } } - assert(deviations == deviations.take(deviations.len() as int)); quotient }