Finish tasks 006 and 017 (#30)

tasks/human_eval_006.rs

@@ -5,14 +5,120 @@ HumanEval/6
 /*
 ### VERUS BEGIN
 */
+use vstd::math::*;
 use vstd::prelude::*;
 
 verus! {
 
 // TODO: Put your solution (the specification, implementation, and proof) to the task here
+/// Given a space separated group of nested parentheses
+/// return a list of maximum depths of each group.
+pub open spec fn spec_nested_parens(s: Seq<char>) -> Option<Seq<int>> {
+    spec_nested_parens_helper(s, 0, 0, seq![])
+}
+
+/// Formalizes the problem as a rewrite system
+pub open spec fn spec_nested_parens_helper(
+    s: Seq<char>,
+    depth: int,
+    max_depth: int,
+    prev_depths: Seq<int>,
+) -> Option<Seq<int>>
+    decreases s.len(),
+{
+    if s.len() == 0 && depth == 0 {
+        if max_depth == 0 {
+            // (s, d, m, p) => Some(p) if s is empty and d is 0 and m == 0
+            Some(prev_depths)
+        } else {
+            // (s, d, m, p) => Some(p + [max_depth]) if s is empty and d is 0 and m != 0
+            Some(prev_depths + seq![max_depth])
+        }
+    } else if s.len() != 0 && s[0] == ' ' && depth == 0 && max_depth != 0 {
+        // Move on to the next group (if the previous group is non-empty)
+        // (s, d, m, p) => (s[1..], 0, 0, prev_depths + [max_depth]) if s[0] == ' ' and d == 0
+        spec_nested_parens_helper(s.drop_first(), 0, 0, prev_depths + seq![max_depth])
+    } else if s.len() != 0 && s[0] == '(' {
+        // (s, d, m, p) => (s[1..], d + 1, max(d + 1, m), p) if s[0] == '('
+        spec_nested_parens_helper(s.drop_first(), depth + 1, max(depth + 1, max_depth), prev_depths)
+    } else if s.len() != 0 && s[0] == ')' && depth > 0 {
+        // (s, d, m, p) => (s[1..], d - 1, m, p) if s[0] == ')' and d > 0
+        spec_nested_parens_helper(s.drop_first(), depth - 1, max_depth, prev_depths)
+    } else {
+        // Otherwise fail
+        None
+    }
+}
+
+/// Executable version
+pub fn parse_nested_parens(s: &str) -> (res: Option<Vec<usize>>)
+    ensures
+        res matches Some(res) ==> spec_nested_parens(s@) == Some(res@.map_values(|d| d as int)),
+        res is None ==> spec_nested_parens(s@) is None,
+{
+    let s_len = s.unicode_len();
+    let mut depth = 0;
+    let mut max_depth = 0;
+    let mut all_depths = vec![];
+
+    assert(s@.skip(0) == s@);
+    assert(all_depths@.map_values(|d| d as int) =~= Seq::<int>::empty());
+
+    for i in 0..s_len
+        invariant
+            i <= s_len == s@.len() <= usize::MAX,
+            0 <= depth <= max_depth <= i,
+            spec_nested_parens_helper(s@, 0, 0, seq![]) == spec_nested_parens_helper(
+                s@.skip(i as int),
+                depth as int,
+                max_depth as int,
+                all_depths@.map_values(|d| d as int),
+            ),
+    {
+        let c = s.get_char(i);  // Not the best performance-wise
+
+        assert(s@.skip(i as int).drop_first() == s@.skip(i + 1));
+
+        if c == ' ' && depth == 0 && max_depth != 0 {
+            // Push and map_values commute
+            assert(all_depths@.push(max_depth).map_values(|d| d as int) == all_depths@.map_values(
+                |d| d as int,
+            ) + seq![max_depth as int]);
+
+            all_depths.push(max_depth);
+            depth = 0;
+            max_depth = 0;
+        } else if c == '(' {
+            depth += 1;
+            if depth > max_depth {
+                max_depth = depth;
+            }
+        } else if c == ')' && depth > 0 {
+            depth -= 1;
+        } else {
+            return None;
+        }
+    }
+
+    assert(s@.skip(s_len as int).len() == 0);
+
+    if depth != 0 {
+        return None;
+    }
+    if max_depth != 0 {
+        // Push and map_values commute
+        assert(all_depths@.push(max_depth).map_values(|d| d as int) == all_depths@.map_values(
+            |d| d as int,
+        ) + seq![max_depth as int]);
+        all_depths.push(max_depth);
+    }
+    Some(all_depths)
+}
 
 } // verus!
-fn main() {}
+fn main() {
+    // eprintln!("{:?}", parse_nested_parens("(()()) ((())) () ((())()())"));
+}
 
 /*
 ### VERUS END

tasks/human_eval_017.rs

@@ -10,9 +10,99 @@ use vstd::prelude::*;
 verus! {
 
 // TODO: Put your solution (the specification, implementation, and proof) to the task here
+pub open spec fn spec_parse_music(s: Seq<char>) -> Option<Seq<int>>
+    decreases s.len(),
+{
+    if s.len() == 0 {
+        Some(seq![])
+    } else if s.len() >= 2 && s[0] == 'o' && s[1] == '|' {
+        if let Some(rest) = spec_parse_music(s.skip(2)) {
+            Some(seq![2] + rest)
+        } else {
+            None
+        }
+    } else if s.len() >= 2 && s[0] == '.' && s[1] == '|' {
+        if let Some(rest) = spec_parse_music(s.skip(2)) {
+            Some(seq![1] + rest)
+        } else {
+            None
+        }
+    } else if s.len() != 0 && s[0] == 'o' {
+        if let Some(rest) = spec_parse_music(s.skip(1)) {
+            Some(seq![4] + rest)
+        } else {
+            None
+        }
+    } else if s.len() != 0 && s[0] == ' ' {
+        // Somewhat more lenient: allows multiple spaces between notes
+        spec_parse_music(s.drop_first())
+    } else {
+        None
+    }
+}
+
+pub fn parse_music(s: &str) -> (res: Option<Vec<u8>>)
+    ensures
+        res matches Some(res) ==> spec_parse_music(s@) == Some(res@.map_values(|b| b as int)),
+        res is None ==> spec_parse_music(s@) is None,
+{
+    let s_len = s.unicode_len();
+    let mut beats = vec![];
+    let mut i = 0;
+
+    assert(s@.skip(0) == s@);
+
+    while i < s_len
+        invariant
+            s_len == s@.len(),
+            0 <= i <= s_len,
+            spec_parse_music(s@) matches Some(all_beats) ==> {
+                &&& spec_parse_music(s@.skip(i as int)) matches Some(rest)
+                &&& all_beats =~= beats@.map_values(|b| b as int) + rest
+            },
+            spec_parse_music(s@.skip(i as int)) matches Some(rest) ==> spec_parse_music(
+                s@,
+            ) matches Some(all_beats),
+            spec_parse_music(s@.skip(i as int)) is None ==> spec_parse_music(s@) is None,
+        decreases s_len - i,
+    {
+        let c = s.get_char(i);
+
+        assert(s@.skip(i as int).skip(1) == s@.skip(i + 1));
+        assert(s@.len() >= i + 2 ==> s@.skip(i as int).skip(2) == s@.skip(i + 2));
+
+        if c == ' ' {
+            i += 1;
+            continue ;
+        }
+        if i < s_len - 1 {
+            let c2 = s.get_char(i + 1);
+
+            if c == 'o' && c2 == '|' {
+                beats.push(2);
+                i += 2;
+                continue ;
+            } else if c == '.' && c2 == '|' {
+                beats.push(1);
+                i += 2;
+                continue ;
+            }
+        }
+        if c == 'o' {
+            beats.push(4);
+            i += 1;
+        } else {
+            return None;
+        }
+    }
+
+    Some(beats)
+}
 
 } // verus!
-fn main() {}
+fn main() {
+    // eprintln!("{:?}", parse_music("o o| .| o| o| .| .| .| .| o o"));
+}
 
 /*
 ### VERUS END