Modified toCL to be able to run add4 ref example and added the add4 ref example

jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography

MIT License

271 stars 55 forks source link

Modified toCL to be able to run add4 ref example and added the add4 ref example #944

Open JoaoDiogoDuarte opened 1 month ago

JoaoDiogoDuarte commented 1 month ago

This merge request adds:

add4.jazz example with abstract predicates and asserts/assumes that will result in a valid and correct cryptoline file

And does the following to these abstracts predicates:

Uncomments pow abstract predicate for algebraic expressions
Adds algebraic abstract predicate b2i that converts a boolean to an integer
Add algebraic abstract predicate u64i that converts a u64 to an integer
Predicate that allows comparing two boolean variables (uses Obeq)

tfaoliveira commented 1 month ago

Hey! I have a question regarding the following types of statements:

\sum (ii \in 0:4) (pow(2, 64*ii)*u64i(result.0[ii]))

Why isn't it proposed an abstraction to reconstruct an array of limbs into an integer?

I was thinking something like limbs from Cryptoline (page 6 of the tutorial) for an example of what I'm referring to.

If there were an limbs version in Jasmin that would take arrays, the slice of the array to be considered, and the radix, I think it would improve readability.

JoaoDiogoDuarte commented 3 weeks ago

Since we support bits natively, we use the statement you mentioned so that we do not have to rely on Cryptoline's internal representation and of limbs.