3 ms·
I've been iterating on sodium bindings in Lean4 for about four months, and now that I've gotten to Ristretto255 I can see why the author is excited about its po
by proof_by_vibes 9mo ago
I've been iterating on sodium bindings in Lean4 for about four months, and now that I've gotten to Ristretto255 I can see why the author is excited about its potential. Ristretto is a tightly designed API that allows me to build arbitrary polynomials on Curve25519 and I've been having a blast tinkering and experimenting with it! If the author by chance reads this, just want to say thank you for your work!
- fshacf 9mo agoYou have a public repo of this?
- proof_by_vibes 9mo agoYes: https://github.com/rj-calvin/sodium https://github.com/rj-calvin/sodium The bindings are set and have a monadic interface, but there's some abstractions that still need refining/iterating: mostly I want to be able to formalize keyboard input and eventually build a tactic framework for zero-knowledge proofs.