Prime-fields
A library about prime fields.
The prime-fields library contains executable formal specifications of
prime fields and related operations, along with a number of rules about
those operations. The elements of the field corresponding to the
prime p are the natural numbers less
than p.
To define the notion of primality, we currently use the
function primep defined
in community book projects/quadratic-reciprocity/euclid.
The following include-book command may be helpful to bring in the library:
(include-book "kestrel/prime-fields/prime-fields" :dir :system)
The key functions in the library are:
- (fep x p): The "Field-element predicate". Tests whether x is an element of the field for the prime p.
- (add x y p): Addition in the field: Computes the sum of x and y modulo the prime p.
- (sub x y p): Subtraction in the field: Computes the difference of x and y modulo the prime p.
- (neg x p): Negation (additive inverse) in the field: Computes the (unary) negation of x modulo the prime p.
- (mul x y p): Multiplication in the field: Computes the product of x and y modulo the prime p.
- (pow x n p): Exponentiation in the field: Computes x to the nth power (x^n) modulo the prime p. Note that n can be any natural.
- (inv x p): Multiplicative inverse in the field: Computes 1/x modulo the prime p. Requires x to be non-zero.
- (div x y p): Division in the field: Computes x/y modulo the prime p. Requires y to be non-zero.
- (minus1 p): Returns p-1. If p is large, this value will be large as well, but it can help to think of it as -1.
