proof: Makefile and workflow for runtest (eventually, only one job fo…

…r the proofs will be kept)

.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
+
 

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