From 5d8ee62ca604baa2946cde16d47ed0f298afce96 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Wed, 10 Jul 2024 14:28:13 -0400
Subject: [PATCH 1/2] Add permissions needed to modify PR (#34)

Fixes:
https://github.com/model-checking/verify-rust-std/actions/runs/9878423942/job/27283663117
which is a 403 error from github.

[Source for
fix](https://stackoverflow.com/questions/70435286/resource-not-accessible-by-integration-on-github-post-repos-owner-repo-ac)

Test:
https://github.com/jaisnan/rust-dev/pull/22/checks?check_run_id=27285370500

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .github/workflows/pr_approval.yml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/pr_approval.yml b/.github/workflows/pr_approval.yml
index 316be83fc0e62..fbac5035e2d3a 100644
--- a/.github/workflows/pr_approval.yml
+++ b/.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}`);
             }

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