From e351be95a79faf0d2f245b042d18ed56f8e325da Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <jaisnan@amazon.com>
Date: Wed, 10 Jul 2024 21:33:34 +0000
Subject: [PATCH] Add first proof

---
 library/core/src/result.rs | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/library/core/src/result.rs b/library/core/src/result.rs
index 4c6dc4bba4377..8dc639e7c2e45 100644
--- a/library/core/src/result.rs
+++ b/library/core/src/result.rs
@@ -492,10 +492,14 @@
 
 #![stable(feature = "rust1", since = "1.0.0")]
 
+use safety::requires;
 use crate::iter::{self, FusedIterator, TrustedLen};
 use crate::ops::{self, ControlFlow, Deref, DerefMut};
 use crate::{convert, fmt, hint};
 
+#[cfg(kani)]
+use crate::kani;
+
 /// `Result` is a type that represents either success ([`Ok`]) or failure ([`Err`]).
 ///
 /// See the [module documentation](self) for details.
@@ -1459,6 +1463,7 @@ impl<T, E> Result<T, E> {
     #[inline]
     #[track_caller]
     #[stable(feature = "option_result_unwrap_unchecked", since = "1.58.0")]
+    #[requires(self.is_ok())]
     pub unsafe fn unwrap_unchecked(self) -> T {
         debug_assert!(self.is_ok());
         match self {
@@ -1491,6 +1496,7 @@ impl<T, E> Result<T, E> {
     #[inline]
     #[track_caller]
     #[stable(feature = "option_result_unwrap_unchecked", since = "1.58.0")]
+    #[requires(self.is_err())]
     pub unsafe fn unwrap_err_unchecked(self) -> E {
         debug_assert!(self.is_err());
         match self {
@@ -1982,3 +1988,17 @@ impl<T, E, F: From<E>> ops::FromResidual<ops::Yeet<E>> for Result<T, F> {
 impl<T, E> ops::Residual<T> for Result<convert::Infallible, E> {
     type TryType = Result<T, E>;
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(Result::unwrap_unchecked)]
+    pub fn check_unwrap_unchecked() {
+        let val: Result<u32, u64> = kani::any();
+        let ok_variant: Result<u32, u64> = Ok(0);
+        let copy = unsafe { ok_variant.unwrap_unchecked() };
+        assert_eq!(val, Result::Ok(copy));
+    }
+}