fiat_25519_tight_field_element
typedef uint64_t fiat_25519_tight_field_element[5];
typedef uint32_t fiat_25519_tight_field_element[10];