diff --git a/.github/workflows/amd64-linux-main-proof.yml b/.github/workflows/amd64-linux-main-proof.yml.0
similarity index 100%
rename from .github/workflows/amd64-linux-main-proof.yml
rename to .github/workflows/amd64-linux-main-proof.yml.0
diff --git a/.github/workflows/amd64-linux-main.yml b/.github/workflows/amd64-linux-main.yml.0
similarity index 100%
rename from .github/workflows/amd64-linux-main.yml
rename to .github/workflows/amd64-linux-main.yml.0
diff --git a/.github/workflows/amd64-linux.yml b/.github/workflows/amd64-linux.yml
new file mode 100644
index 00000000..657cfadd
--- /dev/null
+++ b/.github/workflows/amd64-linux.yml
@@ -0,0 +1,81 @@
+name: amd64-linux
+
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+  pull_request:
+
+jobs:
+
+  # extract src
+  extract-src:
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: 'true'
+
+      - name: extract src from submodules
+        run: ./scripts/extract-all.sh
+
+  # src
+  check-safety:
+    needs: extract-src
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: check safety
+        run: make -j$JOBS -C src/ CI=1 check-safety
+      - name: print report
+        run: make -C src/ CI=1 reporter
+      - name: return error
+        run: make -C src/ CI=1 err
+
+  check-sct:
+    needs: extract-src
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: check speculative constant-time (v1)
+        run: make -j$JOBS -C src/ CI=1 check-sct
+      - name: print report
+        run: make -C src/ CI=1 reporter
+      - name: return error
+        run: make -C src/ CI=1 err
+
+  extract-to-easycrypt:
+    needs: extract-src
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: check extraction from Jasmin to EasyCrypt
+        run: make -j$JOBS -C src/ CI=1 extract-to-easycrypt
+      - name: print report
+        run: make -C src/ CI=1 reporter
+      - name: return error
+        run: make -C src/ CI=1 err
+
+  compile-src:
+    needs: extract-src
+    runs-on: [self-hosted, linux, X64, amd64-main]
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: check compilation of libformosa25519.a
+        run: make -j$JOBS -C src/ CI=1 libformosa25519.a
+      - name: print report
+        run: make -C src/ CI=1 reporter
+      - name: return error
+        run: make -C src/ CI=1 err
+
+
diff --git a/build-common/Makefile b/build-common/Makefile
index 27d7314d..fca928f1 100644
--- a/build-common/Makefile
+++ b/build-common/Makefile
@@ -1,127 +1,242 @@
-# -*- Makefile -*-
+# -----------------------------------------------------------------------------
+
+JASMIN ?= jasminc
+
+# -----------------------------------------------------------------------------
 
-# --------------------------------------------------------------------
-AS      ?= as
 CC      ?= clang
 CFLAGS  ?= -O3 -Wall -Wextra -Wpedantic -Wvla -Werror -std=c99 \
 	         -Wundef -Wshadow -Wcast-align -Wpointer-arith -Wmissing-prototypes \
 	         -fstrict-aliasing -fno-common -pipe
+AR      ?= ar
+RANLIB  ?= ranlib
+
+
+# -----------------------------------------------------------------------------
+
+SRC     := .
+PROOF   := $(abspath ../proof)
+SCRIPTS := $(abspath ../scripts)
+FILTER  ?= $(SRC)/crypto_%
+EXCLUDE ?=
 
-JASMIN    ?= jasminc
-JASMIN_CT ?= jasmin-ct
+IMPLEMENTATIONS_FILES ?= $(filter $(FILTER), $(filter-out $(EXCLUDE), $(sort $(shell find $(SRC)/ -name '*.jazz'))))
+IMPLEMENTATIONS_DIRECTORIES := $(dir $(IMPLEMENTATIONS_FILES))
+
+ASSEMBLY_FILES ?= $(IMPLEMENTATIONS_FILES:%.jazz=%.s)
+OBJECT_FILES   := $(ASSEMBLY_FILES:%.s=%.o)
+C_HEADER_FILES ?= $(addsuffix include/api.h, $(dir $(ASSEMBLY_FILES)))
+
+
+# -----------------------------------------------------------------------------
+# when CI=1, information about compilation/checking properties of the files
+# will be stored under .ci/ folders in the implementations directories. Then
+# the user of this Makefile can run 'make CI=1 report' to get a simple report
+# of the current status: compilation, safety checking, and sct checking.
+CI ?= 0
+CI_REMOVE_OK_LOGS ?= "1"
 
-# --------------------------------------------------------------------
-CI      ?= 0
 export CI
-CICL    ?= "1"
 
-# --------------------------------------------------------------------
-LOGS    := libjade-logs-src.tar.gz
 
-EXCLUDE ?=
-SRC     := .
+# -----------------------------------------------------------------------------
+# setting the default rule as 'all': compiles, and checks safety and sct for
+# all implementations
 
-FILTER  ?= $(SRC)/crypto_%
-JAZZ    ?=  $(filter $(FILTER), $(filter-out $(addprefix ./,$(EXCLUDE)), $(sort $(dir $(shell find $(SRC) -name '*.jazz')))))
-SAFETY  ?= $(addsuffix safety, $(JAZZ))
-SCT     ?= $(addsuffix check_sct, $(JAZZ))
-
-SOURCES ?= $(filter-out ./, $(sort $(dir $(shell find $(SRC) -name 'Makefile'))))
-ASM     := $(shell find $(SRC) -name '*.s')
-API     := $(addsuffix include/api.h, $(dir $(ASM)))
-OBJ     := $(ASM:%.s=%.o)
-
-FAIL_ON_ERROR ?= 0
-
-# --------------------------------------------------------------------
-ifeq ($(CI),1)
-.PHONY: backward_compatibility
-backward_compatibility:
-	$(MAKE) default
-	$(MAKE) reporter
-	mv $(LOGS) check.tar.gz
-	$(MAKE) err
-endif
+default: all
+
+
+# -----------------------------------------------------------------------------
+# compile Jasmin implementations to assembly and create libjade.a
 
-# --------------------------------------------------------------------
-.PHONY: libjade.a libjade.h $(JAZZ) clean distclean $(LOGS)
-.INTERMEDIATE: $(OBJ)
+.PHONY: libjade.a libjade.h $(ASSEMBLY_FILES)
 
-default: libjade.a libjade.h
+.INTERMEDIATE: $(OBJECT_FILES)
 
-all: $(JAZZ)
+just_compile: $(ASSEMBLY_FILES)
 
-libjade.a: $(JAZZ)
+libjade.a: $(ASSEMBLY_FILES)
 	$(MAKE) __libjade
 
-__libjade: $(OBJ)
-	ar -rc libjade.a $(OBJ)
-	ranlib libjade.a
-	echo "" | cat - $(API) > libjade.h
+__libjade: $(OBJECT_FILES)
+	$(AR) -rc libjade.a $(OBJECT_FILES)
+	$(RANLIB) libjade.a
+	echo "" | cat - $(C_HEADER_FILES) > libjade.h
 
-$(JAZZ):
-	$(MAKE) -C $@ || !(($(FAIL_ON_ERROR)))
+$(ASSEMBLY_FILES):
+	$(MAKE) -C $(@D) $(@F)
 
-# --------------------------------------------------------------------
 
-SAFETY_TIMEOUT ?= 1440m
-export SAFETY_TIMEOUT
+# -----------------------------------------------------------------------------
+# safety checking
 
-.PHONY: safety
-safety: $(SAFETY)
+CHECK_SAFETY ?= $(addsuffix check-safety, $(IMPLEMENTATIONS_DIRECTORIES))
 
-$(SAFETY):
-	$(MAKE) -C $(@D) $(@F) || true
+CHECK_SAFETY_TIMEOUT ?= 10m
+export CHECK_SAFETY_TIMEOUT
 
-# --------------------------------------------------------------------
-.PHONY: check_sct
-check_sct: $(SCT)
+.PHONY: check-safety $(CHECK_SAFETY)
 
-$(SCT):
-	$(MAKE) -C $(@D) $(@F) || true
+check-safety: $(CHECK_SAFETY)
 
-# --------------------------------------------------------------------
-ifeq ($(CI),1)
+$(CHECK_SAFETY):
+	$(MAKE) -C $(@D) $(@F)
 
-reporter:
-	$(MAKE) reporter_s
-	$(MAKE) $(LOGS)
 
-reporter_s:
-	./../scripts/ci/reporter/jlog "Compilation status" src/ *.s $(CICL)
-	$(MAKE) $(LOGS)
+# -----------------------------------------------------------------------------
+# speculative "constant-time" checking / "secret-independence" checking
+
+CHECK_SCT ?= $(addsuffix check-sct, $(IMPLEMENTATIONS_DIRECTORIES))
+
+.PHONY: check-sct $(CHECK_SCT)
+
+check-sct: $(CHECK_SCT)
+
+$(CHECK_SCT):
+	$(MAKE) -C $(@D) $(@F)
+
+
+# -----------------------------------------------------------------------------
+# extraction to easycrypt (updates proof/ directory)
+
+EXTRACT_TO_EASYCRYPT ?= $(addsuffix extract-to-easycrypt, $(IMPLEMENTATIONS_DIRECTORIES))
+
+.PHONY: extract-to-easycrypt $(EXTRACT_TO_EASYCRYPT)
+
+extract-to-easycrypt: $(EXTRACT_TO_EASYCRYPT)
+
+$(EXTRACT_TO_EASYCRYPT):
+	$(MAKE) -C $(@D) $(@F)
 
-reporter_safety:
-	./../scripts/ci/reporter/jlog "Safety status" src/ *.safety $(CICL)
-	$(MAKE) $(LOGS)
 
-reporter_sct:
-	./../scripts/ci/reporter/jlog "Speculative constant-time status" src/ *.sct $(CICL)
+# -----------------------------------------------------------------------------
+# preprocess-inplace and revert-preprocess-inplace
 
-ERR := $(shell find $(BIN) -name '*.error')
-CIR := $(shell find $(BIN) -name '*.log') $(ERR)
+PREPROCESS_INPLACE ?= $(addsuffix preprocess-inplace, $(IMPLEMENTATIONS_DIRECTORIES))
+
+.PHONY: preprocess-inplace $(PREPROCESS_INPLACE)
+
+preprocess-inplace: $(PREPROCESS_INPLACE)
+
+$(PREPROCESS_INPLACE):
+	$(MAKE) -C $(@D) $(@F)
+
+
+REVERT_PREPROCESS_INPLACE ?= $(addsuffix revert-preprocess-inplace, $(IMPLEMENTATIONS_DIRECTORIES))
+
+.PHONY: preprocess-inplace $(REVERT_PREPROCESS_INPLACE)
+
+revert-preprocess-inplace: $(REVERT_PREPROCESS_INPLACE)
+
+$(REVERT_PREPROCESS_INPLACE):
+	$(MAKE) -C $(@D) $(@F)
+
+
+# -----------------------------------------------------------------------------
+# reporter: this section defines rules for reporting the current implementation
+# status
+
+LOGS ?= libjade-logs-src.tar.gz
+JLOG := $(SCRIPTS)/reporter/jlog
+
+CI_ERROR_FILES := $(shell find $(SRC) -name '*.error')
+CI_ALL_FILES   := $(shell find $(SRC) -name '*.log') $(CI_ERROR_FILES)
+
+.PHONY: reporter logs $(LOGS) err
+
+reporter:
+	$(JLOG) "Safety checking status" src/ *.safety $(CI_REMOVE_OK_LOGS)
+	$(JLOG) "Speculative constant-time status" src/ *.sct $(CI_REMOVE_OK_LOGS)
+	$(JLOG) "Extraction to EasyCrypt status" src/ *.ec $(CI_REMOVE_OK_LOGS)
+	$(JLOG) "Compilation status (*.jazz -> *.s)" src/ *.s $(CI_REMOVE_OK_LOGS)
+
+logs: $(LOGS)
 
 $(LOGS):
 	@$(JASMIN) -version > notes
-ifeq ($(words $(CIR)),0)
-	@echo "good job." >> 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 $(CIR)
+	@tar -zcvf $@ notes $(CI_ALL_FILES)
 endif
 	@rm notes
 
 err:
-ifneq ($(words $(ERR)),0)
-	$(error $(ERR))
+ifneq ($(words $(CI_ERROR_FILES)),0)
+	$(error $(CI_ERROR_FILES))
 endif
 
-endif
 
-# --------------------------------------------------------------------
+# -----------------------------------------------------------------------------
+# to run 'everything': $ make -j$(nproc) all
+.PHONY: all
+
+all: CI=1
+all:
+	$(MAKE) distclean
+	$(MAKE) check-safety
+	$(MAKE) check-sct
+	$(MAKE) extract-to-easycrypt
+	$(MAKE) libjade.a
+	$(MAKE) libjade.h
+	$(MAKE) reporter
+	$(MAKE) err
+
+all-with-preprocess-inplace: CI=1
+all-with-preprocess-inplace:
+	$(MAKE) distclean
+	$(MAKE) preprocess-inplace
+	$(MAKE) check-safety
+	$(MAKE) check-sct
+	$(MAKE) extract-to-easycrypt
+	$(MAKE) libjade.a
+	$(MAKE) libjade.h
+	$(MAKE) reporter
+	$(MAKE) err
+
+
+# -----------------------------------------------------------------------------
+# clean rules
+
+.PHONY: clean distclean
+
 clean:
-	rm -f libjade.a libjade.h $(LOGS) check.tar.gz
+	rm -f libjade.a libjade.h
+	rm -f $(LOGS)
+	for i in $(IMPLEMENTATIONS_DIRECTORIES); do $(MAKE) -C $$i clean; done
+	rm -f $(PROOF)/arrays/*Array*.ec
 
 distclean: clean
-	for i in $(SOURCES); do $(MAKE) -C $$i clean; done
+
+
+# -----------------------------------------------------------------------------
+# printing section
+.PHONY: print-available-implementations
+
+print-available-implementations:
+	@for i in $(IMPLEMENTATIONS_DIRECTORIES:./%=%); do echo $$i; done
+
+
+# -----------------------------------------------------------------------------
+# 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 "  IMPLEMENTATIONS_DIRECTORIES: $(IMPLEMENTATIONS_DIRECTORIES)\n"
+	@echo "  IMPLEMENTATIONS_FILES: $(IMPLEMENTATIONS_FILES)\n"
+	
+	@echo "  ASSEMBLY_FILES: $(ASSEMBLY_FILES)\n"
+	@echo "  OBJECT_FILES: $(OBJECT_FILES)\n"
+	@echo "  C_HEADER_FILES: $(C_HEADER_FILES)\n"
+	
+	@echo "  CHECK_SAFETY: $(CHECK_SAFETY)\n"
+	@echo "  CHECK_SCT: $(CHECK_SCT)\n"
+	@echo "  EXTRACT_TO_EASYCRYPT: $(EXTRACT_TO_EASYCRYPT)\n"
+	
+	@echo "  LOGS: $(LOGS)\n"
 
diff --git a/build-common/Makefile.checksafety b/build-common/Makefile.checksafety
index 27814f33..9f9ac143 100644
--- a/build-common/Makefile.checksafety
+++ b/build-common/Makefile.checksafety
@@ -1,38 +1,44 @@
-# Notes:
-# - this file defines fine-grained targets that allow checking the safety of individual exported
-#   functions
-# - it is meant to be included by Makefile.common, right before the 'generic' safety targets
+# -----------------------------------------------------------------------------
 
 ifneq ($(OP),)
 
 SAFETY_FLAGS   ?=
-SAFETY_TIMEOUT ?= 4320m
-SAFETY_DIR     := .safety
-CHECK_SAFETY_S  = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC) -slice $* -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$*.safetyparam)  $< 2> $@) $(CIT)
-CHECK_SAFETY    = (time timeout -v $(SAFETY_TIMEOUT) $(JASMINC)           -checksafety $(SAFETY_FLAGS) $(shell cat $(SAFETY_DIR)/$(OP).safetyparam)  $< 2> $@) $(CIT)
+SAFETY_TIMEOUT ?= 10m
 
-SAFETY_TARGETS  = $(addsuffix .safety, $(FUNCTIONS))
+CHECK_SAFETY_SLICE         = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -slice $* -checksafety $(SAFETY_FLAGS) $< 2> $@) $(CI_CMD)
+CHECK_SAFETY_SLICE_STDOUT  = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE) -slice $* -checksafety $(SAFETY_FLAGS) $<      ) $(CI_CMD)
 
-checksafety-all: $(SAFETY_TARGETS)
+CHECK_SAFETY               = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE)           -checksafety $(SAFETY_FLAGS) $< 2> $@) $(CI_CMD)
+CHECK_SAFETY_STDOUT        = (time timeout -v $(SAFETY_TIMEOUT) $(JASMIN) $(JINCLUDE)           -checksafety $(SAFETY_FLAGS) $<      ) $(CI_CMD)
 
-$(OP).safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/$(OP).safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR)
+SAFETY_TARGETS             = $(addsuffix .safety, $(FUNCTIONS))
+SAFETY_TARGETS_STDOUT      = $(addsuffix .stdout, $(SAFETY_TARGETS))
+
+# -----------------------------------------------------------------------------
+
+check-safety: $(SAFETY_TARGETS)
+
+$(OP).safety: $(OP).jazz $(DEPS_DIR)/$(OP).safety.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
 	$(CHECK_SAFETY)
 
+$(OP).safety.stdout: $(OP).jazz $(DEPS_DIR)/$(OP).safety.d | $(CI_DIR)
+	$(DEPS)
+	$(CHECK_SAFETY_STDOUT)
+
+# --
+
 $(SAFETY_TARGETS):
-%.safety : $(OP).jazz $(SAFETY_DIR)/$(OP).safetyparam $(DEPS_DIR)/%.safety.d | $(SAFETY_DIR) $(DEPS_DIR) $(CI_DIR)
+%.safety: $(OP).jazz $(DEPS_DIR)/%.safety.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
-	$(CHECK_SAFETY_S)
+	$(CHECK_SAFETY_SLICE)
+
+%.safety.stdout: $(OP).jazz | $(DEPS_DIR) $(CI_DIR)
+	$(DEPS)
+	$(CHECK_SAFETY_SLICE_STDOUT)
 
 DEPFILES := \
  $(DEPFILES) \
  $(addprefix $(DEPS_DIR)/, $(addsuffix .safety.d, $(FUNCTIONS) $(OP)))
 
-$(SAFETY_DIR)/$(OP).safetyparam: $(SAFETY_DIR)
-	$(MAKE) -C $(TEST) bin/$(RDIR)/safetyparams
-	(cd $(SAFETY_DIR) && $(TDIR)/safetyparams)
-
-$(SAFETY_DIR): ; @mkdir -p $@
-
 endif
-
diff --git a/build-common/Makefile.checksct b/build-common/Makefile.checksct
index 2168ccfb..ecb7a377 100644
--- a/build-common/Makefile.checksct
+++ b/build-common/Makefile.checksct
@@ -1,47 +1,46 @@
-# Notes:
-# - this file defines fine-grained targets that allow checking the speculative constant-time of individual exported
-#   functions
-# - it is meant to be included by Makefile.common
+# -----------------------------------------------------------------------------
 
-# JASMIN_CT belongs here (and not Makefile.common): some options differ from jasminc
 JASMIN_CT ?= jasmin-ct
 
+# -----------------------------------------------------------------------------
+
 ifneq ($(OP),)
 
-# TODO: remove --infer and annotate exported functions
-SCT_FLAGS  ?= --infer
+SCT_FLAGS ?= --infer
 
-CHECK_SCT_SLICE        = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CIT)
-CHECK_SCT_SLICE_STDOUT = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $<          ) $(CIT)
+CHECK_SCT_SLICE        = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CI_CMD)
+CHECK_SCT_SLICE_STDOUT = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT) --slice $* --sct $(SCT_FLAGS) $<          ) $(CI_CMD)
 
-CHECK_SCT              = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT)            --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CIT)
-CHECK_SCT_STDOUT       = (JASMINPATH="Jade=$(SRC)" $(JASMIN_CT)            --sct $(SCT_FLAGS) $<          ) $(CIT)
+CHECK_SCT              = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT)            --sct $(SCT_FLAGS) $< > $@ 2>&1) $(CI_CMD)
+CHECK_SCT_STDOUT       = (JASMINPATH="formosa25519=$(SRC)" $(JASMIN_CT)            --sct $(SCT_FLAGS) $<          ) $(CI_CMD)
 
 SCT_TARGETS         = $(addsuffix .sct, $(FUNCTIONS))
 SCT_TARGETS_STDOUT  = $(addsuffix .stdout, $(SCT_TARGETS))
 
-check_sct: $(SCT_TARGETS)
 
-$(OP).sct : $(OP).jazz $(DEPS_DIR)/$(OP).sct.d | $(DEPS_DIR) $(CI_DIR)
+# -----------------------------------------------------------------------------
+check-sct: $(SCT_TARGETS)
+
+$(OP).sct: $(OP).jazz $(DEPS_DIR)/$(OP).sct.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
 	$(CHECK_SCT)
 
-$(OP).sct.stdout : $(OP).jazz | $(CI_DIR)
+$(OP).sct.stdout: $(OP).jazz | $(CI_DIR)
 	$(CHECK_SCT_STDOUT)
 
+# --
+
 $(SCT_TARGETS):
-%.sct : $(OP).jazz $(DEPS_DIR)/%.sct.d | $(DEPS_DIR) $(CI_DIR)
+%.sct: $(OP).jazz $(DEPS_DIR)/%.sct.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
 	$(CHECK_SCT_SLICE)
 
 $(SCT_TARGETS_STDOUT):
-%.sct.stdout : $(OP).jazz | $(CI_DIR)
+%.sct.stdout: $(OP).jazz | $(CI_DIR)
 	$(CHECK_SCT_SLICE_STDOUT)
 
 DEPFILES := \
  $(DEPFILES) \
  $(addprefix $(DEPS_DIR)/, $(addsuffix .sct.d, $(FUNCTIONS) $(OP)))
 
-$(SCT_DIR): ; @mkdir -p $@
-
 endif
diff --git a/build-common/Makefile.common b/build-common/Makefile.common
index c27a291c..0d621b8e 100644
--- a/build-common/Makefile.common
+++ b/build-common/Makefile.common
@@ -1,107 +1,183 @@
+# -----------------------------------------------------------------------------
+# paths vars
 
-# --------------------------------------------------------------------
-TOP   = $(abspath $(dir $(filter %Makefile.common,$(MAKEFILE_LIST)))../)
-SRC   = $(TOP)/src/
-BC    = $(TOP)/build-common/
-TEST  = $(TOP)/test/
-PROOF = $(TOP)/proof/
-
-CDIR  = $(abspath $(dir $(abspath $(firstword $(MAKEFILE_LIST)))))
-RDIR  = $(subst $(SRC),,$(CDIR))
-TDIR  = $(TEST)bin/$(RDIR)
-PDIR  = $(PROOF)$(RDIR)
-
-# OPERATION: crypto_kem, crypto_hash, ..., common; OP is a shorthand for OPERATION
-OPERATION = $(word 1, $(subst /, ,$(RDIR)))
-OP        = $(word 2, $(subst _, , $(OPERATION)_))
-NAMESPACE = $(subst crypto_,jade_, $(subst -,_,$(subst /,_,$(RDIR))))
+PROJECT_DIR = $(abspath $(dir $(filter %Makefile.common,$(MAKEFILE_LIST)))../)
+PROJECT_PARENT_DIR = $(abspath $(PROJECT_DIR)/../)
 
-# --------------------------------------------------------------------
+BUILD_COMMON = $(PROJECT_DIR)/build-common
+SRC          = $(PROJECT_DIR)/src
+TEST         = $(PROJECT_DIR)/test
+PROOF        = $(PROJECT_DIR)/proof
 
-include $(BC)/Makefile.functions
+ABS_IMPLEMENTATION_DIR = $(abspath $(dir $(abspath $(firstword $(MAKEFILE_LIST)))))
+REL_IMPLEMENTATION_DIR = $(subst $(SRC)/,,$(ABS_IMPLEMENTATION_DIR))
+
+
+# -----------------------------------------------------------------------------
+# implementation vars
+
+OP        = $(word 2, $(subst _, , $(word 1, $(subst /, ,$(REL_IMPLEMENTATION_DIR)))))
+NAMESPACE = $(subst crypto_,jade_, $(subst -,_,$(subst /,_,$(REL_IMPLEMENTATION_DIR))))
+
+ifeq ($(OP),kem)
+ifeq ($(SRCS),kem.jazz)
+FUNCTIONS = $(addprefix $(NAMESPACE)_, keypair_derand keypair enc_derand enc dec)
+endif
+endif
+
+ifeq ($(OP),hash)
+ifeq ($(SRCS),hash.jazz)
+FUNCTIONS = $(NAMESPACE)
+endif
+endif
+
+ifeq ($(OP),onetimeauth)
+ifeq ($(SRCS),onetimeauth.jazz)
+FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_verify
+endif
+endif
+
+ifeq ($(OP),scalarmult)
+ifeq ($(SRCS),scalarmult.jazz)
+FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_base
+endif
+endif
+
+ifeq ($(OP),secretbox)
+ifeq ($(SRCS),secretbox.jazz)
+FUNCTIONS = $(NAMESPACE) $(NAMESPACE)_open
+endif
+endif
+
+ifeq ($(OP),sign)
+ifeq ($(SRCS),sign.jazz)
+FUNCTIONS = $(NAMESPACE)_keypair $(NAMESPACE) $(NAMESPACE)_open
+endif
+endif
+
+ifeq ($(OP),xof)
+ifeq ($(SRCS),xof.jazz)
+FUNCTIONS = $(NAMESPACE)
+endif
+endif
+
+
+# -----------------------------------------------------------------------------
+# ci vars
 
-# --------------------------------------------------------------------
 CI_DIR =
-CIT =
+CI_CMD =
 ifeq ($(CI),1)
 CI_DIR := .ci
-CIT = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \
-     (echo $$? > $(CI_DIR)/$(@F).error && \
-      cat $(CI_DIR)/$(@F).log >> $(CI_DIR)/$(@F).error && \
-      rm $(CI_DIR)/$(@F).log && \
-      exit 127)
+CI_CMD = 2> $(CI_DIR)/$(@F).log && rm -f $(CI_DIR)/$(@F).error || \
+             (echo $$? | cat - $(CI_DIR)/$(@F).log > $(CI_DIR)/$(@F).error && \
+              rm $(CI_DIR)/$(@F).log && \
+              exit 127 \
+             )
 endif
 
-# --------------------------------------------------------------------
-JEXT    ?= jazz
-override JFLAGS += -noinsertarraycopy $(addprefix -slice ,$(FUNCTIONS))
-JINCLUDE = -I Jade:$(SRC)
 
-JASMIN  ?= jasminc
-JASMINC := $(JASMIN) $(JFLAGS) $(JINCLUDE)
-COMPILE  = ($(JASMINC) -o $@ $<) $(CIT)
+# -----------------------------------------------------------------------------
+# compile vars
 
-# --------------------------------------------------------------------
-CHECKS_DIR := checks
+JASMIN ?= jasminc
 
-# --------------------------------------------------------------------
-DEPS_DIR := .deps
-DEPS = ((printf "$@: "; printf "$< "; $(JASMINC) -print-dependencies $<) > $(DEPS_DIR)/$(@F).d) $(CIT)
-DEPFILES :=
+JEXT ?= jazz
+override JFLAGS += -stack-zero loopSCT -noinsertarraycopy
+JINCLUDE ?= -I formosa25519:$(SRC)
 
-# --------------------------------------------------------------------
-compile: $(SRCS:%.$(JEXT)=%.s)
-	@true
+JASMIN_COMPILE = ($(JASMIN) $(JFLAGS) $(JINCLUDE) -o $@ $<) $(CI_CMD)
 
-# --------------------------------------------------------------------
-# Note: by using a single-file extraction, only one Jasmin file can be processed (the first from SRCS)
+ASSEMBLY_FILES = $(SRCS:%.$(JEXT)=%.s)
 
-extract: $(EC_DIR)/extracted_s.ec $(EC_DIR)/extracted_ct.ec
-	@true
 
-$(EC_DIR)/extracted_s.ec : $(SRCS) $(DEPS_DIR)/extracted_s.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
-	$(DEPS)
-	$(EXTRACT_S)
+# preprocessing vars
 
-$(EC_DIR)/extracted_ct.ec : $(SRCS) $(DEPS_DIR)/extracted_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
-	$(DEPS)
-	$(EXTRACT_CT)
+JPP ?= $(PROJECT_DIR)/scripts/releaser/jpp
+PREPROCESSED_FILES := $(SRCS:%.$(JEXT)=%.jpp)
+JASMIN_PREPROCESS = ($(JPP) $(JINCLUDE) -b $(PROJECT_PARENT_DIR)/ -out $@ -in $<) $(CI_CMD)
 
-# --------------------------------------------------------------------
 
-extract0: extract_s extract_ct
-	@true
+# -----------------------------------------------------------------------------
+# extraction vars
 
-extract_s: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_s.ec)
-	@true
+EXTRACT_DIR = $(PROOF)/$(REL_IMPLEMENTATION_DIR)
+EXTRACT_ARRAY_DIR = $(PROOF)/arrays
+EFLAGS ?= $(addprefix -ec , $(FUNCTIONS)) 
+
+JASMIN_EXTRACT = (cd $(EXTRACT_DIR) && $(JASMIN) $(JINCLUDE) $(EFLAGS) -oecarray $(EXTRACT_ARRAY_DIR) -oec $(notdir $@) $(ABS_IMPLEMENTATION_DIR)/$<) $(CI_CMD)
+
+EASYCRYPT_FILES = $(SRCS:%.$(JEXT)=$(EXTRACT_DIR)/%_s.ec)
+
+
+# -----------------------------------------------------------------------------
+# dependencies vars
+
+DEPS_DIR ?= .deps
+DEPS = ((printf "$@: "; printf "$< "; $(JASMIN) $(JINCLUDE) -print-dependencies $<) > $(DEPS_DIR)/$(@F).d) $(CI_CMD)
+DEPFILES ?=
 
-extract_ct: $(SRCS:%.$(JEXT)=$(EC_DIR)/%_ct.ec)
+
+# -----------------------------------------------------------------------------
+# default rule
+
+default: compile
+
+
+# -----------------------------------------------------------------------------
+# preprocess rules
+
+preprocess: $(PREPROCESSED_FILES)
 	@true
 
-%.s : %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR)
+$(PREPROCESSED_FILES):
+%.jpp: %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
-	$(COMPILE)
+	$(JASMIN_PREPROCESS)
+
+preprocess-inplace: preprocess
+	for file in $(SRCS); do mv $${file%.$(JEXT)}.jpp $$file; done
+
+revert-preprocess-inplace:
+	for file in $(SRCS); do git checkout $$file; done
+
+# -----------------------------------------------------------------------------
+# compilation rules
+
+compile: $(ASSEMBLY_FILES)
+	@true
 
-$(EC_DIR)/%_s.ec : %.$(JEXT) $(DEPS_DIR)/%_s.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
+$(ASSEMBLY_FILES):
+%.s: %.$(JEXT) $(DEPS_DIR)/%.s.d | $(DEPS_DIR) $(CI_DIR)
 	$(DEPS)
-	$(EXTRACT_S)
+	$(JASMIN_COMPILE)
+
+
+# -----------------------------------------------------------------------------
+# extraction rules
+
+extract-to-easycrypt: $(EASYCRYPT_FILES)
+	@true
 
-$(EC_DIR)/%_ct.ec : %.$(JEXT) $(DEPS_DIR)/%_ct.ec.d | $(DEPS_DIR) $(EC_DIR) $(CI_DIR)
+$(EASYCRYPT_FILES):
+$(EXTRACT_DIR)/%_s.ec : %.$(JEXT) $(DEPS_DIR)/%_s.ec.d | $(DEPS_DIR) $(EXTRACT_DIR) $(EXTRACT_ARRAY_DIR) $(CI_DIR)
 	$(DEPS)
-	$(EXTRACT_CT)
+	$(JASMIN_EXTRACT)
 
-# --------------------------------------------------------------------
 
-include $(BC)/Makefile.checksafety
+# -----------------------------------------------------------------------------
+# include Makefiles for checking implementations' properties
 
-# --------------------------------------------------------------------
+include $(BUILD_COMMON)/Makefile.checksafety
+include $(BUILD_COMMON)/Makefile.checksct
 
-include $(BC)/Makefile.checksct
 
-# --------------------------------------------------------------------
-$(CHECKSDIR): ; @mkdir -p $@
+# -----------------------------------------------------------------------------
+# directories
+
 $(DEPS_DIR): ; @mkdir -p $@
-$(EC_DIR): ; @mkdir -p $@; touch $@/.gitkeep
+$(EXTRACT_DIR): ; @mkdir -p $@; touch $@/.gitkeep
+$(EXTRACT_ARRAY_DIR): ; @mkdir -p $@; touch $@/.gitkeep
 ifeq ($(CI),1)
 $(CI_DIR): ; @mkdir -p $@
 endif
@@ -109,26 +185,70 @@ endif
 DEPFILES := \
  $(DEPFILES) \
  $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%.s.d) \
- $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_s.ec.d) \
- $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_ct.ec.d) \
- $(DEPS_DIR)/extracted_s.ec.d \
- $(DEPS_DIR)/extracted_ct.ec.d
+ $(SRCS:%.$(JEXT)=$(DEPS_DIR)/%_s.ec.d)
 
 $(DEPFILES):
 
 include $(wildcard $(DEPFILES))
 
-# --------------------------------------------------------------------
-.PHONY: .jflags
-.jflags:
-	@echo -n "$(JFLAGS)" > .jflags
+
+# -----------------------------------------------------------------------------
+# the following rule records the flags used to compile the implementation
+# these are used by the release script
+
+.PHONY: .JFLAGS
+.JFLAGS:
+	@echo -n "$(JFLAGS)" > .JFLAGS
+
 
 # --------------------------------------------------------------------
-.PHONY: clean
+.PHONY: clean distclean
 
 clean:
-	@rm -fr $(DEPS_DIR) $(CHECKS_DIR) $(SAFETY_DIR) *.s *.safety* *.sct* *.o *.a .jflags *.out
-ifeq ($(CI),1)
-	@rm -fr $(CI_DIR)
-endif
+	rm -fr $(CI_DIR) $(DEPS_DIR) *.jpp *.s *.safety* *.sct* *.o .JFLAGS
+
+distclean: clean
+	rm -fr $(EASYCRYPT_FILES)
+
+# --------------------------------------------------------------------
+debug-print-variables:
+	@echo ""
+	@echo "Path variables:"
+	@echo "  PROJECT_DIR: $(PROJECT_DIR)"
+	@echo "  SRC: $(SRC)"
+	@echo "  TEST: $(TEST)"
+	@echo "  PROOF: $(PROOF)"
+	@echo "  ABS_IMPLEMENTATION_DIR: $(ABS_IMPLEMENTATION_DIR)"
+	@echo "  REL_IMPLEMENTATION_DIR: $(REL_IMPLEMENTATION_DIR)"
+	@echo ""
+	@echo "Implementation variables:"
+	@echo "  OP: $(OP)"
+	@echo "  NAMESPACE: $(NAMESPACE)"
+	@echo "  FUNCTIONS: $(FUNCTIONS)"
+	@echo ""
+	@echo "CI variables:"
+	@echo "  CI_DIR: $(CI_DIR)"
+	@echo "  CI_CMD: not printed, it is rule dependent."
+	@echo ""
+	@echo "Compilation variables:"
+	@echo "  JASMIN: $(JASMIN)"
+	@echo "  JEXT: $(JEXT)"
+	@echo "  JFLAGS: $(JFLAGS)"
+	@echo "  JINCLUDE: $(JINCLUDE)"
+	@echo "  SRCS: $(SRCS)"
+	@echo "  ASSEMBLY_FILES: $(ASSEMBLY_FILES)"
+	@echo "  JASMIN_COMPILE: not printed, it is rule dependent."
+	@echo ""
+	@echo "Preprocess variables:"
+	@echo "  JPP: $(JPP)"
+	@echo "  PREPROCESSED_FILES: $(PREPROCESSED_FILES)"
+	@echo "  JASMIN_PREPROCESS: not printed, it is rule dependent."
+	@echo ""
+	@echo "Extraction variables:"
+	@echo "  EXTRACT_DIR: $(EXTRACT_DIR)"
+	@echo "  EXTRACT_ARRAY_DIR: $(EXTRACT_ARRAY_DIR)"
+	@echo "  EFLAGS: $(EFLAGS)"
+	@echo "  EASYCRYPT_FILES: $(EASYCRYPT_FILES)"
+	@echo "  JASMIN_EXTRACT: not printed, it is rule dependent."
+	@echo ""
 
diff --git a/proof/.gitignore b/proof/.gitignore
index 837893af..582c0c2c 100644
--- a/proof/.gitignore
+++ b/proof/.gitignore
@@ -3,3 +3,4 @@
 *_ct.ec
 *.ec.out
 *Array*.ec
+arrays/
diff --git a/scripts/extract-all.sh b/scripts/extract-all.sh
index 3b997727..160d49aa 100755
--- a/scripts/extract-all.sh
+++ b/scripts/extract-all.sh
@@ -30,3 +30,5 @@ for SUBMODULE in "$LIBJADE_ROOT"/submodules/formosa-*;do
     fi
   done
 done
+
+echo "include ../build-common/Makefile" > "$LIBJADE_SRC/Makefile"
diff --git a/scripts/reporter/jlog b/scripts/reporter/jlog
new file mode 100755
index 00000000..504cc54c
--- /dev/null
+++ b/scripts/reporter/jlog
@@ -0,0 +1,72 @@
+#!/usr/bin/env bash
+
+message=$1
+top=$(cd "$(dirname "$0")/../../" ; pwd -P)
+dir=$top/$2
+spattern=$3
+rempty=$4
+
+NORMAL="\e[0m"
+BOLD="\e[1m"
+RED="\e[31m"
+GREEN="\e[32m"
+YELLOW='\e[33m'
+
+# given a pattern (for instance, *.TAG.log or *.TAG.error) and an output file
+# - prints to $output the line counts for each *.TAG.log, sorted by the number of lines
+status()
+{
+  pattern=$1;
+  output=$2;
+
+  find $dir -name $pattern | \
+  while read file; do
+   d=$(dirname $file);
+   b=$(basename $file);
+   c=$(wc -l <$file);
+   echo "$c, $d/$b";
+  done | \
+  sort -t',' -g -k1 | sed -e 's/^[ \t]*//' -e 's/, \.\//, /' > $output
+}
+
+print()
+{
+  color=$1;
+  filter=$2;
+  file=$3;
+  label=$4;
+
+  egrep -E "$filter" $file | \
+  while read line; do
+   echo -e "${color}${BOLD}${label}, ${line}${NORMAL}"
+  done
+}
+
+clear_empty()
+{
+  file=$1;
+  egrep -E "^0" $file | cut -d',' -f2 | \
+  while read log; do
+    rm -f "$log";
+  done
+}
+
+warning=$(mktemp)
+error=$(mktemp)
+
+status "${spattern}.log" $warning;
+status "${spattern}.error" $error;
+
+# print
+echo -e "${BOLD}$message: ${NORMAL}"
+
+print $GREEN "^0" $warning "OK";
+print $YELLOW "^[^0]" $warning "WARNING";
+print $RED "" $error "ERROR";
+
+if [ "$rempty" == "1" ]; then
+  clear_empty $warning;
+fi
+
+rm $warning $error
+