From 8d40628ed0f267e5eb491278fe9745c3ab5202cf Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 5 Sep 2024 11:38:36 +0530 Subject: [PATCH 01/41] wrote 7 programs --- tasks/human_eval_053.rs | 7 +++++- tasks/human_eval_055.rs | 27 ++++++++++++++++++++- tasks/human_eval_056.rs | 48 ++++++++++++++++++++++++++++++++++++- tasks/human_eval_057.rs | 31 ++++++++++++++++++++++-- tasks/human_eval_059.rs | 53 +++++++++++++++++++++++++++++++++++++++-- tasks/human_eval_060.rs | 29 +++++++++++++++++++++- tasks/human_eval_061.rs | 48 ++++++++++++++++++++++++++++++++++++- 7 files changed, 234 insertions(+), 9 deletions(-) diff --git a/tasks/human_eval_053.rs b/tasks/human_eval_053.rs index 4b477c2..2b5d471 100644 --- a/tasks/human_eval_053.rs +++ b/tasks/human_eval_053.rs @@ -9,7 +9,12 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn add (x: i32, y: i32) -> (res: Option) + ensures + res.is_some() ==> res.unwrap() == x + y +{ + x.checked_add(y) +} } // verus! fn main() {} diff --git a/tasks/human_eval_055.rs b/tasks/human_eval_055.rs index 6564c0b..181e724 100644 --- a/tasks/human_eval_055.rs +++ b/tasks/human_eval_055.rs @@ -9,7 +9,32 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_fib(n: nat) -> nat + decreases n +{ + if (n == 0){ + 0 + } else if (n == 1) { + 1 + } else { + spec_fib((n - 1) as nat) + spec_fib((n - 2) as nat) + } +} + +fn fib(n: u32) -> (ret: Option) + ensures + ret.is_some() ==> ret.unwrap() == spec_fib(n as nat) +{ + match n { + 0 => Some(0), + 1 => Some(1), + _ => { + let n1 = fib(n - 1)?; + let n2 = fib(n - 2)?; + n1.checked_add(n2) + } + } +} } // verus! fn main() {} diff --git a/tasks/human_eval_056.rs b/tasks/human_eval_056.rs index fa4b405..c8fde0a 100644 --- a/tasks/human_eval_056.rs +++ b/tasks/human_eval_056.rs @@ -9,7 +9,53 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { + brackets.fold_left((0, true), |p: (int, bool), c| { + let (x, b) = p; + match (c) { + '<' => (x + 1, b), + '>' => (x - 1 , b && x == 0), + _ => (x, b), + } + }) +} + +spec fn spec_bracketing(brackets: Seq) -> bool { + let p = spec_bracketing_helper(brackets); + p.1 && p.0 == 0 +} + +fn correct_bracketing(brackets: &str) -> (ret: bool) + requires + brackets@.len() <= i32::MAX + -brackets@.len() >= i32::MIN + ensures + ret <==> spec_bracketing(brackets@) +{ + let mut i = 0; + let mut b = true; + let mut stack_size: i32 = 0; + + while i < brackets.unicode_len() + invariant + (stack_size as int, b) == spec_bracketing_helper(brackets@.subrange(0, i as int)), + stack_size <= i <= brackets@.len() <= i32::MAX, + stack_size >= -i >= -brackets@.len() >= i32::MIN, + { + let c = brackets.get_char(i); + let ghost prev = spec_bracketing_helper(brackets@.subrange(0, i as int)); + if (c == '<') { + stack_size += 1; + } else if (c == '>') { + b = b && stack_size == 0; + stack_size -= 1; + } + assert(brackets@.subrange(0, i+1 as int).drop_last() =~= brackets@.subrange(0, i as int)); + i += 1; + } + assert(brackets@ =~= brackets@.subrange(0, i as int)); + b && stack_size == 0 +} } // verus! fn main() {} diff --git a/tasks/human_eval_057.rs b/tasks/human_eval_057.rs index dd691d7..d6fb8b0 100644 --- a/tasks/human_eval_057.rs +++ b/tasks/human_eval_057.rs @@ -9,8 +9,35 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here - +fn monotonic(l: Vec) -> (ret: bool) + ensures + ret <==> forall |i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j) || + forall |i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(j) +{ + if l.len() == 0 || l.len() == 1 { + return true; + } + + let mut increasing = true; + let mut decreasing = true; + + let mut n = 0; + while n < l.len() - 1 + invariant + l.len() > 1, + n <= l.len() - 1, + increasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> l@.index(i) <= l@.index(j), + decreasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> l@.index(i) >= l@.index(j), + { + if l[n] < l[n + 1] { + decreasing = false; + } else if l[n] > l[n + 1] { + increasing = false; + } + n += 1; + } + increasing || decreasing +} } // verus! fn main() {} diff --git a/tasks/human_eval_059.rs b/tasks/human_eval_059.rs index fb5f1ad..c140ee1 100644 --- a/tasks/human_eval_059.rs +++ b/tasks/human_eval_059.rs @@ -8,8 +8,57 @@ HumanEval/59 use vstd::prelude::*; verus! { - -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// Note that according to the canonical solution 1 is treated as a possible largest prime. We'll stick to this + +spec fn spec_prime_helper(num: int, limit: int) -> bool { + forall |j: int| 2 <= j < limit ==> (#[trigger] (num % j)) != 0 +} + +spec fn spec_prime(num: int) -> bool { + spec_prime_helper(num, num) +} + +fn is_prime(num: u32) -> (result: bool) + requires num >= 2, + ensures result <==> spec_prime(num as int) +{ + let mut i = 2; + let mut result = true; + while i < num + invariant + 2 <= i <= num, + result <==> spec_prime_helper(num as int, i as int), + { + if num % i == 0 { + result = false; + } + i += 1; + } + result +} + +fn largest_prime_factor(n: u32) -> (largest: u32) + requires n >= 2, + ensures + 1 <= largest <= n, + spec_prime(largest as int), +{ + let mut largest = 1; + let mut j = 1; + while j < n + invariant + 1 <= largest <= j <= n, + spec_prime(largest as int), + + { + j += 1; + let flag = is_prime(j); + if n % j == 0 && flag { + largest = if largest > j { largest } else { j }; + } + } + largest +} } // verus! fn main() {} diff --git a/tasks/human_eval_060.rs b/tasks/human_eval_060.rs index a10a8fe..a1f16e8 100644 --- a/tasks/human_eval_060.rs +++ b/tasks/human_eval_060.rs @@ -9,7 +9,34 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_sum_to_n(n: nat) -> nat + decreases n +{ + if (n == 0) { + 0 + } else { + n + spec_sum_to_n((n-1) as nat) + } +} + +fn sum_to_n(n: u32) -> (sum: Option) + ensures + sum.is_some() ==> sum.unwrap() == spec_sum_to_n(n as nat), +{ + let mut res: u32 = 0; + let mut sum: u32 = 0; + let mut i: u32 = 0; + while i < n + invariant + i <= n, + res == spec_sum_to_n(i as nat), + res <= u32::MAX, + { + i += 1; + res = i.checked_add(res)?; + } + Some(res) +} } // verus! fn main() {} diff --git a/tasks/human_eval_061.rs b/tasks/human_eval_061.rs index ed3b8c0..5a91bf7 100644 --- a/tasks/human_eval_061.rs +++ b/tasks/human_eval_061.rs @@ -9,7 +9,53 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { + brackets.fold_left((0, true), |p: (int, bool), c| { + let (x, b) = p; + match (c) { + '(' => (x + 1, b), + ')' => (x - 1 , b && x == 0), + _ => (x, b), + } + }) +} + +spec fn spec_bracketing(brackets: Seq) -> bool { + let p = spec_bracketing_helper(brackets); + p.1 && p.0 == 0 +} + +fn correct_bracketing(brackets: &str) -> (ret: bool) + requires + brackets@.len() <= i32::MAX + -brackets@.len() >= i32::MIN + ensures + ret <==> spec_bracketing(brackets@) +{ + let mut i = 0; + let mut b = true; + let mut stack_size: i32 = 0; + + while i < brackets.unicode_len() + invariant + (stack_size as int, b) == spec_bracketing_helper(brackets@.subrange(0, i as int)), + stack_size <= i <= brackets@.len() <= i32::MAX, + stack_size >= -i >= -brackets@.len() >= i32::MIN, + { + let c = brackets.get_char(i); + let ghost prev = spec_bracketing_helper(brackets@.subrange(0, i as int)); + if (c == '(') { + stack_size += 1; + } else if (c == ')') { + b = b && stack_size == 0; + stack_size -= 1; + } + assert(brackets@.subrange(0, i+1 as int).drop_last() =~= brackets@.subrange(0, i as int)); + i += 1; + } + assert(brackets@ =~= brackets@.subrange(0, i as int)); + b && stack_size == 0 +} } // verus! fn main() {} From 226e36ecbb65747ac0be57e64108af3a25a0197c Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 9 Sep 2024 05:51:47 +0530 Subject: [PATCH 02/41] run verusfmt --- tasks/human_eval_053.rs | 4 ++-- tasks/human_eval_055.rs | 10 +++++----- tasks/human_eval_056.rs | 30 +++++++++++++++++------------- tasks/human_eval_057.rs | 17 ++++++++++------- tasks/human_eval_059.rs | 25 ++++++++++++++++--------- tasks/human_eval_060.rs | 4 ++-- tasks/human_eval_061.rs | 30 +++++++++++++++++------------- 7 files changed, 69 insertions(+), 51 deletions(-) diff --git a/tasks/human_eval_053.rs b/tasks/human_eval_053.rs index 2b5d471..f002bb5 100644 --- a/tasks/human_eval_053.rs +++ b/tasks/human_eval_053.rs @@ -9,9 +9,9 @@ use vstd::prelude::*; verus! { -fn add (x: i32, y: i32) -> (res: Option) +fn add(x: i32, y: i32) -> (res: Option) ensures - res.is_some() ==> res.unwrap() == x + y + res.is_some() ==> res.unwrap() == x + y, { x.checked_add(y) } diff --git a/tasks/human_eval_055.rs b/tasks/human_eval_055.rs index 181e724..a379fb8 100644 --- a/tasks/human_eval_055.rs +++ b/tasks/human_eval_055.rs @@ -9,10 +9,10 @@ use vstd::prelude::*; verus! { -spec fn spec_fib(n: nat) -> nat - decreases n +spec fn spec_fib(n: nat) -> nat + decreases n, { - if (n == 0){ + if (n == 0) { 0 } else if (n == 1) { 1 @@ -23,7 +23,7 @@ spec fn spec_fib(n: nat) -> nat fn fib(n: u32) -> (ret: Option) ensures - ret.is_some() ==> ret.unwrap() == spec_fib(n as nat) + ret.is_some() ==> ret.unwrap() == spec_fib(n as nat), { match n { 0 => Some(0), @@ -32,7 +32,7 @@ fn fib(n: u32) -> (ret: Option) let n1 = fib(n - 1)?; let n2 = fib(n - 2)?; n1.checked_add(n2) - } + }, } } diff --git a/tasks/human_eval_056.rs b/tasks/human_eval_056.rs index c8fde0a..aaebd73 100644 --- a/tasks/human_eval_056.rs +++ b/tasks/human_eval_056.rs @@ -10,14 +10,18 @@ use vstd::prelude::*; verus! { spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { - brackets.fold_left((0, true), |p: (int, bool), c| { - let (x, b) = p; - match (c) { - '<' => (x + 1, b), - '>' => (x - 1 , b && x == 0), - _ => (x, b), - } - }) + brackets.fold_left( + (0, true), + |p: (int, bool), c| + { + let (x, b) = p; + match (c) { + '<' => (x + 1, b), + '>' => (x - 1, b && x == 0), + _ => (x, b), + } + }, + ) } spec fn spec_bracketing(brackets: Seq) -> bool { @@ -27,10 +31,10 @@ spec fn spec_bracketing(brackets: Seq) -> bool { fn correct_bracketing(brackets: &str) -> (ret: bool) requires - brackets@.len() <= i32::MAX - -brackets@.len() >= i32::MIN + brackets@.len() <= i32::MAX, + -brackets@.len() >= i32::MIN, ensures - ret <==> spec_bracketing(brackets@) + ret <==> spec_bracketing(brackets@), { let mut i = 0; let mut b = true; @@ -39,7 +43,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) while i < brackets.unicode_len() invariant (stack_size as int, b) == spec_bracketing_helper(brackets@.subrange(0, i as int)), - stack_size <= i <= brackets@.len() <= i32::MAX, + stack_size <= i <= brackets@.len() <= i32::MAX, stack_size >= -i >= -brackets@.len() >= i32::MIN, { let c = brackets.get_char(i); @@ -50,7 +54,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) b = b && stack_size == 0; stack_size -= 1; } - assert(brackets@.subrange(0, i+1 as int).drop_last() =~= brackets@.subrange(0, i as int)); + assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); i += 1; } assert(brackets@ =~= brackets@.subrange(0, i as int)); diff --git a/tasks/human_eval_057.rs b/tasks/human_eval_057.rs index d6fb8b0..4e3560f 100644 --- a/tasks/human_eval_057.rs +++ b/tasks/human_eval_057.rs @@ -11,23 +11,25 @@ verus! { fn monotonic(l: Vec) -> (ret: bool) ensures - ret <==> forall |i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j) || - forall |i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(j) + ret <==> forall|i: int, j: int| + 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j) || forall|i: int, j: int| + 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(j), { if l.len() == 0 || l.len() == 1 { return true; } - let mut increasing = true; let mut decreasing = true; - + let mut n = 0; - while n < l.len() - 1 + while n < l.len() - 1 invariant l.len() > 1, n <= l.len() - 1, - increasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> l@.index(i) <= l@.index(j), - decreasing <==> forall |i: int, j: int| 0 <= i < j < n+1 ==> l@.index(i) >= l@.index(j), + increasing <==> forall|i: int, j: int| + 0 <= i < j < n + 1 ==> l@.index(i) <= l@.index(j), + decreasing <==> forall|i: int, j: int| + 0 <= i < j < n + 1 ==> l@.index(i) >= l@.index(j), { if l[n] < l[n + 1] { decreasing = false; @@ -38,6 +40,7 @@ fn monotonic(l: Vec) -> (ret: bool) } increasing || decreasing } + } // verus! fn main() {} diff --git a/tasks/human_eval_059.rs b/tasks/human_eval_059.rs index c140ee1..4244b35 100644 --- a/tasks/human_eval_059.rs +++ b/tasks/human_eval_059.rs @@ -8,10 +8,10 @@ HumanEval/59 use vstd::prelude::*; verus! { -// Note that according to the canonical solution 1 is treated as a possible largest prime. We'll stick to this +// Note that according to the canonical solution 1 is treated as a possible largest prime. We'll stick to this spec fn spec_prime_helper(num: int, limit: int) -> bool { - forall |j: int| 2 <= j < limit ==> (#[trigger] (num % j)) != 0 + forall|j: int| 2 <= j < limit ==> (#[trigger] (num % j)) != 0 } spec fn spec_prime(num: int) -> bool { @@ -19,8 +19,10 @@ spec fn spec_prime(num: int) -> bool { } fn is_prime(num: u32) -> (result: bool) - requires num >= 2, - ensures result <==> spec_prime(num as int) + requires + num >= 2, + ensures + result <==> spec_prime(num as int), { let mut i = 2; let mut result = true; @@ -38,23 +40,28 @@ fn is_prime(num: u32) -> (result: bool) } fn largest_prime_factor(n: u32) -> (largest: u32) - requires n >= 2, - ensures + requires + n >= 2, + ensures 1 <= largest <= n, spec_prime(largest as int), { let mut largest = 1; let mut j = 1; while j < n - invariant + invariant 1 <= largest <= j <= n, spec_prime(largest as int), - { j += 1; let flag = is_prime(j); if n % j == 0 && flag { - largest = if largest > j { largest } else { j }; + largest = + if largest > j { + largest + } else { + j + }; } } largest diff --git a/tasks/human_eval_060.rs b/tasks/human_eval_060.rs index a1f16e8..33e656a 100644 --- a/tasks/human_eval_060.rs +++ b/tasks/human_eval_060.rs @@ -10,12 +10,12 @@ use vstd::prelude::*; verus! { spec fn spec_sum_to_n(n: nat) -> nat - decreases n + decreases n, { if (n == 0) { 0 } else { - n + spec_sum_to_n((n-1) as nat) + n + spec_sum_to_n((n - 1) as nat) } } diff --git a/tasks/human_eval_061.rs b/tasks/human_eval_061.rs index 5a91bf7..32c78a8 100644 --- a/tasks/human_eval_061.rs +++ b/tasks/human_eval_061.rs @@ -10,14 +10,18 @@ use vstd::prelude::*; verus! { spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { - brackets.fold_left((0, true), |p: (int, bool), c| { - let (x, b) = p; - match (c) { - '(' => (x + 1, b), - ')' => (x - 1 , b && x == 0), - _ => (x, b), - } - }) + brackets.fold_left( + (0, true), + |p: (int, bool), c| + { + let (x, b) = p; + match (c) { + '(' => (x + 1, b), + ')' => (x - 1, b && x == 0), + _ => (x, b), + } + }, + ) } spec fn spec_bracketing(brackets: Seq) -> bool { @@ -27,10 +31,10 @@ spec fn spec_bracketing(brackets: Seq) -> bool { fn correct_bracketing(brackets: &str) -> (ret: bool) requires - brackets@.len() <= i32::MAX - -brackets@.len() >= i32::MIN + brackets@.len() <= i32::MAX, + -brackets@.len() >= i32::MIN, ensures - ret <==> spec_bracketing(brackets@) + ret <==> spec_bracketing(brackets@), { let mut i = 0; let mut b = true; @@ -39,7 +43,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) while i < brackets.unicode_len() invariant (stack_size as int, b) == spec_bracketing_helper(brackets@.subrange(0, i as int)), - stack_size <= i <= brackets@.len() <= i32::MAX, + stack_size <= i <= brackets@.len() <= i32::MAX, stack_size >= -i >= -brackets@.len() >= i32::MIN, { let c = brackets.get_char(i); @@ -50,7 +54,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) b = b && stack_size == 0; stack_size -= 1; } - assert(brackets@.subrange(0, i+1 as int).drop_last() =~= brackets@.subrange(0, i as int)); + assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); i += 1; } assert(brackets@ =~= brackets@.subrange(0, i as int)); From ad1a3626729678a33d0d1e1e1046d2f769872c39 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 11 Sep 2024 08:07:26 +0530 Subject: [PATCH 03/41] fix error in spec of correct bracketing - 56 and 61 --- tasks/human_eval_056.rs | 5 +++-- tasks/human_eval_057.rs | 5 ++--- tasks/human_eval_061.rs | 5 +++-- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/tasks/human_eval_056.rs b/tasks/human_eval_056.rs index aaebd73..1e82a6d 100644 --- a/tasks/human_eval_056.rs +++ b/tasks/human_eval_056.rs @@ -9,6 +9,7 @@ use vstd::prelude::*; verus! { +// say the return value is (x: b), x = number of '<' - number of '>', b = whether x ever dipped below 0 spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { brackets.fold_left( (0, true), @@ -17,7 +18,7 @@ spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { let (x, b) = p; match (c) { '<' => (x + 1, b), - '>' => (x - 1, b && x == 0), + '>' => (x - 1, b && x != 0), _ => (x, b), } }, @@ -51,7 +52,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) if (c == '<') { stack_size += 1; } else if (c == '>') { - b = b && stack_size == 0; + b = b && stack_size != 0; stack_size -= 1; } assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); diff --git a/tasks/human_eval_057.rs b/tasks/human_eval_057.rs index 4e3560f..62cb771 100644 --- a/tasks/human_eval_057.rs +++ b/tasks/human_eval_057.rs @@ -11,9 +11,8 @@ verus! { fn monotonic(l: Vec) -> (ret: bool) ensures - ret <==> forall|i: int, j: int| - 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j) || forall|i: int, j: int| - 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(j), + ret <==> (forall|i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) <= l@.index(j)) || ( + forall|i: int, j: int| 0 <= i < j < l@.len() ==> l@.index(i) >= l@.index(j)), { if l.len() == 0 || l.len() == 1 { return true; diff --git a/tasks/human_eval_061.rs b/tasks/human_eval_061.rs index 32c78a8..ba45b79 100644 --- a/tasks/human_eval_061.rs +++ b/tasks/human_eval_061.rs @@ -9,6 +9,7 @@ use vstd::prelude::*; verus! { +// say the return value is (x: b), x = number of '(' - number of ')', b = whether x ever dipped below 0 spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { brackets.fold_left( (0, true), @@ -17,7 +18,7 @@ spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { let (x, b) = p; match (c) { '(' => (x + 1, b), - ')' => (x - 1, b && x == 0), + ')' => (x - 1, b && x != 0), _ => (x, b), } }, @@ -51,7 +52,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) if (c == '(') { stack_size += 1; } else if (c == ')') { - b = b && stack_size == 0; + b = b && stack_size != 0; stack_size -= 1; } assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); From b0a0ce67555c0f7b1b70d4e0869a2adf1eba368a Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 11 Sep 2024 14:25:14 +0530 Subject: [PATCH 04/41] complete 62 63 and 64 --- tasks.md | 20 ++++++++-------- tasks/human_eval_062.rs | 29 ++++++++++++++++++++++- tasks/human_eval_063.rs | 26 ++++++++++++++++++++- tasks/human_eval_064.rs | 51 ++++++++++++++++++++++++++++++++++++++++- 4 files changed, 113 insertions(+), 13 deletions(-) diff --git a/tasks.md b/tasks.md index e42fef8..7365c7f 100644 --- a/tasks.md +++ b/tasks.md @@ -53,18 +53,18 @@ - [ ] 050 - [ ] 051 - [x] 052 - jaylorch -- [ ] 053 +- [x] 053 - edwin1729 - [ ] 054 -- [ ] 055 -- [ ] 056 -- [ ] 057 +- [x] 055 - edwin1729 +- [x] 056 - edwin1729 +- [x] 057 - edwin1729 - [ ] 058 -- [ ] 059 -- [ ] 060 -- [ ] 061 -- [ ] 062 -- [ ] 063 -- [ ] 064 +- [x] 059 - edwin1729 +- [x] 060 - edwin1729 +- [x] 061 - edwin1729 +- [x] 062 - edwin1729 +- [x] 063 - edwin1729 +- [x] 064 - edwin1729 - [ ] 065 - [ ] 066 - [ ] 067 diff --git a/tasks/human_eval_062.rs b/tasks/human_eval_062.rs index 8dbce59..c75afba 100644 --- a/tasks/human_eval_062.rs +++ b/tasks/human_eval_062.rs @@ -9,7 +9,34 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn derivative(xs: &Vec) -> (ret: Option>) + ensures + ret.is_some() ==> xs@.len() == 0 || xs@.map(|i: int, x| i * x).skip(1) + =~= ret.unwrap()@.map_values(|x| x as int), +{ + let mut ret = Vec::new(); + if xs.len() == 0 { + return Some(ret); + } + let mut i = 1; + while i < xs.len() + invariant + xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= ret@.map_values(|x| x as int), + 1 <= i <= xs.len(), + { + ret.push(xs[i].checked_mul(i)?); + + let ghost prods = xs@.map(|i: int, x| i * x); + assert(prods.subrange(1, i as int).push(prods.index(i as int)) =~= prods.subrange( + 1, + i + 1 as int, + )); + + i += 1; + } + assert(xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= xs@.map(|i: int, x| i * x).skip(1)); + Some(ret) +} } // verus! fn main() {} diff --git a/tasks/human_eval_063.rs b/tasks/human_eval_063.rs index be72630..f44704b 100644 --- a/tasks/human_eval_063.rs +++ b/tasks/human_eval_063.rs @@ -9,7 +9,31 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_fibfib(n: nat) -> nat + decreases n, +{ + if (n == 0) { + 0 + } else if (n == 1) { + 0 + } else if (n == 2) { + 1 + } else { + spec_fibfib((n - 1) as nat) + spec_fibfib((n - 2) as nat) + spec_fibfib((n - 3) as nat) + } +} + +fn fibfib(x: u32) -> (ret: Option) + ensures + ret.is_some() ==> spec_fibfib(x as nat) == ret.unwrap(), +{ + match (x) { + 0 => Some(0), + 1 => Some(0), + 2 => Some(1), + _ => fibfib(x - 1)?.checked_add(fibfib(x - 2)?)?.checked_add(fibfib(x - 3)?), + } +} } // verus! fn main() {} diff --git a/tasks/human_eval_064.rs b/tasks/human_eval_064.rs index f7433ca..344d87d 100644 --- a/tasks/human_eval_064.rs +++ b/tasks/human_eval_064.rs @@ -9,7 +9,56 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn is_vowel(c: char) -> bool { + c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c == 'I' + || c == 'O' || c == 'U' +} + +spec fn vowels(s: Seq) -> Seq { + s.filter(|c| is_vowel(c)) +} + +fn vowels_count(s: &str) -> (ret: u32) + requires + s@.len() <= u32::MAX, + ensures + ret == vowels(s@).len() + if (s@.len() > 0 && (s@.last() == 'y' || s@.last() == 'Y')) { + 1int // add 1 if the last letter is 'y' + + } else { + 0int + }, +{ + let mut ctr = 0; + let len = s.unicode_len(); + if len == 0 { + return ctr; + } + assert(len > 0); + let mut i = 0; + for i in 0..len + invariant + ctr == vowels(s@.subrange(0, i as int)).len(), + ctr <= i <= s@.len() == len <= u32::MAX, + ctr < u32::MAX || is_vowel(s@.last()), + { + let c = s.get_char(i); + reveal_with_fuel(Seq::filter, 2); + assert(s@.subrange(0, i + 1 as int).drop_last() =~= s@.subrange(0, i as int)); + if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u' || c == 'A' || c == 'E' || c + == 'I' || c == 'O' || c == 'U') { + ctr += 1; + } + } + assert(ctr == vowels(s@).len()) by { + assert(s@.subrange(0, len as int) =~= s@); + } + let c = s.get_char(len - 1); + if (c == 'y' || c == 'Y') { + ctr += 1 + } + ctr +} } // verus! fn main() {} From 63ac4f193fd7dd75537cccf8efd57537f5f2c5eb Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 12 Sep 2024 06:53:23 +0530 Subject: [PATCH 05/41] initial commit in branch in-progress --- tasks/human_eval_054.rs | 20 ++++- tasks/human_eval_066.rs | 63 +++++++++++++++ tasks/human_eval_068.rs | 43 ++++++++++- tasks/human_eval_070.rs | 95 ++++++++++++++++++++++- tasks/human_eval_072.rs | 165 +++++++++++++++++++++++++++++++++++++++- tasks/human_eval_075.rs | 47 +++++++++++- 6 files changed, 428 insertions(+), 5 deletions(-) diff --git a/tasks/human_eval_054.rs b/tasks/human_eval_054.rs index 1c44e12..d44b7d7 100644 --- a/tasks/human_eval_054.rs +++ b/tasks/human_eval_054.rs @@ -5,11 +5,29 @@ HumanEval/54 /* ### VERUS BEGIN */ +use std::collections::BTreeSet; +use std::collections::HashSet; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// fn str_to_set(s: &str) -> HashSet { +// s.chars().collect() +// } +fn same_chars(left: &str, right: &str) -> (res: bool) + ensures + res <==> left@.to_set() =~= right@.to_set(), +{ + left.chars().collect::>().eq(&right.chars().collect::>()) +} + +#[verifier::external_fn_specification] +proof fn lemma_set_eq(left: BTreeSet, right: BTreeSet) + ensures + left.eq(right) ==> left@ =~= right@, +{ + admit(); +} } // verus! fn main() {} diff --git a/tasks/human_eval_066.rs b/tasks/human_eval_066.rs index 6021409..ad73fbf 100644 --- a/tasks/human_eval_066.rs +++ b/tasks/human_eval_066.rs @@ -11,6 +11,69 @@ verus! { // TODO: Put your solution (the specification, implementation, and proof) to the task here +fn toLower(c: char) -> (ret: char) + // requires + // c.is_ascii(), + ensures 'A' <= c <= 'Z' ==> ret as u32 == add(c as u32, 32u32), + c < 'A' || c > 'Z' ==> ret == c +{ + if ('A' <= c && c <= 'Z') { + char::from_u32(c as u32 + 32).unwrap() + } else { + c + } +} + +// pub fn upper_sum_rec(s: &str) -> u64 +// ensures upper_sum_rec(s) >= 0 +// { +// if s.len() == 0 { +// 0 +// } else { +// let remaining = upper_sum_rec(&s[1..]); +// to_int(s.chars().next().unwrap()) as u64 + remaining +// } +// } + +// pub proof fn upper_sum_rec_prop(s: &str) +// requires s.len() > 0, +// ensures upper_sum_rec(s) == upper_sum_rec(&s[..s.len()-1]) + to_int(s.chars().nth(s.len()-1).unwrap()) as u64 +// { +// if s.len() > 1 { +// assert(s[1..][..s[1..].len() - 1] == s[1..s.len() - 1]); +// } +// } + +// pub fn to_int(c: char) -> u8 +// ensures 'A' <= c <= 'Z' ==> to_int(c) == c as u8, +// c < 'A' || c > 'Z' ==> to_int(c) == 0 +// { +// if 'A' <= c && c <= 'Z' { c as u8 } else { 0 } +// } + +// pub fn upper_sum(s: &str) -> (res: u64) +// ensures res == upper_sum_rec(s) +// { +// let mut res = 0; +// let mut i = 0; +// while i < s.len() +// invariant +// 0 <= i && i <= s.len(), +// res == upper_sum_rec(&s[..i]) +// { +// res = res + to_int(s.chars().nth(i).unwrap()) as u64; +// proof { +// assert(upper_sum_rec(&s[..i+1]) == upper_sum_rec(&s[..i]) + to_int(s.chars().nth(i).unwrap()) as u64); +// assert(s[..i+1][..i] == s[..i]); +// upper_sum_rec_prop(&s[..i+1]); +// } +// i = i + 1; +// } +// proof { +// assert(s == &s[..s.len()]); +// } +// res +// } } // verus! fn main() {} diff --git a/tasks/human_eval_068.rs b/tasks/human_eval_068.rs index b6b971f..6d8da84 100644 --- a/tasks/human_eval_068.rs +++ b/tasks/human_eval_068.rs @@ -9,7 +9,48 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_pluck(s: Seq) -> Seq{ + let filtered = s.map(|i: int, x: usize| (i, x)).filter(|p: (int, usize)| p.1 % 2 == 0); + if filtered.len() == 0 { + Seq::empty() + } else { + let (i, x) = filtered.min_via(|p1: (int, usize), p2: (int, usize)| p1.1 <= p2.1); + seq![x, i as usize] + } +} + +fn pluck(nodes: &Vec) -> (ret: Vec) + ensures + ret@ =~= spec_pluck(nodes@), +{ + let mut ret = Vec::new(); + let ghost filtered: Seq<(int, usize)> = Seq::empty(); + let ghost mapped: Seq<(int, usize)> = Seq::empty(); + for i in 0..nodes.len() + invariant + ret@ =~= spec_pluck(nodes@.subrange(0, i as int)), + mapped =~= nodes@.subrange(0, i as int).map(|i: int, x: usize| (i, x)), + filtered =~= mapped.filter(|p: (int, usize)| p.1 % 2 == 0), + filtered.len() <= mapped.len() == i as int, + i <= nodes.len(), + { + reveal_with_fuel(Seq::filter, 5); + reveal_with_fuel(Seq::min_via, 5); + proof { mapped = mapped.push((i as int, nodes[i as int])); } + // assert(mapped.len() == i + 1 as int); + // assert(mapped.subrange(0, i+1 as int).drop_last() =~= mapped.subrange(0, i as int)); + // assert(nodes@.subrange(0, i+1 as int).drop_last() =~= nodes@.subrange(0, i as int)); + assert(mapped.index(i as int).1 == nodes[i as int]); + if (nodes[i] % 2 == 0) { + proof { filtered = filtered.push((i as int, nodes[i as int])); } + if (ret.len() == 0 || nodes[i] < ret[0]) { + ret = vec![nodes[i], i]; + } + } + } + assert(nodes@.subrange(0, nodes.len() as int) =~= nodes@); + ret +} } // verus! fn main() {} diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index 21b837c..74dee57 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -9,7 +9,100 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn strange_sort_list(s: &Vec) -> (ret: Vec) + ensures s@.len() == ret@.len() +{ + let (_, strange) = strange_sort_list_helper(s); + strange +} + +#[verifier::external_body] +fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) + ensures + s@.to_multiset() == (ret.0)@.to_multiset(), + s@.len() == (ret.0)@.len() == (ret.1)@.len(), + forall|i: int| 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), + forall|i: int| 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index(s@.len() - (i - 1) / 2 - 1) +{ + let sorted = sort_seq(s); + let mut strange = Vec::new(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len(), + strange@.len() == i, + forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2), + forall|j: int| 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index(sorted@.len() - (j / 2) - 1) + { + if i % 2 == 0 { + strange.push(sorted[i / 2]); + } else { + let r = (i - 1) / 2; + strange.push(sorted[s.len() - r - 1]); + } + i += 1; + } + (sorted, strange) +} + +fn sort_seq(s: &Vec) -> (ret: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), + ret@.len() == s@.len(), + s@.to_multiset() == ret@.to_multiset() +{ + let mut sorted = s.clone(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len(), + forall|j: int, k: int| 0 <= j < k < i ==> sorted@.index(j) <= sorted@.index(k), + s@.to_multiset() == sorted@.to_multiset(), + forall|j: int, k: int| 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), + sorted@.len() == s@.len() + { + let mut min_index: usize = i; + let mut j: usize = i + 1; + while j < sorted.len() + invariant + i <= min_index < j <= sorted.len(), + forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k) + { + if sorted[j] < sorted[min_index] { + min_index = j; + } + j += 1; + } + if min_index != i { + let curr_val = sorted[i]; + let min_val = sorted[min_index]; + sorted.set(i, min_val); + sorted.set(min_index, curr_val); + proof { + // swap_preserves_multiset(s@.map_values(|x| x as int), i as int, min_index as int); + assume(s@.to_multiset() == sorted@.to_multiset()); + } + } + i += 1; + } + sorted +} + +// #[verifier::external_body] +// // Helper lemma to prove that swapping two elements doesn't change the multiset +// proof fn swap_preserves_multiset(s: Seq, i: int, j: int) +// requires 0 <= i < s.len() && 0 <= j < s.len() +// ensures s.to_multiset() == s.update(i, s.index(j)).update(j, s.index(i)).to_multiset() +// { +// let s_new = s.update(i, s.index(j)).update(j, s.index(i)); +// assert(s.to_multiset().count(s.index(i)) == s_new.to_multiset().count(s.index(i))); +// assert(s.to_multiset().count(s.index(j)) == s_new.to_multiset().count(s.index(j))); +// assert forall|x: int| s.to_multiset().count(x) == s_new.to_multiset().count(x) by { +// if x != s.index(i) && x != s.index(j) { +// assert(s.to_multiset().count(x) == s_new.to_multiset().count(x)); +// } +// } +// } } // verus! fn main() {} diff --git a/tasks/human_eval_072.rs b/tasks/human_eval_072.rs index 921035d..135f2d9 100644 --- a/tasks/human_eval_072.rs +++ b/tasks/human_eval_072.rs @@ -9,7 +9,170 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn will_it_fly(qs: &Vec, w: u32) -> (ret: bool) + ensures + ret <==> qs@ =~= qs@.reverse() && spec_sum(qs@) <= w, +{ + palindrome(qs) && sum_lesser_than_limit(qs, w) +} + +fn palindrome(qs: &Vec) -> (ret: bool) + ensures + ret <==> qs@ =~= qs@.reverse(), +{ + let mut ret = true; + let mut i: usize = 0; + while i < qs.len() / 2 + invariant + i <= qs@.len() / 2, + ret <==> qs@.subrange(0, i as int) =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse(), + { + // reveal_with_fuel(Seq::reverse, 5); //VERUS BUG on uncomment + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse().push(qs@.index(qs@.len() - (i +1)))); + if qs[i] != qs[qs.len() - i - 1] { + ret = false; + } + i += 1; + } + let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int); + let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int); + + proof { + lemma_palindrome_of_halves(fst_half, snd_half); + if (qs.len() % 2) == 1 { + lemma_palindrome_of_halves_and_middle(fst_half, qs@.index((qs@.len() / 2) as int), snd_half); + assert(qs@ =~= fst_half + qs@.subrange((qs@.len() / 2) as int, qs@.len() - qs@.len() / 2) + snd_half); + } else { + assert(qs@ =~= fst_half + snd_half); + } + } + ret + +} + +proof fn lemma_palindrome_of_halves(fst: Seq, snd: Seq) + requires + fst.len() == snd.len(), + ensures + fst =~= snd.reverse() <==> (fst + snd) =~= (fst + snd).reverse(), +{ + let s1 = fst + snd; + let s2 = s1.reverse(); + if (fst =~= snd.reverse()) { + assert(forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]); + } else { + assert(exists |i: int| 0 <= i < fst.len() && #[trigger] fst[i] != snd.reverse()[i] && s1[i] != s2[i]); + assert(exists |i: int| 0 <= i < s1.len() && s1[i] != s2[i]); + } +} + +proof fn lemma_palindrome_of_halves_and_middle(fst: Seq, middle: T, snd: Seq) + requires + fst.len() == snd.len(), + ensures + fst =~= snd.reverse() <==> (fst + seq![middle] + snd) =~= (fst + seq![middle] + snd).reverse(), +{ + let s1 = fst + seq![middle] + snd; + let s2 = s1.reverse(); + if (fst =~= snd.reverse()) { + assert(forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]); + } else { + assert(exists |i: int| 0 <= i < fst.len() && #[trigger] fst[i] != snd.reverse()[i] && s1[i] != s2[i]); + assert(exists |i: int| 0 <= i < s1.len() && s1[i] != s2[i]); + } +} + +fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) + ensures + ret <==> spec_sum(qs@) <= w +{ + let mut sum: u32 = 0; + for i in 0..qs.len() + invariant + sum == spec_sum(qs@.subrange(0, i as int)), + i <= qs.len(), + sum <= w, + { + proof { + assert(spec_sum(qs@.subrange(0, i+1)) <= spec_sum(qs@)) by { + assert(qs@ == qs@.subrange(0, qs@.len() as int)); + lemma_increasing_sum(qs@); + } + + assert(spec_sum(qs@.subrange(0, i as int)) + qs[i as int] == spec_sum(qs@.subrange(0, i+1))) by { + assert(qs@.subrange(0, i+1).drop_last() == qs@.subrange(0, i as int)); + } + } + let sum_opt = sum.checked_add(qs[i]); + if sum_opt.is_none() { + assert(spec_sum(qs@.subrange(0, i+1)) > u32::MAX >= w); + return false; + } else { + sum = sum_opt.unwrap(); + if sum > w { + assert(spec_sum(qs@.subrange(0, i+1)) > w); + return false; + } + } + } + assume(sum == spec_sum(qs@)); + true +} + +spec fn spec_sum(s: Seq) -> int { + s.fold_left(0, |x: int, y| x + y) +} + +proof fn lemma_increasing_sum(s: Seq) + ensures + forall |i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), +{ + // if s.len() == 0 { + // // Base case: empty sequence + // assert(forall |i: int, j: int| + // #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + // 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j))); + // } else { + // // Inductive case + // let s_init = s.subrange(0, s.len() as int - 1); + + // // Inductive hypothesis + // lemma_increasing_sum(s_init); + + // assert(forall |i: int, j: int| + // #![trigger spec_sum(s_init.subrange(0, i)), spec_sum(s_init.subrange(0, j))] + // 0 <= i <= j <= s_init.len() ==> spec_sum(s_init.subrange(0, i)) <= spec_sum(s_init.subrange(0, j))); + + // // Prove for the full sequence + // assert(forall |i: int, j: int| + // #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + // 0 <= i <= j <= s.len() ==> { + // if j < s.len() { + // // Use inductive hypothesis + // spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) + // } else { + // // j == s.len(), compare with s_init + // if i < s.len() { + // spec_sum(s.subrange(0, i)) <= spec_sum(s_init) && + // spec_sum(s_init) <= spec_sum(s) + // } else { + // // i == j == s.len() + // spec_sum(s.subrange(0, i)) == spec_sum(s) + // } + // } + // }); + + // // Additional assertion to connect s_init and s + // assert(spec_sum(s_init) <= spec_sum(s)) by { + // assert(s == s_init.push(s.last())); + // assert(spec_sum(s) == spec_sum(s_init) + s.last()); + // } + // } + admit(); +} } // verus! fn main() {} diff --git a/tasks/human_eval_075.rs b/tasks/human_eval_075.rs index 4bf4540..fc5f963 100644 --- a/tasks/human_eval_075.rs +++ b/tasks/human_eval_075.rs @@ -9,7 +9,52 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn spec_prime(p: int) -> bool { + p > 1 && + forall|k: int| 1 < k < p ==> #[trigger] (p % k) != 0 +} + +fn prime(p: u64) -> (ret: bool) + ensures + ret <==> spec_prime(p as int), +{ + for k in 2..p { + if p % k == 0 { + return false; + } + } + true +} + +fn is_multiply_prime(x: u64) -> (ans: bool) + requires x > 1, + ensures ans <==> exists|a: int, b: int, c: int| + spec_prime(a) && spec_prime(b) && spec_prime(c) && x == a * b * c, +{ + for a in 2..x+1 + invariant forall|i: int, j: int, k: int| + (spec_prime(i) && spec_prime(j) && spec_prime(k) && i < a as int) ==> x != i * j * k, + { + if prime(a) { + for b in 2..x+1 + invariant forall|j: int, k: int| + (spec_prime(j) && spec_prime(k) && j < b as int) ==> x != (a as int) * j * k, + { + if prime(b) { + for c in 2..x+1 + invariant forall|k: int| + (spec_prime(k) && k < c as int) ==> x != (a as int) * (b as int) * k, + { + if prime(c) && x == a * b * c { + return true; + } + } + } + } + } + } + false +} } // verus! fn main() {} From ee82f5ea633fabebe72433e7bbbcfe2330c77d1d Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 12 Sep 2024 14:52:43 +0530 Subject: [PATCH 06/41] complete is_cube excpet for lemma that cubes are increasing --- tasks/human_eval_077.rs | 106 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 105 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_077.rs b/tasks/human_eval_077.rs index 957a9bb..38331a2 100644 --- a/tasks/human_eval_077.rs +++ b/tasks/human_eval_077.rs @@ -5,11 +5,115 @@ HumanEval/77 /* ### VERUS BEGIN */ +use vstd::arithmetic::mul::*; +// use vstd::arithmetic::internals::mul_internals::*; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn is_cube(x: i32) -> (ret: bool) + requires + x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 + (-1 > x || x > 1), + + ensures + ret <==> exists|i: int| + 1 <= i && spec_abs(x as int) == #[trigger] (i * i * i), +{ + let x_abs = ex_abs(x); + // if x_abs == 0 { + // return true; + // } + // assert(x > 0); + + let mut i = 2; + while i < x_abs + invariant + forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j), + 2 <= i <= spec_abs(x as int) == x_abs, + { + let prod = checked_cube(i); + if prod.is_some() && prod.unwrap() == ex_abs(x){ + return true; + } + i += 1; + } + broadcast use group_mul_properties; + assert(forall|j: int| 2 <= j ==> spec_abs(x as int) != #[trigger] (j * j * j)) by { + assert(forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j)); + + assert(forall|j: int| i <= j ==> spec_abs(x as int) < #[trigger] (j * j * j)) by { + assert(spec_abs(x as int) < #[trigger] (i * i * i)) by { + // lemma_mul_strictly_increases(i as int, i as int); + // lemma_mul_strictly_increases(i as int, i * i); + assert(i <= i * i <= i * i * i); + } + assume(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); + } + } + false +} + +fn checked_cube(x: i32) -> (ret: Option) + requires + x >= 0, + ensures + ret.is_some() ==> ret.unwrap() == x * x * x, + ret.is_none() ==> x * x * x > i32::MAX, +{ + //x == 0 done separately to invoke lemma_mul_increases which requires x > 0 + if x == 0 { + return Some(0); + } + let sqr = x.checked_mul(x); + if sqr.is_some() { + let cube = sqr.unwrap().checked_mul(x); + if cube.is_some() { + let ans = cube.unwrap(); + assert(ans == x * x * x); + Some(ans) + } else { + assert(x * x * x > i32::MAX); + None + } + } else { + assert(x > 0); + assert(x * x > i32::MAX); + proof { + lemma_mul_increases(x as int, x * x); + } + assert(x * x * x >= x * x); + None + } +} + +spec fn spec_abs(x: int) -> int { + if x < 0 { + -x + } else { + x + } +} + +fn ex_abs(x: i32) -> (ret: i32) + requires + x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 + + ensures + ret == spec_abs(x as int), +{ + if x < 0 { + -x + } else { + x + } +} + +// proof fn lemma_cube_increases(x: int) { +// lemma_mul_induction_auto(x, |u: int| 1 < u ==> u * u * u <= (u + 1) * (u + 1) * (u + 1)); +// } + +// assume(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); } // verus! fn main() {} From bbe5c9e8dfd4092ac01a7e33d34457935a68f394 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 12 Sep 2024 14:52:43 +0530 Subject: [PATCH 07/41] complete is_cube excpet for lemma that cubes are increasing --- tasks/human_eval_077.rs | 110 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 109 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_077.rs b/tasks/human_eval_077.rs index 957a9bb..25a9276 100644 --- a/tasks/human_eval_077.rs +++ b/tasks/human_eval_077.rs @@ -5,11 +5,119 @@ HumanEval/77 /* ### VERUS BEGIN */ +use vstd::arithmetic::mul::*; use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn is_cube(x: i32) -> (ret: bool) + requires + x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 + + ensures + ret <==> exists|i: int| 0 <= i && spec_abs(x as int) == #[trigger] (i * i * i), +{ + let x_abs = ex_abs(x); + + // dealing with cases where the the cube is not greater than the number + if x_abs == 0 { + assert(spec_abs(x as int) == 0 * 0 * 0); + return true; + } else if (x_abs == 1) { + assert(spec_abs(x as int) == 1 * 1 * 1); + return true; + } + assert(-1 > x || x > 1); + let mut i = 2; + while i < x_abs + invariant + forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j), + 2 <= i <= spec_abs(x as int) == x_abs, + { + let prod = checked_cube(i); + if prod.is_some() && prod.unwrap() == ex_abs(x) { + return true; + } + i += 1; + } + assert(forall|j: int| 2 <= j ==> spec_abs(x as int) != #[trigger] (j * j * j)) by { + assert(forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j)); + + assert(forall|j: int| i <= j ==> spec_abs(x as int) < #[trigger] (j * j * j)) by { + assert(spec_abs(x as int) < #[trigger] (i * i * i)) by { + broadcast use group_mul_properties; + + assert(i <= i * i <= i * i * i); + } + lemma_cube_increases(); + assert(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); + } + } + false +} + +fn checked_cube(x: i32) -> (ret: Option) + requires + x >= 0, + ensures + ret.is_some() ==> ret.unwrap() == x * x * x, + ret.is_none() ==> x * x * x > i32::MAX, +{ + //x == 0 done separately to invoke lemma_mul_increases which requires x > 0 + if x == 0 { + return Some(0); + } + let sqr = x.checked_mul(x); + if sqr.is_some() { + let cube = sqr.unwrap().checked_mul(x); + if cube.is_some() { + let ans = cube.unwrap(); + assert(ans == x * x * x); + Some(ans) + } else { + assert(x * x * x > i32::MAX); + None + } + } else { + assert(x > 0); + assert(x * x > i32::MAX); + proof { + lemma_mul_increases(x as int, x * x); + } + assert(x * x * x >= x * x); + None + } +} + +spec fn spec_abs(x: int) -> int { + if x < 0 { + -x + } else { + x + } +} + +fn ex_abs(x: i32) -> (ret: i32) + requires + x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 + + ensures + ret == spec_abs(x as int), +{ + if x < 0 { + -x + } else { + x + } +} + +proof fn lemma_cube_increases() + ensures + forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j), +{ + admit(); + // lemma_mul_induction_auto(x, |u: int| 1 < u ==> u * u * u <= (u + 1) * (u + 1) * (u + 1)); +} } // verus! fn main() {} From 103a4908d573b67c6045d7b6d7005c689bd4f85e Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Fri, 13 Sep 2024 10:19:00 +0530 Subject: [PATCH 08/41] add iterative fibonacci (55) and minor spec change to 56 and 61 --- .../{human_eval_055.rs => human_eval_055a.rs} | 0 tasks/human_eval_055b.rs | 105 ++++++++++++++++++ tasks/human_eval_056.rs | 6 +- tasks/human_eval_061.rs | 6 +- 4 files changed, 111 insertions(+), 6 deletions(-) rename tasks/{human_eval_055.rs => human_eval_055a.rs} (100%) create mode 100644 tasks/human_eval_055b.rs diff --git a/tasks/human_eval_055.rs b/tasks/human_eval_055a.rs similarity index 100% rename from tasks/human_eval_055.rs rename to tasks/human_eval_055a.rs diff --git a/tasks/human_eval_055b.rs b/tasks/human_eval_055b.rs new file mode 100644 index 0000000..fddf289 --- /dev/null +++ b/tasks/human_eval_055b.rs @@ -0,0 +1,105 @@ +/* +### ID +HumanEval/55 +*/ +/* +### VERUS BEGIN +*/ +use vstd::prelude::*; + +verus! { + +// O(n) non-recursive solution using same spec as 55a +spec fn spec_fib(n: nat) -> nat + decreases n, +{ + if (n == 0) { + 0 + } else if (n == 1) { + 1 + } else { + spec_fib((n - 1) as nat) + spec_fib((n - 2) as nat) + } +} + +fn fib(n: u32) -> (ret: Option) + ensures + ret.is_some() ==> ret.unwrap() == spec_fib(n as nat), +{ + if n == 0 { + return Some(0); + } + if n == 1 { + return Some(1); + } + 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, + a as int == spec_fib((i - 1) as nat), + b as int == spec_fib(i as nat), + { + let sum = a.checked_add(b)?; + a = b; + b = sum; + } + Some(b) +} + +} // verus! +fn main() {} + +/* +### VERUS END +*/ + +/* +### PROMPT + + +def fib(n: int): + """Return n-th Fibonacci number. + >>> fib(10) + 55 + >>> fib(1) + 1 + >>> fib(8) + 21 + """ + +*/ + +/* +### ENTRY POINT +fib +*/ + +/* +### CANONICAL SOLUTION + if n == 0: + return 0 + if n == 1: + return 1 + return fib(n - 1) + fib(n - 2) + +*/ + +/* +### TEST + + +METADATA = {} + + +def check(candidate): + assert candidate(10) == 55 + assert candidate(1) == 1 + assert candidate(8) == 21 + assert candidate(11) == 89 + assert candidate(12) == 144 + + +*/ diff --git a/tasks/human_eval_056.rs b/tasks/human_eval_056.rs index 1e82a6d..6d80498 100644 --- a/tasks/human_eval_056.rs +++ b/tasks/human_eval_056.rs @@ -9,7 +9,7 @@ use vstd::prelude::*; verus! { -// say the return value is (x: b), x = number of '<' - number of '>', b = whether x ever dipped below 0 +// say the return value is (x, b), x = number of '<' - number of '>', b = whether x ever dipped below 0 spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { brackets.fold_left( (0, true), @@ -18,7 +18,7 @@ spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { let (x, b) = p; match (c) { '<' => (x + 1, b), - '>' => (x - 1, b && x != 0), + '>' => (x - 1, b && x - 1 >= 0), _ => (x, b), } }, @@ -52,7 +52,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) if (c == '<') { stack_size += 1; } else if (c == '>') { - b = b && stack_size != 0; + b = b && stack_size > 0; stack_size -= 1; } assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); diff --git a/tasks/human_eval_061.rs b/tasks/human_eval_061.rs index ba45b79..af571f0 100644 --- a/tasks/human_eval_061.rs +++ b/tasks/human_eval_061.rs @@ -9,7 +9,7 @@ use vstd::prelude::*; verus! { -// say the return value is (x: b), x = number of '(' - number of ')', b = whether x ever dipped below 0 +// say the return value is (x, b), x = number of '(' - number of ')', b = whether x ever dipped below 0 spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { brackets.fold_left( (0, true), @@ -18,7 +18,7 @@ spec fn spec_bracketing_helper(brackets: Seq) -> (int, bool) { let (x, b) = p; match (c) { '(' => (x + 1, b), - ')' => (x - 1, b && x != 0), + ')' => (x - 1, b && x - 1 >= 0), _ => (x, b), } }, @@ -52,7 +52,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool) if (c == '(') { stack_size += 1; } else if (c == ')') { - b = b && stack_size != 0; + b = b && stack_size > 0; stack_size -= 1; } assert(brackets@.subrange(0, i + 1 as int).drop_last() =~= brackets@.subrange(0, i as int)); From e667d0b3d6ae9283d65bb3128a23238fc5f0b2dd Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 16 Sep 2024 15:22:25 +0530 Subject: [PATCH 09/41] complete proof that cubes are increasing --- tasks/human_eval_077.rs | 76 ++++++++++++++++++++++++++--------------- 1 file changed, 48 insertions(+), 28 deletions(-) diff --git a/tasks/human_eval_077.rs b/tasks/human_eval_077.rs index 25a9276..974b6d0 100644 --- a/tasks/human_eval_077.rs +++ b/tasks/human_eval_077.rs @@ -6,6 +6,7 @@ HumanEval/77 ### VERUS BEGIN */ use vstd::arithmetic::mul::*; +use vstd::math::abs; use vstd::prelude::*; verus! { @@ -15,36 +16,36 @@ fn is_cube(x: i32) -> (ret: bool) x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 ensures - ret <==> exists|i: int| 0 <= i && spec_abs(x as int) == #[trigger] (i * i * i), + ret <==> exists|i: int| 0 <= i && abs(x as int) == #[trigger] (i * i * i), { - let x_abs = ex_abs(x); + let x_abs = x.abs(); // dealing with cases where the the cube is not greater than the number if x_abs == 0 { - assert(spec_abs(x as int) == 0 * 0 * 0); + assert(abs(x as int) == 0 * 0 * 0); return true; } else if (x_abs == 1) { - assert(spec_abs(x as int) == 1 * 1 * 1); + assert(abs(x as int) == 1 * 1 * 1); return true; } assert(-1 > x || x > 1); let mut i = 2; while i < x_abs invariant - forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j), - 2 <= i <= spec_abs(x as int) == x_abs, + forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j), + 2 <= i <= abs(x as int) == x_abs, { let prod = checked_cube(i); - if prod.is_some() && prod.unwrap() == ex_abs(x) { + if prod.is_some() && prod.unwrap() == x.abs() { return true; } i += 1; } - assert(forall|j: int| 2 <= j ==> spec_abs(x as int) != #[trigger] (j * j * j)) by { - assert(forall|j: int| 2 <= j < i ==> spec_abs(x as int) != #[trigger] (j * j * j)); + assert(forall|j: int| 2 <= j ==> abs(x as int) != #[trigger] (j * j * j)) by { + assert(forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j)); - assert(forall|j: int| i <= j ==> spec_abs(x as int) < #[trigger] (j * j * j)) by { - assert(spec_abs(x as int) < #[trigger] (i * i * i)) by { + assert(forall|j: int| i <= j ==> abs(x as int) < #[trigger] (j * j * j)) by { + assert(abs(x as int) < #[trigger] (i * i * i)) by { broadcast use group_mul_properties; assert(i <= i * i <= i * i * i); @@ -89,34 +90,53 @@ fn checked_cube(x: i32) -> (ret: Option) } } -spec fn spec_abs(x: int) -> int { - if x < 0 { - -x - } else { - x - } -} - -fn ex_abs(x: i32) -> (ret: i32) +#[verifier::external_fn_specification] +pub fn ex_abs(x: i32) -> (ret: i32) requires x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 ensures - ret == spec_abs(x as int), + ret == abs(x as int), { - if x < 0 { - -x - } else { - x - } + x.abs() } proof fn lemma_cube_increases() ensures forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j), { - admit(); - // lemma_mul_induction_auto(x, |u: int| 1 < u ==> u * u * u <= (u + 1) * (u + 1) * (u + 1)); + assert forall|i: int, j: int| + 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j) by { + lemma_cube_increases_params(i, j); + } +} + +proof fn lemma_cube_increases_params(i: int, j: int) + ensures + 0 <= i <= j ==> (i * i * i) <= (j * j * j), + decreases j - i, +{ + // base case + if (i == j) { + } + // inductive case + else if (i < j) { + lemma_cube_increases_params(i, j - 1); + lemma_cube_increases_helper(j - 1); + + } +} + +proof fn lemma_cube_increases_helper(i: int) + ensures + i >= 0 ==> (i * i * i) <= (i + 1) * (i + 1) * (i + 1), +{ + broadcast use group_mul_properties; + + if (i > 0) { + assert((i + 1) * (i + 1) * (i + 1) == i * i * i + 3 * i * i + 3 * i + 1); + assert(i * i * i + 3 * i * i + 3 * i + 1 > i * i * i); + } } } // verus! From 9cf8c072d350e3ceb3e62183ea5e036dca2debfe Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 16 Sep 2024 15:22:53 +0530 Subject: [PATCH 10/41] complete 75, product of 3 primes --- tasks/human_eval_075.rs | 106 +++++++++++++++++++++++++++++++++------- 1 file changed, 88 insertions(+), 18 deletions(-) diff --git a/tasks/human_eval_075.rs b/tasks/human_eval_075.rs index fc5f963..9984319 100644 --- a/tasks/human_eval_075.rs +++ b/tasks/human_eval_075.rs @@ -5,20 +5,27 @@ HumanEval/75 /* ### VERUS BEGIN */ +use vstd::arithmetic::mul::*; use vstd::prelude::*; verus! { spec fn spec_prime(p: int) -> bool { - p > 1 && - forall|k: int| 1 < k < p ==> #[trigger] (p % k) != 0 + p > 1 && forall|k: int| 1 < k < p ==> #[trigger] (p % k) != 0 } -fn prime(p: u64) -> (ret: bool) +fn prime(p: u32) -> (ret: bool) ensures ret <==> spec_prime(p as int), { - for k in 2..p { + if p <= 1 { + return false; + } + for k in 2..p + invariant + forall|j: int| 1 < j < k ==> #[trigger] (p as int % j) != 0, + k <= p, + { if p % k == 0 { return false; } @@ -26,26 +33,48 @@ fn prime(p: u64) -> (ret: bool) true } -fn is_multiply_prime(x: u64) -> (ans: bool) - requires x > 1, - ensures ans <==> exists|a: int, b: int, c: int| - spec_prime(a) && spec_prime(b) && spec_prime(c) && x == a * b * c, +fn is_multiply_prime(x: u32) -> (ans: bool) + requires + x > 1, + ensures + ans <==> exists|a: int, b: int, c: int| + spec_prime(a) && spec_prime(b) && spec_prime(c) && x == a * b * c, { - for a in 2..x+1 - invariant forall|i: int, j: int, k: int| - (spec_prime(i) && spec_prime(j) && spec_prime(k) && i < a as int) ==> x != i * j * k, + let mut a = 1; + while a < x + invariant + forall|i: int, j: int, k: int| + (spec_prime(i) && spec_prime(j) && spec_prime(k) && i <= a && j <= x && k <= x) + ==> x != i * j * k, + a <= x, { + a += 1; if prime(a) { - for b in 2..x+1 - invariant forall|j: int, k: int| - (spec_prime(j) && spec_prime(k) && j < b as int) ==> x != (a as int) * j * k, + let mut b = 1; + while b < x + invariant + forall|j: int, k: int| + (spec_prime(j) && spec_prime(k) && j <= b && k <= x) ==> x != (a as int) * j + * k, + spec_prime(a as int), + a <= x, + b <= x, { + b += 1; if prime(b) { - for c in 2..x+1 - invariant forall|k: int| - (spec_prime(k) && k < c as int) ==> x != (a as int) * (b as int) * k, + let mut c = 1; + while c < x + invariant + forall|k: int| (spec_prime(k) && k <= c as int) ==> x != a * b * k, + spec_prime(a as int), + spec_prime(b as int), + a <= x, + b <= x, + c <= x, { - if prime(c) && x == a * b * c { + c += 1; + let prod = checked_mul_thrice(a, b, c); + if prime(c) && prod.is_some() && x == prod.unwrap() { return true; } } @@ -53,9 +82,50 @@ fn is_multiply_prime(x: u64) -> (ans: bool) } } } + assert(forall|i: int, j: int, k: int| + i <= x && j <= x && k <= x && spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j + * k); + // prove that that even if the factors are not in the range [2, x], the product is still not equal to x + assert forall|i: int, j: int, k: int| + spec_prime(i) && spec_prime(j) && spec_prime(k) ==> x != i * j * k by { + if (i > 1 && j > 1 && k > 1 && (i > x || j > x || k > x)) { + broadcast use group_mul_properties; + + assert(i * j * k > x); + } + } false } +fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option) + ensures + ret.is_some() ==> ret.unwrap() == x * y * z, + ret.is_none() ==> x * y * z > u32::MAX, +{ + // x,y,z == 0 done separately to invoke lemma_mul_increases which requires x > 0 + if (x == 0 || y == 0 || z == 0) { + return Some(0); + } + assert(x > 0 && y > 0 && z > 0); + let prod2 = x.checked_mul(y); + if prod2.is_some() { + let prod3 = prod2.unwrap().checked_mul(z); + if prod3.is_some() { + let ans = prod3.unwrap(); + assert(ans == x * y * z); + Some(ans) + } else { + assert(x * y * z > u32::MAX); + None + } + } else { + broadcast use group_mul_properties; + + assert(x * y * z >= y * z); + None + } +} + } // verus! fn main() {} From 2d543adbff6d9b5e5fb4e32ba6353d6c756b284b Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 16 Sep 2024 16:46:47 +0530 Subject: [PATCH 11/41] complete will_it_fly by completing proof of increasing sum also remove the palindrome helper lemmas, they were automatically deduced --- tasks/human_eval_072.rs | 144 ++++++++++++++-------------------------- 1 file changed, 50 insertions(+), 94 deletions(-) diff --git a/tasks/human_eval_072.rs b/tasks/human_eval_072.rs index 135f2d9..6b42855 100644 --- a/tasks/human_eval_072.rs +++ b/tasks/human_eval_072.rs @@ -25,11 +25,18 @@ fn palindrome(qs: &Vec) -> (ret: bool) while i < qs.len() / 2 invariant i <= qs@.len() / 2, - ret <==> qs@.subrange(0, i as int) =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse(), + ret <==> qs@.subrange(0, i as int) =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse(), { - // reveal_with_fuel(Seq::reverse, 5); //VERUS BUG on uncomment - assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); - assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse().push(qs@.index(qs@.len() - (i +1)))); + // reveal_with_fuel(Seq::reverse, 5); // VERUS BUG on uncomment. file issue + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() + =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse().push(qs@.index(qs@.len() - (i + 1)))); if qs[i] != qs[qs.len() - i - 1] { ret = false; } @@ -37,81 +44,49 @@ fn palindrome(qs: &Vec) -> (ret: bool) } let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int); let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int); - proof { - lemma_palindrome_of_halves(fst_half, snd_half); if (qs.len() % 2) == 1 { - lemma_palindrome_of_halves_and_middle(fst_half, qs@.index((qs@.len() / 2) as int), snd_half); - assert(qs@ =~= fst_half + qs@.subrange((qs@.len() / 2) as int, qs@.len() - qs@.len() / 2) + snd_half); + assert(qs@ =~= fst_half + qs@.subrange( + (qs@.len() / 2) as int, + qs@.len() - qs@.len() / 2, + ) + snd_half); } else { assert(qs@ =~= fst_half + snd_half); } } ret - -} - -proof fn lemma_palindrome_of_halves(fst: Seq, snd: Seq) - requires - fst.len() == snd.len(), - ensures - fst =~= snd.reverse() <==> (fst + snd) =~= (fst + snd).reverse(), -{ - let s1 = fst + snd; - let s2 = s1.reverse(); - if (fst =~= snd.reverse()) { - assert(forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]); - } else { - assert(exists |i: int| 0 <= i < fst.len() && #[trigger] fst[i] != snd.reverse()[i] && s1[i] != s2[i]); - assert(exists |i: int| 0 <= i < s1.len() && s1[i] != s2[i]); - } -} - -proof fn lemma_palindrome_of_halves_and_middle(fst: Seq, middle: T, snd: Seq) - requires - fst.len() == snd.len(), - ensures - fst =~= snd.reverse() <==> (fst + seq![middle] + snd) =~= (fst + seq![middle] + snd).reverse(), -{ - let s1 = fst + seq![middle] + snd; - let s2 = s1.reverse(); - if (fst =~= snd.reverse()) { - assert(forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i]); - } else { - assert(exists |i: int| 0 <= i < fst.len() && #[trigger] fst[i] != snd.reverse()[i] && s1[i] != s2[i]); - assert(exists |i: int| 0 <= i < s1.len() && s1[i] != s2[i]); - } } -fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) +fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) ensures - ret <==> spec_sum(qs@) <= w + ret <==> spec_sum(qs@) <= w, { let mut sum: u32 = 0; - for i in 0..qs.len() + for i in 0..qs.len() invariant sum == spec_sum(qs@.subrange(0, i as int)), i <= qs.len(), sum <= w, { proof { - assert(spec_sum(qs@.subrange(0, i+1)) <= spec_sum(qs@)) by { + assert(spec_sum(qs@.subrange(0, i + 1)) <= spec_sum(qs@)) by { assert(qs@ == qs@.subrange(0, qs@.len() as int)); lemma_increasing_sum(qs@); } - - assert(spec_sum(qs@.subrange(0, i as int)) + qs[i as int] == spec_sum(qs@.subrange(0, i+1))) by { - assert(qs@.subrange(0, i+1).drop_last() == qs@.subrange(0, i as int)); + assert(spec_sum(qs@.subrange(0, i as int)) + qs[i as int] == spec_sum( + qs@.subrange(0, i + 1), + )) by { + assert(qs@.subrange(0, i + 1).drop_last() == qs@.subrange(0, i as int)); } } let sum_opt = sum.checked_add(qs[i]); if sum_opt.is_none() { - assert(spec_sum(qs@.subrange(0, i+1)) > u32::MAX >= w); + assert(spec_sum(qs@.subrange(0, i + 1)) > u32::MAX >= w); return false; } else { sum = sum_opt.unwrap(); if sum > w { - assert(spec_sum(qs@.subrange(0, i+1)) > w); + assert(spec_sum(qs@.subrange(0, i + 1)) > w); return false; } } @@ -126,52 +101,33 @@ spec fn spec_sum(s: Seq) -> int { proof fn lemma_increasing_sum(s: Seq) ensures - forall |i: int, j: int| - #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), { - // if s.len() == 0 { - // // Base case: empty sequence - // assert(forall |i: int, j: int| - // #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] - // 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j))); - // } else { - // // Inductive case - // let s_init = s.subrange(0, s.len() as int - 1); - - // // Inductive hypothesis - // lemma_increasing_sum(s_init); - - // assert(forall |i: int, j: int| - // #![trigger spec_sum(s_init.subrange(0, i)), spec_sum(s_init.subrange(0, j))] - // 0 <= i <= j <= s_init.len() ==> spec_sum(s_init.subrange(0, i)) <= spec_sum(s_init.subrange(0, j))); - - // // Prove for the full sequence - // assert(forall |i: int, j: int| - // #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] - // 0 <= i <= j <= s.len() ==> { - // if j < s.len() { - // // Use inductive hypothesis - // spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) - // } else { - // // j == s.len(), compare with s_init - // if i < s.len() { - // spec_sum(s.subrange(0, i)) <= spec_sum(s_init) && - // spec_sum(s_init) <= spec_sum(s) - // } else { - // // i == j == s.len() - // spec_sum(s.subrange(0, i)) == spec_sum(s) - // } - // } - // }); - - // // Additional assertion to connect s_init and s - // assert(spec_sum(s_init) <= spec_sum(s)) by { - // assert(s == s_init.push(s.last())); - // assert(spec_sum(s) == spec_sum(s_init) + s.last()); - // } - // } - admit(); + assert forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) by { + if (0 <= i <= j <= s.len()) { + lemma_increasing_sum_params(s, i, j); + } + } +} + +// i and j are ends of the subrange - exclusive +proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int) + requires + 0 <= i <= j <= s.len(), + ensures + spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + decreases j - i, +{ + if (i < j) { + assert (spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { + assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1)); + } + lemma_increasing_sum_params(s, i, j - 1); + } } } // verus! From 204444b19e601e89f39c4045df40f8eb9f57aeb1 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 08:28:59 +0530 Subject: [PATCH 12/41] adding a simple loop invariant to strange sort completes it --- tasks/human_eval_070.rs | 46 ++++++++++++++++++++++++----------------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index 74dee57..ee3e757 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -9,30 +9,30 @@ use vstd::prelude::*; verus! { -fn strange_sort_list(s: &Vec) -> (ret: Vec) - ensures s@.len() == ret@.len() -{ - let (_, strange) = strange_sort_list_helper(s); - strange -} - -#[verifier::external_body] +// returns (sorted, strange). Also returning sorted solely to have access to it for writing postcondition fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) - ensures + ensures s@.to_multiset() == (ret.0)@.to_multiset(), s@.len() == (ret.0)@.len() == (ret.1)@.len(), - forall|i: int| 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), - forall|i: int| 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index(s@.len() - (i - 1) / 2 - 1) + forall|i: int| + 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), + forall|i: int| + 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index( + s@.len() - (i - 1) / 2 - 1, + ), { let sorted = sort_seq(s); let mut strange = Vec::new(); let mut i: usize = 0; while i < sorted.len() invariant - i <= sorted.len(), + i <= sorted.len() == s@.len(), strange@.len() == i, forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2), - forall|j: int| 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index(sorted@.len() - (j / 2) - 1) + forall|j: int| + 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index( + sorted@.len() - (j / 2) - 1, + ), { if i % 2 == 0 { strange.push(sorted[i / 2]); @@ -45,11 +45,19 @@ fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) (sorted, strange) } +fn strange_sort_list(s: &Vec) -> (ret: Vec) + ensures + s@.len() == ret@.len(), +{ + let (_, strange) = strange_sort_list_helper(s); + strange +} + fn sort_seq(s: &Vec) -> (ret: Vec) - ensures + ensures forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), ret@.len() == s@.len(), - s@.to_multiset() == ret@.to_multiset() + s@.to_multiset() == ret@.to_multiset(), { let mut sorted = s.clone(); let mut i: usize = 0; @@ -58,15 +66,16 @@ fn sort_seq(s: &Vec) -> (ret: Vec) i <= sorted.len(), forall|j: int, k: int| 0 <= j < k < i ==> sorted@.index(j) <= sorted@.index(k), s@.to_multiset() == sorted@.to_multiset(), - forall|j: int, k: int| 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), - sorted@.len() == s@.len() + forall|j: int, k: int| + 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), + sorted@.len() == s@.len(), { let mut min_index: usize = i; let mut j: usize = i + 1; while j < sorted.len() invariant i <= min_index < j <= sorted.len(), - forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k) + forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), { if sorted[j] < sorted[min_index] { min_index = j; @@ -103,7 +112,6 @@ fn sort_seq(s: &Vec) -> (ret: Vec) // } // } // } - } // verus! fn main() {} From 828facb0634d8af65043e012bddc741b932562ea Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 08:29:33 +0530 Subject: [PATCH 13/41] use the quantifiers instead of functional programs as spec in pluck smallest even --- tasks/human_eval_068.rs | 71 +++++++++++++++++++++-------------------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/tasks/human_eval_068.rs b/tasks/human_eval_068.rs index 6d8da84..8751cc5 100644 --- a/tasks/human_eval_068.rs +++ b/tasks/human_eval_068.rs @@ -9,47 +9,50 @@ use vstd::prelude::*; verus! { -spec fn spec_pluck(s: Seq) -> Seq{ - let filtered = s.map(|i: int, x: usize| (i, x)).filter(|p: (int, usize)| p.1 % 2 == 0); - if filtered.len() == 0 { - Seq::empty() - } else { - let (i, x) = filtered.min_via(|p1: (int, usize), p2: (int, usize)| p1.1 <= p2.1); - seq![x, i as usize] - } -} - -fn pluck(nodes: &Vec) -> (ret: Vec) +fn pluck_smallest_even(nodes: &Vec) -> (result: Vec) + requires + nodes@.len() <= u32::MAX, + forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] >= 0, ensures - ret@ =~= spec_pluck(nodes@), + result@.len() == 0 || result@.len() == 2, + result@.len() == 2 ==> 0 <= result@[1] < nodes@.len() && nodes@[result@[1] as int] + == result@[0], + result@.len() == 2 ==> result@[0] % 2 == 0, + result@.len() == 2 ==> forall|i: int| + 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> result@[0] <= nodes@[i], + result@.len() == 2 ==> forall|i: int| + 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > result@[0], + result@.len() == 0 ==> forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] % 2 != 0, { - let mut ret = Vec::new(); - let ghost filtered: Seq<(int, usize)> = Seq::empty(); - let ghost mapped: Seq<(int, usize)> = Seq::empty(); + let mut smallest_even: Option = None; + let mut smallest_index: Option = None; + for i in 0..nodes.len() invariant - ret@ =~= spec_pluck(nodes@.subrange(0, i as int)), - mapped =~= nodes@.subrange(0, i as int).map(|i: int, x: usize| (i, x)), - filtered =~= mapped.filter(|p: (int, usize)| p.1 % 2 == 0), - filtered.len() <= mapped.len() == i as int, - i <= nodes.len(), + 0 <= i <= nodes@.len(), + nodes@.len() <= u32::MAX, + smallest_even.is_none() == smallest_index.is_none(), + smallest_index.is_some() ==> 0 <= smallest_index.unwrap() < i as int, + smallest_index.is_some() ==> nodes@[smallest_index.unwrap() as int] + == smallest_even.unwrap(), + smallest_even.is_some() ==> smallest_even.unwrap() % 2 == 0, + smallest_even.is_some() ==> forall|j: int| + 0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j], + smallest_index.is_some() ==> forall|j: int| + 0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j] + > smallest_even.unwrap(), + smallest_index.is_none() ==> forall|j: int| 0 <= j < i ==> nodes@[j] % 2 != 0, { - reveal_with_fuel(Seq::filter, 5); - reveal_with_fuel(Seq::min_via, 5); - proof { mapped = mapped.push((i as int, nodes[i as int])); } - // assert(mapped.len() == i + 1 as int); - // assert(mapped.subrange(0, i+1 as int).drop_last() =~= mapped.subrange(0, i as int)); - // assert(nodes@.subrange(0, i+1 as int).drop_last() =~= nodes@.subrange(0, i as int)); - assert(mapped.index(i as int).1 == nodes[i as int]); - if (nodes[i] % 2 == 0) { - proof { filtered = filtered.push((i as int, nodes[i as int])); } - if (ret.len() == 0 || nodes[i] < ret[0]) { - ret = vec![nodes[i], i]; - } + if nodes[i] % 2 == 0 && (smallest_even.is_none() || nodes[i] < smallest_even.unwrap()) { + smallest_even = Some(nodes[i]); + smallest_index = Some((i as u32)); } } - assert(nodes@.subrange(0, nodes.len() as int) =~= nodes@); - ret + if smallest_index.is_none() { + Vec::new() + } else { + vec![smallest_even.unwrap(), smallest_index.unwrap()] + } } } // verus! From 5a17b657a415abeb6002a490534ce9659d5fe292 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 09:30:37 +0530 Subject: [PATCH 14/41] complete 74 (total match) and overflow checks in 76 (is_simple_power) --- tasks/human_eval_074.rs | 49 ++++++++++++++++++++++++++++++++++++++++- tasks/human_eval_076.rs | 37 +++++++++++++++++++++++++++++-- 2 files changed, 83 insertions(+), 3 deletions(-) diff --git a/tasks/human_eval_074.rs b/tasks/human_eval_074.rs index eeaaecf..b5ea33c 100644 --- a/tasks/human_eval_074.rs +++ b/tasks/human_eval_074.rs @@ -9,7 +9,54 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn total_match<'a>(lst1: Vec<&'a str>, lst2: Vec<&'a str>) -> (ret: Option>) + ensures + ret.is_some() ==> ret.unwrap() == if lst1@.map_values(|s: &str| s@.len()).fold_left( + 0, + |x: int, y| x + y, + ) <= lst2@.map_values(|s: &str| s@.len()).fold_left(0, |x: int, y| x + y) { + lst1 + } else { + lst2 + }, +{ + let mut l1: usize = 0; + for i in 0..lst1.len() + invariant + l1 == lst1@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( + 0, + |x: int, y| x + y, + ), + // i <= lst1.len(), + { + l1 = l1.checked_add(lst1[i].unicode_len())?; + assert(lst1@.subrange(0, i + 1).map_values(|s: &str| s@.len()).drop_last() + == lst1@.subrange(0, i as int).map_values(|s: &str| s@.len())); + } + assert(lst1@ == lst1@.subrange(0, lst1.len() as int)); + + let mut l2: usize = 0; + for i in 0..lst2.len() + invariant + l2 == lst2@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( + 0, + |x: int, y| x + y, + ), + { + let x = lst2[i].unicode_len(); + assert(x == lst2[i as int]@.len()); + l2 = l2.checked_add(x)?; + assert(lst2@.subrange(0, i + 1).map_values(|s: &str| s@.len()).drop_last() + == lst2@.subrange(0, i as int).map_values(|s: &str| s@.len())); + } + assert(lst2@ == lst2@.subrange(0, lst2.len() as int)); + + if l1 <= l2 { + Some(lst1) + } else { + Some(lst2) + } +} } // verus! fn main() {} diff --git a/tasks/human_eval_076.rs b/tasks/human_eval_076.rs index 3a5559e..04a2586 100644 --- a/tasks/human_eval_076.rs +++ b/tasks/human_eval_076.rs @@ -5,11 +5,44 @@ HumanEval/76 /* ### VERUS BEGIN */ +use vstd::arithmetic::logarithm::log; +use vstd::arithmetic::power::pow; use vstd::prelude::*; - verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn is_simple_power(x: u32, n: u32) -> (ret: bool) + requires + n > 1, + ensures + ret <==> x == pow(n as int, log(n as int, x as int) as nat), +{ + let maybe_x = n.checked_pow(x.ilog(n)); + if (maybe_x.is_some() && maybe_x.unwrap() == x) { + true + } else { + false + } +} + +// note that the order of paramters is reverse in exec fn ilog and spec fn log +#[verifier::external_fn_specification] +pub fn ex_ilog(x: u32, base: u32) -> (ret: u32) + requires + base > 1, + ensures + ret == log(base as int, x as int), +{ + x.ilog(base) +} + +#[verifier::external_fn_specification] +pub fn ex_checked_pow(x: u32, exp: u32) -> (ret: Option) + ensures + ret.is_some() <==> ret.unwrap() == pow(x as int, exp as nat), + ret.is_none() <==> pow(x as int, exp as nat) > u32::MAX, +{ + x.checked_pow(exp) +} } // verus! fn main() {} From 78e532d825a6eeed6c6ca6e5f2957e2c5dd60c8e Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 09:37:21 +0530 Subject: [PATCH 15/41] undo programs 54 and 66 --- tasks/human_eval_054.rs | 20 +------------ tasks/human_eval_066.rs | 63 ----------------------------------------- 2 files changed, 1 insertion(+), 82 deletions(-) diff --git a/tasks/human_eval_054.rs b/tasks/human_eval_054.rs index d44b7d7..1c44e12 100644 --- a/tasks/human_eval_054.rs +++ b/tasks/human_eval_054.rs @@ -5,29 +5,11 @@ HumanEval/54 /* ### VERUS BEGIN */ -use std::collections::BTreeSet; -use std::collections::HashSet; use vstd::prelude::*; verus! { -// fn str_to_set(s: &str) -> HashSet { -// s.chars().collect() -// } -fn same_chars(left: &str, right: &str) -> (res: bool) - ensures - res <==> left@.to_set() =~= right@.to_set(), -{ - left.chars().collect::>().eq(&right.chars().collect::>()) -} - -#[verifier::external_fn_specification] -proof fn lemma_set_eq(left: BTreeSet, right: BTreeSet) - ensures - left.eq(right) ==> left@ =~= right@, -{ - admit(); -} +// TODO: Put your solution (the specification, implementation, and proof) to the task here } // verus! fn main() {} diff --git a/tasks/human_eval_066.rs b/tasks/human_eval_066.rs index ad73fbf..6021409 100644 --- a/tasks/human_eval_066.rs +++ b/tasks/human_eval_066.rs @@ -11,69 +11,6 @@ verus! { // TODO: Put your solution (the specification, implementation, and proof) to the task here -fn toLower(c: char) -> (ret: char) - // requires - // c.is_ascii(), - ensures 'A' <= c <= 'Z' ==> ret as u32 == add(c as u32, 32u32), - c < 'A' || c > 'Z' ==> ret == c -{ - if ('A' <= c && c <= 'Z') { - char::from_u32(c as u32 + 32).unwrap() - } else { - c - } -} - -// pub fn upper_sum_rec(s: &str) -> u64 -// ensures upper_sum_rec(s) >= 0 -// { -// if s.len() == 0 { -// 0 -// } else { -// let remaining = upper_sum_rec(&s[1..]); -// to_int(s.chars().next().unwrap()) as u64 + remaining -// } -// } - -// pub proof fn upper_sum_rec_prop(s: &str) -// requires s.len() > 0, -// ensures upper_sum_rec(s) == upper_sum_rec(&s[..s.len()-1]) + to_int(s.chars().nth(s.len()-1).unwrap()) as u64 -// { -// if s.len() > 1 { -// assert(s[1..][..s[1..].len() - 1] == s[1..s.len() - 1]); -// } -// } - -// pub fn to_int(c: char) -> u8 -// ensures 'A' <= c <= 'Z' ==> to_int(c) == c as u8, -// c < 'A' || c > 'Z' ==> to_int(c) == 0 -// { -// if 'A' <= c && c <= 'Z' { c as u8 } else { 0 } -// } - -// pub fn upper_sum(s: &str) -> (res: u64) -// ensures res == upper_sum_rec(s) -// { -// let mut res = 0; -// let mut i = 0; -// while i < s.len() -// invariant -// 0 <= i && i <= s.len(), -// res == upper_sum_rec(&s[..i]) -// { -// res = res + to_int(s.chars().nth(i).unwrap()) as u64; -// proof { -// assert(upper_sum_rec(&s[..i+1]) == upper_sum_rec(&s[..i]) + to_int(s.chars().nth(i).unwrap()) as u64); -// assert(s[..i+1][..i] == s[..i]); -// upper_sum_rec_prop(&s[..i+1]); -// } -// i = i + 1; -// } -// proof { -// assert(s == &s[..s.len()]); -// } -// res -// } } // verus! fn main() {} From d4f9075a8898766365b33ca27c38b81e68a4eee3 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 10:31:47 +0530 Subject: [PATCH 16/41] fix lint --- tasks/human_eval_072.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tasks/human_eval_072.rs b/tasks/human_eval_072.rs index 6b42855..ca938cc 100644 --- a/tasks/human_eval_072.rs +++ b/tasks/human_eval_072.rs @@ -123,7 +123,7 @@ proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int) decreases j - i, { if (i < j) { - assert (spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { + assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1)); } lemma_increasing_sum_params(s, i, j - 1); From 5eea4f95950fdc8bd3a3c6e0dd6690abe0100323 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Tue, 17 Sep 2024 13:10:49 +0530 Subject: [PATCH 17/41] complete filter_by_substring (007) --- tasks/human_eval_007.rs | 96 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 95 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs index b8ba40c..c580ab4 100644 --- a/tasks/human_eval_007.rs +++ b/tasks/human_eval_007.rs @@ -9,7 +9,101 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) + ensures + res@.len() <= strings@.len(), + forall|s: &str| res@.contains(s) ==> strings@.contains(s), + forall|s: &str| + res@.contains(s) ==> exists|i: int| + 0 <= i <= s@.len() - substring@.len() && s@.subrange( + i, + #[trigger] (i + substring@.len()), + ) == substring@, +{ + let mut res = Vec::new(); + let mut i: usize = 0; + + for i in 0..strings.len() + invariant + 0 <= i && i <= strings@.len(), + res@.len() <= i, + forall|s: &str| res@.contains(s) ==> strings@.contains(s), + forall|s: &str| + res@.contains(s) ==> exists|i: int| + 0 <= i <= s@.len() - substring@.len() && s@.subrange( + i, + #[trigger] (i + substring@.len()), + ) == substring@, + { + if check_substring(strings[i], substring) { + let ghost res_old = res; + res.push(strings[i]); + + assert(res@.last() == strings[i as int]); + assert(res@.drop_last() == res_old@); + assert(forall|s: &str| + res@.contains(s) <==> res_old@.contains(s) || s == strings[i as int]); + } + } + res +} + +fn check_substring(s: &str, sub: &str) -> (result: bool) + ensures + result <==> exists|i: int| + 0 <= i <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@, +{ + let s_len = s.unicode_len(); + let sub_len = sub.unicode_len(); + if (s_len < sub_len) { + return false; + } + if sub_len == 0 { + assert(s@.subrange(0, (0 + sub@.len()) as int) == sub@); + return true; + } + for i in 0..s_len - sub_len + 1 + invariant + forall|j: int| 0 <= j < i ==> s@.subrange(j, #[trigger] (j + sub@.len())) != sub@, + i <= s_len - sub_len + 1, + sub_len == sub@.len() <= s_len == s@.len(), + sub_len > 0, + { + if string_eq(sub, s.substring_char(i, i + sub_len)) { + assert(0 <= i <= s@.len() - sub@.len()); + assert(s@.subrange(i as int, i + sub@.len()) == sub@); + return true; + } + } + false +} + +fn string_eq(s1: &str, s2: &str) -> (result: bool) + ensures + result <==> s1@ == s2@, +{ + let s1_len = s1.unicode_len(); + let s2_len = s2.unicode_len(); + if s1_len != s2_len { + return false; + } + for i in 0..s1_len + invariant + s1@.subrange(0, i as int) =~= s2@.subrange(0, i as int), + i <= s1_len == s2_len == s1@.len() == s2@.len(), + { + let c = s1.get_char(i); + if c != s2.get_char(i) { + return false; + } + assert(s1@.subrange(0, i + 1) == s1@.subrange(0, i as int).push(c)); + assert(s1@.subrange(0, i as int).push(c) == s2@.subrange(0, i as int).push(c)); + assert(s2@.subrange(0, i as int).push(c) == s2@.subrange(0, i + 1)); + } + assert(s1@ == s1@.subrange(0, s1_len as int)); + assert(s2@ == s2@.subrange(0, s2_len as int)); + true +} } // verus! fn main() {} From 9f555fe3b8df63b36edcd272407d5141c6a4f44f Mon Sep 17 00:00:00 2001 From: WeetHet Date: Tue, 17 Sep 2024 13:16:28 +0300 Subject: [PATCH 18/41] task 12 --- tasks/human_eval_012.rs | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_012.rs b/tasks/human_eval_012.rs index 4a6722d..0f3ed4e 100644 --- a/tasks/human_eval_012.rs +++ b/tasks/human_eval_012.rs @@ -9,7 +9,42 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn longest(strings: &Vec>) -> (result: Option<&Vec>) + ensures + match result { + None => strings.len() == 0, + Some(s) => { + forall|i: int| + #![auto] + 0 <= i < strings.len() ==> s.len() >= strings[i].len() && exists|i: int| + #![auto] + (0 <= i < strings.len() && s == strings[i] && (forall|j: int| + #![auto] + 0 <= j < i ==> strings[j].len() < s.len())) + }, + }, +{ + if strings.len() == 0 { + return None; + } + let mut result: &Vec = &strings[0]; + let mut pos = 0; + + for i in 1..strings.len() + invariant + 0 <= pos < i, + result == &strings[pos as int], + exists|i: int| 0 <= i < strings.len() && strings[i] == result, + forall|j: int| #![auto] 0 <= j < i ==> strings[j].len() <= result.len(), + forall|j: int| #![auto] 0 <= j < pos ==> strings[j].len() < result.len(), + { + if result.len() < strings[i].len() { + result = &strings[i]; + pos = i; + } + } + Some(result) +} } // verus! fn main() {} From 0045f4952927d09f5a63be505835698a0e82e24e Mon Sep 17 00:00:00 2001 From: WeetHet Date: Tue, 17 Sep 2024 13:38:29 +0300 Subject: [PATCH 19/41] task 14 --- tasks/human_eval_014.rs | 49 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 48 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_014.rs b/tasks/human_eval_014.rs index 9d5d1e5..163dc94 100644 --- a/tasks/human_eval_014.rs +++ b/tasks/human_eval_014.rs @@ -9,7 +9,54 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +#[verifier::loop_isolation(false)] +fn all_prefixes(s: &Vec) -> (prefixes: Vec>) + ensures + prefixes.len() == s.len(), + forall|i: int| #![auto] 0 <= i < s.len() ==> prefixes[i]@ == s@.subrange(0, i + 1), +{ + let mut prefixes: Vec> = vec![]; + let mut prefix = vec![]; + assert(forall|i: int| + #![auto] + 0 <= i < prefix.len() ==> prefix@.index(i) == prefix@.subrange( + 0, + prefix.len() as int, + ).index(i)); + + assert(prefix@ == prefix@.subrange(0, 0)); + assert(forall|i: int| + #![auto] + 0 <= i < prefix.len() ==> prefix@.index(i) == s@.subrange(0, prefix.len() as int).index(i)); + assert(prefix@ == s@.subrange(0, 0)); + for i in 0..s.len() + invariant + prefixes.len() == i, + prefix.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> prefixes[j]@ == s@.subrange(0, j + 1), + prefix@ == s@.subrange(0, i as int), + prefix@ == prefix@.subrange(0, i as int), + { + let ghost pre_prefix = prefix; + prefix.push(s[i]); + assert(pre_prefix@.subrange(0, i as int) == pre_prefix@ && prefix@.subrange(0, i as int) + == pre_prefix@.subrange(0, i as int)); + assert(prefix@.subrange(0, i as int) == s@.subrange(0, i as int)); + assert(prefix[i as int] == s@.subrange(0, i + 1).index(i as int)); + + assert(forall|j: int| + #![auto] + 0 <= j < i + 1 ==> prefix@.index(j) == prefix@.subrange(0, (i + 1) as int).index(j)); + assert(prefix@ == prefix@.subrange(0, (i + 1) as int)); + assert(forall|j: int| + #![auto] + 0 <= j < i + 1 ==> prefix@.index(j) == s@.subrange(0, (i + 1) as int).index(j)); + assert(prefix@ == s@.subrange(0, (i + 1) as int)); + + prefixes.push(prefix.clone()); + } + return prefixes; +} } // verus! fn main() {} From 370682097955b7fde98fac3988e6135a0aa22c54 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Tue, 17 Sep 2024 13:41:30 +0300 Subject: [PATCH 20/41] remove loop_isolation(false) from 14 --- tasks/human_eval_014.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tasks/human_eval_014.rs b/tasks/human_eval_014.rs index 163dc94..ae23a14 100644 --- a/tasks/human_eval_014.rs +++ b/tasks/human_eval_014.rs @@ -9,7 +9,6 @@ use vstd::prelude::*; verus! { -#[verifier::loop_isolation(false)] fn all_prefixes(s: &Vec) -> (prefixes: Vec>) ensures prefixes.len() == s.len(), From 424c6c2e8b4f1c34407532742a70bd8a8219d767 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 18 Sep 2024 10:55:56 +0530 Subject: [PATCH 21/41] sort functions in topological order --- tasks/human_eval_007.rs | 100 +++++++++++++++---------------- tasks/human_eval_070.rs | 118 ++++++++++++++++++------------------ tasks/human_eval_072.rs | 126 +++++++++++++++++++-------------------- tasks/human_eval_075.rs | 58 +++++++++--------- tasks/human_eval_076.rs | 28 ++++----- tasks/human_eval_077.rs | 128 ++++++++++++++++++++-------------------- 6 files changed, 279 insertions(+), 279 deletions(-) diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs index c580ab4..4ff1cc4 100644 --- a/tasks/human_eval_007.rs +++ b/tasks/human_eval_007.rs @@ -9,43 +9,31 @@ use vstd::prelude::*; verus! { -fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) +fn string_eq(s1: &str, s2: &str) -> (result: bool) ensures - res@.len() <= strings@.len(), - forall|s: &str| res@.contains(s) ==> strings@.contains(s), - forall|s: &str| - res@.contains(s) ==> exists|i: int| - 0 <= i <= s@.len() - substring@.len() && s@.subrange( - i, - #[trigger] (i + substring@.len()), - ) == substring@, + result <==> s1@ == s2@, { - let mut res = Vec::new(); - let mut i: usize = 0; - - for i in 0..strings.len() + let s1_len = s1.unicode_len(); + let s2_len = s2.unicode_len(); + if s1_len != s2_len { + return false; + } + for i in 0..s1_len invariant - 0 <= i && i <= strings@.len(), - res@.len() <= i, - forall|s: &str| res@.contains(s) ==> strings@.contains(s), - forall|s: &str| - res@.contains(s) ==> exists|i: int| - 0 <= i <= s@.len() - substring@.len() && s@.subrange( - i, - #[trigger] (i + substring@.len()), - ) == substring@, + s1@.subrange(0, i as int) =~= s2@.subrange(0, i as int), + i <= s1_len == s2_len == s1@.len() == s2@.len(), { - if check_substring(strings[i], substring) { - let ghost res_old = res; - res.push(strings[i]); - - assert(res@.last() == strings[i as int]); - assert(res@.drop_last() == res_old@); - assert(forall|s: &str| - res@.contains(s) <==> res_old@.contains(s) || s == strings[i as int]); + let c = s1.get_char(i); + if c != s2.get_char(i) { + return false; } + assert(s1@.subrange(0, i + 1) == s1@.subrange(0, i as int).push(c)); + assert(s1@.subrange(0, i as int).push(c) == s2@.subrange(0, i as int).push(c)); + assert(s2@.subrange(0, i as int).push(c) == s2@.subrange(0, i + 1)); } - res + assert(s1@ == s1@.subrange(0, s1_len as int)); + assert(s2@ == s2@.subrange(0, s2_len as int)); + true } fn check_substring(s: &str, sub: &str) -> (result: bool) @@ -78,31 +66,43 @@ fn check_substring(s: &str, sub: &str) -> (result: bool) false } -fn string_eq(s1: &str, s2: &str) -> (result: bool) +fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) ensures - result <==> s1@ == s2@, + res@.len() <= strings@.len(), + forall|s: &str| res@.contains(s) ==> strings@.contains(s), + forall|s: &str| + res@.contains(s) ==> exists|i: int| + 0 <= i <= s@.len() - substring@.len() && s@.subrange( + i, + #[trigger] (i + substring@.len()), + ) == substring@, { - let s1_len = s1.unicode_len(); - let s2_len = s2.unicode_len(); - if s1_len != s2_len { - return false; - } - for i in 0..s1_len + let mut res = Vec::new(); + let mut i: usize = 0; + + for i in 0..strings.len() invariant - s1@.subrange(0, i as int) =~= s2@.subrange(0, i as int), - i <= s1_len == s2_len == s1@.len() == s2@.len(), + 0 <= i && i <= strings@.len(), + res@.len() <= i, + forall|s: &str| res@.contains(s) ==> strings@.contains(s), + forall|s: &str| + res@.contains(s) ==> exists|i: int| + 0 <= i <= s@.len() - substring@.len() && s@.subrange( + i, + #[trigger] (i + substring@.len()), + ) == substring@, { - let c = s1.get_char(i); - if c != s2.get_char(i) { - return false; + if check_substring(strings[i], substring) { + let ghost res_old = res; + res.push(strings[i]); + + assert(res@.last() == strings[i as int]); + assert(res@.drop_last() == res_old@); + assert(forall|s: &str| + res@.contains(s) <==> res_old@.contains(s) || s == strings[i as int]); } - assert(s1@.subrange(0, i + 1) == s1@.subrange(0, i as int).push(c)); - assert(s1@.subrange(0, i as int).push(c) == s2@.subrange(0, i as int).push(c)); - assert(s2@.subrange(0, i as int).push(c) == s2@.subrange(0, i + 1)); } - assert(s1@ == s1@.subrange(0, s1_len as int)); - assert(s2@ == s2@.subrange(0, s2_len as int)); - true + res } } // verus! diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index ee3e757..a6b7851 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -9,50 +9,21 @@ use vstd::prelude::*; verus! { -// returns (sorted, strange). Also returning sorted solely to have access to it for writing postcondition -fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) - ensures - s@.to_multiset() == (ret.0)@.to_multiset(), - s@.len() == (ret.0)@.len() == (ret.1)@.len(), - forall|i: int| - 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), - forall|i: int| - 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index( - s@.len() - (i - 1) / 2 - 1, - ), -{ - let sorted = sort_seq(s); - let mut strange = Vec::new(); - let mut i: usize = 0; - while i < sorted.len() - invariant - i <= sorted.len() == s@.len(), - strange@.len() == i, - forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2), - forall|j: int| - 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index( - sorted@.len() - (j / 2) - 1, - ), - { - if i % 2 == 0 { - strange.push(sorted[i / 2]); - } else { - let r = (i - 1) / 2; - strange.push(sorted[s.len() - r - 1]); - } - i += 1; - } - (sorted, strange) -} - -fn strange_sort_list(s: &Vec) -> (ret: Vec) - ensures - s@.len() == ret@.len(), -{ - let (_, strange) = strange_sort_list_helper(s); - strange -} - +// #[verifier::external_body] +// // Helper lemma to prove that swapping two elements doesn't change the multiset +// proof fn swap_preserves_multiset(s: Seq, i: int, j: int) +// requires 0 <= i < s.len() && 0 <= j < s.len() +// ensures s.to_multiset() == s.update(i, s.index(j)).update(j, s.index(i)).to_multiset() +// { +// let s_new = s.update(i, s.index(j)).update(j, s.index(i)); +// assert(s.to_multiset().count(s.index(i)) == s_new.to_multiset().count(s.index(i))); +// assert(s.to_multiset().count(s.index(j)) == s_new.to_multiset().count(s.index(j))); +// assert forall|x: int| s.to_multiset().count(x) == s_new.to_multiset().count(x) by { +// if x != s.index(i) && x != s.index(j) { +// assert(s.to_multiset().count(x) == s_new.to_multiset().count(x)); +// } +// } +// } fn sort_seq(s: &Vec) -> (ret: Vec) ensures forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), @@ -97,21 +68,50 @@ fn sort_seq(s: &Vec) -> (ret: Vec) sorted } -// #[verifier::external_body] -// // Helper lemma to prove that swapping two elements doesn't change the multiset -// proof fn swap_preserves_multiset(s: Seq, i: int, j: int) -// requires 0 <= i < s.len() && 0 <= j < s.len() -// ensures s.to_multiset() == s.update(i, s.index(j)).update(j, s.index(i)).to_multiset() -// { -// let s_new = s.update(i, s.index(j)).update(j, s.index(i)); -// assert(s.to_multiset().count(s.index(i)) == s_new.to_multiset().count(s.index(i))); -// assert(s.to_multiset().count(s.index(j)) == s_new.to_multiset().count(s.index(j))); -// assert forall|x: int| s.to_multiset().count(x) == s_new.to_multiset().count(x) by { -// if x != s.index(i) && x != s.index(j) { -// assert(s.to_multiset().count(x) == s_new.to_multiset().count(x)); -// } -// } -// } +// returns (sorted, strange). Also returning sorted solely to have access to it for writing postcondition +fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) + ensures + s@.to_multiset() == (ret.0)@.to_multiset(), + s@.len() == (ret.0)@.len() == (ret.1)@.len(), + forall|i: int| + 0 <= i < s@.len() && i % 2 == 0 ==> (ret.1)@.index(i) == (ret.0)@.index(i / 2), + forall|i: int| + 0 <= i < s@.len() && i % 2 == 1 ==> (ret.1)@.index(i) == (ret.0)@.index( + s@.len() - (i - 1) / 2 - 1, + ), +{ + let sorted = sort_seq(s); + let mut strange = Vec::new(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len() == s@.len(), + strange@.len() == i, + forall|j: int| 0 <= j < i && j % 2 == 0 ==> strange@.index(j) == sorted@.index(j / 2), + forall|j: int| + 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index( + sorted@.len() - (j / 2) - 1, + ), + { + if i % 2 == 0 { + strange.push(sorted[i / 2]); + } else { + let r = (i - 1) / 2; + strange.push(sorted[s.len() - r - 1]); + } + i += 1; + } + (sorted, strange) +} + +fn strange_sort_list(s: &Vec) -> (ret: Vec) + ensures + s@.len() == ret@.len(), +{ + let (_, strange) = strange_sort_list_helper(s); + strange +} + } // verus! fn main() {} diff --git a/tasks/human_eval_072.rs b/tasks/human_eval_072.rs index ca938cc..1429940 100644 --- a/tasks/human_eval_072.rs +++ b/tasks/human_eval_072.rs @@ -9,52 +9,39 @@ use vstd::prelude::*; verus! { -fn will_it_fly(qs: &Vec, w: u32) -> (ret: bool) +// i and j are ends of the subrange - exclusive +proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int) + requires + 0 <= i <= j <= s.len(), ensures - ret <==> qs@ =~= qs@.reverse() && spec_sum(qs@) <= w, + spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + decreases j - i, { - palindrome(qs) && sum_lesser_than_limit(qs, w) + if (i < j) { + assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { + assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1)); + } + lemma_increasing_sum_params(s, i, j - 1); + } } -fn palindrome(qs: &Vec) -> (ret: bool) +proof fn lemma_increasing_sum(s: Seq) ensures - ret <==> qs@ =~= qs@.reverse(), + forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), { - let mut ret = true; - let mut i: usize = 0; - while i < qs.len() / 2 - invariant - i <= qs@.len() / 2, - ret <==> qs@.subrange(0, i as int) =~= qs@.subrange( - qs@.len() - i, - qs@.len() as int, - ).reverse(), - { - // reveal_with_fuel(Seq::reverse, 5); // VERUS BUG on uncomment. file issue - assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() - =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); - assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange( - qs@.len() - i, - qs@.len() as int, - ).reverse().push(qs@.index(qs@.len() - (i + 1)))); - if qs[i] != qs[qs.len() - i - 1] { - ret = false; - } - i += 1; - } - let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int); - let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int); - proof { - if (qs.len() % 2) == 1 { - assert(qs@ =~= fst_half + qs@.subrange( - (qs@.len() / 2) as int, - qs@.len() - qs@.len() / 2, - ) + snd_half); - } else { - assert(qs@ =~= fst_half + snd_half); + assert forall|i: int, j: int| + #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] + 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) by { + if (0 <= i <= j <= s.len()) { + lemma_increasing_sum_params(s, i, j); } } - ret +} + +spec fn spec_sum(s: Seq) -> int { + s.fold_left(0, |x: int, y| x + y) } fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) @@ -95,39 +82,52 @@ fn sum_lesser_than_limit(qs: &Vec, w: u32) -> (ret: bool) true } -spec fn spec_sum(s: Seq) -> int { - s.fold_left(0, |x: int, y| x + y) -} - -proof fn lemma_increasing_sum(s: Seq) +fn palindrome(qs: &Vec) -> (ret: bool) ensures - forall|i: int, j: int| - #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] - 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + ret <==> qs@ =~= qs@.reverse(), { - assert forall|i: int, j: int| - #![trigger spec_sum(s.subrange(0, i)), spec_sum(s.subrange(0, j))] - 0 <= i <= j <= s.len() ==> spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)) by { - if (0 <= i <= j <= s.len()) { - lemma_increasing_sum_params(s, i, j); + let mut ret = true; + let mut i: usize = 0; + while i < qs.len() / 2 + invariant + i <= qs@.len() / 2, + ret <==> qs@.subrange(0, i as int) =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse(), + { + // reveal_with_fuel(Seq::reverse, 5); // VERUS BUG on uncomment. file issue + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse().drop_last() + =~= qs@.subrange(qs@.len() - i, qs@.len() as int).reverse()); + assert(qs@.subrange(qs@.len() - (i + 1), qs@.len() as int).reverse() =~= qs@.subrange( + qs@.len() - i, + qs@.len() as int, + ).reverse().push(qs@.index(qs@.len() - (i + 1)))); + if qs[i] != qs[qs.len() - i - 1] { + ret = false; + } + i += 1; + } + let ghost fst_half = qs@.subrange(0, (qs@.len() / 2) as int); + let ghost snd_half = qs@.subrange(qs@.len() - qs@.len() / 2, qs@.len() as int); + proof { + if (qs.len() % 2) == 1 { + assert(qs@ =~= fst_half + qs@.subrange( + (qs@.len() / 2) as int, + qs@.len() - qs@.len() / 2, + ) + snd_half); + } else { + assert(qs@ =~= fst_half + snd_half); } } + ret } -// i and j are ends of the subrange - exclusive -proof fn lemma_increasing_sum_params(s: Seq, i: int, j: int) - requires - 0 <= i <= j <= s.len(), +fn will_it_fly(qs: &Vec, w: u32) -> (ret: bool) ensures - spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), - decreases j - i, + ret <==> qs@ =~= qs@.reverse() && spec_sum(qs@) <= w, { - if (i < j) { - assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { - assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1)); - } - lemma_increasing_sum_params(s, i, j - 1); - } + palindrome(qs) && sum_lesser_than_limit(qs, w) } } // verus! diff --git a/tasks/human_eval_075.rs b/tasks/human_eval_075.rs index 9984319..d20fb47 100644 --- a/tasks/human_eval_075.rs +++ b/tasks/human_eval_075.rs @@ -33,6 +33,35 @@ fn prime(p: u32) -> (ret: bool) true } +fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option) + ensures + ret.is_some() ==> ret.unwrap() == x * y * z, + ret.is_none() ==> x * y * z > u32::MAX, +{ + // x,y,z == 0 done separately to invoke lemma_mul_increases which requires x > 0 + if (x == 0 || y == 0 || z == 0) { + return Some(0); + } + assert(x > 0 && y > 0 && z > 0); + let prod2 = x.checked_mul(y); + if prod2.is_some() { + let prod3 = prod2.unwrap().checked_mul(z); + if prod3.is_some() { + let ans = prod3.unwrap(); + assert(ans == x * y * z); + Some(ans) + } else { + assert(x * y * z > u32::MAX); + None + } + } else { + broadcast use group_mul_properties; + + assert(x * y * z >= y * z); + None + } +} + fn is_multiply_prime(x: u32) -> (ans: bool) requires x > 1, @@ -97,35 +126,6 @@ fn is_multiply_prime(x: u32) -> (ans: bool) false } -fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option) - ensures - ret.is_some() ==> ret.unwrap() == x * y * z, - ret.is_none() ==> x * y * z > u32::MAX, -{ - // x,y,z == 0 done separately to invoke lemma_mul_increases which requires x > 0 - if (x == 0 || y == 0 || z == 0) { - return Some(0); - } - assert(x > 0 && y > 0 && z > 0); - let prod2 = x.checked_mul(y); - if prod2.is_some() { - let prod3 = prod2.unwrap().checked_mul(z); - if prod3.is_some() { - let ans = prod3.unwrap(); - assert(ans == x * y * z); - Some(ans) - } else { - assert(x * y * z > u32::MAX); - None - } - } else { - broadcast use group_mul_properties; - - assert(x * y * z >= y * z); - None - } -} - } // verus! fn main() {} diff --git a/tasks/human_eval_076.rs b/tasks/human_eval_076.rs index 04a2586..4804771 100644 --- a/tasks/human_eval_076.rs +++ b/tasks/human_eval_076.rs @@ -10,20 +10,6 @@ use vstd::arithmetic::power::pow; use vstd::prelude::*; verus! { -fn is_simple_power(x: u32, n: u32) -> (ret: bool) - requires - n > 1, - ensures - ret <==> x == pow(n as int, log(n as int, x as int) as nat), -{ - let maybe_x = n.checked_pow(x.ilog(n)); - if (maybe_x.is_some() && maybe_x.unwrap() == x) { - true - } else { - false - } -} - // note that the order of paramters is reverse in exec fn ilog and spec fn log #[verifier::external_fn_specification] pub fn ex_ilog(x: u32, base: u32) -> (ret: u32) @@ -44,6 +30,20 @@ pub fn ex_checked_pow(x: u32, exp: u32) -> (ret: Option) x.checked_pow(exp) } +fn is_simple_power(x: u32, n: u32) -> (ret: bool) + requires + n > 1, + ensures + ret <==> x == pow(n as int, log(n as int, x as int) as nat), +{ + let maybe_x = n.checked_pow(x.ilog(n)); + if (maybe_x.is_some() && maybe_x.unwrap() == x) { + true + } else { + false + } +} + } // verus! fn main() {} diff --git a/tasks/human_eval_077.rs b/tasks/human_eval_077.rs index 974b6d0..bcb8d8a 100644 --- a/tasks/human_eval_077.rs +++ b/tasks/human_eval_077.rs @@ -11,50 +11,42 @@ use vstd::prelude::*; verus! { -fn is_cube(x: i32) -> (ret: bool) - requires - x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 - +proof fn lemma_cube_increases_helper(i: int) ensures - ret <==> exists|i: int| 0 <= i && abs(x as int) == #[trigger] (i * i * i), + i >= 0 ==> (i * i * i) <= (i + 1) * (i + 1) * (i + 1), { - let x_abs = x.abs(); + broadcast use group_mul_properties; - // dealing with cases where the the cube is not greater than the number - if x_abs == 0 { - assert(abs(x as int) == 0 * 0 * 0); - return true; - } else if (x_abs == 1) { - assert(abs(x as int) == 1 * 1 * 1); - return true; + if (i > 0) { + assert((i + 1) * (i + 1) * (i + 1) == i * i * i + 3 * i * i + 3 * i + 1); + assert(i * i * i + 3 * i * i + 3 * i + 1 > i * i * i); } - assert(-1 > x || x > 1); - let mut i = 2; - while i < x_abs - invariant - forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j), - 2 <= i <= abs(x as int) == x_abs, - { - let prod = checked_cube(i); - if prod.is_some() && prod.unwrap() == x.abs() { - return true; - } - i += 1; +} + +proof fn lemma_cube_increases_params(i: int, j: int) + ensures + 0 <= i <= j ==> (i * i * i) <= (j * j * j), + decreases j - i, +{ + // base case + if (i == j) { } - assert(forall|j: int| 2 <= j ==> abs(x as int) != #[trigger] (j * j * j)) by { - assert(forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j)); + // inductive case + else if (i < j) { + lemma_cube_increases_params(i, j - 1); + lemma_cube_increases_helper(j - 1); - assert(forall|j: int| i <= j ==> abs(x as int) < #[trigger] (j * j * j)) by { - assert(abs(x as int) < #[trigger] (i * i * i)) by { - broadcast use group_mul_properties; + } +} - assert(i <= i * i <= i * i * i); - } - lemma_cube_increases(); - assert(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); - } +proof fn lemma_cube_increases() + ensures + forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j), +{ + assert forall|i: int, j: int| + 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j) by { + lemma_cube_increases_params(i, j); } - false } fn checked_cube(x: i32) -> (ret: Option) @@ -101,42 +93,50 @@ pub fn ex_abs(x: i32) -> (ret: i32) x.abs() } -proof fn lemma_cube_increases() - ensures - forall|i: int, j: int| 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j), -{ - assert forall|i: int, j: int| - 0 <= i <= j ==> #[trigger] (i * i * i) <= #[trigger] (j * j * j) by { - lemma_cube_increases_params(i, j); - } -} +fn is_cube(x: i32) -> (ret: bool) + requires + x != i32::MIN, // avoid overflow: -(i32::MIN) == (i32::MAX) + 1 -proof fn lemma_cube_increases_params(i: int, j: int) ensures - 0 <= i <= j ==> (i * i * i) <= (j * j * j), - decreases j - i, + ret <==> exists|i: int| 0 <= i && abs(x as int) == #[trigger] (i * i * i), { - // base case - if (i == j) { - } - // inductive case - else if (i < j) { - lemma_cube_increases_params(i, j - 1); - lemma_cube_increases_helper(j - 1); + let x_abs = x.abs(); + // dealing with cases where the the cube is not greater than the number + if x_abs == 0 { + assert(abs(x as int) == 0 * 0 * 0); + return true; + } else if (x_abs == 1) { + assert(abs(x as int) == 1 * 1 * 1); + return true; } -} + assert(-1 > x || x > 1); + let mut i = 2; + while i < x_abs + invariant + forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j), + 2 <= i <= abs(x as int) == x_abs, + { + let prod = checked_cube(i); + if prod.is_some() && prod.unwrap() == x.abs() { + return true; + } + i += 1; + } + assert(forall|j: int| 2 <= j ==> abs(x as int) != #[trigger] (j * j * j)) by { + assert(forall|j: int| 2 <= j < i ==> abs(x as int) != #[trigger] (j * j * j)); -proof fn lemma_cube_increases_helper(i: int) - ensures - i >= 0 ==> (i * i * i) <= (i + 1) * (i + 1) * (i + 1), -{ - broadcast use group_mul_properties; + assert(forall|j: int| i <= j ==> abs(x as int) < #[trigger] (j * j * j)) by { + assert(abs(x as int) < #[trigger] (i * i * i)) by { + broadcast use group_mul_properties; - if (i > 0) { - assert((i + 1) * (i + 1) * (i + 1) == i * i * i + 3 * i * i + 3 * i + 1); - assert(i * i * i + 3 * i * i + 3 * i + 1 > i * i * i); + assert(i <= i * i <= i * i * i); + } + lemma_cube_increases(); + assert(forall|j: int| i <= j ==> (i * i * i) <= #[trigger] (j * j * j)); + } } + false } } // verus! From bb0d95d1dc51ef277f400037e06b6ab90eb56055 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Wed, 18 Sep 2024 09:16:44 +0300 Subject: [PATCH 22/41] Parenthesize forall and exists --- tasks/human_eval_012.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/tasks/human_eval_012.rs b/tasks/human_eval_012.rs index 0f3ed4e..57ee646 100644 --- a/tasks/human_eval_012.rs +++ b/tasks/human_eval_012.rs @@ -14,13 +14,12 @@ fn longest(strings: &Vec>) -> (result: Option<&Vec>) match result { None => strings.len() == 0, Some(s) => { - forall|i: int| + (forall|i: int| #![auto] 0 <= i < strings.len() ==> s.len() >= strings[i].len()) + && (exists|i: int| #![auto] - 0 <= i < strings.len() ==> s.len() >= strings[i].len() && exists|i: int| + (0 <= i < strings.len() && s == strings[i] && (forall|j: int| #![auto] - (0 <= i < strings.len() && s == strings[i] && (forall|j: int| - #![auto] - 0 <= j < i ==> strings[j].len() < s.len())) + 0 <= j < i ==> strings[j].len() < s.len()))) }, }, { From fa8630acb3d37b9444b7c0d9cc5594d75c16b816 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Wed, 18 Sep 2024 13:21:16 +0300 Subject: [PATCH 23/41] Complete 037 --- tasks/human_eval_037.rs | 154 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 153 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_037.rs b/tasks/human_eval_037.rs index 99af6b8..f438baa 100644 --- a/tasks/human_eval_037.rs +++ b/tasks/human_eval_037.rs @@ -9,7 +9,159 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +// code taken from sort_third (033) +spec fn count(s: Seq, x: T) -> int + decreases s.len(), +{ + if s.len() == 0 { + 0 + } else { + count(s.skip(1), x) + if s[0] == x { + 1int + } else { + 0int + } + } +} + +// This function defines what it means for two sequences to be +// permutations of each other: for every value `x`, each of the two +// sequences has the same number of instances of `x`. +spec fn permutes(s1: Seq, s2: Seq) -> bool { + forall|x: T| count(s1, x) == count(s2, x) +} + +// This lemma establishes the effect of an `update` operation on the +// result of a `count`. That is, it gives a closed-form +// (non-recursive) description of what happens to `count(s, x)` when +// `s` is updated to `s.update(i, v)`. +proof fn lemma_update_effect_on_count(s: Seq, i: int, v: T, x: T) + requires + 0 <= i < s.len(), + ensures + count(s.update(i, v), x) == if v == x && s[i] != x { + count(s, x) + 1 + } else if v != x && s[i] == x { + count(s, x) - 1 + } else { + count(s, x) + }, + decreases s.len(), +{ + if s.len() == 0 { + return ; + } + if i == 0 { + assert(s.update(i, v) =~= seq![v] + s.skip(1)); + assert(s.update(i, v).skip(1) =~= s.skip(1)); + } else { + assert(s.update(i, v) =~= seq![s[0]] + s.skip(1).update(i - 1, v)); + assert(s.update(i, v).skip(1) =~= s.skip(1).update(i - 1, v)); + lemma_update_effect_on_count(s.skip(1), i - 1, v, x); + } +} + +// This lemma proves that if you swap elements `i` and `j` of sequence `s`, +// you get a permutation of `s`. +proof fn lemma_swapping_produces_a_permutation(s: Seq, i: int, j: int) + requires + 0 <= i < s.len(), + 0 <= j < s.len(), + ensures + permutes(s.update(i, s[j]).update(j, s[i]), s), +{ + assert forall|x: T| #[trigger] count(s.update(i, s[j]).update(j, s[i]), x) == count(s, x) by { + lemma_update_effect_on_count(s, i, s[j], x); + lemma_update_effect_on_count(s.update(i, s[j]), j, s[i], x); + } +} + +#[verifier::loop_isolation(false)] +fn sort_pred(l: Vec, p: Vec) -> (l_prime: Vec) + requires + l.len() == p.len(), + ensures + l_prime.len() == l.len(), + forall|i: int| 0 <= i < l.len() && !p[i] ==> l_prime[i] == l[i], + forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && p[i] && p[j] ==> l_prime[i] <= l_prime[j], + permutes(l_prime@, l@), +{ + let ghost old_l = l@; + let l_len = l.len(); + let mut pos_replace: usize = 0; + let mut l_prime: Vec = l; + while pos_replace < l_len + invariant + l_len == l.len() == l_prime.len(), + forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int, j: int| + #![auto] + 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i] <= l_prime[j], + { + if p[pos_replace] { + let mut pos_cur: usize = pos_replace; + let mut pos: usize = pos_replace; + while pos < l_len + invariant + l_len == l.len() == l_prime.len(), + pos_replace <= pos, + pos_replace <= pos_cur < l_len, + p[pos_replace as int], + p[pos_cur as int], + forall|i: int| 0 <= i < l_len && !p[i] ==> l_prime[i] == l[i], + permutes(l_prime@, l@), + forall|i: int| + #![auto] + pos_replace <= i < pos && p[i] ==> l_prime[pos_cur as int] <= l_prime[i], + forall|i: int, j: int| + #![auto] + 0 <= i < pos_replace && i < j < l_len && p[i] && p[j] ==> l_prime[i] + <= l_prime[j], + { + if p[pos] && l_prime[pos] < l_prime[pos_cur] { + pos_cur = pos; + } + pos = pos + 1; + } + proof { + lemma_swapping_produces_a_permutation(l_prime@, pos_replace as int, pos_cur as int); + } + let v1 = l_prime[pos_replace]; + let v2 = l_prime[pos_cur]; + l_prime.set(pos_replace, v2); + l_prime.set(pos_cur, v1); + } + pos_replace = pos_replace + 1; + } + l_prime +} + +#[verifier::loop_isolation(false)] +fn sort_even(l: Vec) -> (result: Vec) + ensures + l.len() == result.len(), + permutes(result@, l@), + forall|i: int| 0 <= i < l.len() && i % 2 == 1 ==> result[i] == l[i], + forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> result[i] <= result[j], +{ + let mut p: Vec = vec![]; + for i in 0..l.len() + invariant + p.len() == i, + forall|j: int| 0 <= j < i ==> p[j] == (j % 2 == 0), + { + p.push(i % 2 == 0); + } + assert(forall|i: int, j: int| + #![auto] + 0 <= i < j < l.len() && i % 2 == 0 && j % 2 == 0 ==> p[i] && p[j]); + sort_pred(l, p) +} } // verus! fn main() {} From e8e0164729b9de1855d9d8e29af95da0631f9c19 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 18 Sep 2024 17:24:16 +0530 Subject: [PATCH 24/41] complete 070 stange sorting without using any assume --- tasks/human_eval_070.rs | 84 ++++++++++++++++++++++++++++++++--------- 1 file changed, 67 insertions(+), 17 deletions(-) diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index a6b7851..6a2186b 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -6,24 +6,71 @@ HumanEval/70 ### VERUS BEGIN */ use vstd::prelude::*; +use vstd::seq_lib::lemma_multiset_commutative; +use vstd::calc; verus! { -// #[verifier::external_body] -// // Helper lemma to prove that swapping two elements doesn't change the multiset -// proof fn swap_preserves_multiset(s: Seq, i: int, j: int) -// requires 0 <= i < s.len() && 0 <= j < s.len() -// ensures s.to_multiset() == s.update(i, s.index(j)).update(j, s.index(i)).to_multiset() -// { -// let s_new = s.update(i, s.index(j)).update(j, s.index(i)); -// assert(s.to_multiset().count(s.index(i)) == s_new.to_multiset().count(s.index(i))); -// assert(s.to_multiset().count(s.index(j)) == s_new.to_multiset().count(s.index(j))); -// assert forall|x: int| s.to_multiset().count(x) == s_new.to_multiset().count(x) by { -// if x != s.index(i) && x != s.index(j) { -// assert(s.to_multiset().count(x) == s_new.to_multiset().count(x)); -// } -// } -// } +proof fn swap_preserves_multiset_helper(s: Seq, i: int, j: int) + requires + 0 <= i < j < s.len(), + ensures + (s.take(j+1)).to_multiset() =~= s.take(i).to_multiset().add(s.subrange(i + 1, j).to_multiset()).insert(s.index(j)).insert(s.index(i)), +{ + let fst = s.take(i); + let snd = s.subrange(i + 1, j); + + assert((s.take(j+1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add(snd.to_multiset().insert(s.index(j)))) by { + assert(s.take(i+1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { + fst.to_multiset_ensures(); + assert(fst.push(s.index(i)) =~= s.take(i+1)); + } + assert(s.subrange(i+1, j+1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { + snd.to_multiset_ensures(); + assert(snd.push(s.index(j)) =~= s.subrange(i+1, j+1)); + } + + lemma_multiset_commutative(s.take(i+1), s.subrange(i+1, j+1)); + assert (s.take(i+1) + s.subrange(i+1, j+1) =~= s.take(j+1) ); + } +} + +// Helper lemma to prove that swapping two elements doesn't change the multiset +proof fn swap_preserves_multiset(s1: Seq, s2: Seq, i: int, j: int) + requires + 0 <= i < j < s1.len() == s2.len(), + forall|x: int| 0 <= x < s1.len() && x != i && x != j ==> s1.index(x) == s2.index(x), + s1.index(i) == s2.index(j), + s1.index(j) == s2.index(i), + + ensures + s1.to_multiset() == s2.to_multiset(), +{ + calc! { + (==) + s1.to_multiset(); { + lemma_multiset_commutative(s1.take(j+1), s1.skip(j+1)); + assert(s1 =~= s1.take(j+1) + s1.skip(j+1)); + } + s1.take(j+1).to_multiset().add(s1.skip(j+1).to_multiset()); { + assert(s1.take(j+1).to_multiset() =~= s2.take(j+1).to_multiset()) by { + assert(s1.take(i) == s2.take(i)); + assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j))); + swap_preserves_multiset_helper(s1, i, j); + swap_preserves_multiset_helper(s2, i, j); + } + assert (s1.skip(j+1).to_multiset() =~= s2.skip(j+1).to_multiset()) by { + assert(s1.skip(j + 1) =~= s2.skip(j + 1)); + } + } + s2.take(j+1).to_multiset().add(s2.skip(j+1).to_multiset()); { + lemma_multiset_commutative(s2.take(j+1), s2.skip(j+1)); + assert(s2 =~= s2.take(j+1) + s2.skip(j+1)); + } + s2.to_multiset(); + } +} + fn sort_seq(s: &Vec) -> (ret: Vec) ensures forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), @@ -54,13 +101,16 @@ fn sort_seq(s: &Vec) -> (ret: Vec) j += 1; } if min_index != i { + let ghost old_sorted = sorted@; let curr_val = sorted[i]; let min_val = sorted[min_index]; sorted.set(i, min_val); + sorted.set(min_index, curr_val); + proof { - // swap_preserves_multiset(s@.map_values(|x| x as int), i as int, min_index as int); - assume(s@.to_multiset() == sorted@.to_multiset()); + swap_preserves_multiset(old_sorted, sorted@, i as int, min_index as int); + assert(old_sorted.to_multiset() =~= sorted@.to_multiset()); } } i += 1; From eec17a9b1c43b8c8e8690f3a5a280a00702b2e65 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Wed, 18 Sep 2024 15:08:41 +0300 Subject: [PATCH 25/41] Complete 034 (cvc5 only) --- tasks/human_eval_034.rs | 177 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 176 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_034.rs b/tasks/human_eval_034.rs index a7c6bdb..efa889d 100644 --- a/tasks/human_eval_034.rs +++ b/tasks/human_eval_034.rs @@ -5,11 +5,186 @@ HumanEval/34 /* ### VERUS BEGIN */ +use vstd::calc; use vstd::prelude::*; +use vstd::seq_lib::lemma_multiset_commutative; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +proof fn swap_preserves_multiset_helper(s: Seq, i: int, j: int) + requires + 0 <= i < j < s.len(), + ensures + (s.take(j + 1)).to_multiset() =~= s.take(i).to_multiset().add( + s.subrange(i + 1, j).to_multiset(), + ).insert(s.index(j)).insert(s.index(i)), +{ + let fst = s.take(i); + let snd = s.subrange(i + 1, j); + + assert((s.take(j + 1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add( + snd.to_multiset().insert(s.index(j)), + )) by { + assert(s.take(i + 1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { + fst.to_multiset_ensures(); + assert(fst.push(s.index(i)) =~= s.take(i + 1)); + } + assert(s.subrange(i + 1, j + 1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { + snd.to_multiset_ensures(); + assert(snd.push(s.index(j)) =~= s.subrange(i + 1, j + 1)); + } + lemma_multiset_commutative(s.take(i + 1), s.subrange(i + 1, j + 1)); + assert(s.take(i + 1) + s.subrange(i + 1, j + 1) =~= s.take(j + 1)); + } +} + +// Helper lemma to prove that swapping two elements doesn't change the multiset +proof fn swap_preserves_multiset(s1: Seq, s2: Seq, i: int, j: int) + requires + 0 <= i < j < s1.len() == s2.len(), + forall|x: int| 0 <= x < s1.len() && x != i && x != j ==> s1.index(x) == s2.index(x), + s1.index(i) == s2.index(j), + s1.index(j) == s2.index(i), + ensures + s1.to_multiset() == s2.to_multiset(), +{ + calc! { + (==) + s1.to_multiset(); { + lemma_multiset_commutative(s1.take(j + 1), s1.skip(j + 1)); + assert(s1 =~= s1.take(j + 1) + s1.skip(j + 1)); + } + s1.take(j + 1).to_multiset().add(s1.skip(j + 1).to_multiset()); { + assert(s1.take(j + 1).to_multiset() =~= s2.take(j + 1).to_multiset()) by { + assert(s1.take(i) == s2.take(i)); + assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j))); + swap_preserves_multiset_helper(s1, i, j); + swap_preserves_multiset_helper(s2, i, j); + } + assert(s1.skip(j + 1).to_multiset() =~= s2.skip(j + 1).to_multiset()) by { + assert(s1.skip(j + 1) =~= s2.skip(j + 1)); + } + } + s2.take(j + 1).to_multiset().add(s2.skip(j + 1).to_multiset()); { + lemma_multiset_commutative(s2.take(j + 1), s2.skip(j + 1)); + assert(s2 =~= s2.take(j + 1) + s2.skip(j + 1)); + } + s2.to_multiset(); + } +} + +fn sort_seq(s: &Vec) -> (ret: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < ret@.len() ==> ret@.index(i) <= ret@.index(j), + ret@.len() == s@.len(), + s@.to_multiset() == ret@.to_multiset(), +{ + let mut sorted = s.clone(); + let mut i: usize = 0; + while i < sorted.len() + invariant + i <= sorted.len(), + forall|j: int, k: int| 0 <= j < k < i ==> sorted@.index(j) <= sorted@.index(k), + s@.to_multiset() == sorted@.to_multiset(), + forall|j: int, k: int| + 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), + sorted@.len() == s@.len(), + { + let mut min_index: usize = i; + let mut j: usize = i + 1; + while j < sorted.len() + invariant + i <= min_index < j <= sorted.len(), + forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), + { + if sorted[j] < sorted[min_index] { + min_index = j; + } + j += 1; + } + if min_index != i { + let ghost old_sorted = sorted@; + let curr_val = sorted[i]; + let min_val = sorted[min_index]; + sorted.set(i, min_val); + + sorted.set(min_index, curr_val); + + proof { + swap_preserves_multiset(old_sorted, sorted@, i as int, min_index as int); + assert(old_sorted.to_multiset() =~= sorted@.to_multiset()); + } + } + i += 1; + } + sorted +} + +fn unique_sorted(s: Vec) -> (result: Vec) + requires + forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j], + ensures + forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j], + forall|i: int| #![auto] 0 <= i < result.len() ==> s@.contains(result[i]), + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]), +{ + let mut result: Vec = vec![]; + for i in 0..s.len() + invariant + forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j], + forall|k: int, l: int| 0 <= k < l < result.len() ==> result[k] < result[l], + forall|k: int| + #![trigger result[k]] + 0 <= k < result.len() ==> (exists|m: int| 0 <= m < i && result[k] == s[m]), + forall|m: int| #![trigger s[m]] 0 <= m < i ==> result@.contains(s[m]), + { + let ghost pre = result; + if result.len() == 0 || result[result.len() - 1] != s[i] { + assert(result.len() == 0 || result[result.len() - 1] < s[i as int]); + result.push(s[i]); + } + assert(forall|m: int| + #![trigger result@[m], pre@[m]] + 0 <= m < pre.len() ==> pre@.contains(result@[m]) ==> result@.contains(pre@[m])) by { + assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]); + } + assert(forall|m: int| + #![trigger s@[m]] + 0 <= m < i ==> pre@.contains(s[m]) && result@.contains(s[m])); + assert(result@.contains(s[i as int])) by { + assert(result[result.len() - 1] == s[i as int]); + } + } + result +} + +fn unique(s: Vec) -> (result: Vec) + ensures + forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j], + forall|i: int| #![auto] 0 <= i < result.len() ==> s@.contains(result[i]), + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]), +{ + let sorted = sort_seq(&s); + assert(forall|i: int| #![auto] 0 <= i < sorted.len() ==> s@.contains(sorted[i])) by { + assert(forall|i: int| + #![auto] + 0 <= i < sorted.len() ==> sorted@.to_multiset().contains(sorted[i])) by { + sorted@.to_multiset_ensures(); + } + assert(forall|i: int| + #![auto] + 0 <= i < sorted.len() ==> s@.to_multiset().contains(sorted[i])); + s@.to_multiset_ensures(); + } + assert(forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> sorted@.contains(s[i])) by { + assert(forall|i: int| #![auto] 0 <= i < s.len() ==> s@.to_multiset().contains(s[i])) by { + s@.to_multiset_ensures(); + } + assert(forall|i: int| #![auto] 0 <= i < s.len() ==> sorted@.to_multiset().contains(s[i])); + sorted@.to_multiset_ensures(); + } + unique_sorted(sorted) +} } // verus! fn main() {} From d96a82b98872e26b5008e9a25941d7dfe45d13c5 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 18 Sep 2024 17:45:09 +0530 Subject: [PATCH 26/41] fix lint --- tasks/human_eval_070.rs | 44 +++++++++++++++++++++-------------------- 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index 6a2186b..fa688ab 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -5,67 +5,69 @@ HumanEval/70 /* ### VERUS BEGIN */ +use vstd::calc; use vstd::prelude::*; use vstd::seq_lib::lemma_multiset_commutative; -use vstd::calc; verus! { proof fn swap_preserves_multiset_helper(s: Seq, i: int, j: int) - requires + requires 0 <= i < j < s.len(), ensures - (s.take(j+1)).to_multiset() =~= s.take(i).to_multiset().add(s.subrange(i + 1, j).to_multiset()).insert(s.index(j)).insert(s.index(i)), + (s.take(j + 1)).to_multiset() =~= s.take(i).to_multiset().add( + s.subrange(i + 1, j).to_multiset(), + ).insert(s.index(j)).insert(s.index(i)), { let fst = s.take(i); let snd = s.subrange(i + 1, j); - assert((s.take(j+1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add(snd.to_multiset().insert(s.index(j)))) by { - assert(s.take(i+1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { + assert((s.take(j + 1)).to_multiset() =~= fst.to_multiset().insert(s.index(i)).add( + snd.to_multiset().insert(s.index(j)), + )) by { + assert(s.take(i + 1).to_multiset() =~= fst.to_multiset().insert(s.index(i))) by { fst.to_multiset_ensures(); - assert(fst.push(s.index(i)) =~= s.take(i+1)); + assert(fst.push(s.index(i)) =~= s.take(i + 1)); } - assert(s.subrange(i+1, j+1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { + assert(s.subrange(i + 1, j + 1).to_multiset() =~= snd.to_multiset().insert(s.index(j))) by { snd.to_multiset_ensures(); - assert(snd.push(s.index(j)) =~= s.subrange(i+1, j+1)); + assert(snd.push(s.index(j)) =~= s.subrange(i + 1, j + 1)); } - - lemma_multiset_commutative(s.take(i+1), s.subrange(i+1, j+1)); - assert (s.take(i+1) + s.subrange(i+1, j+1) =~= s.take(j+1) ); + lemma_multiset_commutative(s.take(i + 1), s.subrange(i + 1, j + 1)); + assert(s.take(i + 1) + s.subrange(i + 1, j + 1) =~= s.take(j + 1)); } } // Helper lemma to prove that swapping two elements doesn't change the multiset proof fn swap_preserves_multiset(s1: Seq, s2: Seq, i: int, j: int) - requires + requires 0 <= i < j < s1.len() == s2.len(), forall|x: int| 0 <= x < s1.len() && x != i && x != j ==> s1.index(x) == s2.index(x), s1.index(i) == s2.index(j), s1.index(j) == s2.index(i), - ensures s1.to_multiset() == s2.to_multiset(), { calc! { (==) s1.to_multiset(); { - lemma_multiset_commutative(s1.take(j+1), s1.skip(j+1)); - assert(s1 =~= s1.take(j+1) + s1.skip(j+1)); + lemma_multiset_commutative(s1.take(j + 1), s1.skip(j + 1)); + assert(s1 =~= s1.take(j + 1) + s1.skip(j + 1)); } - s1.take(j+1).to_multiset().add(s1.skip(j+1).to_multiset()); { - assert(s1.take(j+1).to_multiset() =~= s2.take(j+1).to_multiset()) by { + s1.take(j + 1).to_multiset().add(s1.skip(j + 1).to_multiset()); { + assert(s1.take(j + 1).to_multiset() =~= s2.take(j + 1).to_multiset()) by { assert(s1.take(i) == s2.take(i)); assert(s1.subrange(i + 1, j) =~= (s2.subrange(i + 1, j))); swap_preserves_multiset_helper(s1, i, j); swap_preserves_multiset_helper(s2, i, j); } - assert (s1.skip(j+1).to_multiset() =~= s2.skip(j+1).to_multiset()) by { + assert(s1.skip(j + 1).to_multiset() =~= s2.skip(j + 1).to_multiset()) by { assert(s1.skip(j + 1) =~= s2.skip(j + 1)); } } - s2.take(j+1).to_multiset().add(s2.skip(j+1).to_multiset()); { - lemma_multiset_commutative(s2.take(j+1), s2.skip(j+1)); - assert(s2 =~= s2.take(j+1) + s2.skip(j+1)); + s2.take(j + 1).to_multiset().add(s2.skip(j + 1).to_multiset()); { + lemma_multiset_commutative(s2.take(j + 1), s2.skip(j + 1)); + assert(s2 =~= s2.take(j + 1) + s2.skip(j + 1)); } s2.to_multiset(); } From 5d57ec3b4014bdfcdbda0ff069f1079750509dd0 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Wed, 18 Sep 2024 17:47:49 +0530 Subject: [PATCH 27/41] complete 134: check if last char is a letter --- tasks/human_eval_134.rs | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_134.rs b/tasks/human_eval_134.rs index f0a371a..e3ea285 100644 --- a/tasks/human_eval_134.rs +++ b/tasks/human_eval_134.rs @@ -9,7 +9,39 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +pub spec fn is_alphabetic(c: char) -> (result: bool); + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(is_alphabetic)] +pub fn ex_is_alphabetic(c: char) -> (result: bool) + ensures + result <==> (c.is_alphabetic()), +{ + c.is_alphabetic() +} + +pub spec fn is_whitespace(c: char) -> (result: bool); + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(is_whitespace)] +pub fn ex_is_whitespace(c: char) -> (result: bool) + ensures + result <==> (c.is_whitespace()), +{ + c.is_whitespace() +} + +fn check_if_last_char_is_a_letter(txt: &str) -> (result: bool) + ensures + result <==> (txt@.len() > 0 && txt@.last().is_alphabetic() && (txt@.len() == 1 + || txt@.index(txt@.len() - 2).is_whitespace())), +{ + let len = txt.unicode_len(); + if len == 0 { + return false; + } + txt.get_char(len - 1).is_alphabetic() && (len == 1 || txt.get_char(len - 2).is_whitespace()) +} } // verus! fn main() {} From 9ba1d3f222bea6a648eb912ef73533a24d4a8b03 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 19 Sep 2024 08:24:15 +0530 Subject: [PATCH 28/41] update spec for 007 and 074 --- tasks/human_eval_007.rs | 42 +++++++----------- tasks/human_eval_068.rs | 17 +++---- tasks/human_eval_074.rs | 98 +++++++++++++++++++++++++++-------------- tasks/human_eval_076.rs | 8 ++-- 4 files changed, 94 insertions(+), 71 deletions(-) diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs index 4ff1cc4..ae97a9a 100644 --- a/tasks/human_eval_007.rs +++ b/tasks/human_eval_007.rs @@ -68,38 +68,28 @@ fn check_substring(s: &str, sub: &str) -> (result: bool) fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) ensures - res@.len() <= strings@.len(), - forall|s: &str| res@.contains(s) ==> strings@.contains(s), - forall|s: &str| - res@.contains(s) ==> exists|i: int| - 0 <= i <= s@.len() - substring@.len() && s@.subrange( - i, - #[trigger] (i + substring@.len()), - ) == substring@, + forall|i: int| + 0 <= i < strings@.len() && (exists|j: int| + 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( + j, + #[trigger] (j + substring@.len()), + ) == substring@) ==> res@.contains(#[trigger] (strings[i])), { let mut res = Vec::new(); - let mut i: usize = 0; - - for i in 0..strings.len() + for n in 0..strings.len() invariant - 0 <= i && i <= strings@.len(), - res@.len() <= i, - forall|s: &str| res@.contains(s) ==> strings@.contains(s), - forall|s: &str| - res@.contains(s) ==> exists|i: int| - 0 <= i <= s@.len() - substring@.len() && s@.subrange( - i, - #[trigger] (i + substring@.len()), - ) == substring@, + forall|i: int| + 0 <= i < n && (exists|j: int| + 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( + j, + #[trigger] (j + substring@.len()), + ) == substring@) ==> res@.contains(#[trigger] (strings[i])), { - if check_substring(strings[i], substring) { + if check_substring(strings[n], substring) { let ghost res_old = res; - res.push(strings[i]); - - assert(res@.last() == strings[i as int]); + res.push(strings[n]); + assert(res@.last() == strings[n as int]); assert(res@.drop_last() == res_old@); - assert(forall|s: &str| - res@.contains(s) <==> res_old@.contains(s) || s == strings[i as int]); } } res diff --git a/tasks/human_eval_068.rs b/tasks/human_eval_068.rs index 8751cc5..2c35c9d 100644 --- a/tasks/human_eval_068.rs +++ b/tasks/human_eval_068.rs @@ -12,17 +12,18 @@ verus! { fn pluck_smallest_even(nodes: &Vec) -> (result: Vec) requires nodes@.len() <= u32::MAX, - forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] >= 0, ensures result@.len() == 0 || result@.len() == 2, - result@.len() == 2 ==> 0 <= result@[1] < nodes@.len() && nodes@[result@[1] as int] - == result@[0], - result@.len() == 2 ==> result@[0] % 2 == 0, - result@.len() == 2 ==> forall|i: int| - 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> result@[0] <= nodes@[i], - result@.len() == 2 ==> forall|i: int| - 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > result@[0], result@.len() == 0 ==> forall|i: int| 0 <= i < nodes@.len() ==> nodes@[i] % 2 != 0, + result@.len() == 2 ==> { + let node = result@[0]; + let index = result@[1]; + 0 <= index < nodes@.len() && nodes@[index as int] == node && node % 2 == 0 && forall| + i: int, + | + 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> node <= nodes@[i] && forall|i: int| + 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > node + }, { let mut smallest_even: Option = None; let mut smallest_index: Option = None; diff --git a/tasks/human_eval_074.rs b/tasks/human_eval_074.rs index b5ea33c..3e5c3f7 100644 --- a/tasks/human_eval_074.rs +++ b/tasks/human_eval_074.rs @@ -9,49 +9,83 @@ use vstd::prelude::*; verus! { -fn total_match<'a>(lst1: Vec<&'a str>, lst2: Vec<&'a str>) -> (ret: Option>) +spec fn spec_sum(s: Seq) -> int { + s.fold_left(0, |x: int, y| x + y) +} + +// i and j are ends of the subrange - exclusive +proof fn lemma_increasing_sum(s: Seq, i: int, j: int) + requires + 0 <= i <= j <= s.len(), ensures - ret.is_some() ==> ret.unwrap() == if lst1@.map_values(|s: &str| s@.len()).fold_left( - 0, - |x: int, y| x + y, - ) <= lst2@.map_values(|s: &str| s@.len()).fold_left(0, |x: int, y| x + y) { - lst1 - } else { - lst2 - }, + spec_sum(s.subrange(0, i)) <= spec_sum(s.subrange(0, j)), + decreases j - i, { - let mut l1: usize = 0; - for i in 0..lst1.len() - invariant - l1 == lst1@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( - 0, - |x: int, y| x + y, - ), - // i <= lst1.len(), - { - l1 = l1.checked_add(lst1[i].unicode_len())?; - assert(lst1@.subrange(0, i + 1).map_values(|s: &str| s@.len()).drop_last() - == lst1@.subrange(0, i as int).map_values(|s: &str| s@.len())); + if (i < j) { + assert(spec_sum(s.subrange(0, j - 1)) <= spec_sum(s.subrange(0, j))) by { + assert(s.subrange(0, j).drop_last() == s.subrange(0, j - 1)); + } + lemma_increasing_sum(s, i, j - 1); } - assert(lst1@ == lst1@.subrange(0, lst1.len() as int)); +} - let mut l2: usize = 0; - for i in 0..lst2.len() +spec fn total_str_len(strings: Seq<&str>) -> int { + spec_sum(strings.map_values(|s: &str| s@.len())) +} + +fn checked_total_str_len(lst: &Vec<&str>) -> (ret: Option) + ensures + ret.is_some() <==> total_str_len(lst@) <= usize::MAX, + ret.is_some() <==> ret.unwrap() == total_str_len(lst@), +{ + let ghost lens = Seq::::empty(); + let mut sum: usize = 0; + for i in 0..lst.len() invariant - l2 == lst2@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( + sum == lst@.subrange(0, i as int).map_values(|s: &str| s@.len()).fold_left( 0, |x: int, y| x + y, ), + spec_sum(lens) == sum, + lens =~= lst@.map_values(|s: &str| s@.len()).take(i as int), + lens =~= lst@.take(i as int).map_values(|s: &str| s@.len()), { - let x = lst2[i].unicode_len(); - assert(x == lst2[i as int]@.len()); - l2 = l2.checked_add(x)?; - assert(lst2@.subrange(0, i + 1).map_values(|s: &str| s@.len()).drop_last() - == lst2@.subrange(0, i as int).map_values(|s: &str| s@.len())); + let x = lst[i].unicode_len(); + proof { + assert(lens.push(x as nat).drop_last() == lens); + lens = lens.push(x as nat); + assert(lens =~= lst@.map_values(|s: &str| s@.len()).take(i + 1)); + + lemma_increasing_sum(lst@.map_values(|s: &str| s@.len()), i + 1, lst@.len() as int); + assert(total_str_len(lst@) >= spec_sum(lens)) by { + assert(lst@.map_values(|s: &str| s@.len()) =~= lst@.map_values( + |s: &str| s@.len(), + ).take(lst@.len() as int)); + } + if x + sum > usize::MAX { + assert(sum.checked_add(x).is_none()); + assert(total_str_len(lst@) > usize::MAX); + } + } + sum = sum.checked_add(x)?; + assert(lst@.take(i + 1).map_values(|s: &str| s@.len()).drop_last() == lst@.take( + i as int, + ).map_values(|s: &str| s@.len())); } - assert(lst2@ == lst2@.subrange(0, lst2.len() as int)); + assert(lst@ == lst@.subrange(0, lst.len() as int)); + return Some(sum); +} - if l1 <= l2 { +fn total_match<'a>(lst1: Vec<&'a str>, lst2: Vec<&'a str>) -> (ret: Option>) + ensures + ret.is_some() <== total_str_len(lst1@) <= usize::MAX && total_str_len(lst2@) <= usize::MAX, + ret.is_some() ==> ret.unwrap() == if total_str_len(lst1@) <= total_str_len(lst2@) { + lst1 + } else { + lst2 + }, +{ + if checked_total_str_len(&lst1)? <= checked_total_str_len(&lst2)? { Some(lst1) } else { Some(lst2) diff --git a/tasks/human_eval_076.rs b/tasks/human_eval_076.rs index 4804771..3d5ad48 100644 --- a/tasks/human_eval_076.rs +++ b/tasks/human_eval_076.rs @@ -14,6 +14,7 @@ verus! { #[verifier::external_fn_specification] pub fn ex_ilog(x: u32, base: u32) -> (ret: u32) requires + x > 0, base > 1, ensures ret == log(base as int, x as int), @@ -32,16 +33,13 @@ pub fn ex_checked_pow(x: u32, exp: u32) -> (ret: Option) fn is_simple_power(x: u32, n: u32) -> (ret: bool) requires + x > 0, n > 1, ensures ret <==> x == pow(n as int, log(n as int, x as int) as nat), { let maybe_x = n.checked_pow(x.ilog(n)); - if (maybe_x.is_some() && maybe_x.unwrap() == x) { - true - } else { - false - } + return maybe_x.is_some() && maybe_x.unwrap() == x; } } // verus! From ce762902d4bdbf6b6265642cb0f003d9b4d4a0d5 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 19 Sep 2024 11:42:08 +0530 Subject: [PATCH 29/41] complete task 073 --- tasks/human_eval_073.rs | 44 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_073.rs b/tasks/human_eval_073.rs index ba70ee6..59c2166 100644 --- a/tasks/human_eval_073.rs +++ b/tasks/human_eval_073.rs @@ -9,7 +9,49 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn zip_halves(v: Seq) -> (ret: Seq<(T, T)>) { + v.take((v.len() / 2) as int).zip_with(v.skip(((v.len() + 1) / 2) as int).reverse()) +} + +spec fn diff(s: Seq<(i32, i32)>) -> int { + s.fold_left( + 0, + |acc: int, x: (i32, i32)| + if (x.0 != x.1) { + acc + 1 + } else { + acc + }, + ) +} + +fn smallest_change(v: Vec) -> (change: usize) + requires + v@.len() < usize::MAX, + ensures + change == diff(zip_halves(v@)), +{ + let mut ans: usize = 0; + let ghost zipped = Seq::<(i32, i32)>::empty(); + for i in 0..v.len() / 2 + invariant + ans <= i <= v@.len() / 2 < usize::MAX, + ans == diff(zipped), + zipped =~= zip_halves(v@).take(i as int), + { + proof { + let ghost pair = (v[i as int], v[v.len() - i - 1]); + let ghost zipped_old = zipped; + zipped = zipped.push(pair); + assert(zipped.drop_last() =~= zipped_old); + } + if v[i] != v[v.len() - i - 1] { + ans += 1; + } + } + assert(zip_halves(v@).take((v@.len() / 2) as int) =~= zip_halves(v@)); + ans +} } // verus! fn main() {} From 61d0f6a3cca9849fe9ce415b653dae8c691b3326 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 09:35:42 +0300 Subject: [PATCH 30/41] Make 034 verify without cvc5 Co-authored-by: Bryan Parno --- tasks/human_eval_034.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tasks/human_eval_034.rs b/tasks/human_eval_034.rs index efa889d..4a5fe3e 100644 --- a/tasks/human_eval_034.rs +++ b/tasks/human_eval_034.rs @@ -8,6 +8,7 @@ HumanEval/34 use vstd::calc; use vstd::prelude::*; use vstd::seq_lib::lemma_multiset_commutative; +use vstd::seq_lib::lemma_seq_contains_after_push; verus! { @@ -142,15 +143,16 @@ fn unique_sorted(s: Vec) -> (result: Vec) if result.len() == 0 || result[result.len() - 1] != s[i] { assert(result.len() == 0 || result[result.len() - 1] < s[i as int]); result.push(s[i]); + assert forall|m: int| #![trigger s[m]] 0 <= m < i implies result@.contains(s[m]) by { + assert(pre@.contains(s@[m])); + lemma_seq_contains_after_push(pre@, s@[i as int], s@[m]); + }; } assert(forall|m: int| #![trigger result@[m], pre@[m]] 0 <= m < pre.len() ==> pre@.contains(result@[m]) ==> result@.contains(pre@[m])) by { assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]); } - assert(forall|m: int| - #![trigger s@[m]] - 0 <= m < i ==> pre@.contains(s[m]) && result@.contains(s[m])); assert(result@.contains(s[i as int])) by { assert(result[result.len() - 1] == s[i as int]); } From 1bb4040c66351813199b661c878ec878d597c2f7 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 09:44:55 +0300 Subject: [PATCH 31/41] Complete 035 --- tasks/human_eval_035.rs | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_035.rs b/tasks/human_eval_035.rs index db151d6..5b4a5d9 100644 --- a/tasks/human_eval_035.rs +++ b/tasks/human_eval_035.rs @@ -9,7 +9,25 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn max_element(a: &Vec) -> (max: i32) + requires + a.len() > 0, + ensures + forall|i: int| 0 <= i < a.len() ==> a[i] <= max, + exists|i: int| 0 <= i < a.len() && a[i] == max, +{ + let mut max = a[0]; + for i in 1..a.len() + invariant + forall|j: int| 0 <= j < i ==> a[j] <= max, + exists|j: int| 0 <= j < i && a[j] == max, + { + if a[i] > max { + max = a[i]; + } + } + max +} } // verus! fn main() {} From 696cdd61bbe5a9126040f58a19523ca8cc8a7e62 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 09:55:30 +0300 Subject: [PATCH 32/41] Complete 043 --- tasks/human_eval_043.rs | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_043.rs b/tasks/human_eval_043.rs index 37830cc..1f9b572 100644 --- a/tasks/human_eval_043.rs +++ b/tasks/human_eval_043.rs @@ -9,7 +9,40 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +#[verifier::loop_isolation(false)] +fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool) + requires + nums.len() >= 2, + forall|i: int, j: int| + 0 <= i < nums.len() && 0 <= j < nums.len() ==> nums[i] + nums[j] <= i32::MAX && nums[i] + + nums[j] >= i32::MIN, + ensures + found <==> exists|i: int, j: int| 0 <= i < j < nums.len() && nums[i] + nums[j] == target, +{ + let mut i = 0; + + while i < nums.len() + invariant + 0 <= i <= nums.len(), + forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + { + let mut j = i + 1; + while j < nums.len() + invariant + 0 <= i < j <= nums.len(), + forall|u: int, v: int| + 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + forall|u: int| i < u < j ==> nums[i as int] + nums[u] != target, + { + if nums[i] + nums[j] == target { + return true; + } + j = j + 1; + } + i = i + 1; + } + false +} } // verus! fn main() {} From f2012ef7578b482dd7ad3cde2686fbc909b69436 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 09:56:40 +0300 Subject: [PATCH 33/41] Relax restrictions a bit --- tasks/human_eval_043.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_043.rs b/tasks/human_eval_043.rs index 1f9b572..0fb47ae 100644 --- a/tasks/human_eval_043.rs +++ b/tasks/human_eval_043.rs @@ -14,8 +14,8 @@ fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool) requires nums.len() >= 2, forall|i: int, j: int| - 0 <= i < nums.len() && 0 <= j < nums.len() ==> nums[i] + nums[j] <= i32::MAX && nums[i] - + nums[j] >= i32::MIN, + 0 <= i < j < nums.len() ==> nums[i] + nums[j] <= i32::MAX && nums[i] + nums[j] + >= i32::MIN, ensures found <==> exists|i: int, j: int| 0 <= i < j < nums.len() && nums[i] + nums[j] == target, { From 28a3e270801b39aa698ef18e20d23d9aa5d23ad7 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 10:09:14 +0300 Subject: [PATCH 34/41] Complete 049 --- tasks/human_eval_049.rs | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_049.rs b/tasks/human_eval_049.rs index 3756e13..81321d9 100644 --- a/tasks/human_eval_049.rs +++ b/tasks/human_eval_049.rs @@ -9,7 +9,43 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn modp_rec(n: nat, p: nat) -> nat + decreases n, +{ + if n == 0 { + 1nat % p + } else { + (modp_rec((n - 1) as nat, p) * 2) % p + } +} + +fn modmul(a: u32, b: u32, p: u32) -> (mul: u32) + by (nonlinear_arith) + requires + p > 0, + ensures + mul == ((a as int) * (b as int)) % (p as int), +{ + (((a as u64) * (b as u64)) % (p as u64)) as u32 +} + +#[verifier::loop_isolation(false)] +fn modp(n: u32, p: u32) -> (r: u32) + by (nonlinear_arith) + requires + p > 0, + ensures + r == modp_rec(n as nat, p as nat), +{ + let mut r = 1u32 % p; + for i in 0..n + invariant + r == modp_rec(i as nat, p as nat), + { + r = modmul(r, 2, p); + } + r +} } // verus! fn main() {} From 29966f7e2b6285fe0c558ce5fdeba4aee5faf2b0 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 10:21:52 +0300 Subject: [PATCH 35/41] Complete 050 --- tasks/human_eval_050.rs | 91 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 90 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_050.rs b/tasks/human_eval_050.rs index 71023ab..c97fca3 100644 --- a/tasks/human_eval_050.rs +++ b/tasks/human_eval_050.rs @@ -9,7 +9,96 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn encode_char_spec(c: int) -> int + recommends + 65 <= c <= 90, +{ + (c - 65 + 5) % 26 + 65 +} + +fn encode_char(c: u8) -> (r: u8) + requires + 65 <= c <= 90, + ensures + r == encode_char_spec(c as int), + 65 <= r <= 90, +{ + (c - 65 + 5) % 26 + 65 +} + +spec fn decode_char_spec(c: int) -> int + recommends + 65 <= c <= 90, +{ + (c - 65 + 26 - 5) % 26 + 65 +} + +fn decode_char(c: u8) -> (r: u8) + requires + 65 <= c <= 90, + ensures + r == decode_char_spec(c as int), + 65 <= r <= 90, +{ + (c - 65 + 26 - 5) % 26 + 65 +} + +proof fn opposite_encode_decode(c: int) + requires + 65 <= c <= 90, + ensures + encode_char_spec(decode_char_spec(c)) == c, + decode_char_spec(encode_char_spec(c)) == c, +{ +} + +#[verifier::loop_isolation(false)] +fn encode_shift(s: &Vec) -> (t: Vec) + requires + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90, + ensures + s.len() == t.len(), + forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == encode_char_spec(s[i] as int), + forall|i: int| #![auto] 0 <= i < t.len() ==> decode_char_spec(t[i] as int) == s[i], +{ + let mut t: Vec = vec![]; + for i in 0..s.len() + invariant + t.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> t[j] == encode_char_spec(s[j] as int), + forall|j: int| #![auto] 0 <= j < i ==> decode_char_spec(t[j] as int) == s[j], + { + t.push(encode_char(s[i])); + proof { + opposite_encode_decode(s[i as int] as int); + } + } + t +} + +#[verifier::loop_isolation(false)] +fn decode_shift(s: &Vec) -> (t: Vec) + requires + forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> 65 <= s[i] <= 90, + ensures + s.len() == t.len(), + forall|i: int| #![auto] 0 <= i < t.len() ==> t[i] == decode_char_spec(s[i] as int), + forall|i: int| #![auto] 0 <= i < t.len() ==> encode_char_spec(t[i] as int) == s[i], +{ + let mut t: Vec = vec![]; + for i in 0..s.len() + invariant + t.len() == i, + forall|j: int| #![auto] 0 <= j < i ==> t[j] == decode_char_spec(s[j] as int), + forall|j: int| #![auto] 0 <= j < i ==> encode_char_spec(t[j] as int) == s[j], + { + t.push(decode_char(s[i])); + proof { + opposite_encode_decode(s[i as int] as int); + } + } + t +} } // verus! fn main() {} From 88df3fe32a00d1769c12ccc7a7f62b835de048ab Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 19 Sep 2024 13:56:59 +0530 Subject: [PATCH 36/41] complete 136 reformat 068 --- tasks/human_eval_068.rs | 26 ++++++++++++++------------ tasks/human_eval_136.rs | 40 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 53 insertions(+), 13 deletions(-) diff --git a/tasks/human_eval_068.rs b/tasks/human_eval_068.rs index 2c35c9d..d2e3e58 100644 --- a/tasks/human_eval_068.rs +++ b/tasks/human_eval_068.rs @@ -18,9 +18,10 @@ fn pluck_smallest_even(nodes: &Vec) -> (result: Vec) result@.len() == 2 ==> { let node = result@[0]; let index = result@[1]; - 0 <= index < nodes@.len() && nodes@[index as int] == node && node % 2 == 0 && forall| - i: int, - | + &&& 0 <= index < nodes@.len() + &&& nodes@[index as int] == node + &&& node % 2 == 0 + &&& forall|i: int| 0 <= i < nodes@.len() && nodes@[i] % 2 == 0 ==> node <= nodes@[i] && forall|i: int| 0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > node }, @@ -33,16 +34,17 @@ fn pluck_smallest_even(nodes: &Vec) -> (result: Vec) 0 <= i <= nodes@.len(), nodes@.len() <= u32::MAX, smallest_even.is_none() == smallest_index.is_none(), - smallest_index.is_some() ==> 0 <= smallest_index.unwrap() < i as int, - smallest_index.is_some() ==> nodes@[smallest_index.unwrap() as int] - == smallest_even.unwrap(), - smallest_even.is_some() ==> smallest_even.unwrap() % 2 == 0, - smallest_even.is_some() ==> forall|j: int| - 0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j], - smallest_index.is_some() ==> forall|j: int| - 0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j] - > smallest_even.unwrap(), smallest_index.is_none() ==> forall|j: int| 0 <= j < i ==> nodes@[j] % 2 != 0, + smallest_index.is_some() ==> { + &&& 0 <= smallest_index.unwrap() < i as int + &&& nodes@[smallest_index.unwrap() as int] == smallest_even.unwrap() + &&& smallest_even.unwrap() % 2 == 0 + &&& forall|j: int| + 0 <= j < i ==> nodes@[j] % 2 == 0 ==> smallest_even.unwrap() <= nodes@[j] + &&& forall|j: int| + 0 <= j < smallest_index.unwrap() ==> nodes@[j] % 2 != 0 || nodes@[j] + > smallest_even.unwrap() + }, { if nodes[i] % 2 == 0 && (smallest_even.is_none() || nodes[i] < smallest_even.unwrap()) { smallest_even = Some(nodes[i]); diff --git a/tasks/human_eval_136.rs b/tasks/human_eval_136.rs index 04fda7e..bbe9d57 100644 --- a/tasks/human_eval_136.rs +++ b/tasks/human_eval_136.rs @@ -9,7 +9,45 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +fn largest_smallest_integers(arr: &Vec) -> (res: (Option, Option)) + ensures + ({ + let a = res.0; + let b = res.1; + &&& a.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] >= 0 + &&& a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0 + &&& a.is_some() ==> forall|i: int| + 0 <= i < arr@.len() && arr@[i] < 0 ==> arr@[i] <= a.unwrap() + &&& b.is_none() ==> forall|i: int| 0 <= i < arr@.len() ==> arr@[i] <= 0 + &&& b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0 + &&& b.is_some() ==> forall|i: int| + 0 <= i < arr@.len() && arr@[i] > 0 ==> arr@[i] >= b.unwrap() + }), +{ + let mut i: usize = 0; + let mut a = None; + let mut b = None; + + while i < arr.len() + invariant + 0 <= i <= arr@.len(), + a.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] >= 0, + a.is_some() ==> arr@.contains(a.unwrap()) && a.unwrap() < 0, + a.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] < 0 ==> arr@[j] <= a.unwrap(), + b.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] <= 0, + b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0, + b.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] > 0 ==> arr@[j] >= b.unwrap(), + { + if arr[i] < 0 && (a.is_none() || arr[i] >= a.unwrap()) { + a = Some(arr[i]); + } + if arr[i] > 0 && (b.is_none() || arr[i] <= b.unwrap()) { + b = Some(arr[i]); + } + i = i + 1; + } + (a, b) +} } // verus! fn main() {} From b6d0d2207b3bb96bb1b3b4b8bac0575c682e7e9f Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 12:01:01 +0300 Subject: [PATCH 37/41] Complete 054 --- tasks/human_eval_054.rs | 83 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 82 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_054.rs b/tasks/human_eval_054.rs index 1c44e12..e894030 100644 --- a/tasks/human_eval_054.rs +++ b/tasks/human_eval_054.rs @@ -5,11 +5,92 @@ HumanEval/54 /* ### VERUS BEGIN */ +use vstd::hash_set::HashSetWithView; use vstd::prelude::*; +use vstd::std_specs::hash::axiom_u8_obeys_hash_table_key_model; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +broadcast use axiom_u8_obeys_hash_table_key_model; + +fn hash_set_from(s: &Vec) -> (res: HashSetWithView) + ensures + forall|i: int| #![auto] 0 <= i < s.len() ==> res@.contains(s[i]), + forall|x: int| + 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> #[trigger] s@.contains(x as u8), +{ + let mut res: HashSetWithView = HashSetWithView::new(); + for i in 0..s.len() + invariant + forall|j: int| #![auto] 0 <= j < i ==> res@.contains(s[j]), + forall|x: int| + 0 <= x < 256 ==> #[trigger] res@.contains(x as u8) ==> (exists|j: int| + 0 <= j < i && s[j] == x), + { + res.insert(s[i]); + } + res +} + +proof fn implies_contains(s0: Seq, s1: Seq, hs1: Set) + requires + forall|i: int| #![trigger s0[i]] 0 <= i < s0.len() ==> 0 <= s0[i] < 256, + forall|x: int| + 0 <= x < 256 ==> #[trigger] hs1.contains(x as u8) ==> #[trigger] s1.contains(x as u8), + ensures + forall|i: int| + #![auto] + 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) ==> s1.contains(s0[i]), +{ + assert forall|i: int| + #![auto] + 0 <= i < s0.len() && 0 <= s0[i] < 256 && hs1.contains(s0[i]) implies s1.contains(s0[i]) by { + let x = s0[i]; + assert(0 <= x < 256); + assert(hs1.contains(x as u8)); + assert(s1.contains(x as u8)); + }; +} + +#[verifier::loop_isolation(false)] +fn same_chars(s0: &Vec, s1: &Vec) -> (same: bool) + ensures + same <==> (forall|i: int| #![auto] 0 <= i < s0.len() ==> s1@.contains(s0[i])) && (forall| + i: int, + | + #![auto] + 0 <= i < s1.len() ==> s0@.contains(s1[i])), +{ + let hs0 = hash_set_from(s0); + let hs1 = hash_set_from(s1); + + proof { + implies_contains(s0@, s1@, hs1@); + implies_contains(s1@, s0@, hs0@); + } + + let mut contains_s0 = true; + for i in 0..s0.len() + invariant + contains_s0 <==> forall|j: int| #![auto] 0 <= j < i ==> s1@.contains(s0[j]), + { + if !hs1.contains(&s0[i]) { + contains_s0 = false; + assert(!s1@.contains(s0[i as int])); + } + } + let mut contains_s1 = true; + for i in 0..s1.len() + invariant + contains_s1 <==> forall|j: int| #![auto] 0 <= j < i ==> s0@.contains(s1[j]), + { + if !hs0.contains(&s1[i]) { + contains_s1 = false; + assert(!s0@.contains(s1[i as int])); + } + } + contains_s0 && contains_s1 +} } // verus! fn main() {} From 6751f5d3c7d8ddeaeeac38a1a68f8366c12f7d0a Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 12:23:57 +0300 Subject: [PATCH 38/41] Complete 080 --- tasks/human_eval_080.rs | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/tasks/human_eval_080.rs b/tasks/human_eval_080.rs index 0185958..cdae840 100644 --- a/tasks/human_eval_080.rs +++ b/tasks/human_eval_080.rs @@ -9,7 +9,44 @@ use vstd::prelude::*; verus! { -// TODO: Put your solution (the specification, implementation, and proof) to the task here +spec fn three_distinct_spec(s: Seq, i: int) -> bool + recommends + 0 < i && i + 1 < s.len(), +{ + (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1]) +} + +fn three_distinct(s: &Vec, i: usize) -> (is: bool) + requires + 0 < i && i + 1 < s.len(), + ensures + is <==> three_distinct_spec(s@, i as int), +{ + (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1]) +} + +spec fn happy_spec(s: Seq) -> bool { + s.len() >= 3 && (forall|i: int| 0 < i && i + 1 < s.len() ==> three_distinct_spec(s, i)) +} + +#[verifier::loop_isolation(false)] +fn is_happy(s: &Vec) -> (happy: bool) + ensures + happy <==> happy_spec(s@), +{ + if s.len() < 3 { + return false; + } + for i in 1..(s.len() - 1) + invariant + forall|j: int| 0 < j < i ==> three_distinct_spec(s@, j), + { + if !three_distinct(s, i) { + return false; + } + } + return true; +} } // verus! fn main() {} From f7a7d839ee812a0620d569790baffd6eb17323db Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 23 Dec 2024 09:40:25 +0000 Subject: [PATCH 39/41] strengthen postcondition on 007 (substring filtering) --- tasks/human_eval_007.rs | 76 ++++++++++++++++++++++++++++++----------- 1 file changed, 57 insertions(+), 19 deletions(-) diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs index ae97a9a..845210b 100644 --- a/tasks/human_eval_007.rs +++ b/tasks/human_eval_007.rs @@ -36,10 +36,16 @@ fn string_eq(s1: &str, s2: &str) -> (result: bool) true } +spec fn is_subseq_of(s: Seq, sub: Seq) -> bool { + exists|i: int| 0 <= i <= s.len() - sub.len() && s.subrange(i, #[trigger] (i + sub.len())) == sub +} + fn check_substring(s: &str, sub: &str) -> (result: bool) ensures - result <==> exists|i: int| - 0 <= i <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@, + result <==> is_subseq_of(s@, sub@), +// exists|i: int| +// 0 <= i <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@, + { let s_len = s.unicode_len(); let sub_len = sub.unicode_len(); @@ -66,32 +72,64 @@ fn check_substring(s: &str, sub: &str) -> (result: bool) false } -fn filter_by_substring<'a>(strings: &Vec<&'a str>, substring: &str) -> (res: Vec<&'a str>) +fn filter_by_sub<'a>(strings: &Vec<&'a str>, sub: &str) -> (res: Vec<&'a str>) ensures - forall|i: int| - 0 <= i < strings@.len() && (exists|j: int| - 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( - j, - #[trigger] (j + substring@.len()), - ) == substring@) ==> res@.contains(#[trigger] (strings[i])), + strings@.filter(|s: &str| is_subseq_of(s@, sub@)) + == res@, +// forall|i: int| +// 0 <= i < strings@.len() && +// // strings@.filter (|s: &str| is_subseq_of(s@, sub@)) == res@ +// is_subseq_of(strings[i]@, sub@) ==> res@.contains( +// #[trigger] (strings[i]), +// ) && res@.contains(#[trigger] (strings[i])) ==> is_subseq_of(strings[i]@, sub@), + { let mut res = Vec::new(); + // assert (strings@.subrange(0, 0).filter (|s: &str| is_subseq_of(s@, sub@)) == res@); + assert(res@ == Seq::<&str>::empty()); + let mut n = 0; + // while n < strings.len() for n in 0..strings.len() invariant - forall|i: int| - 0 <= i < n && (exists|j: int| - 0 <= j <= strings@[i]@.len() - substring@.len() && strings[i]@.subrange( - j, - #[trigger] (j + substring@.len()), - ) == substring@) ==> res@.contains(#[trigger] (strings[i])), + // n < strings.len(), + // forall|i: int| + // 0 <= i < n && is_subseq_of(strings[i]@, sub@) ==> res@.contains( + // #[trigger] (strings[i]), + // ), + + strings@.subrange(0, n as int).filter(|s: &str| is_subseq_of(s@, sub@)) == res@, + n <= strings.len(), { - if check_substring(strings[n], substring) { - let ghost res_old = res; + reveal(Seq::filter); + assert(strings@.subrange(0, n as int + 1).drop_last() == strings@.subrange(0, n as int)); + if check_substring(strings[n], sub) { + // let ghost res_old = res@; + // let ghost filtered_sub = strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)); + // let ghost pred = |s: &str| is_subseq_of(s@, sub@); + // let ghost last = ran.last(); + // assert (last@ == strings[n as int]@); + // let ghost ra = ran.drop_last(); + // assert(ra.push(last) == ran); + // assert (ra == strings@.subrange(0, n as int)); + // assert (pred(last)); + // let ghost ran_f = ran.filter(pred); + // let ghost ra_f = ra.filter(pred); + // assert(ra_f == res@); + // assert(ra_f.push(last) == ran_f); + // assert (ran.filter (|s: &str| is_subseq_of(s@, sub@)).last()@ == ran.last()@); res.push(strings[n]); - assert(res@.last() == strings[n as int]); - assert(res@.drop_last() == res_old@); + // assert (ran_f == res@); + // assert(res@.last() == strings[n as int]); + // assert (strings[n as int] == strings@.subrange(0, n as int + 1).last()); + // assert (res_old == filtered_sub); + // assert (strings[n as int] == strings@.subrange(0, n as int + 1).filter (|s: &str| is_subseq_of(s@, sub@)).last()); + // assert (strings@.subrange(0, (n as int) + 1).filter (|s: &str| is_subseq_of(s@, sub@)) == strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)).push(strings[n as int])); + // assert(strings[n as int]@ == strings@.subrange(0, n + 1).filter(|s: &str| is_subseq_of(s@, sub@)).last()@); + // assert(res@.drop_last() == res_old); } } + assert(strings@.subrange(0, strings@.len() as int) == strings@); + // assert (strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)) == res@); res } From f9c2fad6a82a654c7c07c36b48d794e47f276ac2 Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Mon, 23 Dec 2024 09:45:22 +0000 Subject: [PATCH 40/41] remove commented proof code from 007 --- tasks/human_eval_007.rs | 44 +---------------------------------------- 1 file changed, 1 insertion(+), 43 deletions(-) diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs index 845210b..3922afa 100644 --- a/tasks/human_eval_007.rs +++ b/tasks/human_eval_007.rs @@ -43,9 +43,6 @@ spec fn is_subseq_of(s: Seq, sub: Seq) -> bool { fn check_substring(s: &str, sub: &str) -> (result: bool) ensures result <==> is_subseq_of(s@, sub@), -// exists|i: int| -// 0 <= i <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@, - { let s_len = s.unicode_len(); let sub_len = sub.unicode_len(); @@ -74,62 +71,23 @@ fn check_substring(s: &str, sub: &str) -> (result: bool) fn filter_by_sub<'a>(strings: &Vec<&'a str>, sub: &str) -> (res: Vec<&'a str>) ensures - strings@.filter(|s: &str| is_subseq_of(s@, sub@)) - == res@, -// forall|i: int| -// 0 <= i < strings@.len() && -// // strings@.filter (|s: &str| is_subseq_of(s@, sub@)) == res@ -// is_subseq_of(strings[i]@, sub@) ==> res@.contains( -// #[trigger] (strings[i]), -// ) && res@.contains(#[trigger] (strings[i])) ==> is_subseq_of(strings[i]@, sub@), - + strings@.filter(|s: &str| is_subseq_of(s@, sub@)) == res@, { let mut res = Vec::new(); - // assert (strings@.subrange(0, 0).filter (|s: &str| is_subseq_of(s@, sub@)) == res@); assert(res@ == Seq::<&str>::empty()); let mut n = 0; - // while n < strings.len() for n in 0..strings.len() invariant - // n < strings.len(), - // forall|i: int| - // 0 <= i < n && is_subseq_of(strings[i]@, sub@) ==> res@.contains( - // #[trigger] (strings[i]), - // ), - strings@.subrange(0, n as int).filter(|s: &str| is_subseq_of(s@, sub@)) == res@, n <= strings.len(), { reveal(Seq::filter); assert(strings@.subrange(0, n as int + 1).drop_last() == strings@.subrange(0, n as int)); if check_substring(strings[n], sub) { - // let ghost res_old = res@; - // let ghost filtered_sub = strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)); - // let ghost pred = |s: &str| is_subseq_of(s@, sub@); - // let ghost last = ran.last(); - // assert (last@ == strings[n as int]@); - // let ghost ra = ran.drop_last(); - // assert(ra.push(last) == ran); - // assert (ra == strings@.subrange(0, n as int)); - // assert (pred(last)); - // let ghost ran_f = ran.filter(pred); - // let ghost ra_f = ra.filter(pred); - // assert(ra_f == res@); - // assert(ra_f.push(last) == ran_f); - // assert (ran.filter (|s: &str| is_subseq_of(s@, sub@)).last()@ == ran.last()@); res.push(strings[n]); - // assert (ran_f == res@); - // assert(res@.last() == strings[n as int]); - // assert (strings[n as int] == strings@.subrange(0, n as int + 1).last()); - // assert (res_old == filtered_sub); - // assert (strings[n as int] == strings@.subrange(0, n as int + 1).filter (|s: &str| is_subseq_of(s@, sub@)).last()); - // assert (strings@.subrange(0, (n as int) + 1).filter (|s: &str| is_subseq_of(s@, sub@)) == strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)).push(strings[n as int])); - // assert(strings[n as int]@ == strings@.subrange(0, n + 1).filter(|s: &str| is_subseq_of(s@, sub@)).last()@); - // assert(res@.drop_last() == res_old); } } assert(strings@.subrange(0, strings@.len() as int) == strings@); - // assert (strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)) == res@); res } From 4d5105382707f8696d133482c0d4e5ed3a9ff93c Mon Sep 17 00:00:00 2001 From: Edwin Fernando Date: Thu, 31 Jul 2025 17:53:00 +0200 Subject: [PATCH 41/41] fix while loops onow require a decreases clause --- tasks/human_eval_034.rs | 2 ++ tasks/human_eval_043.rs | 2 ++ tasks/human_eval_070.rs | 3 +++ tasks/human_eval_075.rs | 4 ++++ tasks/human_eval_134.rs | 4 ++-- tasks/human_eval_136.rs | 1 + 6 files changed, 14 insertions(+), 2 deletions(-) diff --git a/tasks/human_eval_034.rs b/tasks/human_eval_034.rs index 4a5fe3e..9d96386 100644 --- a/tasks/human_eval_034.rs +++ b/tasks/human_eval_034.rs @@ -90,6 +90,7 @@ fn sort_seq(s: &Vec) -> (ret: Vec) forall|j: int, k: int| 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), sorted@.len() == s@.len(), + decreases (sorted.len() - i), { let mut min_index: usize = i; let mut j: usize = i + 1; @@ -97,6 +98,7 @@ fn sort_seq(s: &Vec) -> (ret: Vec) invariant i <= min_index < j <= sorted.len(), forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), + decreases (sorted.len() - j), { if sorted[j] < sorted[min_index] { min_index = j; diff --git a/tasks/human_eval_043.rs b/tasks/human_eval_043.rs index 0fb47ae..e32fc3b 100644 --- a/tasks/human_eval_043.rs +++ b/tasks/human_eval_043.rs @@ -25,6 +25,7 @@ fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool) invariant 0 <= i <= nums.len(), forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, + decreases nums.len() - i, { let mut j = i + 1; while j < nums.len() @@ -33,6 +34,7 @@ fn pairs_sum_to_zero(nums: &[i32], target: i32) -> (found: bool) forall|u: int, v: int| 0 <= u < v < nums.len() && u < i ==> nums[u] + nums[v] != target, forall|u: int| i < u < j ==> nums[i as int] + nums[u] != target, + decreases nums.len() - j, { if nums[i] + nums[j] == target { return true; diff --git a/tasks/human_eval_070.rs b/tasks/human_eval_070.rs index fa688ab..3e5db36 100644 --- a/tasks/human_eval_070.rs +++ b/tasks/human_eval_070.rs @@ -89,6 +89,7 @@ fn sort_seq(s: &Vec) -> (ret: Vec) forall|j: int, k: int| 0 <= j < i <= k < sorted@.len() ==> sorted@.index(j) <= sorted@.index(k), sorted@.len() == s@.len(), + decreases sorted.len() - i, { let mut min_index: usize = i; let mut j: usize = i + 1; @@ -96,6 +97,7 @@ fn sort_seq(s: &Vec) -> (ret: Vec) invariant i <= min_index < j <= sorted.len(), forall|k: int| i <= k < j ==> sorted@.index(min_index as int) <= sorted@.index(k), + decreases sorted.len() - j, { if sorted[j] < sorted[min_index] { min_index = j; @@ -144,6 +146,7 @@ fn strange_sort_list_helper(s: &Vec) -> (ret: (Vec, Vec)) 0 < j < i && j % 2 == 1 ==> strange@.index(j) == sorted@.index( sorted@.len() - (j / 2) - 1, ), + decreases sorted.len() - i, { if i % 2 == 0 { strange.push(sorted[i / 2]); diff --git a/tasks/human_eval_075.rs b/tasks/human_eval_075.rs index d20fb47..dcbb5d6 100644 --- a/tasks/human_eval_075.rs +++ b/tasks/human_eval_075.rs @@ -40,6 +40,7 @@ fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option) { // x,y,z == 0 done separately to invoke lemma_mul_increases which requires x > 0 if (x == 0 || y == 0 || z == 0) { + assert(0 == x * y * z); return Some(0); } assert(x > 0 && y > 0 && z > 0); @@ -76,6 +77,7 @@ fn is_multiply_prime(x: u32) -> (ans: bool) (spec_prime(i) && spec_prime(j) && spec_prime(k) && i <= a && j <= x && k <= x) ==> x != i * j * k, a <= x, + decreases x - a, { a += 1; if prime(a) { @@ -88,6 +90,7 @@ fn is_multiply_prime(x: u32) -> (ans: bool) spec_prime(a as int), a <= x, b <= x, + decreases x - b, { b += 1; if prime(b) { @@ -100,6 +103,7 @@ fn is_multiply_prime(x: u32) -> (ans: bool) a <= x, b <= x, c <= x, + decreases x - c, { c += 1; let prod = checked_mul_thrice(a, b, c); diff --git a/tasks/human_eval_134.rs b/tasks/human_eval_134.rs index e3ea285..727ff34 100644 --- a/tasks/human_eval_134.rs +++ b/tasks/human_eval_134.rs @@ -9,7 +9,7 @@ use vstd::prelude::*; verus! { -pub spec fn is_alphabetic(c: char) -> (result: bool); +pub uninterp spec fn is_alphabetic(c: char) -> (result: bool); #[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_alphabetic)] @@ -20,7 +20,7 @@ pub fn ex_is_alphabetic(c: char) -> (result: bool) c.is_alphabetic() } -pub spec fn is_whitespace(c: char) -> (result: bool); +pub uninterp spec fn is_whitespace(c: char) -> (result: bool); #[verifier::external_fn_specification] #[verifier::when_used_as_spec(is_whitespace)] diff --git a/tasks/human_eval_136.rs b/tasks/human_eval_136.rs index bbe9d57..cd5c489 100644 --- a/tasks/human_eval_136.rs +++ b/tasks/human_eval_136.rs @@ -37,6 +37,7 @@ fn largest_smallest_integers(arr: &Vec) -> (res: (Option, Option) b.is_none() ==> forall|j: int| 0 <= j < i ==> arr@[j] <= 0, b.is_some() ==> arr@.contains(b.unwrap()) && b.unwrap() > 0, b.is_some() ==> forall|j: int| 0 <= j < i && arr@[j] > 0 ==> arr@[j] >= b.unwrap(), + decreases arr.len() - i, { if arr[i] < 0 && (a.is_none() || arr[i] >= a.unwrap()) { a = Some(arr[i]);