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 add4 ref example and added the add4 ref example #944

Merged
Merged
Changes from 1 commit
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
Next Next commit
PR commit
  • Loading branch information
JoaoDiogoDuarte committed Oct 28, 2024
commit 8b38bc23c13bb93f20c6955bddac3e33976d7b16
72 changes: 72 additions & 0 deletions compiler/examples/jazzline/curve25519/common/add4/add4.jazz
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 11 additions & 1 deletion compiler/src/toCL.ml
Original file line number Diff line number Diff line change
@@ -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 =