avx2 stack extraction

code/jasmin/mlkem_avx2_stack/extraction/Array1.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array1024.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array1088.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array1120.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array1152.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array1184.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array128.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array136.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array144.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array16.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array2.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array2048.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array2144.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array2304.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array24.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array2400.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array25.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array256.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array300.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array32.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array384.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array4.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array400.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array5.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array536.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array6.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array64.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array7.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array768.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array8.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Array960.ec

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

code/jasmin/mlkem_avx2_stack/extraction/Makefile

@@ -0,0 +1,19 @@
+# -*- Makefile -*-
+
+# --------------------------------------------------------------------
+-include ../../../Makefile.conf
+
+# --------------------------------------------------------------------
+.PHONY: all ec clean
+
+# --------------------------------------------------------------------
+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 \
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_dec
+
+clean:
+	rm -f *.ec

code/jasmin/mlkem_avx2_stack/extraction/WArray1.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1  with op size <- 1.

code/jasmin/mlkem_avx2_stack/extraction/WArray1088.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1088  with op size <- 1088.

code/jasmin/mlkem_avx2_stack/extraction/WArray1120.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1120  with op size <- 1120.

code/jasmin/mlkem_avx2_stack/extraction/WArray1152.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1152  with op size <- 1152.

code/jasmin/mlkem_avx2_stack/extraction/WArray1184.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1184  with op size <- 1184.

code/jasmin/mlkem_avx2_stack/extraction/WArray128.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray128  with op size <- 128.

code/jasmin/mlkem_avx2_stack/extraction/WArray1536.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray1536  with op size <- 1536.

code/jasmin/mlkem_avx2_stack/extraction/WArray16.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray16  with op size <- 16.

code/jasmin/mlkem_avx2_stack/extraction/WArray160.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray160  with op size <- 160.

code/jasmin/mlkem_avx2_stack/extraction/WArray192.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray192  with op size <- 192.

code/jasmin/mlkem_avx2_stack/extraction/WArray2.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2  with op size <- 2.

code/jasmin/mlkem_avx2_stack/extraction/WArray200.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray200  with op size <- 200.

code/jasmin/mlkem_avx2_stack/extraction/WArray2048.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2048  with op size <- 2048.

code/jasmin/mlkem_avx2_stack/extraction/WArray2144.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2144  with op size <- 2144.

code/jasmin/mlkem_avx2_stack/extraction/WArray224.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray224  with op size <- 224.

code/jasmin/mlkem_avx2_stack/extraction/WArray2400.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2400  with op size <- 2400.

code/jasmin/mlkem_avx2_stack/extraction/WArray256.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray256  with op size <- 256.

code/jasmin/mlkem_avx2_stack/extraction/WArray32.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray32  with op size <- 32.

code/jasmin/mlkem_avx2_stack/extraction/WArray384.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray384  with op size <- 384.

code/jasmin/mlkem_avx2_stack/extraction/WArray4.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray4  with op size <- 4.

code/jasmin/mlkem_avx2_stack/extraction/WArray4608.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray4608  with op size <- 4608.

code/jasmin/mlkem_avx2_stack/extraction/WArray512.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray512  with op size <- 512.

code/jasmin/mlkem_avx2_stack/extraction/WArray536.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray536  with op size <- 536.

code/jasmin/mlkem_avx2_stack/extraction/WArray64.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray64  with op size <- 64.

code/jasmin/mlkem_avx2_stack/extraction/WArray8.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray8  with op size <- 8.

code/jasmin/mlkem_avx2_stack/extraction/WArray800.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray800  with op size <- 800.

code/jasmin/mlkem_avx2_stack/extraction/WArray960.ec

@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray960  with op size <- 960.