From 6751f5d3c7d8ddeaeeac38a1a68f8366c12f7d0a Mon Sep 17 00:00:00 2001
From: WeetHet <stas.ale66@gmail.com>
Date: Thu, 19 Sep 2024 12:23:57 +0300
Subject: [PATCH] Complete 080

---
 tasks/human_eval_080.rs | 39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/tasks/human_eval_080.rs b/tasks/human_eval_080.rs
index 0185958..cdae840 100644
--- a/tasks/human_eval_080.rs
+++ b/tasks/human_eval_080.rs
@@ -9,7 +9,44 @@ use vstd::prelude::*;
 
 verus! {
 
-// TODO: Put your solution (the specification, implementation, and proof) to the task here
+spec fn three_distinct_spec(s: Seq<char>, i: int) -> bool
+    recommends
+        0 < i && i + 1 < s.len(),
+{
+    (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1])
+}
+
+fn three_distinct(s: &Vec<char>, i: usize) -> (is: bool)
+    requires
+        0 < i && i + 1 < s.len(),
+    ensures
+        is <==> three_distinct_spec(s@, i as int),
+{
+    (s[i - 1] != s[i]) && (s[i] != s[i + 1]) && (s[i] != s[i + 1])
+}
+
+spec fn happy_spec(s: Seq<char>) -> bool {
+    s.len() >= 3 && (forall|i: int| 0 < i && i + 1 < s.len() ==> three_distinct_spec(s, i))
+}
+
+#[verifier::loop_isolation(false)]
+fn is_happy(s: &Vec<char>) -> (happy: bool)
+    ensures
+        happy <==> happy_spec(s@),
+{
+    if s.len() < 3 {
+        return false;
+    }
+    for i in 1..(s.len() - 1)
+        invariant
+            forall|j: int| 0 < j < i ==> three_distinct_spec(s@, j),
+    {
+        if !three_distinct(s, i) {
+            return false;
+        }
+    }
+    return true;
+}
 
 } // verus!
 fn main() {}