Concord: Automatically Checking EVM Bytecode Equivalence - DeFi Security Summit 2025

Transcript

Yeah. Oh. Oh. Oh. All right. I was waiting for the mic to turn on. The mic's been turned on the whole time. What a twist. Okay. Uh, thank you everyone for coming. Um, for those of you who may have been at the Solidity Summit or the Lightning talks yesterday, this is a longer version of that talk. Um, the basic idea is, uh, we want to verify LLM powered code transformations with equivalence checking and formal equivalence checking. Now I think by the end of this talk I will hopefully uh convince you or not talk workshop you know I'll convince you that uh this is actually a more general technique and is equivalence checking is helpful in many different contexts.

So we're going to go all through this again this is the exact same uh uh agenda that I had at the solidity summit talk but we'll be going through it uh slower and in more detail and hopefully with some live demos as well. Okay, so why do we want LLM powered code transformations with equivalence checking? So for those of you who don't know, I I don't know if I said this, but I'm from Sertora. Uh and at Storra, uh the we have the Stor app prover, which is our flagship technology. Oh, my mouse. Okay, so what does this do? It verifies smart contracts written in Solidity and other languages because we operate on the bite code level. So for the EVM that's EVM by

code for things like Solana that's uh SPF and for others it's like uh like uh stellar it is uh W was so what all of these different backends have in common or the different targets that we analyze and prove we need some sort of uh static analysis of memory and storage who here by show of hands knows what static analysis is okay well I think it's worth then sort of going over this what we have is a way for a a algorithm to make conclusions about a program without ever actually running it. Right? That's the static part. We are able to reach this conclusion statically without ever having to run

the program. And static analysis of memory in the context of EVM is trying to understand how the bite code is using memory. For those of you who don't know, EVM byte code exposes access just raw access to the EVM memory which is just a bite address or yes byte addressed array of bytes in print in practice or in principle 2 to the 256 bits long or uh uh bytes long but you know it's actually capped at like 2 to 64. But the point is that it's a very lowle view of memory.

There's no abstractions like allocations or new or anything. It's just here's your memory. Have fun. Now, some people do like to write low-level code that just interacts with memory. But when you write Solidity code that has a memory variable, what actually is happening under the hood is that Solidity is using something called a free pointer, which for those of you who might not know is at uh slot ox. And every time that it allocates memory, it bumps that free pointer to make room for the next thing that you're allocating, whether that's a bytes array, a strct, an array of viewints whatever.

So why do we need to analyze this? Because if we can make conclusions about different uh memory regions, if we see one access and another axis and we can prove that they have nothing to do with each other, that lets us optimize the eventual verification task. So what I'm trying to say is that we have stack analysis of memory and storage and other uh uh uh data in a bite code program and the successful analysis of memory or storage is crucial to optimizing the formula that we ultimately feed to the SAT solver or SMT solver excuse me.

So what is the static analysis kryptonite for us in solidity? It is inline assembly. Solidity is almost unique in that it makes it extremely easy to drop down and write arbitrary low-level bike code. Uh in C and C++ you can also do this too. It usually requires some sort of compiler extension that uh you really shouldn't be using unless you're writing driver code. But this is very easy in solidity and it is frequently used and it causes issues in our critical static analyses. I said that we analyze the way that the program uses the free pointer and how it uses memory. And if you're arbitrarily mutating memory like this, our analysis has to just give up. It has to say, I

don't know. You're doing something very strange. I don't know what it is. I refuse to draw any conclusions about how you're managing memory. So, this is both a motivating example for this. Can you see that? Is that big enough for you all? Is maybe. Okay, let's see if we can zoom in. Here we go. No, that didn't work. Let's try that. That didn't work either. Nope. Well, that's too bad. Okay. Well, to heck with it. Um, the takeaway here, don't try to read the right slide too closely. This comes from the Solotti library. Now, this is

written, it's uh, we can guess at what this function does. It says up here that it is doing a safe transfer from. So it's clearly doing some sort of transfer from. How is it doing that? Who knows, right? It's actually explicitly accessing that free pointer ox40. But then it just stores the two address there. And then it also stores uh data in other various constant hard-coded parts of memory. Then it makes a call which is actually doing the transfer from and then it has some very complicated check to determine whether or not it should revert. uh and then at the very end it actually puts the free pointer back. This murders our static analysis. It sees you writing uh a address into the free pointer and then later writing some other value into

the free pointer and it goes uh I'm not doing it. you can't make me. But it's pretty gas efficient, right? It's also um again pretty hard to understand. Now, I'm not trying to pick on the uh maintainer of Solott. This is quite frankly brilliant once you understand what it's doing. Um it is, you know, absolutely galaxy brain, but again, I'm not trying to pick on the Solotty guy. This is representative of a lot of modern code. And again, it kills our static analyses. But also, beyond just our problems with this, I do think it's hard to audit. I think it's hard for you to review. If someone landed this code in a a PR or inputed PR with this code, it would be pretty tough for you to

review this and really convince yourself you knew what it was doing. And I'll sort of try to give a uh explicit justification of why it's actually hard to reason about exactly what this does uh later in the talk. Okay. So that is the basic motivation for why we started building this and that is can we automatically generate an equivalent implementation to this for something like auditing code review or our own static analyses. So there are two pieces to this uh this idea here. One is automatically generate and equivalent and we're going to take those in two steps. So concordance is this tool that tries to solve this

problem. And so we said automatically generate it is 2025. When you want to automate anything, what do you do? What's the two-letter buzz word that everyone is obsessed with today? AI, right? Okay. No one said it, but I think you all thought it. So again, we're AI powered. Uh we just take our this code, we feed it into some LLM, and we say, "Please rewrite it. Use standard Solidity code instead of inline assembly. Hey, please make sure it's right." Okay? And out comes something. And it looks it looks pretty close. It's not bad. Um, here's the uh is it this simple? Is this am I going to have to find some way to fill the next 50 minutes of this one hour slot? Here's our system diagram. Again, you could use

whatever you want. Anthropic, OpenAI, it doesn't actually matter. So, cool talk, right? Well, if you're AI powered, you're getting AI powered mistakes. So this is a proposed rewrite that we had in a real interaction with Claude. And we want to ask the question, are these actually equal? It looks really close, right? It's encoding a call. That's the selector for transfer from with these arguments. It makes a call. There's some reverting logic that seems to suggest that it's doing what we want. That the call succeeded, return true.

Then that's fine. Otherwise, we allow it to also succeed if the target that we called has code data but didn't actually return anything. This is to support something like tether. For every other case, we revert. This seems pretty good. It's actually not equivalent. And the reason is this little AB code here. Now, I'm going to uh make this a pop quiz later. I guess it's not pop anymore, but I'm going to quiz you and ask you for uh theories about why this actually causes non- equivalence later in the talk. And it's not so surprising that AI means AI powered mistakes, right? All of the LLMs tell us this in very small font, but it's there that these can all make mistakes. Check important output. And that check important output is exactly

what we do. We take the original program that we're trying to simplify, feed it into the LLM with a prompt that says, "Please simplify. Please try to do it right." But then we take that output and we check it. We double check it as they tell us to. We take the original program and feed it into another tool that we call concord which is used by concordance. This formally verifies whether two contracts are equivalent to each other. If it does then hey we did it. We return it back to the user. Otherwise out of it comes a specific explanation of why they are different. You don't just get hey they're different. Figure it out. It gives you an explanation for why these two implementations actually aren't equivalent on all possible inputs. feed

that back into the LLM and it keeps going until it eventually converges to a simplification that is formally verified to be equivalent to the original program. And this bit between the uh dotted lines is roughly the concordance tool. So I keep saying equivalent. I promised that that was the second big part of this and it's going to be what uh a large chunk of this talk is going to be about. So how do we define equivalent? Okay, I'm going to just give a intuitive definition. Uh, two programs are equivalent if they do the same thing on the same inputs. Does everyone like this definition more or less? Did I Does does anyone object to this? Speak now or forever hold your peace. Okay, I think

we all like this. It seems to make sense, right? That matches our intuitive idea about what uh equivalent should mean. There are two parts of this that we need to unpack even further. do the same thing on the same inputs. So let me refine do the same thing. That's a little that's a little handwavy. Can we make this more explicit? Maybe we say they produce the same outputs. And in fact, this is motivated by something in mathematics called uh function extension which says that if two functions have the same output on every single possible input, they are equal. Right? So let's take that. It's a good definition. It's worked for mathematics for several hundred years.

uh and let's use it for our definition of equivalence, right? Same input, same output. Okay, let's test it. Let's let's let's do our bases. Let's do some, you know, pen and paper. Let's see how it works on these two functions. This takes uh a simple uint. It then adds two to it. But on the left, uh we are adding two as the uh left operand and then two as the right operand. We've just switched the variable name and then switched the order. And so we say on these equal inputs if x is equal to y is the output equivalent. Does 2 plus x= y + 2 and basic math tells us that yeah this this absolutely holds. Addition is commutive. Even if you factor in things like overflow checking this is still

going to be equivalent. So we've refined our definition. The same inputs means the exact same call data buffers and the output means the exact same return data buffers. And I should say when I say return data buffer, I am referring to the revert status whether or not the function reverted or returned that I'm just rolling into the return data buffer. Although that's technically separate. Okay. Do we like this? All right. Remember, same inputs, same outputs. That's how we're defining equivalents. And this is how we're defining them for the purposes here. Does anyone have a problem with this? Yes, you got it. Okay. What about this one?

Right. All right, we have equal inputs go to equal outputs. But here we have two storage variables W and Z. And we've declared that the call data is the same. What about their storage? We didn't say anything about it. We can't prove that this is equivalent unless we know that these are also uh the two storage variables are also equivalent to each other. And in fact, it's not just storage. It's all sorts of things, right? This is a screenshot from the yellow paper describing the various parts of the environment that you implicitly have access to as part of the execution of a smart contract. Think about account balances, code sizes, code hashes, whatever. And then you also have storage, not just your storage, but every other contract storage. So we need

to have some expanded notion of equivalence for this. And so let's say these same inputs means both the call data buffers and the environment. And now we also keep the same definition of uh outputs. All right, great catch. Is this good? Does everyone like this? We're done. Are we forgetting anything? So yeah, we got this. We've we've split it to call out a buffer and then we have this state component now which is the environment in storage.

So what about this one? Right, we talked about the input state and so right we've said that these two Z values are equal X and Y are equal but and they return the same return data buffer it's empty or they both revert so I think we'd all agree these are not actually equivalent right does anyone actually think these are equivalent okay yeah can anyone sort of say why they are not equivalent don't just say because the storage is different but like Why does that matter for us?

Well, this get leads to another intuitive definition of equivalence which says that an external actor shouldn't be able to tell the difference between two equivalent implementations and that is clearly violated by that example we just saw. Like imagine you can't look at the bite code or anything, but you can call various functions on a potential contract and you're trying to find a way where if you send them the same inputs, they somehow behave differently. And if Z is public, even if it starts equivalent to each other, when we call them, we get that F function mutates its internal state. It mutates them differently because remember, one adds an additional one on there, the other one doesn't. And so we don't see that when we call F, but when we call Z

later and ask what its value is, it does actually show up different. Right? So now suddenly the external actor goes, wait, these are different things. They're doing different things. I've called them all with the same input. We started in the same state, called them with the same inputs, and yet now suddenly they're behaving differently. What I'm really gesturing towards here is side effects, right? And so let's try to define what the side effects we care about are. So mutating storage, that one's easy. That was our motivating example. Does anyone have a different side effect that we think we might care about? Shout it out. All right, great. Someone said it. No one did. Uh emitting a logger event.

That is a side effect that we care about. That is something that once the contract is over, you can see it did something, right? You can't see it in the actual execution of a smart contract, but an external actor looking at the chain will see that logs were emitted. So that's a side effect that is visible to an external actor. Calling another contract, right? When you are calling another contract, that includes balance transfers, but also calling transfer from, you're transferring tokens from one user to another, that is a side effect. And also contract creation is part of this as well. Can anyone think of the last one? It's a It's kind of tricky.

No. All right. Self-destruct is also technically a side effect. It's also deprecated. So, this is going to be the first and last time I ever mentioned self-destruct. It's just something we don't really care about because you're not supposed to use it anymore. So, that's on you. Here are two more side effects. Pushing and popping the stack or mutating memory. But we actually don't consider these side effects. Now that's kind of weird, right? Because when you mutate memory, it's right there in the name. Mutate. That's a side effect. We are changing the state of memory before and after an M store and the stack even. We push something on the stack. The stack looks different now. So why are these not side effects? I mean, they are side effects on the stack or memory, but they're side effects that we

don't care about. Why? Because remember we define this as saying an external actor cannot tell the difference between two implementations and stack and memory are not visible to an external actor. You can of course you know in in theory you could take the input data replay it locally and you know stop it at some arbitrary point during execution and see that the memory and stack are different. But when it comes to interacting with other smart contracts, it's you don't see what another there's no way to look at what another contract's memory is, right?

Because memory and the stack only exist while the contract is executing. Once it returns, they disappear, right? They're sort of transient. Um, if you want to see it another way, we can say like, you know, if a stack gets popped in the forest and no one's around to hear it, do we actually care about that stack? Okay, one more gas. So, this is a tricky one. This is definitely a observable side effect. When you call a function, you have different amounts of gas consumed and that's different amounts of money.

That's a side effect maybe you care a lot about. But if we required that gas is absolutely equivalent in their consumption between two implementations, the gas fee schedule is such that you would need to essentially restrict the two programs to execute the same EVM op codes on exactly the same inputs and that effectively just means you've proved that a function is equal to itself. Right? It it is definitely a side effect, but one that we've explicitly decided we don't care about. Okay, there are a couple more subtleties to this definition that we need to go over first. If a function reverts, then it has no side effects by definition.

That's it's right there in the name. Revert. Revert any changes that I've made to state. Pretend none of it ever happened. So here, even though these two functions, one of them writes into storage because they both end with revert. We don't care, right? Once it reverts, the right to Z never happened. Logs are not observable on chain. And so the interle between logs and external calls is not important. The ordering of logs with one another is important and the ordering of calls within one another are important. But they can be arbitrarily interled with each other, right? Because you can only see a log event after a block gets published and you can inspect the the logs of the transaction. And so we say that these two are uh equivalent to each other.

We also only care about the final state of storage, not the intermediate states. So this first one writes one to Z and then immediately overwrites it with 42. So that's fine, whatever. So long as it's equal at the end, we don't care. Now there is a asterisk there and we will get back to that asterisk in a little bit. So that's defining equivalence according to us. But there are other reasons especially in the case of doing something like optimization. You might want to know that it uses strictly less gas, right? What's the point of optimizing if you end up using more gas?

Or maybe you want to you actually do care about the interle of calls or logs. And this one's a little bit more subtle. Equivalent modulo valid call data. And you think that's just being saying equivalent modulo uh in good input states. Maybe you don't care that your contract will revert with oh no on a malformed string and the other one reverts with oh god and the other one. You know they still revert so who cares, right? So that is one definition but it turns out writing down equivalent or valid input states is kind of hard to formalize. So we require strict on all possible inputs.

Okay. So this is equivalence written down on one big slide. Two contracts or programs are equivalent if on the same call data and in the same environment which remember includes the contract state, the state of all other contracts, balances, code sizes, whatever they both either revert with identical return data or return with the exact same return data and they emit the same logs in the same relative order to each other. make the same external calls in the same relative order to each other and end with equal stoages.

Okay, before we move on, does anyone have any sort of questions or issues with the definition that we just presented? Yes. Yeah, that's the part of the first if you care about the uh revert data that your function like let's say you're calling a function and the data that you're in that you're including in the revert is important we require that if they revert they have to have the same data because that that data is part of the like the observable result of that

execution. So return data despite its name is also revert data right when you revert that is included that revert string that you give to revert is what is returned in return data buffer sort of confusingly great question thank you any other questions about this definition comments questions concerns okay so we've defined uh equivalence how do we formally verify whether they are equivalent and so that's the sort of the densest part of this talk which is how do we actually formally verify equivalence uh with this definition.

So to go back to the diagram at the beginning of this talk, we have uh the sour prover that means that uh we determine if programs satisfy a specific mathematical formula or property. Now that's the the reasoning part of it. The symbolic uh means the same thing basically as uh static in static analysis. We can do this without ever actually running the program. We're not fuzzing inputs. We're not doing some sort of testing. We are searching infinite state spaces or effectively infinite state spaces and trying to determine whether a program satisfies some mathematical formula or property that asserts something about

its behavior or its state. So if we have a mathematical formula that suggests we need to have some way to express our definition of equivalence as a mathematical formula. So let's say we go back to this here. I've split these out to just be called data buffer storage and then the environment, right? We feed them into two different programs. We can think of P1 as not just returning a single output, but a tupole of possible outputs. So we're going to break this down in a little uh together. R is just the revert flag. Zero for didn't revert, one for did revert. O is the return buffer and that's both the data that was returned and also the payload of a

revert and then S is our resulting storage. Now let's say the function made N external calls then C 1.0 is the hash of the first external call. CN sorry C 1.n is the last call hash. Now again I'm using scare quotes there. We'll talk about what hash means in a little bit. But you can think of as basically being some unique fingerprint that ids exactly the call that you made. And so two calls were the same call if they have the same hash. Right? That's a basic property of hashing. And this is the same but just for the logs, right? And again here we don't care about the relative ordering

of C and L with each other. So we have two lists. And then we say that program 2 also produces the same thing. We can then write this as a mathematical property and get this gobbledygook on the slide here. But let's break this down, right? We're saying that they had to have the same revert status. Remember, they either both had to return or they both had to revert. The same return data means they both had the same revert reason or they returned the same thing if they didn't revert. And then finally, we said if they both reverted, that's fine, right? We don't care about any side effects provided that the revert they both reverted because again, no side effects if you reverted. Otherwise, they had to have the same storage afterwards

or uh or excuse me, and they had the same call hashes. Again, I'm I'm using hash here uh as a placeholder for something we'll talk about later. And then they have the same log hashes as well. Right? This is just basically saying our previous definition of equivalence, but now we can do it in math and look fancy. Right? Right? But I'm trying to convince you here that we can take that definition of equivalence that we wrote in natural language and actually write it down as a mathematical formula that we can then feed into the Storur approver and then just reuse the symbolic reasoning of that. Now I keep having these scare quotes and it's time for me to finally cach this check that I've been writing. What am I talking about when I say a hash of a log? What am I talking about when I say a hash of

a call? So I think I mentioned that the sour approver operates on the bite code level. So this is pseudo ule and it's supposed to represent the low-level op codes that a function is executing reading raw bite code is miserable. So we're working with this sort of intermediate low-level representation. So what we do is we take bite code we decompile it into this a this representation and then we insert these instructions before the uh before these calls. I want to emphasize we are not doing this at the source level. We aren't like changing the solidity source file to add this. Instead, we take the bite code and add these. We decompile it to this representation and then we put these in

there. All right. So, what is this doing? Well, we can see it's it actually looks like we're do we are computing hashes. I said they were logs and hashes and what do you know? They are hashing. All right. So, these hashes includes all of the relevant input data for a call, right? The input includes the target the target contract that we're calling that's R. the balance that we're sending along that's B and then also includes a hash of the buffer that we're sending as part of the external call. This is the call data of this will be turned into the call data of the receiving contract.

We also include a hash I put it in scare quotes again of current storage to deal with re-entry and we'll talk about re-entry in a little bit. Um now we don't reason about what the colle does. The colleague could transfer funds. It could call 100 other contracts. It could call back into our contract. We don't care. We just sort of say and then the colle does something. But we don't actually care so long as it mostly matches the constraints of the EVM. For example, if the call returns uh nonzero amounts of bytes, it has to not be an EOA, right? Because EOAs have no bite code.

And so by definition they always return an empty buffer. If you return a non-MP buffer you had to have some code to execute that constructed that buffer stuff like that. But other than that we don't really constrain what these actors could do. Now I keep saying hash but remember we are working with symbolic reasoning right and hashing requires you to like do a bunch of math. And I want to say that we don't actually try to exactly model the details of the catch 256 function. That would be a nightmare. It wouldn't work. So we instead use an injective uninterpreted function. Just real quick by show of hands, who knows what injective function means besides the one logic guy I know. Okay. All

right. Don't worry. We'll get to that in a little bit. Um, but this actually will pay play a pretty big role in a lot of what we do and describe later. Now, I said we have this hash of the input and output buffers, and this is actually where most of the engineering went in the building of this, and it's also where I'll be glossing over the most detail, because it truly it is just it's a lot of technical stuff. Um, and I'll give you a way to find out more if you really want to know. Now, this is uh writing to these, you know, C and L magic variables, but what we actually do is we create lists. we have a list L with C and we just have a counter that gets initialized to zero and at each of these uh at each of these

operations we just increment the current number of uh calls or logs that we've seen right so this is saying at the let's say call index that is not working let's let's say that call index is two this is basically saying at the well it's zero index so at the third call this is what the hash of the call that we are sending is okay so we actually simplify our mathematical property. Instead of all those C1, C1.n whatever functions, we can just think of them as being two lists and then we can assert that they're equal.

But there are a couple of questions here. How do you compare all of storage? Like storage is huge. It is 2 to the 256 words. And also how do you compare lists? Right? Now again, if we were executing this, how do you compare lists? We all know how to do that, right? Pointwise equivalence, have same length, all that. But how do we do this if we are symbolically reasoning? If we I said we're not executing the code. So how could we possibly compare something like a list? And that's where we're going to uh really get into the weeds here. So to understand this, you need to understand solvers. And so I'm going to talk about those in a little bit. I think I mentioned I'm from Sertora.

Um and if you've ever been in the same room of us, you've probably heard the word solver. So if you're playing along, I think I've said solver about five times now. So that's five drinks. Joking aside, um, how exactly are we using these solvers, right? We keep treating them as this black box that we use as part of our special sauce, but the way we use them is actually a not anything novel. It is a technique that's been known about for uh years in the scientific literature. So what does a solver do? What is the solvers we're talking about? Very roughly, it takes a mathematical formula and decides if it can be satisfied.

That's why they're called SAT solvers. We're seeing if a a formula can be satisfied or it proves that it can never be satisfied. So let's look at an example. Is this formula satisfiable? Is there some value of x and y that this equality holds? If you think yes, raise your hand. All right. For those of you who said no, uh or for those of you who said yes, what are what is one value of x and y that this works for? Johan, >> one and >> what?

>> Four and six. Great. You were almost right. It's actually two and four. But as this points out, satisfiable means there can be there's not just one answer. It's two and four. Four and six. Six and eight. I'm going to list them all. Well, I won't because it's infinite. There are many possible satisfiable ones. What about this one? Do we think this is satisfiable? Is there some value of x where this holds? Who thinks this is satisfiable? >> None of the real numbers. I think not even non the uh trying to think if there's an imaginary but let's say we're looking at integers, right? Do we does anyone think this is satisfiable in the integers? And if you do, I want you to tell me what you think X is.

I guess like again there's something you could be cute where you say something like this is X modulo one, but again we're working in the integers, right? And so no, there's it absolutely cannot be satisfied. There is no possible value of x where this equation can hold. Okay, cool. So we can solve like basic equalities over math. Who cares? So how do we use this for verification? Let's say we have some assertion in our code. We say that x def we don't want x to be equal to three. But we before that required that x has to be greater than four. Now all of us reading this intuitively know yeah obviously like that assertion has to be true. But let's look about how we would prove that with a sat solver. We actually don't ask it if the assertion is true. We ask if the

assertion is false. We essentially negate the condition and challenge the solver to find some value of x where x actually equals 3 and also satisfies that condition. Oops, I didn't forgot to animate that in. We're basically asking is there some value of x? That's what the mac backwards e means. It's there exists. Does there exist some possible value of x that is greater than four and is also equal to three. And obviously no there isn't right. So there's no way that the negation of that assertion can be true. Therefore this assertion has to hold. Does that make sense? This is the sort of the key idea about how you use a SAT solver for

program verification. So it's worth making sure that we understand this before we move on. Does anyone have any questions about this? Okay, great. Congrats to you all our uh formal verification experts. So what does this have to do with comparing lists? This is what I started this. How do you compare lists? Well, we need to understand that because we're asserting that L1 equals L2. And so if we do that trick, we're basically saying, well, this is what we want to say intuitively. What we actually say to the solver is can you find some possible I where the values in these two lists at I are different to one another.

Right? Now let's say that the solver says can't do it. This is not possible. There's no way for me to pick an I where these uh the lists have different values for those that in that position. So again we're sort of double negating. We said we couldn't find a place where they weren't equal. What does that mean? There's no index where the lists differ. So again apply the double negation. The lists are actually equal. This is a technique where if you want to sound fancy and impress your friends, this is scolization. Um, yeah. So now you're both formal verification experts and fun at parties.

Um, so this is the same way we compare lists. It's also how we compare storage. Storage is just a big list, right? We it's conceptually we think of it as a mapping, but you can think of it as a list with two to the 256 elements. Okay, so great, we understand this, but there's actually a another unanswered question we have, which is how are we hashing storage? And the fun trick here is that this is also skolimization. So let's quickly think about what this means. So first of all, why what do I mean by re-entry here, right? Why like why does what am I talking about?

Well, so when we make an external call, we're calling out to some contract C. We assume that the behavior of our external caller is deterministic with respect to its inputs. Okay, so we send the same input to C. It always comes out with the same answer. This is generally true. There's no real source of randomness except for like block time stamp, but that remember that's part of our definition of input. Okay, so these inputs that we're sending to the external caller are call data value and the environment which also includes the storage of the caller P1 and P2.

And it's worth mentioning this cuz let's say you call out to a uh you call out to some contract and then it calls back into you and asks what's the balance of this user, right? Because you're calling some token transfer or you're asking for it to do a swap on a user's behalf, whatever. If your external actor is calling back into you to ask about to answer some question about your state, you need to be sure you're giving the same answer. Otherwise the external call won't be the same and our assumption is violated. So this is why we insist that storage is not just equal when the call ends the outer execution ends but also whenever

you pass control to another contract because you pass control to another contract they can call back into you and observe your state and then they can do different things and then equivalence might be violated. Is this clear to everyone about why we ex So a more sort of precise definition is that we say that the contract has the two implementations storage has to be in the same state whenever control leaves the contract and goes to some external actor that could be either be whoever called it or you called someone else. Okay, so that is re-enter. Any questions so far while I drink some water?

Okay, so you guys just watched me drink water. All right, so we have these uh this is a just the slide we saw before, but we see how it works across these two different implementations, right? We have these two versions of that C list that is recording the hash of all the calls and we later assert that they are equal. And so for them to be equal or rather we said that the the sorry the uh value has to be equal uh of these of these stoages. Excuse me.

There we go. Now I can see what's coming up next. Now I said hash is an injective uninterpreted function. So what does injective mean? It means in natural language that if the output of the functions are the same, the inputs must be the same. In other words, if f ofx equals f of y, x has to equal y. And I argue this is a reasonable model of a hash. We are assuming that hash collisions are extraordinarily rare in practice. They can happen. They have to. We are taking infinite state space with like arbitrary bites and mapping them onto a single UN 256. There have to be collisions. It just it has to happen.

But it is good enough to assume that it doesn't happen at all for our purposes. Okay, does that make sense? Hashes are generally not reversible. And so if you get the same hash out, you had to have passed the same thing in again. Technically not true. True enough. Okay. So remember when we say assert C1 equals C2, we're really asking the solver, can you find a difference between these two lists? Can you find some element where they're different from each other? Now the element of these lists are these hashes. So now we just say can we find the difference between these two hashes, right? Because the elements of

the list come from the hashes. So we need to find different hashes. Now remember we said that the hash was injective that says f ofx equals f of y. The sort of opposite or the inversion of this is also true. If fx if f ofx does not equal f of y, then their inputs had to be different. So in other words, if we want to find a difference between the hashes, we need to find a difference in their arguments. If we want these two hashes to be different, one of their arguments had to be different, right? And so remember that means that we want to try to find a difference between storage.

And a storage is effectively a just really long list. And we just talked about how do you compare lists? It's with this columnization trick. So what we do is we uh do this representative function or this representative variable and actually include that. So this is a little bit of mathematical handwaving but this is effectively telling the solver you can pick any storage slot you want for the first second third call but it has to be the same slot between one and the uh first program and the second program and then we actually use that in place of uh the whole all of storage or the hash of all of storage. This is how we

represent a hash of storage. Pick one just pick a random variable don't care. Now again, why does this work? Because the solver is trying to find a difference between these lists. Finding a difference between these lists means finding a difference between the hash. Finding a difference between the hash means finding a difference between those arguments. And if it can find some index, some slot in storage that's different, it will try to find that. And again, we have to think about what the reverse of this means. If it can't find any It's not working. Ah, if it can't find a value to use here where rep one is different from rep two, then the stoages

had to be equal when control flow left the contract. Does that make sense? Have I lost everyone? Any questions? Okay. Now, even with this exhausting level of detail, we have actually glossed over some things. I mentioned that a lot of the engineering effort went into hashing buffers and I've not talked about that even a little bit. Um I also gestured roughly at the model of external calls but didn't really go into detail about what that looks like and there are other details that I've left out here including the many many optimizations we throw at this basic idea to make sure it actually like finishes in a reasonable amount of time but there's a tech report if you're interested in it.

There are a couple of limitations. Sto contracts have to use the exact same storage layout. And we can see why, right? We saw when we compared storage that we were picking arbitrary indices into storage and saying they had to be equal. If you use different storage layouts, if you've added a field somewhere, that throws the whole thing off and they'll be different. Now, they also have the same API. And the last point is implied by our environment is deterministic assumption, right? If the caller is able to then read your external code hash and then see some difference in it, this will cause it to do something different, right? But I would argue that is a pathological case and something that I don't I've never

seen done in the 5 years of looking at solidity code. If you know of a case where someone actually looks at the Xcode size and cares about its exact value, I mean, you'll have people who check Xcode size greater than zero. But I don't know that anyone checks to see if it's some exact value. And same with Xcode hash. I don't there's I've never seen someone try to figure something out about their caller this way. But I mention it for completeness. Okay. So equivalence checking we have a way to say that two contracts two programs are exactly equivalent with each other with respect to their side effects and it is the core component of the verified rewriting but it's not useful in just that

context. It's useful I'd argue in a bunch of places like say verifying compiler optimizations. They say optimization is the root of all evil and and with compilers that is exactly the case. Right? There have been many many bugs in both the Viper and the Solidity compiler and in LVM. We use Concord and actually discovered that in Viper's experimental compilation pipeline, they have this new IR they call Venom and they have a whole bunch of new optimization passes very much like via IR with Solidity.

And we said compare the behavior of this program with optimizations turned on and with optimizations turned off. And it said they are not equivalent. And we've dug into it and it's because the compiler was wrong. It was generating just absolutely busted code. Now this code was never live. They already fixed it. But it still sort of points to the success of equivalence checking being useful outside of this rewriting context. Okay. So Concord instruments code to record side effects. It then uses the symbolic reasoning of sort prover to check the results and side effects are always the same. And so next up we have to hop aboard the AI hype train.

So some details the concordance here is a feedback loop and I mentioned that if Concord finds a difference in behavior it produces an explanation but I didn't actually say what that was like what that looked like. So to motivate this I want uh to first explain how we get these explanations. I mentioned Storub uses SMT solvers. I said solvers again. So that's another drink for everybody. Um but solvers when they say SAT or unsat they don't just go hey there was a difference you figured it out. They actually say here satisfiable. Remember when we said there was a satisfiable equation, we gave explicit values of x and y to show that that equation with x

and y was satisfiable. And the solver does the same thing. And it's possible for that's okay. Uh there's it's possible to analyze those values and extract some highle description of why the two implementations are different. So I promised a quiz. Has anyone thought about how these why these are different or figured out why they're this behavior? And I've given you a hint. It's this AB code. Preferably someone who hasn't come to my other talks and I've completely given it away.

Anyone? Any guesses? Okay. Well, let's see where they're different. I promised you that Concord, the equivalence checker, would give you a concrete counter example. There it is. Uh so I think we can all agree after seeing this, we know exactly where the difference lies, right? We all understand this perfectly now. Um now despite the unfriendly uh output here, the all the information we need is here. The difference was in the reverting. The original which is the salotti version reverted and its buffer held exactly these bytes and this is

transfer from fail. It reverted with a reason transfer from failed. Our rewrite reverted with an empty buffer just it reverted. They both reverted good but again we care about revert data being the same. And so this one reverted with empty data. And so that's a difference. All right. with that clue. Can anyone tell me why this is different? Okay, the answer actually lies earlier before this. This block here is telling you what happened before in the execution and it tells us that these both of these contracts did make an external call to safe to transfer from with the same arguments. And the return buffer we just decided the solver

decided to pull out of thin air that the return buffer starts with 31 zeros and then one two one or 00002. So what does this mean? This is not a valid encoding of a bool. The ABI specification states that a boolean is either exactly zero or exactly one. Truthiness is not a thing in the ABI specification. And because it is not invalid encoding of a boolean, ABI decode reverts.

And so the original on malformed inputs explicitly reverts with transfer from failed. AID code its behavior which is generated by the compiler is that on any invalid input, any invalid encoding, it reverts with an empty buffer. And so this is why they're not equal. It got so close. So we feed this back into the LLM. Exactly that text. This is exactly what we feed back to it and it's able to analyze this and u rewrite this. The fix here is to cast the return data to a bytes 32 which basically extracts the first 32 bytes of the buffer and turns it into a scalar value then cast that into a uint and see if basically the first 32 bytes of the

return data buffer exactly equals one. And that is actually the trick. This is the fixed implementation. Okay. So concordance is useful in other contexts uh besides just simplification and truly we it's it's as simple as changing the prompt to instead of say please simplify please optimize. We can do this in the other direction. We can take that high level solidity and ask it to uh pour out some super optimized inline assembly or port or refactor. Right? I want to use a new API design etc. any context where equivalence has to be preserved. Anytime you want an LM to change your code in a way that doesn't actually change its

observable behavior, right? Observable means same side effects, same return data etc. Okay, it is open source. Um that is a GitHub link. It is um still the you saw the user interface. It's still a little bit unfriendly, but we are uh we're working on it in the open and I'd love for you to give it a try. Um I don't know if we have time for a demo. No, we have four minutes left, so I think I'm just going to have questions now. Any questions? If not, you have to get a demo. All right. Thank you. [applause] >> Yes.

the function equivalent function function that proxy contract >> proxy contracts that's that's a very interesting question so the question was is there any special handling for proxy contracts um this is not quite the same thing I mentioned that we don't care about external calls we recently like last week added support for allowing you to basically take a library that you delegate call into. And you see this a lot. People get around code size limitations by doing this. You write some core contract then write a bunch of

logic libraries and then you use delegate calls. And if you want to prove equivalence between them, it would clearly not work, right? Because one of them is making a delegate call. The other one isn't. They're different. So what we did is we added special support for uh the case where you have a delegate call that actually calls the real implementation for a function and prove that's equivalent to one where all the implementations in the same contract. Now that's not the exact same thing as a proxy contract. It is close to it. If you have just a pure proxy contract that then just delegate like delegates calls everything inside of a fallback that will just look like well you're calling something delegate call the other one doesn't. Oh, I I don't know. Um, did that answer your

question? Any other questions? Yes. >> But I was curious to know which software is being used and also if you wanted to tell a little bit more about this intermediate lowle language and if there's like any proof of the relation language and EVM. >> Thank you for that question. uh the questions were is there any SMT what's SMT solver do we use and is there a proof of equivalence between the low-level representation and EVM bike code to answer the first question it is

all of them we do what's you know we it's fantily called the portfolio method but what that really means is that we download Z3 CBC4 CBC 5 bit well another one and we just we try them all we just run them because they all have different they all have different performance profiles on different uh problems, it's hard to characterize which one to choose first. So, we try them all. And even within them, there are different like Z3 has a bunch of like strategy flags to control like how it branches on decisions. And so, we actually within each of those solvers, we have a bunch of different configurations that we've determined do better on different problems. And so, fancily, it's portfolio. It really is throw everything at the wall and see what sticks. As to the second question,

um I guess the short answer is no, right? um in part because like the low-level representation well um no that's I'm not going to say that um no I mean I would say that the low-level representation we use is effectively just the bite code operations but that operate on a register instead of the stack so we scalarize the stack but then like we have a call op code right and then in our language we have a call statement which does an external call with exactly the same arguments as the call code.

>> It's not a proof, but it is the low-level language was basically designed to just completely mirror the um the EVM uh bite codes. Can I also but I would also say even if we did prove that equivalence, we do so many intermediate analyses, those static analyses for optimization, we would also have to prove all of those are semantic preserving, right? That they're all equivalent. And in many cases, they're not because we're like slicing stuff out. We're slicing equations. the value proposition of proving the correspondence of the original decompilation sort of like it would be a nice thing to say that we did but it wouldn't have any real impact on the overall soundness of the tool because we would have to then prove

every subsequent sound with respect to blah blah blah right and just we haven't we don't have the we don't have the PhD students to do that [laughter] we're not running a lab and we can't have a bunch of PhD students doing those and publishing dissertations unfortunately great question thank I think we have time for No, we don't have time for one more. I'm uh over time, I think. Is the next speaker here? >> Yes. Oh, all right. Great. Well, then I apologize for taking up one minute of your time and thank you all again. [applause]