ref: annotate loops to guide the safety checker

With these annotations, the key generation function can be proved safe by the automatic safety checker. The “no-termination-check” annotation in gen-matrix acknowledges that proving (propabilistic) termination of this loop is beyond the scope of the automated checker and must be justified by other means.
formosa-crypto · Mar 13, 2023 · 511a108 · 511a108
1 parent 5be30db
commit 511a108
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 0 deletions.
diff --git a/code/jasmin/ref/gen_matrix.jinc b/code/jasmin/ref/gen_matrix.jinc
@@ -95,12 +95,14 @@ fn __gen_matrix(stack u8[KYBER_SYMBYTES] seed, reg u64 transposed) -> stack u16[
 
       // Initialize the poly array
       ctr = 0;
+      #bounded
       while (ctr < KYBER_N / 4) {
         poly[u64 (int) ctr] = ctr;
         ctr += 1;
       }
 
       ctr = 0;
+      #no_termination_check
       while (ctr < KYBER_N)
       {
         sctr = ctr;
@@ -111,6 +113,7 @@ fn __gen_matrix(stack u8[KYBER_SYMBYTES] seed, reg u64 transposed) -> stack u16[
 
       k = 0;
       l = i * KYBER_VECN + j * KYBER_N;
+      #bounded
       while (k < KYBER_N)
       {
         t = poly[(int) k];

diff --git a/code/jasmin/ref/indcpa.jinc b/code/jasmin/ref/indcpa.jinc
@@ -99,6 +99,7 @@ fn __indcpa_enc(stack u64 sctp, reg ptr u8[32] msgp, reg u64 pkp, reg ptr u8[KYB
 
   i = 0;
   pkp += KYBER_POLYVECBYTES;
+  #bounded
   while (i < KYBER_SYMBYTES/8)
   {
     t64 = (u64)[pkp];
@@ -169,6 +170,7 @@ fn __iindcpa_enc(reg ptr u8[KYBER_CT_LEN] ctp, reg ptr u8[32] msgp, reg u64 pkp,
 
   i = 0;
   pkp += KYBER_POLYVECBYTES;
+  #bounded
   while (i < KYBER_SYMBYTES/8)
   {
     t64 = (u64)[pkp];

diff --git a/code/jasmin/ref/jindcpa.jazz b/code/jasmin/ref/jindcpa.jazz
@@ -23,6 +23,7 @@ export fn indcpa_keypair_jazz(reg u64 pkp, reg u64 skp, reg u64 randomnessp)
   sskp = skp;
 
   i = 0;
+  #bounded
   while (i < KYBER_SYMBYTES)
   {
     c = (u8)[randomnessp + i];
@@ -34,6 +35,7 @@ export fn indcpa_keypair_jazz(reg u64 pkp, reg u64 skp, reg u64 randomnessp)
 
   i = 0;
   j = KYBER_SYMBYTES;
+  #bounded
   while (i < KYBER_SYMBYTES)
   {
     c = buf[(int)i];
@@ -107,6 +109,7 @@ export fn indcpa_enc_jazz(reg u64 ctp, reg u64 msgp, reg u64 pkp, reg u64 coinsp
   sctp = ctp;
 
   i = 0;
+  #bounded
   while (i < KYBER_SYMBYTES)
   {
     c = (u8)[coinsp+i];
@@ -118,6 +121,7 @@ export fn indcpa_enc_jazz(reg u64 ctp, reg u64 msgp, reg u64 pkp, reg u64 coinsp
 
   i = 0;
   pkp += KYBER_POLYVECBYTES;
+  #bounded
   while (i < KYBER_SYMBYTES)
   {
     c = (u8)[pkp];

diff --git a/code/jasmin/ref/poly.jinc b/code/jasmin/ref/poly.jinc
@@ -65,6 +65,7 @@ fn _poly_basemul(reg ptr u16[KYBER_N] rp, reg const ptr u16[KYBER_N] ap bp) -> r
   zetasctr = 64;
   i = 0;
 
+  #bounded
   while(i < KYBER_N)
   {
     zetasp = jzetas;
@@ -150,6 +151,7 @@ fn _poly_compress(reg u64 rp, reg ptr u16[KYBER_N] a) -> reg ptr u16[KYBER_N]
 
   i = 0;
   j = 0;
+  #bounded
   while(i < 128)
   {
     t  = a[(int)j];
@@ -186,6 +188,7 @@ fn _i_poly_compress(reg ptr u8[KYBER_POLYCOMPRESSEDBYTES] rp, reg ptr u16[KYBER_
 
   i = 0;
   j = 0;
+  #bounded
   while(i < 128)
   {
     t  = a[(int)j];
@@ -222,6 +225,7 @@ fn _poly_decompress(reg ptr u16[KYBER_N] rp, reg u64 ap) -> stack u16[KYBER_N]
   i = 0;
   j = 0;
 
+  #bounded
   while (i < 128) {
     t  = (u8)[ap+i];
     d0 = (16u)t;
@@ -443,6 +447,7 @@ fn _poly_getnoise(reg ptr u16[KYBER_N] rp, reg ptr u8[KYBER_SYMBYTES] seed, reg
 
   i = 0;
   j = 0;
+  #bounded
   while (i < 128) {
     c = buf[(int)i];
     a = c;
@@ -496,16 +501,19 @@ fn _poly_invntt(reg ptr u16[KYBER_N] rp) -> reg ptr u16[KYBER_N]
   zetasctr = 0;
 
   len = 2;
+  #bounded
   while (len <= 128)
   {
     start = 0;
+    #bounded
     while (start < 256)
     {
       zeta = zetasp[(int)zetasctr];
       zetasctr += 1;
 
       j = start;
       cmp = start + len;
+      #bounded
       while (j < cmp)
       {
         offset = j + len;
@@ -555,15 +563,18 @@ fn _poly_ntt(reg ptr u16[KYBER_N] rp) -> reg ptr u16[KYBER_N]
   zetasp = jzetas;
   zetasctr = 0;
   len = 128;
+  #bounded
   while (len >= 2)
   {
     start = 0;
+    #bounded
     while (start < 256)
     {
       zetasctr += 1;
       zeta = zetasp[(int)zetasctr];
       j = start;
       cmp = start + len;
+      #bounded
       while (j < cmp)
       {
         offset = j + len;
@@ -595,6 +606,7 @@ fn _poly_sub(reg ptr u16[KYBER_N] rp ap bp) -> reg ptr u16[KYBER_N]
   reg u64 i;
 
   i = 0;
+  #bounded
   while (i < KYBER_N) {
     a = ap[(int)i];
     b = bp[(int)i];

diff --git a/code/jasmin/ref/polyvec.jinc b/code/jasmin/ref/polyvec.jinc
@@ -100,6 +100,7 @@ fn __i_polyvec_compress(reg ptr u8[KYBER_POLYVECCOMPRESSEDBYTES] rp, stack u16[K
 
   aa = __polyvec_csubq(a);
 
+  #bounded
   while (i < KYBER_VECN)
   {
     for k = 0 to 4
@@ -163,6 +164,7 @@ fn __polyvec_decompress(reg u64 ap) -> stack u16[KYBER_VECN]
   i = 0;
   j = 0;
 
+  #bounded
   while (i < KYBER_VECN)
   {
     for k = 0 to 5