Verifying LLM powered Code Transformations with Equivalence Checking - John Toman

Transcript

I'm John Toman. I'm from Storra. Uh, and I'll be talking about uh, yeah, verifying LM powered code transformations with equivalence checking. Uh, this is our obligatory uh, table of contents slide. I'm going to be first giving some background and modification for both why we want to do this rewriting and then both uh, what do we mean by equivalence checking. Uh, that'll be followed by a quick overview of this tool concordance which uh, actually implements this. Whoops. Uh then we're going to define equivalence. Can you guys still hear me? Is the mic still on? Okay, good. Sorry.

Uh then about checking equivalence and then finally go into some details about the pipeline of concordance. Okay, so background and motivation. So as a quick digression, um Storra prover is our flagship technology open source. Uh it verifies smart contracts written in solidity and many other languages both for EVM and other blockchains. Um this is a quick sort of system diagram but it relies very heavily on static analysis of memory access storage access and so on. Um now why does this matter?

Because solidity has a frequently abused feature which is inline assembly. Um this inline assembly can do all sort basically anything and this can cause uh pretty critical issues with the critical static analyses that we have. Um this is a motivating example that I took from the Solotti uh library. It's kind of representative of that entire library. It's heavily optimized. It's very gas efficient. It is also absolutely galaxy. Um it is really hard to understand what this code is doing just from looking at it. From the title of the function, we can sort of imagine what it's doing, but how it's actually going about doing that is uh sort of opaque on a first reading.

Um, but I don't I'm not trying to pick on Solotti in particular. This is actually representative of a lot of modern D5 code, right? Gas costs need to be optimized and inline assembly is what a lot of uh people uh turn to. Um, and as I mentioned, this absolutely kills some of our static analyses. And not for nothing, it's it's not to audit. It's not easy to audit either, right? So that leads to the question of can we automatically generate equivalent implementations for either auditing, code review, analysis, documentation. What do we mean by doing this? And that motivates this concordance tool. Now there are two key parts of this which is automatically generate and equivalent.

Um and so that sort of sets up the description of concordance. Now automatically generate you know it's the year of our lord 2025. So whenever you want to do something automated uh that means you're AI powered. So we can take this source code uh feed it into any available LLM. That's an interesting emoji. uh we can ask it to please rewrite the following code to use standard solidity. Make sure it's right and then out comes some nice simplified uh version of the the the the in uh code. So is it this simple? Super quick talk. Um here's a sort of a system diagram. Um pretty simple. So is it actually this simple? Well, uh, when

we're talking about AI powered, man. Oh, man. When we're talking about AI powered, we also should be talking about AI powered mistakes. So, this is a rewrite of the safe transfer from code that was proposed by Claude. And are these two equivalent? You know, uh, it looks pretty plausible. It looks really, really close, but in fact, these are not actually equivalent. And the reason is because of this line here, this little uh uh innocuous looking ABID code here. Now, it shouldn't be surprising that these LLMs make mistake. After all, they are very careful to remind us in very small text that in fact they can make mistakes all the time and there's no real guarantee about the output here.

So that motivates the next slide. There we go. So how do we actually, you know, trust the output of the AI here? Well, we have the user, they feed in some original Solidity code implementation that has this very complex assembly logic. Uh, we then feed it into an LLM with some prompt that says, "Please simplify this." And out comes some simplified implementation. We then take the original uh implementation that was fed into the LLM and feed it into this uh tool called Concord. Uh, Concord uh formally verifies whether or not two contracts are equivalent. And we'll talk about equivalent in a little bit. um if it is equivalent then we return that output to the user otherwise Concord produces an explanation of why they are

different and that gets fed back in to the LM for refinement and this keeps looping and iterating until we uh converge to a uh uh equivalent rewrite or you run out of tokens. Uh so the everything between these two dotted lines is this tool we're calling concordance. Um now again I keep writing this check of equivalent. What does that mean? uh and that is going to be sort of the next big topic of this talk. Um so an intuitive definition that I think we can all get behind is that two programs are equivalent if they do the same thing on the same inputs. Now those scare quotes are doing a lot of work. Um and so let's sort of unpack these a little bit deeper. Uh let's look actually at a

simpler definition which is that two programs are equivalent if they produce the same outputs on the same input. Now this goes back to something in mathematics called function extensionality which basically says on any input if two programs produce the same output we can declare them to be equal. Um and this has a nice sort of uh intuitive uh uh appeal to it. Uh so for example we have these two uh implementations of f. They are I think we can all agree basically the exact same program because they're just relying on the commutativity of addition. And so here we have equal inputs. X and Y are equal. And then we can ask are the outputs that is 2 plus x and y plus2 are these equal? And basic mathematic logic tells us that the former in fact implies the latter. So

this seems like a pretty good definition. So let's just say that the same inputs just mean the same call data buffers and produce the same outputs mean produce the same return data buffer. And I am including in return data the revert status as well. Well, what about this example? It's a slight tweak on the previous one. And here we've actually introduced two storage variables. And so now can we ask are these outputs equivalent given the equivalent call data inputs? And the answer is not necessarily. It depends on what the storage is, right? And so our definition of inputs is lacking a little bit. Smart contracts implicitly receive a lot of their uh extra state including their storage, the block environment, the balances of all the different contracts, xcode sizes, whatever. This is a snapshot of the uh yellow paper that defines just some of these. And so

we need to expand inputs to say the same call data buffers and environment. And again that includes the current contract state and anything else that is uh part of the environment that can be accessed by the smart contract implementation. Now there's this is actually we're still not done um because uh well we can sort of update our diagram here to say that yeah okay the input is both the call data buffer and the environment but in fact this definition is still lacking because uh what about these two functions? I think we could agree that these are definitely not equivalent um even though they do in fact advance the slide. There we go. even though they do in fact have the exact same return data buffers on the same outputs. Now,

why are these not equivalent? Like, you know, we can all look at it and say obviously they're not equivalent. They're doing different things to storage, but can we formalize that a bit better? And so, a different way to say two programs are equivalent is to say that an external actor shouldn't be able to tell the difference between two equivalent implementations. Starting in some starting state, you should be able to call any arbitrary sequence of external methods on these two contracts. Then after those steps, you shouldn't be able to tell any difference in their behavior. And this is clearly violated by those two programs we just saw. Right? Starting in a equal starting state, we could call these two functions and we get different results after we call this f function when we later query the value of z. And so what I'm reallying towards here are side effects,

right? And so we need to have some accounting for these as well. So what are some different possible side effects that uh we want care about? Well, we've already talked about mutating storage. Um, emitting a log or event that's visible to an external actor, not onchain, but you know, the uh it's observable as a result of what the smart contract did. Um, calling another contract. Um, and that includes both balance transfers and also contract creation. Um there's one more um self-destruct which I'm going to acknowledge exists but then ignore for the rest of this talk because it's I believe deprecated now and um I mention it here for uh intellectual honesty. So let's talk about some things that are not side effects um like pushing and popping the stack and mutating the memory. Now you

could argue these are definitely side effects. We when we do an MT store the state of memory looks different before and after that MT store. So what what justification do we have for ignoring these? And the key point here is external actor should not be able to tell the difference between two uh equivalent implementations. And the stack and memory are not visible to an external actor. It is effectively part of a black box once control enters into the contract execution. So if you want to be cute about it, you could say if the stack gets popped in the forest and no one's around to hear it, does it actually get popped? Okay, there's actually one final side effect that I haven't mentioned at all. Does someone want to shout it out?

Okay, great. Well, gas. So, we also exclude gas from our definition. Now, this is definitely an observable side effect. The consumption of gas decreases someone's ether balance. Um, it is a conscious choice that we made. Uh, because insisting on equivalent gas consumption effectively constrains you to execute the same sequence of op codes in the same order. And that basically just means you have exactly the same program. It restricts the state space of equivalent programs to exactly the original program itself. So there are a couple more subtleties in this definition of equivalence. One is that if a function reverts then it has no side effects by definition. So you know here in the first function we're writing one and then we're immediately reverting and the tab size is different

on this computer. Uh but we can ignore this write into Z because that's by definition what happens when you revert. All side effects are wiped away. Uh logs are not observable on chain. They're something that you can only sort of observe as an external actor. And so we allow you to commute uh log and uh function calls um because we consider that order their relative ordering not to be important. And then finally we only care about the final state of storage not intermediate states. Now there's an asterisk there because there's a point here about re-entry that we need to come back to later in the talk. But for example, we would say these two are equivalent because while yes, the contract is briefly in a different state, by the time the function is ended and an external actor can observe the state of the contract,

they're on they are in the same state as we would want. Okay, this is just one definition. It is one that is actually inspired by um compiler verification research. Uh uh seminal paper called concert talks about system trace equivalents for 2C programs and that's exactly the same thing. Basically the observable side effects of a program. But there are other possible definitions as well. things like we might want to require strictly less gas or require identical interleings of calls and logs. Another one is maybe you only want to insist on equivalence for some definition of valid inputs. Maybe you don't care about exactly the error that something reverts with when there's some malformed input. You only care about sort of the happy path of execution. But we found that sort of horistically this is a good definition. So in summary,

equivalents are two contracts or programs are equivalent if on the same call data and in the same environment they both either revert with identical return data buffers or they return with identical return data buffers and emit the same logs, make the same external calls and end with equal stoages. Okay, so as promised, we've defined equivalents. Uh it then means we need to uh talk about how we actually check or verify this equivalence. And so we're going to talk about how the Concord tool works. So um concord is the name of the uh tool that actually checks the equivalence that's used within the larger concordance tool. Um and this is going to be the densest part of the talk. Uh so concord is actually just an

application of the prover which I mentioned at the beginning of this talk. Um it is a symbolic reasoning tool and roughly what that means is that it can determine if two programs satisfy certain mathematical formula. Now the symbolic part of this means that this determination is reached uh without actually running the program and it's actually about searching a infinite state space. There's no fuzzing. There's no testing going on here. There's no concrete inputs at all. We do all this by simply analyzing the low-level bite code representation of programs. And so this means we need to have a some sort of mathematical formula that says two uh functions are equivalent. And so we have a sort of modified version of this uh diagram that we've been looking at. So

here we have the call out of buffer, storage and environment as the inputs to these two programs and we can define the output as this mumble jumbo. So here we're this R is just the revert flag. O is the return data buffer. S is just the representation of the resulting storage. These are the hashes of the calls and these are in scare quotes because I'll talk about exactly what that means in a little bit. And these are the uh hashes of the various logs that were emitted during the execution. And we can define the output of program two equivalently. And then we can write this gobbledygook which expresses the mathematical property that these two executions were in fact equivalent. Breaking this down, this simply says that they have the same revert status. Again, they either both

they both have to revert or they both have to uh return. Uh they have the same return data and it was a revert because remember if they reverted, we don't care about any of the other side effects. But if they didn't revert, then they need to have the same storage. They need to have made the same calls. and they needed to have the same logs and I keep talking about these hashes. So what exactly does uh what exactly am I talking about here? So the sto prover works on a bite code level. We operate on code that comes out of the compiler. And so I'm going to represent that bite code using this pseudo uh ule representation here. And so the at the within the con cord pipeline we ingest this bite code and then we instrument

it. And so for example here before every single call we've we insert this uh hash uh operator. Before every log we also uh insert this hash operation and before returns and reverts we also uh insert these hash operations. So these hash operations uh include all of the relevant data in the external side effect. So for call that includes the receiver contract the amount that we're sending that's R&B here. It also includes a hash of the buffer that we're sending the call data buffer that's being sent to the external contract. It also includes the hash of the current storage. And this is about that uh my comment about uh external uh or excuse me re-entry and uh storage states. We insist that if two contracts make the

same external call out, they have to be in the same storage state because that external actor could call back in and if it was allowed to call back in while the contracts were in different states, you would not have an equivalent execution. So there are these moments of quiescence and actually a more formal definition would be to say that uh the storage has to be equivalent whenever control flow leaves the contract and that means either returning or calling out. Um the we actually don't reason about what these external calls do. We just soundly model them using an over approximate that basically says the external quality could either revert, it could return a huge buffer, it could return no data, whatever, it could be an EOA whatever.

Um, for those of you who are familiar with symbolic reasoning, the uh hash is simply defined as an injective uninterpreted function. And uh you may be wondering how we are hashing these buffers symbolically because these are arbitrary length bite address buffers. Um this is in fact where most of the engineering is and it is the subject of like another 25minute talk. Um but yeah I'll give a little bit more details of how to find out more uh a little bit later. So we don't actually uh write to these special C variables. We actually have two vectors uh L and C and we just include the uh write the instrumentation so that it's writing into sequential uh locations into these two vectors during

the execution. And then we can just simply rewrite our mathematical property that compares these two uh vectors C and L across the two implementations. Now again there are maybe a couple of questions here like how do we compare all of storage? Right? Storage is two of the 256 possible indices. We definitely don't compare all two to the 256 of them and a simple question is how are we actually comparing these vectors that we're constructing. The answer to both of these and to the question of how we hash storage is actually something called scholization. It is a well-known technique in uh you know using SMT solvers. Uh I don't have a ton of time to go into explaining that. We'd have to go into a really long digression but I'm happy to go into details if anyone wants to find me after the talk. Um even with

all that there is some things that we're sort of handwaving over here. Uh there is a question about how do we know things are equivalent if there's actual re-entry. There is an argument for that but just one that is kind of uh heady and requires induction and whatnot. uh the details of how we do this buffer hashing and the actual complete model of how we model those external calls um all of those are available in this tech report that you can find by uh scanning that QR code uh 25 pages of more details than you probably ever wanted to know about this okay so that uh is the tool and as sort of a validation of this approach um it is not just used for uh our rewriting although that's uh sort of the motivating use case it's actually

useful in other context, namely verifying compiler optimizations and rewrites. And in fact, when we were testing this on a old version of the Viper compiler, we discovered that there was a bug in one of their optimization passes that incorrectly moved a variable to the same stack slot. Usually Viper stores variables in separate slots in memory and they had accidentally moved them to live in the same stack slot. So it ended up uh basically cutting a loop after one iteration and that's in the blog post. You can find that on the STOR blog for the details there. So in summary, uh Concord instruments the code to record the side effects uh and then uses the symbolic reasoning of the Stor approver to check that the results and side effects are the same on all

possible inputs. And so next up, Choo Choo, it's all aboard the AI hype train. Um and so let's talk more about the concordance tool itself. Um, so I mentioned that concordance is this feedback loop where we uh ask the LLM to generate a rewrite for us and then we check its equivalence and we get an explanation out. But I didn't really go into detail about what this explanation is or what it looks like. So to explain a bit more uh the Storver I think I've already mentioned uses SMT solvers during its uh formal verification by to explore this infinite state space. And when these solvers are able to find a case where the two programs are not equivalent, they don't

just say they're not equivalent. They give a concrete example of when their behavior is different on some possible input on some possible behavior external contracts. Um we can analyze this rather low-level uh counter example that comes out of the solver and to construct a higher level sort of human readable description of what happens. And so I want to go back to this example where this is an actually almost right rewrite. But I mentioned that this AB code is the culprit for their behavior being different. And so let's see what happens when we run these two through uh Concord. It spits out this be uh beautiful uh mess. Uh the important detail here is this. So this is basically saying what happens if the uh

token that you're transferring you're calling to transfer from on returns 0000 a word whose lower bit or bite is two. Now this is not a valid encoding of a boolean. A boolean either has to be zero or one nothing else. And so the original just if any of the if any of the output is uh malenccoded it reverts with transfer from failed. But abid code uses code that's generated by the solidity compiler and when it has a malformed input it reverts with an empty buffer and again so now we have a case where the two contracts on some particular behavior revert with different return data buffers and so they are not equivalent. So we feed this into the LLM and it comes up with this

fix simply to interpret the return data as a bite and then cast it to aint and see if it's equal to one and that means it's a validly encoded boolean that encodes true. Another part here that I want to discuss is the actual prompt that we're using here. I mentioned the motivation for this was to try to get rid of inline assembly that could be causing problems for our static analyses. So when we prompt the LM to rewrite, we say please simplify. But there's nothing fundamental about simplification here, right? We could ask uh we could ask the LM to have any number of different objectives like please optimize basically do the opposite. take uh straightforward readable solidity code

and use as much inline assembly as possible to make it gas efficient or uh port it to different libraries or different abstractions or come on uh refactor right the point here is that this is more of a general pipeline not just for L for simplifications but any LLM powered transformation the point is that these are transformations that you want to automate but make sure that you don't actually change the underlying meaning of the program now of course two programs being equivalent means that they have the same bugs as well, right? So, um that's something to also know. Uh but you can if you are confident in a reference implementation, you can generate any number of variants using LMS and then be confident that they are in fact the same.

It is also open source. Um like I said, it's part of the sort approver which is open source. So the Concord tool which is a the low-level uh mechanism for checking equivalents is open source as is the Concord script which is really a thin wrapper that mediates the interaction between an LLM and uh Concord itself. And with that I am done and thank you very much. [applause] Thank you so much John that was a really good talk. Um, two questions for you.

First one, has Concord ever discovered a more gas efficient version of the original code with without any ule? >> Without anyone? >> Has Concord ever discovered a more gas efficient version of the original code without any ule? >> No, but that is because we are usually putting it into um like really heavily optimized code and saying please simplify this. And so the state space that the LLM is effectively exploring is heavily biased towards less gas efficient like the objective is less inline assembly easier to understand and that necessarily means consuming more gas.

>> Okay, awesome. Um, can detect if there's simply no simpler version of the input source and prevent the LLM to hallucinate over and over again? >> Yes. So the tool here uh you know the the diagram I showed is simple. There is a way for it to ask for help and it's prompted to basically say if you are stuck please ask for help. Um I have seen it basically iterate a bunch of times and then just return the source code because it couldn't find a equivalent rewrite. So there is a sort of a recursion limit built into the tool itself. There is also uh the LM will itself just decide to converge. Um, and it also has explicit prompting to ask for help if it needs to get unstuck.

>> Thank you so much. Um, uh, any more questions for John because we have some time left. Any any questions from the crowd? >> Okay, awesome. Thank you so much. Give it up for John, please.