|
|
|---|
|
|
|
|---|
Abbreviations for the prime field functions for Semaphore.
The Semaphore is defined on BabyJubjub, which means that the prime field of interest (e.g. in the R1CS) is the one defined by baby-jubjub-prime.
The functions in the prime fields library are parameterized over the prime that defines the prime field.
Here we define macros that abbreviate
calls of the prime field library functions with the BabyJubjub prime,
where the prime is generated by the macro.
So the macro only takes the other arguments,
resulting in more readable terms.
We also introduce macros for
The increased readability applies to the ACL2 files where they are used. Proof output will show the expanded calls with the prime. We may consider defining optional output modifications (using ACL2's facilities for that) that print the calls as calls of these macro abbreviations.