From 68800594182690325a91b2a21358a9380a1bf651 Mon Sep 17 00:00:00 2001
From: Joao Diogo Duarte <joao@diogoduarte.pt>
Date: Fri, 4 Oct 2024 15:45:08 +0100
Subject: [PATCH 1/2] Added files to allow this proof to be ran on the external
 ci

---
 proof/crypto_scalarmult/curve25519/easycrypt.project | 3 +++
 proof/crypto_scalarmult/curve25519/tests.config      | 2 ++
 2 files changed, 5 insertions(+)
 create mode 100644 proof/crypto_scalarmult/curve25519/easycrypt.project
 create mode 100644 proof/crypto_scalarmult/curve25519/tests.config

diff --git a/proof/crypto_scalarmult/curve25519/easycrypt.project b/proof/crypto_scalarmult/curve25519/easycrypt.project
new file mode 100644
index 0000000..7f23900
--- /dev/null
+++ b/proof/crypto_scalarmult/curve25519/easycrypt.project
@@ -0,0 +1,3 @@
+[general]
+idirs = ../../arrays/
+rdirs = amd64
diff --git a/proof/crypto_scalarmult/curve25519/tests.config b/proof/crypto_scalarmult/curve25519/tests.config
new file mode 100644
index 0000000..f5981de
--- /dev/null
+++ b/proof/crypto_scalarmult/curve25519/tests.config
@@ -0,0 +1,2 @@
+[test-curve25519]
+okdirs  = !amd64

From ba5660237f91b78f9ad4e0cfdaeb695a3ccea01e Mon Sep 17 00:00:00 2001
From: Tiago Oliveira <tiago.oliveira@sandboxquantum.com>
Date: Fri, 4 Oct 2024 19:05:29 +0100
Subject: [PATCH 2/2] proof: Makefile and workflow for runtest (eventually,
 only one job for the proofs will be kept)

---
 .github/workflows/amd64-linux.yml | 16 ++++++++++++++++
 proof/Makefile                    |  6 ++++++
 2 files changed, 22 insertions(+)

diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml
index fd9fff0..38d0b27 100644
--- a/.github/workflows/amd64-linux.yml
+++ b/.github/workflows/amd64-linux.yml
@@ -112,4 +112,20 @@ jobs:
       - name: return error
         run: make -C proof/ CI=1 err
 
+  # proof (using runtest)
+  proof-runtest:
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+      - name: preprocess
+        run: make -j$JOBS -C src/ CI=1 preprocess-inplace
+
+      - name: run proof
+        run: make -j$JOBS -C proof/ all-runtest
+      - name: print report
+        run: make -C proof/ CI=1 reporter
+      - name: return error
+        run: make -C proof/ CI=1 err
+
 
diff --git a/proof/Makefile b/proof/Makefile
index cb82935..3eedd38 100644
--- a/proof/Makefile
+++ b/proof/Makefile
@@ -127,6 +127,12 @@ all-no-report:
 	$(MAKE) check-extracted
 	$(MAKE) check-all
 
+all-runtest: CI=1
+all-runtest:
+	$(MAKE) distclean
+	$(MAKE) -C $(SRC) extract-to-easycrypt
+	(cd $(PROOF)/crypto_scalarmult/curve25519 && $(EASYCRYPT) runtest tests.config curve25519)
+
 # -----------------------------------------------------------------------------
 # clean rules