gimli proofs: adapt to new leakage extraction

.gitlab-ci.yml

@@ -178,7 +178,13 @@ check-proofs:
   stage: test
   parallel:
     matrix:
-      - EASYCRYPT_REF: [release, dev]
+      # Use CTG for easycrypt release, since for checking CT, it need a patch
+      # that is not in the release for now (2024-12-13).
+      - EASYCRYPT_REF: release
+        CT_MODE: CTG
+      - EASYCRYPT_REF: dev
+        CT_MODE: CT
+
   variables:
     EXTRA_NIX_ARGUMENTS: --arg testDeps true --argstr ecRef $EASYCRYPT_REF
     WHY3_CONF: $CI_PROJECT_DIR/why3.conf
@@ -191,7 +197,7 @@ check-proofs:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc -version'
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt     config -why3 $WHY3_CONF'
-  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler/examples/gimli/proofs'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler/examples/gimli/proofs CT_MODE=$CT_MODE'
 
 libjade-compile-to-asm:
   stage: test

compiler/examples/gimli/proofs/Makefile

@@ -1,26 +1,34 @@
-ECARGS ?=
+ECARGS ?= -I Jasmin:../../../../eclib
 
 JASMIN2EC := ../../../jasmin2ec
 
+CT_MODE ?= CT
+GIMLI_CT = gimli_$(shell echo $(CT_MODE) | tr A-Z a-z).ec
+
 .SUFFIXES: .jazz .ec
 
-all: gimli_arm.ec gimli_x86.ec gimli_x86_ct.ec gimli_arm_ct.ec gimli_avx.ec gimli_avx_ct.ec
+all: ct gimli_arm.ec gimli_x86.ec gimli_x86_ct.ec gimli_arm_ct.ec gimli_avx.ec gimli_avx_ct.ec
 	easycrypt runtest $(ECARGS) ec.config $@
 
+ct: $(GIMLI_CT) gimli_x86_ct.ec gimli_arm_ct.ec gimli_avx_ct.ec
+	easycrypt $(ECARGS) $<
+
 gimli_arm.ec: ../arm-m4/gimli.jazz
 	$(JASMIN2EC) --arch=arm-m4 -o $@ $^
 
 gimli_arm_ct.ec: ../arm-m4/gimli.jazz
-	$(JASMIN2EC) --arch=arm-m4 --model=CT -o $@ $^
+	$(JASMIN2EC) --arch=arm-m4 --model=$(CT_MODE) -o $@ $^
 
 gimli_x86.ec: ../x86-64/gimli.jazz
 	$(JASMIN2EC) --arch=x86-64 -o $@ $^
 
 gimli_x86_ct.ec: ../x86-64/gimli.jazz
-	$(JASMIN2EC) --arch=x86-64 --model=CT -o $@ $^
+	$(JASMIN2EC) --arch=x86-64 --model=$(CT_MODE) -o $@ $^
 
 gimli_avx.ec: ../x86-64/gimliv.jazz ../x86-64/gimliv.jinc
 	$(JASMIN2EC) --arch=x86-64 -o $@ $<
 
 gimli_avx_ct.ec: ../x86-64/gimliv.jazz ../x86-64/gimliv.jinc
-	$(JASMIN2EC) --arch=x86-64 --model=CT -o $@ $<
+	$(JASMIN2EC) --arch=x86-64 --model=$(CT_MODE) -o $@ $<
+
+.PHONY: all ct

compiler/examples/gimli/proofs/ec.config

@@ -4,3 +4,4 @@ args = -I Jasmin:../../../../eclib
 
 [test-all]
 okdirs = .
+file_exclude = ./gimli_ct.ec ./gimli_ctg.ec

compiler/examples/gimli/proofs/gimli_ct.ec

@@ -5,13 +5,13 @@ from Jasmin require import JLeakage.
   * Since it is an address, its value is leaked, and should be public. *)
 
 equiv gimli_x86_ct :
-  Gimli_x86_ct.M.gimli ~ Gimli_x86_ct.M.gimli : ={ Gimli_x86_ct.M.leakages } ==> ={ Gimli_x86_ct.M.leakages }.
-proof. proc; inline *; sim. qed.
+  Gimli_x86_ct.M.gimli ~ Gimli_x86_ct.M.gimli : true ==> res{1}.`1 = res{2}.`1.
+proof. proc; inline *; sim: (={leak}). qed.
 
 equiv gimli_arm_ct :
-  Gimli_arm_ct.M.gimli ~ Gimli_arm_ct.M.gimli : ={ Gimli_arm_ct.M.leakages } ==> ={ Gimli_arm_ct.M.leakages }.
-proof. proc; inline *; sim. qed.
+  Gimli_arm_ct.M.gimli ~ Gimli_arm_ct.M.gimli : true  ==> res{1}.`1 = res{2}.`1.
+proof. proc; inline *; sim: (={leak}). qed.
 
 equiv gimli_avx_ct :
-  Gimli_avx_ct.M.gimli ~ Gimli_avx_ct.M.gimli : ={ io, Gimli_avx_ct.M.leakages } ==> ={ Gimli_avx_ct.M.leakages }.
+  Gimli_avx_ct.M.gimli ~ Gimli_avx_ct.M.gimli : ={ io } ==> ={ res }.
 proof. proc; inline *; sim. qed.

compiler/examples/gimli/proofs/gimli_ctg.ec

@@ -0,0 +1,17 @@
+require Gimli_x86_ct Gimli_arm_ct Gimli_avx_ct.
+from Jasmin require import JLeakage.
+
+(** The [io] argument holds a pointer to the data that undergoes the permutation.
+  * Since it is an address, its value is leaked, and should be public. *)
+
+equiv gimli_x86_ct :
+  Gimli_x86_ct.M.gimli ~ Gimli_x86_ct.M.gimli : ={ Gimli_x86_ct.M.leakages } ==> ={ Gimli_x86_ct.M.leakages }.
+proof. proc; inline *; sim. qed.
+
+equiv gimli_arm_ct :
+  Gimli_arm_ct.M.gimli ~ Gimli_arm_ct.M.gimli : ={ Gimli_arm_ct.M.leakages } ==> ={ Gimli_arm_ct.M.leakages }.
+proof. proc; inline *; sim. qed.
+
+equiv gimli_avx_ct :
+  Gimli_avx_ct.M.gimli ~ Gimli_avx_ct.M.gimli : ={ io, Gimli_avx_ct.M.leakages } ==> ={ Gimli_avx_ct.M.leakages }.
+proof. proc; inline *; sim. qed.