correctness claim for stack variant

formosa-crypto · Dec 6, 2024 · 715d3b4 · 715d3b4
1 parent e56e947
commit 715d3b4
Show file tree

Hide file tree

Showing 7 changed files with 1,214 additions and 49 deletions.
diff --git a/code/jasmin/mlkem_avx2_stack/extraction/Array148.ec b/code/jasmin/mlkem_avx2_stack/extraction/Array148.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JArray.
+
+clone export PolyArray as Array148  with op size <- 148.
diff --git a/code/jasmin/mlkem_avx2_stack/extraction/Array33.ec b/code/jasmin/mlkem_avx2_stack/extraction/Array33.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JArray.
+
+clone export PolyArray as Array33  with op size <- 33.
diff --git a/code/jasmin/mlkem_avx2_stack/extraction/Makefile b/code/jasmin/mlkem_avx2_stack/extraction/Makefile
@@ -10,9 +10,9 @@
 all: ec
 
 ec:
-	$(JASMINC) ../jkem.jazz -oec jkem_avx2.ec \
-	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_keypair \
-	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_enc \
+	$(JASMINC) ../jkem.jazz -oec jkem_avx2_stack.ec \
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand \
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand \
 	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_dec
 
 clean:

diff --git a/code/jasmin/mlkem_avx2_stack/extraction/WArray33.ec b/code/jasmin/mlkem_avx2_stack/extraction/WArray33.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray33  with op size <- 33.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		from Jasmin require import JArray.

		clone export PolyArray as Array148 with op size <- 148.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		from Jasmin require import JArray.

		clone export PolyArray as Array33 with op size <- 33.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		from Jasmin require import JWord_array.

		clone export WArray as WArray33 with op size <- 33.