Ethereum Foundation DevCon 6 - Developer Infrastructure Track, 15 Oct 2022

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Symbolic Computation for Fun and for Profit by Hari | 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/symbolic-computation-for-fun-and-for-profit/

How symbolic computation in EVM / Solidity works, end-to-end. I'll try to give insights on problems that can be solved efficiently, forming constraints, relaxations, how to build custom solvers from scratch, and produce computer proofs. We'll be saving gas!

Speaker(s): Hari
Skill level: Intermediate
Track: Developer Infrastructure
Keywords: solidity,optimizor,smart-contracts

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

A

Yeah, so what he's saying is that this brand is not reachable, um for whatever reasons we're going to figure out how we will symbolically figure this out um and how we can use symbolic computation to find out this branch is unreachable.

A

So what is symbolic computation, symbolic computation is about representing properties using mathematical equations, and we use the solutions of these equations to reason about the properties we started with the property we wanted to know in. The previous example is that the reward is unreachable and we have to figure out a way to convert this solidity core into a mathematical equation and I want to give some hint about the climax, which is usually these systems having the system of equation, having a solution means that a property can be violated and on the other.

A

On the contrary, um if the system of equations don't have any solution, then it usually means that the property is always true. I mean this is not generally true, but most of the time. This is what you're trying to do, um and now we want to convert core into mathematical equations. How do we do that?

A

A

um So the question is: what do we encode? So we could encode solidity directly. We could encode Yule, which is an intermediate representation of solidity. It's a one level down from solidity. We could also encode evm, which is at the lowest level.

A

So solidity is a complex language and there's, let's maybe like skip encoding- that because there is like too many rules we have to handle evm, on the other hand, is like too simple and we have to extract a lot of information about the control flow and then code it so maybe Let's ignore solidity and evm for encoding and just deal with dual it's it's in the right middle ground. It's simple enough and it has enough information about the control flow.

A

So the most fundamental thing to encode would be a variable, and a variable in AVM is a 256 256 bit integer.

A

um Most of the time you represent variables as an element of integers um Z, as the notation, if possible, we add the constraints to roll less than or equal to X less than or equal to 2 raised to 256 minus 1..

A

um Now that we know how to encode a very simple variable, we need to figure out how to how to assign um values to the variables.

A

So here's, a very simple dual block with three variables x, y and z, x, is assigned the value 1 Y is a sign called that a lot 0 and Z is an expression in uh U, less than or less than x y.

A

So we want to represent each of this assignment by constraints for X and Y. It's pretty simple for X. You just have the equation x, equal to one for y. We have to just say y That's it it's a simple AVM variable. We can't we can't. We can't really like produce any extra constraints from collateral zero, because it can be anything so we just have to treat y as a regular, even variable um and with Z. We have to figure out a way to encode a less than of X Y.

A

uh We will deal with that later, uh but the big question is that: can we handle every assignment?

A

So here is a different Yule block where you assign the value 1 to X and there's a switch of statement which has a three different control flow branches. So, depending on the value of call that a lot zero, which we don't know what it is, we can assign um x, 2, 3 or 4..

A

So the question is: can we actually encode the switch? um This brings us to the notion of a single static assignment, um so these are variables that are only assigned once and working with. Ssa variables simplifies our analysis quite a bit. So here is an example of a different. You will block. You have two variables: X and Y gets a sign called that load 32 at the beginning and then reassign something else by definition, Y is not an SSA variable.

A

It's signed twice, but it's actually possible to transform the same, transform this block into another Yule block, where we introduce a new variable Z and all these variables are actually SSA variables. So, generally speaking, we only want to work with SS variables because they really simplify our analysis.

A

However, it's not always possible to do a yule to Jewel transformation. Such that all the variables are SSA there was the example of like two slides ago: uh the switch, the switch, uh the switch example.

A

You cannot encode X as an SSA variable purely in dual, but we can still get a lot done with just uh taking whatever is as I say, and maybe we have you know. We also have this step in the Dual Optimizer called the SSA transform that lets us transform fuel into what we call as a pseudo SSA format. So a lot of variables are SSA, but it's uh uh it's not not it's, not necessarily that that every variable is SSA.

A

So whenever we encounter a non-ssa variable during the analysis, we would replace it by a pre-variable. So a free variable is what we mentioned like uh two slides ago, uh sorry three slides ago, which is just uh the basic constraints that you can give to any variable in in the evm.

A

But there is this important caveat here that, okay, uh whenever we encounter a known as a variable, we have to replace it with a fresh variable, because the value may have been assigned something else during the two reads, but we can of course optimize this further, but this is what we'll do now so now, let's think about how do we encode some evm instructions, um so perhaps the most fundamental evm instruction is addition. You take two numbers and you know you add them and leave it at the stack.

A

So how do we symbolically represent uh the addition? You know X Plus y? um What do you think it's just? Is it just X Plus y? um Unfortunately, it's not that simple. So if you look at the evm semantics of addition, uh addition is defined by X Plus Y modulo 2 raised to 256., and if you look at high level solidity code since 080, we have the check arithmetic, so X, Plus y would revert, If X, Plus Y is greater than 2 raised to greater than or equal to, 2 is to 256..

A

So we are already seeing that it's not as simple. It's not that simple to encode add it's doable, but it's not the easiest, but perhaps here is like an easier set of instructions. Less than greater than and e0 here's a former former like um representation of these op codes.

A

um We Define when, when these values take one or zero um there are like, if for less than or a B, if a is less than b the value takes unless the off code gives one. In the other case, it gives zero uh almost the opposite for greater than um for s0. If the value is zero, then you get one answer otherwise, so let's uh decrease for a bit and talk about difference logic.

A

So, let's start with an example, so x, y and z are integer variables and let there be constraints, two of them x, minus y, less than or equal to four and x, minus Z, less than or equal to 3.. The question is: does the system have a solution? It does have a solution. You can just assign x, equal to 4 y equal to zero Z equal to one, and these two constraints are satisfied.

A

So to go to go back a bit. You can generalize this um a difference logic by saying, okay, you can have n number of variables X1 to X N that are integers and constraints of the form x. I minus x, j, less than or equal to a constant. But let's look at a different example. You add one more constraint here, which is z, minus X, less than or equal to minus eight, and the question is: does this have a solution now any any takers?

A

It actually doesn't have a solution, and how do we prove this so assume that there is a solution? Let's just add all the variables. So, let's out, let's add all the equations, so you add x, minus y plus one minus Z, Plus Z, minus X and the rhs is going to be four plus three minus 8 and the ls is going to be zero, so we arrive at something less than or equal to minus one, which is a contradiction.

A

So there is no solution.

A

Some graph Theory trick to do the same thing. So we try to encode each of this constraint using a graph.

A

Every variable is a naught in this graph, so you can see that x, y and z are three nodes and we assign some weights. These are the weights that come from the equation, so x, minus y is less than or equal to 4. That would be the weight of the X. Similarly, for the others, what's important is that it's a direct graph and the direction follows you know so in case of a minus B less than or equal to K uh the edges from B to a and has a weight of K.

A

So the important takeaway here is that if there is a negative cycle uh in our direct graph, then there are no Solutions uh to our problem. um You can see here you can see here. There is a negative cycle, so if you add up four plus three plus minus a that is negative one so that that's what we are looking for, so how do we find uh negative Cycles in a graph? So there is this very classical algorithm called the development Ford, which can tell you given a direct graph. Is there a?

A

Is there a negative cycle? You can also use it to find the shortest path between two um two nodes: that's the classical use case, but it can also tell you if there's a negative cycle- and it's a pro, it's surprisingly easy to implement. You can even implement this in solidity.

A

Leo has a repo where he implements the Bellman Ford and much more in completely in solidity, and he's going to have a talk tomorrow at 11 PM 11 am you can come for the talk for more details, and here is like some insight about unsatisfiability like unsatisfiability, is when uh the set of constraints have no Solutions um and a lot of times. We only encode like a very small set of like uh what we can actually encode, and we are very generous about like ignoring the constraints we can.

A

We can't solve, like I said already, uh we ignore like non-necessary variables. uh So as long as we only care about unsatisfiability, we can do this um and we can optimize and we can usually optimize when the constraints are unsatisfiable. Otherwise, we just leave the code unchanged.

A

um So we talked about difference logic, but what does it have to do with um all this? Like evm um opcodes, so it turns out that we can represent these three evm of codes using uh Expressions. That would match a difference logic so in case of less than of a b. So when the value is 1, it's only when a minus B is less than or equal to -1 and 0 when B minus a less than or equal to zero. So similarly, you can build these constraints for greater than and is zero.

A

So in the last example, zero is just a variable that we used to indicate at zero. There is some like Nuance here, but you could just treat zero as a variable here. So how do we encode yule so a lot of times? We want to know if the value of an expression is always zero or always non-zero.

A

So if you take this example of if of condition and then uh something going on in the if statement uh we can replace so the question we want to know is: if we can replace condition by zero or one inside the branch we can actually replace. We can add additional constraint that condition equal to true so to take a in particular.

A

If you look at less than F of less than x y, um we start by checking if adding the constraint X less than y, make the system unsatisfiable so in in reference logic, this is x, minus y, less than or equal to minus one. We just add it to our other set of constraints, and if the system is unsatisfiable, we can replace less than of X Y by zero.

A

Similarly, we can check if the system, if the constraint, X greater than or equal to Y, make the system unsatisfiable. uh In that case, we can replace less than of X Y by 1. and inside the. If body, we can add the additional constraint that x, minus X is less than y and difference logic that is x, minus y, less than or equal to minus 1, and then we can keep uh doing our symbolic computation.

A

So going back to the problem from the beginning, um here is like a version of the same. Like solidity chord in uh we have three variables: X, Y and Z. They all read from call data. They are not 100 equivalent, but more or less. These are. This is how they will call would look like, and we have three.

A

um We have three. If statements, the first one has less than of X comma Y. The second one is less than of Y, comma z, n, the third one has less than of Z comma X, and the last one would revert if we can register- and the question we want to know is, if the last less than of X, that can ever be zero.

A

Sorry it can, it ever be um true, and if it's never true, we can replace it by F 0, which is what we want, let's think about how to encode uh the problem now, so we have three variables: XYZ that are integers.

A

uh We don't have any extra conditions for call data law, because it's uh we can't really tell anything about it.

A

um We add a dummy variable zero, as I said before now we add the constraints that these variables are 256-bit numbers that is 0 less than or equal to a less than or equal to the U N Max. So the first set of constraints are simply saying that X is x. Y and z are positive. You can see that and the second one would say that x, y and z are bounded by the maximum value of uh U in 256.

A

and inside the. If branch in the first Branch, you can add the first constraint x, minus y, less than or equal to minus one uh inside the second. If Branch we can add the constraint y minus Z less than or equal to minus one, the third one we can add a similar one, Z minus X less than or equal to minus one and we'll learn quite a bit here. So how do we represent all these constraints as a single graph?

A

So you can see the nodes X, Y and Z. You can also see the node 0.. uh These are the constraints for the positivity and also the boundedness. So here m is the the maximum value of a 256 bit number and uh sorry.

A

um This this constraint is a z, minus X, less than or equal to minus one. Similarly, the others are on the outer. I mean the outer edges of the node, and the question we want to ask now is: is there a negative cycle in this graph and turns out? There is one um the the one uh and on the outside is the negative cycle, which means that the system has no Solutions.

A

um So now we can. We can actually replace this F of less than x, z by F of 0, and once we have this first zero. We can just completely remove this uh branch, and, um after that, these branches are simply empty. You could actually remove the entirety of the code.

A

um So in case of the difference Logic, the solver is very simple. um As I said, you can write it in Solarity layouts and that, however, in general, the solver can get quite complex and the question of correctness will always come up. The biggest priority for solidity is like the correctness of the compiler, and we really want to like minimize a trusting external tools as much as possible when they influence the code generated, so so in case of a symbolic solver.

A

If there's a way to verify that um the result is indeed true, then that is very good for us. So in case of a difference logic you can ask: is it possible to produce a proof that the system is indeed unsatisfiable that there are no Solutions turns out? You can actually do that. uh The proof of unsatisfiability in this case would be just giving a set of constraints where the, if you add up the left, hand side it's going to be zero.

A

If you add up the right hand side, it's going to be a negative number, so you get 0 less than or equal to minus one, which is contradiction, and the solver can't just tell you that. Oh these are the constraints that would add up to zero on the left and a negative number on the right, and this can be verified by you know, whatever tool that is going to use the result of the solver, but in general you can, you can get proofs for a lot of symbolic um logic.

A

um I mean you can get through some a lot of symbolic solvers, but it's not always possible um I mean. Maybe the example was like very simple like who cares about this three? um If branches? Let's look at the more real world example where this could be actually useful um as a lot of times, users would like to add their own uh text before compiler checks. So here is an array that uses read from the ra and you read from other one of the index um and um and the user want to check.

A

If the the index is going to be greater than equal to our rate of length, which means there is an auto back bounce access and the user want to like reward uh by um this customer.

A

uh However, the compiler will automatically do this check when I mean in this code. So doing this is doing. This check manually is actually like wasting gas and it's redundant, uh but this is like a good pattern like so sometimes users want to like reward with their own error messages, but we can actually use different logic to see that the second, um the second like constraint, I, mean once you get out of this.

A

uh If Brands, you can add the constraint that the index is less than less than array of length, because this branch is always terminating like if you get into this brand, it's going to revert, but in general it can also be a Brands where it's always going to return.

A

um So we can actually add this extra constraint so and if we have this check once again, you can actually prove that this uh check is going to be unreachable and then you can optimize out those brands. So how do we improve um yeah? How do we?

A

Where do we go from the difference logic, so we could only encode less than greater than an e0, but once we graduate from the constraints of the from X, less than or equal to y, less than or equal to k, Sorry x minus k x, minus y less than equal to K. We can't think about generalizing this, so one generalization would be constraints of the form a1x plus a to X. Until a and x n, less than or equal to B, um where a I and a I and B are constants and x.

A

I is a symbolic uh variable in integers uh we can actually solve that using um what's called like linear programs and the Simplex method, and once you can do that, you can encode addition and subtractions, because addition would be like X1, plus, X2 and subtraction would be X1 minus X2. They would satisfy that that, like form- um but there are some nuances here, because um addition and evm has a wrapping Behavior. So you have to have some kind of branching to deal with this motor law modeler, but it's doable.

A

um We can also encode multiplication and division. uh Similarly, where one of the one of them has to be a constant and the other one can be symbolic in case of division. The the second one has to be uh constant and get a case of multiplication. You can anything. One of the variable has to be symbolic and the other one constant, yeah I. Think that that's it from uh for my talk.

B

Okay, thank you, Harry. um We have some time for questions, so please raise your hand. Yeah I, see a hand over there um in the back. The volunteer is coming to you with a mic one. Second, oh and another one there, nice, oh and another one there yeah.

C

Hey um I'm wondering how do you know as a celebrity developer when your checks are redundant and what can you do to inspect that.

A

Yeah I think the only way to do that would be perhaps.

A

Do both the tests I mean write both of them and see if they have the same gas or set the um yeah check the intermediate representation, perhaps or the assembly, and make a diff um I mean none of the things I mentioned here are implemented so far there are some branches. uh These are just mostly experimental features.

A

Sorry, what yeah, but it's not moist,.

D

Maybe just to use it as a segue which parts are already implemented and what else might we see in the future.

A

um So we have an experimental solver that uses an smt Checker, um an experimental, optimization States. Already it's called a reasonable simplifier. It uses the full power of an smt solver, uh but it's it's uh it's disabled by default in the compiler, but you can probably enable it if you specify the optimization sequence that includes uh this one step, um so you can still get some of this. If you add an extra, um an extra like um letter to the optimization sequence, but the rest of so the wall.

A

Point of the talk is you can build a very simple logic that can do a small subset of computations. This is not done. uh This is not in the master yet, um but most of the SSA transform it's already. There.

A

B

I I thought I saw a third question somewhere. Please raise your hand if you have one, if not a big round of applause for Harry. Thank you.

A

We got one more one more question, one.

B

More okay, one more last one.

C

um So you said we should be uh doing this optimization on you all, rather than uh evm by code or solidity or or it's more conducive um and I'm wondering uh it seems like people would use this sort of uh use. This sort of analysis to potentially like look at Mev constraints um and I'm wondering how you could apply this to on-chain by code or, uh if that's uh infeasible, yeah.

A

You can probably like decompile evm into maybe some Yule and try to do similar analysis on it. There is this tool, that's getting built by Leo and some other people called Yules. You can probably check the status of that can do some of this symbolic computation. It doesn't I mean it uses like the full power of smt solvers that not this restricted version, but you can. You can probably check it out.

A

So once you have a translator from evm to you, you can apply these tools or you can use sevm, which works on evm bytecode directly. Another possibility.

B

Awesome. Thank you so much Hari.

B

I hope your brains got kind of preheated throughout the last two talks, because now we are going even deeper and we can I guess already use the time while I announce the next speaker to set up, because this will be more of a workshop setup Zina. Maybe you want to come up uh on the stage already to set your infrastructure up.

B

The next speaker we will have here is Xena he's part of the go ethereum team and in the team, his focused days, mostly on tracing the Json RPC and the graphql apis, and today, he'll be talking about evm tracing in Geth, um yeah, brace yourselves for a very detailed download on basic tracing commonly faced problems, as well as an introduction to the more recently shipped features and how to write efficient, tracers welcome Xena, big Applause.