|
|
|---|
|
|
|
|---|
Curve parameterization in Leo.
The (static and dynamic) semantics of Leo is parameterized over a choice of (i) a prime field, (ii) an elliptic curve over the field, and (iii) a generator point on the curve. Collectively, these are sometimes referred to just as `curve', because the curve is the primary component in some sense, with the prime field being considered in a way part of the curve, and with the generator point being closely related to the curve. The prime field is the `base field'. The generator point must have prime order, and its order defines another prime field, namely the `scalar field'. The curve is chosen in the Leo configuration file, which will be supported in future versions of Leo. All of this is explained in the Leo Reference.
In our ACL2 formalization, we capture the possible curve choices via a fixtype. Since currently Leo supports just one curve, for now the fixtype is a singleton. However, this will be extended as more curves are added.
We define functions that take the aforementioned fixtype as parameter and that define semantic aspects of Leo that depend on the curve. An example is the base field prime. These functions are used to define the semantics of Leo.