PR commit

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

@@ -0,0 +1,72 @@
+// 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 = 0;
+
+  for i=0 to 4 {
+      h[i] = f[i];
+  }
+
+  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;
+j
+  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/src/toCL.ml

@@ -518,12 +518,14 @@ module I (S:S): I = struct
     let (!>) e = gexp_to_rexp ~sign e in
     let (!>>) e = gexp_to_rpred ~sign e in
     match e with
+    | Pvar { gv = { pl_desc = { v_ty=Bty Bool }}} -> eq !> e (Rconst(1, Z.of_int 1))
     | Pbool (true) -> RPand []
     | Papp1(Onot, e) -> RPnot (!>> e)
     | Papp2(Oand, e1, e2)  -> RPand [!>> e1; !>> e2]
     | Papp2(Oor, e1, e2)  -> RPor [!>> e1; !>> e2]
     | Papp2(Ole int, e1, e2)  -> ule !> e1 !> e2
     | Papp2(Oge int, e1, e2)  -> uge !> e1 !> e2
+    | Papp2(Obeq, e1, e2)
     | Papp2(Oeq _, e1, e2) -> eq !> e1 !> e2
     | Papp2(Olt int, e1, e2)  -> ult !> e1 !> e2
     | Papp2(Ogt int, e1, e2)  -> ugt !> e1 !> e2
@@ -612,7 +614,15 @@ module I (S:S): I = struct
               (Pconst (w2i ~sign z U16)) 
          | _ -> !> v 
        end 
-    (* | Pabstract ({name="pow"}, [b;e]) -> power !> b !> e *)
+    | Pabstract ({name="pow"}, [b;e]) -> power !> b !> e
+    | Pabstract ({name="u64i"}, [v]) ->
+       begin
+         match v with
+         | Papp1 (Oword_of_int _ws, Pconst z) ->  !>
+              (Pconst (w2i ~sign z U64))
+         | _ -> !> v
+      end
+    | Pabstract ({name="b2i"}, [v]) -> !> v
     | Pabstract ({name="mon"}, [c;a;b]) ->
       let c = get_const c in
       let v =