From 8b38bc23c13bb93f20c6955bddac3e33976d7b16 Mon Sep 17 00:00:00 2001
From: Joao Diogo Duarte <joao@diogoduarte.pt>
Date: Mon, 28 Oct 2024 18:13:26 +0000
Subject: [PATCH 1/2] PR commit

---
 .../jazzline/curve25519/common/add4/add4.jazz | 72 +++++++++++++++++++
 compiler/src/toCL.ml                          | 12 +++-
 2 files changed, 83 insertions(+), 1 deletion(-)
 create mode 100644 compiler/examples/jazzline/curve25519/common/add4/add4.jazz

diff --git a/compiler/examples/jazzline/curve25519/common/add4/add4.jazz b/compiler/examples/jazzline/curve25519/common/add4/add4.jazz
new file mode 100644
index 000000000..34eab65e4
--- /dev/null
+++ b/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;
+}
diff --git a/compiler/src/toCL.ml b/compiler/src/toCL.ml
index 3495fa2df..9fe292f44 100644
--- a/compiler/src/toCL.ml
+++ b/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 =

From 47ef562bf3d1ee1fbfc5252a53efd628c5b1d5ec Mon Sep 17 00:00:00 2001
From: Joao Diogo Duarte <joao@diogoduarte.pt>
Date: Sat, 9 Nov 2024 20:49:03 +0000
Subject: [PATCH 2/2] Add4 now uses copy and set0 to match formosa-25519
 implementation

---
 .../examples/jazzline/curve25519/common/add4/add4.jazz   | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/compiler/examples/jazzline/curve25519/common/add4/add4.jazz b/compiler/examples/jazzline/curve25519/common/add4/add4.jazz
index 34eab65e4..3a1ffbb8c 100644
--- a/compiler/examples/jazzline/curve25519/common/add4/add4.jazz
+++ b/compiler/examples/jazzline/curve25519/common/add4/add4.jazz
@@ -23,11 +23,8 @@ inline fn __add4_rrs(reg u64[4] f, stack u64[4] g) -> reg u64[4]
   reg u64 z;
   reg bool cf, carryo;
 
-  z = 0;
-
-  for i=0 to 4 {
-      h[i] = f[i];
-  }
+  ?{}, z = #set0();
+  h = #copy(f);
 
   cf, h[0] += g[0];
 
@@ -46,7 +43,7 @@ inline fn __add4_rrs(reg u64[4] f, stack u64[4] g) -> reg u64[4]
   #[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;}