ToEC: deprecate mode CTG

.gitlab-ci.yml

@@ -178,12 +178,8 @@ check-proofs:
   stage: test
   parallel:
     matrix:
-      # 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
@@ -197,7 +193,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 CT_MODE=$CT_MODE'
+  - 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/extraction-unit-tests'
 
 libjade-compile-to-asm:

CHANGELOG.md

@@ -90,7 +90,8 @@
   ([PR #914](https://github.com/jasmin-lang/jasmin/pull/914),
   [PR #952](https://github.com/jasmin-lang/jasmin/pull/952),
   [PR #967](https://github.com/jasmin-lang/jasmin/pull/967)),
-  [PR #995](https://github.com/jasmin-lang/jasmin/pull/995)).
+  [PR #995](https://github.com/jasmin-lang/jasmin/pull/995)),
+  [PR #1047](https://github.com/jasmin-lang/jasmin/pull/1047)).
 
 - The “allocation” pass now uses the liveness information to reduce the sizes
   of the tables it uses internally; it should be faster on large functions

compiler/entry/jasmin2ec.ml

@@ -59,7 +59,7 @@ let model =
     $(b,CT): Functions additionally return timing-observable leakage for
     'cryptographic constant time' (if/while conditions, memory access
     addresses, array indices, for loop bounds).
-    $(b,CTG): Cryptographic constant time leakage is added to a
+    (Deprecated) $(b,CTG): Cryptographic constant time leakage is added to a
     global variable."
   in
   Arg.(value & opt (Arg.enum alts) Normal & info [ "m"; "model" ] ~doc)

compiler/examples/gimli/proofs/.gitignore

@@ -1,4 +1,5 @@
 Array12.ec
+BArray48.ec
 WArray48.ec
 gimli_arm.ec
 gimli_avx.ec

compiler/examples/gimli/proofs/Makefile

@@ -2,33 +2,27 @@ 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: ct gimli_arm.ec gimli_x86.ec gimli_x86_ct.ec gimli_arm_ct.ec gimli_avx.ec gimli_avx_ct.ec
+all: gimli_arm.ec gimli_arm_ct.ec gimli_x86.ec gimli_x86_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_MODE) -o $@ $^
+	$(JASMIN2EC) --arch=arm-m4 --model=CT -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_MODE) -o $@ $^
+	$(JASMIN2EC) --arch=x86-64 --model=CT -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_MODE) -o $@ $<
+	$(JASMIN2EC) --arch=x86-64 --model=CT -o $@ $<
 
-.PHONY: all ct
+.PHONY: all

compiler/examples/gimli/proofs/ec.config

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

compiler/src/toEC.ml

@@ -2073,7 +2073,10 @@ let extract ((globs,funcs):('info, 'asm) prog) arch pd asmOp (model: model) amod
   let module EL: EcLeakage = (val match model with
     | Normal -> (module EcLeakNormal(EE): EcLeakage)
     | ConstantTime -> (module EcLeakConstantTime(EE): EcLeakage)
-    | ConstantTimeGlobal -> (module EcLeakConstantTimeGlobal(EE): EcLeakage)
+    | ConstantTimeGlobal ->
+        warning Deprecated Location.i_dummy
+          "EasyCrypt extraction for constant-time in CTG mode is deprecated. Use the CT mode instead.";
+        (module EcLeakConstantTimeGlobal(EE): EcLeakage)
   ) in
   let module E = Extraction(EA)(EL) in
   let prog = E.pp_prog env asmOp fmt globs funcs in