aboutsummaryrefslogtreecommitdiff
path: root/to_gallina.md
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-04-21 16:28:18 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-04-21 16:28:18 -0400
commite4f24c70af9044a9f2e8279d98ed9842eb858858 (patch)
tree0fb38704bcc0ec9425eae6af5ff2ed2c505858d9 /to_gallina.md
parent40c0d0557233d49ad9712d333ad4c6187b908a26 (diff)
wrote up remaining tasks needed for Gallina code (from board at 04/19 meeting)
Diffstat (limited to 'to_gallina.md')
-rw-r--r--to_gallina.md11
1 files changed, 11 insertions, 0 deletions
diff --git a/to_gallina.md b/to_gallina.md
new file mode 100644
index 000000000..bf5ab8270
--- /dev/null
+++ b/to_gallina.md
@@ -0,0 +1,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