Merge branch 'main' into c-0013-rajathm-from_ptr

.github/workflows/pr_approval.yml

@@ -52,8 +52,11 @@ jobs:
               pull_number = context.issue.number;
             }
 
+            console.log(`owner is ${owner}`);
+            console.log(`pull_number is ${pull_number}`);
 
             // Get parsed data
+            let requiredApprovers;
             try {
               const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8');
               console.log('TOML content:', tomlContent);
@@ -85,23 +88,22 @@ jobs:
             );
 
             const requiredApprovals = 2;
-            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:', requiredApprovals);
+            const committeeApprovers = Array.from(approvers)
+              .filter(approver => requiredApprovers.includes(approver));
+            const currentCountfromCommittee = committeeApprovers.length;
 
             // Core logic that checks if the approvers are in the committee
-            const checkName = 'PR Approval Status';
-            const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure';
-            const output = {
-              title: checkName,
-              summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`,
-              text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
-            };
+            const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
 
+            console.log('PR Approval Status');
+            console.log(`PR has ${approvers.size} total approvals and ${currentCountfromCommittee} required approvals from the committee.`);
+            
+            console.log(`Committee Members: [${requiredApprovers.join(', ')}]`);
+            console.log(`Committee Approvers: ${committeeApprovers.length === 0 ? 'NONE' : `[${committeeApprovers.join(', ')}]`}`);
+            console.log(`All Approvers: ${approvers.size === 0 ? 'NONE' : `[${Array.from(approvers).join(', ')}]`}`);
+            
             if (conclusion === 'failure') {
-              core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
+              core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
+            } else {
+              core.info('PR approval check passed successfully.');
             }

doc/src/challenges/0002-intrinsics-memory.md

@@ -1,4 +1,4 @@
-# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
+# Challenge 2: Verify the memory safety of core intrinsics using raw pointers
 
 - **Status:** Open
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
@@ -61,7 +61,7 @@ All the following usages of intrinsics were proven safe:
 
 
 
-Annotate and verify all the functions that below that expose intrinsics with safety contracts
+Annotate and verify all the functions below that expose intrinsics with safety contracts
 
 | Function | Location |
 |---------|---------|

doc/src/challenges/0005-linked-list.md

@@ -11,7 +11,7 @@
 
 ## Goal
 
-Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate the its internal inductive-defined data type.
+Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type.
 
 ### Details
 

library/core/src/slice/iter.rs

@@ -3607,10 +3607,6 @@ mod verify {
                 check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
                 check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
 
-                // FIXME: The functions that are commented out are currently failing verification.
-                // Debugging the issue is currently blocked by:
-                // https://github.com/model-checking/kani/issues/3670
-                //
                 // Public functions that call safe abstraction `make_slice`.
                 check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| {
                     iter.as_slice();