Completed task 066

tasks/human_eval_066.rs

@@ -9,7 +9,58 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn is_upper_case(c: char) -> bool {
+    c >= 'A' && c <= 'Z'
+}
+
+// This spec function computes uppercase character (i.e, ASCII code) sum.
+spec fn count_uppercase_sum(seq: Seq<char>) -> int
+    decreases seq.len(),
+{
+    if seq.len() == 0 {
+        0
+    } else {
+        count_uppercase_sum(seq.drop_last()) + if is_upper_case(seq.last()) {
+            seq.last() as int
+        } else {
+            0 as int
+        }
+    }
+}
+
+// This function takes a string as input and returns the sum of the upper characters only'
+fn digit_sum(text: &[char]) -> (sum: u128)
+    ensures
+        count_uppercase_sum(text@) == sum,
+{
+    let mut index = 0;
+    let mut sum = 0u128;
+
+    while index < text.len()
+        invariant
+            0 <= index <= text.len(),
+            count_uppercase_sum([email protected](0, index as int)) == sum,
+            forall|j: int|
+                0 <= j <= index ==> (u64::MIN * index <= (count_uppercase_sum(
+                    #[trigger] [email protected](0, j),
+                )) <= u64::MAX * index),
+            u64::MIN * index <= sum <= u64::MAX * index,
+    {
+        if (text[index] >= 'A' && text[index] <= 'Z') {
+            assert([email protected](0, index as int) =~= [email protected](
+                0,
+                (index + 1) as int,
+            ).drop_last());
+            sum = sum + text[index] as u128;
+        }
+        index += 1;
+        assert([email protected](0, index - 1 as int) == [email protected](0, index as int).drop_last());
+
+    }
+    assert(index == [email protected]());
+    assert(text@ == [email protected](0, index as int));
+    sum
+}
 
 } // verus!
 fn main() {}