adjustments for the external CI

- the spec relies on Array8 which is was ignored.

Author: ruipedro16

.gitignore

@@ -1,5 +1,4 @@
 .vscode
 venv
 
-proof/extraction/*.ec
-proof/common/
+proof/extraction/*.ec

proof/Makefile

@@ -21,9 +21,6 @@ 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: ../ref-jasmin/xmss/xmss.jinc | common/
 	printf "from XMSS require \"params/params-xmssmt-sha2_20_2_256.jinc\"" > tmp
 	cat $< >> tmp
@@ -34,27 +31,27 @@ extraction/XMSS_IMPL.ec: ../ref-jasmin/xmss/xmss.jinc | common/
 
 # --------------------------------------------------------------------------------------------------
 
-check_xmss_common_spec: common/Array8.ec
+check_xmss_common_spec: 
 	$(ECRUNTEST) config/tests.config common-spec
 
-check_xmss_spec: common/Array8.ec
+check_xmss_spec: 
 	$(ECRUNTEST) config/tests.config xmss-spec
 
-check_xmss_mt_spec: common/Array8.ec
+check_xmss_mt_spec: 
 	$(ECRUNTEST) config/tests.config xmss-mt-spec
 
 # FIXME: This is currently not checked
-check_xmss_spec_extra: common/Array8.ec
+check_xmss_spec_extra: 
 	$(ECRUNTEST) config/tests.config xmss-spec-extra
 
-check_spec: common/Array8.ec check_xmss_common_spec check_xmss_spec check_xmss_mt_spec
+check_spec:  check_xmss_common_spec check_xmss_spec check_xmss_mt_spec
 
 check_extraction: extraction/XMSS_IMPL.ec
 	$(ECRUNTEST) config/tests.config extraction
 
 ################################### correctness proof ##############################################
 
-check_correctness_proof: extraction/XMSS_IMPL.ec common/Array8.ec
+check_correctness_proof: extraction/XMSS_IMPL.ec 
 	$(ECRUNTEST) config/tests.config correctness
 
 ####################################################################################################
@@ -67,7 +64,7 @@ check_security_proof:
 ####################################################################################################
 
 # FIXME: This would currently be subsumed by the xmss-spec-extra target, if activated
-check_xmss_xmssmt_proof: common/Array8.ec
+check_xmss_xmssmt_proof: 
 	$(EASYCRYPT) $(EC_FLAGS) spec/extra/XMSS_vs_XMSS_MT.ec
 
 check_proofs: check_xmss_xmssmt_proof check_correctness_proof check_security_proof
@@ -100,6 +97,3 @@ distclean:
 extraction/:
 	mkdir -p $@
 
-
-common/:
-	mkdir -p $@

proof/common/Array8.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JArray.
+
+clone export PolyArray as Array8  with op size <- 8.

proof/spec/extra/SpecSecurity.ec

@@ -7,6 +7,8 @@ import Params Types XMSS_Types Hash WOTS Address LTree BaseW.
 
 (* Get checksum from XMXX_Checksum and then plug those results
    here *)
+
+(*
 clone import XMSS_TW as XMSS_ABSTRACT with
    type mseed <- nbytes,
    op dmseed <- (dmap ((dlist W8.dword n)) NBytes.insubd),
@@ -81,3 +83,4 @@ equiv ver_eq : XMSS_TW(FakeRO).verify ~ XMSS_PRF.verify : pkrel pk{1} pk{2} /\ =
 proc. 
 admitted.
 
+*)