From a455bcb5adbc5b8727fed98b5a1365c5c4c879cf Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Mon, 16 Dec 2024 18:00:04 -0500
Subject: [PATCH] documentation

---
 .github/workflows/kani.yml | 7 +++++--
 scripts/run-kani.sh        | 6 ++++--
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 10bf91a745fab..59a0c56a5d49f 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -35,16 +35,19 @@ jobs:
       PARALLEL_TOTAL: 4
     
     steps:
+      # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
-
+      
+      # Step 2: Install jq
       - name: Install jq
         if: matrix.os == 'ubuntu-latest'
         run: sudo apt-get install -y jq
-
+      
+      # Step 3: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
    
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 84d8400d02947..13b2dfc2afaa1 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -155,8 +155,9 @@ get_kani_path() {
     echo "$(realpath "$build_dir/scripts/kani")"
 }
 
-# Run kani list with JSON format and process with jq to extract all harness names
-# Note: This code is based on `kani list` JSON version 0.1 -- if the version changes, this logic may need to change as well.
+# Run kani list with JSON format and process with jq to extract harness names and total number of harnesses.
+# Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1.
+# If FILE_VERSION changes, this logic may need to change as well.
 get_harnesses() {
     local kani_path="$1"
     "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json
@@ -168,6 +169,7 @@ get_harnesses() {
     HARNESS_COUNT=${#ALL_HARNESSES[@]}
 }
 
+# Given an array of harness names, run verification for those harnesses
 run_verification_subset() {
     local kani_path="$1"
     local harnesses=("${@:2}")  # All arguments after kani_path are harness names