# Solidity Internals - Raoul Schaffranek | Runtime Verification

- Speakers: Raoul Schaffranek
- Channel: [ETH Belgrade Community](https://streameth.org/eth-belgrade-community)
- Date: 2025-10-07
- Duration: 34:31
- Topics: People & Blogs
- Watch: https://streameth.org/watch/yt-ujBgLNxPKSM
- YouTube: https://www.youtube.com/watch?v=ujBgLNxPKSM

## Description

Solidity Internals - Raoul Schaffranek | Runtime Verification

## Transcript

I've given like a dozens of talks but you can see I'm shaking like because I'm a little bit nervous today because I found that the audience here is really technical. Um, so I wanted to do something more in-depth than what I usually do. And usually what I want to do today, I usually take for that like an hour workshop, but now I compress it into like 20 minutes. So we will see if this works out. If I lose you midway, then that's my fault. It's definitely not your fault. So my talk is about solidity internals. Um, quick introduction to myself. I'm Rahul Chafranek. I'm the head of developer tooling at runtime verification. Um so we do formal verification and developer tooling mostly uh for some of the work that we for example we did formally verify the deposit contract uh when Ethereum did the switch to proof of stake uh with our tools like this is where control was basically born. Um we are a long-term formal verification uh partner for optimism and also a formal verification partner uh for Immunifi Magnus. I see there's some Magnus people in the back there. Hi. Um and yeah, some of the tools that we've developed uh maybe you came across one of the other tools. Uh just quick overview, symbolic is a solidity debugger. That will be kind of the topic of today. Uh but we also have control which is our formal verification tool. Uh we have KVM uh formal semantics formal executable semantics of the EVM and uh some other tools. So agenda for today is um I'm going to talk about a new format that is called east debug format or new standard. It's called east debug and I think well not everybody may have heard of it because it's still work in progress. uh it's still in the specification phase. So I'm going to give you an overview why this is needed. Um and then I provide a little bit of theory uh that is unfortunately I cannot get around it. We need to do this. Um and then for the second part we are going to see the east debug format in action. How it makes developer tooling uh developer experience better for everyone. And then finally we will go really really deep and reverse some solidity compiler internals. Uh and this is where I'm very nervous about. Um all right so why east debug? Let's start with the motivation. Why do we need it? Um well we have a solid annual solidity developer survey where we ask developers hey what is your pain points? And since 2020, every year again, debugging shows up as one of the dreadest, most dreadest ex aspects of solidity. And 2024 is not on this slide, but um I can spoil you. Uh it showed up again. So, and the goal is now it should not show up next year again. Like we need finally need to solve this longest standing developer experience problem that solidity devs are having. And this is really what we're trying to solve here. Like it's um it's it's really a hard problem that we didn't solve for years. And for example, why are solidity devs complaining about it? And I don't want to call out this tool. This is great. This is the foundry debugger. But the foundry debugger has to work with the information that is available from the compiler. And at the moment that is not very much. So when you use the foundry debugger uh you are actually looking at some really low-level details like you see like memory uh in hexadc amps you see a stack you see the bite code and uh well you can at least see which program counter like which bite code corresponds to uh which solidity line. So that's something but it's not ideal like people are not meant to read this. This is the This is another great tool. Uh this is from this is a screenshot from the Tenderly app and I use it daily. It's it's awesome. It's incredible. But again, this tool has to work with what the solidity compiler can give us and that's not very much and that why you see like well you see a lot of low-level information here that is not really human readable. So and we need to solve this human readability problem. So and this is the state this is the status quo. So we we have a problem because well humans are really good at reading and writing solidity but they are very bad at reading and interpreting low-level EVM information and bite codes. On the other hand our tools they all operate on the EVM level and trust me tools are way easier to implement at the EVM level. Um but then these tools are having a really hard time to making the translation back to solidity so that humans can read it. Uh so this leaves us in like this unfortunate uh we live in a matrix situation. So how are we going to solve this with the east debug format? Well, two things that you need to know. So developer tools that want to be developer friendly and present the information error information or debugging information or anything really in solidity they in solidity whether than in EVM they have to do two follow two things. So left hand side you have solidity, right hand side you have the EVM and you have the compiler that takes the source code to the bite code and then funnly enough the compiler generates a source map that a debugger or any testing tool can take to map the bite code back to the source code. So that's when you remember the slide with the foundry debugger that's why the foundry debugger was able to show you in which line of code of of the source code it stopped. Now there's another thing that tools need to do and that is they need to translate the runtime information back to solidity. Like you don't want to look at raw memory. You don't want to look at the stack or at the raw storage. That's all like hexadimal numbers that doesn't make any sense. There's pointers in there that doesn't make any sense. Uh you want to um translate them back to your solidity variables. Uh now the problem is that we need a one-time map for that. And this is the missing link really. Uh the solidity compiler so far does not give it to us. So this is why these tools uh can only show you the memory or the stack but they cannot show you hey what was the content of this variable uh at this point in time. So this is the missing link. This is what the EF debug format is trying to solve. Um context about E debug format. I said it it's a work in progress standard specification. Um and it's meant for compiler debugger communication. It should solve the debugging problem that we are seeing. Um and it's led by Nick who built the truffle debugger. So uh this guy really knows his stuff. So he's leading this effort. Uh he really like he went down uh like the rabbit hole for us before us. Unfortunately the truffle debugger shut down. But luckily Nick did not give up on this. So now he's trying to solve this problem for all of us. Um in short mapping source code to or mapping bite code to source code is not enough. We also need to map the runtime verif uh the runtime information back to the um back to the solidity information. So turn war memory stack into solidity variables. turn EVM stack frames into readable solidity function call stacks and identify the variables that are in scope. How is easy debug helping us? Well, it's giving us all this information. Um so and the more important part is this information can now be retained even through compiler optimizations. Compile optimizations is really what makes it all harder for the developer tooling uh providers to implement it. And uh one thing well we can like if you know symbolic the tool that I will show you later the debugger we can already decode local variables. The problem is this only works with uh contracts that have not been optimized. With east debug we can do it in the future even on optimized contracts which is what everybody does. And now the other thing right now is um how we did it in symbolic this took us a lot of reverse engineering what the solidity compiler was doing. We looked at the solidity compiler code. Uh we gener we compiled small solidity snippets just to figure out what we wanted um what the compiler is doing. So and then we implemented an algorithm to like decode a variable from the raw memory and then the solidity compiler uh implements a patch or the language changes and suddenly what we've done our reverse engineering effort uh needs to be overthrown and we need to start from scratch. With these debug format, this will no longer be a problem because the language and the compiler, they can keep evolving, but as long as the format uh stays constant, they are not breaking the debuggers. So there have been at least three bug debuggers that I know of that have been discontinued and none of them are working anymore because of these breaking changes. So the debuggers that we are seeing today that are implementing ETH debug they will be there for a long time even if they are not actively maintained. I think they will be there for a longer time. Um and finally it means debuggers and dev tools can share code and now you're wondering okay why that should they do this aren't they competing each other and um and who would do that and the answer is well we do at runetime verification. So we've implemented a library that's called ETH debug pi. So it's a Python library and it's a complete implementation of the debugger side uh of the debugger side uh of the ETH debug format. Everybody can use it. It's it's complete. It's free and open source. Uh we were lucky uh that the Ethereum Foundation uh sponsored us to award um awarded us a grant to do this work. So it's all open source. Check out this GitHub repository. Uh the goals is of course accelerating this east debug format adoption because it solves our developer experience problems and then we want to provide a reusable library. So we think this is useful outside of debuggers. This will be useful for u testing frameworks. I think this will be useful for wake uh that we've seen in the talk before. Uh it will be use it will be useful for static analysis tools. So this is a great library. And finally, the last goal is assist compiler teams uh with implementing these debug format. And actually, we found like a handful of bugs in the Solidity compiler implementation already with the help of this library. So, if you're building a tool, check it out. Use it. Contributions are welcome. So, let's look. So, this was the theory part. Let me check the clock. Oh, I went really fast. Am I going too fast? I can start from the beginning. Uh, no, I don't I don't want to do that. No, I'm just slowing down. Um, so because what comes what what's coming now that's that's going really deep. So first of all, let me show you what our debugger looks like and what hopefully most debuggers will look like in the future when they have E debug. So now this is Visual Studio Code. On the right hand side you see some code. You see our debugger paused here in line 49. And interesting thing is maybe the more interesting thing is here what is not on the screen and you don't see any low-level information. You don't see like the war memory the stack the storage. Instead you see like the solidity variables. So you can see this parameter amount is set to 100. You can see who's the sender, who is the recipient. And this works for every local variable. That works for every data type. Um, everything that you can wish for. You never need to go back to looking at the EVM memory or was or or stack. Um, that said, I still want to do that today with you. I want to show you how you make sense of the war memory to get a feeling of uh how difficult this actually is. Um, so, uh, don't be scared by the next slide. There's pointers on it. So, uh, you've heard of dynamic arrays in Solidity. You've probably all used them. So, I have a really small function here and you think you see things are already getting really complicated on the low-level side of things. So we have a really low-level function here that is just uh taking three strings and then it's concatenating them and it's emitting a message. So where are these strings actually stored in memory? So well we can see them in the variables here. So you don't need to look at this still I want to do it today once with you. So you can see the string hello is stored at this memory offset. Uh this is the ask key encoding of the string hello. This is the ask encoding of the string world and this is the ask encoding of the string hello world. So and then you see well there's another thing here and that is a copy of the hello world string. You wouldn't have guessed from this code that the strings are copied like three times. Like you copy hello to this string. You copy it again into this string. So why is it? Um well you have one allocation for the greeting variable that's storing hello once. You have one allocation for the world variable. It's storing uh the string world once. Then you are concatenating them. And concatenating here is a copy operation even though it would not be needed. The solidity compiler could optimize for that and just uh don't copy the data but it does it. So you have this copy string and then finally um we are emitting an event. So and when we are calling this emit operation uh the string the entire string is copied once more. So you see this is a the point is not to remember what's on this slide so you can't forget about it. I probably forget about it in like the other day the day after tomorrow. The point here is even simple solidity programs get complicated really fast if you need to look at the wall memory and this is the debugger the defex issue that we are seeing today. Um so let's look at uh some more pointer stuff. Let's look at a dynamic array in Solidity. So we have a dynamic array of strings. Uh even though the size is known here or could be statically known, Solidity does not recognize it. It's still allocating a dynamic array for that. Um again, I'm just storing three words in the string uh in this array and then I'm concatenating all the strings and I'm emitting a message. Again, solidity code intentionally very very simple. left hand side low-level code very very complicated. So you but you can see some stuff like you can see okay the error length is three we have here three you have a three here and you have a three here. So this is where the error length is stored in the memory and then the three following words um are storing pointers to the elements of the array. So um and these are absolute pointers. We will meet a different kind of pointer on the next slide. But keep in mind this is an absolute pointer. So I can just read off the address which is or the offset of the memory which is 100 points me to here or 140 hexodimal pointing me to here. And this is where the string contents or where the string starts. Not even the string contents. If we look at this line we will find at the end dude I'm shaking. Um you will find the length of the strings. So the string hello five asky characters long or bite no it's asky character it's bytes it's bytes uh string world also five characters string um exclamation mark one character long and then this combined string it contains an additional space is uh like cact long which is 12 I think it's hexodimal 12 Um, so have a pointer pointing to the array element on the array element that stores the length of the strings and the next word stores the string contents. Okay, are you still can you still follow me? Nice. I I like this audience. It's very technical. Yeah, it's nice. Okay, let's look let's make things more complicated. uh how are strings um laid out or how are dynamic arrays laid out in call data. So I just showed you how strings are uh how dynamic arrays are laid out in memory. And you would think well in call data it's probably the same. Uh no it's not. And I needed to learn this the hard way because when I implemented symbolic and this debugger and I reverse engineered all this and I did all this work and I did it for the memory and I was like yeah huge achievement I finally made it. Um and then I looked at the I tried the same algorithm for the call data arrays and turns out no this is completely different algorithm that I need there. So um let's look at dynamic arrays in call data. Uh so I just to do that I just changed slightly the code. So we now have an external function here that's calling concat. It's taking a dynamic arrays of strings in call data now and it's concatenating them and returning the result. Um we stopped here in line 25. So we know that we have all the parameters that we used in this call um in our call data. So I open the call data view here. uh the first four bytes are always the function selector in the call data in case of solidity. So this is just the internal function name that the solidity compiler gives to the concat function. Um so and now things get tricky. Let let me stretch. What follows is the next word in the call data stores a pointer to the first parameters to the first function parameter. So in this case we only have one parameter but there could be more um for the functions right in this case we are lucky only one parameter. So there's only one parameter pointer here. But now this pointer if you look at um if we would look at offset 20 well you wouldn't uh you would end up somewhere in the middle here. That would that is weird. Um and that is because this is not an absolute pointer but it's a relative pointer. And to get to the address where the um where the parameter is actually encoded we need to add this value 20 to hexadimal four. So this is the base offset and this is the relative pointer. We add them together, we end up at uh offset hexodimal 24. So this is pointing here. Now this is the beginning of our array and dynamic array. Now we are lucky uh the first word again store once again stores the array length. So array length is still three. So and then once again we have three pointers pointing to the OA elements and again these are relative pointers. So we add we need to add this number 60 here to this uh base address 64. I did not put an error here because then it would be all errors on the slide. So, but this is a relative pointer pointing us to this address. And then we can weed off here the string length and here can we can we read off the string contents. All right. So, and let me check if I have another thing that I wanted to show. Oh, yeah. I do. Um, okay. Small small pause. Oh, there's a question. Yeah. >> Uh maybe on previous slide the base offset was just zero >> on in memory you mean? >> Yeah. Yeah. No, no, it's not. Um like the base offset is also is always the offset of the word where this um pointer is stored. So the base offset here is 0xa. Um yeah but but yeah it's you can think of it as in memory base offset is always zero. Um so you turn basically just yeah you get a different representation. Um yeah but thing is um pointers in memory they are always absolute pointers in call data are always relative to the base address. I don't know why they did it um but that's how it is and unfortunately this cannot be changed because AI encoding is actually something that is standardized that is used in production. Um now let's look at something else. So from this slide you may you may think that the array elements are always stored in the order that they um appear the array but that's not the case as this example shows. So here we are assigning the string uh the second or the third item of the words to exclamation mark and then only after we are assigning the string hello uh the string world and you can see this leads to here are the pointers and they are like they are crossing lines. Look at these yellow uh these pink things. Um, now what happens if we copy this array into the call data and cool thing about call data is it untangles these pointers. Now why is this why should you care about it? Well, it basically means that copying stuff from memory to call data is not it's not a simple operation. If you have complex dynamic data involved, the Solidity compiler needs to iterate over this array every time you return some uh you copy something into the call data. And it's not just copying chunks by chunks. It really needs to do arithmetic. It needs to resolve these absolute pointers into memory pointers. So there's all stuff going on. And now you see I just what's the point? Why I'm showing you this? If if all this is not needed in the future, um well, I don't know. I just wanted to nerd snipe you. Uh so in the future, you really don't have to look at this low-level data. Uh you can just look at the at the solidity variables directly. So this was like really um unneeded x course into solidity internals. But well, it said it on my topic, so and you still showed up. Uh, okay. Some shameless advertising for this tool. Uh, it's called Symbolic. And this is just a a list of my favorite features. So, what can you expect? This tool is, first of all, it's free to use. You can just go there. Um, it's partially open source. So, this east debug library, we completely open sourced it. Uh, the Visual Studio Code extension is completely open source. There's some bits that are not open source yet that we want to open source. as we secure funding for them and kind of make it sustainable because um well this we our company is also not running on laugh. Um so but this is the end goal. All our other tools completely open source. Um so what can you expect? You can set break points. You can do step-by-step execution in the solidity. really you can just step on solidity lines and not what you may experience from other debuggers is going from one event lock or from some storage operation to the next or to the next external low-level call. No, this is really stepping at the solidity level. We have full support for all variable types and data locations already. That means for unoptimized contracts, for optimized contracts, we have this E debug library which is implemented in symbolic but the compiler is not yet generating this information for us. It's still work in progress. So I don't know how long it will take them. I know that this team is busy and they are uh like they they have a lot of people to work on this. Um you can inspect event blocks. I didn't show that, but that's nice. If you want to, if you are not sniped, you can go to the disassembly view. You can see the disassembled bite code. You can set break points at the bite code. Uh you can inspect memory call data just as we did. You see that? And then one of my favorite features is time travel debugging. So this was really fun. H So that means you can go backwards in your solidity code execution. And this is um I implemented this because it was fun. But then this is I think one of the biggest productivity boosts uh that I had while solidity debugging because that means I never need to restart my debugging session when I accidentially stepped over the point um that interested me. So I can simply set a break point and I don't know on the first line again go back and this is really strong. So time travel debugging is really cool. Try it out. Uh and then there's a symbolic execution mode which is really advanced. Um and I don't have the time to go into that in any detail but symbolic execution is basically uh one flavor of doing formal verification and um this is what my company actually focuses on. So we are first and foremost we are a formal verification company. symbolic has a uh symbolic like with an I and a K at the end has a symbolic execution mode. Honestly, I don't remember why we choose this name like so this is the case because we are doing the K framework and all our tools start with K or end with K. That's cool. I don't know why we replaced the I. That was probably just a typo but now we stick with it. So symbolic execution is possible. That's a very cool feature. Um it's a very interactive way of doing formal verification. Um a very visual way of doing it. So it's essentially it's not much more difficult than using a debugger. So I think this is a well like a great um uh a great way to onboard new formal verification engineers who've never used the tech before um and get them just to to work on it. This is however still in alpha and this is only available to um our commercial clients if they if they want that. Okay. So this is uh a QR code that links you to the website. Everything else is there. There's the documentation you will need. You will see where you can download the tool. You can try even it runs in your browser. You don't even have to install anything. Um but of course you can. Um yeah and that's everything I have. Thank you again once again. I'm so happy that um so many of you uh stayed here for me with the last talk and I know like some of you guys you just came for the ending sever but that's okay. All right. Thank you. >> Yes, there you go. I was difficult to implement supporting of mappings because I think it is more like dynamic than like uh implementation of tracing arrays. >> I I sorry I didn't get the first sentence >> like was hard to implement tracing of mappings in solidity. >> Oh that's really hard. >> Yeah. >> And I have also uh the second question. what will be the next features uh to this debugging tool? >> Oh, that's a great follow-up question. >> Yeah, and thank you for your presentation. It is exciting. >> Thank you. Uh uh so mappings are really complicated data structures because you cannot just enumerate over the keys in the mapping. You can look up a key. You cannot enumerate all the keys in the array. This is a limitation that we currently have. We have a very cool solution um where we actually never so when you have a mapping there's some key that gets catched and this catchacking is a non-reversible cryptographic operation. So we cannot rec like we cannot see we cannot get the pre-image of the hash. So this is why it's so difficult to enumerate overs. We have a solution that we are playing around with um but I'm not sure if it will ever see the light of the day. But the solution basically is we never actually compute the catcher cache but we leave it some symbolic value some as some symbolic variable. Um that's something that's already uh working in the symbolic execution mode but I'm not sure if we can um if we can port it back to the concrete execution mode. Um I don't have a solution to that problem. I asked a similar question yesterday uh to in another talk where where I expected somebody had a solution to that but no they don't. And then the follow-up question was what are the next features to expect? Um uh what one other limitation that we currently have you cannot just debug any foundry test case that you have but that is what everybody wants to use it for. Everybody wants just to debug their foundry tests. And the challenge here is very very technical but basically found solidity cheat codes. These are um operations that don't have a counterpart on the EVM. They are a hack that is implemented in Foundry and we don't have the same hacks implemented in our debugger. So that's one thing that we needed to do. Um symbolic execution mode again that's also something that we are working on and that we want to make public for everyone. And then um yeah there will be a tighter integration with our formal verification tool control and our cloud compute platform. So uh that you can actually one uh like compute intensive tasks not locally but uh on our cloud comput platform. So this is what to expect. Um I cannot commit to any time frame. It always uh well depends on um uh well on on the funding that comes in because again our company does not run on laugh. Uh we need to secure funding for every feature development that we do for that and that's a um well that's the more challenging part. More questions. So you have to interpret the VM right to implement the debugger. Do you do it all in K? How does it work underneath? >> The symbolic execution mode is uses using K. Um the concrete execution mode does not use K. It's using um actually it's pluggable but it's using Anvil by default. Um we are about to make a switch to the Phoenix engine from the BuildBar team uh because they have implemented these solidity cheat codes that we want that everybody wants. Um so um yeah the problem why are we not using K for the concrete execution is basically uh K is a complete semantics um in terms of the like really EVM execution but it does not have semantics for the JSON RPC uh protocol. So this is the missing link there. We've started implementing that. So ultimately we want to move it all to K and connect it back. Um but yeah, not currently.