Use latest Jasmin release (2023.06.3)

formosa-crypto · Apr 19, 2024 · 1cc454f · 1cc454f
1 parent 7222f3f
commit 1cc454f
Show file tree

Hide file tree

Showing 7 changed files with 15 additions and 13 deletions.
diff --git a/code/Makefile.conf b/code/Makefile.conf
@@ -5,3 +5,4 @@ current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 # --------------------------------------------------------------------
 JASMINC ?=  $(current_dir)/../jasmin/compiler/jasminc
+JAZZCT ?=  $(current_dir)/../jasmin/compiler/jazzct
diff --git a/code/jasmin/mlkem_avx2/Makefile b/code/jasmin/mlkem_avx2/Makefile
@@ -97,7 +97,7 @@ test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(SOURCES) $(INCS) jpolyve
 .PHONY: ct clean
 
 ct:
-	$(JASMINC) -checkCT -infer jkem.jazz
+	$(JAZZCT) --infer jkem.jazz
 
 clean:
 	-rm -f *.o

diff --git a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
@@ -100,7 +100,7 @@ abbrev pc_mask_s = W16.of_int 15.
 abbrev pc_shift1_s = W16.of_int 512.
 
 
-abbrev KeccakF1600RoundConstants = Array24.of_list witness [W256.of_int 6277101735386680764176071790128604879584176795969512275969;
+abbrev keccakF1600RoundConstants = Array24.of_list witness [W256.of_int 6277101735386680764176071790128604879584176795969512275969;
 W256.of_int 206504092890751023779864409751650843328560248233805014854828162;
 W256.of_int (-57896044618657891154337237002533387566728630465883811983015055433200855646070);
 W256.of_int (-57896044605177918687001956587831074660851270707671256656745893357814858874880);
@@ -137,7 +137,7 @@ W64.of_int (-9223372036854775808); W64.of_int (-9223372036854775808);
 W64.of_int (-9223372036854775808)].
 
 
-abbrev KECCAK1600_RC = Array24.of_list witness [W64.of_int 1;
+abbrev kECCAK1600_RC = Array24.of_list witness [W64.of_int 1;
 W64.of_int 32898; W64.of_int (-9223372036854742902);
 W64.of_int (-9223372034707259392); W64.of_int 32907; W64.of_int 2147483649;
 W64.of_int (-9223372034707259263); W64.of_int (-9223372036854743031);
@@ -925,7 +925,7 @@ module M(SC:Syscall_t) = {
     rC <- witness;
     e <- witness;
     s_e <- witness;
-    rC <- KECCAK1600_RC;
+    rC <- kECCAK1600_RC;
     e <- s_e;
     c <- (W64.of_int 0);
 
@@ -1390,7 +1390,7 @@ module M(SC:Syscall_t) = {
     bbi <@ __rol_4u64 (t256, 43);
     t256 <- VPANDN_256 bbe bbi;
     t256 <- (t256 `^` bba);
-    t256 <- (t256 `^` KeccakF1600RoundConstants.[index]);
+    t256 <- (t256 `^` keccakF1600RoundConstants.[index]);
     e_4x.[0] <- t256;
     ca <- t256;
     t256 <- a_4x.[18];
@@ -1671,7 +1671,7 @@ module M(SC:Syscall_t) = {
     bbi <@ __rol_4u64 (t256, 43);
     t256 <- VPANDN_256 bbe bbi;
     t256 <- (t256 `^` bba);
-    t256 <- (t256 `^` KeccakF1600RoundConstants.[index]);
+    t256 <- (t256 `^` keccakF1600RoundConstants.[index]);
     e_4x.[0] <- t256;
     ca <- t256;
     t256 <- a_4x.[18];
@@ -1963,7 +1963,7 @@ module M(SC:Syscall_t) = {
     bbi <@ __rol_4u64 (t256, 43);
     t256 <- VPANDN_256 bbe bbi;
     t256 <- (t256 `^` bba);
-    t256 <- (t256 `^` KeccakF1600RoundConstants.[index]);
+    t256 <- (t256 `^` keccakF1600RoundConstants.[index]);
     e_4x.[0] <- t256;
     t256 <- a_4x.[18];
     t256 <- (t256 `^` do_0);

diff --git a/code/jasmin/mlkem_ref/Makefile b/code/jasmin/mlkem_ref/Makefile
@@ -84,7 +84,7 @@ test/test_polyvec_%: test/test_polyvec_%.c $(HEADERS) $(SOURCES) jpolyvec.s
 .PHONY: ct clean
 
 ct:
-	$(JASMINC) -checkCT -infer jkem.jazz
+	$(JAZZCT) --infer jkem.jazz
 
 clean:
 	-rm -f *.s

diff --git a/code/jasmin/mlkem_ref/extraction/jkem.ec b/code/jasmin/mlkem_ref/extraction/jkem.ec
@@ -79,7 +79,7 @@ W16.of_int 996; W16.of_int 991; W16.of_int 958; W16.of_int 1869;
 W16.of_int 1522; W16.of_int 1628].
 
 
-abbrev KECCAK1600_RC = Array24.of_list witness [W64.of_int 1;
+abbrev kECCAK1600_RC = Array24.of_list witness [W64.of_int 1;
 W64.of_int 32898; W64.of_int (-9223372036854742902);
 W64.of_int (-9223372034707259392); W64.of_int 32907; W64.of_int 2147483649;
 W64.of_int (-9223372034707259263); W64.of_int (-9223372036854743031);
@@ -338,7 +338,7 @@ module M(SC:Syscall_t) = {
     rC <- witness;
     e <- witness;
     s_e <- witness;
-    rC <- KECCAK1600_RC;
+    rC <- kECCAK1600_RC;
     e <- s_e;
     c <- (W64.of_int 0);
 

diff --git a/jasmin b/jasmin
diff --git a/shell.nix b/shell.nix
@@ -1,7 +1,7 @@
 { pkgs ?
     import (fetchTarball {
-      url = https://github.com/NixOS/nixpkgs/archive/51063ed4f2343a59fdeebb279bb81d87d453942b.tar.gz;
-      sha256 = "sha256:0my8bdc7js7gdcl8z8ik49sl9gccqz39xg8q335sharf5qxq13ww";
+      url = "https://github.com/NixOS/nixpkgs/archive/e402c3eb6d88384ca6c52ef1c53e61bdc9b84ddd.tar.gz";
+      sha256 = "sha256:0yz78sahc3mzv38bah8chl2y9cmwsmp9r2p7xv4ny6rcvl1f94cf";
     }) {}
 , full ? true
 }:
@@ -35,6 +35,7 @@ in
 
 mkShell ({
   JASMINC = "${jasmin-compiler.bin}/bin/jasminc";
+  JAZZCT = "${jasmin-compiler.bin}/bin/jazzct";
 } // lib.optionalAttrs full {
   packages = [
     ec
Original file line number	Diff line number	Diff line change
Expand Up		@@ -5,3 +5,4 @@ current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))

		# --------------------------------------------------------------------
		JASMINC ?= $(current_dir)/../jasmin/compiler/jasminc
		JAZZCT ?= $(current_dir)/../jasmin/compiler/jazzct