Leveraging Duality for Programming with zkSNARKs
summary
Language adds a single combined block that is annotated at variable declarations with C/P/CP labels, then a compiler projects that block into two low-level programs: a witness-computation pass followed by a proof-generation pass suitable for existing zkSNARK libraries. A modal type system rejects programs where red and blue data illegally depend on each other (example: moving X across projections), and the prototype handles Merkle-path style examples; ongoing metatheory aims to prove adequacy of the surface semantics and RHP (robust relational hyperproperty preservation).
AI-written summary · about
chapters (9)
- 0:00zkSNARKs introduction
- 3:11How zkSNARKs work
- 8:09Duplicated code problem
- 10:16Combined code blocks
- 12:45Type system for safety
- 13:49Semantics of combined blocks
- 16:15Robust compilation proof
- 18:42Summary and future work
- 19:59Question and answer session
related talks
18mSoK: Understanding zk-SNARKs: The Gap Between Research and Practice
56mCollaborative zk-SNARKs: Proving as One over Distributed Secrets
36mPanel Discussion
18mA Selection of Pairing Based zk-SNARKs
39mPrivacy and Evolution of SNARKs
01h 00mThe Path to Shielded Programmability
19mDIZK: A Distributed Zero Knowledge Proof System
54mSnarky: Algebraic effects in the Coda cryptocurrency