ZKP MOOC Lecture 3: Programming Zero-Knowledge Proofs (R1CS, circom, Arkworks, ZoKrates)

[00:00:01]hello hi everyone I'm pratyush and together with Alex ostomier I'm going to be lecturing on programming zero knowledge proof systems all right let's get started so let's say you have an idea for an application it could be a private payment system could be a private voting application you know anything where you think a zero knowledge proof system might be useful so how do you actually get started expressing this idea and sort of implementing it so if you're a programmer the first thing that comes to mind would be to try to implement your pro your idea as a program in some high-level programming language like say a c or a python or a Java or something similar right unfortunately zero knowledge proves they don't understand these high-level programming languages and instead understand things like constraint systems or arithmetic circuits right so say we have somehow expressed our idea in this arithmetic circuit or constraint system form um then we can sort of feed this uh circuit into say the zero knowledge proof system setup algorithm which will produce some public parameters for us which we can then go ahead um and use for proving and then later verification okay but how do we actually go from our idea into this format that the zero knowledge proof system understands well this is going to be the focus of this lecture exactly how to take your idea and make it in a into a format which the zero knowledge group system um can understand and then prove okay so in this lecture we'll start by first doing a high level overview of what it means to program a zero knowledge proof and then dive into three different ways that you know prominent Frameworks uh try to do this the first approach will be to use a hardware description language such as circom and it will describe you know what the core operations and objects of this Hardware description language are and then we'll also do a short tutorial where we go over how you can Implement a simple example of Sudoku inside this Hardware description language the next approach that we'll take or that will show is how to use a library that's implemented inside an existing high-level language in our case it will be the arc Works Library which is implemented in Rusk so we'll um describe some common operations and objects that are sort of common to everything in this class of Library based approaches and then we'll also do a short tutorial which uses the aquax library to illustrate what this looks like in practice the Final Approach that we'll cover is actually a new language or the approach of describing a new language and implementing a compiler for it which is intended to be oriented towards your knowledge proving so the language has constructs within it that correspond to operations that you would want to perform in your zero knowledge proof system so we'll cover at a high level what this languages look like and then also do a tutorial in one popular language called Socrates finally we'll conclude by doing an overview of various prominent ckp tool chains which fall into one of these three categories and we'll try to do sort of a compare and contrast of these as well as an idea on how to unify all of these approaches as we move forward okay so before we start maybe let's quickly recall what the Zoological system does a Zoological system it's a way for approver to convince or verifier that some statement or predicate is true without repealing information about why it's true in more detail approver knows some predicate or claim five a public input X and a private input W such that Phi on X comma W is satisfied the verifier in Turn Only Knows the predicate and X the zero knowledge proof allows the prover to show that the predicate is satisfied namely that Phi on X comma W outputs one in a way that completely hides the private input w okay um so this is you know nice in theory but if you want to implement something we have to know what Phi can actually Express right what kind of computations can be captured uh by this predicate file the nice thing is that in theory for many popular zero knowledge proof systems Phi can be any NP statement right so for example you could use Phi to uh prove the knowledge of the factorization of an integer so your W your private input would be the factorization and the public input would be the integer itself and Phi would just multiply the factorization and check that it equals the public input you could use Phi to show knowledge of a private key for some public key which is a public input you could use it to show you know the password for an account and you could show that um you have a valid transaction you can do basically you know whatever you might imagine you can use Phi to capture that but all of this is in theory what does PHI actually look like when you sort of try to implement it um so in practice five in a format that the zero knowledge proof system understands is going to be an arithmetic circuit over the public input X and the private input w okay so let's dive a little bit deeper into what an arithmetic circuit is okay so an arithmetics okay you can think of it as similar to a Boolean socket you might be familiar with it from um say your undergraduate classes uh but you replace the Boolean Gates such as and ores with arithmetic Gates such as additions and multiplications furthermore all this arithmetic is performed over um what's called a prime field you can think of this as the integers modulo some large Prime P so your additional multiplication they all happen modulo p so one example would be you said P equals five then addition mod 5 looks like if you want to add four and five you'll get nine and then mod 5 that is four similarly if you want to multiply four by four mod P you'll get 16 mod 5 which is just one okay so basically it's like a Boolean circuit but all the operations uh instead of being ands and ORS and so on they instead become additional multiplication model of this Prime p all right okay so that sort of uh is the background upon which these arithmetic circuits are defined but how do you actually express any computation in teams see one way one way to view these arithmetic circuits is at a system of equations over these Prime over the prime field so for example once a system would be I multiply the first private input by itself three times and I want to check that equals the public input X and then I do almost the same thing with the second private input I must multiply it by itself so I'm squaring the first one uh the W1 and again I want to check that it equals the public input all right you can basically express any polynomial um uh over the field as an arithmetic circuit right and you can you know I just talked about multiplications but you can also throw it in an addition there all right so that's uh one way to view arithmetic circuits right but it's kind of uh difficult to visualize what the circuit is Computing in this way another way to view arithmetic circuits is as a directed acyclic graph or dag right here the nodes of this dag would be things like the inputs to the Circuit the gates such as addition multiplication equality testing and some constants which are sort of input into these Gates as well right so that would be the nodes the edges of this graph are going to be wires which sort of carry values from one node to the next so a wire from a multiplication gate into an addition gate will sort of carry the output of the multiplication gate as an input into the addition gate let's see what this actually looks like by taking our example from the previous slide right so we want to express these two field equations as a dag for the first one or rather for the second one what we're going to do is we're going to multiply W1 by itself so we're going to feed W1 into the multiplication gate twice and then we're going to take the output of that multiplication gate and feed it as an input into the equality gate and similar similarly we'll feed X the public input as an input to the equality gate also and here all of these arrows they correspond to um the wires of the tag right so this um is a sub-circuit which corresponds to the second equation and the first equation we can express in a similar way as you can see we are taking w0 feeding it into the multiplication gate taking the output of that multiplication gate and feeding it as input into another multiplication gate and w0 is again fed as the other input into that multiplication gate so the output of the second multiplication gate is going to be w0 times W 0 times w0 so w 0 cubed and finally we'll check that this w0 cubed is equal again to the public input by drawing a wire um from X to the Quality gain all right so this is uh one way to sort of visualize these arithmetic circuits okay so this is one format which a zero knowledge group systems understand on the next slide Alex will cover another format which is very popular for modern zero knowledge proofing systems and that is called r1cs or rank one constraint system okay now it's time for us to get into the details of one particular predicate representation used by a zero knowledge proof we're going to be talking about the predicate representation called a rank one constraint system or r1cs r1cs is not the only predicate format that's used with zkps but it is the most common one and historically it's been the most important the definition of r1cs is very simple x is represented as L field elements X1 through XL W is represented as M minus L minus one field elements W1 through w m minus L minus 1.

[00:12:05]and the predicate itself is just a set of n constraints or n equations where every equation has to form Alpha times beta equals gamma where Alpha and beta and gamma are all affine combinations of linear variable variables um so you can think of this as a linear combination of variables optionally with a constant added so let's look at a few examples of constraints that do and do not have this form our first example is W2 times W3 minus W2 minus 1 is equal to X1 this is a constraint that does have this form Alpha is just W2 beta is W3 minus W2 minus 1 and Gamma is X1 so the most interesting of the outline combinations here is beta It's a combination of W3 W2 and a constant the coefficient for W3 is 1 the coefficient for W2 is -1 and the uh the constant is minus one this is an acceptable constraint another acceptable constraint is W2 times W2 equals W2 one constraint that's unacceptable is W2 times W2 equals X1 so this is unacceptable essentially because on the left hand side you have three different variables all being multiplied together so you have two products of variables and that means that however you view Alpha and beta one of alpha or beta is going to have a product of variables inside it and that's that's not okay because Alpha and beta each have to be affine combinations however if we wanted to take this constraint we actually can encode it using multiple rank one constraints by introducing fresh intermediate variables so we could say that W2 times W2 needs to be W4 where W4 is a new variable that we haven't used already and then we would say that W4 times W2 is equal to X1 so together these constraints and imply the constraint that we saw before indeed if you if you eliminate W4 if you substitute W 2 times W2 in for W4 and the second constraint you get you get the original one but what we've done here is we've just split that constraint into two in order to reduce the number of non-linear products per constraint so this is how you can see rank one constraint systems in terms of n constraints but there's also another way of seeing them an equivalent way of seeing them that is sometimes useful and this is the matrix definition of r1cs the definition starts very similarly you view X and and W as vectors of field elements but you define the predicate in a slightly different way you say that the predicate is now defined by three matrices a b and c so such that the predicate holds when if Z is defined to be one concatenated with X concatenate with w a z element wise product with bz is equal to CZ so a z b z and CZ those are three different Matrix products and we're saying that the element wise product are the first two Matrix products should be equal to the Third if you draw this definition pictorially you get something like this I've got my Matrix products a z times bz and is equal to CZ and the interesting thing about drawing it pictorially is that the correspondence between this definition and the rank one constraints becomes very clear when you because you see when you take a matrix product a times Z you take Z and you compute its inner product with every row of a and so what that means is that every row of a is essentially defining a linear combination or or more precisely an affine combination of the variables in X and w and so every so if you look at a row in a a row and B and a row and C then those three rows they Define a single rank one constraint so the height of the Matrix the matrices here the height of a b and and C is exactly n the number of rank one constraints and the width m is one more than the total number of variables and it's one more because the the Z Vector includes this constant one so if this this matrix definition is a bit hard for you to understand that's all right you can pause the video take a look at it but ultimately when people program zero knowledge proofs they they usually don't think about the constraint system that they're building in terms of matrices usually they just think about it in terms of rank one constraints in terms of linear combinations and so we're going to get a little bit of practice working with those linear combinations right now and the way that we're going to get that practice is we're going to take this pictorial arithmetic circuit that I've drawn on the left and we're going to turn it into a rank one constraint system we're going to use a very simple non-optimal algorithm for doing this and this algorithm just has two steps the first step is to introduce a new witness variable for every intermediate wire so that means since there are three intermediate variables we're going to need three new Witnesses W2 W3 and W4 now in the second step we write down a single rank one constraint for every gate so each gate will have its own constraint we'll end up with four constraints our first constraint is going to be for the upper multiplication and that constraint is just w0 times W1 equals W2 so in general any multiplication you can write down a constraint of this form the first input times the second input equals the third input and that that constraint is rank one because it's only a single multiplication now let's do the addition for the addition we're going to write this down as W3 equals W2 the first input plus x0 second input so here this is a rank one constraint because W3 is our Alpha combination W2 plus x0 is our gamma combination and our beta combination is just one so we've actually omitted it we've left it implicit the next multiplication we handle like the first W1 times x0 is equal to W4 and then our final gate is this equality constraint this equals and we can we can just write that down W3 equals W4 and once again this is a rank one constraint because the beta linear combination is one just like it was for our addition gate uh okay so this is a nice example the algorithm that we've shown by example here generalizes immediately to any arithmetic circuit and it produces one constraint per gate so if we zoom out at this point you've learned about r1cs rank one constraint systems a way of writing down a predicate so that you can write a zero knowledge proof about that product and so when we think about the problem that we have our problem is going from high level ideas about the predicates that we want to be able to write zero knowledge proofs for things like I know the secret key for a public key things like I know of a coin that's never been spent before and you need to be able to take that high level idea and then turn it into a rank one constraint system so this is this is pretty hard in some sense this is like trying to take the idea of a photo sharing application and come up with assembly code that implements that application on your computer the rank one constraint system it's kind of like assembly and viewing the rank one constraint system like assembly is useful because it turns out that the same kinds of tools that we use to turn high level programs into assembly are going to be useful for turning high level descriptions of predicates into rank 1 constraints that is we're going to be using libraries we're going to be using compilers we're going to be using programming languages we're going to be using domain specific languages and in uh very briefly in in the rest of today's talk we're going to or the rest of today's lecture we're going to be going over different libraries compilers programming languages for this task but to drive home this point even more the idea is that we're going to start with some high level code that high level code is going to include structures such as booleans user-defined structures modules functions we're going to feed this high level code into some kind of compiler or library that library is going to spit out rank 1 constraints and then we can feed those rank 1 constraints into our zero knowledge proof system so we can we can produce a set of algorithm approve algorithm in a verify algorithm lots of basically every real deployment of zero knowledge proofs is built in exactly this manner so to give you an example the Z crash cryptocurrency is built like this the high level um the core of the z-crash cryptocurrency is this predicate that describes what it means to spend money anonymously and the description of of that predicate is a circuit that involves ideas such as Merkle trees Patterson hashing signatures and logic that describes when and it is and is not okay to actually spend money and so the zcash circuit is written down using a library called Bellman and what Bellman produces on its output side is a set of rank 1 constraints and then those rank 1 constraints in the case of the sapling distribution of zcash are fed into a zero knowledge proof system designed by John grot in 2016. this the system is called grot16.

[00:21:20]and then graph 16 runs on the computer of everybody who uses zcash okay so uh that's that's one example of this pipeline in action and today we're not just going to illustrate this pipeline or the library we're also going to illustrate it using other kinds of tools as well so we're also going to look at a hardware description language as well as a programming language and its compiler and we're actually going to start with the hardware description language now it's time for our first tutorial I'll be telling you about how to use circom which is an HDL or a hardware description language for r1cs the tutorial is going to have two of Hearts we're going to start with slides we're going to see the basic syntax and ideas of circom and then we're going to hop into a text editor and write some sir com code together so let's start with the idea of Sir pump the first thing to understand about sarcom is that it is an HDL or a hardware description language which is very different from APL or a programming language you're probably used to using programming languages you know that in a programming language you have objects such as variables you can perform operations on them and you can Define functions and programs the kinds of actions that you can take with these objects are the actions you're used to you can mutate variables you can evaluate operations and you can call functions or run programs but in HDL the objects and the actions are very different hdls are all about describing circuits so the basic objects are wires Gates and circuits or sub-circuits and then the kinds of actions that you can do you can't mutate things you can't haul functions all you can do is connect wires and you can create sub-circuits and then perhaps connect your wires to the wires of the sub-circuits hdls are are so different from PLS because they were originally designed for a very different purpose hdls are actually used to design digital circuits so for example the processor in your computer was designed using an HDL in fact it was probably designed using verilog or system verilog which are the the dominant hdls but it might have also or components within it may have been designed using something like vhdl or chisel which are which are other hdls um generally speaking vhcl differs from system verilog differs from verilog and that system verilog and includes more features as well as sort of tools for helping you verify that the circuit is correct vhdl is more verbose and explicit than verilogue and chisels higher level than prologue but but surcom it's not an HDL for digital circuits it's an HDL for r1cs and so that means that the wires of circums the signals those are r1cs variables and the gates that you create are rank 1 constraints the final thing that I'll say about circon before we dive into it is that ultimately every circum circuit has two things that it needs to do for all of its signals first of all it needs to set a value for them so it needs to set a variable a value for every variable and then second of all it needs to um and used to create rank one constraints so let's look at a Smalls for common example in this example we're just going to be multiplying two field elements the way that you create a template the way that you create a circuit in circum is using the temple keyword so here we hit say template multiply and then we have the body of the template multiply here is the name um inside our template we start by declaring the inputs and outputs to our template so a signal insert com is a wire or an r1cs variable and we have two input signals X and Y and then one output signal Z in circon the way that you set the value of a new variable or sorry a new signal is using the left Arrow operator so the output signal Z that's created by this template so we need to set a variable for it we need to set a value for it and we do that by saying that Z left Arrow X times y um or Z gets x times y so while this sets the value of Z and the value that an honest prover will assign it doesn't create any rank 1 constraints you create a rank one constraints separately um so we're going to do that by saying that Z triple equals x times y and triple equals is the operator for creating rank one constraints so there are some some constraints associated with how you use it whenever you use triple equals one side has to be a linear function of signals and the other side has to be a quadratic function or a rank one construct or a quadratic expression so the product of two linear combinations so one example of using triple equals in an invalid way is this saying that Z triple equals x times x times y on the right hand side here we have a product of three variables so this is not a rank one constraint if you're interested in set so in the above example we both set Z to be equal to x times Y and we also constrained Z to be equal to x times Y and Zircon actually has a special operator that allows you to do both of those and the operator for this is a left Arrow where there are two lines instead of one so instead of doing left angle dash dash you do left angle equals equals so this looks visually like the combination of the signal assignment operation and the constraint creation operation and it is actually just both those things so this is a shorthand for Z gets x times Y and Z is constrained to be equal to x times y okay so great we've just created our first circum template however circom ultimately doesn't synthesize templates it synthesizes main templates so we have to tell sarcom that this is our main template and we do that by declaring the main component and setting it to be equal to multiply and whenever um you create a main component in surcom you have to tell cercom which signals are public and which are private these correspond to the public data and the private data in their zero knowledge proof the output is always if there is an output is always public but the input is is private unless you say otherwise and so here we use circon's syntax to state that X should be public uh so with with this main component uh circom is going to have the verifier know X and then the verifiable so no Z this is a very simple that was a very simple example now it's time for a more complex one we're going to look at so a few a few a slightly more complex template that's going to show off some of Sir Khan's meta programming features this template is going to check repeated squaring so we're going to check that if you start with X you square it n times then you get y a and so the first thing that we see in this example is a template argument n it's an argument to the template itself the thing to remember about template arguments is that template arguments are fixed at compile time so whenever we run the compiler we're going to specify a value of n saying that we want to generate a circuit that checks for example a thousand squarings you can do a lot of things with these template arguments because they're known at compile time one of the things that you can do is you can declare an array of signals whose length depends on the template argument so here we've created n plus one values in an array of size array called X's of size n plus one and we've set the first element to this array to be equal to X so this is one thing you can do you can you can create these arrays and then you can access these arrays at constants another thing that you can do with template arguments is you can create for Loops whose bounds depend on template arguments so here we're creating a for Loop the iteration variable is I it starts at zero and it goes up to n the template argument and it does that in steps of one so this is an example of a loop in circum the loop creates uh can declare an iteration variable I that iteration variable is going to be incremented at compile time so when circuit when circom processes this template when it gets to this loop it's actually going to process the body and different times and it's important that of course the bounds of the loop are things like template arguments or functions that depend on them because those bounds are also evaluated at compile time so since our interest is in doing repeated squaring in every iteration of this loop we're going to do one squaring so what we're going to do is we're going to access the next element of the array and we're going to say that it needs to be equal to the square of the previous element um so yeah that's what that line of code does and then after the loop we need to set the output to be equal to the final element of the array because the final the element of the array now contains the result of doing n squarings so we do that by saying that y gets and should be assigned should be constrained to be equal to X's of n and then of course we declare our main component and now since our our main component is going to be the result of a template that takes a template argument we need to actually provide that argument so here our main component is going to check a thousand squarings okay um so this is a slightly more complex example and it shows off how you can use variables how you can use template arguments and how you can use Loops in circom now I want to tell you about two additional features I want to illustrate how witness computation or how signal assignment is more General than r1cs and then also I want to show off sub-circuits the example that we're going to use to get us started is the idea of creating a template that ensures its input is non-zero so the input here is called in and we want to guarantee that n is not equal to zero we can't of course do this directly because rank 1 constraints assert equalities not inequalities but one way to check that a value is non-zero or to require a value to be non-zero is to require that it has a multiplicative inverse so to require that it actually has a reciprocal and we can actually do that in circle column so we can say okay we want a signal called inverse and we want inverse to be equal to one divided by n and when you look at that expression 1 divided by n one of the things that you should notice is that that is not a rank one constraint right division has no place in rank one constraints but the left Arrow insert column the gets operation is more General than rank one constraints in fact you can put pretty much any expression on the right hand side of a gets operation because the gets operation is just setting the value of inverse it's not trying to create rank one constraints and then in our non-zero circuit on the next line we can create the rank one constraint that corresponds to the sketch operation so that constraint is saying that one needs to be the product of N and signal so this rank one constraint of course is only satisfiable if n is non-zero because if n is zero then the right-hand side of the constraint is always going to be zero and the constraint is always going to be falsified so this this template really does ensure that the input is non-zero and in order to write this template we had to compute inverse separately from creating um constraints over it okay so that's an example of how we can do witness computation now I want to show how you can include one template inside of another and so we're going to do that by creating a tiny toy template that uses non-zero so our toy template we're going to call it Main and it has two inputs A and B it creates a sub-circuit using the component keyword so we create a new component called NZ which is going to be equal to the result of synthesizing the non-zero template and then on the next line what we want to do is we want to connect our our input a to the input of our sub-circuit and so we can refer to the signals of sub-circuits using dot notation so NZ dot in refers to the uh the in Signal inside the non-zero component or the non-zero template okay great so we just set a or we set the non-zero input to be a and then we also assert that a is equal a times B is equal to zero So In Sum since a is non-zero and a times B is equal to zero this is just a roundabout way of saying b equals zero so of course if you actually wanted to to require B to be zero you would you would just say that but doing it in this roundabout way allows us to show how you use sub-circuits okay great so this has been our um our introduction to circom in terms of slides so this is a very fast introduction to the syntax of sarcom what we're going to do now is we're going to hop into a text editor and we're going to write some circle code together the goal of the the small example that we're going to program together is going to be to create a sudoku-like game so if you're not familiar with Sudoku Sudoku is a puzzle where there's a 9x9 grid some cells initially have numbers on the left hand side I have the puzzles you can see that some of the cells have numbers in them some of them don't all the numbers if they're there are between 1 and 9 and your goal is to fill in all of the blanks with the numbers one through nine so that no row has any duplicates no column has any duplicates and no three by three grid has any duplicates so if you think about it like the solution to the puzzle is just a nine by nine grid of numbers that satisfies a few constraints there are no duplicates in any row there are no duplicates in any column there are no duplicates in any three by three grid and the numbers in your solution need to agree with the numbers in the original puzzle if the number if there was a number in the particular cell that of the original puzzle um okay so in the language of a zero knowledge proof the puzzle here is the public information it's the X the solution is the witness uh the predicate is all these constraints and in our uh in our tutorial we're actually not going to code up all of Sudoku we're only going to enforce that every row has no duplicates ensuring that no column has any duplicates and that no 3x3 grid has any duplicates it's very similar but to keep the tutorial short we're just going to do rows for now okay great now uh we'll cut into the text editor okay welcome back so now we're going to hop into a text editor and work through writing a small circle program together I'm doing this from the starter code in the zero knowledge mooc examples repository that you should have access to so in my starting point I've got this file sudoku.circom that we're going to be editing you can of course do this with whatever text editor you like okay so here's the file and so what we're going to do in this file is we're going to create a sequence of templates ultimately building a template that checks a solution to Sudoku or at least that checks that you respect the row constraints of Sudoku and you know we're going to do this piece by piece so the first template that we're going to create is called non-equal and so what this template should do is ensure that n0 and N1 are not equal to one another and the way that we're going to do that is we're going to check that in 0 minus in one is non-zero and we actually saw earlier the tool for checking that something is non-zero which is that we need to verify that an inverse exists so we're going to declare a new signal we're going to call this signal inverse and we're going to set inverse to be equal to 1 divided by n0 minus N1 but of course we also have to ensure that that constraint is respected and so we can do that by enforcing that inverse times n0 minus N1 is equal to 1.

[00:37:35]great okay so that's our first template now on to our next template this template is called distinct it takes an argument n and its inputs are well its input is an array of n different signals and what it is sure it ensures is that uh each pair of signals in this array are not equal to one another which ensures that every single element is unique so all elements are unique in the array and we're going to do that by creating a bunch of components okay so um and what we're basically we're going to do is just for every we're going to do this very naively for every single pair for every pair of of inputs we're going to create a component um that ensures that that those two pairs or that pair those two elements are not equal to one another and so we're going to do that using a for Loop so we're going to say okay first of all let's have I which is going to go up to n and then inside this we're going to do another for Loop um in J and what J is going to do is it's just going to go up to I great and so um so for every pair so I J is now a pair of indices into this array and for every pair we want to create a non-zero sub-circuit and we want to wire it up to this pair of inputs so we create the component by setting non-equal i j to be equal to a non-equal template instantiation and then we have to to wire we have to connect our inputs to the inputs to this to this non-equal component and so we'll set in 0 to be our input at location I and we'll set N1 to be our input at location J and notice that I actually just made an error so so here I'm creating a component and I can actually use the equal sign for that that's the right Syntax for for creating a component but here I'm trying to connect two wires and you'll remember that the way that we connect wires both doing assignment and constraining is we'd use this um this left arrow with equal signs so that this is the gets and assign and constraints operator great okay so now we have um something that we can use to to check that and different values are distinct this will be important for checking that our rows are distinct um but what about um what other constraints do we have well in Sudoku we know that all the numbers have to be in the range one to nine and that actually turns out that checking that a value is in a range and surcom is quite painful it's quite challenging um and so I've actually done it in advance we're not going to walk through it together right now I will say a bit about the structure that we use to do it which is that we start by creating this template called bits four that essentially just checks that n fits in four bits more precisely it ensures that n is in the range 0 through 15. and it turns out this is not so hard to do because that is that range has width which is a power of two um and so what you can do is you can just provide the bit decomposition that's this this array of signals here and then you can check that that every every element is zero and and you can build this bit sum that essentially ensures that those bits when you sum them up with powers of two give you the input so and then ultimately this ensures that that n is in this range 0 to 15. and then to ensure that n is in a Range one to nine inclusive on both sides it suffices to check that n minus one is in the range of 0 to 15 and to check that in plus six is in the range 0 to 15. so that's how we we've ultimately build this template one to nine okay but now let's actually get into into the Sudoku puzzle itself okay so how does this puzzle work well okay um we've got we've got the solution it's just going to be a 2d array of numbers um we want to ensure that all those numbers are one to nine and then we've got the puzzle it's going to be a 2d array of numbers but now there can be some zeros and those zeros represent blanks so what should we do first hmm um well how about we start by just ensuring that everything is in the range one to nine so we're going to need a for Loop so we're going to do 4 I equals zero I less than n i plus plus oh I guess I didn't say but n here is going to be the dimension of the puzzle so so uh really we're only going to care about n equals nine okay but so uh but by making a variable perhaps we could use we use this part of the code in the future uh to ensure that for example a six by six Sudoku puzzle is solved correctly Okay so we've got this this double for Loop and this double for Loop is just going over uh the two dimensions of the puzzle and what we want to do is ensure that every value is in the range one to nine so I'm going to need an array of components so component in range and n it's a two-dimensional array because we want to have one component for every cell of the puzzle and so now what I'll do is I'll set in range i j to be equal to oops to be equal to a one to nine template and then I need to connect the input so I'm going to set the in for this component to be both equal to and constrained to equal to our solution at location IJ so the whole point of all of this and it's always good to write comments is to ensure that each solution cell our each solution number is in range and that and this code does that okay and so actually one thing that we should be able to do right away is test that a candidate solution is valid of course you know this isn't we're not we're not done we still need to check that the values inside different rows are unique and also that the solution agrees with the puzzle but it's good to test your code as you go and already this is something that we can test because if our solution is valid then all the all the values should be in range okay so what is the next thing that we want to do uh well perhaps now what we should do is we should ensure that the puzzle and the solution agree and so what I mean by that is that in every location either the puzzle should be zero or the puzzle in the solution should be equal the reason that it's or is that if the puzzle is zero it's blank and so um well you know any anything in the solution will agree with a bank a blank in the puzzle but if the puzzle has a non-zero value then it's important that there's agreement so this is also going to be a two-dimensional for Loop so we'll go ahead and copy that from our previous our previous Loop and how how are we gonna how are we going to do this well it turns out is a very nice way um it suffices to say that the puzzle cell times the puzzle cell minus the solution cell is zero if the puzzle cell is zero this is satisfied immediately because the left hand side of the product is zero but if the puzzle cell is non-zero then the right side has to be zero I.E puzzle cell minus solution cell has to be zero I.E they have to be equal and so we'll just go ahead and write that constraint so we'll say that the puzzle at location i j times the puzzle at location i j minus the solution at location i j needs to be equal to zero great okay so we're making some progress and now um what we have to do is uh check that every row has at most one copy of every number so we need to use that distinctness thing from earlier and so once again a 2d array seems useful so our goal now is to ensure uniqueness in rows great okay and so and to ensure uniqueness in rows we're going to need some distinct components so let's declare an array component distinct of length n and so um let's see so here J will be our iterator for different row numbers and uh uh or sorry I will be our iterator for different row numbers and J will be our variable for different column numbers and so if we want to ensure that uniqueness in each row for every row we need a new component so here we're going to say that distinct I is equal to a distinct template instantiation okay and then J now is going to be the different column indices and so what we want to do here is we want to say that the distinct components input in particular it's j input is going to be equal to our solution that location IJ so we're taking our cell and we're contacting it connecting it to our component good okay and then at the end we have our our main declaration um our main component is a Sudoku circuit with template parameter nine and the puzzle is is public and of course the the solution is not public so great um we've just done that and so now I'm gonna to go out into the main file now sorry I'm back in my terminal and we've actually what we've done is we've written a make file for you um so I'll I'll just print it out right now here's our here's our make file um or maybe I should and basically what it does is it just runs all the different steps of the circle compiler and the proof itself in order um and so the first thing that we're going to do actually is uh we're just going to run the circum compiler and so we can we can run the circum compiler just to check our code by running circom and then passing it the file and it's going to run it's actually going to tell us that we have an error and if our error is apparently on line 37 we had some unrecognized token and an ending curly brace when we should have had something else so let's go ahead and open our file and go to line 67 so we're now on line 67 and we're going to see why this curly brace was unexpected and I bet this curly brace is unexpected because we forgot a semicolon on the line four so we've added that semicolon and now we're going to run our compiler again and it's saying okay so you've created this component called distinct using uh or you've invoked this distinct template and it you gave zero parameters but one parameter was expected so I can bet I know what's going on there I bet that the stink takes an argument for the number and flies of the array and it should be uh that the argument should be 9 or it should be n but we didn't give one so we're gonna we're gonna go do that so let's go down to the bottom find that distinct component here it is and we're going to set the argument to be n good so we've found two syntax errors and now um okay great so now it's telling us that we're okay so let's go ahead and uh let's run the make file and that's just going to go ahead it's going to do a lot of things it's going to have to run the setup algorithm for the zero knowledge proof which actually takes a while that's what all this time right now is doing and it's going to go ahead and write our proof and it's going to go ahead and verify it and you can actually see the make file printing out the commands that it runs so let's see let's go well I guess we'll we'll look at them reading make is kind of hard yeah so let's so first of all we run this powers of Tao ceremony um we earlier the compiler outputted the sudoku.r1cs file that represents the r1cs itself so we do setup with the r1cs and then we run our proving and then we run our verification um so if you want if you're interested in the details of like the steps that you have to to to run to compile your circuit and then later to create the zero knowledge proof they're actually a little bit intricate I mean you can find them in the make file in the starter code but for now for our purposes this is the end of the tutorial we've successfully made a circuit that checked part of a Sudoku puzzle okay practice here again so now we're going to cover the second approach for programming uh constraint systems and in particular r1cs and that is the so-called Library approach so to recap on cercom it's this Hardware description language for specifying r1cs and a key feature of Socom is that you get direct control over constraints however it's a custom language and this can be good or bad depending on sort of you know how well designed the HDL is and how easy to use it is okay a different approach to sort of programming zkps which gives you the same very direct control over constrained systems is to use a library so in this approach you define a library which is implemented in some host language which is usually a popular high-level programming language such as rust or camel C plus plus go and so on right in all of the sort of libraries that sort of implement this approach there is one key type and that is a constraint system so this constraint system object is responsible for maintaining State about the r1cs constraint system as you build it up and the variables and values assigned to the variables as you sort of are doing the constraint system generation a little bit more detail the constraint system internally contains um the representation of the three constrained matrices a b and c as well as the values that are assigned to the variables you know if there's any values assigned the key operations that you can perform on this constraint system object are creating a new variable which basically involves appending a new entry into this list of variables creating a linear combination of variables which corresponds to for example you know five variable one plus two variable three plus three variable four and so on and so forth right so basically any arbitrary linear combination of the variables in this list finally you can add a constraint which adds a new entry into each of these three matrices let's see what this actually looks like um in sort of pseudo rust okay for variable creation you will have a ad that function or method which takes us input the constraint system so that it can mutate it and add a new entry the visibility of the variable whether it's public or private value that's assigned to the variable in case you are doing proving and the result is a variable ID which sort of is an identified or a handle on the variable which can be used later on for example in linear combination creation as well as in constraint generation okay so in the process of uh you know when you call CS dot add where a new entry is added into the variables list which is consists of the Tuple ID P comma V so it contains the variable handle the visibility and the value okay once you have a bunch of variables that you've gotten by calling cs.advare you can construct so-called linear combinations this is um basically as I've said a list consisting of coefficient comma handle pairs right so what this looks like as you can use cs.0 to create an empty linear combination which contains nothing and then once you have this empty linear combination you can add a term to it by giving the coefficient c as well as the variable handle I ID as input and then you'll get the modified LC represented here as LC Prime and that contains the original terms of the LC plus an additional term which corresponds to c times ID right so for example if your original linear combination contained five comma V1 then and you and you call LC dot add 2 comma V2 then your new LC Prime will contain 5 comma V1 and 2 comma V2 all right so it's basically just a pending uh this pair of coefficient comma variable handle to the linear combination list finally um the most important operation in a constrained system object is to as we said add constraints right and this is um this happens via this API CS dot constraint which takes in three linear combinations corresponding to the three matrices and adds a constraint which enforces that the LCA times LCB equals LCC once you sort of substitute the values of the variables in place of their handles right so these lcabc are added to the A B and C matrices respectively okay so this is quite a you know high level description let's see what it actually looks like when you're trying to implement a common operation and we'll take uh the example of performing a Boolean and okay so we'll Define a new rust function which takes us input the constraint system a variable representing the first input to the and and another variable B representing the second input the and what we will do is we will construct a new variable result which is a witness variable right so this is a shorthand for passing in the private visibility into the new VAR method okay and the value that's assigned to this variable is the value of a and the value of B right so we just do the logical and between a and b and that should be the value that's assigned to the result Okay so we've created a new variable but now we have to enforce that it's actually correct right that it actually satisfies uh the constraint that namely it is the and of a and two to do this we will first construct some linear combinations and this is where this rust macro which returns a shorthand for returning an empty a linear combination okay so we will create a linear combination containing just the term a one containing just the term B and the final one which contains the result okay finally to enforce our and constraint we will pass these three linear combinations into the enforce constraint or constraint method and this will enforce that a times b equals result so the reason why this is correct is if a has value 0 or 1 or B has value 0 or 1.

[00:59:49]um then the and of these corresponds basically exactly to the multiplication of these variables seen as field elements right so think about it if a is 0 B is 0 then 0 times 0 is still zero and then this corresponds exactly to the and so the result must have also value zero and if you sort of enumerate the other cases you'll see that it all works out okay in the end we sort of return the result variable and get our result as needed all right okay so this is not too complex but it's kind of a lot of boilerplate um that you might not want to repeat every time right you can get tedious and error prone and writing any complex algorithm say such as signature verification in this style would be quite a pain so instead of programming our computations are programs just by enforcing manually the enforce constraint and new variable declaration and so on we instead want to Leverage The Power of the host language rust for example to be able to abstract away these low-level operations right so because the load our host language provides abstractions such as structs enums operator overloading methods and many more we should use these to allow better developer ux and here we can see one example of that what we'll do is we will wrap our variable in a dedicated type right so we'll have a Boolean struct and then we will use the operator overloading feature of rust to allow in the future just doing literally writing a Ampersand B then we want to compute the and of two Boolean variables so we will put the same logic as what was on the previous slide inside uh the function body but sort of once we've done this now we can use high level syntax okay does it so does this approach actually work so yes we can declare our variables you know very nicely we just say it's a new witness or a new witness or whatever right so we give a and b true and false and then we can enforce that the result of a and b equals false we have this very simple line right so now we don't have to have manual calls to constrain and a new variable and you know manual LC generation we can just write a opposite B okay so there's many different Gadget libraries not all of them you know use this approach to the full extent they don't all try to use the language abstractions but many of them do all right okay so that's nice from the abstraction perspective but what about our the expressiveness of the language in terms of enabling witness computation now the good thing is that because we are embedded in a host language which is a general purpose language we can leverage that power to perform arbitrary computations to actually compute and generate our Witnesses right so for example instead of just providing true we can actually say that the value of this a witness variable is you know some random expression in this case 4 equals equals 5 which is going to be false and X less than y where X and Y are some other variables or some other native host variables right so you can imagine putting whatever logic you want inside this um and the good thing is that this logic is executed only when needed only during proving and not during say setup when the value or the variable assignments might not even exist right so we're not going to if it's an expensive computation we're not going to execute it unless it's needed all right so this is this was a high level overview um let's now dive into a tutorial on how we can use this approach concretely with one specific uh programming constraint programming Library which is in the arc Works ecosystem okay so now let's dive into how we can Implement our Sudoku checker using the aquax r1cs constraint libraries in particular we'll make use of the aquax r1cs standard libraries which contain constrained versions of many popular Primitives such as integers booleans equality comparison and so on okay so first we have to Define our puzzle and solution types and here we are able to use rusts type system and particular we're able to define a puzzle which is generic over the size so any n by n Matrix works and is also generic over the underlying constraint field we're not limited to a particular finite field we can make it work with any final field that we want to instantiate it later but anyway the type that we want to put in here is basically an array of arrays so um and the element of the array is going to be sort of an N by an array of phrase and the same thing goes for the solution um but we have to do though is we have to additionally specify the constraint field in here and the same thing here so now puzzle in solution are both generic over the constraint field type so any constraint field will suffice okay so we're going to reprise this strategy that we had in the circum example and what we're going to do is we're going to do perform two checks first we have to check that each row contains only unique entries there's no repeated entry in every row and then we have to check that the puzzle matches the solution and what this means is that we have to check that the solutions entries are within the particular range of one through nine and that they match the entries in the puzzle okay so let's take the you know each task one by one starting with uh the row checker all right so what we'll do in this is we'll iterate over each row all right and again here we're using rust's iteration syntax and then we're going to iterate over each row in turn over the entries in each row rather and basically the syntax says for the jth element which is cell um and we're basically able to obtain this we are using rust iterator infrastructure okay so what we're going to do now is that we have an iterator over each cell in a row what we have to show is that this cell is not equal to any of the prior cells in that row so we can do this by performing another iteration over the prior entries in the row and to get this list of Prior entries we're going to be using rusts slicing syntax well basically this says is give me the entries in rows starting from 0 and up to but not including J okay so now we have the cell and sort of every prior cell and what we need to do is check for inequality so we need to check whether this is um not equal to the prior so with the current cell is not equal to the prior cell and then we need to enforce that this is true that that the current cell is not equal to the pressure cell so we reinforce that condition is true so this is all that that we need to actually specify our um example here to in particular to just check the rows are correct so now we can move on to the next part of the solution which is checking that the present matches the solution all right so we'll set this up in a similar way we'll iterate um over the rows and Columns of the puzzle and solution but thanks to rust's iterator syntax we're able to iterate over both the puzzle rows and the solution rows at the same time as follows so what we're going to do is we're going to first iterate over the puzzles the rows and we're going to zip that with the rows of the solution and similarly we're going to now iterate over the entries in each of these rows at the same time using again the iterator okay so we have this um now we have an iterator over every so corresponding entries of the puzzle and the solution and the first thing we want to do is we need to ensure that the solution uh this s is in the correct range say one through n inclusive right in this case and normal Sudoku n would be nine so the range will be one two three four five six seven eight nine okay so what we're going to do here is we're going to first get a Boolean indicating whether um the solutions entry is less than n or less than equal to n right and then this has so this is one side of the condition the other side of the condition is that it is greater than or equal to the constant one right foreign syntax and now we need to enforce that this the end of these two actually equals true this is a slightly more verbose than using say Socom or the next one that we'll see which is Socrates but it's still you know pretty readable and we can also try to Leverage yeah we can try to leverage rusts of operational learning better here r1cs standard doesn't fully Implement that yet okay all right so um now we've ensured that the solutions entry is within the appropriate range what we need to do next is ensure that the solution entry matches the puzzle entry okay so we need to ensure that either the puzzles locked is zero which means that is something that can be filled in by the solver or that the slot matches the equivalent slot in the solution so the solutions slot it fits as one then it must be the same entry in the puzzle must also be one okay and we'll enforce this by first checking that either the puzzle entry is equal to the solution entry or if that's not the case then we have to ensure that the puzzle entry is zero right okay so now we have this R which represents the whole condition and we need to enforce that this is true okay so I'll let it that it takes so now we've enforced that the solution is in the correct range and that it matches the puzzle okay um all we need to do is return ok to indicate that the puzzle can that the function completed successfully without any errors and we will do the same thing here as well okay so we have an additional check helper function that's already written for us what it basically does is it creates a new constraint system um allocates new variables for the puzzle and the solution so for the puzzle it says it's a public input for the solution it says it's a witness okay and then we call these two methods that we just defined puzzle matches solution and the check rows finally we check or we assert that the constraint system is satisfied all right this is basically just a helper function because we're going to be um having two kinds of tests in our main so for the first test we want to check that our solution that the code that we've written actually accepts valid Solutions so in this case we'll Define the puzzle to be one zero zero two and a valid solution to this puzzle will be one two one two right um the entries of the rows are distinct there's no repetition and um yeah the entries of the solution match the entries of the puzzle when necessary so we expect this check to pass and let's try to see if that's the case uh right after going over the next check which is to check that it rejects uh incorrect Solutions we'll come to this in just a second let me just comment it out so that we can get the compiler running so let's create a new terminal and here let's do cargo run oh we forgot to save and we have a slight bug we forgot some syntax here so this should be uh in and if we save and run again we should have everything compiling and we'll see that this assertion passes it does not lead to an error which means that our solute that our code accepts valid Solutions now let's comment out in the invalid solution and now our assertion should fail again let's try cargo running again and we'll see that it is unsatisfied um because this solution is invalid in particular it contains a Zero Entry right so it should be the entries of the solution should be in the range one or two okay so that sort of wraps it up um you can use the artworks interface to um use these constraint systems with any r1cs accepting stocks such as cross 16 Marlin Germany many others right um and I won't go into that here but it's very easy to plug this constraint system into that into those snarks okay so after seeing that example of how to program this Sudoku Checker in Socrates let's now take a look at our next programming framework and that is compiling a high level ckp specific language to r1cs we'll start by doing a quick recap of the previous two approaches and this serve as a starting point for the rest of this section so hdls and circuit libraries do have their differences one being that circuit libraries use their host language which can be a full-featured programming language whereas hdls are limited to whatever custom language that they have specified right um but despite this difference there are actually in terms of the core operations you do there are similarities namely in both approaches we have to explicitly create wires or variables and then explicitly write down constraints which enforce some conditions on these variables and you know this is despite the fact that we might be able to Leverage The abstractions of our languages right so for example in Socom you could use templates in artworks you could use the rust programming language features however at the end of the day somebody somewhere has to write down code which explicitly creates variables and explicitly constrains them so the question we should ask ourselves now is this is whether we are limited to this paradigm and thankfully for us the answer is no there is a more ergonomic way and that is to sort of design and specify a high level language which you know has the niceties of something like rust but doesn't require us to explicitly program r1cs or Reason about individual variables so we would specify we write down a program in this high level language making use of nice features such as functions for Loops variables arrays structs and so on and then we would throw this at a compiler whose task would be to take this representation this textual representation and spit out r1cs which consists of the familiar wires and constraints and variables and so on so this is a high level idea and let's take a look at how this manifests in one of the most popular ZK programming languages called Socrates foreign Ty's um supports many popular features of languages such as you know custom types types you can define a custom type as a struct or as a type Alias right and then every Socrates program has a main entry point called the main function and inside this function and subsequent other functions we can Define new variables which have values that are used during execution or proving um we can annotate the inputs to the main function in terms of their visibility so in this case this function or this variable X is public and is known to the verifier and finally we can enforce specific constraints on these variables via the assert keyword note that this is different from the sort of constrain method that we saw in the arc Works approach here assert can take any Boolean expression as input right it does not need to take a linear combination since input but can take any Boolean expression in this case it's checking that x equals y 0 times y1 but you could put whatever you wanted as long as it evaluates to true or false okay so this is the high level syntax um in a little bit more detail Socrates supports a lot of advanced features such as generic integer generic type parameters um to functions so this allows this basically says that this repeated squaring function is generic over some integer argument okay we can specify arrays that can be mutated for example in in for Loops that have some fixed compile time known length and we can have if Expressions as well as compile time known array accesses so the index into an array must be known at compile time okay so put together all of these features allow us to have a very rich programming environment and write quite high level code so this is nice from a ux perspective but what about expressivity do we take a hit here and the answer is unfortunately yes particularly from the perspective of witness computation in more detail there is no way in Socrates to compute a witness during the execution of a program and instead all Witnesses or private inputs must be provided as arguments to the main function right so this main function which is the entry point into into a Socrates program the arguments to that main function are the only places where we can specify um private inputs so we cannot declare a private variable during the execution even of Min it must be declared at this point all right okay so how does the how do these pros and cons play out in practice to investigate that let's take a look at our next tutorial which will be the Sudoku Checker in Socrates okay so let's get started our task as we know is to implement the Sudoku chakra in this high level language called um Socrates right so we'll start as in the artworks example by defining our custom puzzle and solution types and just like rust Socrates also supports integer generics as we saw right so like in the artworks example we're going to Define our puzzle as a multi-dimensional array two-dimensional array in this case so it's an array of arrays and each array is of size n so this works for the puzzle and for the solution all right and again now our strategy for implementing our constraints is going to be the same as before we're going to check that each row is unique and we're going to check that um then that the puzzle matches the solution and furthermore that the entries of the solution are within the required range all right so let's get started with our check Rose function okay so we're going to iterate over each row so for u32i in zero dot dot n so in the range 0 to n including n minus 1. and then for each entry in each row we're going to do for you 32 J in zero dot dot dot and and now what we're going to do as before is check that the I comma jth element is not equal to any of the previous um elements in that row so to do this we will instantiate yet another for Loop but the range of this for Loop is going to be up to J so it'll be 0 1 2 3 up to J minus including J minus 1. those will be the values of K and so what we need to do is assert that the I comma J element of the solution is not equal to this is LMS is not equal to any of the previous um elements in natural okay all right so here we're able to use you know to access the inner element of solve we have this dots and tags we're able to use array indexing and we have our four Loops for iterating over the compile time fixed range an interesting thing to note here is that this innermost Loop you know on the face of it it looks like it has a variable number of iterations because J takes varying values but the Socrates compiler is able to figure out that actually the number of iterations of the number of sorry the value of J and in a particular iteration is going to be fixed right so you know say J equals 0 in the first iteration then the range of this for Loop will be from 0 to 0 so the follow-up will not execute if J equals 1 in the next iteration then this for Loop this inner for Loop will go from zero to one so the value of K will be zero and so on and so forth so basically each time the uh in each iteration where basically the length of of this Loop is fixed all right okay so at the end we will return true just to indicate that our function completed successfully okay so that's it that's all we need to do to check uniqueness it's very similar um to the aquax code but it looks a bit more readable because we're able to use these native operators such as naughty codes and so on okay so that's that now let's move on to the next step which is to check that the puzzle matches the solution and the solution entries are in the correct range so we'll follow the same strategy we'll iterate over uh for sorry n0 dot dot and so we'll iterate over the rows and over each entry in each row and we're going to assert two things first that um the elements are in the correct range right so they're greater than zero and they are less than so let's say in this case we'd only support Sudoku numbers so this is going to be less than 10.

[01:26:49]okay this is the first assertion the second assertion is going to ensure that the puzzle matches the solution so we'll again we'll have the same uh strategy as in the aquax case we have to assert that either the this entry of the puzzle is zero which is an empty slot and can be filled with anything or if that's not the case then it must equal the corresponding entry in the solution okay yeah if it is zero then it can be filled in with whatever value and we don't care about the value of the solution as long as it satisfies the chakra function but if it is not zero uh in the the entry in the puzzle is not zero then it must equal the corresponding entry in the solution and that's exactly what we're checking okay so then as before we will return true to indicate that the function completed executing correctly all right and so our main entry point for the function or for the program in general is going to be this main method and it's going to take in a public input which is the puzzle this is known to the verifier and a private solution which is known only to the prover and then we'll pass these two into the uh check rows and check puzzle matches solution functions okay so this looks um nice let's try to try it out and we're going to open up a new terminal window so Socrates has a few different commands that you can that need to execute to be able to generate the proof the first is to actually compile our program into r1cs so we're going to invoke the compile command with input the name of the file okay so we have a compile time error and it seems like we forgot to put a semicolon in our code this is you know very common problem for anybody's program C or C plus plus or rust anyway so we once we fix that we can see that it compiles and it requires a relatively large number of constraints even for a two by two Matrix it requires three thousand constraints but no matter you know it's still quite small and the larger scheme of things so the next step is to invoke the setup command to be able to generate a set of public parameters that we can use to test our code so we should not use this in production instead you want to use something like powers of Tau type setup ceremony multi-party computation based ceremony okay so here we're going to perform the setup and it's going to be for the default uh zkp which is grot16 all right so we've done the setup and as you can see it's using draw 16's key uh the grot16 scheme and there are some um warnings here about malleability we don't have to care about that for this example the verification key and proven key have been written to these files and the setup is now complete all right the next step is to sort of compute the witnesses that we will use during proving okay and to do this we have to provide the concrete instance of the puzzle as well as of the solution so the way to do this is um there's a variety of ways to do this you can read them from a file you can read them from different file formats in fact but what we're going to do here is we're going to pass the puzzle and solution as input on the command line and we're going to do this by um sort of ordering our puzzle and solution in row major order so this one zero zero two is going to be the puzzle which means the first row is one comma zero the second row is zero comma two and then we're going to pass in our solution which is going to be 1 comma 2 1 comma 2. so it's very similar to the artworks example all right so the properties computes the witness and basically this involves generating the values or any intermediate variables that are generated um in the r1cs constraints okay so all those values are written into this witness file and then we can invoke the generic proof command which will take this witness file will take the proven key and spit out a zero knowledge proof which is improve.json which we can then verify using the Socrates verifier and as we'll see the verification passed we can try to pass as before an incorrect witness right but as we'll see here uh it made Socrates tries to plug in these values into the uh execution it will fail in particular the check that we expect to fail is going to be the row uniqueness check and indeed we'll say the assertion failed at line 17 it's exactly where we're having the failure right okay so that wraps up um Socrates and now I'll hand things back to Alex for the rest of the lecture welcome back at this point we've gone through three tutorials you've seen how to use circom how to use ARC works and how to use Socrates and now we're going to take a few minutes at the end of the lecture to synthesize we're going to think about differences and similarities between these different tools and the benefits and costs of using them three different kinds of tools that we saw were first Hardware description languages which are the languages Standalone languages for describing circuit synthesis second we saw a circuit synthesis libraries and third we saw a programming language Socrates and a compiler that turns it into a circuit in understanding these three different classes of tools hdls libraries and PLS I think it's useful to view them as differing in two different ways the first axis of difference is the type of language whether the language is fundamentally about describing circuit synthesis or whether it's about describing a program so that's the vertical axis here circuit versus program the horizontal axis is whether or not the language has its own syntax whether it is a standalone language if yes then the language has its own compiler parser and so on and if no then the language is embedded inside some host so a circumstances library is an example of an embedded language for describing circuit synthesis artworks is like this it's embedded inside the syntax of rust and it produces it describes explicitly how to synthesize the circuit on the other hand circom is also about synthesizing a circuit but it has its own syntax so it's a standalone language and then finally zocrates or in general programming languages they're about describing a program and they have their own syntax and then they have a compiler that interprets the center that consumes the syntax and produces a circuit that has the same meaning as the program so this is one useful way to see these three different kinds of tools in terms of the kind of thing they describe circuit versus program and in terms of whether they have their own syntax but another way uh to another useful way to understand these different tools is in terms of the benefits and costs of using them the pros and cons and so right now we'll talk about some of the pros and cons of using circom Arc works and Socrates let's start with circon the pros of using sarcom is that it has an elegant syntax and it's very clear what the constraints are you have direct control over them whenever you want to create a constraint use this triple equality or perhaps you use the Double struct Arrow the con of using circle is that it's hard to learn at least for most people who come from computer science background because it's not really a programming language it's a hardware description language and the even bigger con is that Zircon has very limited tools for creating good abstractions there's no notion of user-defined structure in fact the only kind of abstraction that you can create is the abstraction of a sub-circuit there are no types that there's just signals and arrays of signals so if you want to create something like a Boolean um there there really isn't good tooling for doing that now let's talk about artworks the pro of using our work the pros of using Arc works is essentially that it preserves the clear description of constraints that servercom has but it gives you all the expressiveness of a language like rust and in general whenever using a circuit synthesis Library you have all the expressiveness of the language that the library is written in con is of course that you need to know that language so you need to know rust or whatever other language the library is written in and the um the library well it just synthesizes a circuit it doesn't really do much optimization for you so it's up to you to optimize you really need to hand tune and get all of the constraints to be as few a number as possible the final class of tools that we looked at is is it's the class of programming languages we look specifically at Socrates the pro of using a programming language is that it's out of all the options by far the easiest to learn because the semantics of a programming language those are the kinds of semantics that we're used to there are variables there are functions these are things that we're familiar with program languages can also have very very elegant syntax because they get to design the syntax themselves they're not they're not stuck to whatever rust or whatever the host language is using con though of using one of these programming languages is that you have to give up some control um and so we saw an example of this with Socrates Socrates doesn't allow you to describe explicitly how to compute intermediate Witnesses you just write a program and all the intermediate Witnesses are automatically generated and when the compiler is doing that well it's fantastic when the compiler is doing that sub-optimally it can be hard for you to optimize further okay so these are these are the pros and cons of circom artworks and Socrates but one of the things I want to say is that circum artworks and Socrates those are not the end-all be-all in fact there are lots and lots of tools for using zero knowledge proofs in terms of Hardware description languages surcom is is about it a hardware description language is a very simple thing and circum is a very good Hardware description language so people haven't really found the need to make another one but when it comes to libraries and PLS there there's a whole Variety in terms of libraries Arc works is the rust library that we saw but there's also AC plus Library called gadgetlib there's another competing rust Library called Bellman there's a library in ocamel called snarky there's another library in Rust called planckish that doesn't produce rank 1 constraints it produces constraints that can be used with the plunk proof system in terms of programming languages there are also a number of competitors to zocrates there's Noir ligo and Cairo pyro is is interesting here because it also doesn't produce r1s yes it produces the kinds of constraints that you need to use a stark process so it produces this thing called air the arithmetic intermediate representation uh in terms of of the history these these different tools and and languages have been developed over the course of more or less the last seven years here is the approximate date at which each of these tools was created and on the right hand slide you you can see that the timeline continues to to to go off to the right because I don't think that we've seen the end of these languages I think that over the course of the next few years people will come up with still new languages for for producing zero knowledge proofs perhaps even somebody in this class will will have an Insight they'll see a better way to build a language for zkps and maybe their language will be on this slide one day one thing that I want to emphasize given that there are so many different languages is that these languages they're not wildly different in the end of the day they're all about programming zero knowledge proofs um so these these many these languages they take in different representations different Source representations of the predicate But ultimately they produce a fairly small set of different kinds of constraint systems rank one constraint systems constraint systems for Planck constraint systems for Starks and that means that there are lots of common techniques that these the the libraries and that the compilers for the for the PLS share these techniques include techniques for representing booleans and operations over them techniques for representing fixed with integers techniques for encoding variable semantics such as mutation techniques for encoding user-defined structures techniques for encoding control flow techniques for optimizing circuits and techniques for representing interactions with arrays um so there's there's a lot of common ground um and and you know in some sense you saw this when you were using uh the when you're using the zocrates language you are able to create equalities booleans and when you were using the arc Works synthesis Library you were also able to create booleans using gadgets and there are some common ideas that underlie um the booleans and Socrates and the Boolean gadgets and artworks and so one one thing that's very interesting to me as a researcher is whether it's possible to try to create essentially a library for building zkp languages that centralizes a lot of these ideas so that when you're building new zqp language you don't have to design your own Boolean infrastructure you can use machinery for generating very efficient constraint systems that represent booleans that's that's already been built for you our interpretation of what that infrastructure is is this this Library called Cersei it's a library for defining zkp languages and you can find it on GitHub um and and whether or not sourcese is ultimately interesting to you I think it's useful to remember that all these languages have have a lot of common features okay um so this is the end of the lecture this lecture at a high level it's about going from high level ideas to zero knowledge proofs and we essentially saw three different ways that you can do that all these ways share in common the idea of producing a constraint system that the zero knowledge proof is going to be written about and there are essentially three ways to build that that constraint system you can use the hardware description language like circon you can use Library like artworks or you can use a programming language like Noir or zocrates and then once you've got your rank one constraint system um you're Off to the Races you can write your zero knowledge proof