Batch files script

.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

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

Common/ntt.bat → 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"

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

Primitive/Asymmetric/Cipher/Kyber/3.01/verify.bat → 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

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

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

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