search

idris-hackers / idris-crypto

Implementation of cryptographic primitives using Idris
BSD 3-Clause "New" or "Revised" License
121 stars 13 forks source link

Switch to inductive binary? #9

Open clayrat opened 7 years ago

clayrat commented 7 years ago

There's a port of inductive binary number arithmetics in the works at https://github.com/sbp/idris-bi/, which I suspect will work much faster than Fin (though the analogue of Fin still has to be defined).

clayrat commented 7 years ago

I'm currently doing the integers mod 2^n @idris-bi to express proofs for functions on machine bytes, which seems to be sufficient to translate the current version of this library - it only uses Mod 256 in ARC4.idr. I wonder however, if it'd be useful to implement a general mod n arithmetic as well? My guess is yes, if we would also want something like RSA or Diffie-Hellman?