Merge branch 'main' into feature/armv7m

proof/crypto_scalarmult/curve25519/amd64/mulx/extracted_ct_proof.ec

@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_mulx : 
   M.jade_scalarmult_curve25519_amd64_mulx ~ M.jade_scalarmult_curve25519_amd64_mulx :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_mulx_base : 
   M.jade_scalarmult_curve25519_amd64_mulx_base ~ M.jade_scalarmult_curve25519_amd64_mulx_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.

proof/crypto_scalarmult/curve25519/amd64/ref4/extracted_ct_proof.ec

@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_ref4 : 
   M.jade_scalarmult_curve25519_amd64_ref4 ~ M.jade_scalarmult_curve25519_amd64_ref4 :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_ref4_base : 
   M.jade_scalarmult_curve25519_amd64_ref4_base ~ M.jade_scalarmult_curve25519_amd64_ref4_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.

proof/crypto_scalarmult/curve25519/amd64/ref5/extracted_ct_proof.ec

@@ -2,14 +2,14 @@ require import Extracted_ct.
 
 equiv jade_scalarmult_curve25519_amd64_ref5 : 
   M.jade_scalarmult_curve25519_amd64_ref5 ~ M.jade_scalarmult_curve25519_amd64_ref5 :
-    ={q, n, p, M.leakages} ==> ={M.leakages}.
+    ={qp, np, pp, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.
 
 equiv jade_scalarmult_curve25519_amd64_ref5_base : 
   M.jade_scalarmult_curve25519_amd64_ref5_base ~ M.jade_scalarmult_curve25519_amd64_ref5_base :
-    ={q, n, M.leakages} ==> ={M.leakages}.
+    ={qp, np, M.leakages} ==> ={M.leakages}.
 proof.
 proc; inline *; sim => />.
 qed.

src/crypto_scalarmult/curve25519/amd64/common/51/decode_u5.jinc

@@ -0,0 +1,53 @@
+inline fn __decode_u_coordinate5(reg u64[4] t) -> reg u64[5]
+{
+  reg u64[5] u;
+  reg u64 mask;
+
+  mask = 0x7ffffffffffff;
+
+  //u[0] = t[0] & mask; // 51; 13 left
+  u[0] = t[0];
+  u[0] &= mask;
+
+  //u[1] = (t[1] << 13) || (t[0] >> 51) & mask; // 38; 26 left
+  u[1] = t[1];
+  u[1] <<= 13;
+  t[0] >>= 51;
+  u[1] |= t[0];
+  u[1] &= mask;
+
+  //u[2] = (t[2] << 26) || (t[1] >> 38) & mask; // 25; 39 left
+  u[2] = t[2];
+  u[2] <<= 26;
+  t[1] >>= 38;
+  u[2] |= t[1];
+  u[2] &= mask;
+
+  //u[3] = (t[3] << 39) || (t[2] >> 25) & mask; // 12; '52' left
+  u[3] = t[3];
+  u[3] <<= 39;
+  t[2] >>= 25;
+  u[3] |= t[2];
+  u[3] &= mask;
+
+  //u[4] = (t[3] >> 12) & mask;
+  u[4] = t[3];
+  u[4] >>= 12;
+  u[4] &= mask;
+
+  return u;
+}
+
+inline fn __decode_u_coordinate_base5() -> reg u64[5]
+{
+  reg u64[5] u;
+
+  u[0] = 9;
+  u[1] = 0;
+  u[2] = 0;
+  u[3] = 0;
+  u[4] = 0;
+
+  return u;
+}
+

src/crypto_scalarmult/curve25519/amd64/common/51/init_points5.jinc

@@ -0,0 +1,56 @@
+inline fn __init_points5(
+  reg u64[5] initr)
+  ->
+  stack u64[5],
+  reg   u64[5],
+  stack u64[5],
+  stack u64[5]
+{
+  inline int i;
+  stack u64[5] x2 x3 z3;
+  reg u64[5] z2r;
+  reg u64 z;
+
+  ?{}, z = #set0();
+
+  x2[0] = 1;
+  z2r[0] = 0;
+  x3 = #copy(initr);
+  z3[0] = 1;
+
+  for i=1 to 5
+  { x2[i] = z;
+    z2r[i] = z;
+    z3[i] = z;
+  }
+
+  //     (1,   0, init, 1)
+  return x2, z2r, x3,  z3;
+}
+
+inline fn __init_points5_x3()
+  ->
+  stack u64[5],
+  reg   u64[5],
+  stack u64[5]
+{
+  inline int i;
+  stack u64[5] f1s f3s;
+  reg   u64[5] f2;
+  reg   u64 z;
+
+  ?{}, z = #set0();
+
+  f1s[0] = 1;
+  f2[0]  = 1;
+  f3s[0] = 1;
+
+  for i=1 to 5
+  { f1s[i] = z;
+    f2[i]  = z;
+    f3s[i] = z;
+  }
+
+  return f1s, f2, f3s;
+}
+

src/crypto_scalarmult/curve25519/amd64/common/64/decode_u4.jinc

@@ -0,0 +1,18 @@
+inline fn __decode_u_coordinate4(reg u64[4] u) -> reg u64[4]
+{
+  u[3] &= 0x7fffffffffffffff;
+  return u;
+}
+
+inline fn __decode_u_coordinate_base4() -> reg u64[4]
+{
+  reg u64[4] u;
+
+  u[0] = 9;
+  u[1] = 0;
+  u[2] = 0;
+  u[3] = 0;
+
+  return u;
+}
+

src/crypto_scalarmult/curve25519/amd64/common/64/load4.jinc → src/crypto_scalarmult/curve25519/amd64/common/64/init_points4.jinc

@@ -1,27 +1,3 @@
-inline fn __decode_u_coordinate4(reg u64 up) -> reg u64[4]
-{
-  inline int i;
-  reg u64[4] u;
-
-  for i=0 to 4
-  { u[i] = [up + 8*i]; }
-  u[3] &= 0x7fffffffffffffff;
-
-  return u;
-}
-
-inline fn __decode_u_coordinate_base4() -> reg u64[4]
-{
-  reg u64[4] u;
-
-  u[0] = 9;
-  u[1] = 0;
-  u[2] = 0;
-  u[3] = 0;
-
-  return u;
-}
-
 inline fn __init_points4(
   reg u64[4] initr)
   ->

src/crypto_scalarmult/curve25519/amd64/common/decode_scalar.jinc

@@ -0,0 +1,28 @@
+inline fn __decode_scalar(reg u64[4] k) -> stack u8[32]
+{
+  inline int i;
+  stack u8[32] ks;
+
+  for i=0 to 4
+  { ks[u64 i] = k[i]; }
+
+  ks[0]  &= 0xf8;
+  ks[31] &= 0x7f;
+  ks[31] |= 0x40;
+
+  return ks;
+}
+
+inline fn __decode_scalar_shl1(reg u64[4] k) -> stack u64[4]
+{
+  stack u64[4] ks;
+
+  k[3] <<= 1;
+  k[0] &= 0xfffffffffffffff8;
+  k[3] |= 0x8000000000000000;
+
+  ks = #copy(k);
+
+  return ks;
+}
+