Restore existing tasks to a verifying state with the latest version of

parno · parno · commit a558d4e4caeb · 2025-08-11T15:54:43.000-07:00
Verus.  Largest change is adding decreases clauses.
diff --git a/tasks/human_eval_005.rs b/tasks/human_eval_005.rs
@@ -106,6 +106,7 @@ pub fn intersperse(numbers: Vec<u64>, delimiter: u64) -> (result: Vec<u64>)
                 result.len() == 2 * index,
                 forall|i: int| 0 <= i < index ==> #[trigger] result[even(i)] == numbers[i],
                 forall|i: int| 0 <= i < index ==> #[trigger] result[odd(i)] == delimiter,
+            decreases numbers.len() - 1 - index,
         {
             result.push(numbers[index]);
             result.push(delimiter);
diff --git a/tasks/human_eval_013.rs b/tasks/human_eval_013.rs
@@ -46,6 +46,7 @@ fn compute_gcd(a: u64, b: u64) -> (g: u64)
     loop
         invariant
             gcd(a1 as nat, b1 as nat) == gcd(a as nat, b as nat),
+        decreases b1,
     {
         if a1 == 0 {
             return b1;
diff --git a/tasks/human_eval_015.rs b/tasks/human_eval_015.rs
@@ -130,6 +130,7 @@ pub fn number_to_char_impl(n: u8) -> (char_vec: Vec<char>)
     while (i > 0)
         invariant
             number_to_char(n as nat) == number_to_char(i as nat).add(output@),
+        decreases i,
     {
         let m = i % 10;
         let current = single_digit_number_to_char_impl(m);
diff --git a/tasks/human_eval_024.rs b/tasks/human_eval_024.rs
@@ -13,7 +13,7 @@ use vstd::prelude::*;
 verus! {
 
 pub open spec fn mul(a: nat, b: nat) -> nat {
-    builtin::mul(a, b)
+    vstd::prelude::mul(a, b)
 }
 
 /// Specification for what it means for d to divide a
@@ -73,6 +73,7 @@ fn largest_divisor(n: u32) -> (ret: u32)
             n > 0,
             i < n,
             forall|k: u32| i < k < n ==> !divides(k as nat, n as nat),
+        decreases i,
     {
         if n % i == 0 {
             assert(divides(i as nat, n as nat)) by {
diff --git a/tasks/human_eval_025.rs b/tasks/human_eval_025.rs
@@ -326,6 +326,7 @@ pub fn factorize(n: u8) -> (factorization: Vec<u8>)
             forall|i: nat, j: nat|
                 (1 < i <= j < factorization.len()) ==> ((#[trigger] factorization[i as int] as nat)
                     <= (#[trigger] factorization[j as int] as nat) <= m),
+        decreases n + 2 - m, k,
     {
         if (k as u16 % m == 0) {
             assert(is_prime(m as nat)) by { lemma_first_divisor_is_prime(k as nat, m as nat) };
@@ -354,7 +355,10 @@ pub fn factorize(n: u8) -> (factorization: Vec<u8>)
             assert((k as int) == ((k as int) / (m as int)) * (m as int)) by {
                 lemma_fundamental_div_mod(k as int, m as int)
             };
-
+            proof { 
+                // Prove that we're still making progress towards termination
+                lemma_div_decreases(k as int, m as int);
+            }
             k = k / m as u8;
         } else {
             m = m + 1;
diff --git a/tasks/human_eval_026.rs b/tasks/human_eval_026.rs
@@ -37,6 +37,7 @@ fn count_frequency(elements: &Vec<i64>, key: i64) -> (frequency: usize)
             0 <= index <= elements.len(),
             0 <= counter <= index,
             count_frequency_spec(elements@.subrange(0, index as int), key) == counter,
+        decreases elements.len() - index,
     {
         if (elements[index] == key) {
             counter += 1;
diff --git a/tasks/human_eval_028.rs b/tasks/human_eval_028.rs
@@ -51,6 +51,7 @@ fn concatenate_impl(strings: Vec<Vec<char>>) -> (joined: Vec<char>)
                 strings.deep_view(),
                 i as nat,
             ),
+        decreases strings.len() - i,
     {
         assert(concatenate(strings.deep_view()) == joined@ + strings[i as int]@ + concat_helper(
             strings.deep_view(),
diff --git a/tasks/human_eval_031.rs b/tasks/human_eval_031.rs
@@ -46,6 +46,7 @@ fn is_prime_impl(n: u8) -> (res: bool)
         invariant
             2 <= k <= n,
             res == is_prime_so_far(n as nat, k as nat),
+        decreases n - k,
     {
         assert((is_prime_so_far(n as nat, k as nat) && (n as nat) % (k as nat) != 0)
             == is_prime_so_far(n as nat, (k + 1) as nat));
diff --git a/tasks/human_eval_033.rs b/tasks/human_eval_033.rs
@@ -103,6 +103,7 @@ fn sort_third(l: Vec<i32>) -> (l_prime: Vec<i32>)
             forall|i: int, j: int|
                 0 <= i < pos_being_set_to_smallest && i < j < l_len && i % 3 == 0 && j % 3 == 0
                     ==> l_prime[i] <= l_prime[j],
+        decreases l_len + 3 - pos_being_set_to_smallest,
     {
         // Iterate `pos_during_scan_for_smallest` by 3 from `pos_being_set_to_smallest`
         // to `l_len`. Keep track of the position of the smallest element found so far
@@ -125,6 +126,7 @@ fn sort_third(l: Vec<i32>) -> (l_prime: Vec<i32>)
                 forall|i: int, j: int|
                     0 <= i < pos_being_set_to_smallest && i < j < l_len && i % 3 == 0 && j % 3 == 0
                         ==> l_prime[i] <= l_prime[j],
+            decreases l_len + 3 - pos_during_scan_for_smallest,
         {
             if l_prime[pos_during_scan_for_smallest] < l_prime[pos_of_smallest_found_so_far] {
                 pos_of_smallest_found_so_far = pos_during_scan_for_smallest;
diff --git a/tasks/human_eval_055a.rs b/tasks/human_eval_055a.rs
@@ -45,6 +45,7 @@ fn fib(n: u32) -> (ret: Option<u32>)
             None => spec_fib(n as nat) > u32::MAX,
             Some(f) => f == spec_fib(n as nat),
         },
+    decreases n,
 {
     if n > 47 {
         proof {
diff --git a/tasks/human_eval_056.rs b/tasks/human_eval_056.rs
@@ -46,6 +46,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool)
             (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,
+        decreases brackets@.len() - i,
     {
         let c = brackets.get_char(i);
         let ghost prev = spec_bracketing_helper(brackets@.subrange(0, i as int));
diff --git a/tasks/human_eval_057.rs b/tasks/human_eval_057.rs
@@ -29,6 +29,7 @@ fn monotonic(l: Vec<i32>) -> (ret: bool)
                 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),
+        decreases l.len() - 1 - n,
     {
         if l[n] < l[n + 1] {
             decreasing = false;
diff --git a/tasks/human_eval_059.rs b/tasks/human_eval_059.rs
@@ -30,6 +30,7 @@ fn is_prime(num: u32) -> (result: bool)
         invariant
             2 <= i <= num,
             result <==> spec_prime_helper(num as int, i as int),
+        decreases num - i,
     {
         if num % i == 0 {
             result = false;
@@ -56,6 +57,7 @@ fn largest_prime_factor(n: u32) -> (largest: u32)
             spec_prime(largest as int),
             n % largest == 0,
             forall|p| 0 <= p <= j && spec_prime(p) && n as int % p == 0 ==> p <= largest,
+        decreases n - j,
     {
         j += 1;
         let flag = is_prime(j);
diff --git a/tasks/human_eval_060.rs b/tasks/human_eval_060.rs
@@ -70,6 +70,7 @@ fn sum_to_n(n: u32) -> (sum: Option<u32>)
             i <= n < 92682,
             res == spec_sum_to_n(i as nat),
             res <= u32::MAX,
+        decreases n - i,
     {
         i += 1;
         proof {
diff --git a/tasks/human_eval_061.rs b/tasks/human_eval_061.rs
@@ -46,6 +46,7 @@ fn correct_bracketing(brackets: &str) -> (ret: bool)
             (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,
+        decreases brackets@.len() - i,
     {
         let c = brackets.get_char(i);
         let ghost prev = spec_bracketing_helper(brackets@.subrange(0, i as int));
diff --git a/tasks/human_eval_062.rs b/tasks/human_eval_062.rs
@@ -28,6 +28,8 @@ fn derivative(xs: &Vec<u32>) -> (ret: Vec<u64>)
         invariant
             xs@.map(|i: int, x| i * x).subrange(1, i as int) =~= ret@.map_values(|x| x as int),
             1 <= i <= xs.len() <= u32::MAX,
+        decreases
+            xs.len() - i,
     {
         proof {
             // Prove that the multiplication does not overflow
@@ -37,8 +39,10 @@ fn derivative(xs: &Vec<u32>) -> (ret: Vec<u64>)
                 i as int,
                 u32::MAX as int,
             );
-            assert(u32::MAX * u32::MAX <= u64::MAX);
-            assert((i as u64) * (xs[i as int] as u64) == i as int * xs[i as int]);
+            assert((i as u64) * (xs[i as int] as u64) <= u64::MAX) by {
+                assert(u32::MAX * u32::MAX <= u64::MAX);
+                assert((i as u64) * (xs[i as int] as u64) == i as int * xs[i as int]);
+            }
         }
         ret.push((i as u64) * (xs[i] as u64));
 
diff --git a/tasks/human_eval_063.rs b/tasks/human_eval_063.rs
@@ -52,6 +52,7 @@ fn fibfib(x: u32) -> (ret: Option<u32>)
             None => spec_fibfib(x as nat) > u32::MAX,
             Some(f) => f == spec_fibfib(x as nat),
         },
+    decreases x,
 {
     if x > 39 {
         proof {
diff --git a/tasks/human_eval_066.rs b/tasks/human_eval_066.rs
@@ -45,6 +45,7 @@ fn digit_sum(text: &[char]) -> (sum: u128)
                     #[trigger] text@.subrange(0, j),
                 )) <= u64::MAX * index),
             u64::MIN * index <= sum <= u64::MAX * index,
+        decreases text@.len() - index,
     {
         if (text[index] >= 'A' && text[index] <= 'Z') {
             assert(text@.subrange(0, index as int) =~= text@.subrange(
diff --git a/tasks/human_eval_085.rs b/tasks/human_eval_085.rs
@@ -50,6 +50,7 @@ fn add(lst: Vec<u32>) -> (sum: u64)
             0 < lst.len() < u32::MAX,
             sum <= (u32::MAX) * i,
             sum == add_odd_evens(lst@) - add_odd_evens(lst@.skip(i - 1 as int)),
+        decreases lst.len() + 2 - i,
     {
         if (lst[i] % 2 == 0) {
             sum += lst[i] as u64;
diff --git a/tasks/human_eval_087.rs b/tasks/human_eval_087.rs
@@ -90,7 +90,7 @@ proof fn coords_distinct_after_push(coords: Seq<(usize, usize)>, x: usize, y: us
     requires
         coords_distinct(coords),
         forall|k: int|
-            0 <= k < coords.len() ==> #[trigger coords[k]]
+            0 <= k < coords.len() ==> #[trigger]
             coords[k].0 < x || coords[k].1 > y,
     ensures
         coords_distinct(coords.push((x, y))),
diff --git a/tasks/human_eval_127.rs b/tasks/human_eval_127.rs
@@ -52,6 +52,7 @@ fn is_prime_2(num: u64) -> (result: bool)
         invariant
             2 <= i <= num,
             result <==> spec_prime_helper(num as int, i as int),
+        decreases num - i,
     {
         if num % i == 0 {
             result = false;
diff --git a/tasks/human_eval_129.rs b/tasks/human_eval_129.rs
@@ -440,17 +440,18 @@ pub fn min_path<const N: usize>(grid: [[u8; N]; N], k: u8) -> (path: Vec<u8>)
         k_counter = k_counter - 1;
 
         //proving adjacency
+        let ghost grid = grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int));
         assert(forall|i: int|
             (0 <= #[trigger] (i + 0) < path@.map_values(|j: u8| j as int).len() - 1) ==> (exists|
                 i0: int,
                 j0: int,
             |
-                (is_adjacent::<N>(
-                    grid@.map_values(|row: [u8; N]| row@.map_values(|item| item as int)),
-                    path@.map_values(|j: u8| j as int)[i],
-                    path@.map_values(|j: u8| j as int)[(i + 1)],
-                    (i0, j0),
-                ))));
+                ({
+                let m = path@.map_values(|j: u8| j as int)[i];
+                let n = path@.map_values(|j: u8| j as int)[(i + 1)];
+                #[trigger] grid[i0][j0] == m &&
+                is_adjacent::<N>(grid, m, n, (i0, j0))
+                })));
     }
     assert(forall|i: int|
         (0 <= i + 0 < path@.len() - 1) ==> adjacent_numbers::<N>(
diff --git a/tasks/human_eval_130.rs b/tasks/human_eval_130.rs
@@ -64,6 +64,7 @@ fn tri(n: u32) -> (result: Vec<Option<u32>>)
                     0 <= j < i ==> ((result[j].is_some() ==> result[j].unwrap() == spec_tri(
                         j as nat,
                     )) && (result[j].is_none() ==> spec_tri(j as nat) > u32::MAX)),
+            decreases n + 1 - i,
         {
             if i % 2 == 0 {
                 result.push(Some(1 + (i / 2)));
diff --git a/tasks/human_eval_139.rs b/tasks/human_eval_139.rs
@@ -124,6 +124,7 @@ pub fn brazilian_factorial_impl(n: u64) -> (ret: Option<u64>)
         };
 
         fact_i = start * fact_i;
+        assert(factorial(start as nat) == fact_i);
 
         special_fact = fact_i * special_fact;
 
diff --git a/tasks/human_eval_146.rs b/tasks/human_eval_146.rs
@@ -23,6 +23,7 @@ spec fn extract_first_digit_spec(n: int) -> int
 fn extract_first_digit(n: u32) -> (res: u32)
     ensures
         res == extract_first_digit_spec(n as int),
+    decreases n,
 {
     if n < 10 {
         n
@@ -89,6 +90,7 @@ fn special_filter(numbers: &Vec<i32>) -> (count: usize)
             0 <= index <= numbers.len(),
             0 <= counter <= index,
             counter == special_filter_spec(numbers@.subrange(0, index as int)),
+        decreases numbers.len() - index,
     {
         if (is_valid_element(numbers[index])) {
             counter += 1;
diff --git a/tasks/human_eval_150.rs b/tasks/human_eval_150.rs
@@ -29,6 +29,7 @@ fn is_prime(num: u32) -> (result: bool)
         invariant
             2 <= i <= num,
             result <==> spec_prime_helper(num as int, i as int),
+        decreases num - i,
     {
         if num % i == 0 {
             result = false;
diff --git a/tasks/human_eval_163.rs b/tasks/human_eval_163.rs
@@ -53,9 +53,6 @@ fn generate_integers(a: u32, b: u32) -> (result: Vec<u32>)
     let lower = max(2, left);
     let upper = min(8, right);
 
-    assert(2 <= lower);
-    assert(upper <= 8);
-
     let mut result: Vec<u32> = vec![];
     let mut i = lower;
     while i <= upper
@@ -67,10 +64,30 @@ fn generate_integers(a: u32, b: u32) -> (result: Vec<u32>)
                     || result[i] == 8),
             forall|j: int| 0 <= j < result.len() ==> result[j] <= i,
             forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] <= result[j],
+            forall|x: int|
+                vmin(a as int, b as int) <= x < i && 2 <= x <= 8 && x % 2 == 0
+                    ==> #[trigger] result@.contains(x as u32),
+        decreases upper + 1 - i,
     {
+        let ghost old_result = result@;
         if i % 2 == 0 {
             result.push(i);
+            assert(result@.contains(i)) by {
+                assert(result@[result@.len() - 1] == i);    // trigger
+            }
+            assert forall|x: int|
+                    vmin(a as int, b as int) <= x < i && 2 <= x <= 8 && x % 2 == 0
+                        implies #[trigger] result@.contains(x as u32) by {
+                if x == i {
+                } else {
+                    assert(old_result.contains(x as u32));
+                    let i = choose |i| 0 <= i < old_result.len() && old_result[i] == x as u32;
+                    assert(result@[i] == x as u32);   // trigger
+                    assert(result@.contains(x as u32));
+                }
+            }
         }
+        i = i + 1;
     }
     result
 }

Original file line number	Diff line number	Diff line change
`@@ -106,6 +106,7 @@ pub fn intersperse(numbers: Vec<u64>, delimiter: u64) -> (result: Vec<u64>)`
`106`	`106`	`result.len() == 2 * index,`
`107`	`107`	`forall\|i: int\| 0 <= i < index ==> #[trigger] result[even(i)] == numbers[i],`
`108`	`108`	`forall\|i: int\| 0 <= i < index ==> #[trigger] result[odd(i)] == delimiter,`
	`109`	`+ decreases numbers.len() - 1 - index,`
`109`	`110`	`{`
`110`	`111`	`result.push(numbers[index]);`
`111`	`112`	`result.push(delimiter);`
Original file line number	Diff line number	Diff line change
`@@ -46,6 +46,7 @@ fn compute_gcd(a: u64, b: u64) -> (g: u64)`
`46`	`46`	`loop`
`47`	`47`	`invariant`
`48`	`48`	`gcd(a1 as nat, b1 as nat) == gcd(a as nat, b as nat),`
	`49`	`+ decreases b1,`
`49`	`50`	`{`
`50`	`51`	`if a1 == 0 {`
`51`	`52`	`return b1;`
Original file line number	Diff line number	Diff line change
`@@ -130,6 +130,7 @@ pub fn number_to_char_impl(n: u8) -> (char_vec: Vec<char>)`
`130`	`130`	`while (i > 0)`
`131`	`131`	`invariant`
`132`	`132`	`number_to_char(n as nat) == number_to_char(i as nat).add(output@),`
	`133`	`+ decreases i,`
`133`	`134`	`{`
`134`	`135`	`let m = i % 10;`
`135`	`136`	`let current = single_digit_number_to_char_impl(m);`
Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,7 @@ use vstd::prelude::*;`
`13`	`13`	`verus! {`
`14`	`14`
`15`	`15`	`pub open spec fn mul(a: nat, b: nat) -> nat {`
`16`		`- builtin::mul(a, b)`
	`16`	`+ vstd::prelude::mul(a, b)`
`17`	`17`	`}`
`18`	`18`
`19`	`19`	`/// Specification for what it means for d to divide a`
`@@ -73,6 +73,7 @@ fn largest_divisor(n: u32) -> (ret: u32)`
`73`	`73`	`n > 0,`
`74`	`74`	`i < n,`
`75`	`75`	`forall\|k: u32\| i < k < n ==> !divides(k as nat, n as nat),`
	`76`	`+ decreases i,`
`76`	`77`	`{`
`77`	`78`	`if n % i == 0 {`
`78`	`79`	`assert(divides(i as nat, n as nat)) by {`
Original file line number	Diff line number	Diff line change
`@@ -37,6 +37,7 @@ fn count_frequency(elements: &Vec<i64>, key: i64) -> (frequency: usize)`
`37`	`37`	`0 <= index <= elements.len(),`
`38`	`38`	`0 <= counter <= index,`
`39`	`39`	`count_frequency_spec(elements@.subrange(0, index as int), key) == counter,`
	`40`	`+ decreases elements.len() - index,`
`40`	`41`	`{`
`41`	`42`	`if (elements[index] == key) {`
`42`	`43`	`counter += 1;`
Original file line number	Diff line number	Diff line change
`@@ -51,6 +51,7 @@ fn concatenate_impl(strings: Vec<Vec<char>>) -> (joined: Vec<char>)`
`51`	`51`	`strings.deep_view(),`
`52`	`52`	`i as nat,`
`53`	`53`	`),`
	`54`	`+ decreases strings.len() - i,`
`54`	`55`	`{`
`55`	`56`	`assert(concatenate(strings.deep_view()) == joined@ + strings[i as int]@ + concat_helper(`
`56`	`57`	`strings.deep_view(),`
Original file line number	Diff line number	Diff line change
`@@ -46,6 +46,7 @@ fn is_prime_impl(n: u8) -> (res: bool)`
`46`	`46`	`invariant`
`47`	`47`	`2 <= k <= n,`
`48`	`48`	`res == is_prime_so_far(n as nat, k as nat),`
	`49`	`+ decreases n - k,`
`49`	`50`	`{`
`50`	`51`	`assert((is_prime_so_far(n as nat, k as nat) && (n as nat) % (k as nat) != 0)`
`51`	`52`	`== is_prime_so_far(n as nat, (k + 1) as nat));`
Original file line number	Diff line number	Diff line change
`@@ -45,6 +45,7 @@ fn fib(n: u32) -> (ret: Option<u32>)`
`45`	`45`	`None => spec_fib(n as nat) > u32::MAX,`
`46`	`46`	`Some(f) => f == spec_fib(n as nat),`
`47`	`47`	`},`
	`48`	`+ decreases n,`
`48`	`49`	`{`
`49`	`50`	`if n > 47 {`
`50`	`51`	`proof {`