Thanks! I meant “elaborate in the README” but this is an excellent first step. Two remarks:
-
The F*/HACL people have verified implementations of some of these crypto primitives ( https://github.com/project-everest/hacl-star ), and I think they can extract to either C or OCaml code. You may be able to depend on some of their libraries, or at least reuse some of their glue. (I’m not sure who to contact to get more information, I mostly learned about this work from the PhD defense of https://github.com/jkzinzindohoue ).
-
I think the Tezos project also had a tweetnacl binding (which you could reuse), but they switched to the HACL codebase now.