update spec for 007 and 074

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
-        [email protected]() <= [email protected](),
-        forall|s: &str| [email protected](s) ==> [email protected](s),
-        forall|s: &str|
-            [email protected](s) ==> exists|i: int|
-                0 <= i <= [email protected]() - [email protected]() && [email protected](
-                    i,
-                    #[trigger] (i + [email protected]()),
-                ) == substring@,
+        forall|i: int|
+            0 <= i < [email protected]() && (exists|j: int|
+                0 <= j <= strings@[i]@.len() - [email protected]() && strings[i]@.subrange(
+                    j,
+                    #[trigger] (j + [email protected]()),
+                ) == substring@) ==> [email protected](#[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 <= [email protected](),
-            [email protected]() <= i,
-            forall|s: &str| [email protected](s) ==> [email protected](s),
-            forall|s: &str|
-                [email protected](s) ==> exists|i: int|
-                    0 <= i <= [email protected]() - [email protected]() && [email protected](
-                        i,
-                        #[trigger] (i + [email protected]()),
-                    ) == substring@,
+            forall|i: int|
+                0 <= i < n && (exists|j: int|
+                    0 <= j <= strings@[i]@.len() - [email protected]() && strings[i]@.subrange(
+                        j,
+                        #[trigger] (j + [email protected]()),
+                    ) == substring@) ==> [email protected](#[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([email protected]() == strings[i as int]);
+            res.push(strings[n]);
+            assert([email protected]() == strings[n as int]);
             assert([email protected]_last() == res_old@);
-            assert(forall|s: &str|
-                [email protected](s) <==> [email protected](s) || s == strings[i as int]);
         }
     }
     res

tasks/human_eval_068.rs

@@ -12,17 +12,18 @@ verus! {
 fn pluck_smallest_even(nodes: &Vec<u32>) -> (result: Vec<u32>)
     requires
         [email protected]() <= u32::MAX,
-        forall|i: int| 0 <= i < [email protected]() ==> nodes@[i] >= 0,
     ensures
         [email protected]() == 0 || [email protected]() == 2,
-        [email protected]() == 2 ==> 0 <= result@[1] < [email protected]() && nodes@[result@[1] as int]
-            == result@[0],
-        [email protected]() == 2 ==> result@[0] % 2 == 0,
-        [email protected]() == 2 ==> forall|i: int|
-            0 <= i < [email protected]() && nodes@[i] % 2 == 0 ==> result@[0] <= nodes@[i],
-        [email protected]() == 2 ==> forall|i: int|
-            0 <= i < result@[1] ==> nodes@[i] % 2 != 0 || nodes@[i] > result@[0],
         [email protected]() == 0 ==> forall|i: int| 0 <= i < [email protected]() ==> nodes@[i] % 2 != 0,
+        [email protected]() == 2 ==> {
+            let node = result@[0];
+            let index = result@[1];
+            0 <= index < [email protected]() && nodes@[index as int] == node && node % 2 == 0 && forall|
+                i: int,
+            |
+                0 <= i < [email protected]() && 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<u32> = None;
     let mut smallest_index: Option<u32> = None;

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<Vec<&'a str>>)
+spec fn spec_sum(s: Seq<nat>) -> 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<nat>, i: int, j: int)
+    requires
+        0 <= i <= j <= s.len(),
     ensures
-        ret.is_some() ==> ret.unwrap() == if [email protected]_values(|s: &str| [email protected]()).fold_left(
-            0,
-            |x: int, y| x + y,
-        ) <= [email protected]_values(|s: &str| [email protected]()).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 == [email protected](0, i as int).map_values(|s: &str| [email protected]()).fold_left(
-                0,
-                |x: int, y| x + y,
-            ),
-    // i <= lst1.len(),
-    {
-        l1 = l1.checked_add(lst1[i].unicode_len())?;
-        assert([email protected](0, i + 1).map_values(|s: &str| [email protected]()).drop_last()
-            == [email protected](0, i as int).map_values(|s: &str| [email protected]()));
+    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@ == [email protected](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| [email protected]()))
+}
+
+fn checked_total_str_len(lst: &Vec<&str>) -> (ret: Option<usize>)
+    ensures
+        ret.is_some() <==> total_str_len(lst@) <= usize::MAX,
+        ret.is_some() <==> ret.unwrap() == total_str_len(lst@),
+{
+    let ghost lens = Seq::<nat>::empty();
+    let mut sum: usize = 0;
+    for i in 0..lst.len()
         invariant
-            l2 == lst2@.subrange(0, i as int).map_values(|s: &str| [email protected]()).fold_left(
+            sum == lst@.subrange(0, i as int).map_values(|s: &str| [email protected]()).fold_left(
                 0,
                 |x: int, y| x + y,
             ),
+            spec_sum(lens) == sum,
+            lens =~= [email protected]_values(|s: &str| [email protected]()).take(i as int),
+            lens =~= [email protected](i as int).map_values(|s: &str| [email protected]()),
     {
-        let x = lst2[i].unicode_len();
-        assert(x == lst2[i as int]@.len());
-        l2 = l2.checked_add(x)?;
-        assert([email protected](0, i + 1).map_values(|s: &str| [email protected]()).drop_last()
-            == [email protected](0, i as int).map_values(|s: &str| [email protected]()));
+        let x = lst[i].unicode_len();
+        proof {
+            assert(lens.push(x as nat).drop_last() == lens);
+            lens = lens.push(x as nat);
+            assert(lens =~= [email protected]_values(|s: &str| [email protected]()).take(i + 1));
+
+            lemma_increasing_sum([email protected]_values(|s: &str| [email protected]()), i + 1, [email protected]() as int);
+            assert(total_str_len(lst@) >= spec_sum(lens)) by {
+                assert([email protected]_values(|s: &str| [email protected]()) =~= [email protected]_values(
+                    |s: &str| [email protected](),
+                ).take([email protected]() 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([email protected](i + 1).map_values(|s: &str| [email protected]()).drop_last() == [email protected](
+            i as int,
+        ).map_values(|s: &str| [email protected]()));
     }
-    assert(lst2@ == [email protected](0, lst2.len() as int));
+    assert(lst@ == [email protected](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<Vec<&'a str>>)
+    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)

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<u32>)
 
 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!