Ethereum Foundation DevCon 6 - Cryptoeconomics Track, 18 Oct 2022

Previous Meeting Next Meeting

⏯

youtube image

►

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

Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/compositionality-the-10x-engineer-secret-sauce/

Proponents of blockchains argue that compositionality is a key feature. What is compositionality though? Maybe surprisingly, there is a rich mathematical framework in which the concept can be made precise as a theory of systems. In this workshop, we provide a primer of that theory and we showcase two practical applications based on it: compositionality in game theory (open games) and in formal verification (automata). The workshop is aimed at devs. There are no mathematical prerequisites.

Speaker(s): Fabrizio Romano Genovese, Philipp Zahn
Track: Cryptoeconomics
Keywords: Compositionality,Applied Category Theory,Open Games

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

A

B

This will be a talk about compositionality.

B

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.

B

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.

B

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?

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

You have to specify morphisms that are the process, the boxes that transform objects into objects.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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?

B

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.

B

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.

C

It's like sorry.

B

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.

B

Your systems will be linear applications that respect the linearity of the vector space uh yeah.

D

B

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.

B

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.

B

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.

E

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

So the point is: how can we do that in a automated and, more importantly, compositional way?

B

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.

B

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.

B

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.

B

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.

B

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.

B

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?

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

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.

B

That's everything for me and I'll just pass it to Philip. Thank you.

B

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.

B

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.

B

Yeah there are various ways to do that. uh Philip is the expert in this and I don't know. Maybe you won't.

A

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

Basically, second part is hopefully to convince you that at least this might be interesting and hopefully more that this might be really useful.

F

Okay, so a large chunk of the talk will also focus on the implementation. So what does the implementation actually provide?

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

Okay, um what's the key Innovation? Well, compositionality. Obviously, that's a key point, but what does it actually mean here?

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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.

G

F

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.

F

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.

F

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.

F

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.

F

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.

F

Okay, questions so far,.

G

Can you explain why the utility function is applied? Sequentially.

F

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.

F

Okay, um implementation first, a bit of an overview.

F

So what is actually what does the implementation actually look like it's uh the main specific language embedded in Haskell.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

Okay, here's the prisoner dilemma um again, the diagram from before.

F

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.

F

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.

F

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.

F

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.

F

Okay, questions so far is the center roughly clear at least area. So so yeah, you have a question.

E

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.

F

Of sorry on this slide, yeah.

E

Yes, so the first inputs and feedback, the ones that have a blank.

F

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?

F

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.

F

So sometimes these diagrams can be extremely helpful in kind of understanding what actually dependencies for.

E

Sure, thank you. Okay,.

F

Other questions, okay,.

F

So in the last part, I want to look at a staking model.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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?

F

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?

F

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.

F

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.

F

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.

F

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.

F

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?

F

This is one of the motivating examples.

F

Okay, do you have questions to the basic setup, more details to follow? Okay,.

F

um If not, let me jump to.

F

um That's not really looking nice.

F

Okay, can you read this? Should I increase the fund? Is it okay.

F

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?

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

F

Let me jump here, foreign.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

Okay, now the thing um I cheated you a bit um on two places, maybe already spotted it.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

Okay, these are the components that we need. um Now we want to take the next step.

F

First, I'll be awesome.

F

We have not only one validator.

F

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.

F

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.

F

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.

F

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.

F

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.

F

Yes, you have a question.

E

F

Maybe you ask a question again and everyone yeah.

C

He was asking uh I'd like to know: what's operation the.

F

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.

F

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.

F

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,.

C

Then there'll be an operation between returns and feedback.

F

Sorry, second, like.

C

So so this is doing the like from left to right, yeah movement, correct, and what about the other direction? Okay,.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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.

G

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.

F

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.

F

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.

F

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.

F

To that specific um character test, which means, if I'm reusing it, it's mounted okay, other questions.

F

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.

F

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?

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

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?

F

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.

F

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.

F

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,.

D

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,.

F

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.

F

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.

F

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.

D

F

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.

F

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.

F

Okay, other questions.

F

All right, if not slide, one, shall we start again, maybe maybe afterwards.

F

Okay, um let's jump a bit into the um analysis.

F

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.

F

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?

F

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.

F

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.

F

um So I'm analyzing.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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?

F

Okay, let's jump to this.

F

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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.

F

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?

F

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.

F

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.

F

Okay, questions before I conclude.

F

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.

F

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.

F

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.

F

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.

F

The theory itself is also continuously developed.

F

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.

F

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.

F

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.

F

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.

F

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.

F

Thank you very much.

F

Questions yeah or to me or to repeat soon, maybe you wanna.

G

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.

F

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.

F

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.

F

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.

G

uh Can you establish bounds on those parameters.

F

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.

G

So yeah I don't mean, like a type bound, I mean uh value, bounce.

F

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.

F

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.

B

Another thing to keep in mind is that, as Philip said, um you can have that a game can you know just have.

A

A function as internals or it can have you know, strategies.

B

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.

A

Right way, I guess that would be the case of like the centralized oracles, where you know, people are incentivated to.

B

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.

B

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.

B

How expensive would be to it.

A

D

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.

D

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.

F

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.

B

You rechecked the research of uh these professors called dangika that is using category Theory to do compiler.

A

Optimization uh so yeah that would be probably the closest thing. Okay,.

D

A

That's exactly where my knowledge of it and.

D

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?

D

F

Very cool: okay, thanks for coming.