From 2cd0a8cbc2e58f3aa395b2cea5e9d2adb6775e73 Mon Sep 17 00:00:00 2001
From: Tiago Oliveira <tiago.oliveira@sandboxquantum.com>
Date: Tue, 6 Aug 2024 01:32:38 +0100
Subject: [PATCH] check proofs

---
 .github/workflows/amd64-linux.yml |  10 ++
 proof/.gitignore                  |   4 +
 proof/Makefile                    | 152 ++++++++++++++++++++++++++++++
 src/Makefile.common               |   2 +-
 4 files changed, 167 insertions(+), 1 deletion(-)
 create mode 100644 proof/.gitignore
 create mode 100644 proof/Makefile

diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml
index e804b4a..ce84379 100644
--- a/.github/workflows/amd64-linux.yml
+++ b/.github/workflows/amd64-linux.yml
@@ -27,6 +27,15 @@ jobs:
       - name: run tests
         run: make -j$JOBS -C test/
 
+  proof:
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: run proof
+        run: make -j$JOBS -C proof/
+
   bench:
     runs-on: [self-hosted, linux, X64, amd64-main]
     steps:
@@ -38,3 +47,4 @@ jobs:
       - name: run benchmarks
         run: make -j$JOBS -C bench/
 
+
diff --git a/proof/.gitignore b/proof/.gitignore
new file mode 100644
index 0000000..e54f987
--- /dev/null
+++ b/proof/.gitignore
@@ -0,0 +1,4 @@
+*_s.ec
+*.ec.out
+*.eco
+.ci
diff --git a/proof/Makefile b/proof/Makefile
new file mode 100644
index 0000000..e9e59d5
--- /dev/null
+++ b/proof/Makefile
@@ -0,0 +1,152 @@
+# -----------------------------------------------------------------------------
+
+ECARGS    ?=
+ECJOBS    ?= 1
+ECCONF    := tests.config
+JASMIN    ?= jasminc
+EASYCRYPT ?= easycrypt
+
+
+# -----------------------------------------------------------------------------
+
+SRC     := $(abspath ../src)
+PROOF   := .
+FILTER  ?= $(PROOF)/crypto_%
+EXCLUDE ?=
+
+EXTRACTED ?= $(shell find $(PROOF) -name "*_s.ec")
+EXTRACTED_OUT := $(addsuffix .out, $(EXTRACTED))
+
+ALL ?= $(shell find $(PROOF) -name "*.ec")
+ALL_OUT := $(addsuffix .out, $(ALL))
+
+
+# -----------------------------------------------------------------------------
+
+CI ?= 0
+CI_REMOVE_OK_LOGS ?= "1"
+
+export CI
+
+CI_DIR =
+CI_CMD =
+ifeq ($(CI),1)
+CI_DIR := .ci
+CI_CMD = 2> $(@D)/$(CI_DIR)/$(@F).log && rm -f $(@D)/$(CI_DIR)/$(@F).error || \
+             (echo $$? | cat - $(@D)/$(CI_DIR)/$(@F).log > $(@D)/$(CI_DIR)/$(@F).error && \
+              rm $(@D)/$(CI_DIR)/$(@F).log && \
+              exit 0 \
+             )
+endif
+
+
+# -----------------------------------------------------------------------------
+# setting the default rule as 'all'
+
+default: all
+
+
+# -----------------------------------------------------------------------------
+# extract implementations
+
+.PHONY: extract-to-easycrypt
+
+extract-to-easycrypt:
+	$(MAKE) -C $(SRC) extract-to-easycrypt
+
+
+# -----------------------------------------------------------------------------
+# check
+
+.PHONY: __phony
+
+check-all: $(ALL_OUT)
+check-extracted: $(EXTRACTED_OUT)
+
+$(ALL_OUT):
+ifeq ($(CI),1)
+	mkdir -p $(@D)/$(CI_DIR)
+endif
+	($(EASYCRYPT) -R arrays/ $(ECARGS) $(subst .out,,$@) > $@) $(CI_CMD)
+
+
+# -----------------------------------------------------------------------------
+# reporter: this section defines rules for reporting the current implementation
+# status
+
+LOGS ?= formosa25519-logs-proof.tar.gz
+JLOG := ./../scripts/reporter/jlog
+
+CI_ERROR_FILES := $(shell find $(PROOF) -name '*.error')
+CI_ALL_FILES   := $(shell find $(PROOF) -name '*.log') $(CI_ERROR_FILES)
+
+.PHONY: reporter logs $(LOGS) err
+
+reporter:
+	$(JLOG) "Extraction from Jasmin to EasyCrypt status" src/ *_s.ec $(CI_REMOVE_OK_LOGS)
+	$(JLOG) "Checking EasyCrypt - extracted files status" proof/ *_s.ec.out $(CI_REMOVE_OK_LOGS)
+	#$(JLOG) "Checking EasyCrypt - all files status" proof/ *.ec.out $(CI_REMOVE_OK_LOGS)
+
+logs: $(LOGS)
+
+$(LOGS):
+	@$(JASMIN) -version > notes
+ifeq ($(words $(CI_ALL_FILES)),0)
+	@echo "There are no logs with warnings or errors. Good job." >> notes
+	@tar -zcvf $@ notes
+else
+	@tar -zcvf $@ notes $(CI_ALL_FILES)
+endif
+	@rm notes
+
+err:
+ifneq ($(words $(CI_ERROR_FILES)),0)
+	$(error $(CI_ERROR_FILES))
+endif
+
+# -----------------------------------------------------------------------------
+# to run 'everything': $ make -j$(nproc) all
+.PHONY: all
+
+all: CI=1
+all:
+	$(MAKE) distclean
+	$(MAKE) -C $(SRC) extract-to-easycrypt
+	$(MAKE) check-extracted
+	#$(MAKE) check-all
+	$(MAKE) reporter
+	$(MAKE) err
+
+# -----------------------------------------------------------------------------
+# clean rules
+
+.PHONY: clean distclean
+
+clean:
+	rm -f $(LOGS) $(ALL_OUT)
+	find . -type d -name ".ci" -exec rm -fr "{}" +
+	find . -name "*.eco" -exec rm {} +
+
+distclean: CI=1
+distclean: clean
+	rm -f $(PROOF)/arrays/*Array*.ec
+	find . -name "*_s.ec" -exec rm {} +
+	make -C $(SRC)/ distclean
+
+# -----------------------------------------------------------------------------
+# debug/print rules: helps to check the effects of FILTER or EXCLUDE
+
+debug-print-variables:
+	@echo ""
+	@echo "  SRC: $(SRC)\n"
+	@echo "  PROOF: $(PROOF)\n"
+	@echo "  FILTER: $(FILTER)\n"
+	@echo "  EXCLUDE: $(EXCLUDE)\n"
+	
+	@echo "  EXTRACTED: $(EXTRACTED)\n"
+	@echo "  EXTRACTED_OUT: $(EXTRACTED_OUT)\n"
+	
+	@echo "  ALL: $(ALL)\n"
+	@echo "  ALL_OUT: $(ALL_OUT)\n"
+
+
diff --git a/src/Makefile.common b/src/Makefile.common
index 21a3786..9859746 100644
--- a/src/Makefile.common
+++ b/src/Makefile.common
@@ -43,7 +43,7 @@ endif
 # -----------------------------------------------------------------------------
 # compile vars
 
-JASMIN  ?= jasminc
+JASMIN ?= jasminc
 
 JEXT ?= jazz
 override JFLAGS += -noinsertarraycopy