aboutsummaryrefslogtreecommitdiff
path: root/to_gallina.md
blob: bf5ab8270da70f27067cca405a48bee63b5b0270 (plain)
1
2
3
4
5
6
7
8
9
10
11
Remaining work needed for Gallina verification code
---------------------------------------------------
+ GF subtraction
+ efficient GF exponentiation
+ efficient GF inverse
+ make EdDSA point addition use ModularBaseSystem
+ represent scalars (Fl) in ModularBaseSystem (large c)
+ elliptic curve decidable equality
+ associativity nonseroes
+ negation of elliptic curve points
+ canonical representations of field elements