From 23c41e31942201b81ef5f9f04676f32f8de64904 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Wed, 12 Oct 2022 15:48:16 +0100 Subject: [PATCH 1/5] wip for fqmul --- examples/libjade/kyber/fqmul/fqmul.hw.cl | 53 ++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 examples/libjade/kyber/fqmul/fqmul.hw.cl diff --git a/examples/libjade/kyber/fqmul/fqmul.hw.cl b/examples/libjade/kyber/fqmul/fqmul.hw.cl new file mode 100644 index 00000000..0ba3be32 --- /dev/null +++ b/examples/libjade/kyber/fqmul/fqmul.hw.cl @@ -0,0 +1,53 @@ +proc main (sint16 di, sint16 si) = +{ + true + && + and [ + (-3329)@16 <=s di, di SP = 0x7fffffffd968 *) +#! 0x7fffffffd968 = 0x7fffffffd968; + +(* movswl %di,%eax #! PC = 0x555555555160 *) +cast eax@sint32 di; + +(* movswl %si,%ecx #! PC = 0x555555555163 *) +cast ecx@sint32 si; + +(* imul %ecx,%eax #! PC = 0x555555555166 *) +mul eax ecx eax; + +(* imul $0xf301,%eax,%ecx #! PC = 0x555555555169 *) +smull dontcare ecx 0xf301@sint32 eax; + +(* shl $0x10,%ecx #! PC = 0x55555555516f *) +split dontcare ecx ecx 16; +shl ecx ecx 16; + +(* sar $0x10,%ecx #! PC = 0x555555555172 *) +(*split ecx dontcare ecx 16;*) + +(*wip*) + +(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 *) +(*smull dontcare ecx 0xd01@sint32 ecx;*) + +(* sub %ecx,%eax #! PC = 0x55555555517b *) +(*subb carry eax eax ecx;*) + +(* sar $0x10,%eax #! PC = 0x55555555517d *) +(*sar eax eax 0x10;*) + +(* #! <- SP = 0x7fffffffd968 *) +#! 0x7fffffffd968 = 0x7fffffffd968; +(* #retq #! PC = 0x555555555180 *) +#retq #! 0x555555555180 = 0x555555555180; +{ + true + && + true +} + From 6c604f18086fc6bf718a5b218d3a8b4264523a01 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Wed, 12 Oct 2022 15:51:31 +0100 Subject: [PATCH 2/5] fqmul.jazz --- examples/libjade/kyber/fqmul/fqmul.jazz | 34 +++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 examples/libjade/kyber/fqmul/fqmul.jazz diff --git a/examples/libjade/kyber/fqmul/fqmul.jazz b/examples/libjade/kyber/fqmul/fqmul.jazz new file mode 100644 index 00000000..97cdb7fc --- /dev/null +++ b/examples/libjade/kyber/fqmul/fqmul.jazz @@ -0,0 +1,34 @@ +param int KYBER_Q = 3329; +param int QINV = 62209; /* q^(-1) mod 2^16 */ +param int MONT = 2285; /* 2^16 % Q */ +param int BARR = 20159; /* (1U << 26)/KYBER_Q + 1 */ + +export fn fqmul(reg u16 a, reg u16 b) -> reg u16 +{ + reg u32 ad; + reg u32 bd; + reg u32 c; + reg u32 t; + reg u16 r; + reg u32 u; + + ad = (32s)a; + bd = (32s)b; + + c = ad * bd; + + u = c * QINV; + + u <<= 16; + u >>s= 16; + + t = u * KYBER_Q; + t = c - t; + // assert firsts 16 bits as zero + + t >>s= 16; + r = t; + + return r; +} + From 7e5af51c9045931360dd297e9ee002a088d2ed3c Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Fri, 14 Oct 2022 14:44:47 +0100 Subject: [PATCH 3/5] libjade kyber768 fqmul example working + some doc. --- examples/libjade/kyber/fqmul/README.md | 62 +++++++++++++++++++ .../libjade/kyber/fqmul/fqmul.annotated.cl | 57 +++++++++++++++++ examples/libjade/kyber/fqmul/fqmul.cl | 51 +++++++++++++++ .../kyber/fqmul/{fqmul.hw.cl => fqmul.cl.0} | 47 ++++++-------- examples/libjade/kyber/fqmul/fqmul.gas | 31 ++++++++++ examples/libjade/kyber/fqmul/fqmul.gas.0 | 19 ++++++ examples/libjade/kyber/fqmul/fqmul.jazz | 11 +--- examples/libjade/kyber/fqmul/fqmul.s | 17 +++++ examples/libjade/kyber/fqmul/main.c | 10 +++ 9 files changed, 269 insertions(+), 36 deletions(-) create mode 100644 examples/libjade/kyber/fqmul/README.md create mode 100644 examples/libjade/kyber/fqmul/fqmul.annotated.cl create mode 100644 examples/libjade/kyber/fqmul/fqmul.cl rename examples/libjade/kyber/fqmul/{fqmul.hw.cl => fqmul.cl.0} (67%) create mode 100644 examples/libjade/kyber/fqmul/fqmul.gas create mode 100644 examples/libjade/kyber/fqmul/fqmul.gas.0 create mode 100644 examples/libjade/kyber/fqmul/fqmul.s create mode 100644 examples/libjade/kyber/fqmul/main.c diff --git a/examples/libjade/kyber/fqmul/README.md b/examples/libjade/kyber/fqmul/README.md new file mode 100644 index 00000000..70e6251d --- /dev/null +++ b/examples/libjade/kyber/fqmul/README.md @@ -0,0 +1,62 @@ +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 fqmul.cl +Parsing CryptoLine file: [OK] 0.000343 seconds +Checking well-formedness: [OK] 0.000064 seconds +Transforming to SSA form: [OK] 0.000020 seconds +Normalizing specification: [OK] 0.000024 seconds +Rewriting assignments: [OK] 0.000009 seconds +Verifying program safety: [OK] 0.030387 seconds +Verifying range specification: [OK] 20.948068 seconds +Rewriting value-preserved casting: [OK] 0.000011 seconds +Verifying algebraic specification: [OK] 0.001294 seconds +Verification result: [OK] 20.980513 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. + diff --git a/examples/libjade/kyber/fqmul/fqmul.annotated.cl b/examples/libjade/kyber/fqmul/fqmul.annotated.cl new file mode 100644 index 00000000..a93baec7 --- /dev/null +++ b/examples/libjade/kyber/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= 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 ] +} diff --git a/examples/libjade/kyber/fqmul/fqmul.cl b/examples/libjade/kyber/fqmul/fqmul.cl new file mode 100644 index 00000000..5ea5dc7f --- /dev/null +++ b/examples/libjade/kyber/fqmul/fqmul.cl @@ -0,0 +1,51 @@ +proc main (sint16 di, sint16 si) = +{ + true + && + and [ + 0@16 <=s si, + si <=s 3328@16 + ] +} + +(* fqmul: *) +#fqmul:; +(* #! -> SP = 0x7fffffffd9b8 *) +#! 0x7fffffffd9b8 = 0x7fffffffd9b8; +(* movswl %di,%eax #! PC = 0x555555555160 *) +cast eax@sint32 di; +(* movswl %si,%ecx #! PC = 0x555555555163 *) +cast ecx@sint32 si; +(* imul %ecx,%eax #! PC = 0x555555555166 *) +mull dontcare eax ecx eax; +(* imul $0xf301,%eax,%ecx #! PC = 0x555555555169 *) +cast eax@sint32 eax; +mull dontcare ecx 0xf301@sint32 eax; +(* shl $0x10,%ecx #! PC = 0x55555555516f *) +split dontcare ecx ecx 16; +shl ecx ecx 16; +(* sar $0x10,%ecx #! PC = 0x555555555172 *) +cast ecx@sint32 ecx; +ssplit ecx dontcare ecx 16; +(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 *) +cast ecx@sint32 ecx; +mull dontcare ecx 0xd01@sint32 ecx; +(* sub %ecx,%eax #! PC = 0x55555555517b *) +cast eax@uint32 eax; +subb carry eax eax ecx; +(* sar $0x10,%eax #! PC = 0x55555555517d *) +cast eax@sint32 eax; +ssplit eax dontcare eax 16; +(* #! <- SP = 0x7fffffffd9b8 *) +#! 0x7fffffffd9b8 = 0x7fffffffd9b8; +(* #retq #! PC = 0x555555555180 *) +#retq #! 0x555555555180 = 0x555555555180; + +{ + true + && + and [ eqsmod ( eax * 65536@32 ) ((sext di 16) * (sext si 16)) (3329@32), + (-3328)@32 <=s eax, + eax <=s 3328@32 ] +} + diff --git a/examples/libjade/kyber/fqmul/fqmul.hw.cl b/examples/libjade/kyber/fqmul/fqmul.cl.0 similarity index 67% rename from examples/libjade/kyber/fqmul/fqmul.hw.cl rename to examples/libjade/kyber/fqmul/fqmul.cl.0 index 0ba3be32..5b4234c9 100644 --- a/examples/libjade/kyber/fqmul/fqmul.hw.cl +++ b/examples/libjade/kyber/fqmul/fqmul.cl.0 @@ -1,50 +1,43 @@ -proc main (sint16 di, sint16 si) = +proc main (di, si) = { true && - and [ - (-3329)@16 <=s di, di SP = 0x7fffffffd968 *) -#! 0x7fffffffd968 = 0x7fffffffd968; - +(* fqmul: *) +fqmul:; +(* #! -> SP = 0x7fffffffd9b8 *) +#! 0x7fffffffd9b8 = 0x7fffffffd9b8; (* movswl %di,%eax #! PC = 0x555555555160 *) cast eax@sint32 di; - (* movswl %si,%ecx #! PC = 0x555555555163 *) cast ecx@sint32 si; - (* imul %ecx,%eax #! PC = 0x555555555166 *) -mul eax ecx eax; - +mull dontcare eax ecx eax; (* imul $0xf301,%eax,%ecx #! PC = 0x555555555169 *) -smull dontcare ecx 0xf301@sint32 eax; - +cast eax@sint32 eax; +mull dontcare ecx 0xf301@sint32 eax; (* shl $0x10,%ecx #! PC = 0x55555555516f *) split dontcare ecx ecx 16; shl ecx ecx 16; - (* sar $0x10,%ecx #! PC = 0x555555555172 *) -(*split ecx dontcare ecx 16;*) - -(*wip*) - +cast ecx@sint32 ecx; +ssplit ecx dontcare ecx 16; (* imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 *) -(*smull dontcare ecx 0xd01@sint32 ecx;*) - +cast ecx@sint32 ecx; +mull dontcare ecx 0xd01@sint32 ecx; (* sub %ecx,%eax #! PC = 0x55555555517b *) -(*subb carry eax eax ecx;*) - +cast eax@uint32 eax; +subb carry eax eax ecx; (* sar $0x10,%eax #! PC = 0x55555555517d *) -(*sar eax eax 0x10;*) - -(* #! <- SP = 0x7fffffffd968 *) -#! 0x7fffffffd968 = 0x7fffffffd968; +cast eax@sint32 eax; +ssplit eax dontcare eax 16; +(* #! <- SP = 0x7fffffffd9b8 *) +#! 0x7fffffffd9b8 = 0x7fffffffd9b8; (* #retq #! PC = 0x555555555180 *) #retq #! 0x555555555180 = 0x555555555180; + { true && diff --git a/examples/libjade/kyber/fqmul/fqmul.gas b/examples/libjade/kyber/fqmul/fqmul.gas new file mode 100644 index 00000000..2f58017a --- /dev/null +++ b/examples/libjade/kyber/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 = 0x0 +# %rsi = 0x0 +# %rdx = 0x0 +# %rcx = 0x555555555190 +# %r8 = 0x0 +# %r9 = 0x7ffff7fe0d50 + #! -> SP = 0x7fffffffd9b8 + movswl %di,%eax #! PC = 0x555555555160 + movswl %si,%ecx #! PC = 0x555555555163 + imul %ecx,%eax #! PC = 0x555555555166 + imul $0xf301,%eax,%ecx #! PC = 0x555555555169 + shl $0x10,%ecx #! PC = 0x55555555516f + sar $0x10,%ecx #! PC = 0x555555555172 + imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 + sub %ecx,%eax #! PC = 0x55555555517b + sar $0x10,%eax #! PC = 0x55555555517d + #! <- SP = 0x7fffffffd9b8 + #retq #! PC = 0x555555555180 diff --git a/examples/libjade/kyber/fqmul/fqmul.gas.0 b/examples/libjade/kyber/fqmul/fqmul.gas.0 new file mode 100644 index 00000000..6fd39f1a --- /dev/null +++ b/examples/libjade/kyber/fqmul/fqmul.gas.0 @@ -0,0 +1,19 @@ +fqmul: +# %rdi = 0x0 +# %rsi = 0x0 +# %rdx = 0x0 +# %rcx = 0x555555555190 +# %r8 = 0x0 +# %r9 = 0x7ffff7fe0d50 + #! -> SP = 0x7fffffffd9b8 + movswl %di,%eax #! PC = 0x555555555160 + movswl %si,%ecx #! PC = 0x555555555163 + imul %ecx,%eax #! PC = 0x555555555166 + imul $0xf301,%eax,%ecx #! PC = 0x555555555169 + shl $0x10,%ecx #! PC = 0x55555555516f + sar $0x10,%ecx #! PC = 0x555555555172 + imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 + sub %ecx,%eax #! PC = 0x55555555517b + sar $0x10,%eax #! PC = 0x55555555517d + #! <- SP = 0x7fffffffd9b8 + #retq #! PC = 0x555555555180 diff --git a/examples/libjade/kyber/fqmul/fqmul.jazz b/examples/libjade/kyber/fqmul/fqmul.jazz index 97cdb7fc..d2bc1829 100644 --- a/examples/libjade/kyber/fqmul/fqmul.jazz +++ b/examples/libjade/kyber/fqmul/fqmul.jazz @@ -1,16 +1,10 @@ param int KYBER_Q = 3329; param int QINV = 62209; /* q^(-1) mod 2^16 */ -param int MONT = 2285; /* 2^16 % Q */ -param int BARR = 20159; /* (1U << 26)/KYBER_Q + 1 */ -export fn fqmul(reg u16 a, reg u16 b) -> reg u16 +export fn fqmul(reg u16 a b) -> reg u16 { - reg u32 ad; - reg u32 bd; - reg u32 c; - reg u32 t; + reg u32 ad bd c t u; reg u16 r; - reg u32 u; ad = (32s)a; bd = (32s)b; @@ -24,7 +18,6 @@ export fn fqmul(reg u16 a, reg u16 b) -> reg u16 t = u * KYBER_Q; t = c - t; - // assert firsts 16 bits as zero t >>s= 16; r = t; diff --git a/examples/libjade/kyber/fqmul/fqmul.s b/examples/libjade/kyber/fqmul/fqmul.s new file mode 100644 index 00000000..a315b1c4 --- /dev/null +++ b/examples/libjade/kyber/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 diff --git a/examples/libjade/kyber/fqmul/main.c b/examples/libjade/kyber/fqmul/main.c new file mode 100644 index 00000000..76ebe0d5 --- /dev/null +++ b/examples/libjade/kyber/fqmul/main.c @@ -0,0 +1,10 @@ +#include + +extern uint16_t fqmul(uint16_t, uint16_t); + +int main(void) +{ + uint16_t r, a, b; + r = fqmul(a, b); + return 0; +} From 3909b24319c394b3b43ae9dcdf4761a0cb3ff2ad Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Fri, 14 Oct 2022 14:45:35 +0100 Subject: [PATCH 4/5] rename example libjade kyber to libjade kyber768 --- examples/libjade/{kyber => kyber768}/fqmul/README.md | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.annotated.cl | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.cl | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.cl.0 | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.gas | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.gas.0 | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.jazz | 0 examples/libjade/{kyber => kyber768}/fqmul/fqmul.s | 0 examples/libjade/{kyber => kyber768}/fqmul/main.c | 0 9 files changed, 0 insertions(+), 0 deletions(-) rename examples/libjade/{kyber => kyber768}/fqmul/README.md (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.annotated.cl (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.cl (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.cl.0 (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.gas (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.gas.0 (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.jazz (100%) rename examples/libjade/{kyber => kyber768}/fqmul/fqmul.s (100%) rename examples/libjade/{kyber => kyber768}/fqmul/main.c (100%) diff --git a/examples/libjade/kyber/fqmul/README.md b/examples/libjade/kyber768/fqmul/README.md similarity index 100% rename from examples/libjade/kyber/fqmul/README.md rename to examples/libjade/kyber768/fqmul/README.md diff --git a/examples/libjade/kyber/fqmul/fqmul.annotated.cl b/examples/libjade/kyber768/fqmul/fqmul.annotated.cl similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.annotated.cl rename to examples/libjade/kyber768/fqmul/fqmul.annotated.cl diff --git a/examples/libjade/kyber/fqmul/fqmul.cl b/examples/libjade/kyber768/fqmul/fqmul.cl similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.cl rename to examples/libjade/kyber768/fqmul/fqmul.cl diff --git a/examples/libjade/kyber/fqmul/fqmul.cl.0 b/examples/libjade/kyber768/fqmul/fqmul.cl.0 similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.cl.0 rename to examples/libjade/kyber768/fqmul/fqmul.cl.0 diff --git a/examples/libjade/kyber/fqmul/fqmul.gas b/examples/libjade/kyber768/fqmul/fqmul.gas similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.gas rename to examples/libjade/kyber768/fqmul/fqmul.gas diff --git a/examples/libjade/kyber/fqmul/fqmul.gas.0 b/examples/libjade/kyber768/fqmul/fqmul.gas.0 similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.gas.0 rename to examples/libjade/kyber768/fqmul/fqmul.gas.0 diff --git a/examples/libjade/kyber/fqmul/fqmul.jazz b/examples/libjade/kyber768/fqmul/fqmul.jazz similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.jazz rename to examples/libjade/kyber768/fqmul/fqmul.jazz diff --git a/examples/libjade/kyber/fqmul/fqmul.s b/examples/libjade/kyber768/fqmul/fqmul.s similarity index 100% rename from examples/libjade/kyber/fqmul/fqmul.s rename to examples/libjade/kyber768/fqmul/fqmul.s diff --git a/examples/libjade/kyber/fqmul/main.c b/examples/libjade/kyber768/fqmul/main.c similarity index 100% rename from examples/libjade/kyber/fqmul/main.c rename to examples/libjade/kyber768/fqmul/main.c From fdd184de00adffa61ada9e6b3a3206ccc5144194 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Tue, 18 Oct 2022 14:30:52 +0100 Subject: [PATCH 5/5] libjade kyber768 fqmul example : main.c implements small test; review required. --- examples/libjade/kyber768/fqmul/README.md | 34 +++++++------- examples/libjade/kyber768/fqmul/fqmul.cl | 49 ++++++++++++++------- examples/libjade/kyber768/fqmul/fqmul.cl.0 | 30 ++++++------- examples/libjade/kyber768/fqmul/fqmul.gas | 28 ++++++------ examples/libjade/kyber768/fqmul/fqmul.gas.0 | 28 ++++++------ examples/libjade/kyber768/fqmul/main.c | 25 +++++++++-- 6 files changed, 117 insertions(+), 77 deletions(-) diff --git a/examples/libjade/kyber768/fqmul/README.md b/examples/libjade/kyber768/fqmul/README.md index 70e6251d..1896f942 100644 --- a/examples/libjade/kyber768/fqmul/README.md +++ b/examples/libjade/kyber768/fqmul/README.md @@ -18,11 +18,11 @@ export fn fqmul(reg u16 a b) -> reg u16 u = c * QINV; u <<= 16; - u >>s= 16; + u >>s= 16; t = u * KYBER_Q; t = c - t; - + t >>s= 16; r = t; @@ -38,24 +38,28 @@ The next step was to write a simple `main` function, using C, that includes a ca 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. +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. +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 fqmul.cl -Parsing CryptoLine file: [OK] 0.000343 seconds -Checking well-formedness: [OK] 0.000064 seconds -Transforming to SSA form: [OK] 0.000020 seconds -Normalizing specification: [OK] 0.000024 seconds -Rewriting assignments: [OK] 0.000009 seconds -Verifying program safety: [OK] 0.030387 seconds -Verifying range specification: [OK] 20.948068 seconds -Rewriting value-preserved casting: [OK] 0.000011 seconds -Verifying algebraic specification: [OK] 0.001294 seconds -Verification result: [OK] 20.980513 seconds +$ 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. diff --git a/examples/libjade/kyber768/fqmul/fqmul.cl b/examples/libjade/kyber768/fqmul/fqmul.cl index 5ea5dc7f..caea1fbc 100644 --- a/examples/libjade/kyber768/fqmul/fqmul.cl +++ b/examples/libjade/kyber768/fqmul/fqmul.cl @@ -1,3 +1,21 @@ +(* +$ 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 @@ -10,37 +28,36 @@ proc main (sint16 di, sint16 si) = (* fqmul: *) #fqmul:; -(* #! -> SP = 0x7fffffffd9b8 *) -#! 0x7fffffffd9b8 = 0x7fffffffd9b8; -(* movswl %di,%eax #! PC = 0x555555555160 *) +(* #! -> SP = 0x7fffffffd9a8 *) +#! 0x7fffffffd9a8 = 0x7fffffffd9a8; +(* movswl %di,%eax #! PC = 0x555555555240 *) cast eax@sint32 di; -(* movswl %si,%ecx #! PC = 0x555555555163 *) +(* movswl %si,%ecx #! PC = 0x555555555243 *) cast ecx@sint32 si; -(* imul %ecx,%eax #! PC = 0x555555555166 *) +(* imul %ecx,%eax #! PC = 0x555555555246 *) mull dontcare eax ecx eax; -(* imul $0xf301,%eax,%ecx #! PC = 0x555555555169 *) +(* imul $0xf301,%eax,%ecx #! PC = 0x555555555249 *) cast eax@sint32 eax; mull dontcare ecx 0xf301@sint32 eax; -(* shl $0x10,%ecx #! PC = 0x55555555516f *) +(* shl $0x10,%ecx #! PC = 0x55555555524f *) split dontcare ecx ecx 16; shl ecx ecx 16; -(* sar $0x10,%ecx #! PC = 0x555555555172 *) +(* sar $0x10,%ecx #! PC = 0x555555555252 *) cast ecx@sint32 ecx; ssplit ecx dontcare ecx 16; -(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 *) +(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555255 *) cast ecx@sint32 ecx; mull dontcare ecx 0xd01@sint32 ecx; -(* sub %ecx,%eax #! PC = 0x55555555517b *) +(* sub %ecx,%eax #! PC = 0x55555555525b *) cast eax@uint32 eax; subb carry eax eax ecx; -(* sar $0x10,%eax #! PC = 0x55555555517d *) +(* sar $0x10,%eax #! PC = 0x55555555525d *) cast eax@sint32 eax; ssplit eax dontcare eax 16; -(* #! <- SP = 0x7fffffffd9b8 *) -#! 0x7fffffffd9b8 = 0x7fffffffd9b8; -(* #retq #! PC = 0x555555555180 *) -#retq #! 0x555555555180 = 0x555555555180; - +(* #! <- SP = 0x7fffffffd9a8 *) +#! 0x7fffffffd9a8 = 0x7fffffffd9a8; +(* #retq #! PC = 0x555555555260 *) +#retq { true && diff --git a/examples/libjade/kyber768/fqmul/fqmul.cl.0 b/examples/libjade/kyber768/fqmul/fqmul.cl.0 index 5b4234c9..d3d72e38 100644 --- a/examples/libjade/kyber768/fqmul/fqmul.cl.0 +++ b/examples/libjade/kyber768/fqmul/fqmul.cl.0 @@ -7,36 +7,36 @@ proc main (di, si) = (* fqmul: *) fqmul:; -(* #! -> SP = 0x7fffffffd9b8 *) -#! 0x7fffffffd9b8 = 0x7fffffffd9b8; -(* movswl %di,%eax #! PC = 0x555555555160 *) +(* #! -> SP = 0x7fffffffd9a8 *) +#! 0x7fffffffd9a8 = 0x7fffffffd9a8; +(* movswl %di,%eax #! PC = 0x555555555240 *) cast eax@sint32 di; -(* movswl %si,%ecx #! PC = 0x555555555163 *) +(* movswl %si,%ecx #! PC = 0x555555555243 *) cast ecx@sint32 si; -(* imul %ecx,%eax #! PC = 0x555555555166 *) +(* imul %ecx,%eax #! PC = 0x555555555246 *) mull dontcare eax ecx eax; -(* imul $0xf301,%eax,%ecx #! PC = 0x555555555169 *) +(* imul $0xf301,%eax,%ecx #! PC = 0x555555555249 *) cast eax@sint32 eax; mull dontcare ecx 0xf301@sint32 eax; -(* shl $0x10,%ecx #! PC = 0x55555555516f *) +(* shl $0x10,%ecx #! PC = 0x55555555524f *) split dontcare ecx ecx 16; shl ecx ecx 16; -(* sar $0x10,%ecx #! PC = 0x555555555172 *) +(* sar $0x10,%ecx #! PC = 0x555555555252 *) cast ecx@sint32 ecx; ssplit ecx dontcare ecx 16; -(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 *) +(* imul $0xd01,%ecx,%ecx #! PC = 0x555555555255 *) cast ecx@sint32 ecx; mull dontcare ecx 0xd01@sint32 ecx; -(* sub %ecx,%eax #! PC = 0x55555555517b *) +(* sub %ecx,%eax #! PC = 0x55555555525b *) cast eax@uint32 eax; subb carry eax eax ecx; -(* sar $0x10,%eax #! PC = 0x55555555517d *) +(* sar $0x10,%eax #! PC = 0x55555555525d *) cast eax@sint32 eax; ssplit eax dontcare eax 16; -(* #! <- SP = 0x7fffffffd9b8 *) -#! 0x7fffffffd9b8 = 0x7fffffffd9b8; -(* #retq #! PC = 0x555555555180 *) -#retq #! 0x555555555180 = 0x555555555180; +(* #! <- SP = 0x7fffffffd9a8 *) +#! 0x7fffffffd9a8 = 0x7fffffffd9a8; +(* #retq #! PC = 0x555555555260 *) +#retq #! 0x555555555260 = 0x555555555260; { true diff --git a/examples/libjade/kyber768/fqmul/fqmul.gas b/examples/libjade/kyber768/fqmul/fqmul.gas index 2f58017a..8cda1d14 100644 --- a/examples/libjade/kyber768/fqmul/fqmul.gas +++ b/examples/libjade/kyber768/fqmul/fqmul.gas @@ -11,21 +11,21 @@ #! sub $1v, $2v -> cast $2v@uint32 $2v;\nsubb carry $2v $2v $1v fqmul: -# %rdi = 0x0 +# %rdi = 0xffff8000 # %rsi = 0x0 # %rdx = 0x0 -# %rcx = 0x555555555190 +# %rcx = 0x555555555270 # %r8 = 0x0 # %r9 = 0x7ffff7fe0d50 - #! -> SP = 0x7fffffffd9b8 - movswl %di,%eax #! PC = 0x555555555160 - movswl %si,%ecx #! PC = 0x555555555163 - imul %ecx,%eax #! PC = 0x555555555166 - imul $0xf301,%eax,%ecx #! PC = 0x555555555169 - shl $0x10,%ecx #! PC = 0x55555555516f - sar $0x10,%ecx #! PC = 0x555555555172 - imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 - sub %ecx,%eax #! PC = 0x55555555517b - sar $0x10,%eax #! PC = 0x55555555517d - #! <- SP = 0x7fffffffd9b8 - #retq #! PC = 0x555555555180 + #! -> 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 diff --git a/examples/libjade/kyber768/fqmul/fqmul.gas.0 b/examples/libjade/kyber768/fqmul/fqmul.gas.0 index 6fd39f1a..7cebc4d0 100644 --- a/examples/libjade/kyber768/fqmul/fqmul.gas.0 +++ b/examples/libjade/kyber768/fqmul/fqmul.gas.0 @@ -1,19 +1,19 @@ fqmul: -# %rdi = 0x0 +# %rdi = 0xffff8000 # %rsi = 0x0 # %rdx = 0x0 -# %rcx = 0x555555555190 +# %rcx = 0x555555555270 # %r8 = 0x0 # %r9 = 0x7ffff7fe0d50 - #! -> SP = 0x7fffffffd9b8 - movswl %di,%eax #! PC = 0x555555555160 - movswl %si,%ecx #! PC = 0x555555555163 - imul %ecx,%eax #! PC = 0x555555555166 - imul $0xf301,%eax,%ecx #! PC = 0x555555555169 - shl $0x10,%ecx #! PC = 0x55555555516f - sar $0x10,%ecx #! PC = 0x555555555172 - imul $0xd01,%ecx,%ecx #! PC = 0x555555555175 - sub %ecx,%eax #! PC = 0x55555555517b - sar $0x10,%eax #! PC = 0x55555555517d - #! <- SP = 0x7fffffffd9b8 - #retq #! PC = 0x555555555180 + #! -> 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 diff --git a/examples/libjade/kyber768/fqmul/main.c b/examples/libjade/kyber768/fqmul/main.c index 76ebe0d5..6e936741 100644 --- a/examples/libjade/kyber768/fqmul/main.c +++ b/examples/libjade/kyber768/fqmul/main.c @@ -1,10 +1,29 @@ #include +#include -extern uint16_t fqmul(uint16_t, uint16_t); +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) { - uint16_t r, a, b; - r = fqmul(a, b); + 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; }