From f5dff08dc4d25b38a59cab3d39b327d4968ef7b4 Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Fri, 20 Sep 2024 14:41:12 -0400 Subject: [PATCH 1/2] did task015 (Elanor, Amar, Yi) --- tasks/human_eval_015.rs | 150 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 148 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_015.rs b/tasks/human_eval_015.rs index 1fb9bd4..9fa2f9b 100644 --- a/tasks/human_eval_015.rs +++ b/tasks/human_eval_015.rs @@ -1,3 +1,5 @@ + + /* ### ID HumanEval/15 @@ -7,12 +9,155 @@ HumanEval/15 */ 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 ((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); + + // assert (number_to_char(i as nat) == number_to_char((i/10) as nat).add(seq![single_digit_number_to_char((i % 10) as nat)])); + // assert (number_to_char(n as nat) == number_to_char((i/10) as nat).add(seq![single_digit_number_to_char((i % 10) as nat)]).add(output@)); + + 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) + requires n >= 0 + 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); + + // assert (string_sequence((i) as nat) == string_sequence((i-1) as nat).add(seq![' '].add(number_to_char(i as nat)))); + + // assert (string_sequence((n) as nat) == string_sequence((i-1) as nat).add(seq![' '].add(number_to_char(i as nat))) + output@); + + next.append(&mut output); + output = next; + // assert (string_sequence((n) as nat) == string_sequence((i-1) as nat).add(seq![' ']) + output@); + 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!("{:?}", number_to_char_impl(158)); + // print!("{:?}", string_sequence_impl(20)); + } /* ### VERUS END @@ -59,3 +204,4 @@ def check(candidate): assert candidate(10) == '0 1 2 3 4 5 6 7 8 9 10' */ + From b3a1fa4a0cca9961dcc9c471bd0f01aac37213bf Mon Sep 17 00:00:00 2001 From: Amar Shah Date: Fri, 20 Sep 2024 18:07:44 -0400 Subject: [PATCH 2/2] Made changes requested by Bryan; ran verusfmt --- tasks/human_eval_015.rs | 277 +++++++++++++++++++++------------------- 1 file changed, 145 insertions(+), 132 deletions(-) diff --git a/tasks/human_eval_015.rs b/tasks/human_eval_015.rs index 9fa2f9b..2acd8d4 100644 --- a/tasks/human_eval_015.rs +++ b/tasks/human_eval_015.rs @@ -1,5 +1,3 @@ - - /* ### ID HumanEval/15 @@ -9,155 +7,171 @@ HumanEval/15 */ use vstd::prelude::*; - - verus! { - // 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' - } +// 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 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))) - } +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 ((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' - } +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![]; - pub fn number_to_char_impl(n : u8) -> (char_vec : Vec) - ensures char_vec@ == number_to_char(n as nat) + while (i > 0) + invariant + number_to_char(n as nat) == number_to_char(i as nat).add(output@), { - 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); - - // assert (number_to_char(i as nat) == number_to_char((i/10) as nat).add(seq![single_digit_number_to_char((i % 10) as nat)])); - // assert (number_to_char(n as nat) == number_to_char((i/10) as nat).add(seq![single_digit_number_to_char((i % 10) as nat)]).add(output@)); - - output.insert(0, current); - i = i / 10; + 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; + 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) - requires n >= 0 - ensures string_seq@ == string_sequence(n as nat) +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 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); - - // assert (string_sequence((i) as nat) == string_sequence((i-1) as nat).add(seq![' '].add(number_to_char(i as nat)))); - - // assert (string_sequence((n) as nat) == string_sequence((i-1) as nat).add(seq![' '].add(number_to_char(i as nat))) + output@); - - next.append(&mut output); - output = next; - // assert (string_sequence((n) as nat) == string_sequence((i-1) as nat).add(seq![' ']) + output@); - 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; + 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() { - // print!("{:?}", number_to_char_impl(158)); - // print!("{:?}", string_sequence_impl(20)); - } + print!("{:?}", string_sequence_impl(0)); + print!("{:?}", string_sequence_impl(5)); + print!("{:?}", string_sequence_impl(20)); +} /* ### VERUS END @@ -204,4 +218,3 @@ def check(candidate): assert candidate(10) == '0 1 2 3 4 5 6 7 8 9 10' */ -