Split batch files; check & prove

.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

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