From 4feb3e60ced153edd9754a615ddf17d30bf8f5b9 Mon Sep 17 00:00:00 2001
From: Alannah Carr <acarr@existx.com>
Date: Mon, 22 Jan 2024 09:04:22 -0500
Subject: [PATCH] Batch files script

---
 .github/workflows/ci.yml   | 38 +++++++++++++++++++++++++-
 scripts/run_batch_files.sh | 56 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 93 insertions(+), 1 deletion(-)
 create mode 100755 scripts/run_batch_files.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c4c36af1..7897e3c6 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -44,12 +44,30 @@ jobs:
     - name: Check Cryptol Properties
       run: bash scripts/test_all_properties.sh
 
+  batch-check:
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/galoisinc/cryptol:nightly
+      options: --user root
+    needs: load
+    env:
+      STAGE: check
+    steps:
+    - name: Installing dependencies..
+      run: |
+        apt update
+        apt install -y git
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Check Cryptol Properties
+      run: bash scripts/run_batch_files.sh
+
   prove:
     runs-on: ubuntu-latest
     container:
       image: ghcr.io/galoisinc/cryptol:nightly
       options: --user root
-    needs: check
+    needs: [check, batch-check]
     steps:
     - name: Installing dependencies..
       run: |
@@ -66,3 +84,21 @@ jobs:
         path: |
           manual_proves.txt
           fast_proves.txt
+
+  batch-prove:
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/galoisinc/cryptol:nightly
+      options: --user root
+    needs: [check, batch-check]
+    env:
+      STAGE: prove
+    steps:
+    - name: Installing dependencies..
+      run: |
+        apt update
+        apt install -y git
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Check Cryptol Properties
+      run: bash scripts/run_batch_files.sh
diff --git a/scripts/run_batch_files.sh b/scripts/run_batch_files.sh
new file mode 100755
index 00000000..fc1fe503
--- /dev/null
+++ b/scripts/run_batch_files.sh
@@ -0,0 +1,56 @@
+#!/bin/bash
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+pushd $DIR/.. > /dev/null
+
+NUM_FILES=0
+NUM_BATCH_FILES=0
+BATCH_FILES=()
+NUM_FAILS=0
+FAILS=()
+
+run_batch() {
+  for FILE in "$1"/*; do
+    if [ -d "$FILE" ]; then
+      run_batch "$FILE"
+    elif [[ -f "$FILE" && "$FILE" == *"$STAGE".bat ]]; then
+      NUM_FILES=$(($NUM_FILES+1))
+      echo "Running $FILE..."
+      result=$(cryptol -e --batch $FILE)
+      echo "$result"
+      if grep -q "Counterexample" <<< "$result"; then
+        NUM_FAILS=$(($NUM_FAILS+1))
+        FAILS+=("$FILE")
+      else
+        NUM_BATCH_FILES=$(($NUM_BATCH_FILES+1))
+        BATCH_FILES+=("$FILE")
+      fi
+    fi
+  done
+}
+
+# run_batch "Common"
+run_batch "Primitive"
+
+echo ""
+echo "=== Done running $NUM_FILES Cryptol batch file(s) ==="
+
+if (( $NUM_BATCH_FILES != 0 )); then
+  echo "$NUM_BATCH_FILES Cryptol batch files ran:"
+  for FILE in "${BATCH_FILES[@]}"; do
+    echo "  $FILE"
+  done
+fi
+
+if (( $NUM_FAILS != 0 )); then
+  echo "$NUM_FAILS batch file(s) failed:"
+  for prop in "${FAILS[@]}"; do
+    echo "  $prop"
+  done
+  exit 1
+else
+  echo "All batch files succeeded."
+  exit 0
+fi
+
+popd > /dev/null