Compositionality: The 10x Engineer Secret Sauce | Devcon Bogotá

foreign [Music] this will be a talk about compositionality uh it's probably a word that not all of you know and I'll try to explain what this is about in the course of this Workshop uh in the last months probably a year or so we've been hearing a lot about composable things composable blockchains composable service compositionality is basically just a mathematical Structure Theory that tells you how to do that in the most principle way possible uh I'll start and if you have any question just feel free to like raise your hand and interrupt me and I'll try to answer and or clarify okay so first of all to introduce the concept of compositionality we need to introduce some basic building blocks that are systems and processes so compositionality is basically the study of how systems compose to give life to more complex systems systems are basically things that can be transformed enacted upon and processes are exactly the things that act on systems and transform them uh a very interesting Insight from Modern mathematics the mathematics developed from 1950 onwards is that often is way more fruitful to understand something to describe it by looking at how the thing composes and behaves in a context so instead of splitting things open and look how they look on the inside we describe them by saying how they behave and how they interact um okay so let's start with something very very simple I will use a lot of pictures in this talk and hopefully close to zero mathematics uh for people that love mathematics I cannot that there is a soundness a completeness theorem that says that these pictures are formal which means by doing pictures we're actually doing mathematics it's just easier and more beautiful in my opinion so in here we have a very simple process that we depict as a box it just takes a number in input adds one and spits a number in as output I mean for I guess everyone acquainted to with programming that's just like man yeah okay uh the point is that when we have a process a process like that we can compose it with other processes so for instance in here we take this process we notice that it needs an input that is a number and spits out an output that is a number and we realize that oh we can actually pipe this process with itself and if we do that by just concatenating the boxes you see that this will be equivalent to the process that adds to to your input now this seems very naive but the nice thing about this picture is that it goes both ways you can start from the top row where you have simple components and you actually abstract away so add to uh is basically just you know the dotted box encompassing the two or you can do the opposite you can start from a process up to and open it up and further specify it with a finer degree of accuracy and since you have an equal sign you can basically go both ways now there are very peculiar processes that that are called identity processes these are the processes that don't do anything in this case with the number example we have a process that is at zero that takes a number in input does absolutely nothing with it and spits the same number as output the good thing about graphical reasoning is that since this thing is not doing absolutely anything we can just not draw it and indeed I'm drawing it as a dotted box uh down here just to highlight that there should be something there but you know with this very simple trick we can already start proving some equations that are very simple so if I add one and then I add 0 is like just adding one right if you know you adopt the convention of not drawing identity processes then the picture on the top row just looks like the one in the bottom row while you have stretched a wire a little bit more similarly from I don't have it here on on the slides but you can understand that in this formalism the composition is associative we don't use parentheses if you concatenate three boxes one after the other it doesn't matter in which order you obstruct them in the end you only have three boxes so it doesn't matter how you group them okay let's do another example so for this example I'm using gravitation gravitation that has absolutely nothing to do with crypto I admit uh at least I I think I don't know maybe uh so we have a system that is a sun that is just sit there and you know does nothing and raise the earth that is orbiting around the Sun so you know during many centuries people thought a lot about this and at some point basically a guy called Newton found out that there is a process that you can call evolve in which you can feed a state of your system and then you can say okay show me what happens one second later and this is a beautiful predictive power of physics in this case of dynamical systems that allows you to start from some experimental evidence and predict what is going to happen uh in the future you see that in this example you also have an identity process that is the process that doesn't evolve evolve for like zero time it's just taking the input and is not looking in the future or in the past it's just giving you the state that is as it is now and we see that we have a notion of composition because if I let evolve the process for I don't know one second I go from the position Mark type t0 to the position Mark T1 again I can feed T1 to the system another time let it evolve for another second and I go to T2 and that would be the same of evolving the system for two seconds so again I can combine These Bricks now the important thing is that anything that matters everything that matters in this formalism is how things are connected you can deform the wires no problem what you can't do is you cannot make new connections or splitting connections if you do you are getting something that has a different meaning another important thing is that you can only compose things with matching types for instance senior I have the Hub one process we saw that that spits out a number but the evolved thing wanted something of type sun earth as an input so you see that it doesn't really make sense to compose these things because they are apples and pears Okay so this tells us the types in this formalism are very important the way you type your processes changes what you can and cannot compose okay as an example imagine that you have a car right you have the wheel and the shaft and the gas tank and you could see this as a process that takes some inputs for instance I don't know fuel or and Human Action and produces heat and motion but when you look very carefully you see that you could pour any liquid in your car right like the gas tank won't complain if you fill it with water clearly the engine will though and basically from this you can you know infer that the problem here is that the type of input of our process is to General and it allows you to fiddle with the process in a way that produces unintended Behavior another example that I like is imagine a socket in the wall you can put a plug into it and you know use any electronic Appliance but if you have a couple of nails you can also stick the nails in the socket and what you go what you get is emerging behavior all over you and very painful so the important thing here is this is the main message of compositionality so when you look at this process like the socket and plug process you can start asking what are the properties that are preserved when I compose these processes together so physically sticking the nails in the socket makes total sense because they fit but if you're looking at things through the lens of safety regulations you see that a nail can be safe can you know be certified with whatever standard your country has same thing for the socket but when you compose them suddenly you have a very very unsafe system compositionality is exactly the art of choosing these types in a way that emergent behavior is averted as much as possible so that when you compose things you know precisely what is going what we are going to get now under the hood compositionality is based on a theory called category Theory this was invented in 1942 and had a monstrous impact on Modern mathematics essentially you can see it as a super glue of mathematics that describes how different theories compose and interact basically all the main progress in you know big areas of mathematics like algebraic geometry or algebraic topology come from here and in the last year people started realizing that this thing can be applied also outside of mathematics because again it embodies this perspective that you can describe things but looking how they behave in a context so when I show you those diagrams what I'm really doing I'm always speaking a category that defines the universe I'm working on and working in uh let me just dig a bit deeper into this idea so if you want to define a category if you're a mathematician you want to Define it formally basically you have to specify various entities you have to specify objects that correspond to systems in the pictures I showed you before so objects would be the wires in the box and wire pictures you have to specify morphisms that are the process the boxes that transform objects into objects you are required to specify identities so for each system you need to have a process that doesn't do anything to it and then you basically have to specify a composition law uh a recipe that tells you what happens when you compose processes together uh let me give you some examples of categories that are probably familiar to uh I hope as many people as possible here there's a category called set where your objects are sets and your morphisms so your processes are functions between sets there is always a function that doesn't do anything and you can pipe functions into each other for programmers there is another category called Data where your objects are data types and your programs are programs that turn data types into data types again you can compose programs this is basically functional programming Style programming you can pipe you know the output of a program into the input of another program if the data type matches and you are also a program that just Returns the input without doing anything so what is the difference between these two categories well set offers an intention sorry an extensional perspective what it means is that for instance if I consider the set of integer numbers I have exactly one function that takes a number and adds n to it on the contrary in data I have multiple ways of either specify what integer numbers are and I have multiple programs that sum n to your term in here I just brought two of them but in general you see that in the car in the category data the formalization the implementation matters so these two categories offer very different views on the same phenomenon in one case you're saying I'm only interested about behavior I'm not interested about the inner workings of these functions in the other one you say no I do and I distinguish two processes they could uh emit the same output on the same input but I want to keep them distinguished now the cool thing about category theory is that you can connect these different perspectives there is a notion called functor that turns a category into another category in our framework this would be a box that is sort of like level two box that allows you to change the universe you are working in so um basically what you do to define a functor is you specify a mapping from the object of the category C to the objects of the category D so you have to say where systems of C go in D you do the same for the morphism so for each process in C you have to map it to a process in D and and this is the important thing these mappings have to map identities into identities and compositions into compositions so what it means is that if I compose two processes in C and then I use the functor is the same of using the functions on the components and then composing them in D questions or sure not necessarily you can have functors that are called full and faithful that allow you to yet basically be inverted and go one direction to the other but no in general these can you can lose information or you can embed embed a less expressive Universe into a more expressive Universe if you want to sure it's like sorry factors as information so I don't oh linear transformations uh maybe I don't know like there is this very convenient thing that in category Theory everything is everything else like not going in depth into that but you can describe a category as a factor and a functor as a category and blah blah blah so it it is possible maybe to describe a function as a sort of linear transformation in general what I can say is that you can Define categories of vector spaces for instance and in that case your morphisms your systems will be linear applications that respect the linearity of the vector space uh yeah you know uh yeah yeah this is exactly what happens because this thing is basically mapping processes of C to processes of D so you can see it as an higher level function and indeed a factor is a process in the category of categories so you can do this kind of you know level up let me give you an example of functor this is a function that actually collapses information we saw two categories data and set and we can define a functor that sends a data type into the set it implements and sends every program to the function it implements so this is exactly what I was saying before that you can start in the category data and be you know very detailed about distinguishing things and then you say actually I don't care I want to collapse all this information and I want to forget about you know these different details you apply this functor and that's exactly what you get all your process compositions now you know lose a part of information obviously there are very interesting questions like how do I invert these things can is there a procedure to canonically invert a functor and actually go for instance from just a specification to sorry from a behavioral extensional perspective to something more complicated sometimes you can sometimes you can I don't think yeah so imagine that int is a data type that you define I don't know inascal uh about integers that data type is basically modeling the set of integers in a computer right so conceptually you can say I can send that to Z similarly if you have the data type string you can have a set of all the possible words on an alphabet and again you can send string to that set uh with this functor basically what happens is that these two programs here get mapped to the same function between sets so I have two different implementations of the same program that maybe you know I consider separate as programs like if I for instance hash the one on the left and the one on the right the hashes will be different uh but they correspond to the same function they are implementing the same function so when I go from data to set i'm I deciding willingly to lose that information okay let's try to use what we got up to now to do some process design that is actually the interesting part of it this is a very simple example imagine that you have a grid and you want to define the process of moving on this grid so imagine that you can only move of you know a kind of fixed amount of things so it's not like I cannot move like 0.1 steps but only one step at a time in this case you'll see that wherever you are there will be four fundamental processes that are up down left right that allow you to move one step and now I can basically describe every path as a concatenation of these processes so for instance if I move three times right and two times down I'm describing the L part I have there if I feed to this process a couple of coordinates that tell me where I am then these coordinates will be transformed as in the end of the path basically and we see that in this kind of theory we also have some equations like if you move right and then down does the same of moving down and then right you are describing a square you are just walking in like different paths but you end up in the same place let's spice this up and let's do it concurrently now we have multiple agents uh wandering on this grid and we want to model you know how they move intuitively what you do is well now we want to consider processes that happen in parallel like if I have two agents for instance I can have this process here that says agent one moves three times on the right and agent two moves down and then on the right and now we see that new equations pop out so for instance I have this equation here called The Interchange law that basically says these two threads are separate you can see the first are saying I move somewhere internet do nothing the other agent does nothing in which for you to move and then moves in this setup is the same if you just you know swap the things and second agent moves first and first agent moves later why because intuitively these two agents are not causally interfering with each other agent one doesn't care at all about what agent 2 does and vice versa and so in these formalization of moving on a grid concurrently I have these extra equations mathematically we say that the Universe we are relying upon is not just a category but it's something called the monoidal category that basically means a category where you can do also things in parallel okay let's do uh more like programming oriented example so let's consider a very simple record uh let's call it person uh This Record has two Fields name and surname okay um now you can notice that in this record in this example person is basically just a couple of terms of type name and surname now we want to be able to you know functionally describe the procedure of extracting a subfield of this record so you give me a person I give you the name for instance and we also want to be able to replace the subfield of a given type with a subfield of a different type this is a bit more complicated but what it really means is that for instance imagine that I want to edit this personal record I want to strip surname out and put a new field in called age that is of different type so the point is how can we do that in a automated and more importantly compositional way uh so what I mean by compositional is Imagine This example where I have the record person but one of the fields is itself a record it's a sub record and now I say okay I want to replace the city thing there Bogota with something else intuitively I want to be able to pipe the process for editing person with the process for editing address and you know feed these compose these two processes in a way so that I don't have to reinvent the wheel every time the way you do this in a functional programming and in compositionality is with something called a lens that is a particular example of something called an optic so what is the idea uh the idea is that the lens is just a couple of processes one called get and one could put and basically get is taking your record and is giving you the subfield that in this case is s subfield of a what put does instead put is taking your record a is taking something of type T and intuitively is replacing s with t and now it's spitting out something of type B you see the type of a could change because you replace the type of a subfield of this thing if a was a couple of strings with this put I could substitute a string type with a nint type and then the overall type of the record will change the funny thing about this is that you know there is an ask a library for instance that allow you allows you to automatically get these things for every a s and t as soon as you define your type A this thing will you know create the Setters and Getters automatically for you so it's a it's a procedure that you can automate and that's the cool thing you don't have to do it manually the library does it for you okay so I'll do these things compose imagine that I have two lenses so the first is taking the subfield s from a and the second one is taking the sub field V from s the get part is easy because you see you can just telescopically access the records you can say I start from a I pull out s and I pull out V from s the part is a bit more complicated so what happens here is that imagine that in S I am replacing the subfield V with a subfield W and I obtain something of type t and now I want to replace uh s with this type B into a how do I compose these two things well with this sort of like monstrous awful thing here in in the bottom where I basically take a I copy a I get S from a now you see I can use this put put V and basically substitute uh V in s with W I get something of type T and then I can use put on T and A to get a B I know that this sounds very cumbersome and difficult to follow but the good thing is that you can you know topologically deform these diagrams and basically Express them in a way that makes way more sense so in here instead of considering this funk these things are two couple separate processes I'm you know packaging them as a unique thing so as you can see this thing is a bit strange because it has arrows going in opposite directions so on the top row a gets processed into an S so you are extracting s from a on the bottom row you are getting this t on the right and you know you are writing s with t and you're getting a B on the left this is an example of a bimodular data accepts accessor the way you can think about it is as a process that says if you give me an a I will read field s and forward the output to you and if someone else from the future will give me a t i will replace S in a with it and return u a b and the good thing about it is now you can compose them exactly as you composed the processes we sew up to now and when you do this if you squint your eyes a bit you see that we are doing something that is basically equivalent at that um to that cumbersome composition we had before but now is again graphical like you can just compose these Lego bricks together again and this is the art of compositionality anything that really changing is the point of view so you can still deform this thing in another way I'm just rewriting the top diagram as the bottom diagram if you see the interconnectivity of the diagram didn't change and I can shape it as a comb basically and again it's the same like you get a in you get an S out then you get a t in and then you get a B out these is really interesting because when you look at this comp process it really looks like something that wants to be a normal function but it can't because it's waiting for you to do something intuitively if you have an automated way to turn S into T that thing would just be one of those naive building blocks we saw in the beginning and you know in this framework the composition will be nested he would be of this sort you are basically composing comms by substituting a comb in the whole of the bigger comp and again this composition is exactly the same when you follow the the processes and the interconnections of this one this one and this one are the same thing we just deformed the way we arrange the diagrams now again as I said you can see a comb as an incomplete process that basically is waiting for you to do something to turn a nest into a t and that would be that F that you put there and if you put it there this thing basically closes up and just becomes a normal process but what is really interesting about this is that we found a pattern so we started by modeling record rewriting but now we found a new pattern of composition that is this kind of nested composition and indeed there are a lot of things that compose in this way if you abstract from details for a second these two processes are basically representing two different points of view of the same thing that is bi-directional transformations now let me give you an example of how you can use these things an example would be estrus what is an escrow trade an escrow trade is when I want to give something to someone but I don't trust that someone or that someone doesn't trust me and so what I do is I take my funds instead of giving them directly I lock them up in a vault and then basically you know my counterparty will ship me some goods and when I receive them I will confirm that I received them and at that point my funds are unlocked and forwarded and that is exactly a calm looking thing it's like I committed my funds I locked them and now I'm waiting for confirmation and as soon as you give me confirmation and you put it in.com then this looks like a standard transaction from A to B another example and this will be the main point of the second part that my colleague Philip will do is Game Theory so we can model games in Game Theory as op as open processes basically in that case a game will be a process that has again two inputs and two outputs it will take in input and observation so it will observe the word it will spit out an action According to some strategy if we receive a payoff from the outside world and you will return a feedback the feedback is probably the most difficult part to get in this composition method and you have to imagine it one of the ways to imagine it is is the portion of your payoff that you have to return to someone else stupid example if you take a depth you place a bet you win you get a payoff that you have to repay the debt and the debt repayment would be the feedback wire in this system of compositional Game Theory we can recover traditional games as a composition of processes so this for instance is the prisoner dilemma uh I guess a game most of you are familiar with and normally we see it as a payoff Matrix and you know like if player R does this then this is what happens if player B does that blah blah blah in this case prisoner dilemma is the composition of three different processes player one player two and payoff Matrix these three things in isolations are games player one and player two are games that do not observe anything because you don't do any observation in the prisoner dilemma they just act they just you know Express a choice and they receive a feedback for that choice the payoff Matrix gain is a game that doesn't act it doesn't have any strategic value but it just observes the players move and returns some feedback and again you see that in this setting the players payoffs are the payoff Matrix feedback and the player's actions are the payoff Matrix observations so yeah the cool thing about that is that now we can quickly prototype games by basically creating these blocks and interconnecting them with each other one thing we are currently working on uh and Philip will show a demo of this is for instance a way to lift evm byte code to open games automatically in doing that you know if you deploy a smart contract we can take your smart contract and put it into this framework and then we can strategically probe it your smart contract would become like the payoff Matrix in the system and then we can economically probe it with players that can be honest or untrustworthy and see you know which strategies are actually winning strategies or not and so if your contract is economically sound economically stable or not or in within which bounds it operates financially in the way you intended so this is the theory part that is concluded and I will leave for the second part everything to Philip uh and basically yeah in this short tutorial we saw how we can use this compositionality techniques to guide our intuition in designing processes we started with something very simple then we start we did a bit more involved the um examples and then we found out that those examples were actually modeling and more General pattern this bi-directional composition and we were able to basically recycle that pattern to instantiate other things like escrows or open games and yeah that's everything for me and I'll just pass it to Philip thank you [Applause] if you have any questions if you have any questions we can in the meantime that Philips up the computer feel free to ask sure uh the final uh yeah uh I I mean in here I kind of cheated because I basically just defined an optic as you know this box obstructing the details indeed mathematically you can uh prove the I mean the definition of optic is exactly something that embeds that thing mathematically it's a bit complicated to describe uh but graphically that's exactly what it is an optic is something that has this sort of nested notion of composition basically sure yeah there are various ways to do that uh Philip is the expert in this and I don't know maybe you won't yeah sorry um what's your question whether you can also do repeated ly yeah yeah you can do that um so the game that for business short is a one shot game but you can also think about this as taking that let's say you want to iterate it finally many times you just stack it on each other the only qualification you have to make um if you looked at the slide they were basically the um the the wires were not coming in from the outside you have the game with wires and then you can stack it basically alternative way to do is also you can turn it into a Markov game which has a state and then you can basically think about it as approximating it to be run infinitely okay other questions to the first part there is a question in the first part um let me do the following I'm trying I'm jumping on my slides ahead um to show you this then I will go back ah sorry could you guys sorry can you switch on the okay um let me go to the so here um you have to think about it as two Dimensions right so time flows from left to right and if you start from the left there are two things P1 and P2 they are not connected which means they happen in parallel so this is simultaneously happening then afterwards they output the move which is y1 and Y2 that move is consumed by U which is the payoff function and in that sense you follow sequentially after these two games right you can also think about these two games P1 and B2 being merged into one and then it's just big two games being stacked on top okay so let me go back to the start you can already see what is coming okay um so what we want to do in this in this part in the second part by the way hi I'm Philip thanks thank you all for coming um what we want to do in the second part is basically take a deeper look look at compositional Game Theory as one specific instance of um how you can think about compositionality and what compositionality possibly can give you as value to um as an approach to thinking about in that specific context of strategic interactions okay compositional Game Theory what is that actually so it's a at the beginning actually this was a research project which was focused on providing a new formal language for game theoretic reasoning yeah you probably have heard about Game Theory many of you probably have already seen it it's a mathematical language to express the reasoning about agents and what we provide is just another language in some sense now this language is as for pizza already introduced based on the categorical framework and this has several consequences one is you give you first of all you get a graphical way of reasoning but most importantly you get a way of compositionally approaching the modeling problems um that you that you face okay now if you just do the diagrams and you you know suppose you would be forced of you know using diagrams for very large systems like a staking protocol or other complicated more complicated systems that would be limiting it would not be that much help it might be a cool new Theory it might be of interest because some academics but practically maybe not so much relevant what is up what however is a consequence of what also for pizza already said dami there is a very close connection to Optics and Optics allow more or less these things to be directly implemented enabled us to also develop on the site a software tool which basically takes the language of category theory for modeling games and turns it into a software framework that you can use that supports your modeling process and that's the key thing because if you would be forced to doing things on pen and paper well yeah would not be that practical once you have this Tooling in the back then you can actually leverage um the basically the benefits of compositionality and the purpose of that basically second part is hopefully to convince you that at least this might be interesting and hopefully more that this might be really useful okay so a large chunk of the talk will also focus on the implementation so what does the implementation actually provide um first and foremost it's just a framework in which you can express and represent strategic interactions like the prison dilemma but obviously also more complicated stuff many times you're not only interested in representing models but you naturally are interested in you know what kind of behavior may result from these models so you want to you also want to analyze them in various ways in the current engine there are basically three ways to do that one is interactively so you basically run a session and then you can query um your model let's say I'm looking at a stake staking protocol and I have some idea what would constitute an honest strategy of the participants and then I can ask okay if I'm feeding in a strategy this is actually an equilibrium or do specifications have an incentive to deviate and the way it works is a bit like a proof assistant it will tell you you know your proposition that these strategies make sense either makes sense and then it's good or it will they will the compiler or the engine will tell you wait at least one agent basically has an incentive to deviate and here's the incentive here's a specific action that this player can take um now the interactive part is very useful to explore parts of the model and for the staking stuff we will also see an extended example on this it's quite useful to think about specific vectors of attack and then you can verify does this actually work or you know what two specific agents actually react to If a strategy of another player changes you can also think about this for pizza alluded to that um that there is a system a which is somehow represented as an open game or several open games you make changes in that system these changes propagate in your open games and then in the back you're running tests on what kind of behavior would you expect from this kind of system yeah so it might be that you have an incentive mechanism and it works but you make a change to the overall protocol a how does that actually is then this is translated into the open games framework and in the back you're running tests on the behavior of the agents and then maybe things go through or you get a warning something is not working anymore as before and lastly theoretically as well as from a practical implementation perspective there's a very close connection to machine learning framework specifically reinforcement learning I will say a bit more at the end if I have time but the idea basically is that you can either leverage reinforcement learning techniques and machine learning techniques more generally for solving and analyzing games solving of course has limitations because it's very complex but for some specific games it's feasible and on the other hand you can also turn it around you can also make Learners basically part of the game so that you have an interactive interaction of learning agents basically which is also quite useful because you basically have to think about this as you know institutional players um updating or actually um Learners themselves as part of the um of the model for instance in pricing settings okay um what's the key Innovation well compositionality obviously that's a key point but what does it actually mean here if you think about the prisoner dilemma what is already showed um is that you can think about the prison dilemma at least from what you have seen so far as either one monolithic building block or at the minimum you're splitting it up in three components right now for a prisoner dilemma that's not that relevant but the more complex your scenarios become the more helpful it actually is to say look I'm taking that part I'm zooming in I'm modeling it zoom out take another part model that zoom out and so on and so on and later on if you do it right you have basically systematic ways of composing these things together into a bigger model now this doesn't end at that level you can also for programming purposes or because of convenience you can further um modernize your code let's say there is a specific thing a specific way you want to approach it you can split this up implement it in different ways and the key thing about all of this basically so far is that all what you're doing will be guaranteed to make game theoretic sense if you follow basically the syntactic descriptions or restrict restrictions of the engine that means you start out modeling if you use our language you end up you can decompose things each of these components will make sense from a gametheory perspective and the composed thing will also make game Authority sense that's compositionality at action why is this useful well you get an overall few on the over on the on your situation that you want to model and it is sound and you can ask questions like okay what's equilibrium of that or you know if we repeat it um a Serial deviation strategy if you think about more um like a Markov strategy for instance other ways of um deviating that a profitable profitable for specific players another perspective basically is that this turns the pro the modeling exercise into a programming exercise so the idea of zooming in and zooming out I'm sorry and you know modeling Parts in isolation is more or less just like divide and conquer a typical pattern that you would apply in any kind of or many programming um problems okay and the key thing again is you can modulize your code further we will see this later on we will you know we will have regular High School functions that we just lived into that and you can change these components but as long as you're staying inside of that system you are guaranteed that these things make um are kind of well-defined no warning uh the fact that is uh this is game 3D well designed well well defined does of course not mean that your model makes sense you can come you know you can model complete garbage um we can't help you with that if you're you know really intended to do that but what we can guarantee to you is or what this kind of helps you is at least in the process of modeling we have a scaffold that you can use all right so how is this useful um the main thing basically is I alluded to that if you have you know if you can apply divide and conquer you can easily deal with complex scenarios um it overall also speeds up the process of modeling in several ways first you know division of labor so in principle the larger the systems you can actually very easily collaborate with people um secondly if you want to change a component you can easily do that as long as the rest stays intact and lastly because everything is expressed as code there is obvious reuse for components and you know we have been said we have had several projects in the past and we can see that there are some patterns that just emerge that you can use over and over again which is useful because it speeds up um down the road how um you know and you want to model something foreign you can also think about it as just being part of a larger stack where um it's just feeling a proper it's fulfilling a certain um service um like testing properties again on your on the safeness of the system from an economic perspective okay this is kind of the introduction very roughly what this engine is doing why it's possibly useful why it's maybe interesting what I want to do for the rest of this Workshop um and for basically the second part I will give you an intuition about how to model with this tool how to represent games and again the focus will be on showing that compositionality is actually useful or hopefully useful um secondly I will also give you an intuition of you know how does an analysis actually work what does it look like I will be shorter on that second part the reason is in order to make sense of the analysis you obviously have to have a deep understanding of the model um this is given the type constraints not really feasible but I still will give you an intuition of how does it actually work how does this look like okay and a leading example um that we will converge to is basically a staking protocol it's a simplified model that illustrates um these two components of compositionality and also the kind of analysis you want to run in this in this system good I start with not code but directly coming back to what for pizza actually namely um introducing a bit Theory this will be partly repetition but it doesn't hurt it will be mostly about diagrams so not much mathematical content the reason I do this is the theoretical approach is more or less directly the way that implementation works model is some kind of difficulties in the back obviously if you understand how the modeling on the theoretical side works you basically have a very good idea of how then the syntax actually works and operates and that means you also basically know how to use that that um that engine basically okay so you've seen this this is a bi-directional information transformation Transformer from both sides so X is transformed into Y and then there's something coming from R to S both directions again convention is if you want to think about this is that time is from time is on the left so on the side of X and S and the future is basically the passes on the X side and the future is on the Y side okay now in some sense in the essence of compositional game theory is that what we showed is any kind of game that you want to model has this shape and can be put into this shape whether it's just a single player making a decision which is kind of a non-typical game or a very large complex system many players moving and interacting everything can be modeled in that shape whether it's very large or very small now why is this good or why is this useful well it's useful because you can start out with small components like one player maybe just also computation something very trivial and you can plug these things together and slowly from the bottom up yeah like Lego blocks you can build up a system that is quite quite complex and of course because you're programming you can also kind of box things and say well this is a pattern maybe two players interacting in a certain way this is quite useful you know I'm giving that a name and I'm going to be reusing that component over again okay so everything is of that shape you know so it's a bit like it's like a closer closure property in some sense you start out with a number you add a number you end up with a number the same here you started with one game compose another game you end up in another game and this is in some sense what I referred to before as this guarantees you that you stay in a formerly well defined framework okay let me come back a bit to the concrete Implement concrete interpretation of this specific box and for the next few minutes think about this box as just one player doing something now one way to think about this is essentially the player is just doing some kind of information transformation right so there is something coming from the past a move information whatever X the player observes this and internally something happens he's outputting a move why okay now the question of course is what kind of move will a player make this depends on what what kind of moves he has available but it also of course if it is a game theoretic agent Let Me Assume for now it's a rational agent who wants to maximize something he needs to think about what's my effect of choosing wire on my utility and you see that the wire is an open wire so it doesn't really specify exactly how it is interacting yet within my with the environment but what we can say is the player is expecting an R back from the environment and this openness between my action Y and the payoff data or whatever actually are is in fact what I receive from the environment that openness makes it possible to take it like a building block put it in specific situations and then sometimes I might be able to close the loop um in a certain way the most trivial way of closing it would be I have one player and I'm just bending the Y back into R and then basically my why my action that I take will be directly to think that I observe and I affect I have full control basically most interesting scenarios from a game theory perspective are obviously not like that but my why will not solely determine what my payoff actually is like in a prison dilemma there's another agent doing something and this will also affect my payoff and of course this is the idea that at some point we will give a concrete environment which determines how this y actually spent back into a specific payoff whatever or whatever result you actually care about as an agent okay so that's the basic structure now I said before we are building up from the bottom what we want is we want to compose larger games by composing simpler games and what we need for this are essentially two kind of things we want some building blocks think a bit you know again like Lego um you have one specific thing and from that if you have it and you have more of them you can just build up a wall for instance so we need the building blocks the atomic units if you like and then we need operations how to compose stuff on the buildings on the atomic building blocks we have essentially two which is a decision a single player making a decision and the computation computation means just some input is observed some output is basically the result um these these computations can have side effects so it could be um actually a deterministic input is turned into a probability distribution or a probability probability distribution as an input is turned into another probability distribution good what are the composition operations for those of you who already followed for pizza you will already guess it it's parallel and sequential composition um parallel in the game 360 is maybe more easier interpreted as simultaneous and what this looks like essentially is again repeating a bit of what we have seen you have two games do you want a G2 if they are in parallel you can compose them and then they again will have this basic shape of input X cross the X2 X2 in that case turned into a certain output and it's the same time expecting a certain result and sending some information back into the past okay sequential composition we have G first H following you can stack them on each other so that they look in the following way now what is important so far I haven't said anything about what these labels x y and actually correspond to um you can think about them as shapes and only games that actually have the right shape can be stacked on each other and this is important because you know if I say you know give me two games and I can compose them you might wonder that sounds weird how can this be possible in generality right I can easily come up with two games that are not so easy to or maybe not at all composable the Restriction that you have is that these shapes the labels here actually have to match up only then can you stack games together forbidity already set from a categorical perspective and then of course also from the programming perspectives perspective these labels will be types so only if the types match up can you actually stack games together this is quite useful um and it's actually an important restriction because you know if let's say G is outputting a Boolean and H is expecting a numerical value a numerical type you can't match them up basically right what is even more important if you try to do that the engine in that case the Hustler compiler will loudly complain that this is not feasible you can't do that what is more because you can't obviously design your own types you have also degrees of freedom of you know being very specific about what kind of input type is actually expected yeah so it's basically also part of the modeling effort that you can you have control over um how easy is it actually to um stack these things okay and full circle back to the prisoner dilemma again I already alluded to it just very briefly what is this actually representing um two compositions first parallel or simultaneous between P1 and P2 and then sequential um the U and again if you go back to the parallel composition you can basically think I'm first composing the two players in parallel into again this shape and then I'm composing that one sequentially with the utility function of the payoff function okay questions so far can you explain why the utility function is applied sequentially um yes in a sense of the the utility function essentially is just a computation right so it's waiting there for you and it's waiting for two actions One Way player one and remember player two so it has to wait until these action these actions realize in that sense it's sequential in the implementation that I that I show you will decide this directly as variable output of P1 being fed into the U okay other questions okay um implementation first a bit of an overview so what is actually what does the implementation actually look like it's uh the main specific language embedded in Haskell uh you might wonder why Haskell um one of the reasons is that and repeats are already status as well as well the Optics and lenses are something that exist and you can build implementation basically on pre-existing structures in Hesco which is nice because um your theory has a direct correspondence to the elements that you use for the implementation in other words it makes it also easier to control that your implementation actually is correct okay another thing which is quite useful the typing system of Haskell is um actually um can be well sometimes your enemy but sometimes also your friend if you have larger components larger operations and you wonder what inputs if you want to query games do I actually have to supply the type system is quite useful because it can it infers the types and they can tell you your strategy that you have to supply has the following type right it has it's a tuple of double pool or maybe something much more complicated this sounds at the beginning kind of bit you know why are you in beneath yet why would you need that but the more complex your scenarios are the more useful these properties and these this functionality actually is okay this is under active development it's under the active development from two sides from the programming perspective of things we you know we feel like features that we want and we want to implement but also the theory is continuously developed right this is something I will come back to um at the end if I have time okay we are using it for a couple of things um staking protocols an example a simple example you will see today token design and there are also applications outside of crypto good the first thing we want to focus on how does the engine actually work in the sense of how do we represent games how does this work all right so on the left you can see again the the game with the inputs and outputs on the right hand right hand side you basically see the syntactic expression um which is basically this square bracket open game and then what follows until the the last square bracket that internally is basically the DSL and telling here is a game coming with a certain shape okay um there is what is called internals of G between the dashed lines I will say something about this in a minute first what you should see is there are four Fields inputs feedback output returns and they exactly correspond to the wires so you can see this as basically a way of expressing a two-dimensional element kind of language into on the the language or the the programming syntax in within Haskell so the inputs are just the outside system another way to think about this box essentially is each open game is almost like an interface right you have something internally happen but to the outside world is somehow it is um connected or maybe not connected through its interface that it offers what happens internally internally is where the place of credit information is generated so insights of these dashed lines there are what we call line blocks these are five lines basically there could be many of them um they roughly correspond again or mirror the outside wires so inputs feedback output returns and then there is an additional field which is the operation field that is essentially where information is created now the first thing to observe is in a simplest game if I'm just talking about one single player making a decision the input X could be exactly linked to the outside wire X that I showed you before and it's the wire going out or actually coming in similarly the output y um is will be the result of the information that is created and will be directly pushed outside of the box however this is not this is not necessarily the case in the sense of there could be more line blocks there could be more complicated things and some of these inputs and output fields and so on could be just totally consumed inside of that game without any exposure to the outside world okay the operation can be two things like here this is the dependent decision just means this is a decision operation so one player makes a decision or alternatively a computation these two building blocks either you don't need more if you have that you can basically build the most complicated model you want okay here's the prisoner dilemma um again the diagram from before first you can see um if you look at the left hand side the outside Fields the outside interfaces here are empty this tells you two things first you don't always need to supply information sometimes the games don't have are not connected to the outside world or only partly connected and internally what you can see is um there are three line blocks the first one the second one and the first and the second basically are player one and player two again for both of them they don't observe anything from the past there is no input the output something which is the decision player one and decision Player Two And they also need something from the environment back this is the payoff player one payoff player 2 which are only defined at the third line block which is the payoffs PD this is the utility function and here coming back to connecting to your question before the form this function is expecting basically an input from above which tells you this is a sequential um a sequential composition right keep in mind the diagrammatic language is two-dimensional hassle is not okay now the last element the pair of SPD is also outputting the payoffs and these payouts are then connected back to the the players and you can see already um you know certain elements of has to also help because the order of where these things are actually don't matter and it helps in the evaluation later yeah okay questions so far is the center roughly clear at least area so so yeah you have a question I want to ask about oh thank you I wanted to ask about the inputs and feedback before and after the uh internal definitions like like are those the inputs going into P1 you mean outside of sorry on this slide yeah yes so the first inputs and feedback the ones that have a blank um this okay I should have feel precise thanks for the pointer so um what is actually the inputs would correspond to an ingoing wire into the overall game um I could think about the overall game as a box itself right so this this is just one box with possible in-going in-going and outgoing wires what it essentially represents is an empty not an empty box but a box which is not connected at all to the outside world right okay I'm cutting just away four of these wires and um why is this relevant actually if you think about a prisoner dilemma a One-Shot game it has no past and it has also no future right it's one shot by definition there is no need to send information back or send information into the future and topologically I can kind of represent these features in a sense that there are wires or they are not wires it's also useful in the sense that you know if you model more complex games you can see that only when there is a connection through a wire there is actually an effect happening so sometimes these diagrams can be extremely helpful in kind of understanding what actually dependencies for sure thank you okay other questions okay so in the last part I want to look at a staking model this is you know a simple model still in the sense that I can most mostly explain all the components that are needed in the in the scope of the workshop the motivation comes actually have said that part of the engine um we're kind of funded by the ethereum foundation and we were working with the robust incentive group that was one of the examples they prompted us to work on um and that's basically what we did so this is this is a simplified version of that of that work I will focus on compositionality we can guess it already um specifically now I want what I want to show is how I'm basically not composing things but I first will actually decompose stuff I will look at the overall problem and I will put it in as small parts and bits as possible I want to also illustrate um what we sometimes refer to as a zooming in operation I said before all of the components are making game theoretic sense which means if I'm modeling something complicated I can when I want to obviously look at the overall complex thing and you know analyze this but sometimes I might not care about the overall thing but I might just care let's say the the validator is a mistaken protocol what are they actually doing for a specific input what I can do then is if I have the model as a specific component I can just zoom in look at this specific thing analyze this specific thing without regard of the rest it's a bit like unit testing of specific units if you like which can be extremely useful given time there are obviously more details that I can I cannot explain all the details behind it but this is explicitly based on a blog post that we wrote which gives much more context also on the relation to you know where the idea for the model comes from and also all of the components are explained in detail okay so what's the basic setup here we have essentially um several periods possibly in each period there is one proposal and there are two validators um what are they doing the proposal basically observes a chain I will say in a minute or give you a picture of how this actually looks like and the proposal basically observes their chain and then decides um yeah I want to extend the chain at the chain and basically says okay there are several blocks on which block am I actually building again it's simplified and what are the validators doing the validators basically observe the Delta between what was the chain before and what was um basically the result after the proposal moved and then they can make it they have to make a decision on a voting decision on what do they think is the legitimate head of that chain and legitimate obviously in the sense if they are trying to be honest and are not malicious okay so this would be one example of how this looks like what is the underlying data type um it has we'll be using Haskell obviously in Haskell this will be what is called an algebraic graph it's just a simple graph here um each block has two information namely an ID and then votes in that specific example here this would be kind of the ideal world we started with I'm block one built on on that block two and so on have a linear chain the votes are in everything looks fine okay now if you take that as a specific input for one period let's say this system you know now is period four coming what will be the action of The Proposal The Proposal will basically um say yeah I want to build on that chain I'm choosing in that case I'm choosing um ID3 which is the legitimate hat according to the protocol that we are interested in at that moment he makes the decision that block gets appended but there are no no votes yet and then the validators come in they observe the ID which was proposed and then they can cast their vote and in this case here they will do everything is very nice yeah this is the this is a really nice World here okay um however sometimes things are not so easy um specifically if uh if you know everything would be deterministic then obviously all the problems will go away but you have networks issue in reality which means the staking Protocols are hard you have to think about certain problems one of the problems could be that um what if there is time lag between the proposal and the tester and what happens if this is an example here there was a proposal in period four and he's actually malicious he's just letting time pass by at some point proposal from The Next Period observes the chain thinks okay the other guy hasn't done anything I'm building on the chain and legitimately you know he's honest Builds on ID3 and that moment before the validators come in I said the first the four proposal from period four actually sneaks in and places in all his own his own um block on that check so it's basically and now the question is what happens this is one of the motivating examples okay do you have questions to the basic setup more details to follow okay um if not let me jump to um that's not really looking nice okay can you read this should I increase the fund is it okay okay um left hand side is basically the model right hand side will be just an interactive session that I will be using um let me start with something first um in order to implement the model you need a lot of background information right I need to actually think about what's the data type of the chain if there is a new block being proposed how do I actually edit um this for instance this function here at the chain um it's just observing a chain it's observing an ID which was proposed and it's you know creating a new chain so I lead them I need a lot of background stuff in order to make this model work which is just basically you know Haskell in that sense Haskell functions and computations another one would be for instance determine head I'm clearly in order for the protocol to work which has a certain goal um I need to be able to at each point say what are the hat or the heads if they are non-determinate and this is basically the second function what it's doing and there's a lot of other stuff that I'm not showing you um that comes in so you need for that in order to kind of use this you need first this um the structure in order to basically I'll say that this is the computational background to which I'm working now you might wonder okay for you know it wouldn't it be nice if this would be coming from the outside world and indeed for some problems you just need to create it but in other cases and this is something we'll be working with in the future or towards is can part of that basic infrastructure that we are interfacing with in the end and that is actually not that interesting from your modeling perspective it's just something you want to take as given can you somehow import it from the outside world or can you connect this tooling to the outside world okay for this purpose here I'm just recreating it um what it actually does is not so important just think about it for now what the behavior is um of air chain and so on and so some functionality I will explain on the Fly good these are all functions the first thing we want to do we want to create basic building blocks that we'll be relying on yeah I said before we'll be making it here really really kind of I'm fine-grained in a sense we start at the real bottom of let's make add to chain actually an open gate put it into a computational framework so that we have a building block that we can move around if we want to similarly let's do that for determined head maybe we needed a different points um and then we kind of have this billing clock available as an open day also note essentially for the whole system here the protocol logic is exclusively in determined head this is this function that you can see here if you change that all the rest stays intact and that's another way of if you make it you know if you try to approach the problem in that way you will save a lot of redoing um if you want to make changes to the protocol okay um let me jump here foreign okay so I showed you the the function before um let me actually put it next to each other so add to Adblock basically is doing nothing else it's just a computation um it observes the chain old and observes an ID and then it you know puts that into the inputs field inside and it's basically this is the forward function keyword remember we had the decision and basically computation this is one instance of the computation and then it does just the add chain to weight which is uh similar to what we have on the attitude chain by the way I can explain in a minute yeah but it's the same in principle it's the same idea you just take a component plug it in and lift it into an open gate it's just a computation similarly determine head of the chain um here as you can see this input here um is basically just a function from the right hand side I'm lifting it into an open game just a building block good these are very boring building blocks so let's move on what do I need I have proposer and I have validators so what makes probably sense is to think about how does the validator actually look like okay let's model the validator um if you think about what a validator is doing I said before the action he does is he observes the new chain he observes the Delta which means he also has an access to the oil chain that's the input here um that's also the input the line element here and then there is a decision and what you can see here in that expression is just basically that's telling internally the dependent decision operator what is the action space the where Cutters they actually can choose from um here this is basically just because we start the IDS of the of the blocks from one until the vertex count basically how many vertex are there and then this is basically the choice that the validator can do okay so we have basically a bit of computational background adds adds a block we have the determined head of chain we have the validator um now we have the proposer okay what is the proposal doing well the proposal observes the chain also internally he makes a decision um what decision does it do well you can choose basically on which block to build that is the outset this is the decision proposer which is coming out here and then you can see this is the first game in that in that context where we have another line block there's some kind of additional functionality this is just basically producing the new chain this is taking two graphs this is as I said this is a specific library from Haskell which is algebraic you can just plug things together and you get the new the new chain and the output so the wiring of that game is basically chain old and chain new this is my interface of what the proposer is doing okay now the thing um I cheated you a bit um on two places maybe already spotted it if you look at for the validator as well as the proposer if you look at the return type here a return field I'm returning a constant zero which is kind of weird right because I said before isn't that where actually the Strategic context come from the environment telling me what to do blah blah blah blah and now it's just saying it's zero it doesn't look really strategic now this is an instance and I will come back to this this is an instance of where we actually had exactly what I just blah blah namely we had the inputs coming from the outside world and blocked them through but then realized that there is actually a very neat useful pattern here that we can abstract out and make it much easier to compose later on the payoffs in a different way yeah this is in some sense a bit of Haskell background that made it possible to kind of split this up even further that is what I meant initially when I said when you start modeling in this chain you can of course sometimes realize just programming patterns drastically abstract them out and replace them with something else why is this actually happening in a sense keep in mind for the protocol to work in Period T the decisions of proposal as well as validators are not rewarded they are only rewarded in the future that means their reward actually is conditioning on what is coming from the future and this is a way and I will show you in a minute how we actually can deal with this and the same is true for the validator as well as the proposal okay so here's an example um of what you can see here but basically how this is done this is what is called up update payoff validator this is an auxiliary thing it's taking in a boom the bull is basically was the validation correct according to the protocol that is then determining the payoff um payoff can also be negative so if the pro and basically the protocol determines what this validator did actually in t in t plus one doesn't actually look good so we will punish it could be a negative value okay that value is feed forward and then there's this add payoffs construction this is just another open game and what internally is happening internally this is associating the payoff to the player which is parameterized spending so you can you can put this component in different places and it will automatically add the payoff at that point to your player do you have to do it in that form no I said before you could also kind of make it more with the wires and so on but this is a pattern which makes it extremely lightweight of recomposing the pairs and again this is useful for the following reason if you think about and for here I'm assuming the payoffs are evaluated just in one period advanced a proposal do something the validators do something and then in the next period it gets evaluated what they actually do of course I could have a protocol which actually takes more more episodes what do I do then I can of course kind of take the wires put them through which is still okay but I can also just use it and say well the information Flows In Direction and I can compose this value at payoffs with the same name with the same identifier again at that point and I'm done it's not something we planned for but it's just something which emerged out of working on this and there are other examples like this okay these are the components that we need um now we want to take the next step first I'll be awesome we have not only one validator but we have several what we do here we are grouping them together right so we say well there's a chain U chain old input and then there is some kind of information this is just information about past behavior from the other validators from the period before and then the thing is what this should observe is the following here and here validator this is the construct which is on the right hand side so we take that and block in the open game here and this is basically the second step of nesting we already have one for the proposal but for the validator basically we bottle it as an open game and then we plug it into the group and now you can also see um the the structure basically of that component validator's group decision is made that you can also extend the number of players if you want you just basically add one line here add functionality but the overall interfacing of that group of decision making process is the same whether it's 100 or just two and there are also ways I should say this you don't always have to make this explicit if they are symmetric in some sense there's also convenience patterns such as you can say here 10 players of the same type put them there good so this is the validated group decision we also need to make the payment for the validators again it's not only one validated but two and again you could think about this as being extended to more players the thing to keep in mind um is again is um and I repeat myself but it's important this validation step is in time t for the behavior of T minus one yes you have a question okay maybe you ask a question again and everyone yeah he was asking uh I'd like to know what's operation the operation field basically the operation field okay the operation field is from one perspective basically what the where the the um strategic information is created if it's a function it will be just saying um let me give you the example here I'm filling the operation with basically two keywords namely either um forward function or depend decision yeah what is the forward function doing it's just lifting a normal function a normal Haskell function into an open gain which means in the simplest case it's just a deterministic function that determined head takes a chain and outputs ahead and then I'm interfacing it with the outside world if you're talking about a decision it's different look at the validator this is the keyword dependent decision the validator in this case the decision is the following the player observes this chain U chain old that this observation is information and then he makes a move he has to pick an element and this element in that case is an index to which of the block elements do I believe to be the head or I'm choosing to be the head yeah okay then there'll be an operation between returns and feedback sorry second like so so this is doing the like from left to right yeah movement correct and what about the other direction okay that's a good point so first let's take one step back um if you think about the prisoner dilemma there was also the case where the agents did not send information back into the past yeah okay so that explains and the reasoning is simply here I don't need to send the information from these players back into the past and the reason I don't need to do that is um there's basically the protocol is moving forward and I don't need to send this information back it's like I'm creating a state and the state will summarize what is going on why I'm doing this in this form is the following the following reason I will end up with one episode that episode will be basically a basic game for Markov game and then I can stack these again on it on each other and repeat them if I want to now you are right if you wanted let's say you you're just explicitly wanted to model two episodes you could say um parts of these elements for instance what these guys expect here what the return is is actually coming from this returns field over here and I said before you can do that the reason I'm not doing it is here is exactly for if I want to Stack more more episodes with payoff still being created for players in let's say T minus four I can easier do that okay maybe it will become clearer when we come to the rest if not you know feel free to ask again other questions could you tell me the time yeah 25 okay good okay well it is payments um again this looks like a bit more you know convenient stuff but this is a I mean the question we should ask if you model it yourself is how can you how can you model it in a way that it's actually really a building block um I said before one way of doing it is that the interfaces are relatively flexible so I'm just leading the fee which is an outside outside parameter um and then internally basically I just need the payoffs I need to chain new and the hat ID which was chosen and with that basically I have the full picture and that the protocol can evaluate once the behavior actually correct okay and you can see this is actually happening in a function that I didn't show you this is a tested correct they tested correct is basically just telling according to the logic of the of on the protocol the information I got yes made sense or no and it's outputting a pool it's just saying yes or no and it's doing that for player one and it's doing it for player two and these then corrected a tests that are basically input into this function pay or validator here on the right which you can also see here it's just taking was the validator correct or not and then it's basically updating good okay also what you should see and this is kind of coming back to this discussion on why is there no information being sent back this is also um there's also no information sent in the future right if I would be doing this again without my way of composing this one player which just magically updates I would have to explicitly feedback that information uh so here you have uh potentially Boolean values that are that that um the outputs which is the correct attested one and two uh but then in a different block you had an input and output that was actually called boo so I'm a little confused whether uh that's this is supposed to be like a label or a type um okay this is basically the question of the scope of the of the um of the environment basically so the reason I call this rule here is I'm just telling now basically me for the reader I know this is a pool and I basically know what is happening why am I doing this here differently I'm doing the correct to test it because I'm giving it information that I can easier pass it right if I would be just saying Bull in that specific context I might know what it is but I don't know where the bull is coming from right so it's it's like you might disagree with my um basically with my nominator or with the way I I label things but for me internally it was just like I understand what it actually means and that's the reason basically yeah the thing to keep in mind in a categorical framework because you have these wires going in basically bound variables come in um the outgoing wires are basically binding new variables to the output right so in case of the correct the test that I'm binding a value that is the outcome of that operation to that specific um character test which means if I'm reusing it it's mounted okay other questions all right let's continue so we have to validate us payment and now we have everything assembled for a one period game one episode game okay this is this Beast here just barely makes it on not completely what it basically tells you is this is one episode I'm now pulling everything together there are certain parametrizations ignore them for now they're just details um of you know how do I call the players what is the reward and what is the fee and so on you should really think about it again as an as a diagram with in-going and outgoing wires so the in-going wires are basically chain old head of chain from the period -2 um validators map this is just basically summarizing the information of what the validators have done before and in principle you should think about this I keep enough information so that the protocol Works in a simple case here just one episode if there would be more episodes this would be it's just a record type basically it would contain more records okay um what we then have basically is the proposal moves first he observes the chain he outputs a new chain keep in mind this is this again so he's observing the chain and then internally is also at the same time creating the new chain this is a computation taking place here okay proposal Moves new chain is created then the validators move as a group they observe the new chain they observed the old chain there's also access to the old information validator smash validators hashmap old and then they make a decision they create new this is basically new map containing the updated information how did all of these validators actually behave and they also have the chain updated because when they cast their votes remember the shape of the of um the blocks are basically an ID and a voting value all right the thing to remember and I'm repeating myself I know but it's important to understand what is happening that the payments basically that happen are happening not for the decisions to that are made by the players in that episode but from the episode before or if I would be looking at them more longer Horizon from the episodes before good after this this is the main things the decisions are made by the proposal by the validators now I'm basically during bookkeeping um I'm determining the head of the chain I do the validators payment this is from the past I also check I didn't explain this but this is basically also bookkeeping I'll just look at what was the old proposal actually doing did he actually do something and then I'm getting that as an input to the proposal payment again for the period before now the complicating thing here is that I'm targeting a model which itself has a structure that if you just look at the output chain new updated head of chain and so on validators hashmap and you look above you can see there's a pattern basically the input types here chain old head of I mean you can't see that but I'm telling you the input type Jane old head of chain and that here are exactly the output types which means I now I can take the one episode and just say okay maybe I want to run it for three episodes I'm taking the same element and I'm just connecting them or I'm not doing that here if I want to run this as a Markov game and you know I want to approximate it like I'm running this for a long time I could just basically use a specific operator we developed that you can embed the stage game and then I'm repeating it yeah so you're starting you're initializing the game you create a one-stage output that is fed back into the next period And so you go on thank you okay I'm not doing that here um I want to jump for the last part basically a bit and looking into how do you actually analyze these games I mentioned before on the slide what I want to do is I want to um illustrate a bit of what is the zooming actually what is the zooming how does the zooming work and you can already see because I'm focusing on the one episode I'm actually ignoring any kind of repetition clearly if you care about the overall protocol at some point you have to think about the Dynamics and also longer time period periods but for some questions it might be relevant to see um is it actually working locally to give you an example suppose you're interested in honest Behavior by proposal as well as validator and I'm giving you you know I'm initially initializing this with specific inputs and I'm testing in that one period do the players actually have an incentive to work in that way and if not if you find out basically just by zooming in on that context it's not well the info can you just can put everything else aside you don't have to think about the Dynamics that's enough similarly if you care about let's say vectors of attacks very often it's enough to focus on specific Parts in order to evaluate whether the attack is actually working or not question no yes maybe okay I said um in the context of like uh you know modeling like the domain of like a game and you know like a software team working with like a program like this you know if they have to Liaison with like the product team which will have an understanding of like the ux wouldn't it be easier for them if they want to model attack vectors to just model what the agents could do and then use a genetic algorithm for example might well be depends on the context right um the key thing is here you can have you have both basically The Best of Both Worlds you can just look at the one component but if that is not the only query you want to do but you also want to look at the more complicated stuff you have it as well right so nothing I mean in principle what you could do is actually you can take this component interface it to the outside world runs a learning algorithm on top and that's it and it would be exactly the same thing but it will be part of the overall consistent framework and that's an important thing if you care about the design for instance you want to make sure that everything is somehow consistent obviously right and then it's much easier to say I'm taking an element which is consistent with the rest and just interface it to the outside world and then simulate it clearly I mean you know this is also ethical I'm not sure how many people will be using it in that form right that's another question that is I think lurking in the yeah in the back so there are I mean this is at the moment actually to work with that you don't need that much high school because you need to understand the syntax of the engine and most of what I showed you is inside clearly you need some kind of knowledge of Haskell to work with the outside world but if that also goes away it's easy to think of this as basically working as you have a domain specific language and that's all you need to know and you have some operators on top then parts of the pain hopefully go away okay other questions all right if not slide one shall we start again maybe maybe afterwards okay um let's jump a bit into the um analysis um okay here's a bit more Haskell pain for you um and even more than average namely I'm using something which is um kind of what is called arrows uh if you don't even know what it is for now you just think about this as I'm defining a strategy for proposal as well as for the validator what is this basically doing is the following is creating a function and the function tells me I'm observing a chain and what you want me to do is I'm basically sending an ID remember the proposal observes the chain and decides on which which element to build what the rest is basically saying is this is an honest strategy it does the following determine head this is a functionality from before so I'm looking into the chain I'm looking at what is the what is the what is the head of the chain according to the protocol if it is play that game play that strategy if not if there are multiple candidates randomize this is happening here basically and this is done uniformly and the validator does exactly the same it's basically a super honest as well he's just looking at um what's the head if the hat is a single value play that if multiple values randomized among them good and then basically we kind of encapsulate everything in this so reminder this is basically um uh referring to the one episode game I'm plugging in some variables or some parameters which you can ignore for now and then what is the thing that I'm doing let me actually open it differently um so I'm analyzing the scenario and then this is I should have said this this is the interactive way this is the right hand side is an interactive session with the high school compiler I'm querying that thing and what I'm getting out basically is simplistic information namely um the output just tells me everything is fine um you don't have to worry go home or go to the pub everything is working now this is a specific thing what it actually tells you and in fact this is the protocol is inspired by you know by one of the biggest um by ethereum basically you can see that the specific assumption is working no incent no agent has an incentive to deviate okay nice and nice and clean so far but now we want to do the following now we want to come back to this picture here I said before that let's suppose in the past period there's a guy who's actually not so nice and he's deciding not to propose he's waiting at that moment at some point after some time threshold the next proposal which is um the lower one here basically observes the chain steps in he wants to be nice he's honest proposes a new a new head um and at that moment before the testers can actually be active the old proposal steps in and just basically proposes his own his own head of the chain okay there are various ways of doing this I could just model explicitly the attack game and it is actually Merit to do that but here's an alternative way you can do it and this is I'm referring to the zooming in that I want to illustrate foreign I've created another version here which is doing this one episode attack which is doing a simple trick namely I'm introducing an additional variable because I'm just focused on this one period I can do that it's easy I just add which is a chain manipulated um all the rest is the same the proposer observes the old change so he's basically still operating under the information from the past and then what happens is this line block is added I'm merging the two proposed heads into one chain so then I have really a fork and then what is happening the validators are observing the forked version so they have to deal with the problem basically right now is this the only way to do it no you have multiple ways of doing it but this is you know this is part of the what the model has to decide how can this be done in an easy and accessible way another way to another way to do this and on one branch we actually do this is explicitly keeping time of the um keeping track of time and basically look at the timing game right so that time passes and then the proposal from the first period can until a certain point act the problem is that until a certain threshold the all the other players don't know whether the other guy moved or just they haven't received a signal yet but this is much more involved here I'm just cutting into this thing and I'm just focusing on that one aspect that I care about namely what do the validators actually do foreign okay let's jump to this um attack okay um strategy proposal is the same then we have what I call the strategy validator random it's also the same from before I add two new strategies for validators one is strategy validator four and validator five this is something very um very simple namely in case of a tie when there are multiple things I'm just taking here by hand I'm just taking the fourth element and you know for that specific example I'm just specializing it for that specific thing because it's enough but you could also easily extend it to a more General version in other words when there are multiple candidates I'm just deterministically choosing one of the elements right and I'm doing the same for five but just on the other on the other element okay now I have several scenarios um I have scenario four and five which is just the same proposal strategy as before honest in the manipulator chain and then the validators are just deterministically both um voting for id4 in case of a type or alternatively five and lastly the random is basically I'm just taking the element so the honest behavior from before namely if there is a tie I'm just randomizing which obviously is also debatable whether this is a good idea but for illustration purposes that's enough okay let me run through four you can see this is nice this is also not nice this isn't this is an equilibrium and five as well okay so far this looks like pretty useless because everything is in equilibrium but in fact what it tells you is that suddenly we have two equilibrium at the same time and both are kind of either we go with the honors proposal and the one who proposed the four or we actually go with the five which tells you um this is not in the interest of the protocol this one of them should not be in equilibrium and you'll see even more if I'm sticking to the actual Behavior of introducing the possibility of random basically just honestly saying I don't know when I'm randomizing you can you get different information um and this is the alternative namely the system recognizes one of the agents has a deviation the formatting is horrible but um for basically focus on the first part the player with the name a21 has a deviating property it's optimal payoff is two current payoff is one what's the optimal action you just he should choose is move one why is this the case you can easily imagine because basically these players tried to coordinate and if they are diverging the protocol will punish them so they actually are better off voting for both coordinating on the wrong or the manipulated head of the chain instead of sticking to their honor strategy so at that moment you see Things Fall Apart because that's very very relatively simple model and again this kind of it's a simple illustration here but that kind of structure was actually motivation from a unrealistic attack good let me close with one more thing and this is then more or less the end with kind of some remarks this is the interactive version I said before you can also think about this as being part of a system so you can um um basically also run the testing in parallel or as an alternative so if you do this basically what will happen is you have some kind of specification test this includes the equilibrium but it can also be the parts you know is the staking protocol working in the right way um and then hesper is actually quite nice in that end because it can create a lot of very well structured arbitrary examples that you care about and then you will see at the end hopefully something green like this which generated in that case I think 100 different starting points for the chain evaluated them and you get some result yeah and can you can see this is basically you can you can extend this in all kinds of versions it can be either on the behavioral level really thinking about equilibrium that would be the first test or if you go down really just the components okay questions before I conclude let me conclude um on two levels first a bit more concretely what is the end of the next steps for this engine and then circling back to where we actually started so this is connected the rest of category Theory or maybe more precisely black category Theory so one of the things and some of actually formal verification people are here we are one project that we have is I mentioned this we want to have more pipeline from let's say starting from evm code into actual open games representation a lot of work has already been done that we can dock on and one project is basically to kind of extend this towards the open games framework so that if you can start with some um smart contracts you basically get an open games representation and then you can start querying them um either automatically or with your manual maybe you have some ideas of what you want to query in a manual in a manual way or you have some more bigger and analyst tools on top thank you uh you know the analytics we have so far we're extending them permanently we're also you know going into different applications and thinking about how they you know what specific analytics are relevant there um it's outside of staking and I should mention this before which is an actually important thing the engine itself the end the version that you see here is basically built on Theory version outdated time -3 or so there have been three more iterations and one of the tasks in the next weeks a month will be basically an update of the engine the theory itself is also continuously developed okay lastly compositionality that was the starting point you've seen one instance of why compositionality might be useful in the context of open games what is interesting about this specific example is that when we started um out there is this basic question that probably raised in the initial slide mean or in the initial beginning of his presentation then how the systems compose in the game theory are in the game City setting we have a relatively clear answer and what was interesting was in the beginning the implementation and the way we did it categorically is not at all doesn't resemble at all the way it looks right now because at the beginning we had a very different way what we realized actually is the connection to lenses in a categorical framework what we also realized um was actually realizing that the the existing deterministic lenses are not enough and this is quite obvious because games need Randomness right you need to deal with um non-deterministic moves that actually LED also to Innovations on the on the side of the um Optics implementation and that itself profits alluded to that is itself now kind of a you know in an area which is almost exploding in all kinds of directions and making connections and extending this framework this is one of the things which is quite nice actually about all of this work that it's tightly it's tying back into other fields within the categorical framework and examples of that are control theory reinforcement learning active inference others to be developed and the abstraction here really enables you to see that these patterns are or that these different instances are actually related to Common patterns and lastly what is more you can also make cross cross combinations one of the interesting ones is actually thinking about games and learning right which is not new itself but if you see it in that form and you have this new pattern it's quite info I find it quite insightful and quite useful actually to see it in that form good thank you very much [Applause] questions yeah or to me or to repeat soon maybe you wanna so I'm wondering if we can talk about like uh real world attack example and how that would um come into such a system and in particular I guess on my mind is the mango attack from a couple days ago where it was essentially an oracle exploit and the um it seems to me like an orca would be inherently outside of a system that you're modeling this way or is that is that an incorrect assumption um sorry let me go back go back here just if you think about no here if you think about this um X doesn't have to come from the in from the world it's from the game itself right it can be something from the outside perspective so I can interface this that system with something which is drawn from an outset could be from a database or whatever it actually is where it's coming from depending on how I deployed this it could be continuously updated and I'm running that basically on a permanent basis so this is this is clearly possible um you can also parameterize games um I'm not sure you maybe remember this part I just go there um if you look something like this one episode editor attack there are a couple of parameters which are actually exogenous they are not part of the internal structure I can make them endogenous querying them but I can also just say they're coming from the outside and I'm fixing them like the names of the players of feedbacks or sorry fees and Rewards uh can you establish bounds on those parameters um it depends on what you mean with bounce first of all keep in mind that I mean they're structured it because they have to be typed right so if they have the wrong time they will not will not work um then I mean what exactly do you mean by by bounds in the sense of values or so yeah I don't mean like a type bound I mean uh value bounce um well again I mean you have limitations in a sense if you're working with an escrow world you clearly have boundaries for certain types that you can use um there are also of course the question of the computational complexity at some point right um I haven't talked about this because this is also part of active research um so far I'm using compositionality exclusively on the level of composing the representation there are results that show that you know Computing equilibrium is very hard um and we will not break these results but in the practice of actually Computing concrete concrete games um you might be able to leverage also the compositionality right because some components here might be computed but it might be independent of that and then you can compute or um some compute some component here might compute but it will only affect another component another thing to keep in mind is that as Philip said um you can have that a game can you know just have a function as internals or it can have you know strategies so in the case of an oracle you can either treat it as a parameter that basically comes from the outside world or you can model it as a stupid function that has no agency whatsoever or you can model it as I don't know a protocol that has its own set of economic incentives to work in the right way I guess that would be the case of like the centralized oracles where you know people are incentivated to not to lie and whatever the cool thing about this is that then you can start from a scenario where the Oracle is honest the the very cool thing that practice teaches us is that usually when people design a protocol they have already an intuitive notion of what is the equilibrium where everyone is honest so you say okay you test that you have an equilibrium and now you can basically start bribing the Oracle so you can start basically you know adding incentives to the Oracle to lie and one thing that you can do very efficiently computationally is finding a bound that is basically the cost of breaking your equilibrium so say how much do I have to bribe the Oracle to break the equilibrium and then this is super useful because now you can find parameters and and you know since you are starting from equilibrium that you already knew you don't have to do equilibrium search it's just equilibrium checking you just like linearly increment this parameter and it's okay this is how much we are protected and and then yeah that that would be a sort of bound between your model how expensive would be to it up basically oh hi um I have a few questions because I've been really listening so intently and I've written some things down so it's okay um the first one was um you know could you perhaps optimize the compiler by modeling like modeling it with category Theory and with your tools oh sorry was that kind of hard to understand um could you perhaps Model A compiler and optimize a compiler using your tools and with category Theory okay um they're actually doing people doing this here uh I think at least at least trying but honestly this is definitely the outset of my expertise I can't say that you rechecked the research of uh these professors called dangika that is using category Theory to do compiler optimization uh so yeah that would be probably the closest thing okay and that's exactly where my knowledge of it and it's thanks um and then another question and I'm going to speed run it so nobody gets offended that we're taking a long time um could you model uh perhaps an iterated prisoners dilemma with a variable number of agents and rounds yeah beautiful very cool and um will you ever release uh like a function annotated sort of preprocessor language that's maybe syntax agnostic or something that you could add into other code bases that aren't quite High School based in the future maybe very cool okay thanks for coming