We try to use the ideas from the paper "Closure-Free Functional Programming in a Two-Level Type Theory" by András Kovács to build a libary of algebra operations useful in the context cryptography (in particular zero knowledge proofs).
Note: This is very much a work-in-progress experimental prototype, intended primarily as a proof-of-concept and a learning device.
- fixed-size big integers (eg. 256-bit ones)
- bit operations
- comparison
- addition, subtraction
- multiplication, squaring, scaling
- division
- large finite fields
- addition, subtraction, negation
- Barrett reduction, multiplication
- Montgomery multiplication, squaring
- conversion to/from Montgomery representation
- exponentiation
- inversion, division
- batch inversion
- field extensions
- elliptic curves
- polynomials
- number theoretical transform
- the user application is written in Agda (as a metaprogram)
- building on the top of the "frontend", which is also written in Agda
- the backend is written in Haskell
- You write your application as a metaprogram in Agda, using HOAS representation and whatever convenience the library can offer
- This gets translated into a very standard well-typed first-order representation of simply typed lambda calculus
- In theory you could have a well-typed interpreter at this level, but I haven't implement the primops yet
- The first order representation gets downgraded to an untyped "raw" representation
- That raw AST is then exported as a text file (using a hand-written
Showinstance) - The resulting text file can be read by Haskell with the standard derived
Readinstance - This can be interpreted at this point too
- Lambda lifting transformation is applied
- ANF conversion is applied
- Code generation (as C source code)
- Finally the resulting C code is compiled by a standard C compiler
TODO: make a script automating this