Snarky: Algebraic effects in the Coda cryptocurrency
summary
Snarky is an OCaml embedded DSL that compiles high‑level, Hindley‑Milner style code with algebraic effects into rank‑1 constraint systems so zk‑SNARKs can prove “I know data such that the property holds.” It implements requests/handlers and assertions, encodes booleans as field elements, and supports recursion/recursive composition for unbounded chains. O(1) Labs uses it in Coda to compress the entire transaction history into a few‑hundred‑byte proof, verifiable in milliseconds, and the system is in active use.
AI-written summary · about
chapters (6)
- 0:00Start
- 1:35Verifiable Computation
- 3:14Argument of Knowledge
- 26:25Arithmetic Constraints
- 37:23Recursive Composition
- 41:19Takeaways
related talks
25mThe Next 700 ZKP Programming Languages
28mNotes from the SNARKonomicon: Techniques for Writing SNARK Programs
18mSoK: Understanding zk-SNARKs: The Gap Between Research and Practice
48mzkSNARKs — Cryptographic Proofs for Scaling and Security Challenges
39mPrivacy and Evolution of SNARKs
26mLeveraging Duality for Programming with zkSNARKs
36mPanel Discussion
23mSonic: Nearly Trustless SNARK Setups