External Computation with Kontrol:
Leveraging Foundry Execution for Formal Verification

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!

Before giving more technical details, let’s first understand the motivation behind it.

Formal Verification and Realistic Scenarios

Many approaches can be taken when embarking on the quest to formally verify a piece of software, from lightweight and time-efficient to more involved and costly. For instance, if the verification goal is to show the correctness of the logic inside a mathematical function, we might verify the function in isolation from the rest of the system since the focus is on the logic it implements (provided it is sufficiently self-contained). Conversely, suppose we are concerned about the system-wide properties of a protocol. In that case, we should perform the verification in a realistic enough setting to translate the verification results into the deployed code.

That is, for verifying system-wide properties, the closer the verification scenario is to what will be deployed, the stronger the guarantees that the verification results actually translate into the real deal.

In Optimism’s case, we want to verify that the pausability mechanism works correctly. That is, when the `SuperchainConfig` contract says that the system is paused, no ETH or tokens should ever be withdrawable from L1 contracts. The logic that implements this is not the most complex, but we must ensure it works system-wide. This means we should verify Optimism’s contracts as intended to be deployed, which entails recreating the deployment logic in Kontrol.

Historically, the way to recreate any deployment logic in Kontrol has been to execute the deployment sequence entirely in Kontrol, or at least a simplified version of the real deployment sequence. It is a time-wise acceptable approach for less complex deployments, but running them in Kontrol can take a big time toll on very big deployment sequences, such as Optimism’s. The reason for the time toll is that Kontrol computes in math; it converts the given code to its underlying mathematical representation and then performs the mathematical operations that represent code execution. That is naturally more time-consuming than plain execution.

Given the above, we needed a way to include as much of Optimism’s deployment sequence as fast as possible into Kontrol to perform the verification realistically and time-efficiently. The key to accomplishing this is Foundry State Diff cheatcodes.

Foundry State Diffs

As fate would have it, just a few weeks before this project started, the Optimism team developed new Foundry cheatcodes that record resulting EVM state updates from executing code. This means we can now get a transcript of what happens when executing a function in Foundry. Perfect timing!

So, how do the `startStateDiffRecording` and `stopAndReturnStateDiff` cheatcodes work ¹ ? While this article does not explain them in-depth, we’ll exemplify their usage so that it’s clear enough throughout the text.

Let’s say you have a deployment function (it can be any function, really) that deploys a contract and does some stuff:

function run() public {
	Contract1 c1 = new Contract1(42);
	Contract1 c2 = new Contract2(address(c1));

	c1.doStuff();
	c2.doSomeOtherStuff();
}

And we superpower it with the state diff recording cheatcodes:

function runAndRecord() public {
	vm.startStateDiffRecording();
	run();
	Vm.AccountAccess[] memory records = vm.stopAndReturnStateDiff();
}

When we execute runAndRecord with Forge, records will hold all relevant state updates, allowing us to correctly reconstruct the effects of executing the run function. In particular, we’ll know the address where the contract’s bytecode has been deployed and any storage updates.
These storage updates are recorded for any address, so all storage-altering effects will be sequentially recorded no matter the functions called.

Thus, with the information stored in records, we can recreate the effects of the recorded function by means of vm.etch and vm.store. If a contract is deployed, we can just etch its deployed bytecode to the corresponding address. Likewise, if a function modifies any storage slot in any address, we can just store it away. This way, we don’t have to care about all the possible intricacies that have led a particular function to modify a storage slot, nor how complex the chain of deployments is. Moreover, we can use almost all vm.magic that we fancy since all of it is proxied by the state diff transcript. Note that, in contrast with vm.dumpState, the StateDiff cheatcodes don’t record any vm.store or vm.etch.

At this point, the simplification benefits that state diff recordings can bring are clear, but we’re still in the Foundry realm. We need to bring them to Kontrol!

Kontrolling the State Diffs

The first striking point is that all the state diffs are held in a `memory` variable, so we’ll need to dump that information into a file. Using the JSON-related cheatcodes, the Optimism team provided a library to pour the state-diff contents into a JSON, which Kontrol can use for its state-recreation purposes. We have provided extensive documentation on how to achieve this and how to adapt it to your project.

It’s worth mentioning that if `vm.dumpState` is used instead, it’ll directly create a JSON (with a different format) containing the updated state.

Kontrol can consume a JSON file containing state updates for two different purposes, the first of which we have hinted at before. With those state updates, Kontrol can automatically produce what we call “state recreation contracts.” A state recreation (or summary) contract has all the information needed to recreate the state updates that result from function execution faithfully. In particular, the recreation happens through a function called `recreateState`, which only uses the `store` and `etch` cheatcodes to recreate said EVM state changes. For more information on the structure of the summary contracts, refer to our documentation. This is what a slice of such a function looks like:

vm.etch(optimismPortalProxyAddress, optimismPortalProxyCode);
slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
vm.store(optimismPortalProxyAddress, slot, value);
vm.etch(l2OutputOracleProxyAddress, l2OutputOracleProxyCode);
slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
vm.store(l2OutputOracleProxyAddress, slot, value);
vm.etch(systemConfigProxyAddress, systemConfigProxyCode);
slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
vm.store(systemConfigProxyAddress, slot, value);

Instead of computing in Kontrol whatever intricate logic is responsible for producing these state updates, we can simply execute this function with Kontrol to get the same state that results from the deployment of the Optimism contracts! This is already a massive simplification of the execution logic and a big leap in efficiency for using Kontrol on complex deployment scenarios. However, this can still be optimized much further!

With the `recreateState` function, we simplify the Solidity code that needs to be run to reach the same EVM state. However, running this function in Kontrol still requires computing it with math, which is not optimal. To maximally optimize the time it takes to get those state updates into a proof, we take advantage of Kontrol being a K-based tool. Using K as the grounding framework gives us a lot of power to manipulate the underlying formalisms to which the code is translated. In this case, we can tell Kontrol to read the JSON file containing the state updates and directly incorporate them into the initial proof state before doing any mathematical computation. We take the generic initial state of a proof and start adding the information provided, such as which code corresponds to which account and what the storage mapping looks like. The need to execute (in Kontrol) any EVM-related code to get all the necessary state updates is effectively eliminated.

This is hugely significant! We now have all the `vm.magic` and fast execution times brought by Foundry at our disposal to create the initial state of Kontrol’s proofs—with zero cost in proof set-up time!

Going back to Optimism’s deployment sequence, we can now run the whole sequence while recording all the resulting state updates, produce the appropriate JSON files, and politely ask Kontrol to run our proofs, taking into account all the necessary deployment information. This has been one of the two main pillars that have made the verification of Optimism’s pausability mechanism possible. The other pillar is the native symbolic support for symbolic `bytes` and `bytes[]` arguments.

Loading the unaltered deployment sequence into Kontrol ensures that:

• The contracts under verification are deployed following the same steps as they will be deployed on-chain.
• Any changes to the deployment steps will be immediately reflected in the portion of the deployment sequence used by Kontrol.

This gives great assurance that the verification result will be translated to the deployed system. It also takes into account any changes that may happen during the development of the deployment sequence. However, we can still go the extra mile to ensure that everything is as correct as possible.

Another Layer of Trust

Introducing Foundry-recorded execution into Kontrol proofs adds another piece to our verification trust base. We have to trust that:

1. Foundry correctly records the state updates into the JSON files, and
2. Kontrol correctly retrieves the information and faithfully incorporates it into the proofs

But do we have to trust it blindly? Certainly not.

With the `recreateState` function, we can bring back the state as it is interpreted by Kontrol to Foundry and test it. Since the state recreated is what happens after deploying the contracts, we can simply run the tests that were intended for said contracts and check that everything is well deployed. This ensures that the initial state of the Kontrol proofs is correct. You can check the tests for Optimism’s deployment state updates here.

Moving Forward

Thanks to Optimism’s specific needs and their recent contribution to Foundry, we identified and fulfilled the need to add as much initial computation to proofs as fast as possible. This has significantly improved Kontrol’s usability on large projects and shows how working with other projects significantly impacts the tooling available to the ecosystem as a whole.

Regarding Kontrol’s external computation, there is also room for improvement! While we can now include as many state updates as we want, the process is not the most trivial. Ideally, we’d like to burden users as little as possible to get their relevant state updates into Kontrol. However, fear not! We are already working on solutions to address this need. Watch out in the future since you might find this solved!

If you have made it this far, first and foremost, thank you! Also, here are some links that might be of interest:

• How to add Foundry computation to your Kontrol setup 
• Kontrol documentation
• Got any questions? Ask them on our discord!

Footnotes

1. Now we also support external computation via the vm.dumpState cheatcode. ↩