create individual proof targets

for specification security, specification correctness, and implementation correctness
formosa-crypto · Jul 20, 2024 · d4c59cf · d4c59cf
1 parent 5358a27
commit d4c59cf
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -1,7 +1,7 @@
 # -*- Makefile -*-
 
 # --------------------------------------------------------------------
-ECCONF := config/tests.config 
+ECCONF := config/tests.config
 CHECKS ?= mlkem
 
 # --------------------------------------------------------------------

diff --git a/config/tests.config b/config/tests.config
@@ -1,3 +1,12 @@
 [test-mlkem]
 okdirs  = !proof
 exclude = !proof/attic
+
+[test-mlkem-spec-sec]
+okdirs  = proof/security
+
+[test-mlkem-spec-corr]
+okdirs  = proof/spec
+
+[test-mlkem-impl-corr]
+okdirs  = !proof/correctness !proof/eclib