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]
you