From 65cdf99094a214d97b7d195c10fdb048901292ac Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Mon, 23 Sep 2024 14:46:49 -0400 Subject: [PATCH 01/22] Complete task015 (Elanor, Amar, Yi) (#13) --------- Co-authored-by: Amar Shah --- tasks/human_eval_015.rs | 163 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 161 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_015.rs b/tasks/human_eval_015.rs index 1fb9bd4..2acd8d4 100644 --- a/tasks/human_eval_015.rs +++ b/tasks/human_eval_015.rs @@ -9,10 +9,169 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// specification +pub closed spec fn single_digit_number_to_char(n: nat) -> char { + if n == 0 { + '0' + } else if n == 1 { + '1' + } else if n == 2 { + '2' + } else if n == 3 { + '3' + } else if n == 4 { + '4' + } else if n == 5 { + '5' + } else if n == 6 { + '6' + } else if n == 7 { + '7' + } else if n == 8 { + '8' + } else { + '9' + } +} + +pub closed spec fn number_to_char(n: nat) -> Seq + decreases n, +{ + if (n == 0) { + seq![] + } else { + number_to_char(n / 10).add(seq![single_digit_number_to_char(n % 10)]) + } +} + +pub open spec fn string_sequence(n: nat) -> Seq + decreases n, +{ + if n == 0 { + seq!['0'] + } else { + string_sequence((n - 1) as nat).add(seq![' '].add(number_to_char(n))) + } +} + +proof fn sanity_check() { + assert(string_sequence(1) == seq!['0', ' ', '1']) by (compute); + assert(string_sequence(3) == seq!['0', ' ', '1', ' ', '2', ' ', '3']) by (compute); + assert(string_sequence(12) == seq![ + '0', + ' ', + '1', + ' ', + '2', + ' ', + '3', + ' ', + '4', + ' ', + '5', + ' ', + '6', + ' ', + '7', + ' ', + '8', + ' ', + '9', + ' ', + '1', + '0', + ' ', + '1', + '1', + ' ', + '1', + '2', + ]) by (compute); + assert((number_to_char(158) == seq!['1', '5', '8'])) by (compute); +} + +// implementation +fn single_digit_number_to_char_impl(n: u8) -> (output: char) + requires + 0 <= n <= 9, + ensures + single_digit_number_to_char(n as nat) == output, +{ + if n == 0 { + '0' + } else if n == 1 { + '1' + } else if n == 2 { + '2' + } else if n == 3 { + '3' + } else if n == 4 { + '4' + } else if n == 5 { + '5' + } else if n == 6 { + '6' + } else if n == 7 { + '7' + } else if n == 8 { + '8' + } else { + '9' + } +} + +pub fn number_to_char_impl(n: u8) -> (char_vec: Vec) + ensures + char_vec@ == number_to_char(n as nat), +{ + let mut i = n; + let mut output = vec![]; + + while (i > 0) + invariant + number_to_char(n as nat) == number_to_char(i as nat).add(output@), + { + let m = i % 10; + let current = single_digit_number_to_char_impl(m); + output.insert(0, current); + i = i / 10; + + assert(number_to_char(n as nat) == number_to_char(i as nat).add(output@)); + } + return output; +} + +fn string_sequence_impl(n: u8) -> (string_seq: Vec) + ensures + string_seq@ == string_sequence(n as nat), +{ + let mut i = n; + let mut output = vec![]; + while (i > 0) + invariant + n >= i >= 0, + string_sequence(n as nat) == string_sequence(i as nat) + output@, + decreases i, + { + let mut next = number_to_char_impl(i); + next.append(&mut output); + output = next; + output.insert(0, ' '); + i = i - 1; + + assert(string_sequence((n) as nat) == string_sequence((i) as nat) + output@); + } + output.insert(0, '0'); + assert(string_sequence(n as nat) == output@); + return output; +} } // verus! -fn main() {} +fn main() { + print!("{:?}", string_sequence_impl(0)); + print!("{:?}", string_sequence_impl(5)); + print!("{:?}", string_sequence_impl(20)); +} /* ### VERUS END From 6bd1eed59949b8bf79d8e8ea2e1eeab5c9596fc3 Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Wed, 25 Sep 2024 06:00:37 -0700 Subject: [PATCH 02/22] Complete task 026 (#14) --- tasks/human_eval_026.rs | 71 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 70 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_026.rs b/tasks/human_eval_026.rs index 2f34c81..4556cfc 100644 --- a/tasks/human_eval_026.rs +++ b/tasks/human_eval_026.rs @@ -9,7 +9,76 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// This spec function recursively computes the frequency of an element in a given sequence. +pub open spec fn count_frequency_spec(seq: Seq, key: i64) -> int + decreases seq.len(), +{ + if seq.len() == 0 { + 0 + } else { + count_frequency_spec(seq.drop_last(), key) + if (seq.last() == key) { + 1 as int + } else { + 0 as int + } + } +} + +// This auxilary exe function computes the frequency of an element in a given sequence +fn count_frequency(elements: &Vec, key: i64) -> (frequency: usize) + ensures + count_frequency_spec(elements@, key) == frequency, +{ + let ghost elements_length = elements.len(); + let mut counter = 0; + let mut index = 0; + while index < elements.len() + invariant + 0 <= index <= elements.len(), + 0 <= counter <= index, + count_frequency_spec(elements@.subrange(0, index as int), key) == counter, + { + if (elements[index] == key) { + counter += 1; + } + index += 1; + assert(elements@.subrange(0, index - 1 as int) == elements@.subrange( + 0, + index as int, + ).drop_last()); + } + assert(elements@ == elements@.subrange(0, elements_length as int)); + counter +} + +//This function removes all elements that occur more than once +// Implementation following the ground-truth +fn remove_duplicates(numbers: &Vec) -> (unique_numbers: Vec) + ensures + unique_numbers@ == numbers@.filter(|x: i64| count_frequency_spec(numbers@, x) == 1), +{ + let ghost numbers_length = numbers.len(); + let mut unique_numbers: Vec = Vec::new(); + assert(numbers@.take(0int).filter(|x: i64| count_frequency_spec(numbers@, x) == 1) == Seq::< + i64, + >::empty()); + + for index in 0..numbers.len() + invariant + 0 <= index <= numbers.len(), + unique_numbers@ == numbers@.take(index as int).filter( + |x: i64| count_frequency_spec(numbers@, x) == 1, + ), + { + if count_frequency(&numbers, numbers[index]) == 1 { + unique_numbers.push(numbers[index]); + } + assert(numbers@.take((index + 1) as int).drop_last() == numbers@.take(index as int)); + reveal(Seq::filter); + } + assert(numbers@ == numbers@.take(numbers_length as int)); + unique_numbers +} } // verus! fn main() {} From 2133f8e00e60ddb68c7b3265480fa3cd81a44a51 Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Thu, 26 Sep 2024 13:58:16 -0700 Subject: [PATCH 03/22] Completed task 027 (#15) --- tasks/human_eval_027.rs | 53 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_027.rs b/tasks/human_eval_027.rs index a954145..d7016ba 100644 --- a/tasks/human_eval_027.rs +++ b/tasks/human_eval_027.rs @@ -9,7 +9,58 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +pub open spec fn is_upper_case(c: char) -> bool { + c >= 'A' && c <= 'Z' +} + +pub open spec fn is_lower_case(c: char) -> bool { + c >= 'a' && c <= 'z' +} + +pub open spec fn shift_plus_32_spec(c: char) -> char { + ((c as u8) + 32) as char +} + +pub open spec fn shift_minus_32_spec(c: char) -> char { + ((c as u8) - 32) as char +} + +// This spec function tranforms a lowercase character to uppercase and vice-versa +pub open spec fn flip_case_spec(c: char) -> char { + if is_lower_case(c) { + shift_minus_32_spec(c) + } else if is_upper_case(c) { + shift_plus_32_spec(c) + } else { + c + } +} + +// Implementation following the ground-truth (i.e, swapcase()) +fn flip_case(str: &[char]) -> (flipped_case: Vec) + ensures + str@.len() == flipped_case@.len(), + forall|i: int| 0 <= i < str.len() ==> flipped_case[i] == flip_case_spec(#[trigger] str[i]), +{ + let mut flipped_case = Vec::with_capacity(str.len()); + + for index in 0..str.len() + invariant + 0 <= index <= str.len(), + flipped_case.len() == index, + forall|i: int| 0 <= i < index ==> flipped_case[i] == flip_case_spec(#[trigger] str[i]), + { + if (str[index] >= 'a' && str[index] <= 'z') { + flipped_case.push(((str[index] as u8) - 32) as char); + } else if (str[index] >= 'A' && str[index] <= 'Z') { + flipped_case.push(((str[index] as u8) + 32) as char); + } else { + flipped_case.push(str[index]); + } + assert(flipped_case[index as int] == flip_case_spec(str[index as int])); + } + flipped_case +} } // verus! fn main() {} From 1aa8515aef1120a688dcd7dbbd34b549b228de3e Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Sat, 28 Sep 2024 08:52:58 -0700 Subject: [PATCH 04/22] Completed task 066 (#19) --- tasks/human_eval_066.rs | 53 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_066.rs b/tasks/human_eval_066.rs index 6021409..9b37076 100644 --- a/tasks/human_eval_066.rs +++ b/tasks/human_eval_066.rs @@ -9,7 +9,58 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn is_upper_case(c: char) -> bool { + c >= 'A' && c <= 'Z' +} + +// This spec function computes uppercase character (i.e, ASCII code) sum. +spec fn count_uppercase_sum(seq: Seq) -> int + decreases seq.len(), +{ + if seq.len() == 0 { + 0 + } else { + count_uppercase_sum(seq.drop_last()) + if is_upper_case(seq.last()) { + seq.last() as int + } else { + 0 as int + } + } +} + +// This function takes a string as input and returns the sum of the upper characters only' +fn digit_sum(text: &[char]) -> (sum: u128) + ensures + count_uppercase_sum(text@) == sum, +{ + let mut index = 0; + let mut sum = 0u128; + + while index < text.len() + invariant + 0 <= index <= text.len(), + count_uppercase_sum(text@.subrange(0, index as int)) == sum, + forall|j: int| + 0 <= j <= index ==> (u64::MIN * index <= (count_uppercase_sum( + #[trigger] text@.subrange(0, j), + )) <= u64::MAX * index), + u64::MIN * index <= sum <= u64::MAX * index, + { + if (text[index] >= 'A' && text[index] <= 'Z') { + assert(text@.subrange(0, index as int) =~= text@.subrange( + 0, + (index + 1) as int, + ).drop_last()); + sum = sum + text[index] as u128; + } + index += 1; + assert(text@.subrange(0, index - 1 as int) == text@.subrange(0, index as int).drop_last()); + + } + assert(index == text@.len()); + assert(text@ == text@.subrange(0, index as int)); + sum +} } // verus! fn main() {} From 8db9b06f016c2b79e8d31a86d7870f48bf5afdb4 Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Sat, 28 Sep 2024 11:11:55 -0700 Subject: [PATCH 05/22] Completed task 082 (#20) --- tasks/human_eval_082.rs | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_082.rs b/tasks/human_eval_082.rs index 7ff2683..dc7735d 100644 --- a/tasks/human_eval_082.rs +++ b/tasks/human_eval_082.rs @@ -9,7 +9,39 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +pub open spec fn is_divisible(n: int, divisor: int) -> bool { + (n % divisor) == 0 +} + +pub open spec fn is_prime(n: int) -> bool { + if n < 2 { + false + } else { + (forall|k: int| 2 <= k < n ==> !is_divisible(n as int, k)) + } +} + +// Implementation following the ground-truth +// This function checks whether a given string length is prime +fn prime_length(str: &[char]) -> (result: bool) + ensures + result == is_prime(str.len() as int), +{ + if str.len() < 2 { + return false; + } + for index in 2..str.len() + invariant + 2 <= index <= str.len(), + forall|k: int| 2 <= k < index ==> !is_divisible(str.len() as int, k), + { + if ((str.len() % index) == 0) { + assert(is_divisible(str.len() as int, index as int)); + return false; + } + } + true +} } // verus! fn main() {} From 6cb516d000a5e2c6612f7274423652342d545022 Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Sat, 28 Sep 2024 11:13:24 -0700 Subject: [PATCH 06/22] Completed task 051 (#18) --- tasks/human_eval_051.rs | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_051.rs b/tasks/human_eval_051.rs index fac3fd7..4e31c40 100644 --- a/tasks/human_eval_051.rs +++ b/tasks/human_eval_051.rs @@ -9,7 +9,44 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// This spec function checks whether a character is vowel +pub open spec fn is_vowel_spec(c: char) -> bool { + c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c == 'I' + || c == 'O' || c == 'U' +} + +// This auxilary exe function checks whether a character is vowel +fn is_vowel(c: char) -> (is_vowel: bool) + ensures + is_vowel == is_vowel_spec(c), +{ + c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c == 'I' + || c == 'O' || c == 'U' +} + +// Implementation following the ground-truth +// This function removes vowels from a given string +fn remove_vowels(str: &[char]) -> (str_without_vowels: Vec) + ensures + str_without_vowels@ == str@.filter(|x: char| !is_vowel_spec(x)), +{ + let ghost str_length = str.len(); + let mut str_without_vowels: Vec = Vec::new(); + assert(str@.take(0int).filter(|x: char| !is_vowel_spec(x)) == Seq::::empty()); + + for index in 0..str.len() + invariant + str_without_vowels@ == str@.take(index as int).filter(|x: char| !is_vowel_spec(x)), + { + if !is_vowel(str[index]) { + str_without_vowels.push(str[index]); + } + assert(str@.take((index + 1) as int).drop_last() == str@.take(index as int)); + reveal(Seq::filter); + } + assert(str@ == str@.take(str_length as int)); + str_without_vowels +} } // verus! fn main() {} From d6a314c14946068e007e419d385256b3758485c2 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Sat, 28 Sep 2024 15:52:21 -0400 Subject: [PATCH 07/22] Strengthen specs (#21) The specs for tasks 8, 55a, 55b, 59, 60, 62, and 63 permitted trivial programs (e.g., that simply returned None). The new versions are more restrictive, only allowing None to be returned under specific circumstances. --- tasks/human_eval_008.rs | 17 +++++++++++++- tasks/human_eval_055a.rs | 40 +++++++++++++++++++++++++++++++-- tasks/human_eval_055b.rs | 41 +++++++++++++++++++++++++++++++--- tasks/human_eval_059.rs | 4 ++++ tasks/human_eval_060.rs | 37 ++++++++++++++++++++++++++++--- tasks/human_eval_062.rs | 30 +++++++++++++++++++------ tasks/human_eval_063.rs | 48 ++++++++++++++++++++++++++++++++++++++-- 7 files changed, 199 insertions(+), 18 deletions(-) diff --git a/tasks/human_eval_008.rs b/tasks/human_eval_008.rs index 424cb15..b3466d9 100644 --- a/tasks/human_eval_008.rs +++ b/tasks/human_eval_008.rs @@ -38,7 +38,14 @@ fn sum_product(numbers: Vec) -> (result: (u64, Option)) numbers.len() < u32::MAX, ensures result.0 == sum(numbers@), - result.1 matches Some(v) ==> v == product(numbers@), + match result.1 { + None => // Computing the product overflowed at some point + exists|i| + #![auto] + 0 <= i < numbers.len() && product(numbers@.subrange(0, i)) * numbers[i] as int + > u32::MAX, + Some(v) => v == product(numbers@), + }, { let mut sum_value: u64 = 0; let mut prod_value: Option = Some(1); @@ -47,6 +54,14 @@ fn sum_product(numbers: Vec) -> (result: (u64, Option)) numbers.len() < u32::MAX, sum_value == sum(numbers@.take(index as int)), prod_value matches Some(v) ==> v == product(numbers@.take(index as int)), + match prod_value { + None => // Computing the product overflowed at some point + exists|i| + #![auto] + 0 <= i < index && product(numbers@.subrange(0, i)) * numbers[i] as int + > u32::MAX, + Some(v) => v == product(numbers@.take(index as int)), + }, index <= numbers.len(), index >= 0, { diff --git a/tasks/human_eval_055a.rs b/tasks/human_eval_055a.rs index a379fb8..4fb5fb3 100644 --- a/tasks/human_eval_055a.rs +++ b/tasks/human_eval_055a.rs @@ -9,6 +9,7 @@ use vstd::prelude::*; verus! { +#[verifier::memoize] spec fn spec_fib(n: nat) -> nat decreases n, { @@ -21,17 +22,52 @@ spec fn spec_fib(n: nat) -> nat } } +proof fn lemma_fib_monotonic(i: nat, j: nat) + requires + i <= j, + ensures + spec_fib(i) <= spec_fib(j), + decreases j - i, +{ + if (i < 2 && j < 2) || i == j { + } else if i == j - 1 { + reveal_with_fuel(spec_fib, 2); + lemma_fib_monotonic(i, (j - 1) as nat); + } else { + lemma_fib_monotonic(i, (j - 1) as nat); + lemma_fib_monotonic(i, (j - 2) as nat); + } +} + fn fib(n: u32) -> (ret: Option) ensures - ret.is_some() ==> ret.unwrap() == spec_fib(n as nat), + match ret { + None => spec_fib(n as nat) > u32::MAX, + Some(f) => f == spec_fib(n as nat), + }, { + if n > 47 { + proof { + assert(spec_fib(48) > u32::MAX) by (compute_only); + lemma_fib_monotonic(48, n as nat); + } + return None; + } match n { 0 => Some(0), 1 => Some(1), _ => { + proof { + // Prove that the recursive calls below succeed, + // and that n1 + n2 won't overflow + assert(spec_fib(47) < u32::MAX) by (compute_only); + lemma_fib_monotonic(n as nat, 47); + lemma_fib_monotonic((n - 1) as nat, 47); + lemma_fib_monotonic((n - 2) as nat, 47); + } let n1 = fib(n - 1)?; let n2 = fib(n - 2)?; - n1.checked_add(n2) + Some(n1 + n2) }, } } diff --git a/tasks/human_eval_055b.rs b/tasks/human_eval_055b.rs index fddf289..5d4aaf9 100644 --- a/tasks/human_eval_055b.rs +++ b/tasks/human_eval_055b.rs @@ -10,6 +10,7 @@ use vstd::prelude::*; verus! { // O(n) non-recursive solution using same spec as 55a +#[verifier::memoize] spec fn spec_fib(n: nat) -> nat decreases n, { @@ -22,9 +23,29 @@ spec fn spec_fib(n: nat) -> nat } } +proof fn lemma_fib_monotonic(i: nat, j: nat) + requires + i <= j, + ensures + spec_fib(i) <= spec_fib(j), + decreases j - i, +{ + if (i < 2 && j < 2) || i == j { + } else if i == j - 1 { + reveal_with_fuel(spec_fib, 2); + lemma_fib_monotonic(i, (j - 1) as nat); + } else { + lemma_fib_monotonic(i, (j - 1) as nat); + lemma_fib_monotonic(i, (j - 2) as nat); + } +} + fn fib(n: u32) -> (ret: Option) ensures - ret.is_some() ==> ret.unwrap() == spec_fib(n as nat), + match ret { + None => spec_fib(n as nat) > u32::MAX, + Some(f) => f == spec_fib(n as nat), + }, { if n == 0 { return Some(0); @@ -32,17 +53,31 @@ fn fib(n: u32) -> (ret: Option) if n == 1 { return Some(1); } + if n > 47 { + proof { + assert(spec_fib(48) > u32::MAX) by (compute_only); + lemma_fib_monotonic(48, n as nat); + } + return None; + } let mut a: u32 = 0; let mut b: u32 = 1; let mut i: u32 = 2; for i in 1..n invariant - 1 <= i as int <= n, + 1 <= i as int <= n <= 47, a as int == spec_fib((i - 1) as nat), b as int == spec_fib(i as nat), { - let sum = a.checked_add(b)?; + proof { + // Prove that that n1 + n2 won't overflow + assert(spec_fib(47) < u32::MAX) by (compute_only); + lemma_fib_monotonic(i as nat, 47); + lemma_fib_monotonic((i - 1) as nat, 47); + lemma_fib_monotonic((i + 1) as nat, 47); + } + let sum = a + b; a = b; b = sum; } diff --git a/tasks/human_eval_059.rs b/tasks/human_eval_059.rs index 4244b35..21eaf92 100644 --- a/tasks/human_eval_059.rs +++ b/tasks/human_eval_059.rs @@ -45,6 +45,8 @@ fn largest_prime_factor(n: u32) -> (largest: u32) ensures 1 <= largest <= n, spec_prime(largest as int), + n % largest == 0, + forall|p| 0 <= p < n && spec_prime(p) && n as int % p == 0 ==> p <= largest, { let mut largest = 1; let mut j = 1; @@ -52,6 +54,8 @@ fn largest_prime_factor(n: u32) -> (largest: u32) invariant 1 <= largest <= j <= n, spec_prime(largest as int), + n % largest == 0, + forall|p| 0 <= p <= j && spec_prime(p) && n as int % p == 0 ==> p <= largest, { j += 1; let flag = is_prime(j); diff --git a/tasks/human_eval_060.rs b/tasks/human_eval_060.rs index 33e656a..92ea98a 100644 --- a/tasks/human_eval_060.rs +++ b/tasks/human_eval_060.rs @@ -19,21 +19,52 @@ spec fn spec_sum_to_n(n: nat) -> nat } } +proof fn lemma_sum_monotonic(i: nat, j: nat) + requires + i <= j, + ensures + spec_sum_to_n(i) <= spec_sum_to_n(j), + decreases j - i, +{ + if (i == 0 && j == 0) || i == j { + } else if i == j - 1 { + lemma_sum_monotonic(i, (j - 1) as nat); + } else { + lemma_sum_monotonic(i, (j - 1) as nat); + } +} + fn sum_to_n(n: u32) -> (sum: Option) ensures - sum.is_some() ==> sum.unwrap() == spec_sum_to_n(n as nat), + match sum { + None => spec_sum_to_n(n as nat) > u32::MAX, + Some(f) => f == spec_sum_to_n(n as nat), + }, { + if n >= 92682 { + proof { + assert(spec_sum_to_n(92682) > u32::MAX) by (compute_only); + lemma_sum_monotonic(92682, n as nat); + } + return None; + } let mut res: u32 = 0; let mut sum: u32 = 0; let mut i: u32 = 0; while i < n invariant - i <= n, + i <= n < 92682, res == spec_sum_to_n(i as nat), res <= u32::MAX, { i += 1; - res = i.checked_add(res)?; + proof { + // Prove that that n1 + n2 won't overflow + assert(spec_sum_to_n(92681) < u32::MAX) by (compute_only); + lemma_sum_monotonic(i as nat, 92681); + lemma_sum_monotonic((i - 1) as nat, 92681); + } + res = i + res; } Some(res) } diff --git a/tasks/human_eval_062.rs b/tasks/human_eval_062.rs index c75afba..a5c3706 100644 --- a/tasks/human_eval_062.rs +++ b/tasks/human_eval_062.rs @@ -9,22 +9,38 @@ use vstd::prelude::*; verus! { -fn derivative(xs: &Vec) -> (ret: Option>) +fn derivative(xs: &Vec) -> (ret: Vec) + requires + xs.len() <= u32::MAX, ensures - ret.is_some() ==> xs@.len() == 0 || xs@.map(|i: int, x| i * x).skip(1) - =~= ret.unwrap()@.map_values(|x| x as int), + if xs.len() == 0 { + ret.len() == 0 + } else { + ret@.map_values(|x| x as int) =~= xs@.map(|i: int, x| i * x).skip(1) + }, { let mut ret = Vec::new(); if xs.len() == 0 { - return Some(ret); + return 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(), + 1 <= i <= xs.len() <= u32::MAX, { - ret.push(xs[i].checked_mul(i)?); + proof { + // Prove that the multiplication does not overflow + vstd::arithmetic::mul::lemma_mul_upper_bound( + xs[i as int] as int, + u32::MAX as int, + i as int, + u32::MAX as int, + ); + assert(u32::MAX * u32::MAX <= u64::MAX); + assert((i as u64) * (xs[i as int] as u64) == i as int * xs[i as int]); + } + ret.push((i as u64) * (xs[i] as u64)); 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( @@ -35,7 +51,7 @@ fn derivative(xs: &Vec) -> (ret: Option>) 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) + ret } } // verus! diff --git a/tasks/human_eval_063.rs b/tasks/human_eval_063.rs index f44704b..e94d131 100644 --- a/tasks/human_eval_063.rs +++ b/tasks/human_eval_063.rs @@ -9,6 +9,7 @@ use vstd::prelude::*; verus! { +#[verifier::memoize] spec fn spec_fibfib(n: nat) -> nat decreases n, { @@ -23,15 +24,58 @@ spec fn spec_fibfib(n: nat) -> nat } } +proof fn lemma_fibfib_monotonic(i: nat, j: nat) + requires + i <= j, + ensures + spec_fibfib(i) <= spec_fibfib(j), + decreases j - i, +{ + if (i < 3 && j < 3) || i == j { + } else if i == j - 1 { + reveal_with_fuel(spec_fibfib, 3); + lemma_fibfib_monotonic(i, (j - 1) as nat); + } else if i == j - 2 { + reveal_with_fuel(spec_fibfib, 3); + lemma_fibfib_monotonic(i, (j - 1) as nat); + lemma_fibfib_monotonic(i, (j - 2) as nat); + } else { + lemma_fibfib_monotonic(i, (j - 1) as nat); + lemma_fibfib_monotonic(i, (j - 2) as nat); + lemma_fibfib_monotonic(i, (j - 3) as nat); + } +} + fn fibfib(x: u32) -> (ret: Option) ensures - ret.is_some() ==> spec_fibfib(x as nat) == ret.unwrap(), + match ret { + None => spec_fibfib(x as nat) > u32::MAX, + Some(f) => f == spec_fibfib(x as nat), + }, { + if x > 39 { + proof { + assert(spec_fibfib(40) > u32::MAX) by (compute_only); + lemma_fibfib_monotonic(40, x as nat); + } + return None; + } match (x) { 0 => Some(0), 1 => Some(0), 2 => Some(1), - _ => fibfib(x - 1)?.checked_add(fibfib(x - 2)?)?.checked_add(fibfib(x - 3)?), + _ => { + proof { + // Prove that the recursive calls below succeed, + // and that the additions won't overflow + assert(spec_fibfib(39) < u32::MAX) by (compute_only); + lemma_fibfib_monotonic(x as nat, 39); + lemma_fibfib_monotonic((x - 1) as nat, 39); + lemma_fibfib_monotonic((x - 2) as nat, 39); + lemma_fibfib_monotonic((x - 3) as nat, 39); + } + Some(fibfib(x - 1)? + fibfib(x - 2)? + fibfib(x - 3)?) + }, } } From daabbc0740b9d4bb41da87b8a4dd121be19b7bee Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Sat, 28 Sep 2024 15:59:35 -0400 Subject: [PATCH 08/22] Minor edits to 51 --- tasks/human_eval_051.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_051.rs b/tasks/human_eval_051.rs index 4e31c40..edbaf26 100644 --- a/tasks/human_eval_051.rs +++ b/tasks/human_eval_051.rs @@ -9,13 +9,13 @@ use vstd::prelude::*; verus! { -// This spec function checks whether a character is vowel +// This spec function checks whether a character is a vowel pub open spec fn is_vowel_spec(c: char) -> bool { c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c == 'I' || c == 'O' || c == 'U' } -// This auxilary exe function checks whether a character is vowel +// This auxilary exec function checks whether a character is a vowel fn is_vowel(c: char) -> (is_vowel: bool) ensures is_vowel == is_vowel_spec(c), From 9be5e82393196f4ee4a4ceef22b07e9a7660eef9 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Sat, 28 Sep 2024 16:17:34 -0400 Subject: [PATCH 09/22] Optimize 60's proof through an arimethic lemma, rather than assert-by-compute --- tasks/human_eval_060.rs | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_060.rs b/tasks/human_eval_060.rs index 92ea98a..a4ba17f 100644 --- a/tasks/human_eval_060.rs +++ b/tasks/human_eval_060.rs @@ -34,6 +34,20 @@ proof fn lemma_sum_monotonic(i: nat, j: nat) } } +proof fn lemma_sum_to_n_closed_form(n: nat) + ensures + spec_sum_to_n(n) == (n * (n + 1)) / 2, + decreases n, +{ + if n == 0 { + } else { + assert(spec_sum_to_n((n - 1) as nat) == ((n - 1) * n) / 2) by { + lemma_sum_to_n_closed_form((n - 1) as nat); + } + assert(n + (((n - 1) * n) / 2) == (n * (n + 1)) / 2) by (nonlinear_arith); + } +} + fn sum_to_n(n: u32) -> (sum: Option) ensures match sum { @@ -43,7 +57,7 @@ fn sum_to_n(n: u32) -> (sum: Option) { if n >= 92682 { proof { - assert(spec_sum_to_n(92682) > u32::MAX) by (compute_only); + lemma_sum_to_n_closed_form(92682); lemma_sum_monotonic(92682, n as nat); } return None; @@ -60,7 +74,7 @@ fn sum_to_n(n: u32) -> (sum: Option) i += 1; proof { // Prove that that n1 + n2 won't overflow - assert(spec_sum_to_n(92681) < u32::MAX) by (compute_only); + lemma_sum_to_n_closed_form(92681); lemma_sum_monotonic(i as nat, 92681); lemma_sum_monotonic((i - 1) as nat, 92681); } From 24726b00c443015ac68ee999498b49dba64422c8 Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Mon, 30 Sep 2024 21:20:46 -0400 Subject: [PATCH 10/22] Finished task025 (#16) --------- Co-authored-by: Amar Shah --- tasks/human_eval_025.rs | 368 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 366 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_025.rs b/tasks/human_eval_025.rs index a6c97cf..4891c0c 100644 --- a/tasks/human_eval_025.rs +++ b/tasks/human_eval_025.rs @@ -5,14 +5,378 @@ HumanEval/25 /* ### VERUS BEGIN */ +use vstd::arithmetic::div_mod::*; +use vstd::arithmetic::mul::*; +use vstd::assert_by_contradiction; +use vstd::calc; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +pub closed spec fn is_prime(n: nat) -> bool { + forall|i: nat| 1 < i < n ==> #[trigger] (n % i) != 0 +} + +// canonical definition of prime factoriztion +pub closed spec fn is_prime_factorization(n: nat, factorization: Seq) -> bool { + // all factors are prime + &&& forall|i: int| + 0 <= i < factorization.len() ==> #[trigger] is_prime( + factorization[i] as nat, + ) + // product of factors is n + &&& factorization.fold_right(|x: nat, acc: nat| (acc * x as nat), 1nat) + == n + // factors are listed in ascending order + &&& forall|i: nat, j: nat| + (1 < i <= j < factorization.len()) ==> (#[trigger] factorization[i as int] + <= #[trigger] factorization[j as int]) +} + +// these two pull out lemmas are the same except for types +// would prefer to have one polymorphic function, but won't go through +// See https://github.com/verus-lang/verus/issues/1287 +proof fn lemma_fold_right_pull_out_nat(seq: Seq, k: nat) + ensures + seq.fold_right(|x, acc: nat| (acc * x) as nat, k) == (seq.fold_right( + |x, acc: nat| (acc * x) as nat, + 1, + ) * k) as nat, + decreases seq.len(), +{ + if seq.len() == 0 { + } else { + calc! { + (==) + seq.fold_right(|x, acc: nat| (acc * x) as nat, k); { + lemma_fold_right_pull_out_nat(seq.drop_last(), (k * seq.last()) as nat) + } + (seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * (k + * seq.last()) as nat) as nat; { + lemma_mul_is_commutative(k as int, seq.last() as int) + } + (seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * (seq.last() + * k) as nat) as nat; { + lemma_mul_is_associative( + seq.drop_last().fold_right(|x: nat, acc: nat| (acc * x) as nat, 1nat) as int, + seq.last() as int, + k as int, + ); + } // {lemma_mul_is_associative(seq.drop_last().fold_right(|x, acc : nat| (acc * x) as nat, 1) as int, seq.last() as int, k as int)} + (((seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * seq.last()) as nat) + * k) as nat; { lemma_fold_right_pull_out_nat(seq.drop_last(), seq.last() as nat) } + (seq.fold_right(|x, acc: nat| (acc * x) as nat, 1) * k) as nat; + } + } +} + +proof fn lemma_fold_right_pull_out_hybrid(seq: Seq, k: nat) + ensures + seq.fold_right(|x, acc: nat| (acc * x) as nat, k) == (seq.fold_right( + |x, acc: nat| (acc * x) as nat, + 1, + ) * k) as nat, + decreases seq.len(), +{ + if seq.len() == 0 { + } else { + calc! { + (==) + seq.fold_right(|x, acc: nat| (acc * x) as nat, k); { + lemma_fold_right_pull_out_hybrid(seq.drop_last(), (k * seq.last()) as nat) + } + (seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * (k + * seq.last()) as nat) as nat; { + lemma_mul_is_commutative(k as int, seq.last() as int) + } + (seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * (seq.last() + * k) as nat) as nat; { + lemma_mul_is_associative( + seq.drop_last().fold_right(|x: u8, acc: nat| (acc * x) as nat, 1nat) as int, + seq.last() as int, + k as int, + ); + } + (((seq.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1) * seq.last()) as nat) + * k) as nat; { lemma_fold_right_pull_out_hybrid(seq.drop_last(), seq.last() as nat) + } + (seq.fold_right(|x, acc: nat| (acc * x) as nat, 1) * k) as nat; + } + } +} + +proof fn lemma_unfold_right_fold(factors: Seq, old_factors: Seq, k: u8, m: u8) + requires + old_factors.push(m) == factors, + k % m == 0, + m != 0, + ensures + factors.fold_right(|x, acc: nat| (acc * x) as nat, ((k / m) as nat)) + == old_factors.fold_right(|x, acc: nat| (acc * x) as nat, ((k as nat))), +{ + assert((old_factors.push(m)).drop_last() == old_factors); + assert(((k as int) / (m as int)) * (m as int) + (k as int) % (m as int) == (k as int)) by { + lemma_fundamental_div_mod(k as int, m as int) + }; +} + +proof fn lemma_unfold_right_fold_new(factors: Seq, old_factors: Seq, m: u8) + requires + old_factors.push(m as u8) == factors, + m != 0, + ensures + factors.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == old_factors.fold_right( + |x, acc: nat| (acc * x) as nat, + 1nat, + ) * (m as nat), +{ + assert((old_factors.push(m as u8)).drop_last() == old_factors); + assert(factors.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == old_factors.fold_right( + |x, acc: nat| (acc * x) as nat, + 1, + ) * (m as nat)) by { lemma_fold_right_pull_out_hybrid(old_factors, m as nat) } +} + +proof fn lemma_multiple_mod_is_zero(m: int, n: int, k: int) + requires + n % k == 0, + k % m == 0, + k > 0, + m > 0, + ensures + n % (k / m) == 0, +{ + assert(k == (k / m) * m) by { lemma_fundamental_div_mod(k, m) }; + assert(n == (n / k) * k) by { lemma_fundamental_div_mod(n, k) }; + + assert(n == ((n / k) * m) * (k / m)) by { + broadcast use group_mul_properties; + + }; + assert(n % (k / m) == 0) by { lemma_mod_multiples_basic((n / k) * m, k / m) }; +} + +proof fn lemma_multiple_mod_is_zero_new(m: int, n: int, k: int) + requires + n % k == 0, + k % m == 0, + k > 0, + m > 0, + n > 0, + ensures + m * (n / k) == n / (k / m), +{ + assert(k == (k / m) * m) by { lemma_fundamental_div_mod(k, m) }; + let a = choose|a: int| (#[trigger] (a * m) == k && (a == k / m)); + + assert(n == (n / k) * k) by { lemma_fundamental_div_mod(n, k) }; + let b = choose|b: int| (#[trigger] (b * k) == n && b == n / k); + + assert((a * m) * b == n) by { lemma_mul_is_commutative(b, a * m) } + assert(a * (m * b) == n) by { lemma_mul_is_associative(a, m, b) }; + assert((m * b) == n / a) by { lemma_div_multiples_vanish(m * b, a) }; +} + +proof fn lemma_factor_mod_is_zero(k: int, m: int, j: int) + requires + k % j != 0, + k % m == 0, + 1 <= j < m, + ensures + (k / m) % j != 0, +{ + assert_by_contradiction!((k/m) % j != 0, + { /* proof */ + assert (k == (k/m) * m) by {lemma_fundamental_div_mod(k, m)}; + let a = choose|a:int| (#[trigger] (a * m) == k); + + assert ((k/m) == ((k/m)/j) * j) by {lemma_fundamental_div_mod(k/m, j)}; + let b = choose|b:int| (#[trigger] (b * j) == k/m); + + calc! { + (==) + k % j; {broadcast use group_mul_properties;} + ((b * m) * j) % j; {broadcast use lemma_mod_multiples_basic;} + 0; + } + }); + +} + +proof fn lemma_mod_zero_twice(k: int, m: int, i: int) + requires + k % m == 0, + m % i == 0, + m > 0, + i > 0, + ensures + k % i == 0, +{ + assert(k == (k / m) * m) by { lemma_fundamental_div_mod(k as int, m as int) }; + let a = choose|a: int| (#[trigger] (a * m) == k); + + assert(m == (m / i) * i) by { lemma_fundamental_div_mod(m as int, i as int) }; + let b = choose|b: int| (#[trigger] (b * i) == m); + + assert(k == (a * b) * i) by { lemma_mul_is_associative(a, b, i) }; + assert(k % i == 0) by { lemma_mod_multiples_vanish(a * b, 0, i) }; + +} + +proof fn lemma_first_divisor_is_prime(k: nat, m: nat) + requires + k % m == 0, + forall|j: nat| 1 < j < m ==> #[trigger] (k % j) != 0, + m >= 2, + ensures + is_prime(m), +{ + assert_by_contradiction!(is_prime(m), + { + let i = choose|i:nat| (1 < i < m && #[trigger] (m % i) == 0); + assert (k % i == 0) by {lemma_mod_zero_twice(k as int, m as int, i as int)}; + }) +} + +proof fn lemma_drop_last_map_commute(seq: Seq) + requires + seq.len() >= 1, + ensures + seq.map(|_idx, j: u8| j as nat).drop_last() == seq.drop_last().map(|_idx, j: u8| j as nat), +{ + assert(seq.map(|_idx, j: u8| j as nat).drop_last() == seq.drop_last().map( + |_idx, j: u8| j as nat, + )); +} + +proof fn lemma_fold_right_equivalent_for_nat_u8(factorization: Seq) + requires + factorization.fold_right(|x, acc: u8| (acc * x) as u8, 1u8) <= 255 as u8, + forall|i: int| 0 <= i < factorization.len() ==> factorization[i] > 0, + ensures + factorization.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == factorization.map( + |_idx, j: u8| j as nat, + ).fold_right(|x: nat, acc: nat| (acc * x as nat), 1nat), + decreases factorization.len(), +{ + if (factorization.len() == 0) { + } else { + let factorization_ = factorization.drop_last(); + let last = factorization.last(); + + calc! { + (==) + factorization.map(|_idx, j: u8| j as nat).fold_right(|x, acc: nat| acc * x, 1nat); { + lemma_drop_last_map_commute(factorization) + } + factorization.drop_last().map(|_idx, j: u8| j as nat).fold_right( + |x, acc: nat| acc * x, + (factorization.last() as nat), + ); { + lemma_fold_right_pull_out_nat( + factorization.drop_last().map(|_idx, j: u8| j as nat), + (factorization.last() as nat), + ) + } + factorization.drop_last().map(|_idx, j: u8| j as nat).fold_right( + |x, acc: nat| acc * x, + 1nat, + ) * (factorization.last() as nat); { + lemma_fold_right_equivalent_for_nat_u8(factorization.drop_last()) + } + factorization.drop_last().fold_right(|x, acc: nat| (acc * x) as nat, 1nat) * ( + factorization.last() as nat); { + lemma_fold_right_pull_out_hybrid( + factorization.drop_last(), + (factorization.last() as nat), + ) + } + factorization.drop_last().fold_right( + |x, acc: nat| (acc * x) as nat, + (factorization.last() as nat), + ); + } + } +} + +pub fn factorize(n: u8) -> (factorization: Vec) + requires + 1 <= n <= 255, + ensures + is_prime_factorization(n as nat, factorization@.map(|_idx, j: u8| j as nat)), +{ + let mut factorization = vec![]; + let mut k = n; + let mut m = 2u16; + let ghost n_nat = n as nat; + while (m <= n as u16) + invariant + 1 < m < n + 2, + n <= 255, + 0 < k <= n, + forall|j: u8| 1 < j < m ==> #[trigger] (k % j) != 0, + factorization@.fold_right(|x: u8, acc: nat| (acc * x) as nat, 1nat) == n as nat / ( + k as nat), + forall|i: nat| + 0 <= i < factorization.len() ==> #[trigger] is_prime( + factorization[i as int] as nat, + ), + forall|i: int| 0 <= i < factorization.len() ==> factorization[i] > 0, + n % k == 0, + forall|i: nat, j: nat| + (1 < i <= j < factorization.len()) ==> ((#[trigger] factorization[i as int] as nat) + <= (#[trigger] factorization[j as int] as nat) <= m), + { + if (k as u16 % m == 0) { + assert(is_prime(m as nat)) by { lemma_first_divisor_is_prime(k as nat, m as nat) }; + let ghost old_factors = factorization; + let l = factorization.len(); + factorization.insert(l, m as u8); + + assert(old_factors@.push(m as u8) == factorization@); + + assert(factorization@.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == ((m as nat) + * (n as nat / (k as nat))) as nat) by { + lemma_unfold_right_fold_new(factorization@, old_factors@, m as u8) + }; + + assert(n % (k / m as u8) == 0) by { + lemma_multiple_mod_is_zero(m as int, n as int, k as int); + }; + + assert(factorization@.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == ((n as nat / ( + (k / m as u8) as nat))) as nat) by { + lemma_multiple_mod_is_zero_new(m as int, n as int, k as int) + }; + + assert forall|j: u8| (1 < j < m && (k % j != 0)) implies #[trigger] ((k / m as u8) % j) + != 0 by { lemma_factor_mod_is_zero(k as int, m as int, j as int) }; + assert((k as int) == ((k as int) / (m as int)) * (m as int)) by { + lemma_fundamental_div_mod(k as int, m as int) + }; + + k = k / m as u8; + } else { + m = m + 1; + } + } + proof { + assert_by_contradiction!(k == 1, { + assert (k % k == 0); + }); + } + + assert(factorization@.map(|_idx, j: u8| j as nat).fold_right( + |x: nat, acc: nat| (acc * x as nat), + 1nat, + ) == n) by { lemma_fold_right_equivalent_for_nat_u8(factorization@) }; + return factorization; +} } // verus! -fn main() {} +fn main() { + print!("{:?}", factorize(254)); +} /* ### VERUS END From ea898a43fd580e865ed9e7b6b501bc674fce6ecc Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Thu, 3 Oct 2024 10:08:54 -0400 Subject: [PATCH 11/22] Finished task 139 (#22) --- tasks/human_eval_025.rs | 6 +- tasks/human_eval_139.rs | 131 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 132 insertions(+), 5 deletions(-) diff --git a/tasks/human_eval_025.rs b/tasks/human_eval_025.rs index 4891c0c..cbaab9c 100644 --- a/tasks/human_eval_025.rs +++ b/tasks/human_eval_025.rs @@ -251,7 +251,7 @@ proof fn lemma_drop_last_map_commute(seq: Seq) proof fn lemma_fold_right_equivalent_for_nat_u8(factorization: Seq) requires - factorization.fold_right(|x, acc: u8| (acc * x) as u8, 1u8) <= 255 as u8, + factorization.fold_right(|x, acc: u8| (acc * x) as u8, 1u8) <= u8::MAX as u8, forall|i: int| 0 <= i < factorization.len() ==> factorization[i] > 0, ensures factorization.fold_right(|x, acc: nat| (acc * x) as nat, 1nat) == factorization.map( @@ -301,7 +301,7 @@ proof fn lemma_fold_right_equivalent_for_nat_u8(factorization: Seq) pub fn factorize(n: u8) -> (factorization: Vec) requires - 1 <= n <= 255, + 1 <= n <= u8::MAX, ensures is_prime_factorization(n as nat, factorization@.map(|_idx, j: u8| j as nat)), { @@ -312,7 +312,7 @@ pub fn factorize(n: u8) -> (factorization: Vec) while (m <= n as u16) invariant 1 < m < n + 2, - n <= 255, + n <= u8::MAX, 0 < k <= n, forall|j: u8| 1 < j < m ==> #[trigger] (k % j) != 0, factorization@.fold_right(|x: u8, acc: nat| (acc * x) as nat, 1nat) == n as nat / ( diff --git a/tasks/human_eval_139.rs b/tasks/human_eval_139.rs index 793ba21..7c956c0 100644 --- a/tasks/human_eval_139.rs +++ b/tasks/human_eval_139.rs @@ -5,14 +5,141 @@ HumanEval/139 /* ### VERUS BEGIN */ +use vstd::arithmetic::mul::*; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// specification +pub closed spec fn factorial(n: nat) -> nat + decreases n, +{ + if n <= 1 { + 1 + } else { + n * factorial((n - 1) as nat) + } +} + +pub closed spec fn brazilian_factorial(n: nat) -> nat + decreases n, +{ + if n <= 1 { + factorial(1) + } else { + factorial(n) * brazilian_factorial((n - 1) as nat) + } +} + +proof fn lemma_factorial_positive(n: nat) + ensures + factorial(n) >= 1, + decreases n, +{ + if (n == 0) { + } else { + lemma_factorial_positive((n - 1) as nat); + assert(factorial(n) >= 1) by { + broadcast use lemma_mul_strictly_positive; + + }; + } +} + +proof fn lemma_brazilian_factorial_positive(n: nat) + ensures + brazilian_factorial(n) >= 1, + decreases n, +{ + if (n == 0) { + } else { + lemma_factorial_positive((n) as nat); + lemma_brazilian_factorial_positive((n - 1) as nat); + assert(brazilian_factorial(n) >= 1) by { + lemma_mul_strictly_positive( + factorial(n) as int, + brazilian_factorial((n - 1) as nat) as int, + ) + }; + } +} + +proof fn lemma_brazilian_fib_monotonic(i: nat, j: nat) + requires + 0 <= i <= j, + ensures + brazilian_factorial(i) <= brazilian_factorial(j), + decreases j - i, +{ + if (i == j) { + } else if (j == i + 1) { + assert(factorial(j) >= 1) by { lemma_factorial_positive(j) }; + assert(brazilian_factorial(j) >= brazilian_factorial(i)) by { + broadcast use lemma_mul_increases; + + }; + } else { + lemma_brazilian_fib_monotonic(i, (j - 1) as nat); + lemma_brazilian_fib_monotonic((j - 1) as nat, j); + } +} + +pub fn brazilian_factorial_impl(n: u64) -> (ret: Option) + ensures + match ret { + None => brazilian_factorial(n as nat) > u64::MAX, + Some(bf) => bf == brazilian_factorial(n as nat), + }, +{ + if n >= 9 { + assert(brazilian_factorial(9nat) > u64::MAX) by (compute_only); + assert(brazilian_factorial(n as nat) >= brazilian_factorial(9nat)) by { + lemma_brazilian_fib_monotonic(9nat, n as nat) + }; + return None; + } + let mut start = 1u64; + let mut end = n + 1u64; + let mut fact_i = 1u64; + let mut special_fact = 1u64; + + while start < end + invariant + brazilian_factorial((start - 1) as nat) == special_fact, + factorial((start - 1) as nat) == fact_i, + 1 <= start <= end < 10, + decreases (end - start), + { + assert(brazilian_factorial(start as nat) <= brazilian_factorial(8nat)) by { + lemma_brazilian_fib_monotonic(start as nat, 8nat) + }; + assert(brazilian_factorial(8nat) < u64::MAX) by (compute_only); + + assert(brazilian_factorial((start - 1) as nat) >= 1) by { + lemma_brazilian_factorial_positive((start - 1) as nat) + }; + assert(factorial(start as nat) <= brazilian_factorial(start as nat)) by { + broadcast use lemma_mul_ordering; + + }; + + fact_i = start * fact_i; + + special_fact = fact_i * special_fact; + + start = start + 1; + } + return Some(special_fact); + +} } // verus! -fn main() {} +fn main() { + println!("{:?}", brazilian_factorial_impl(4)); + // > 288 + println!("{:?}", brazilian_factorial_impl(6)); + // > 24883200 +} /* ### VERUS END From 67b1597b10a21ad18900f74d1e74c6dff2eff76e Mon Sep 17 00:00:00 2001 From: elanortang <77796517+elanortang@users.noreply.github.com> Date: Thu, 3 Oct 2024 10:40:46 -0400 Subject: [PATCH 12/22] completed tasks 31 and 28 (#17) --------- Co-authored-by: Elanor Tang --- tasks/human_eval_028.rs | 68 +++++++++++++++++++++++++++++++++++++++-- tasks/human_eval_031.rs | 56 +++++++++++++++++++++++++++++++-- 2 files changed, 120 insertions(+), 4 deletions(-) diff --git a/tasks/human_eval_028.rs b/tasks/human_eval_028.rs index 1f3179d..5a3da83 100644 --- a/tasks/human_eval_028.rs +++ b/tasks/human_eval_028.rs @@ -9,10 +9,74 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +pub closed spec fn concat_helper(strings: Seq>, i: nat) -> Seq + recommends + i <= strings.len(), + decreases strings.len() - i, +{ + if (i >= strings.len()) { + seq![] + } else { + strings[i as int] + concat_helper(strings, i + 1) + } +} + +pub open spec fn concatenate(strings: Seq>) -> Seq { + concat_helper(strings, 0) +} + +proof fn sanity_check() { + assert(concatenate(seq![seq!['a'], seq!['b'], seq!['c']]) == seq!['a', 'b', 'c']) by (compute); + assert(concatenate(Seq::empty()) == Seq::::empty()); + assert(concatenate(seq![seq!['a', 'z'], seq!['b'], seq!['c', 'y']]) == seq![ + 'a', + 'z', + 'b', + 'c', + 'y', + ]) by (compute); +} + +fn concatenate_impl(strings: Vec>) -> (joined: Vec) + ensures + joined@ == concatenate(strings.deep_view()), +{ + let mut i = 0; + let mut joined = vec![]; + + while (i < strings.len()) + invariant + 0 <= i <= strings.len(), + concatenate(strings.deep_view()) == joined@ + concat_helper( + strings.deep_view(), + i as nat, + ), + { + assert(concatenate(strings.deep_view()) == joined@ + strings[i as int]@ + concat_helper( + strings.deep_view(), + (i + 1) as nat, + )); + + let mut copy_str = strings[i].clone(); + joined.append(&mut copy_str); + i = i + 1; + } + return joined; +} } // verus! -fn main() {} +fn main() { + let test1 = vec![vec!['a'], vec!['b'], vec!['c']]; + let test2: Vec> = Vec::new(); + let test3 = vec![vec!['a', 'z'], vec!['b'], vec!['c', 'y']]; + + print!("concatenation of {:?}:\n", test1); + print!("{:?}\n", concatenate_impl(test1)); + print!("concatenation of {:?}:\n", test2); + print!("{:?}\n", concatenate_impl(test2)); + print!("concatenation of {:?}:\n", test3); + print!("{:?}\n", concatenate_impl(test3)); +} /* ### VERUS END diff --git a/tasks/human_eval_031.rs b/tasks/human_eval_031.rs index 0570ee0..a9a4394 100644 --- a/tasks/human_eval_031.rs +++ b/tasks/human_eval_031.rs @@ -9,10 +9,62 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// specification +pub open spec fn is_prime(n: nat) -> bool { + (n > 1) && forall|i| 1 < i < n ==> #[trigger] (n % i) != 0 +} + +pub closed spec fn is_prime_so_far(n: nat, k: nat) -> bool + recommends + n >= k > 1, +{ + forall|i| 1 < i < k ==> #[trigger] (n % i) != 0 +} + +// Verus does not yet support quantifiers when using proof-by-compute +// proof fn sanity_check() { +// assert(is_prime(6) == false) by (compute); +// assert(is_prime(101) == true) by (compute); +// assert(is_prime(11) == true) by (compute); +// assert(is_prime(13441) == true) by (compute); +// assert(is_prime(61) == true) by (compute); +// assert(is_prime(4) == false) by (compute); +// assert(is_prime(1) == false) by (compute); +// } +// implementation +fn is_prime_impl(n: u8) -> (res: bool) + ensures + res == is_prime(n as nat), +{ + if n < 2 { + return false; + } + let mut k = 2; + let mut res = true; + + while (k < n) + invariant + 2 <= k <= n, + res == is_prime_so_far(n as nat, k as nat), + { + assert((is_prime_so_far(n as nat, k as nat) && (n as nat) % (k as nat) != 0) + == is_prime_so_far(n as nat, (k + 1) as nat)); + + res = res && n % k != 0; + k = k + 1; + } + return res; +} } // verus! -fn main() {} +fn main() { + print!("6 is prime? {}\n", is_prime_impl(6)); + print!("101 is prime? {}\n", is_prime_impl(101)); + print!("11 is prime? {}\n", is_prime_impl(11)); + print!("61 is prime? {}\n", is_prime_impl(61)); + print!("4 is prime? {}\n", is_prime_impl(4)); + print!("1 is prime? {}\n", is_prime_impl(1)); +} /* ### VERUS END From ddb9ba36557774251e728f5341c731390364bd91 Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Fri, 4 Oct 2024 09:11:40 -0400 Subject: [PATCH 13/22] Finished task018 (#23) --- tasks/human_eval_018.rs | 138 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 136 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_018.rs b/tasks/human_eval_018.rs index 21a8437..556dcb7 100644 --- a/tasks/human_eval_018.rs +++ b/tasks/human_eval_018.rs @@ -9,10 +9,144 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// spec +pub closed spec fn how_many_times(string: Seq, substring: Seq) -> nat + decreases string.len(), +{ + if (string.len() == 0) { + 0 + } else if substring.is_prefix_of(string) { + 1 + how_many_times(string.skip(1), substring) + } else { + how_many_times(string.skip(1), substring) + } +} + +// implementation +proof fn lemma_step_subrange(substring: Seq, string: Seq) + requires + substring.len() > 0, + string.len() >= substring.len(), + ensures + (substring[0] == string.subrange(0, substring.len() as int)[0] && (substring.skip(1) + =~= string.skip(1).subrange(0, substring.skip(1).len() as int))) ==> (substring + =~= string.subrange(0, substring.len() as int)), + decreases substring.len(), +{ + if (substring[0] == string.subrange(0, substring.len() as int)[0] && (substring.skip(1) + =~= string.skip(1).subrange(0, substring.skip(1).len() as int))) { + assert forall|i: int| 0 <= i < substring.len() implies #[trigger] substring[i] + == string.subrange(0, substring.len() as int)[i] by { + if i == 0 { + } else { + assert(forall|j: int| + (0 <= #[trigger] (j + 0) < substring.len() - 1) ==> substring.skip(1)[j] + == string.skip(1).subrange(0, substring.skip(1).len() as int)[j]); + assert(0 <= #[trigger] (i - 1 + 0) < substring.len() - 1); + } + } + } else { + } +} + +fn is_prefix(substring: Vec, string: Vec) -> (b: bool) + ensures + b == substring@.is_prefix_of(string@), +{ + let mut current_substring = substring.clone(); + let mut current_string = string.clone(); + + if substring.len() > string.len() { + return false + } + while (current_substring.len() > 0) + invariant + 0 <= current_substring.len() <= current_string.len(), + substring.len() <= string.len(), + (substring@ =~= string@.subrange(0, substring@.len() as int)) == (current_substring@ + =~= current_string@.subrange(0, current_substring@.len() as int)), + decreases current_substring.len(), + { + if (current_substring[0] != current_string[0]) { + return false; + } + let old_substring = current_substring.clone(); + let old_string = current_string.clone(); + + let substring_first = current_substring.remove(0); + let string_first = current_string.remove(0); + assert((old_substring@ =~= old_string@.subrange(0, old_substring@.len() as int)) <== ( + old_substring@[0] == old_string@.subrange(0, old_substring@.len() as int)[0] && ( + old_substring@.skip(1) =~= old_string@.skip(1).subrange( + 0, + old_substring@.skip(1).len() as int, + )))) by { lemma_step_subrange(old_substring@, old_string@) }; + } + return true; +} + +proof fn lemma_how_many_times_zero(string: Seq, substring: Seq) + requires + string.len() < substring.len(), + ensures + how_many_times(string, substring) == 0, + decreases string.len(), +{ + if string.len() == 0 { + } else { + lemma_how_many_times_zero(string.skip(1), substring) + } +} + +fn how_many_times_impl(string: Vec, substring: Vec) -> (opt_k: Option) + requires + substring.len() >= 1, + ensures + match opt_k { + Some(k) => k as nat == how_many_times(string@, substring@), + None => how_many_times(string@, substring@) > u32::MAX, + }, +{ + let mut k = 0u64; + let mut current_string = string; + while current_string.len() >= substring.len() + invariant + how_many_times(string@, substring@) == k + how_many_times(current_string@, substring@), + k <= u32::MAX as u64, + substring.len() >= 1, + decreases current_string.len(), + { + if (is_prefix(substring.clone(), current_string.clone())) { + if (k >= u32::MAX as u64) { + current_string = current_string.split_off(1); + assert(how_many_times(string@, substring@) == k + 1 + how_many_times( + current_string@, + substring@, + )); + return None; + } + k = k + 1; + } + current_string = current_string.split_off(1); + } + assert(how_many_times(current_string@, substring@) == 0) by { + lemma_how_many_times_zero(current_string@, substring@) + }; + return Some(k as u32); +} } // verus! -fn main() {} +fn main() { + println!("{:?}", how_many_times_impl(vec![], vec!['a'])); + // 0 + println!("{:?}", how_many_times_impl(vec!['a', 'a', 'a'], vec!['a'])); + // 3 + println!( + "{:?}", + how_many_times_impl(vec!['a', 'a', 'a', 'a'], vec!['a', 'a']) + ); + // 3 +} /* ### VERUS END From 9125a3699eba3eeb6ef9b8c204a3363fb25f4a05 Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Sat, 23 Nov 2024 19:31:52 -0500 Subject: [PATCH 14/22] Finished task129 (#24) * finished task 129 * ran verusfmt * made Bryan's requested changes * ran verusfmt * made changes Bryan requested --- tasks/human_eval_129.rs | 463 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 459 insertions(+), 4 deletions(-) diff --git a/tasks/human_eval_129.rs b/tasks/human_eval_129.rs index 3bc77ef..30e49b3 100644 --- a/tasks/human_eval_129.rs +++ b/tasks/human_eval_129.rs @@ -5,14 +5,469 @@ HumanEval/129 /* ### VERUS BEGIN */ +use vstd::arithmetic::mul::*; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// specification +pub open spec fn path_less_than(path1: Seq, path2: Seq) -> bool + recommends + path1.len() == path2.len(), +{ + (exists|i: int| + (0 <= i < path1.len() && path1[i] < path2[i] && (forall|j: int| + 0 <= j < i ==> path1[j] == path2[j]))) +} + +#[verusfmt::skip] +pub open spec fn is_adjacent( + grid: Seq>, + m: int, + n: int, + coords: (int, int), +) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + &&& (0 <= coords.0 <= N - 1) + &&& (0 <= coords.1 <= N - 1) + &&& grid[coords.0][coords.1] == m + &&& ( (coords.0 < N - 1 && grid[coords.0 + 1][coords.1] == n) + || (coords.0 > 0 && grid[coords.0 - 1][coords.1] == n) + || (coords.1 < N - 1 && grid[coords.0][coords.1 + 1] == n) + || (coords.1 > 0 && grid[coords.0][coords.1 - 1] == n)) +} + +pub open spec fn adjacent_numbers(grid: Seq>, m: int, n: int) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + exists|i: int, j: int| #[trigger] (is_adjacent::(grid, m, n, (i, j))) +} + +pub open spec fn exists_a_cell_with_value(grid: Seq>, n: int) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + (exists|i: int, j: int| (0 <= i < N && 0 <= j < N) && #[trigger] (grid[i][j]) == n) +} + +pub open spec fn no_repeats_in_grid(grid: Seq>) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + &&& (forall|i: int, j: int| (0 <= i < N && 0 <= j < N) ==> 1 <= #[trigger] grid[i][j] <= N * N) + &&& (forall|n: int| 1 <= n <= N * N ==> #[trigger] exists_a_cell_with_value::(grid, n)) + &&& (forall|i1: int, j1: int, i2: int, j2: int| + (0 <= i1 < N && 0 <= j1 < N && 0 <= i2 < N && 0 <= j2 < N) ==> (#[trigger] grid[i1][j1] + == #[trigger] grid[i2][j2]) ==> i1 == i2 && j1 == j2) +} + +pub open spec fn is_valid_path(grid: Seq>, path: Seq) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + &&& forall|i: int| + (0 <= i < path.len() - 1) ==> adjacent_numbers::(grid, #[trigger] path[i], path[(i + 1)]) + &&& forall|i: int| (0 <= i <= path.len() - 1) ==> 1 <= #[trigger] path[i] <= N * N +} + +pub open spec fn is_minpath(grid: Seq>, path: Seq) -> bool + recommends + grid.len() == N, + forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), +{ + &&& (is_valid_path::(grid, path)) + &&& (forall|alternate_path: Seq| + ((#[trigger] alternate_path.len() == path.len() && is_valid_path::(grid, alternate_path)) + ==> (#[trigger] path_less_than(path, alternate_path) || path == alternate_path))) +} + +// implementation +pub fn find_smallest_adjacent_to_one(grid: [[u8; N]; N]) -> (ret: ( + (usize, usize), + (usize, usize), + u8, +)) + requires + no_repeats_in_grid::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item: u8| item as int)), + ), + N >= 2, + 2 <= N <= u8::MAX, + N * N <= u8::MAX, + ensures + grid[ret.0.0 as int][ret.0.1 as int] == 1, + grid[ret.1.0 as int][ret.1.1 as int] == ret.2, + adjacent_numbers::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item: u8| item as int)), + ret.2 as int, + 1, + ), + 0 <= ret.0.0 < N, + 0 <= ret.0.1 < N, + 0 <= ret.1.0 < N, + 0 <= ret.1.1 < N, + (ret.0.0 < N - 1 && ret.0.0 + 1 == ret.1.0 && ret.0.1 == ret.1.1) || (ret.0.0 > 0 && ret.0.0 + - 1 == ret.1.0 && ret.0.1 == ret.1.1) || (ret.0.1 < N - 1 && ret.0.0 == ret.1.0 + && ret.0.1 + 1 == ret.1.1) || (ret.0.1 > 0 && ret.0.0 == ret.1.0 && ret.0.1 - 1 + == ret.1.1), + (ret.0.0 < N - 1 ==> grid[ret.0.0 + 1][ret.0.1 as int] >= ret.2) && (ret.0.0 > 0 + ==> grid[ret.0.0 - 1][ret.0.1 as int] >= ret.2) && (ret.0.1 < N - 1 + ==> grid[ret.0.0 as int][ret.0.1 + 1] >= ret.2) && (ret.0.1 > 0 + ==> grid[ret.0.0 as int][ret.0.1 - 1] >= ret.2), +{ + let mut ones_i = 0usize; + let mut ones_j = 0usize; + let mut i = 0usize; + + assert(N * N >= 1) by { lemma_mul_strictly_positive(N as int, N as int) }; + + assert(exists_a_cell_with_value::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + 1, + )); + + while i < N + invariant + (grid[ones_i as int][ones_j as int] == 1) || (exists|i0: int, j0: int| + (i <= i0 < N) && 0 <= j0 < N && grid[i0 as int][j0 as int] == 1), + (0 <= i <= N), + N == grid.len(), + (0 <= ones_i < N), + N == grid[ones_i as int].len(), + (0 <= ones_j < N), + decreases (N - i), + { + let mut j = 0usize; + while j < N + invariant + ((grid[ones_i as int][ones_j as int] == 1) || (exists|i0: int, j0: int| + ((i < i0 < N && 0 <= j0 < N) || (i0 == i && j <= j0 < N)) + && grid[i0 as int][j0 as int] == 1)), + 0 <= j <= N, + 0 <= i < N, + (0 <= ones_i < N), + (0 <= ones_j < N), + decreases N - j, + { + if grid[i][j] == 1 { + ones_i = i; + ones_j = j; + } + j = j + 1; + } + i = i + 1; + } + let mut smallest = (N * N) as u8; + let mut smallest_i = 0usize; + let mut smallest_j = 0usize; + + assert(1 <= smallest); + + assert((forall|i: int, j: int| + (0 <= i < N && 0 <= j < N) ==> 1 <= grid@.map_values( + |row: [u8; N]| row@.map_values(|item: u8| item as int), + )[#[trigger] (i + 0)][#[trigger] (j + 0)] <= N * N)); + assert((forall|i: int, j: int| + (0 <= i < N && 0 <= j < N) ==> 1 <= #[trigger] grid[i + 0][j + 0] <= N * N)); + + assert(ones_j > 0 ==> grid[(ones_i + 0) as int][(ones_j - 1) + 0] <= N * N); + + assert(ones_j > 0 ==> grid[(ones_i + 0) as int][(ones_j - 1) + 0] <= smallest); + assert(ones_j < N - 1 ==> grid[(ones_i + 0) as int][(ones_j + 1) + 0] <= smallest); + assert(ones_i > 0 ==> grid[(ones_i - 1) + 0][ones_j + 0] <= smallest); + assert(ones_i < N - 1 ==> grid[(ones_i + 1) + 0][ones_j + 0] <= smallest); + + assert((ones_j > 0 && grid[ones_i as int][ones_j - 1] <= smallest) || (ones_j < N - 1 + && grid[ones_i as int][ones_j + 1] <= smallest) || (ones_i > 0 && grid[ones_i + - 1][ones_j as int] <= smallest) || (ones_i < N - 1 && grid[ones_i + 1][ones_j as int] + <= smallest)); + + if (ones_j > 0 && grid[ones_i][ones_j - 1] <= smallest) { + smallest = grid[ones_i][ones_j - 1]; + smallest_i = ones_i; + smallest_j = ones_j - 1; + } + if (ones_j < N - 1 && grid[ones_i][ones_j + 1] <= smallest) { + smallest = grid[ones_i][ones_j + 1]; + smallest_i = ones_i; + smallest_j = ones_j + 1; + } + if (ones_i > 0 && grid[ones_i - 1][ones_j] <= smallest) { + smallest = grid[ones_i - 1][ones_j]; + smallest_i = ones_i - 1; + smallest_j = ones_j; + } + if (ones_i < N - 1 && grid[ones_i + 1][ones_j] <= smallest) { + smallest = grid[ones_i + 1][ones_j]; + smallest_i = ones_i + 1; + smallest_j = ones_j; + } + assert(ones_j > 0 ==> grid@.map_values( + |row: [u8; N]| row@.map_values(|item| item as int), + )[ones_i as int][ones_j - 1] >= smallest); + + assert(0 <= (smallest_i + 0) as int <= N - 1); + assert(0 <= (smallest_j + 0) as int <= N - 1); + assert(grid[(smallest_i + 0) as int][(smallest_j + 0) as int] == smallest); + assert((((smallest_i + 0) < (N - 1)) && grid[(smallest_i + 0) as int + 1][(smallest_j + + 0) as int] == 1) || ((smallest_i + 0) > 0 && grid[(smallest_i + 0) as int][(smallest_j + + 0) as int] == smallest && grid[(smallest_i + 0) as int - 1][(smallest_j + 0) as int] == 1) + || ((smallest_j + 0) < N - 1 && grid[(smallest_i + 0) as int][(smallest_j + 0) as int] + == smallest && grid[(smallest_i + 0) as int][(smallest_j + 0) as int + 1] == 1) || (( + smallest_j + 0) as int > 0 && grid[(smallest_i + 0) as int][(smallest_j + 0) as int] == smallest + && grid[(smallest_i + 0) as int][(smallest_j + 0) as int - 1] == 1)); + + assert(is_adjacent::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + smallest as int, + 1, + (smallest_i + 0 as int, smallest_j + 0 as int), + )); + assert(exists|i: int, j: int| + (is_adjacent::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + smallest as int, + 1, + (#[trigger] (i + 0), #[trigger] (j + 0)), + ))); + + return ((ones_i, ones_j), (smallest_i, smallest_j), smallest) +} + +// basically want a lemma that says if \forall alt_path (path < alt_path) +// then if alt_path' < path + [x] +// we get that alt_path'[:path.len()] == path adn alt_path[path.len()] < x +proof fn lemma_less_than_step_even( + path: Seq, + grid: [[u8; N]; N], + extra_item: int, +) + requires + no_repeats_in_grid::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + ), + forall|alternate_path: Seq| + ((alternate_path.len() == path.len() && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path, + )) ==> (#[trigger] path_less_than(path, alternate_path) || path == alternate_path)), + extra_item == 1, + ensures + forall|alternate_path_: Seq| + ((#[trigger] alternate_path_.len() == path.len() + 1 && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path_, + )) ==> (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ + extra_item, + ] == alternate_path_)), +{ + assert forall|alternate_path_: Seq| + ((#[trigger] alternate_path_.len()) == path.len() + 1 && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path_, + )) implies (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ + extra_item, + ] == alternate_path_) by { + if path_less_than(path, alternate_path_.subrange(0, path.len() as int)) { + } else { + if (alternate_path_[path.len() as int] > extra_item) { + } else { + assert(path + seq![extra_item] =~= alternate_path_); + } + } + } +} + +proof fn lemma_less_than_step_odd( + path: Seq, + grid: [[u8; N]; N], + extra_item: int, + ones_i: int, + ones_j: int, +) + requires + no_repeats_in_grid::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + ), + forall|alternate_path: Seq| + ((alternate_path.len() == path.len() && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path, + )) ==> (#[trigger] path_less_than(path, alternate_path) || path == alternate_path)), + path.len() >= 1, + path[path.len() - 1] == 1, + 0 <= ones_i <= N - 1, + 0 <= ones_j <= N - 1, + grid[ones_i][ones_j] == 1, + ones_i < N - 1 ==> grid[ones_i + 1][ones_j] >= extra_item, + ones_i > 0 ==> grid[ones_i - 1][ones_j] >= extra_item, + ones_j < N - 1 ==> grid[ones_i][ones_j + 1] >= extra_item, + ones_j > 0 ==> grid[ones_i][ones_j - 1] >= extra_item, + ones_i < N - 1 || ones_i > 0, + ones_j < N - 1 || ones_j > 0, + ensures + forall|alternate_path_: Seq| + ((#[trigger] alternate_path_.len() == path.len() + 1 && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path_, + )) ==> (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ + extra_item, + ] == alternate_path_)), +{ + assert forall|alternate_path_: Seq| + ((#[trigger] alternate_path_.len()) == path.len() + 1 && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path_, + )) implies (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ + extra_item, + ] == alternate_path_) by { + assert(is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path_.subrange(0, path.len() as int), + )); + + if path_less_than(path, alternate_path_.subrange(0, path.len() as int)) { + } else { + let m = alternate_path_[(path.len() - 1) as int]; + let n = alternate_path_[(path.len() + 0) as int]; + + let pair = choose|pair: (int, int)| + (is_adjacent::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + m, + n, + (#[trigger] pair.0, #[trigger] pair.1), + )); + + let i = pair.0; + let j = pair.1; + + assert(1 == grid@.map_values( + |row: [u8; N]| row@.map_values(|item| item as int), + )[ones_i][ones_j]); + + if (alternate_path_[path.len() as int] > extra_item) { + } else { + assert(path + seq![extra_item] =~= alternate_path_); + } + } + } +} + +pub fn min_path(grid: [[u8; N]; N], k: u8) -> (path: Vec) + requires + no_repeats_in_grid::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + ), + 2 <= N <= u8::MAX, + N * N <= u8::MAX, + ensures + path.len() == k, + is_minpath::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + path@.map_values(|item| item as int), + ), +{ + let (ones_coordinates, smallest_coordinates, smallest) = find_smallest_adjacent_to_one(grid); + let mut path: Vec = vec![]; + let mut k_counter = k; + let mut even = true; + + assert(forall|alternate_path: Seq| + ((alternate_path.len() == path.len() ==> path@.map_values(|j: u8| j as int) + == alternate_path))); + + #[verifier::loop_isolation(false)] + while k_counter > 0 + invariant + path.len() + k_counter == k, + // what we are trying to prove + forall|i: int| + (0 <= #[trigger] (i + 0) < path@.map_values(|j: u8| j as int).len() - 1) + ==> adjacent_numbers::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + path@.map_values(|j: u8| j as int)[i], + path@.map_values(|j: u8| j as int)[(i + 1)], + ), + forall|alternate_path: Seq| + ((#[trigger] alternate_path.len() == path@.map_values(|j: u8| j as int).len() + && is_valid_path::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + alternate_path, + )) ==> (path_less_than(path@.map_values(|j: u8| j as int), alternate_path) + || path@.map_values(|j: u8| j as int) == alternate_path)), + //remembering the last element + (path.len() > 0 && even) ==> path[path.len() - 1] == smallest, + (path.len() > 0 && !even) ==> path[path.len() - 1] == 1u8, + even || (path.len() >= 1), + decreases k_counter, + { + if (even) { + let t = path.len(); + let old_path = path.clone(); + let mut next_item = vec![1u8]; + path.append(&mut next_item); + proof { + lemma_less_than_step_even( + path@.map_values(|j: u8| j as int).subrange(0, path.len() - 1), + grid, + 1 as int, + ); + } + } else { + let mut next_item = vec![smallest]; + path.append(&mut next_item); + + proof { + lemma_less_than_step_odd( + path@.map_values(|j: u8| j as int).subrange(0, path.len() - 1), + grid, + smallest as int, + ones_coordinates.0 as int, + ones_coordinates.1 as int, + ); + } + } + even = !even; + k_counter = k_counter - 1; + + //proving adjacency + assert(forall|i: int| + (0 <= #[trigger] (i + 0) < path@.map_values(|j: u8| j as int).len() - 1) ==> (exists| + i0: int, + j0: int, + | + (is_adjacent::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + path@.map_values(|j: u8| j as int)[i], + path@.map_values(|j: u8| j as int)[(i + 1)], + (i0, j0), + )))); + } + assert(forall|i: int| + (0 <= i + 0 < path@.len() - 1) ==> adjacent_numbers::( + grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), + #[trigger] path@[i] as int, + path@[(i + 1)] as int, + )); + return path +} } // verus! -fn main() {} +fn main() { + println!("{:?}", min_path([[1, 2, 3], [4, 5, 6], [7, 8, 9]], 3)); + // > [1, 2, 1] + println!("{:?}", min_path([[5, 9, 3], [4, 1, 6], [7, 8, 2]], 7)); + // > [1, 4, 1, 4, 1, 4, 1] +} /* ### VERUS END @@ -21,7 +476,7 @@ fn main() {} /* ### PROMPT -def minPath(grid, k): +def min_path(grid, k): """ Given a grid with N rows and N columns (N >= 2) and a positive integer k, each cell of the grid contains a value. Every integer in the range [1, N * N] @@ -56,7 +511,7 @@ def minPath(grid, k): /* ### ENTRY POINT -minPath +min_path */ /* From 15c6e766b4b2b2014d6ebaa22766dfc7f5f06a5b Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Sat, 23 Nov 2024 19:32:55 -0500 Subject: [PATCH 15/22] Fix formatting --- tasks/human_eval_129.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tasks/human_eval_129.rs b/tasks/human_eval_129.rs index 30e49b3..fa6e672 100644 --- a/tasks/human_eval_129.rs +++ b/tasks/human_eval_129.rs @@ -34,10 +34,10 @@ pub open spec fn is_adjacent( &&& (0 <= coords.0 <= N - 1) &&& (0 <= coords.1 <= N - 1) &&& grid[coords.0][coords.1] == m - &&& ( (coords.0 < N - 1 && grid[coords.0 + 1][coords.1] == n) - || (coords.0 > 0 && grid[coords.0 - 1][coords.1] == n) - || (coords.1 < N - 1 && grid[coords.0][coords.1 + 1] == n) - || (coords.1 > 0 && grid[coords.0][coords.1 - 1] == n)) + &&& ( (coords.0 < N - 1 && grid[coords.0 + 1][coords.1 ] == n) + || (coords.0 > 0 && grid[coords.0 - 1][coords.1 ] == n) + || (coords.1 < N - 1 && grid[coords.0 ][coords.1 + 1] == n) + || (coords.1 > 0 && grid[coords.0 ][coords.1 - 1] == n)) } pub open spec fn adjacent_numbers(grid: Seq>, m: int, n: int) -> bool From 82583d330ef3b4c659d31d8f5e773f811502fbe9 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 25 Nov 2024 21:38:43 -0500 Subject: [PATCH 16/22] Patch from @amarshah1 --- tasks/human_eval_129.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_129.rs b/tasks/human_eval_129.rs index fa6e672..bf1dc86 100644 --- a/tasks/human_eval_129.rs +++ b/tasks/human_eval_129.rs @@ -275,7 +275,7 @@ proof fn lemma_less_than_step_even( alternate_path_, )) implies (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ extra_item, - ] == alternate_path_) by { + ] =~= alternate_path_) by { if path_less_than(path, alternate_path_.subrange(0, path.len() as int)) { } else { if (alternate_path_[path.len() as int] > extra_item) { @@ -328,7 +328,7 @@ proof fn lemma_less_than_step_odd( alternate_path_, )) implies (path_less_than(path + seq![extra_item], alternate_path_) || path + seq![ extra_item, - ] == alternate_path_) by { + ] =~= alternate_path_) by { assert(is_valid_path::( grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)), alternate_path_.subrange(0, path.len() as int), From 9b030cc5e0ebc2548cf8cb30439bc5cb06eaa7d9 Mon Sep 17 00:00:00 2001 From: Natalie Neamtu Date: Tue, 26 Nov 2024 12:39:13 -0800 Subject: [PATCH 17/22] Task 85 (#27) --- tasks/human_eval_085.rs | 54 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 53 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_085.rs b/tasks/human_eval_085.rs index 77474be..8b53740 100644 --- a/tasks/human_eval_085.rs +++ b/tasks/human_eval_085.rs @@ -9,7 +9,59 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +/// Returns x if x is odd, else returns 0. +pub open spec fn odd_or_zero(x: u32) -> u32 { + if x % 2 == 0 { + x + } else { + 0 + } +} + +/// Sum of all even elements at odd indices in the list. +pub open spec fn add_odd_evens(lst: Seq) -> int + decreases lst.len(), +{ + if (lst.len() < 2) { + 0 + } else { + odd_or_zero(lst[1]) + add_odd_evens(lst.skip(2)) + } +} + +/// Implementation: +/// Needed to change from (signed) integer to unsigned integer: Verus doesn't yet support % for signed integers. +/// Original definition is underspecified when list has no applicable elements: +/// assume that the desired return value is 0 for lists with no even integers at odd indices. +fn add(lst: Vec) -> (sum: u64) + requires + 0 < lst.len() < u32::MAX, + ensures + sum == add_odd_evens(lst@), +{ + let mut sum: u64 = 0; + let mut i = 1; + proof { + assert(lst@ =~= lst@.skip(0)); + } + while (i < lst.len()) + invariant + 1 <= i <= lst.len() + 1, + 0 < lst.len() < u32::MAX, + sum <= (u32::MAX) * i, + sum == add_odd_evens(lst@) - add_odd_evens(lst@.skip(i - 1 as int)), + { + if (lst[i] % 2 == 0) { + sum += lst[i] as u64; + } + proof { + // proves: add_odd_evens(lst@.skip(i - 1)) == odd_or_zero(lst[i]) + add_odd_evens(lst@.skip(i + 1)) + assert(lst@.skip(i - 1 as int).skip(2) =~= lst@.skip(i + 1 as int)); + } + i += 2; + } + return sum; +} } // verus! fn main() {} From b9e3e44f6d49e7a922f36d6377bca9e33200fd18 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Mon, 2 Dec 2024 10:49:53 -0500 Subject: [PATCH 18/22] Add a workflow that runs Verus on each task (#25) --- .github/workflows/verus.yml | 52 +++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 .github/workflows/verus.yml diff --git a/.github/workflows/verus.yml b/.github/workflows/verus.yml new file mode 100644 index 0000000..5efc68b --- /dev/null +++ b/.github/workflows/verus.yml @@ -0,0 +1,52 @@ +name: verus + +on: [pull_request, workflow_dispatch] + +jobs: + verus: + runs-on: ubuntu-latest + steps: + - name: checkout + uses: actions/checkout@v4 + + - name: Install toolchain dependencies + shell: bash + run: | + curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --profile minimal --default-toolchain none -y + echo "${CARGO_HOME:-$HOME/.cargo}/bin" >> $GITHUB_PATH + + - name: Install Rust toolchain + run: | + rustup update --no-self-update stable + rustup install 1.79.0-x86_64-unknown-linux-gnu + + - name: Get the URL for the latest Verus release + id: verus-release-info + run: | + jq --version + echo "VERUS_URL=$(curl -s https://api.github.com/repos/verus-lang/verus/releases | jq -r '.[].assets[].browser_download_url' | grep x86-linux -)" >> $GITHUB_OUTPUT + + - name: Download the latest Verus release + run: | + curl --proto '=https' --tlsv1.2 -LsSf ${{ steps.verus-release-info.outputs.VERUS_URL }} -o verus.zip; unzip verus.zip + + - name: run Verus + working-directory: ./tasks + run: | + # Run `verus` on each file, collecting failures if any + ANYFAILED="" + for i in *.rs; do + echo -n "[verus] $i: " + if ../verus-x86-linux/verus "$i" >/dev/null 2>/dev/null; then + echo "success" + else + echo "failed" + # Re-run `verus` on any failure just to display the actual output + ../verus-x86-linux/verus "$i" || true + ANYFAILED="$ANYFAILED $i" + fi + done + if [ -n "$ANYFAILED" ]; then + echo "Failed:$ANYFAILED" + exit 1 + fi From edf5779ee46c5f3a542fe8b8b3322a9fac9f3b78 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Fri, 6 Dec 2024 21:42:24 -0500 Subject: [PATCH 19/22] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3a24145..81b3f05 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# VerusBench: Hand-Written Examples of Verified Verus Code +# HumanEval-Verus: Hand-Written Examples of Verified Verus Code Derived From HumanEval This is intended to be a collection of examples translated from the [HumanEval] benchmark into Rust. The goal is that each example will include a textual From 126c905b3ccd704c53666e016a184315b384cb6e Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Fri, 6 Dec 2024 21:52:13 -0500 Subject: [PATCH 20/22] Add a list of contributors --- CONTRIBUTORS.md | 10 ++++++++++ README.md | 4 ++-- 2 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 CONTRIBUTORS.md diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md new file mode 100644 index 0000000..4147d46 --- /dev/null +++ b/CONTRIBUTORS.md @@ -0,0 +1,10 @@ +Alex Bai +Jay Bosamiya +Edwin Fernando +Md Rakib Hossain +Jay Lorch +Shan Lu +Natalie Neamtu +Bryan Parno +Amar Shah +Elanor Tang diff --git a/README.md b/README.md index 81b3f05..4f38d81 100644 --- a/README.md +++ b/README.md @@ -16,8 +16,8 @@ folder](./tasks/gpt), we have (unverified) Rust code generated by ChatGPT. Of course, the code may be completely incorrect, so feel free to ignore it and start your code from scratch. -Contributors will be acknowledged in any publications that may be published -about this benchmark. +[Contributors](./CONTRIBUTORS.md) should be acknowledged in any publications +that may be published about this benchmark. [HumanEval]: https://github.com/openai/human-eval [Verus]: https://github.com/verus-lang/verus From 4196755da573deb08c3cff684dbfe4163ddbe961 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Fri, 6 Dec 2024 21:54:35 -0500 Subject: [PATCH 21/22] Update CONTRIBUTORS.md to use bullets --- CONTRIBUTORS.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md index 4147d46..d52b7a9 100644 --- a/CONTRIBUTORS.md +++ b/CONTRIBUTORS.md @@ -1,10 +1,10 @@ -Alex Bai -Jay Bosamiya -Edwin Fernando -Md Rakib Hossain -Jay Lorch -Shan Lu -Natalie Neamtu -Bryan Parno -Amar Shah -Elanor Tang +- Alex Bai +- Jay Bosamiya +- Edwin Fernando +- Md Rakib Hossain +- Jay Lorch +- Shan Lu +- Natalie Neamtu +- Bryan Parno +- Amar Shah +- Elanor Tang From 69128e369a88100383f51bb4682e79ebe1d91592 Mon Sep 17 00:00:00 2001 From: MRHMisu <6449333+MRHMisu@users.noreply.github.com> Date: Thu, 12 Dec 2024 06:13:37 -0800 Subject: [PATCH 22/22] Completed task 146 (#29) --- tasks/human_eval_146.rs | 94 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 93 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_146.rs b/tasks/human_eval_146.rs index fbaa5ce..fdfc46e 100644 --- a/tasks/human_eval_146.rs +++ b/tasks/human_eval_146.rs @@ -9,7 +9,99 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// This spec function extracts the first digit of an integer +spec fn extract_first_digit_spec(n: int) -> int + decreases n, +{ + if n < 10 { + n + } else { + extract_first_digit_spec(n / 10) + } +} + +fn extract_first_digit(n: u32) -> (res: u32) + ensures + res == extract_first_digit_spec(n as int), +{ + if n < 10 { + n + } else { + extract_first_digit(n / 10) + } +} + +// This spec function extracts the last digit of an integer +spec fn extract_last_digit_spec(n: int) -> int { + n % 10 +} + +fn extract_last_digit(n: u32) -> (res: u32) + ensures + res == extract_last_digit_spec(n as int), +{ + n % 10 +} + +spec fn is_odd(n: int) -> bool { + (n % 2) != 0 +} + +//This spec function determines a valid integer according to the problem description +spec fn is_valid_element_spec(n: int) -> bool { + &&& (n > 10) + &&& is_odd(extract_first_digit_spec(n)) + &&& is_odd(extract_last_digit_spec(n)) +} + +fn is_valid_element(n: i32) -> (res: bool) + ensures + res == is_valid_element_spec(n as int), +{ + ((n > 10) && (extract_first_digit(n as u32) % 2 != 0) && (extract_last_digit(n as u32) % 2 + != 0)) +} + +//This spec function specifies the postcondition according to the problem description +spec fn special_filter_spec(seq: Seq) -> int + decreases seq.len(), +{ + if seq.len() == 0 { + 0 + } else { + special_filter_spec(seq.drop_last()) + if (is_valid_element_spec(seq.last() as int)) { + 1 as int + } else { + 0 as int + } + } +} + +fn special_filter(numbers: &Vec) -> (count: usize) + ensures + count == special_filter_spec(numbers@), +{ + let ghost numbers_length = numbers.len(); + let mut counter: usize = 0; + let mut index = 0; + while index < numbers.len() + invariant + 0 <= index <= numbers.len(), + 0 <= counter <= index, + counter == special_filter_spec(numbers@.subrange(0, index as int)), + { + if (is_valid_element(numbers[index])) { + counter += 1; + } + index += 1; + assert(numbers@.subrange(0, index - 1 as int) == numbers@.subrange( + 0, + index as int, + ).drop_last()); + } + assert(numbers@ == numbers@.subrange(0, numbers_length as int)); + counter +} } // verus! fn main() {}