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

[JoaoDiogoDuarte]

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]

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]

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.