# Symbolic Computation for Fun and for Profit by Hari | Devcon Bogotá

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2023-10-07
- Duration: 26:46
- Watch: https://streameth.org/watch/yt-4JODicZ1r-U
- YouTube: https://www.youtube.com/watch?v=4JODicZ1r-U

## 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/

## Transcript

foreign [Music] 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 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 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 so 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 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 so the most fundamental thing to encode would be a variable and a variable in AVM is a 256 256 bit integer 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. 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 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 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 uh we will deal with that later uh but the big question is that can we handle every assignment 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. 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 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 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 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 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 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 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. 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 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 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 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 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 so there is no solution some graph Theory trick to do the same thing so we try to encode each of this constraint using a graph 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 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 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 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 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 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 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 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 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 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 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 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 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 uh we don't have any extra conditions for call data law because it's uh we can't really tell anything about it 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. 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 [Music] [Applause] [Music] 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 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 yeah I think the only way to do that would be perhaps 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 sorry what yeah but it's not moist maybe just to use it as a segue which parts are already implemented and what else might we see in the future 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 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 no idea 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 we got one more one more question one more okay one more last one 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 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 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 awesome thank you so much Hari 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 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