Kani Workflow Updates (#214)

Update the `kani list` part of our workflow to:
- Be its own step of the workflow so it can run in parallel, which is
nice because it finishes much faster than the other jobs in the Kani
workflow
- Use the new markdown format. This makes the list much more readable
(compare [current
format](https://github.com/model-checking/verify-rust-std/actions/runs/12199714877/attempts/2#summary-34034201022)
to [markdown
format](https://github.com/carolynzech/verify-rust-std/actions/runs/12203155221/attempts/1#summary-34045490103)).

Also remove the Test Kani workflow step, because it's expensive and
duplicates verification work.

Author: Carolyn Zech

.github/workflows/kani.yml

@@ -38,18 +38,10 @@ jobs:
       # Step 2: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
-
-  test-kani-script:
-    name: Test Kani script
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-        include:
-          - os: ubuntu-latest
-            base: ubuntu
-          - os: macos-latest
-            base: macos
+   
+  run-kani-list:
+    name: Kani List
+    runs-on: ubuntu-latest
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository
@@ -58,25 +50,18 @@ jobs:
           path: head
           submodules: true
 
-      # Step 2: Test Kani verification script with specific arguments
-      - name: Test Kani script (Custom Args)
-        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
-
-      # Step 3: Test Kani verification script in the repository directory
-      - name: Test Kani script (In Repo Directory)
-        working-directory: ${{github.workspace}}/head
-        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
-      
-      # Step 4: Run list on the std library and add output to job summary
+      # Step 2: Run list on the std library
       - name: Run Kani List
         run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
-
+      
+      # Step 3: Add output to job summary
       - name: Add Kani List output to job summary
         uses: actions/github-script@v6
         with:
           script: |
             const fs = require('fs');
-            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
             await core.summary
-              .addRaw(kaniOutput)
-              .write();
+              .addHeading('Kani List Output', 2)
+              .addRaw(kaniOutput, false)
+              .write();

scripts/run-kani.sh

@@ -221,7 +221,7 @@ main() {
             --cbmc-args --object-bits 12
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt
+        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown
     fi
 }