fix while loops onow require a decreases clause

Author: edwin1729

tasks/human_eval_034.rs

@@ -90,13 +90,15 @@ fn sort_seq(s: &Vec<i32>) -> (ret: Vec<i32>)
             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;
         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),
+            decreases (sorted.len() - j),
         {
             if sorted[j] < sorted[min_index] {
                 min_index = j;

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;

tasks/human_eval_070.rs

@@ -89,13 +89,15 @@ fn sort_seq(s: &Vec<i32>) -> (ret: Vec<i32>)
             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;
         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),
+            decreases sorted.len() - j,
         {
             if sorted[j] < sorted[min_index] {
                 min_index = j;
@@ -144,6 +146,7 @@ fn strange_sort_list_helper(s: &Vec<i32>) -> (ret: (Vec<i32>, Vec<i32>))
                 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]);

tasks/human_eval_075.rs

@@ -40,6 +40,7 @@ fn checked_mul_thrice(x: u32, y: u32, z: u32) -> (ret: Option<u32>)
 {
     // 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);

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)]

tasks/human_eval_136.rs

@@ -37,6 +37,7 @@ fn largest_smallest_integers(arr: &Vec<i32>) -> (res: (Option<i32>, Option<i32>)
             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]);