From f0043c35cada6c01f9e57d5e4f3793cdca431bc8 Mon Sep 17 00:00:00 2001
From: Alannah Carr <acarr@existx.com>
Date: Mon, 22 Jan 2024 09:15:38 -0500
Subject: [PATCH] Split batch files; check & prove

---
 .github/workflows/ci.yml                       |  4 ++--
 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
 8 files changed, 24 insertions(+), 22 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%)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7897e3c6..3b267789 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -59,7 +59,7 @@ jobs:
         apt install -y git
     - name: Checkout
       uses: actions/checkout@v4
-    - name: Check Cryptol Properties
+    - name: Run check batch files..
       run: bash scripts/run_batch_files.sh
 
   prove:
@@ -100,5 +100,5 @@ jobs:
         apt install -y git
     - name: Checkout
       uses: actions/checkout@v4
-    - name: Check Cryptol Properties
+    - 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