|
|
|---|
|
|
|
|---|
Leo scalar field arithmetic operations.
Currently the only operations supported are addition between scalars and multiplication of a group value by a scalar. Multiplication of a group value by a scalar is defined in group-arithmetic-operations.
Since scalars are field elements of the scalar field,
it could make sense in the future to support operations on scalars
similar to those supported on base
These ACL2 functions are defined over scalar element values, which in general may not be below the prime. 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.