Formal Verification of Foundry Tests

Transcript

hey everyone um I'm Everett hildenbrandt and Gregory roshu our CEO is also here so say hi to him as well uh today I'm talking about formal verification of Foundry tests which is an ambitious title uh so this is what a Foundry test looks like you have um there's a link to this example you have some sort of setup function which allows you to initialize your scenario and then you have functions that are prefixed with tests that can take in parameters like this and Foundry will basically fuzz over these parameters and run your test with you know a bunch of different values of the parameters what Jordan was just talking about actually Foundry is really nice because it you know it doesn't really instrument the contracts or anything like that other instruments the run time instead but in

a minimal way uh yeah so starting from blank state yeah execute the setup function get a state and then use that to execute each of your tests with different parameters for input these Foundry tests can get really big very quickly I don't I guess I can't click on this this is an example of a large suite of Foundry property tests but they can actually describe pretty complex behaviors with you know complicated deployment schemes that need to be described and then lots of tests that each individual property that's important for your um for your protocol is holding basically so the

um yeah these can get big Foundry allows fuzzing uh which you just do with Forge test and so here I just had some simple test Suite that I fuzzed over so here you can see it's calling like the test withdraw function but it doesn't have any parameters and so it just runs it once and that's it but here you have test withdraw fuzz which takes in a unit 96 and it ran at 256 times on different input values to with to make sure that the test is holding right same with these print tests the key things about Foundry is yeah there's lots of runs thing and that it's super fast right and talk a little bit about the speed in a second here but you might not think it's important but it is important um hevm is a different symbolic execution

engine that actually already supports Foundry tests because Foundry inherited a lot of good design decisions from a suite of tools called daptools and we are basically following the atvm path we have this KVM Foundry Decay command which will basically generate all of the case specifications needed for a given Foundry test Suite um so these can get quite big I have a I had a very simple test Suite ended up being you know 23 000 lines of K code obviously you don't want to write all those specifications by hand right and this is what an example specification looks like here so you know it's massive but you obviously don't want to write

all this by hand so that's what The Foundry Decay tool does for you [Music] foreign once you've generated your K specifications with Foundry Decay you need to compile them so that's to translate your case specifications to core which is machine readable matching logic matching logic is the deductive verification framework we use for discharging our proof obligations this is a fixed amount of time it's always going to be about two minutes basically then you need to discharge the KVM specifications so there are 55 specifications there that were generated you have to call KVM prove on the specifications to discharge them if you're lucky or if your tests are right

and your code is right you get something back that says true but if you're unlucky or your code is wrong you get something back that looks like this and then you have to call up an expert or you have to become an expert in K in order to do this the times here can very wildly they're going to depend on the properties you're verifying and the you know the complexity of your code basically so the current work right now is we're implementing the remaining codes Foundry has this notion of cheat codes that's the instrumented run time I was talking about right now we support one cheat code but we have pull requests open for supporting the next eight most popular ones we need to support the setup function I think that'll take a few weeks and then we need to improve performance we do I'm going to give you a sneak peek

about some performance numbers that we've been working on um for concrete execution I've included foundries times here for your guys's reference Foundry claims to be I actually I haven't seen any data on this but Foundry claims to be really fast and so here's foundry's time to execute like the sum to two this is just a program that counts one to two and adds them up or one to twenty adds them up right so Foundry is taking you know 364 microseconds to sum to two but it's taking 10 seconds to sum to 20 million um our KVM on the same tests is taking these times right here right and so you can see that is what like four three or

four orders of magnitude slower but we have this exciting new performance Improvement that we're rolling out in the next few months to all of our case semantics not just our evm semantics that gives us a two orders of magnitude Improvement and performance so we're actually now only one order of magnitude slower than Foundry which puts us in the realm of being the same performance bracket as several other clients on the network I don't know foundry's claims of being the fastest are actually true I didn't validate that another thing that's important is that this performance Improvement that we see here there's two orders of magnitude performance Improvement using this semantics based compilation actually translates to symbolic execution as well and so we can I mean the numbers are a little more scattered but you can see

basically the same uh we can get out to some to a thousand using symbolic execution in the same amount of time that it took to sum to 10 instead so that's kind of cool um you want to get involved install KVM try out this presentation's instructions go to kframework.org and do the K tutorial it's taking a lot of people about two weeks there's our Discord we have a Twitter RV Inc we have a Blog where we'll be announcing when we finish up these cheat codes we'll also be announcing any of the performance improvements that come and big thanks to Stanford Satora and Lori for putting up with my late emails so thanks everyone