Field-arithmetic-operations
Leo field arithmetic operations.
These are negation (unary), doubling (unary), inverse (unary), square (unary),
addition, subtraction, multiplication, division, and exponentiation
(all binary).
These ACL2 functions are defined over values of the
value-field type
value-field type. These values contain natural numbers that
are not guaranteed to be below the prime returned by
(curve-base-prime curve).
It should be an invariant (to be formally proved eventually)
that, given a prime number used in Leo computation steps,
Leo computation states will have field element values below the prime.
The ACL2 functions defined below defensively check that this is the case,
returning an indication of error if not.
Subtopics
- Op-field-pow
- Leo field exponentiation operation.
- Op-field-sub
- Leo field subtraction operation.
- Op-field-mul
- Leo field multiplication operation.
- Op-field-div
- Leo field division operation.
- Op-field-add
- Leo field addition operation.
- Op-field-square-root
- Leo field square-root operation.
- Op-field-square
- Leo field squaring operation.
- Op-field-inv
- Leo field inverse (reciprocal) operation.
- Op-field-double
- Leo field double operation.
- Op-field-neg
- Leo field negation operation.
