Missing files

formosa-crypto · Aug 27, 2024 · 9809171 · 9809171
1 parent 1474c8e
commit 9809171
Show file tree

Hide file tree

Showing 7 changed files with 21 additions and 0 deletions.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray160.ec b/code/jasmin/mlkem_avx2/extraction/WArray160.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray160  with op size <- 160.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray2048.ec b/code/jasmin/mlkem_avx2/extraction/WArray2048.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2048  with op size <- 2048.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray2176.ec b/code/jasmin/mlkem_avx2/extraction/WArray2176.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray2176  with op size <- 2176.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray224.ec b/code/jasmin/mlkem_avx2/extraction/WArray224.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray224  with op size <- 224.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray288.ec b/code/jasmin/mlkem_avx2/extraction/WArray288.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray288  with op size <- 288.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray544.ec b/code/jasmin/mlkem_avx2/extraction/WArray544.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray544  with op size <- 544.
diff --git a/code/jasmin/mlkem_avx2/extraction/WArray8.ec b/code/jasmin/mlkem_avx2/extraction/WArray8.ec
@@ -0,0 +1,3 @@
+from Jasmin require import JWord_array.
+
+clone export WArray as WArray8  with op size <- 8.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		from Jasmin require import JWord_array.

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

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

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

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

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

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

		clone export WArray as WArray8 with op size <- 8.