Add result contract

.github/workflows/pr_approval.yml

@@ -9,6 +9,11 @@ on:
     types: [submitted]
   workflow_dispatch:
 
+# Without these permissions, we get a 403 error from github
+# for trying to modify the pull request for newer project.
+# Source: https://stackoverflow.com/a/76994510
+permissions: write-all
+
 jobs:
   check-approvals:
     if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch'
@@ -95,20 +100,20 @@ jobs:
             );
 
             const requiredApprovals = 2;
-            const requiredApproversCount = Array.from(approvers)
+            const currentCountfromCommittee = Array.from(approvers)
               .filter(approver => requiredApprovers.includes(approver))
               .length;
 
             // TODO: Improve logging and messaging to the user
             console.log('PR Approvers:', Array.from(approvers));
-            console.log('Required Approvers:', requiredApproversCount);
+            console.log('Required Approvers:', requiredApprovals);
 
             // Core logic that checks if the approvers are in the committee
             const checkName = 'PR Approval Status';
-            const conclusion = (approvers.size >= requiredApprovals && requiredApproversCount >= 2) ? 'success' : 'failure';
+            const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure';
             const output = {
               title: checkName,
-              summary: `PR has ${approvers.size} total approvals and ${requiredApproversCount} required approvals.`,
+              summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`,
               text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
             };
 
@@ -152,5 +157,5 @@ jobs:
             }
 
             if (conclusion === 'failure') {
-              core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApproversCount}`);
+              core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
             }

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));
+    }
+}