Cryptoline curve25519 examples

compiler/examples/jazzline/curve25519/common/add4/add4.jazz

@@ -0,0 +1,69 @@
+// h = f + g
+// h = 2**0*f0 + 2**64*f1 + 2**128*f2 + 2**192*f3 +
+//     2**0*g0 + 2**64*g1 + 2**128*g2 + 2**192*g3
+
+abstract predicate bool eqmod(int, int, tuple);
+abstract predicate tuple single(int);
+abstract predicate int b2i(bool);
+abstract predicate int u64i(u64);
+abstract predicate int pow(int, int);
+
+inline fn __add4_rrs(reg u64[4] f, stack u64[4] g) -> reg u64[4]
+  ensures #[prover=cas] {
+  eqmod (
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(result.0[ii])),
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(f[ii])) + \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(g[ii])),
+     single((pow(2,255)) - 19)
+    )
+  }
+{
+  inline int i;
+
+  reg u64[4] h;
+  reg u64 z;
+  reg bool cf, carryo;
+
+  ?{}, z = #set0();
+  h = #copy(f);
+
+  cf, h[0] += g[0];
+
+  for i=1 to 4
+  { cf, h[i] += g[i] + cf; }
+
+  carryo = cf;
+  cf, z -= z - cf;
+
+  #[kind=Assert, prover=smt] assert (cf == carryo);
+  #[kind=Assume, prover=cas] assert (b2i(cf) ==  b2i(carryo));
+
+  z &= 38;
+
+  #[kind=Assert, prover=smt] assert ((!cf && z == 0x0) || (cf && z == 0x26));
+  #[kind=Assume, prover=cas] assert (u64i(z) == b2i(cf)*0x26);
+
+  cf, h[0] += z;
+
+  for i=1 to 4
+  { cf, h[i] += 0 + cf;}
+
+  carryo = cf;
+  cf, z -= z - cf;
+
+  #[kind=Assert, prover=smt] assert (cf == carryo);
+  #[kind=Assume, prover=cas] assert (b2i(cf) ==  b2i(carryo));
+
+
+  z &= 38;
+
+  #[kind=Assert, prover=smt] assert ((!cf && z == 0x0) || (cf && z == 0x26));
+  #[kind=Assume, prover=cas] assert (u64i(z) == b2i(cf)*0x26);
+
+
+  cf, h[0] += z;
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+
+  return h;
+}

compiler/examples/jazzline/curve25519/common/sub4/sub4.jazz

@@ -0,0 +1,63 @@
+abstract predicate bool eqmod(int, int, tuple);
+abstract predicate tuple single(int);
+abstract predicate int b2i(bool);
+abstract predicate int u64i(u64);
+abstract predicate int pow(int, int);
+
+inline fn __sub4_rrs(reg u64[4] f, stack u64[4] gs) -> reg u64[4]
+  ensures #[prover=cas] {
+  eqmod (
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(result.0[ii])),
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(f[ii])) - \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(gs[ii])),
+     single((pow(2,255)) - 19)
+    )
+  }
+{
+  inline int i;
+  reg bool cf, borrowo;
+  reg u64[4] h;
+  reg u64 z;
+
+  z = #set0_64();
+
+  h = #copy(f);
+
+
+  cf, h[0] -= gs[0];
+  for i=1 to 4
+  { cf, h[i] -= gs[i] - cf; }
+
+  borrowo = cf;
+  cf, z -= z - cf;
+
+  #[kind=Assert, prover=smt] assert (cf == borrowo);
+  #[kind=Assume, prover=cas] assert (b2i(cf) ==  b2i(borrowo));
+
+  z &= 38;
+
+  #[kind=Assert, prover=smt] assert ((!cf && z == 0x0) || (cf && z == 0x26));
+  #[kind=Assume, prover=cas] assert (u64i(z) == b2i(cf)*0x26);
+
+  cf, h[0] -= z;
+  for i=1 to 4
+  { cf, h[i] -= 0 - cf; }
+
+  borrowo = cf;
+  cf, z -= z - cf;
+
+  #[kind=Assert, prover=smt] assert (cf == borrowo);
+  #[kind=Assume, prover=cas] assert (b2i(cf) ==  b2i(borrowo));
+
+  z &= 38;
+
+
+  #[kind=Assert, prover=smt] assert ((!cf && z == 0x0) || (cf && z == 0x26));
+  #[kind=Assume, prover=cas] assert (u64i(z) == b2i(cf)*0x26);
+
+  cf, h[0] -= z;
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+
+  return h;
+}

compiler/examples/jazzline/curve25519/mulx/mul4/mul4_a24.jazz

@@ -0,0 +1,66 @@
+abstract predicate bool eqmod(int, int, tuple);
+abstract predicate tuple single(int);
+abstract predicate int b2i(bool);
+abstract predicate int u64i(u64);
+abstract predicate int pow(int, int);
+
+inline fn __mul4_a24_rs(reg u64[4] fs) -> reg u64[4]
+ ensures #[prover=cas] {
+  eqmod (
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(result.0[ii])),
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(fs[ii])) * 121665,
+     single((pow(2,255)) - 19)
+    )
+  }
+
+{
+  reg bool cf carryo;
+  reg u64[4] h;
+  reg u64 c r0 lo;
+
+  c = (64u)121665;
+  #[kind=Assert, prover=smt] assert (c == 121665);
+  #[kind=Assume, prover=cas] assert (u64i(c) == 121665);
+
+  (h[1], h[0]) = #MULX(c, fs[0]);
+  (h[2], lo)   = #MULX(c, fs[1]);
+
+  cf, h[1] += lo;
+
+  (h[3], lo)   = #MULX(c, fs[2]);
+
+  cf, h[2] += lo + cf;
+
+  (r0,   lo)   = #MULX(c, fs[3]);
+
+  cf, h[3] += lo + cf;
+
+  cf, r0 += 0 + cf;
+
+  _, _, _, _, _, r0 = #IMULri (r0, 38);
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+
+  cf, h[0] += r0;
+  cf, h[1] += 0 + cf;
+  cf, h[2] += 0 + cf;
+  cf, h[3] += 0 + cf;
+
+  carryo = cf;
+  cf, c -= c - cf;
+
+  #[kind=Assert, prover=smt] assert (cf == carryo);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == b2i(carryo));
+
+  c &= 38;
+  #[kind=Assert, prover=smt] assert ((!cf && c == 0x0) || (cf && c == 0x26));
+  #[kind=Assume, prover=cas] assert (u64i(c) == b2i(cf)*0x26);
+
+  cf, h[0] += c;
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+
+  return h;
+}

compiler/examples/jazzline/curve25519/mulx/mul4/mul4_rsr.jazz

@@ -0,0 +1,198 @@
+require "reduce4.jazz"
+
+abstract predicate bool eqmod(int, int, tuple);
+abstract predicate tuple single(int);
+abstract predicate int b2i(bool);
+abstract predicate int u64i(u64);
+abstract predicate int pow(int, int);
+
+inline fn __mul4_c0
+( reg u64    f0,
+  reg u64[4] g,
+  reg u64    z, // zero
+  reg bool   cf of // cf = 0 and of = 0
+  ) ->
+  reg u64[4],
+  reg u64[4],
+  reg bool,
+  reg bool
+{
+  reg u64 lo;
+  reg u64[4] h r;
+
+  (h[1], h[0]) = #MULX ( f0, g[0] );
+
+  ( h[2], lo ) = #MULX ( f0, g[1] );
+    cf, h[1]   = #ADCX ( h[1], lo, cf );
+
+  ( h[3], lo ) = #MULX ( f0, g[2] );
+    cf, h[2]   = #ADCX ( h[2], lo, cf );
+
+  ( r[0], lo ) = #MULX ( f0, g[3] );
+    cf, h[3]   = #ADCX ( h[3], lo, cf );
+
+  cf, r[0] = #ADCX ( r[0], z, cf ); // cf = 0
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+
+  return h, r, cf, of;
+}
+
+inline fn __mul4_c1
+( reg u64[4] h,
+  reg u64[4] r,
+  reg u64    f,
+  reg u64[4] g,
+  reg u64    z, // zero
+  reg bool   cf of // cf = 0 and of = 0
+  ) ->
+  reg u64[4],
+  reg u64[4],
+  reg bool,
+  reg bool
+{
+  reg u64 hi lo;
+
+  ( hi, lo )   = #MULX ( f, g[0] );
+  of, h[1]     = #ADOX ( h[1], lo, of );
+  cf, h[2]     = #ADCX ( h[2], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[1] );
+  of, h[2]     = #ADOX ( h[2], lo, of );
+  cf, h[3]     = #ADCX ( h[3], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[2] );
+  of, h[3]     = #ADOX ( h[3], lo, of );
+  cf, r[0]     = #ADCX ( r[0], hi, cf );
+
+  ( r[1], lo ) = #MULX ( f, g[3] );
+  of, r[0]     = #ADOX ( r[0], lo, of);
+
+  cf, r[1]     = #ADCX ( r[1], z, cf);
+  of, r[1]     = #ADOX ( r[1], z, of);
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+  #[kind=Assert, prover=smt] assert (!of);
+  #[kind=Assume, prover=cas] assert (b2i(of) == 0);
+
+
+  return h, r, cf, of;
+}
+
+inline fn __mul4_c2
+( reg u64[4] h,
+  reg u64[4] r,
+  reg u64    f,
+  reg u64[4] g,
+  reg u64    z, // zero
+  reg bool   cf of // cf = 0 and of = 0
+  ) ->
+  reg u64[4],
+  reg u64[4],
+  reg bool,
+  reg bool
+{
+  reg u64 hi lo;
+
+  ( hi, lo )   = #MULX ( f, g[0] );
+  of, h[2]     = #ADOX ( h[2], lo, of );
+  cf, h[3]     = #ADCX ( h[3], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[1] );
+  of, h[3]     = #ADOX ( h[3], lo, of );
+  cf, r[0]     = #ADCX ( r[0], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[2] );
+  of, r[0]     = #ADOX ( r[0], lo, of );
+  cf, r[1]     = #ADCX ( r[1], hi, cf );
+
+  ( r[2], lo ) = #MULX ( f, g[3] );
+  of, r[1]     = #ADOX ( r[1], lo, of);
+
+  cf, r[2]     = #ADCX ( r[2], z, cf);
+  of, r[2]     = #ADOX ( r[2], z, of);
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+  #[kind=Assert, prover=smt] assert (!of);
+  #[kind=Assume, prover=cas] assert (b2i(of) == 0);
+return h, r, cf, of;
+}
+
+inline fn __mul4_c3
+( reg u64[4] h,
+  reg u64[4] r,
+  reg u64    f,
+  reg u64[4] g,
+  reg u64    z, // zero
+  reg bool   cf of // cf = 0 and of = 0
+  ) ->
+  reg u64[4],
+  reg u64[4],
+  reg bool,
+  reg bool
+{
+  reg u64 hi lo;
+
+  ( hi, lo )   = #MULX ( f, g[0] );
+  of, h[3]     = #ADOX ( h[3], lo, of );
+  cf, r[0]     = #ADCX ( r[0], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[1] );
+  of, r[0]     = #ADOX ( r[0], lo, of );
+  cf, r[1]     = #ADCX ( r[1], hi, cf );
+
+  ( hi, lo )   = #MULX ( f, g[2] );
+  of, r[1]     = #ADOX ( r[1], lo, of );
+  cf, r[2]     = #ADCX ( r[2], hi, cf );
+
+  ( r[3], lo ) = #MULX ( f, g[3] );
+  of, r[2]     = #ADOX ( r[2], lo, of);
+
+  cf, r[3]     = #ADCX ( r[3], z, cf);
+  of, r[3]     = #ADOX ( r[3], z, of);
+
+  #[kind=Assert, prover=smt] assert (!cf);
+  #[kind=Assume, prover=cas] assert (b2i(cf) == 0);
+  #[kind=Assert, prover=smt] assert (!of);
+  #[kind=Assume, prover=cas] assert (b2i(of) == 0);
+
+  return h, r, cf, of;
+}
+
+inline fn __mul4_rsr(stack u64[4] fs, reg u64[4] g) -> reg u64[4]
+ ensures #[prover=cas] {
+  eqmod (
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(result.0[ii])),
+     \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(fs[ii])) * \sum (ii \in 0:4) (pow(2, 64*ii)*u64i(g[ii])),
+     single((pow(2,255)) - 19)
+    )
+  }
+
+{
+  reg bool cf of;
+  reg u64[4] h r g0;
+  reg u64 _38 f z;
+
+  g0 = #copy(g);
+  z = 0;
+
+  f = fs[0];
+  h, r, cf, of = __mul4_c0(      f, g0, z, cf, of);
+
+  f = fs[1];
+  h, r, cf, of = __mul4_c1(h, r, f, g0, z, cf, of);
+
+  f = fs[2];
+  h, r, cf, of = __mul4_c2(h, r, f, g0, z, cf, of);
+
+  f = fs[3];
+  h, r, cf, of = __mul4_c3(h, r, f, g0, z, cf, of);
+
+  _38 = 38;
+  h = __reduce4(h, r, _38, z, cf, of);
+
+  return h;
+}