From 7308f25a226d4d49f685785a5cfcc0da6ef9951f 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 ++++++++++++-
 Common/ntt_check.bat                          |  4 ++
 Common/{ntt.bat => ntt_prove.bat}             |  3 -
 .../Cipher/Kyber/3.01/verify_check.bat        | 18 ++++++
 .../3.01/{verify.bat => verify_prove.bat}     | 17 ------
 .../{verify2.bat => verify2_check.bat}        |  0
 .../{verify3.bat => verify3_check.bat}        |  0
 .../{verify5.bat => verify5_check.bat}        |  0
 scripts/prove_all_properties.sh               |  2 +-
 scripts/run_batch_files.sh                    | 56 +++++++++++++++++++
 scripts/test_all_properties.sh                |  2 +-
 11 files changed, 117 insertions(+), 23 deletions(-)
 create mode 100644 Common/ntt_check.bat
 rename Common/{ntt.bat => ntt_prove.bat} (79%)
 create mode 100644 Primitive/Asymmetric/Cipher/Kyber/3.01/verify_check.bat
 rename Primitive/Asymmetric/Cipher/Kyber/3.01/{verify.bat => verify_prove.bat} (65%)
 rename Primitive/Asymmetric/Signature/Dilithium/Final_Draft/{verify2.bat => verify2_check.bat} (100%)
 rename Primitive/Asymmetric/Signature/Dilithium/Final_Draft/{verify3.bat => verify3_check.bat} (100%)
 rename Primitive/Asymmetric/Signature/Dilithium/Final_Draft/{verify5.bat => verify5_check.bat} (100%)
 create mode 100755 scripts/run_batch_files.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c4c36af1..3b267789 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: Run check batch files..
+      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: Run prove batch files..
+      run: bash scripts/run_batch_files.sh
diff --git a/Common/ntt_check.bat b/Common/ntt_check.bat
new file mode 100644
index 00000000..d569e94c
--- /dev/null
+++ b/Common/ntt_check.bat
@@ -0,0 +1,4 @@
+:load ntt.cry
+:! printf "\nCan't prove the naive NTT.\n"
+:! printf "Check the naive NTT.\n"
+:check naive_ntt_correct
diff --git a/Common/ntt.bat b/Common/ntt_prove.bat
similarity index 79%
rename from Common/ntt.bat
rename to Common/ntt_prove.bat
index 23ef4899..44ca6c8b 100644
--- a/Common/ntt.bat
+++ b/Common/ntt_prove.bat
@@ -1,9 +1,6 @@
 :load ntt.cry
 :! printf "\nProve the base NTT is correct.\n"
 :prove ntt_correct
-:! printf "\nCan't prove the naive NTT.\n"
-:! printf "Check the naive NTT.\n"
-:check naive_ntt_correct
 :! printf "\n\nProve the connection with naive ntt "
 :! printf "and recursive ntt is correct.\n"
 :! printf "\nProve the NTT agrees with naive NTT.\n"
diff --git a/Primitive/Asymmetric/Cipher/Kyber/3.01/verify_check.bat b/Primitive/Asymmetric/Cipher/Kyber/3.01/verify_check.bat
new file mode 100644
index 00000000..2c13bbf2
--- /dev/null
+++ b/Primitive/Asymmetric/Cipher/Kyber/3.01/verify_check.bat
@@ -0,0 +1,18 @@
+:l kyber.tex
+
+:set tests=3
+
+:! printf "\nRunning 'check' commands for concatPlusCorrect property\n\n"
+:check concatPlusCorrect`{x=4, y=4}
+
+:! printf "\nRunning 'check' command for CorrectnessEncodeDecode' property\n\n"
+:check CorrectnessEncodeDecode'
+
+:! printf "\nRunning 'check' command for CorrectnessEncodeDecode property\n\n"
+:check CorrectnessEncodeDecode
+
+:! printf "\nRunning 'check' command for CorrectnessPKE property\n\n"
+:check CorrectnessPKE
+
+:! printf "\nRunning 'check' command for CorrectnessKEM property\n\n"
+:check CorrectnessKEM
diff --git a/Primitive/Asymmetric/Cipher/Kyber/3.01/verify.bat b/Primitive/Asymmetric/Cipher/Kyber/3.01/verify_prove.bat
similarity index 65%
rename from Primitive/Asymmetric/Cipher/Kyber/3.01/verify.bat
rename to Primitive/Asymmetric/Cipher/Kyber/3.01/verify_prove.bat
index f2650fed..7e763407 100644
--- a/Primitive/Asymmetric/Cipher/Kyber/3.01/verify.bat
+++ b/Primitive/Asymmetric/Cipher/Kyber/3.01/verify_prove.bat
@@ -1,10 +1,5 @@
 :l kyber.tex
 
-:set tests=3
-
-:! printf "\nRunning 'check' commands for concatPlusCorrect property\n\n"
-:check concatPlusCorrect`{x=4, y=4}
-
 :! printf "\nRunning 'prove' commands for concatPlusCorrect property\n\n"
 :prove concatPlusCorrect`{x=0, y=0}
 :prove concatPlusCorrect`{x=1, y=1}
@@ -35,15 +30,3 @@
 
 :! printf "\nRunning 'prove' command for CorrectnessEncodeBytes property\n\n"
 :prove CorrectnessEncodeBytes
-
-:! printf "\nRunning 'check' command for CorrectnessEncodeDecode' property\n\n"
-:check CorrectnessEncodeDecode'
-
-:! printf "\nRunning 'check' command for CorrectnessEncodeDecode property\n\n"
-:check CorrectnessEncodeDecode
-
-:! printf "\nRunning 'check' command for CorrectnessPKE property\n\n"
-:check CorrectnessPKE
-
-:! printf "\nRunning 'check' command for CorrectnessKEM property\n\n"
-:check CorrectnessKEM
diff --git a/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify2.bat b/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify2_check.bat
similarity index 100%
rename from Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify2.bat
rename to Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify2_check.bat
diff --git a/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify3.bat b/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify3_check.bat
similarity index 100%
rename from Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify3.bat
rename to Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify3_check.bat
diff --git a/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify5.bat b/Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify5_check.bat
similarity index 100%
rename from Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify5.bat
rename to Primitive/Asymmetric/Signature/Dilithium/Final_Draft/verify5_check.bat
diff --git a/scripts/prove_all_properties.sh b/scripts/prove_all_properties.sh
index 9d10c9f9..cf414c4d 100755
--- a/scripts/prove_all_properties.sh
+++ b/scripts/prove_all_properties.sh
@@ -23,7 +23,7 @@ prove_properties() {
       prove_properties "$FILE"
     elif [[ -f "$FILE" && ("$FILE" == *.cry || "$FILE" == *.md || "$FILE" == *.tex) ]]; then
       # Find all of the properties in the file
-      props=$(grep -oE "^ *property [a-zA-Z0-9_']+" $FILE | awk '{print $2}')
+      props=$(grep -oE "^property [a-zA-Z0-9_']+" $FILE | awk '{print $2}')
       if [ -z "$props" ]; then
         echo "$FILE has no properties to prove."
       else
diff --git a/scripts/run_batch_files.sh b/scripts/run_batch_files.sh
new file mode 100755
index 00000000..a69dd356
--- /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
diff --git a/scripts/test_all_properties.sh b/scripts/test_all_properties.sh
index bb0c07f8..fb1783e7 100755
--- a/scripts/test_all_properties.sh
+++ b/scripts/test_all_properties.sh
@@ -14,7 +14,7 @@ test_properties() {
       test_properties "$FILE"
     elif [[ -f "$FILE" && ("$FILE" == *.cry || "$FILE" == *.md || "$FILE" == *.tex) ]]; then
       # Find all the properties in the file
-      props=$(grep -oE "^ *property [a-zA-Z0-9_']+" $FILE | awk '{print $2}')
+      props=$(grep -oE "^property [a-zA-Z0-9_']+" $FILE | awk '{print $2}')
       if [ -z "$props" ]; then
         echo "$FILE has no properties to check."
       else