|
|
|---|
|
|
|
|---|
Fixtype of Leo values.
This is a tagged union type, introduced by fty::deftagsum.
There are boolean values, unsigned and signed integer values of five sizes, base field element values, group element values, scalar field element values, address values, string values, tuple values, and struct values.
Since the primes that define the base and prime fields may vary (see curve-parameterization), here we allow a field or scalar element to consist of any natural number. That the natural number is below the respective prime is enforced elsewhere.
Analogously, since the elliptic curve that defines the group may vary, here we allow a group element to consist of any possible point of any possible elliptic curve. We use the type of elliptic curve points from the elliptic curve library, which includes representations for both finite points and the point of infinity.
We do not require tuple values to have zero or two or more components (i.e. not to have one component). We can formulate and prove that invariant separately. Keeping the fixtype of values more general also facilitates a possible future extension of Leo in which tuple values with one components are actually allowed.
Struct values are modeled as finite maps from identifiers (i.e. the names of the components) to values (i.e. the values of the components). We also include the name of the struct type.