CI: get jasminc & eclib from the same repo ; check correctness proof using easycrypt runtest

Author: ruipedro16

Dockerfile

@@ -5,8 +5,9 @@ LABEL maintainer="[email protected]"
 
 ARG USER="xmss-user"
 
-ARG ECLIB_COMMIT=14d8b2e2b2a3b4ccdb6366781d371afd0ac49bde
 ARG EASYCRYPT_RELEASE=r2025.02 
+
+# We dont use a Jasmin release because it doesnt't have jasmin2ec
 ARG JASMIN_COMMIT=4ab734290304bf832095a3939032678169f114d8
 
 SHELL ["/bin/bash", "-c"]
@@ -58,20 +59,15 @@ RUN eval $(opam env) && \
     opam depext easycrypt && \
     opam install easycrypt && \
     easycrypt why3config
-    
-# Download ECLib
-RUN git clone https://github.com/jasmin-lang/jasmin.git jasmin-eclib && \
-    cd jasmin-eclib && \    
-    git checkout ${ECLIB_COMMIT} && \
-    echo -e "[general]\nidirs = Jasmin:$(pwd)/eclib" > ~/.config/easycrypt/easycrypt.conf
 
-# Install Jasmin
+# Install Jasmin & set ECLib
 RUN git clone https://gitlab.com/jasmin-lang/jasmin-compiler.git jasmin-compiler && \
     cd jasmin-compiler && git checkout ${JASMIN_COMMIT} && \
     USER=$USER source /home/$USER/.nix-profile/etc/profile.d/nix.sh && \
     nix-channel --update && \
     cd compiler/ && nix-shell --command "make" && \
-    sudo install -D jasmin* /usr/local/bin/
+    sudo install -D jasmin* /usr/local/bin/ && \
+    cd - && echo -e "[general]\nidirs = Jasmin:$(pwd)/eclib" > ~/.config/easycrypt/easycrypt.conf
 
 COPY --chown=$USER:$USER . /home/$USER/xmss-jasmin
 WORKDIR /home/$USER/xmss-jasmin

proof/Makefile

@@ -6,9 +6,7 @@ EC_FLAGS   ?= -timeout 20 ${ECADDFLAGS}
 
 JASMIN2EC        ?= jasmin2ec
 JASMIN2EC_FLAGS  ?= --array-model=old
-
-JPP          := ../submodules/jasmin-preprocessor/jpp
-PREPROCESSOR := ../submodules/jasmin-preprocessor/preprocessor
+JPATH            := JASMINPATH="XMSS=../ref-jasmin:Stdlib=../ref-jasmin/stdlib"
 
 # --------------------------------------------------------------------------------------------------
 
@@ -26,8 +24,11 @@ extract: extraction/XMSS_IMPL.ec
 common/Array8.ec: | common/
 	printf "from Jasmin require import JArray.\n\nclone export PolyArray as Array8  with op size <- 8.\n" > $@
 
-extraction/XMSS_IMPL.ec: extraction/XMSS_IMPL.jazz | common/
-	$(JASMIN2EC) $(JASMIN2EC_FLAGS) $< -o $@
+extraction/XMSS_IMPL.ec: ../ref-jasmin/xmss/xmss.jinc | common/
+	printf "from XMSS require \"params/params-xmssmt-sha2_20_2_256.jinc\"" > tmp
+	cat $< >> tmp
+	$(JPATH) $(JASMIN2EC) $(JASMIN2EC_FLAGS) tmp -o $@
+	-$(RM) tmp
 	mv extraction/WArray* common/
 	mv extraction/Array* common/
 
@@ -53,17 +54,8 @@ check_extraction: extraction/XMSS_IMPL.ec
 
 ################################### correctness proof ##############################################
 
-# The targets check_c_* are used to check the correctness proof files
-# FIXME: Why are these individual jobs rather than a single runtest scenario?
-# TODO: After checking for Chesterton's fence, replace this entire section with
-# check_correctness_proof: extraction/XMSS_IMPL.ec
-#   $(ECRUNTEST) config/tests.config correctness
-check_c_%: extraction/XMSS_IMPL.ec
-	$(EASYCRYPT) $(EC_FLAGS) correctness/$*.ec
-
-CORRECTNESS_PROOF_FILES := $(addprefix check_c_, $(notdir $(basename $(wildcard correctness/*.ec))))
-
-check_correctness_proof: extraction/XMSS_IMPL.ec $(CORRECTNESS_PROOF_FILES)
+check_correctness_proof: extraction/XMSS_IMPL.ec
+	$(ECRUNTEST) config/tests.config correctness
 
 ####################################################################################################