From d4c59cf00212f2534ba1fb2e5b64c579fc636707 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Sat, 20 Jul 2024 16:18:03 +0100
Subject: [PATCH] create individual proof targets

for specification security, specification correctness, and
implementation correctness
---
 Makefile            | 2 +-
 config/tests.config | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index daa3a98b..71fd1aad 100644
--- 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
index d783a576..00f140bb 100644
--- 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