Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Modified toCL to be able to run mula24 ref example and added the mula24 ref example #945

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions compiler/examples/jazzline/curve25519/common/add4/add4.jazz
Original file line number Diff line number Diff line change
@@ -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;
}
71 changes: 71 additions & 0 deletions compiler/examples/jazzline/curve25519/ref4/mul4/mul4_a24.jazz
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
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] xa) -> 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(xa[ii])) * 121666,
single((pow(2,255)) - 19)
)
}
{
reg u64 rax rdx c t1 t2 t3 t4;
reg u64[4] r;
reg bool cf;
stack u64 dc;

c = (64u)121666;
#[kind=Assert, prover=smt] assert (c == (64u)121666);
#[kind=Assume, prover=cas] assert (u64i(c) == 121666);

rax = xa[0];
rdx, rax = rax * c;
r[0] = rax;
r[1] = rdx;

rax = xa[2];
rdx, rax = rax * c;
r[2] = rax; r[3] = rdx;

rax = xa[1];
rdx, rax = rax * c;
t1 = rax;
t2 = rdx;

rax = xa[3];
rdx, rax = rax * c;
t3 = rax;
t4 = rdx;

cf, r[1] += t1;
cf, r[2] += t2 + cf;
cf, r[3] += t3 + cf;
cf, t4 += 0 + cf;

#[kind=Assert, prover=smt] assert (!cf);
#[kind=Assume, prover=cas] assert (b2i(cf) == 0);

dc, t4 *= 38;

#[kind=Assert, prover=smt] assert (dc == 0);
#[kind=Assume, prover=cas] assert (dc == 0);

cf, r[0] += t4;
cf, r[1] += 0 + cf;
cf, r[2] += 0 + cf;
cf, r[3] += 0 + cf;

t1 = 38;
t2 = #MOV(0);
t1 = t2 if !cf;
cf, r[0] += t1;

#[kind=Assert, prover=smt] assert (!cf);
#[kind=Assume, prover=cas] assert (b2i(cf) == 0);

return r;
}
33 changes: 31 additions & 2 deletions compiler/src/toCL.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -803,6 +813,20 @@ module X86BaseOpU : BaseOp
let l = I.glval_to_lval (List.nth xs 0) in
i @ [CL.Instr.Op1.mov l a]

| CMOVcc ws -> (* warning, does not work with ! cf *)
let a2, i2 = cast_atome ws (List.nth es 1) in
let a3, i3 = cast_atome ws (List.nth es 2) in
let x1 = I.glval_to_lval (List.nth xs 0) in
begin match (List.nth es 0) with
| Pvar _ as cc->
let cc = I.gexp_to_var cc in
i2 @ [CL.Instr.Op2_2.cmov x1 cc a2 a3]
| Papp1(Onot, (Pvar _ as cc)) ->
let cc = I.gexp_to_var cc in
i2 @ [CL.Instr.Op2_2.cmov x1 cc a3 a2]
| _ -> assert false
end

| ADD ws ->
begin
let l = ["smt", `Smt ; "default", `Default] in
Expand Down Expand Up @@ -843,7 +867,12 @@ module X86BaseOpU : BaseOp
let ty = CL.Sint (int_of_ws ws) in
i1 @ i2 @ [CL.Instr.Op2_2.mull l_tmp l_tmp1 a1 a2;
CL.Instr.cast ty l !l_tmp1]

| MUL ws ->
let a1, i1 = cast_atome ws (List.nth es 0) in
let a2, i2 = cast_atome ws (List.nth es 1) in
let l1 = I.glval_to_lval (List.nth xs 5) in
let l2 = I.glval_to_lval (List.nth xs 6) in
i1 @ i2 @ [CL.Instr.Op2_2.mull l1 l2 a1 a2;]
(* (\* *)
(* | IMULri ws -> *)
(* let a1, i1 = cast_atome ws (List.nth es 0) in *)
Expand Down