# Prime-field-abbreviations

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 n-ary versions
of the addition and multiplication operations,
again for greater readability.

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.

### Subtopics

- Pfmulall
- Abbreviation for n-ary multiplication in the BabyJubjub prime field.
- Pfaddall
- Abbreviation for n-ary addition in the BabyJubjub prime field.
- Pfsub
- Abbreviation for subtraction in the BabyJubjub prime field.
- Pfneg
- Abbreviation for negation in the BabyJubjub prime field.
- Pfmul
- Abbreviation for binary multiplication in the BabyJubjub prime field.
- Pfminus1
- Abbreviation for -1 in the BabyJubjub prime field.
- Pfinv
- Abbreviation for inverse in the BabyJubjub prime field.
- Pfep
- Abbreviation to check if something is a BabyJubjub field element.
- Pfdiv
- Abbreviation for division in the BabyJubjub prime field.
- Pfadd
- Abbreviation for binary addition in the BabyJubjub prime field.