From bcd1e5f3e8b90931489b5bf0855793771fb37073 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Sat, 28 Sep 2024 14:36:27 -0400
Subject: [PATCH] Strength spec for 63

---
 tasks/human_eval_063.rs | 48 +++++++++++++++++++++++++++++++++++++++--
 1 file changed, 46 insertions(+), 2 deletions(-)

diff --git a/tasks/human_eval_063.rs b/tasks/human_eval_063.rs
index f44704b..b19853f 100644
--- a/tasks/human_eval_063.rs
+++ b/tasks/human_eval_063.rs
@@ -9,6 +9,7 @@ use vstd::prelude::*;
 
 verus! {
 
+#[verifier::memoize]
 spec fn spec_fibfib(n: nat) -> nat
     decreases n,
 {
@@ -23,15 +24,58 @@ spec fn spec_fibfib(n: nat) -> nat
     }
 }
 
+proof fn lemma_fibfib_monotonic(i:nat, j:nat)
+    requires
+        i <= j
+    ensures
+        spec_fibfib(i) <= spec_fibfib(j),
+    decreases j - i,
+{
+    if (i < 3 && j < 3) || i == j {
+    } else if i == j - 1 {
+        reveal_with_fuel(spec_fibfib, 3);
+        lemma_fibfib_monotonic(i, (j - 1) as nat);
+    } else if i == j - 2 {
+        reveal_with_fuel(spec_fibfib, 3);
+        lemma_fibfib_monotonic(i, (j - 1) as nat);
+        lemma_fibfib_monotonic(i, (j - 2) as nat);
+    } else {
+        lemma_fibfib_monotonic(i, (j - 1) as nat);
+        lemma_fibfib_monotonic(i, (j - 2) as nat);
+        lemma_fibfib_monotonic(i, (j - 3) as nat);
+    }
+}
+
 fn fibfib(x: u32) -> (ret: Option<u32>)
     ensures
-        ret.is_some() ==> spec_fibfib(x as nat) == ret.unwrap(),
+        match ret {
+            None => spec_fibfib(x as nat) > u32::MAX,
+            Some(f) => f == spec_fibfib(x as nat)
+        },
 {
+    if x > 39 {
+        proof {
+            assert(spec_fibfib(40) > u32::MAX) by (compute_only);
+            lemma_fibfib_monotonic(40, x as nat);
+        }
+        return None;
+    }
     match (x) {
         0 => Some(0),
         1 => Some(0),
         2 => Some(1),
-        _ => fibfib(x - 1)?.checked_add(fibfib(x - 2)?)?.checked_add(fibfib(x - 3)?),
+        _ => {
+            proof {
+                // Prove that the recursive calls below succeed,
+                // and that the additions won't overflow
+                assert(spec_fibfib(39) < u32::MAX) by (compute_only);
+                lemma_fibfib_monotonic(x as nat, 39);
+                lemma_fibfib_monotonic((x - 1) as nat, 39);
+                lemma_fibfib_monotonic((x - 2) as nat, 39);
+                lemma_fibfib_monotonic((x - 3) as nat, 39);
+            }
+            Some(fibfib(x - 1)? + fibfib(x - 2)? + fibfib(x - 3)?)
+        }
     }
 }