From e4f24c70af9044a9f2e8279d98ed9842eb858858 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 21 Apr 2016 16:28:18 -0400 Subject: wrote up remaining tasks needed for Gallina code (from board at 04/19 meeting) --- to_gallina.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 to_gallina.md (limited to 'to_gallina.md') 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 -- cgit v1.2.3