Kyber768 Jasmin reference implementation of fqmul

examples/libjade/kyber768/fqmul/README.md

@@ -0,0 +1,66 @@
+This file describes the contents of this directory.
+
+We start with the following Jasmin program, defined in `fqmul.jazz`, that is used by Kyber768 reference implementation.
+```
+param int KYBER_Q = 3329;
+param int QINV    = 62209;     /* q^(-1) mod 2^16 */
+
+export fn fqmul(reg u16 a b) -> reg u16
+{
+  reg u32 ad bd c t u;
+  reg u16 r;
+
+  ad = (32s)a;
+  bd = (32s)b;
+
+  c = ad * bd;
+
+  u = c * QINV;
+
+  u <<= 16;
+  u >>s= 16;
+
+  t = u * KYBER_Q;
+  t = c - t;
+
+  t >>s= 16;
+  r = t;
+
+  return r;
+}
+```
+
+Intuitively, we want to prove that `r * 2^16` is equal to `a * b` mod `KYBER_Q`.
+
+To compile `fqmul.jazz` into an assembly file, the Jasmin compiler can be used: `jasminc fqmul.jazz -o fqmul.s`. For the pushed `fqmul.s`, Jasmin compiler `v2022.09.0` was used.
+
+The next step was to write a simple `main` function, using C, that includes a call to function `fqmul` and compile the corresponding binary: `gcc -o main main.c fqmul.s`.
+
+Next, we produced `fqmul.gas.0` with `../../../../scripts/itrace.py main fqmul fqmul.gas.0`. In `fqmul.gas` we defined the translation rules and copied the contents of `fqmul.gas.0`.
+
+From this file, we extracted the CryptoLine representation with `../../../../scripts/to_zdsl.py fqmul.gas > fqmul.cl.0`. We used `fqmul.cl.0` to define `fqmul.cl` which contains the pre and post-conditions.
+
+As a convention, we keep and push the auto-generated files without modifications (`*.0`), to check (with diff,for instance) that only what was supposed to change did change during the manual editing of the file.
+
+Running `cv -v fqmul.cl` should be OK:
+
+```
+$ cv -v -isafety fqmul.cl
+Parsing CryptoLine file:        [OK]        0.000265 seconds
+Checking well-formedness:       [OK]        0.000052 seconds
+Transforming to SSA form:       [OK]        0.000022 seconds
+Normalizing specification:      [OK]        0.000031 seconds
+Rewriting assignments:          [OK]        0.000015 seconds
+Verifying program safety:
+     Cut 0
+         Round 1 (1 safety conditions, timeout = 300 seconds)
+         Safety condition #0    [OK]
+     Overall                    [OK]        0.027311 seconds
+Verifying range specification:        [OK]        18.345685 seconds
+Rewriting value-preserved casting:    [OK]        0.000026 seconds
+Verifying algebraic specification:    [OK]        0.001105 seconds
+Verification result:                  [OK]        18.374723 seconds
+```
+
+In addition to the `fqmul.cl`, we also include `fqmul.annotated.cl` which contains the original Jasmin code in comments and some intermediate assertions.
+

examples/libjade/kyber768/fqmul/fqmul.annotated.cl

@@ -0,0 +1,57 @@
+proc main (sint16 di, sint16 si) =
+{
+  true
+  &&
+  and [
+    0@16 <=s si,
+    si <=s 3328@16
+  ]
+}
+
+(* movswl %di,%eax // ad = (32s)a; *)
+cast eax@sint32 di;
+
+(* movswl %si,%ecx // bd = (32s)b; *)
+cast ecx@sint32 si;
+
+(* imul %ecx,%eax // c (eax) = ad (eax) * bd (ecx); *)
+mull dontcare eax ecx eax;
+
+(* imul $0xf301,%eax,%ecx // u (ecx) = c (eax) * QINV (62209); *)
+cast eax@sint32 eax;
+mull dontcare ecx 0xf301@sint32 eax;
+
+assert true && eqsmod (eax * 62209@32) ecx (65536@32);
+
+(* shl    $0x10,%ecx // u <<= 16; *)
+split dontcare ecx ecx 16;                         
+shl ecx ecx 16;
+
+(* sar    $0x10,%ecx // u >>s= 16; *)
+cast ecx@sint32 ecx;
+ssplit ecx dontcare ecx 16;
+
+assert true && and [ 
+                     eqsmod (eax * 62209@32) ecx (65536@32),
+                     (-32768)@32 <=s ecx,
+                     ecx <s 32768@32 ];
+
+(* imul   $0xd01,%ecx,%ecx // t (ecx) = u (ecx) * KYBER_Q; *)
+cast ecx@sint32 ecx;
+mull dontcare ecx 3329@sint32 ecx;
+
+(* sub    %ecx,%eax // t (eax) = c - t; *)
+cast eax@uint32 eax;
+subb carry eax eax ecx;
+
+(* sar    $0x10,%eax // t >>s= 16; *)
+cast eax@sint32 eax;
+ssplit eax dontcare eax 16;
+
+{
+  true
+  &&
+  and [ eqsmod ( eax * 65536@32 ) ((sext di 16) * (sext si 16)) (3329@32),
+        (-3328)@32 <=s eax,
+        eax <=s 3328@32 ]
+}

examples/libjade/kyber768/fqmul/fqmul.cl

@@ -0,0 +1,68 @@
+(*
+$ cv -v -isafety fqmul.cl
+Parsing CryptoLine file:		[OK]		0.000265 seconds
+Checking well-formedness:		[OK]		0.000052 seconds
+Transforming to SSA form:		[OK]		0.000022 seconds
+Normalizing specification:		[OK]		0.000031 seconds
+Rewriting assignments:			[OK]		0.000015 seconds
+Verifying program safety:
+	 Cut 0
+	     Round 1 (1 safety conditions, timeout = 300 seconds)
+		 Safety condition #0	[OK]
+	 Overall			[OK]		0.027311 seconds
+Verifying range specification:		[OK]		18.345685 seconds
+Rewriting value-preserved casting:	[OK]		0.000026 seconds
+Verifying algebraic specification:	[OK]		0.001105 seconds
+Verification result:			[OK]		18.374723 seconds
+*)
+
+proc main (sint16 di, sint16 si) =
+{
+  true
+  &&
+  and [
+    0@16 <=s si,
+    si <=s 3328@16
+  ]
+}
+
+(* fqmul: *)
+#fqmul:;
+(* #! -> SP = 0x7fffffffd9a8 *)
+#! 0x7fffffffd9a8 = 0x7fffffffd9a8;
+(* movswl %di,%eax                                 #! PC = 0x555555555240 *)
+cast eax@sint32 di;
+(* movswl %si,%ecx                                 #! PC = 0x555555555243 *)
+cast ecx@sint32 si;
+(* imul   %ecx,%eax                                #! PC = 0x555555555246 *)
+mull dontcare eax ecx eax;
+(* imul   $0xf301,%eax,%ecx                        #! PC = 0x555555555249 *)
+cast eax@sint32 eax;
+mull dontcare ecx 0xf301@sint32 eax;
+(* shl    $0x10,%ecx                               #! PC = 0x55555555524f *)
+split dontcare ecx ecx 16;
+shl ecx ecx 16;
+(* sar    $0x10,%ecx                               #! PC = 0x555555555252 *)
+cast ecx@sint32 ecx;
+ssplit ecx dontcare ecx 16;
+(* imul   $0xd01,%ecx,%ecx                         #! PC = 0x555555555255 *)
+cast ecx@sint32 ecx;
+mull dontcare ecx 0xd01@sint32 ecx;
+(* sub    %ecx,%eax                                #! PC = 0x55555555525b *)
+cast eax@uint32 eax;
+subb carry eax eax ecx;
+(* sar    $0x10,%eax                               #! PC = 0x55555555525d *)
+cast eax@sint32 eax;
+ssplit eax dontcare eax 16;
+(* #! <- SP = 0x7fffffffd9a8 *)
+#! 0x7fffffffd9a8 = 0x7fffffffd9a8;
+(* #retq                                           #! PC = 0x555555555260 *)
+#retq
+{
+  true
+  &&
+  and [ eqsmod ( eax * 65536@32 ) ((sext di 16) * (sext si 16)) (3329@32),
+        (-3328)@32 <=s eax,
+        eax <=s 3328@32 ]
+}
+

examples/libjade/kyber768/fqmul/fqmul.cl.0

@@ -0,0 +1,46 @@
+proc main (di, si) =
+{
+  true
+  &&
+  true
+}
+
+(* fqmul: *)
+fqmul:;
+(* #! -> SP = 0x7fffffffd9a8 *)
+#! 0x7fffffffd9a8 = 0x7fffffffd9a8;
+(* movswl %di,%eax                                 #! PC = 0x555555555240 *)
+cast eax@sint32 di;
+(* movswl %si,%ecx                                 #! PC = 0x555555555243 *)
+cast ecx@sint32 si;
+(* imul   %ecx,%eax                                #! PC = 0x555555555246 *)
+mull dontcare eax ecx eax;
+(* imul   $0xf301,%eax,%ecx                        #! PC = 0x555555555249 *)
+cast eax@sint32 eax;
+mull dontcare ecx 0xf301@sint32 eax;
+(* shl    $0x10,%ecx                               #! PC = 0x55555555524f *)
+split dontcare ecx ecx 16;
+shl ecx ecx 16;
+(* sar    $0x10,%ecx                               #! PC = 0x555555555252 *)
+cast ecx@sint32 ecx;
+ssplit ecx dontcare ecx 16;
+(* imul   $0xd01,%ecx,%ecx                         #! PC = 0x555555555255 *)
+cast ecx@sint32 ecx;
+mull dontcare ecx 0xd01@sint32 ecx;
+(* sub    %ecx,%eax                                #! PC = 0x55555555525b *)
+cast eax@uint32 eax;
+subb carry eax eax ecx;
+(* sar    $0x10,%eax                               #! PC = 0x55555555525d *)
+cast eax@sint32 eax;
+ssplit eax dontcare eax 16;
+(* #! <- SP = 0x7fffffffd9a8 *)
+#! 0x7fffffffd9a8 = 0x7fffffffd9a8;
+(* #retq                                           #! PC = 0x555555555260 *)
+#retq                                           #! 0x555555555260 = 0x555555555260;
+
+{
+  true
+  &&
+  true
+}
+

examples/libjade/kyber768/fqmul/fqmul.gas

@@ -0,0 +1,31 @@
+#! %di = %%di
+#! %si = %%si
+#! %eax = %%eax
+#! %ecx = %%ecx
+
+#! movswl $1v, $2v -> cast $2v@sint32 $1v
+#! imul $1v, $2v -> mull dontcare $2v $1v $2v
+#! imul \$$1c, $2v, $3v -> cast $2v@sint32 $2v;\nmull dontcare $3v $1c@sint32 $2v
+#! shl \$0x10, $1v -> split dontcare $1v $1v 16;\nshl $1v $1v 16
+#! sar \$0x10, $1v -> cast $1v@sint32 $1v;\nssplit $1v dontcare $1v 16
+#! sub $1v, $2v -> cast $2v@uint32 $2v;\nsubb carry $2v $2v $1v
+
+fqmul:
+# %rdi = 0xffff8000
+# %rsi = 0x0
+# %rdx = 0x0
+# %rcx = 0x555555555270
+# %r8  = 0x0
+# %r9  = 0x7ffff7fe0d50
+	#! -> SP = 0x7fffffffd9a8
+	movswl %di,%eax                                 #! PC = 0x555555555240
+	movswl %si,%ecx                                 #! PC = 0x555555555243
+	imul   %ecx,%eax                                #! PC = 0x555555555246
+	imul   $0xf301,%eax,%ecx                        #! PC = 0x555555555249
+	shl    $0x10,%ecx                               #! PC = 0x55555555524f
+	sar    $0x10,%ecx                               #! PC = 0x555555555252
+	imul   $0xd01,%ecx,%ecx                         #! PC = 0x555555555255
+	sub    %ecx,%eax                                #! PC = 0x55555555525b
+	sar    $0x10,%eax                               #! PC = 0x55555555525d
+	#! <- SP = 0x7fffffffd9a8
+	#retq                                           #! PC = 0x555555555260

examples/libjade/kyber768/fqmul/fqmul.gas.0

@@ -0,0 +1,19 @@
+fqmul:
+# %rdi = 0xffff8000
+# %rsi = 0x0
+# %rdx = 0x0
+# %rcx = 0x555555555270
+# %r8  = 0x0
+# %r9  = 0x7ffff7fe0d50
+	#! -> SP = 0x7fffffffd9a8
+	movswl %di,%eax                                 #! PC = 0x555555555240
+	movswl %si,%ecx                                 #! PC = 0x555555555243
+	imul   %ecx,%eax                                #! PC = 0x555555555246
+	imul   $0xf301,%eax,%ecx                        #! PC = 0x555555555249
+	shl    $0x10,%ecx                               #! PC = 0x55555555524f
+	sar    $0x10,%ecx                               #! PC = 0x555555555252
+	imul   $0xd01,%ecx,%ecx                         #! PC = 0x555555555255
+	sub    %ecx,%eax                                #! PC = 0x55555555525b
+	sar    $0x10,%eax                               #! PC = 0x55555555525d
+	#! <- SP = 0x7fffffffd9a8
+	#retq                                           #! PC = 0x555555555260

examples/libjade/kyber768/fqmul/fqmul.jazz

@@ -0,0 +1,27 @@
+param int KYBER_Q = 3329;
+param int QINV    = 62209;     /* q^(-1) mod 2^16 */
+
+export fn fqmul(reg u16 a b) -> reg u16
+{
+  reg u32 ad bd c t u;
+  reg u16 r;
+
+  ad = (32s)a;
+  bd = (32s)b;
+
+  c = ad * bd;
+
+  u = c * QINV;
+
+  u <<= 16;
+  u >>s= 16; 
+
+  t = u * KYBER_Q;
+  t = c - t;
+
+  t >>s= 16;
+  r = t;
+
+  return r;
+}
+

examples/libjade/kyber768/fqmul/fqmul.s

@@ -0,0 +1,17 @@
+	.att_syntax
+	.text
+	.p2align	5
+	.globl	_fqmul
+	.globl	fqmul
+_fqmul:
+fqmul:
+	movswl	%di, %eax
+	movswl	%si, %ecx
+	imull	%ecx, %eax
+	imull	$62209, %eax, %ecx
+	shll	$16, %ecx
+	sarl	$16, %ecx
+	imull	$3329, %ecx, %ecx
+	subl	%ecx, %eax
+	sarl	$16, %eax
+	ret 

examples/libjade/kyber768/fqmul/main.c

@@ -0,0 +1,29 @@
+#include <stdint.h>
+#include <assert.h>
+
+extern int16_t fqmul(int16_t, int16_t);
+
+int32_t m(int32_t a, int32_t b)
+{
+    int32_t r = a % b;
+    if( r < 0 ){ r += b; }
+    return r;
+}
+
+int main(void)
+{
+  int16_t r, a, b;
+  int32_t t1, t2;
+
+  for (a = INT16_MIN; a < INT16_MAX; a++)
+  { for (b = 0; b < 3329; b++)
+    { r = fqmul(a, b);
+
+      t1 = m( ((int32_t)r) * 65536, 3329 );
+      t2 = m( (((int32_t)a) * ((int32_t)b)), 3329 );
+
+      assert( t1 == t2 );
+    }
+  }
+  return 0;
+}