<style> .reveal h1 { color: #a23; font-family: serif; text-shadow:0 1px 0 rgb(137, 27, 41), 0 2px 0 rgb(144, 28, 43), 0 3px 0 rgb(126, 25, 38), 0 4px 0 rgb(132, 26, 40), 0 5px 0 rgb(114, 23, 34), 0 6px 1px rgba(0, 0, 0, 0.1), 0 0 5px rgba(0, 0, 0, 0.1), 0 1px 3px rgba(0, 0, 0, 0.3), 0 3px 5px rgba(0, 0, 0, 0.2), 0 5px 10px rgba(0, 0, 0, 0.25), 0 20px 20px rgba(0, 0, 0, 0.15) } .reveal h2 { color: #a23; font-family: serif; } .reveal h3 { color: #a23; font-family: serif; } .reveal h4 { font-family: serif; text-decoration: underline #a23; } .reveal strong { color: #a23; } </style> # Vamp-IR a universal intermediate representation for circuits --- **VAMP-IR** is a proof system agnostic language for arithmetic circuits. <br> Circuits written in **VAMP-IR** can be compiled to any proof system backend using any arithmetic constraint system or configuration, including those with custom gates or lookup tables --- ### Arithmetic Circuits Arithmetic circuits are a representation of systems of polynomial constraints.  $$b_0^2-b_0\quad\quad b_1^2-b_1\\ b_2^2-b_2\quad\quad b_3^2-b_3\\ 8b_3+4b_2+2b_1+b_0 -y =0$$ --- ### Constraint Systems A constraint system is another representation of a system of polynomials, but the participating polynomials must have a particular format. <br> | **R1CS** | **Plonkish** | | --- | --- | | one product of linear combinations of variables | fixed number of variables | --- ### Annoyances - Circuits written in different constraint systems can look very different - Constraints written in some constraint system may not resemble the source - Circuits have to be rewritten in order to use them in another proof system or configuration - Painful to benchmark a circuit in different proof systems or configurations ---- ### More annoyances - No canonical circuit format - Iterating on circuit designs is difficult - Front-end languages or DSLs become tied to a particular constraint system or proof system implementation ---- ### Circuits don't resemble each other, or the source <br> Twisted Edwards addition: $(x_1, y_1) + (x_2, y_2) = (x_3, y_3)$ if $x_3+Dx_1x_2x_3y_1y_2 - x_1y_2 - y_1x_2 = 0$ $y_3-Dx_1x_2y_1y_2y_3 - y_1y_2 + Ax_1x_2 = 0$ ---- | **R1CS**$^{\tiny{1}}$ | **3-wire Plonk** | | -- | -- | | $\scriptsize{x_1y_2 - o_1 = 0\\ x_2y_1 - o_2 = 0\\ Do_1o_2 - o_3 = 0\\ (x_1+y_1)(y_2-ax_2) - o_4 = 0\\ x_3(1+o_3)-o_1-o_2 = 0\\ y_3(1 -o_3)-o_4+o_1-Ao_2 = 0}$ | $\scriptsize{x_1y_2 - o_1 = 0 \\ x_2y_1 - o_2 = 0 \\ Do_1o_2 - o_3 = 0\\ y_1y_2 - o_4 =0\\ x_1x_2 - o_5 =0\\ x_3o_3 +x_3 - o_6 =0\\ o_6-o_1-o_2 = 0\\ y_3o_3 - y_3 + o_7 =0\\ o_7-o_4+Ao_5 = 0}$ | | **Original** | | -- | | $\scriptsize{x_3+Dx_1x_2x_3y_1y_2 - x_1y_2 - y_1x_2 = 0} \\ \scriptsize{y_3-Dx_1x_2y_1y_2y_3 - y_1y_2 + Ax_1x_2 = 0}$ | --- ### The cure We need a circuit language that allows for arbitrary polynomial constraints. Then arithmetic circuits can be written in a canonical, universal way. --- ### What about lookup tables and custom gates? Arbitrary polynomial constraints aren't enough: we need to include some extra information that allows a proof system implementation to replace subcircuits with lookup gates or custom gates. --- <br> <br> | **V**🧛 | | -- | | **A**liased | | **M**ultivariable | | **P**olynomial | | **I**ntermediate | | **R**epresentation | --- ## Design Principles - A representation of a circuit should express the *intention* of the circuit - A representation of a circuit should be flexible enough to allow for custom gates or lookup tables --- ## How does Vamp-IR work? <br> Vamp-IR accepts multivariable polynomial constraints of any format. <br> ```java 0 = x3 + D*x1*x2*x3*y1*y2 - x1*y2 - y1*x2 0 = y3 - D*x1*x2*y1*y2*y3 - y1*y2 + A*x1*x2 ``` ---- ### How does Vamp-IR work? The VampIR language allows collections of polynomial constraints (or *subcircuits*) to be given a reusable name, called an **alias**. ```javascript def check_on_sw_curve x y { 0 = x^3 + A*x + B - y^2 } def range_4 x { 0 = b0*b0 - b0 0 = b1*b1 - b1 0 = b2*b2 - b2 0 = b3*b3 - b3 0 = 8*b3 + 4*b2 + 2*b1 + b0 - x } ``` ---- ### How does Vamp-IR work? Aliases have a signature---like a function signature---that indicates which variables can be regarded as "inputs" or as "outputs". <br> ```java def twisted_edwards_add x1 y1 x2 y2 -> x3 y3 { 0 = x3 + D*x1*x2*x3*y1*y2 - x1*y2 - y1*x2 0 = y3 - D*x1*x2*y1*y2*y3 - y1*y2 + A*x1*x2 } ``` <br> The signature `x1 y1 x2 y2 -> x3 y3` indicates that `x3` and `y3` can be treated as outputs of the circuit. ---- ### How does Vamp-IR work? <br> Aliases can be composed <br> ```java def twisted_edwards_add x1 y1 x2 y2 -> x3 y3 { 0 = x3 + D*x1*x2*x3*y1*y2 - x1*y2 - y1*x2 0 = y3 - D*x1*x2*y1*y2*y3 - y1*y2 + A*x1*x2 } twisted_edwards_add (twisted_edwards_add x1 y1 x2 y2) x3 y3 ``` ---- ### How does Vamp-IR work? Standard aliases can indicate opportunities for lookup gates: ```javascript def range_4bit a { bool b0 bool b1 bool b2 bool b3 0 = a - 8*b3 - 4*b2 - 2*b1 - b0 } ``` A compiler targeting a proof system that has lookups is free to replace `range_4bit` with an appropriate lookup table. --- DSLs or front-end languages have a consistent target to compile to  --- A complicated circuit can become fairly readable... ```javascript def sapling_output cv cm epk gu gv pk v rcv rcm esk { cm = extract (note_commit (repr gu gv) pk v) cv = value_commit v not_small_order gu gv epk = jubjub_mul esk gu gv } ``` ... and checkable against the spec$^{\tiny{1}}$  Or, circuits written in **VAMP-IR** can serve as a spec themselves --- ## Citations 1. Zcash Protocol Specification, https://raw.githubusercontent.com/zcash/zips/main/protocol/protocol.pdf