Mapping finite state machines to zkSNARKs by Fabrizio Romano Genovese (Devcon5)

hello everyone I'm from Brazil from state box and I'm going to talk about how to map finite state machines to ZK snarks using category theory this is joint work with unready SPO and Josh aphids are all four from our team as well we have a paper about what we did which is this archive link there okay so let's start what is a zero knowledge snark they are just a way to prove that some computation follows some rules without revealing anything about the computation itself they are good for privacy they compress a lot of information and blockchain people seem to love them so why not doing some research about them the nice thing is that for this talk you don't really have to know what does that case not is everything you have to know is that if you have a boolean circuit then you can turn it into a set case not so now the question becomes cool but what is a boolean circuit well it's just literally a bunch of logical gates who are together so in here you see for instance four gates an and gate and or gate a copy gate and a constant gate and you know this is a boolean circuit you just like work them together and you put bits in the vertical wires and you get an output bit on the right okay so what is a finite state machine a fine state machine in some very old gadget in theoretical computer science all the means good because it means that a lot of period has been redeveloped about fine state machines we know perfectly well how they work and how to prove formal properties about them so in here you can see this is just a vending machine a model of a very simple vending machine you can think about it just as a graph the vertex is represent all the possible states of the system and the edges so the arcs represent operations that mutate state so you see that in here you can insert the coin and go from ready to select and then you can order stuff and get changed and a competition that follows the rules of the thrusting machine is just a path in this graph so you see that you can't buy coke if you are not in the Select State you need to and if you're in your ready state then you have to insert a coin first so the idea is that if we can map these paths of this graph to boolean circuits then we can basically turn this circuit into a snark that verifies that a computation followed the rules determined by the final state machine okay so but what is category theory like where do you use category theory so category theory is a super complicated thing that is used to do simple things that seems like not great but actually it is because it scales better so the idea is that in category theory everything is compositional it's super related to type theory so if you like functional programming you should really like category theory even if functional programmers won't agree with me on this so the idea is that in category theory you can relate different mathematical structures everything is formally interconnected in a way that respects the structures of the things you are connecting this means that if we build a categorical correspondence between graphs and boolean circuits then we can be sure that if we morph the graph the circuit will morph accordingly and moreover once you category FIA concept you automatically connect it to the whole of mathematics and this basically means that now if you have a categorical correspondence between whatever you like to graphs then you will be able to pipe this correspondence inside the thing we are doing and get automatically that case narks out of it so this is an example with each graph G you can build a free category free of G this free khattak will represent all the possible paths in the graph so the posse lawful computations were interested about and you know this is a community square which is the very heart of category theory and what it means is that if you have an F that morphs your graph G to a graph G prime then you obtain automatically a way to morph the corresponding categories and if you map the graph G to the free category and then you morph does the same of morphine's morphing the graph first and then doing the free category so these square commutes it doesn't matter which path you take you can go from G to free of G prime using both paths so what we do is this we can basically use the adjacency matrix of the graph corresponding to the EFSM to build a circuit in this circuit you see you basically plug in an enumeration of a vertex on the left and an edge and this circuit will give you 0 or 1 depending if the vertex you plugged in is the starting vertex of the edge and it will give you the next vertex so if X to the e is a thing that goes from A to B and you plug a on the left on XV then you get one and B on the other side now we can connect these things together and this is exactly what this tree category will do so we can map now everything in this tree category to a piping of this modular circuits basically but we can do more we can obstruct the adjacency matrix which at the moment is encoded in these s of G and T of G like this and now the idea is that in this densely dotted wire you can also specify the adjacency matrix of the graph you want to use so now you are plugging in the vertex and edge and also the graph the vertex and the edge belong to so again all these things are composable and you can basically obtain a functor that goes from your free categories to these circuits this means that you are basically a cat Oracle way to map a fun estate machine to discard with boolean circuits and everything we built is compositional so basically you see in this huge diagram you start with graphs on the left then you calculate these three category thing and then you can there are different kind of things that are related to knowledge proofs or zero knowledge proof and the idea is that you know if you morph the graph down there you can basically prover s-- this diagram in any way you want it doesn't matter which path you take the only thing that matters is what is your starting point and your end point and is exactly what category theory is about so the take-home message of this dope is this if you build things categorically there's a good chance that they will be formally correct because category theory is all about structure and when you are able to express some concept categorically then the concept will be correct and type check by definition you can think about category theory is really like a semantics for type theory if you want then you will be able to verify that your constructions satisfy some nice properties and this is because categories are very structured so once you turn something into categories you have a plethora of formal tools that you can use to verify the your constructions of some properties and they will be more easily implementable in a formally verified setting because basically many formally verified settings are fully functional for instance we are merely using idris to implement this stuff and we just built a category theory library in idris we literally took a category theory book and implemented all the definitions with proofs in in idris and then you see that if you are able to you just have to translate the theory we developed to the idris library just is between quotes obviously because it's not easy but it's a very conceptual straight path to to get to formal verification and yeah in the end you will be able to link things together without making an a mess so that's basically it so yeah category theory is difficult in the beginning especially if you don't know it but it pays off big time as your system becomes more complicated so for instance in this case we have basically built a categorical module for our infrastructure a categorical gadget that trans graphs into zero knowledge proof now whatever you are doing if you are able to translate the stuff you care about into graphs then you can just use this module to get a zero knowledge proof from that graph that verifies that the rules specified by the finite state machine corresponding to a graph are being followed yeah I think that's it basically thank you [Applause]