Add Kontrol proofs for OptimismPortal (#8634)

* Remove `OptimismPortal` from `Counter.t.sol`

* Add simple state diff contract

* Add `broadcast` modifier

* Add json cleaning scripts

* Add `statediff.sh`: execution script for summary contract generation

* Add second Counter instance

* Update execution script

* Add `StateDiffCheatcode` contract

* `run-kontrol.sh`: run `StateDiffCheatcode.recreateDeployment` test

* `run-kontrol.sh`: Set `FOUNDRY_PROFILE` flag to `kontrol`

* `run-kontrol.sh`: Remove `--no-forge-build`

* Add `stategen` foundry profile

* Update instructions to create a custom deployment from `Deploy`

* Add `run-kontrol-local.sh`

* Reflect `Counter.sol` being moved to kontrol folder

* `statediff.sh`: update for newest summary kontrol version

* Add `test/kontrol/state-change/` folder

* forge install: kontrol-cheatcodes

* foundry.toml: add `kontrol-cheatcodes` remapping

* statediff.sh: Execute custom deployment script with `kontrol` profile

* `run-kontrol-local.sh`: make `test_proveWithdrawalTransaction_paused` the default

* `statediff.sh`: create dummy save files if they don't exist

* `statediff.sh`: replace mustGetAddress by getAddress in Deploy.s.sol

* `foundry.toml`: add `read` access to `kout` folder

* Update addresses to `internal constant`s

* `forge-std`: update version to `80a8f6e`

* Save guardian address

* Decrease `forge script` verbosity

* Update summary contracts to latest version

* Rename `StateDiff` to `KontrolDeployment`

* Rename `statediff.sh` to `makeSummaryDeployment.sh` and move to `kontrol` folder

* Update `makeSummaryDeployment.sh`

* Change summary name to `DeploymentSummary`

* Move deployment files and `KontrolUtils` to `utils`

* Rename `StateDiffTest.sol` to `OptimismPortal.k.sol`

* `OptimismPortal.k.sol`: fix typo renaming `DeploymentSummary`

* Rename `state-change` to `proofs`

* Move scripts under `kontrol/kontrol/scripts`

* Add json cleaning scripts under `scripts/json` folder

* `run-kontrol-local.sh`: update module name

* `DeploymentSummary.sol`: fix typo on importing code contract

* `KontrolDeployment`: do not save the guardian address

* `run-kontrol-local.sh`: update proof names

* Update kontrol foundry profile names

* `run-kontrol-local.sh`: remove unnecessary comments

* `run-kontrol.sh`: add `proveWithdrawalTransaction` proof to run

* Tidy up `run-kontrol-local.sh`

* Update `run-kontrol.sh`

* `OptimismPortal.k.sol`: clean file

* `OptimismPortal.k.sol`: add `test_finalizeWithdrawalTransaction_paused_reverts` proof

* Add `test_finalizeWithdrawalTransaction_paused` to `run-kontrol-local.sh`

* `.gitignore`: add `kout-deployment` and `kout-proofs`

* `OptimismPortalKontrol`: make size of symbolic bytes param be 320

* `KontrolUtils`: optimizations for symbolic `withdrawalProof`

* Add `README.md`

* Run `forge fmt`

* Move dummy tests to `proofs/tests`

* Update `run-kontrol.sh`

* Update `DeploymentSummaryCode.sol`

* `README.md`: add execution instructions

* Update symbolic optimizations

* Cleanup `make-summary-deployment.sh`

* Cleanup `KontrolUtils`

* `kontrol/README.md`: add description for `pausability-lemmas.k`

* Add description for Kontrol Foundry profiles

* Move `kontrol/kontrol` contents to `kontrol`

* Change interface naming convention

* `make-summary-deployment.sh`: `set -euo pipefail`

* `run-kontrol.sh`: reorg `regen` and `rekompile` empty assignments

* `KontrolUtils`: update name parameters of `createWithdrawalTransaction`

* `OptimismPortal.k.sol`: Replace `assert` by `requires`

* `OptimismPortal.k.sol`: remove `test_kontrol_in_foundry`

* `.gitignore`: update kontrol logs location

* `make-summary-deployment.sh`: change `sed` for `awk` and make its changes transient

* `kontrol/README.md`: reflect dissolution of `kontrol/kontrol`

* Keep track of statediff deployment json instead of `DeploymentSummary`

* `KontrolUtils`: `freshAddress` typo

* `KontrolUtils`: set first symbolic workaround; symb `bytes[].length` 10

* forge install: forge-std

v1.7.4

* `make-summary-deployment.sh`: explanation for `mustGetAddress` replacement

* `make-summary-deployment.sh`: missing `utils` folder in summary dir

* Merging local and container script; New call methdo  to run locally otherwise no input expected or accepted

* Enforcing new paramters local/container/dev for various run scenarios of version enforcement and developer god mode for expereimenting with versions/builds of kontrol

* usage wording improvement

* Fixing scenario no arguments passed and shifting

* Update packages/contracts-bedrock/test/kontrol/scripts/make-summary-deployment.sh
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Update packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Typo in packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Update description of packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

* Document `run-kontrol.sh` in README

* README.md: Update description of the Kontrol folder

* README.md: refine foundry profile description

* remove remaining `kontrol/kontrol` instances

* correct location of `run-kontrol.sh` script

* OptimismPortal.k.sol: rename `test_*` to `proof_*`

* Kontrol-Deploy.json: update to latest code

* make-summary-deployment.sh: add `forge fmt` as last summary gen step

* README.md: fix formatting typo

* contracts-bedrock: update bindings (kontrol proofs)

* Replace `/* */` comments by `//`

* OptimismPortal.k.sol: remove commented `_withdrawalProof` argument

* Remove `CounterNames.json`

* KontrolUtils.sol: remove unused functions

* Describe `clean_json.py` and `reverse_key_values.py`

* test/kontrol/README.md: fix typos

* OptimismPortal.k.sol: license and typo

* KontrolUtils: document the goal of `arrayLength` range

* `OptimismPortal.k.sol`: rename `proof_*` to `prove_*`

* Remove `createWithdrawalTransaction` function; better proof parameters

* OptimismPortal.k.sol: Add tracking issue for symbolic `bytes` support

* Add deployment summaries license and disclaimer comment

* versions.json: bump Kontrol to 0.1.117

* run-kontrol.sh: update Kontrol version getter method

* run-kontrol.sh: fix typo for enforcing local Kontrol version

* `OptimismPortal.k.sol`: remove `== true` no-ops

* contracts-bedrock: update bindings (kontrol proofs)

---------
Co-authored-by: F-WRunTime <Freeman.Wenzl@runtimeverification.com>
Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com>
Co-authored-by: Matt Solomon <matt@mattsolomon.dev>

.gitmodules

@@ -17,6 +17,9 @@
 	path = packages/contracts-bedrock/lib/safe-contracts
 	url = https://github.com/safe-global/safe-contracts
 	branch = v1.4.0
+[submodule "packages/contracts-bedrock/lib/kontrol-cheatcodes"]
+	path = packages/contracts-bedrock/lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes
 [submodule "packages/contracts-bedrock/lib/solady"]
 	path = packages/contracts-bedrock/lib/solady
 	url = https://github.com/Vectorized/solady

op-bindings/bindings/weth9.go

@@ -31,7 +31,7 @@ var (
 // WETH9MetaData contains all meta data concerning the WETH9 contract.
 var WETH9MetaData = &bind.MetaData{
 	ABI: "[{\"type\":\"fallback\",\"stateMutability\":\"payable\"},{\"type\":\"function\",\"name\":\"allowance\",\"inputs\":[{\"name\":\"\",\"type\":\"address\",\"internalType\":\"address\"},{\"name\":\"\",\"type\":\"address\",\"internalType\":\"address\"}],\"outputs\":[{\"name\":\"\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"approve\",\"inputs\":[{\"name\":\"guy\",\"type\":\"address\",\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"outputs\":[{\"name\":\"\",\"type\":\"bool\",\"internalType\":\"bool\"}],\"stateMutability\":\"nonpayable\"},{\"type\":\"function\",\"name\":\"balanceOf\",\"inputs\":[{\"name\":\"\",\"type\":\"address\",\"internalType\":\"address\"}],\"outputs\":[{\"name\":\"\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"decimals\",\"inputs\":[],\"outputs\":[{\"name\":\"\",\"type\":\"uint8\",\"internalType\":\"uint8\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"deposit\",\"inputs\":[],\"outputs\":[],\"stateMutability\":\"payable\"},{\"type\":\"function\",\"name\":\"name\",\"inputs\":[],\"outputs\":[{\"name\":\"\",\"type\":\"string\",\"internalType\":\"string\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"symbol\",\"inputs\":[],\"outputs\":[{\"name\":\"\",\"type\":\"string\",\"internalType\":\"string\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"totalSupply\",\"inputs\":[],\"outputs\":[{\"name\":\"\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"stateMutability\":\"view\"},{\"type\":\"function\",\"name\":\"transfer\",\"inputs\":[{\"name\":\"dst\",\"type\":\"address\",\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"outputs\":[{\"name\":\"\",\"type\":\"bool\",\"internalType\":\"bool\"}],\"stateMutability\":\"nonpayable\"},{\"type\":\"function\",\"name\":\"transferFrom\",\"inputs\":[{\"name\":\"src\",\"type\":\"address\",\"internalType\":\"address\"},{\"name\":\"dst\",\"type\":\"address\",\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"outputs\":[{\"name\":\"\",\"type\":\"bool\",\"internalType\":\"bool\"}],\"stateMutability\":\"nonpayable\"},{\"type\":\"function\",\"name\":\"withdraw\",\"inputs\":[{\"name\":\"wad\",\"type\":\"uint256\",\"internalType\":\"uint256\"}],\"outputs\":[],\"stateMutability\":\"nonpayable\"},{\"type\":\"event\",\"name\":\"Approval\",\"inputs\":[{\"name\":\"src\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"guy\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"indexed\":false,\"internalType\":\"uint256\"}],\"anonymous\":false},{\"type\":\"event\",\"name\":\"Deposit\",\"inputs\":[{\"name\":\"dst\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"indexed\":false,\"internalType\":\"uint256\"}],\"anonymous\":false},{\"type\":\"event\",\"name\":\"Transfer\",\"inputs\":[{\"name\":\"src\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"dst\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"indexed\":false,\"internalType\":\"uint256\"}],\"anonymous\":false},{\"type\":\"event\",\"name\":\"Withdrawal\",\"inputs\":[{\"name\":\"src\",\"type\":\"address\",\"indexed\":true,\"internalType\":\"address\"},{\"name\":\"wad\",\"type\":\"uint256\",\"indexed\":false,\"internalType\":\"uint256\"}],\"anonymous\":false}]",
-	Bin: "0x60c0604052600d60808190526c2bb930b83832b21022ba3432b960991b60a090815261002e916000919061007a565b50604080518082019091526004808252630ae8aa8960e31b602090920191825261005a9160019161007a565b506002805460ff1916601217905534801561007457600080fd5b50610115565b828054600181600116156101000203166002900490600052602060002090601f016020900481019282601f106100bb57805160ff19168380011785556100e8565b828001600101855582156100e8579182015b828111156100e85782518255916020019190600101906100cd565b506100f49291506100f8565b5090565b61011291905b808211156100f457600081556001016100fe565b90565b6107f9806101246000396000f3fe6080604052600436106100bc5760003560e01c8063313ce56711610074578063a9059cbb1161004e578063a9059cbb146102cb578063d0e30db0146100bc578063dd62ed3e14610311576100bc565b8063313ce5671461024b57806370a082311461027657806395d89b41146102b6576100bc565b806318160ddd116100a557806318160ddd146101aa57806323b872dd146101d15780632e1a7d4d14610221576100bc565b806306fdde03146100c6578063095ea7b314610150575b6100c4610359565b005b3480156100d257600080fd5b506100db6103a8565b6040805160208082528351818301528351919283929083019185019080838360005b838110156101155781810151838201526020016100fd565b50505050905090810190601f1680156101425780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561015c57600080fd5b506101966004803603604081101561017357600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610454565b604080519115158252519081900360200190f35b3480156101b657600080fd5b506101bf6104c7565b60408051918252519081900360200190f35b3480156101dd57600080fd5b50610196600480360360608110156101f457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135811691602081013590911690604001356104cb565b34801561022d57600080fd5b506100c46004803603602081101561024457600080fd5b503561066b565b34801561025757600080fd5b50610260610700565b6040805160ff9092168252519081900360200190f35b34801561028257600080fd5b506101bf6004803603602081101561029957600080fd5b503573ffffffffffffffffffffffffffffffffffffffff16610709565b3480156102c257600080fd5b506100db61071b565b3480156102d757600080fd5b50610196600480360360408110156102ee57600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610793565b34801561031d57600080fd5b506101bf6004803603604081101561033457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160200135166107a7565b33600081815260036020908152604091829020805434908101909155825190815291517fe1fffcc4923d04b559f4d29a8bfc6cda04eb5b0d3c460751c2402c5c5cc9109c9281900390910190a2565b6000805460408051602060026001851615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b820191906000526020600020905b81548152906001019060200180831161042f57829003601f168201915b505050505081565b33600081815260046020908152604080832073ffffffffffffffffffffffffffffffffffffffff8716808552908352818420869055815186815291519394909390927f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925928290030190a350600192915050565b4790565b73ffffffffffffffffffffffffffffffffffffffff83166000908152600360205260408120548211156104fd57600080fd5b73ffffffffffffffffffffffffffffffffffffffff84163314801590610573575073ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff14155b156105ed5773ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020548211156105b557600080fd5b73ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020805483900390555b73ffffffffffffffffffffffffffffffffffffffff808516600081815260036020908152604080832080548890039055938716808352918490208054870190558351868152935191937fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef929081900390910190a35060019392505050565b3360009081526003602052604090205481111561068757600080fd5b33600081815260036020526040808220805485900390555183156108fc0291849190818181858888f193505050501580156106c6573d6000803e3d6000fd5b5060408051828152905133917f7fcf532c15f0a6db0bd6d0e038bea71d30d808c7d98cb3bf7268a95bf5081b65919081900360200190a250565b60025460ff1681565b60036020526000908152604090205481565b60018054604080516020600284861615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b60006107a03384846104cb565b9392505050565b60046020908152600092835260408084209091529082529020548156fea265627a7a723158201668ab2847c86647a20370de3c85906542e9da3d84f500326fc63321f2774e9264736f6c63430005110032",
+	Bin: "0x60c0604052600d60808190526c2bb930b83832b21022ba3432b960991b60a090815261002e916000919061007a565b50604080518082019091526004808252630ae8aa8960e31b602090920191825261005a9160019161007a565b506002805460ff1916601217905534801561007457600080fd5b50610115565b828054600181600116156101000203166002900490600052602060002090601f016020900481019282601f106100bb57805160ff19168380011785556100e8565b828001600101855582156100e8579182015b828111156100e85782518255916020019190600101906100cd565b506100f49291506100f8565b5090565b61011291905b808211156100f457600081556001016100fe565b90565b6107f9806101246000396000f3fe6080604052600436106100bc5760003560e01c8063313ce56711610074578063a9059cbb1161004e578063a9059cbb146102cb578063d0e30db0146100bc578063dd62ed3e14610311576100bc565b8063313ce5671461024b57806370a082311461027657806395d89b41146102b6576100bc565b806318160ddd116100a557806318160ddd146101aa57806323b872dd146101d15780632e1a7d4d14610221576100bc565b806306fdde03146100c6578063095ea7b314610150575b6100c4610359565b005b3480156100d257600080fd5b506100db6103a8565b6040805160208082528351818301528351919283929083019185019080838360005b838110156101155781810151838201526020016100fd565b50505050905090810190601f1680156101425780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561015c57600080fd5b506101966004803603604081101561017357600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610454565b604080519115158252519081900360200190f35b3480156101b657600080fd5b506101bf6104c7565b60408051918252519081900360200190f35b3480156101dd57600080fd5b50610196600480360360608110156101f457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135811691602081013590911690604001356104cb565b34801561022d57600080fd5b506100c46004803603602081101561024457600080fd5b503561066b565b34801561025757600080fd5b50610260610700565b6040805160ff9092168252519081900360200190f35b34801561028257600080fd5b506101bf6004803603602081101561029957600080fd5b503573ffffffffffffffffffffffffffffffffffffffff16610709565b3480156102c257600080fd5b506100db61071b565b3480156102d757600080fd5b50610196600480360360408110156102ee57600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610793565b34801561031d57600080fd5b506101bf6004803603604081101561033457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160200135166107a7565b33600081815260036020908152604091829020805434908101909155825190815291517fe1fffcc4923d04b559f4d29a8bfc6cda04eb5b0d3c460751c2402c5c5cc9109c9281900390910190a2565b6000805460408051602060026001851615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b820191906000526020600020905b81548152906001019060200180831161042f57829003601f168201915b505050505081565b33600081815260046020908152604080832073ffffffffffffffffffffffffffffffffffffffff8716808552908352818420869055815186815291519394909390927f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925928290030190a350600192915050565b4790565b73ffffffffffffffffffffffffffffffffffffffff83166000908152600360205260408120548211156104fd57600080fd5b73ffffffffffffffffffffffffffffffffffffffff84163314801590610573575073ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff14155b156105ed5773ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020548211156105b557600080fd5b73ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020805483900390555b73ffffffffffffffffffffffffffffffffffffffff808516600081815260036020908152604080832080548890039055938716808352918490208054870190558351868152935191937fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef929081900390910190a35060019392505050565b3360009081526003602052604090205481111561068757600080fd5b33600081815260036020526040808220805485900390555183156108fc0291849190818181858888f193505050501580156106c6573d6000803e3d6000fd5b5060408051828152905133917f7fcf532c15f0a6db0bd6d0e038bea71d30d808c7d98cb3bf7268a95bf5081b65919081900360200190a250565b60025460ff1681565b60036020526000908152604090205481565b60018054604080516020600284861615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b60006107a03384846104cb565b9392505050565b60046020908152600092835260408084209091529082529020548156fea265627a7a72315820da81c51fd0d922de9c089035f567f35f651802d142623db49c311d681ade1c6064736f6c63430005110032",
 }
 
 // WETH9ABI is the input ABI used to generate the binding from.

op-bindings/bindings/weth9_more.go

@@ -13,7 +13,7 @@ const WETH9StorageLayoutJSON = "{\"storage\":[{\"astId\":1000,\"contract\":\"src
 
 var WETH9StorageLayout = new(solc.StorageLayout)
 
-var WETH9DeployedBin = "0x6080604052600436106100bc5760003560e01c8063313ce56711610074578063a9059cbb1161004e578063a9059cbb146102cb578063d0e30db0146100bc578063dd62ed3e14610311576100bc565b8063313ce5671461024b57806370a082311461027657806395d89b41146102b6576100bc565b806318160ddd116100a557806318160ddd146101aa57806323b872dd146101d15780632e1a7d4d14610221576100bc565b806306fdde03146100c6578063095ea7b314610150575b6100c4610359565b005b3480156100d257600080fd5b506100db6103a8565b6040805160208082528351818301528351919283929083019185019080838360005b838110156101155781810151838201526020016100fd565b50505050905090810190601f1680156101425780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561015c57600080fd5b506101966004803603604081101561017357600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610454565b604080519115158252519081900360200190f35b3480156101b657600080fd5b506101bf6104c7565b60408051918252519081900360200190f35b3480156101dd57600080fd5b50610196600480360360608110156101f457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135811691602081013590911690604001356104cb565b34801561022d57600080fd5b506100c46004803603602081101561024457600080fd5b503561066b565b34801561025757600080fd5b50610260610700565b6040805160ff9092168252519081900360200190f35b34801561028257600080fd5b506101bf6004803603602081101561029957600080fd5b503573ffffffffffffffffffffffffffffffffffffffff16610709565b3480156102c257600080fd5b506100db61071b565b3480156102d757600080fd5b50610196600480360360408110156102ee57600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610793565b34801561031d57600080fd5b506101bf6004803603604081101561033457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160200135166107a7565b33600081815260036020908152604091829020805434908101909155825190815291517fe1fffcc4923d04b559f4d29a8bfc6cda04eb5b0d3c460751c2402c5c5cc9109c9281900390910190a2565b6000805460408051602060026001851615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b820191906000526020600020905b81548152906001019060200180831161042f57829003601f168201915b505050505081565b33600081815260046020908152604080832073ffffffffffffffffffffffffffffffffffffffff8716808552908352818420869055815186815291519394909390927f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925928290030190a350600192915050565b4790565b73ffffffffffffffffffffffffffffffffffffffff83166000908152600360205260408120548211156104fd57600080fd5b73ffffffffffffffffffffffffffffffffffffffff84163314801590610573575073ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff14155b156105ed5773ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020548211156105b557600080fd5b73ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020805483900390555b73ffffffffffffffffffffffffffffffffffffffff808516600081815260036020908152604080832080548890039055938716808352918490208054870190558351868152935191937fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef929081900390910190a35060019392505050565b3360009081526003602052604090205481111561068757600080fd5b33600081815260036020526040808220805485900390555183156108fc0291849190818181858888f193505050501580156106c6573d6000803e3d6000fd5b5060408051828152905133917f7fcf532c15f0a6db0bd6d0e038bea71d30d808c7d98cb3bf7268a95bf5081b65919081900360200190a250565b60025460ff1681565b60036020526000908152604090205481565b60018054604080516020600284861615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b60006107a03384846104cb565b9392505050565b60046020908152600092835260408084209091529082529020548156fea265627a7a723158201668ab2847c86647a20370de3c85906542e9da3d84f500326fc63321f2774e9264736f6c63430005110032"
+var WETH9DeployedBin = "0x6080604052600436106100bc5760003560e01c8063313ce56711610074578063a9059cbb1161004e578063a9059cbb146102cb578063d0e30db0146100bc578063dd62ed3e14610311576100bc565b8063313ce5671461024b57806370a082311461027657806395d89b41146102b6576100bc565b806318160ddd116100a557806318160ddd146101aa57806323b872dd146101d15780632e1a7d4d14610221576100bc565b806306fdde03146100c6578063095ea7b314610150575b6100c4610359565b005b3480156100d257600080fd5b506100db6103a8565b6040805160208082528351818301528351919283929083019185019080838360005b838110156101155781810151838201526020016100fd565b50505050905090810190601f1680156101425780820380516001836020036101000a031916815260200191505b509250505060405180910390f35b34801561015c57600080fd5b506101966004803603604081101561017357600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610454565b604080519115158252519081900360200190f35b3480156101b657600080fd5b506101bf6104c7565b60408051918252519081900360200190f35b3480156101dd57600080fd5b50610196600480360360608110156101f457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135811691602081013590911690604001356104cb565b34801561022d57600080fd5b506100c46004803603602081101561024457600080fd5b503561066b565b34801561025757600080fd5b50610260610700565b6040805160ff9092168252519081900360200190f35b34801561028257600080fd5b506101bf6004803603602081101561029957600080fd5b503573ffffffffffffffffffffffffffffffffffffffff16610709565b3480156102c257600080fd5b506100db61071b565b3480156102d757600080fd5b50610196600480360360408110156102ee57600080fd5b5073ffffffffffffffffffffffffffffffffffffffff8135169060200135610793565b34801561031d57600080fd5b506101bf6004803603604081101561033457600080fd5b5073ffffffffffffffffffffffffffffffffffffffff813581169160200135166107a7565b33600081815260036020908152604091829020805434908101909155825190815291517fe1fffcc4923d04b559f4d29a8bfc6cda04eb5b0d3c460751c2402c5c5cc9109c9281900390910190a2565b6000805460408051602060026001851615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b820191906000526020600020905b81548152906001019060200180831161042f57829003601f168201915b505050505081565b33600081815260046020908152604080832073ffffffffffffffffffffffffffffffffffffffff8716808552908352818420869055815186815291519394909390927f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925928290030190a350600192915050565b4790565b73ffffffffffffffffffffffffffffffffffffffff83166000908152600360205260408120548211156104fd57600080fd5b73ffffffffffffffffffffffffffffffffffffffff84163314801590610573575073ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff14155b156105ed5773ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020548211156105b557600080fd5b73ffffffffffffffffffffffffffffffffffffffff841660009081526004602090815260408083203384529091529020805483900390555b73ffffffffffffffffffffffffffffffffffffffff808516600081815260036020908152604080832080548890039055938716808352918490208054870190558351868152935191937fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef929081900390910190a35060019392505050565b3360009081526003602052604090205481111561068757600080fd5b33600081815260036020526040808220805485900390555183156108fc0291849190818181858888f193505050501580156106c6573d6000803e3d6000fd5b5060408051828152905133917f7fcf532c15f0a6db0bd6d0e038bea71d30d808c7d98cb3bf7268a95bf5081b65919081900360200190a250565b60025460ff1681565b60036020526000908152604090205481565b60018054604080516020600284861615610100027fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0190941693909304601f8101849004840282018401909252818152929183018282801561044c5780601f106104215761010080835404028352916020019161044c565b60006107a03384846104cb565b9392505050565b60046020908152600092835260408084209091529082529020548156fea265627a7a72315820da81c51fd0d922de9c089035f567f35f651802d142623db49c311d681ade1c6064736f6c63430005110032"
 
 
 func init() {

packages/contracts-bedrock/.gitignore

@@ -3,8 +3,9 @@ artifacts
 forge-artifacts
 cache
 broadcast
-kout
-test/kontrol/kontrol/logs
+kout-deployment
+kout-proofs
+test/kontrol/logs
 
 # Metrics
 coverage.out

packages/contracts-bedrock/foundry.toml

@@ -19,6 +19,7 @@ remappings = [
   'forge-std/=lib/forge-std/src',
   'ds-test/=lib/forge-std/lib/ds-test/src',
   'safe-contracts/=lib/safe-contracts/contracts',
+  'kontrol-cheatcodes/=lib/kontrol-cheatcodes/src',
   'solady/=lib/solady/src',
 ]
 extra_output = ['devdoc', 'userdoc', 'metadata', 'storageLayout']
@@ -38,6 +39,7 @@ fs_permissions = [
   { access='read', path = './forge-artifacts/' },
   { access='write', path='./semver-lock.json' },
   { access='read-write', path='./.testdata/' },
+  { access='read', path='./kout-deployment' }
 ]
 libs = ["node_modules", "lib"]
 
@@ -73,9 +75,16 @@ optimizer = false
 ################################################################
 #                         PROFILE: KONTROL                     #
 ################################################################
+# See test/kontrol/README.md for an explanation of how the profiles are configured
 
-[profile.kontrol]
+[profile.kdeploy]
 src = 'src/L1'
-out = 'kout'
+out = 'kout-deployment'
 test = 'test/kontrol'
 script = 'scripts-kontrol'
+
+[profile.kprove]
+src = 'test/kontrol/proofs'
+out = 'kout-proofs'
+test = 'test/kontrol/proofs'
+script = 'scripts-kontrol'

kontrol-cheatcodes @ 2c48ae1a

+Subproject commit 2c48ae1ab44228c199dca29414c0b4b18a3434e6

packages/contracts-bedrock/package.json

@@ -19,7 +19,7 @@
     "build:go-ffi": "(cd scripts/go-ffi && go build)",
     "autogen:invariant-docs": "npx tsx scripts/invariant-doc-gen.ts",
     "test": "pnpm build:go-ffi && forge test",
-    "test:kontrol": "./test/kontrol/kontrol/run-kontrol.sh",
+    "test:kontrol": "./test/kontrol/scripts/run-kontrol.sh",
     "genesis": "./scripts/generate-l2-genesis.sh",
     "coverage": "pnpm build:go-ffi && forge coverage",
     "coverage:lcov": "pnpm build:go-ffi && forge coverage --report lcov",

packages/contracts-bedrock/test/kontrol/KontrolDeployment.sol

+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import { Deploy } from "scripts/Deploy.s.sol";
+
+contract KontrolDeployment is Deploy {
+    function runKontrolDeployment() public stateDiff {
+        deploySafe();
+        setupSuperchain();
+
+        // deployProxies();
+        deployERC1967Proxy("OptimismPortalProxy");
+        deployERC1967Proxy("L2OutputOracleProxy");
+        deployERC1967Proxy("SystemConfigProxy");
+        transferAddressManagerOwnership(); // to the ProxyAdmin
+
+        // deployImplementations();
+        deployOptimismPortal();
+        deployL2OutputOracle();
+        deploySystemConfig();
+
+        // initializeImplementations();
+        initializeSystemConfig();
+        initializeOptimismPortal();
+    }
+}

packages/contracts-bedrock/test/kontrol/README.md

+# Kontrol Verification
+
+This folder contains Kontrol symbolic property tests.
+
+## Directory structure
+
+The directory is structured as follows
+
+```tree
+test/kontrol
+├── KontrolDeployment.sol
+├── pausability-lemmas.k
+├── proofs
+│   ├── interfaces
+│   │   └── KontrolInterfaces.sol
+│   ├── OptimismPortal.k.sol
+│   ├── tests
+│   │   ├── Counter.sol
+│   │   └── Counter.t.sol
+│   └── utils
+│       ├── DeploymentSummaryCode.sol
+│       ├── DeploymentSummary.sol
+│       └── KontrolUtils.sol
+├── README.md
+└── scripts
+    ├── json
+    │   ├── clean_json.py
+    │   └── reverse_key_values.py
+    ├── make-summary-deployment.sh
+    └── run-kontrol.sh
+```
+
+### Root folder
+
+- [`KontrolDeployment.sol`](./KontrolDeployment.sol): Reduced deployment to generate the summary contract
+- [`pausability-lemmas.k`](./pausability-lemmas.k): File containing the necessary lemmas for this project
+- [`proofs`](./proofs): Where the proofs of the project live
+- [`scripts`](./scripts): Where the scripts of the projects live
+
+### [`proofs`](./proofs) folder
+
+- [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol): Symbolic property tests
+- [`interfaces`](./proofs/interfaces): Files with the signature of the functions involved in the verification effort
+- [`utils`](./proofs/utils): Dependencies for `OptimismPortal.k.sol`, including the summary contracts
+
+### [`scripts`](./scripts) folder
+
+- [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh): Executes [`KontrolDeployment.sol`](./KontrolDeployment.sol), curates the result and writes the summary deployment contract
+- [`run-kontrol.sh`](./scrpts/run-kontrol.sh): Proof execution script
+- [`json`](./scripts/json): Data cleaning scripts for the output of [`KontrolDeployment.sol`](./KontrolDeployment.sol)
+
+## Verification execution
+
+The verification execution consists of two steps, although the first step may be omitted to use the committed version. There's one script to run per step. These scripts should be run from the [`contracts-bedrock`](../../) directory.
+
+1. Generate a deployment summary contract from [`KontrolDeployment.sol`](./KontrolDeployment.sol)
+```bash
+  ./test/kontrol/scripts/make-summary-deployment.sh
+```
+This step is optional. The default summary can be found [here](./proofs/utils/DeploymentSummary.sol), which is the summarization of the [`KontrolDeployment.sol`](./KontrolDeployment.sol) script.
+
+2. Execute the tests in [`OptimismPortal.k.sol`](./proofs/OptimismPortal.k.sol)
+```bash
+  ./test/kontrol/scripts/run-kontrol.sh $option
+```
+See below for further documentation on `run-kontrol.sh`.
+
+### `run-kontrol.sh` script
+The `run-kontrol.sh` script handles all modes of proof execution. The modes, corresponding to the available arguments of the script, are the following:
+- `container`: Run the proofs in the same docker image used in CI. The intended use case is CI debugging. This is the default execution mode, meaning that if no arguments are provided, the proofs will be executed in this mode.
+- `local`: Run the proofs with your local Kontrol install, enforcing the version to be the same as the one used in CI. The intended use case is running the proofs without risking discrepancies because of different Kontrol versions.
+- `dev`: Run the proofs with your local Kontrol install, without enforcing any version in particular. The intended use case is proof development and related matters.
+
+For a similar description of the options run `run-kontrol.sh --help`.
+
+## Kontrol Foundry profiles
+
+This project uses two different [Foundry profiles](../../foundry.toml), `kdeploy` and `kprove`.
+
+- `kdeploy`: This profile is used to generate a summary contract from the execution of the [`KontrolDeployment.sol`](./KontrolDeployment.sol) script. In particular, the `kdeploy` profile is used by the [`make-summary-deployment.sh`](./scripts/make-summary-deployment.sh) script to generate the [deployment summary contract](./proofs/utils/DeploymentSummary.sol). The summary contract is then used with the `kprove` profile to load the post-setUp state directly into Kontrol. We don't need the output artifacts from this step, so we save them to the `kout-deployment` directory, which is not used anywhere else. We also point the script path to the `scripts-kontrol` directory, which does not exist, to avoid compiling scripts we don't need, which reduces execution time.
+
+- `kprove`: This profile is used by the [`run-kontrol.sh`](./scrpts/run-kontrol.sh) script, which needs to be run after executing [`./test/kontrol/script/make-summary-deployment`](./scripts/make-summary-deployment.sh) (this last script uses the `kdeploy` profile). The proofs are executed using the `kprove` profile. The `src` directory points to a test folder because we only want to compile what is in the `test/kontrol/proofs` folder since it contains all the deployed bytecode and the proofs. We similarly point the script path to a non-existent directory for the same reason as above. The `out` folder for this profile is `kout-proofs`.
+
+Note that the compilation of the necessary `src/L1` files is done with the `kdeploy` profile, and the results are saved into [`test/kontrol/proofs/utils/DeploymentSummary.sol`](./proofs/utils/DeploymentSummary.sol). So, when running the `kprove` profile, the deployed bytecode of the `src/L1` files are recorded in the automatically generated file `test/kontrol/proofs/utils/DeploymentSummaryCode.sol`.
+
+## References
+
+[Kontrol docs](https://docs.runtimeverification.com/kontrol/overview/readme)

packages/contracts-bedrock/test/kontrol/proofs/OptimismPortal.k.sol

+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+import { DeploymentSummary } from "./utils/DeploymentSummary.sol";
+import { KontrolUtils } from "./utils/KontrolUtils.sol";
+import { Types } from "src/libraries/Types.sol";
+import {
+    IOptimismPortal as OptimismPortal,
+    ISuperchainConfig as SuperchainConfig
+} from "./interfaces/KontrolInterfaces.sol";
+
+contract OptimismPortalKontrol is DeploymentSummary, KontrolUtils {
+    OptimismPortal optimismPortal;
+    SuperchainConfig superchainConfig;
+
+    function setUp() public {
+        recreateDeployment();
+        optimismPortal = OptimismPortal(payable(OptimismPortalProxyAddress));
+        superchainConfig = SuperchainConfig(SuperchainConfigProxyAddress);
+    }
+
+    /// TODO: Replace struct parameters and workarounds with the appropriate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_proveWithdrawalTransaction_paused(
+        // WithdrawalTransaction args
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        uint256 _value,
+        uint256 _gasLimit,
+        // bytes   memory _data,
+        uint256 _l2OutputIndex,
+        // OutputRootProof args
+        bytes32 _outputRootProof0,
+        bytes32 _outputRootProof1,
+        bytes32 _outputRootProof2,
+        bytes32 _outputRootProof3
+    )
+        external
+    {
+        bytes memory _data = freshBigBytes(320);
+
+        bytes[] memory _withdrawalProof = freshWithdrawalProof();
+
+        Types.WithdrawalTransaction memory _tx =
+            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
+        Types.OutputRootProof memory _outputRootProof =
+            Types.OutputRootProof(_outputRootProof0, _outputRootProof1, _outputRootProof2, _outputRootProof3);
+
+        // After deployment, Optimism portal is enabled
+        require(optimismPortal.paused() == false, "Portal should not be paused");
+
+        // Pause Optimism Portal
+        vm.prank(optimismPortal.GUARDIAN());
+        superchainConfig.pause("identifier");
+
+        // Portal is now paused
+        require(optimismPortal.paused(), "Portal should be paused");
+
+        // No one can call proveWithdrawalTransaction
+        vm.expectRevert("OptimismPortal: paused");
+        optimismPortal.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+
+    /// TODO: Replace struct parameters and workarounds with the appropiate
+    /// types once Kontrol supports symbolic `bytes` and `bytes[]`
+    /// Tracking issue: https://github.com/runtimeverification/kontrol/issues/272
+    function prove_finalizeWithdrawalTransaction_paused(
+        uint256 _nonce,
+        address _sender,
+        address _target,
+        uint256 _value,
+        uint256 _gasLimit
+    )
+        external
+    {
+        bytes memory _data = freshBigBytes(320);
+
+        Types.WithdrawalTransaction memory _tx =
+            Types.WithdrawalTransaction(_nonce, _sender, _target, _value, _gasLimit, _data);
+
+        // After deployment, Optimism portal is enabled
+        require(optimismPortal.paused() == false, "Portal should not be paused");
+
+        // Pause Optimism Portal
+        vm.prank(optimismPortal.GUARDIAN());
+        superchainConfig.pause("identifier");
+
+        // Portal is now paused
+        require(optimismPortal.paused(), "Portal should be paused");
+
+        vm.expectRevert("OptimismPortal: paused");
+        optimismPortal.finalizeWithdrawalTransaction(_tx);
+    }
+}

packages/contracts-bedrock/test/kontrol/proofs/interfaces/KontrolInterfaces.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { Types } from "src/libraries/Types.sol";
+
+interface IOptimismPortal {
+    function GUARDIAN() external view returns (address);
+
+    function guardian() external view returns (address);
+
+    function paused() external view returns (bool paused_);
+
+    function proveWithdrawalTransaction(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external;
+
+    function finalizeWithdrawalTransaction(Types.WithdrawalTransaction memory _tx) external;
+}
+
+interface ISuperchainConfig {
+    function guardian() external view returns (address);
+
+    function paused() external view returns (bool paused_);
+
+    function pause(string memory _identifier) external;
+
+    function unpause() external;
+}

packages/contracts-bedrock/test/kontrol/proofs/utils/DeploymentSummary.sol

+// SPDX-License-Identifier: MIT
+// This file was autogenerated by running `kontrol summary`. Do not edit this file manually.
+
+pragma solidity ^0.8.13;
+
+import { Vm } from "forge-std/Vm.sol";
+
+import { DeploymentSummaryCode } from "./DeploymentSummaryCode.sol";
+
+contract DeploymentSummary is DeploymentSummaryCode {
+    // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
+    address internal constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+    Vm internal constant vm = Vm(VM_ADDRESS);
+
+    address internal constant AddressManagerAddress = 0xBb2180ebd78ce97360503434eD37fcf4a1Df61c3;
+    address internal constant L2OutputOracleAddress = 0x1B9F0e648A0A4780120A6Cd07B952F76560c8F8b;
+    address internal constant L2OutputOracleProxyAddress = 0x8B71b41D4dBEb2b6821d44692d3fACAAf77480Bb;
+    address internal constant OptimismPortalAddress = 0x94eA1235778aDc02FD93c242e6A23Ef5C8c3CE44;
+    address internal constant OptimismPortalProxyAddress = 0x978e3286EB805934215a88694d80b09aDed68D90;
+    address internal constant ProtocolVersionsAddress = 0xfbfD64a6C0257F613feFCe050Aa30ecC3E3d7C3F;
+    address internal constant ProtocolVersionsProxyAddress = 0x416C42991d05b31E9A6dC209e91AD22b79D87Ae6;
+    address internal constant ProxyAdminAddress = 0xDB8cFf278adCCF9E9b5da745B44E754fC4EE3C76;
+    address internal constant SafeProxyFactoryAddress = 0x34A1D3fff3958843C43aD80F30b94c510645C316;
+    address internal constant SafeSingletonAddress = 0x90193C961A926261B756D1E5bb255e67ff9498A1;
+    address internal constant SuperchainConfigAddress = 0x068E44eB31e111028c41598E4535be7468674D0A;
+    address internal constant SuperchainConfigProxyAddress = 0xDEb1E9a6Be7Baf84208BB6E10aC9F9bbE1D70809;
+    address internal constant SystemConfigAddress = 0xc7B87b2b892EA5C3CfF47168881FE168C00377FB;
+    address internal constant SystemConfigProxyAddress = 0x1c23A6d89F95ef3148BCDA8E242cAb145bf9c0E4;
+    address internal constant SystemOwnerSafeAddress = 0x2601573C28B77dea6C8B73385c25024A28a00C3F;
+
+    function recreateDeployment() public {
+        bytes32 slot;
+        bytes32 value;
+        vm.etch(SafeProxyFactoryAddress, SafeProxyFactoryCode);
+        vm.etch(SafeSingletonAddress, SafeSingletonCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SafeSingletonAddress, slot, value);
+        vm.etch(SystemOwnerSafeAddress, SystemOwnerSafeCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"00000000000000000000000090193c961a926261b756d1e5bb255e67ff9498a1";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"e90b7bceb6e7df5418fb78d8ee546e97c83a08bbccc01a0644d599ccd2a7c2e0";
+        value = hex"0000000000000000000000001804c8ab1f12e6bbf3894d4083f33e07309d1f38";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"d1b0d319c6526317dce66989b393dcfb4435c9a65e399a088b63bbf65d7aee32";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000003";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"cc69885fda6bcc1a4ace058b4a62bf5e179ea78fd58a1ccd71c22cc9b688792f";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        vm.etch(AddressManagerAddress, AddressManagerCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000001804c8ab1f12e6bbf3894d4083f33e07309d1f38";
+        vm.store(AddressManagerAddress, slot, value);
+        vm.etch(ProxyAdminAddress, ProxyAdminCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000001804c8ab1f12e6bbf3894d4083f33e07309d1f38";
+        vm.store(ProxyAdminAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000003";
+        value = hex"000000000000000000000000bb2180ebd78ce97360503434ed37fcf4a1df61c3";
+        vm.store(ProxyAdminAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000002601573c28b77dea6c8b73385c25024a28a00c3f";
+        vm.store(ProxyAdminAddress, slot, value);
+        vm.etch(SuperchainConfigProxyAddress, SuperchainConfigProxyCode);
+        slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        vm.etch(SuperchainConfigAddress, SuperchainConfigCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SuperchainConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(SuperchainConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SuperchainConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"000000000000000000000000068e44eb31e111028c41598e4535be7468674d0a";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        slot = hex"d30e835d3f35624761057ff5b27d558f97bd5be034621e62240e5c0b784abe68";
+        value = hex"0000000000000000000000009965507d1a55bcc2695c58ba16fb37d819b0a4dc";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SuperchainConfigProxyAddress, slot, value);
+        vm.etch(ProtocolVersionsProxyAddress, ProtocolVersionsProxyCode);
+        slot = hex"b53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        vm.etch(ProtocolVersionsAddress, ProtocolVersionsCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(ProtocolVersionsAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(ProtocolVersionsAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"0000000000000000000000004e59b44847b379578588920ca78fbf26c0b4956c";
+        vm.store(ProtocolVersionsAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"000000000000000000000000000000000000000000000000000000000000dead";
+        vm.store(ProtocolVersionsAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(ProtocolVersionsAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000002";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"000000000000000000000000fbfd64a6c0257f613fefce050aa30ecc3e3d7c3f";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"0000000000000000000000009965507d1a55bcc2695c58ba16fb37d819b0a4dc";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(ProtocolVersionsProxyAddress, slot, value);
+        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);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(AddressManagerAddress, slot, value);
+        vm.etch(OptimismPortalAddress, OptimismPortalCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(OptimismPortalAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(OptimismPortalAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000032";
+        value = hex"000000000000000000000000000000000000000000000000000000000000dead";
+        vm.store(OptimismPortalAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        value = hex"000000000000000100000000000000000000000000000000000000003b9aca00";
+        vm.store(OptimismPortalAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(OptimismPortalAddress, slot, value);
+        vm.etch(L2OutputOracleAddress, L2OutputOracleCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(L2OutputOracleAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(L2OutputOracleAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(L2OutputOracleAddress, slot, value);
+        vm.etch(SystemConfigAddress, SystemConfigCode);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"0000000000000000000000001804c8ab1f12e6bbf3894d4083f33e07309d1f38";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"000000000000000000000000000000000000000000000000000000000000dead";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000068";
+        value = hex"0000000000000000000000000000000000000000000000000000000001406f40";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000069";
+        value = hex"0000ffffffffffffffffffffffffffffffff000f42403b9aca00080a01312d00";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemConfigAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000003";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"000000000000000000000000c7b87b2b892ea5c3cff47168881fe168c00377fb";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"000000000000000000000000db8cff278adccf9e9b5da745b44e754fc4ee3c76";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000033";
+        value = hex"0000000000000000000000009965507d1a55bcc2695c58ba16fb37d819b0a4dc";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000067";
+        value = hex"0000000000000000000000003c44cdddb6a900fa2b585dd299e03d12fa4293bc";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000065";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000834";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000066";
+        value = hex"00000000000000000000000000000000000000000000000000000000000f4240";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000068";
+        value = hex"00000000000000000000000000000000000000000000000000000000017d7840";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"65a7ed542fb37fe237fdfbdd70b31598523fe5b32879e307bae27a0bd9581c08";
+        value = hex"0000000000000000000000009965507d1a55bcc2695c58ba16fb37d819b0a4dc";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000069";
+        value = hex"0000ffffffffffffffffffffffffffffffff000f42403b9aca00080a01312d00";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(SystemConfigProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000005";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000004";
+        vm.store(SystemOwnerSafeAddress, slot, value);
+        slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc";
+        value = hex"00000000000000000000000094ea1235778adc02fd93c242e6a23ef5c8c3ce44";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000101";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000035";
+        value = hex"0000000000000000000000deb1e9a6be7baf84208bb6e10ac9f9bbe1d7080900";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000032";
+        value = hex"000000000000000000000000000000000000000000000000000000000000dead";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        value = hex"000000000000000100000000000000000000000000000000000000003b9aca00";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+        slot = hex"0000000000000000000000000000000000000000000000000000000000000000";
+        value = hex"0000000000000000000000000000000000000000000000000000000000000001";
+        vm.store(OptimismPortalProxyAddress, slot, value);
+    }
+}

packages/contracts-bedrock/test/kontrol/proofs/utils/KontrolUtils.sol

+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.15;
+
+import { Vm } from "forge-std/Vm.sol";
+import { Types } from "src/libraries/Types.sol";
+import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol";
+
+contract GhostBytes {
+    bytes public ghostBytes;
+}
+
+contract GhostBytes10 {
+    bytes public ghostBytes0;
+    bytes public ghostBytes1;
+    bytes public ghostBytes2;
+    bytes public ghostBytes3;
+    bytes public ghostBytes4;
+    bytes public ghostBytes5;
+    bytes public ghostBytes6;
+    bytes public ghostBytes7;
+    bytes public ghostBytes8;
+    bytes public ghostBytes9;
+
+    function getGhostBytesArray() public view returns (bytes[] memory _arr) {
+        _arr = new bytes[](10);
+        _arr[0] = ghostBytes0;
+        _arr[1] = ghostBytes1;
+        _arr[2] = ghostBytes2;
+        _arr[3] = ghostBytes3;
+        _arr[4] = ghostBytes4;
+        _arr[5] = ghostBytes5;
+        _arr[6] = ghostBytes6;
+        _arr[7] = ghostBytes7;
+        _arr[8] = ghostBytes8;
+        _arr[9] = ghostBytes9;
+    }
+}
+
+/// @notice tests inheriting this contract cannot be run with forge
+abstract contract KontrolUtils is KontrolCheats {
+    /// @dev we only care about the vm signature
+    // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D.
+    address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code"))));
+    Vm private constant vm = Vm(VM_ADDRESS);
+
+    /// @dev Creates a fresh bytes with length greater than 31
+    /// @param bytesLength: Length of the fresh bytes. Should be concrete
+    function freshBigBytes(uint256 bytesLength) internal returns (bytes memory sBytes) {
+        require(bytesLength >= 32, "Small bytes");
+
+        uint256 bytesSlotValue;
+        unchecked {
+            bytesSlotValue = bytesLength * 2 + 1;
+        }
+
+        // Deploy ghost contract
+        GhostBytes ghostBytes = new GhostBytes();
+
+        // Make the storage of the ghost contract symbolic
+        kevm.symbolicStorage(address(ghostBytes));
+
+        // Load the size encoding into the first slot of ghostBytes
+        vm.store(address(ghostBytes), bytes32(uint256(0)), bytes32(bytesSlotValue));
+
+        sBytes = ghostBytes.ghostBytes();
+    }
+
+    /// @dev Creates a bounded symbolic bytes[] memory representing a withdrawal proof
+    /// Each element is 17 * 32 = 544 bytes long, plus ~10% margin for RLP encoding: each element is 600 bytes
+    /// The length of the array to 10 or fewer elements
+    function freshWithdrawalProof() public returns (bytes[] memory withdrawalProof) {
+        // Assume arrayLength = 2 for faster proof speeds
+        // TODO: have the array length range between 0 and 10 elements
+        uint256 arrayLength = 6;
+
+        withdrawalProof = new bytes[](arrayLength);
+
+        // Deploy ghost contract
+        // GhostBytes10 ghostBytes10 = new GhostBytes10();
+
+        // Make the storage of the ghost contract symbolic
+        // kevm.symbolicStorage(address(ghostBytes10));
+
+        // Each bytes element will have a length of 600
+        // uint256 bytesSlotValue = 600 * 2 + 1;
+
+        // Load the size encoding into the first slot of ghostBytes
+        // vm.store(address(ghostBytes10), bytes32(uint256(0)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(1)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(2)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(3)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(4)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(5)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(6)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(7)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(8)), bytes32(bytesSlotValue));
+        // vm.store(address(ghostBytes10), bytes32(uint256(9)), bytes32(bytesSlotValue));
+
+        // withdrawalProof = ghostBytes10.getGhostBytesArray();
+
+        // Second approach
+
+        // withdrawalProof[0] = ghostBytes10.ghostBytes0();
+        // withdrawalProof[1] = ghostBytes10.ghostBytes1();
+        // withdrawalProof[2] = ghostBytes10.ghostBytes2();
+        // withdrawalProof[3] = ghostBytes10.ghostBytes3();
+        // withdrawalProof[4] = ghostBytes10.ghostBytes4();
+        // withdrawalProof[5] = ghostBytes10.ghostBytes5();
+        // withdrawalProof[6] = ghostBytes10.ghostBytes6();
+        // withdrawalProof[7] = ghostBytes10.ghostBytes7();
+        // withdrawalProof[8] = ghostBytes10.ghostBytes8();
+        // withdrawalProof[9] = ghostBytes10.ghostBytes9();
+
+        // First approach
+
+        for (uint256 i = 0; i < withdrawalProof.length; ++i) {
+            withdrawalProof[i] = freshBigBytes(600);
+        }
+    }
+}

packages/contracts-bedrock/test/kontrol/scripts/json/clean_json.py

+"""
+Description:
+    Unescapes the JSON produced by the stateDiff modifier
+    defined in contracts-bedrock/scripts/Deploy.s.sol
+    This script is used in ../make-summary-deployment.sh
+
+Usage:
+    After producing a state diff JSON with the stateDiff modifier
+    (e.g. by executing KontrolDeployment::runKontrolDeployment), the JSON is
+    saved under contracts-bedrock/snapshots/state-diff/Deploy.json. To unescape
+    it, run: python3 clean_json.py $path_to_state_diff_json
+    The unescaped JSON will rewrite the input file
+"""
+
+import sys
+import json
+
+def clean_json(input_file):
+    with open(input_file, 'r') as file:
+        input_string = file.read()
+
+    result = input_string
+
+    # Remove backslashes
+    result = result.replace('\\', '')
+
+    # Remove " between ] and ,
+    result = result.replace(']",', '],')
+
+    # Remove " between } and ]
+    result = result.replace('}"]', '}]')
+
+    # Remove " between [ and {
+    result = result.replace('["{', '[{')
+
+    # Remove " between } and ,
+    result = result.replace('}",', '},')
+
+    # Remove " between , and {
+    result = result.replace(',"{', ',{')
+
+    # Remove " before [{
+    result = result.replace('"[{', '[{')
+
+    # Remove " after }]
+    result = result.replace('}]"', '}]')
+
+    with open(input_file, 'w') as file:
+        file.write(result)
+
+if __name__ == "__main__":
+    # Check if a file path is provided as a command line argument
+    if len(sys.argv) != 2:
+        print("Usage: clean_json.py <file_path>")
+        sys.exit(1)
+
+    input_file_path = sys.argv[1]
+
+    clean_json(input_file_path)
+
+    print(f"Operation completed. Result saved to {input_file_path}")

packages/contracts-bedrock/test/kontrol/scripts/json/reverse_key_values.py

+"""
+Description:
+    Reverses the key-value pairs of a given JSON
+    The use case for this script within the project is to reverse the key-value
+    pairs of the auto generated file contracts-bedrock/deployments/hardhat/.deployment
+    so that it can be fed as the `--contract-names` argument to `kontrol summary`
+    This script is used in ../make-summary-deployment.sh
+
+Usage:
+    To reverse the order of an $input_file and save it to an $output_file run
+    `python3 reverse_key_values.py $input_file $output_file`
+"""
+
+import sys
+import json
+
+def reverse_json(input_file, output_file):
+    try:
+        with open(input_file, 'r') as file:
+            json_data = json.load(file)
+
+        reversed_json = {str(value): key for key, value in json_data.items()}
+
+        with open(output_file, 'w') as file:
+            json.dump(reversed_json, file, indent=2)
+
+        print(f"Reversed JSON saved to {output_file}")
+
+    except FileNotFoundError:
+        print(f"Error: File not found: {input_file}")
+        sys.exit(1)
+    except json.JSONDecodeError:
+        print(f"Error: Invalid JSON format in file: {input_file}")
+        sys.exit(1)
+
+if __name__ == "__main__":
+    # Check if both input and output file paths are provided
+    if len(sys.argv) != 3:
+        print("Usage: reverse_key_values.py <input_file_path> <output_file_path>")
+        sys.exit(1)
+
+    input_file_path = sys.argv[1]
+    output_file_path = sys.argv[2]
+
+    # Execute the function to reverse JSON and save to the output file
+    reverse_json(input_file_path, output_file_path)

packages/contracts-bedrock/test/kontrol/scripts/make-summary-deployment.sh

+#!/bin/bash
+set -euo pipefail
+
+# create deployments/hardhat/.deploy and snapshots/state-diff/Deploy.json if necessary
+if [ ! -d "deployments/hardhat" ]; then
+  mkdir deployments/hardhat;
+fi
+if [ ! -f "deployments/hardhat/.deploy" ]; then
+  touch deployments/hardhat/.deploy;
+fi
+if [ ! -d "snapshots/state-diff" ]; then
+  mkdir snapshots/state-diff;
+fi
+if [ ! -f "snapshots/state-diff/Deploy.json" ]; then
+  touch snapshots/state-diff/Deploy.json;
+fi
+
+DEPLOY_SCRIPT="./scripts/Deploy.s.sol"
+
+# Create a backup
+cp ${DEPLOY_SCRIPT} ${DEPLOY_SCRIPT}.bak
+
+# Replace mustGetAddress by getAddress in Deploy.s.sol
+# This is needed because the Kontrol deployment is only a partial
+# version of the full Optimism deployment. Since not all the components
+# of the system are deployed, we'd get some reverts on the `mustGetAddress` functions
+awk '{gsub(/mustGetAddress/, "getAddress")}1' ${DEPLOY_SCRIPT} > temp && mv temp ${DEPLOY_SCRIPT}
+
+FOUNDRY_PROFILE=kdeploy forge script -vvv test/kontrol/KontrolDeployment.sol:KontrolDeployment --sig 'runKontrolDeployment()'
+echo "Created state diff json"
+
+# Restore the file from the backup
+cp ${DEPLOY_SCRIPT}.bak ${DEPLOY_SCRIPT}
+rm ${DEPLOY_SCRIPT}.bak
+
+# Clean and store the state diff json in snapshots/state-diff/Kontrol-Deploy.json
+JSON_SCRIPTS=test/kontrol/scripts/json
+GENERATED_STATEDIFF=Deploy.json # Name of the statediff json produced by the deployment script
+STATEDIFF=Kontrol-${GENERATED_STATEDIFF} # Name of the Kontrol statediff
+mv snapshots/state-diff/${GENERATED_STATEDIFF} snapshots/state-diff/${STATEDIFF}
+python3 ${JSON_SCRIPTS}/clean_json.py snapshots/state-diff/${STATEDIFF}
+echo "Cleaned state diff json"
+
+CONTRACT_NAMES=deployments/hardhat/.deploy
+python3 ${JSON_SCRIPTS}/reverse_key_values.py ${CONTRACT_NAMES} ${CONTRACT_NAMES}Reversed
+CONTRACT_NAMES=${CONTRACT_NAMES}Reversed
+
+SUMMARY_DIR=test/kontrol/proofs/utils
+SUMMARY_NAME=DeploymentSummary
+LICENSE=MIT
+kontrol summary ${SUMMARY_NAME} snapshots/state-diff/${STATEDIFF} --contract-names ${CONTRACT_NAMES} --output-dir ${SUMMARY_DIR} --license ${LICENSE}
+forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}.sol
+forge fmt ${SUMMARY_DIR}/${SUMMARY_NAME}Code.sol
+echo "Added state updates to ${SUMMARY_DIR}/${SUMMARY_NAME}.sol"

packages/contracts-bedrock/test/kontrol/kontrol/run-kontrol.sh → packages/contracts-bedrock/test/kontrol/scripts/run-kontrol.sh

@@ -6,11 +6,20 @@ set -euo pipefail
 #####################
 blank_line() { echo '' >&2 ; }
 notif() { echo "== $0: $*" >&2 ; }
+usage() {
+  echo "Usage: $0 [-h|--help] [container|local|dev]" 1>&2
+  echo "Options:" 1>&2
+  echo "  -h, --help         Display this help message." 1>&2
+  echo "  container          Run tests in docker container. Reproduce CI execution. (Default)" 1>&2
+  echo "  local              Run locally, enforces CI Registered .kontrolrc Kontrol version for better reproducibility. (Recommended)" 1>&2
+  echo "  dev                Run locally, do NOT enforce CI registered Kontrol version (Recomended w/ greater kup & kontrol experience)" 1>&2
+  exit 0
+}
 
 #############
 # Variables #
 #############
-# Set Script Directory Variables <root>/packages/contracts-bedrock/test/kontrol/kontrol
+# Set Script Directory Variables <root>/packages/contracts-bedrock/test/kontrol
 SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 notif "Script Home: $SCRIPT_HOME"
 blank_line
@@ -20,11 +29,50 @@ WORKSPACE_DIR=$( cd "${SCRIPT_HOME}/../../.." >/dev/null 2>&1 && pwd )
 notif "Run Directory: ${WORKSPACE_DIR}"
 blank_line
 
-export FOUNDRY_PROFILE=kontrol
+export FOUNDRY_PROFILE=kprove
 export CONTAINER_NAME=kontrol-tests
-KONTROLRC=$(jq -r .kontrol < ${WORKSPACE_DIR}/../../versions.json)
+KONTROLRC=$(jq -r .kontrol < "${WORKSPACE_DIR}/../../versions.json")
 export KONTROL_RELEASE=${KONTROLRC}
+export LOCAL=false
 
+#######################
+# Check for arguments #
+#######################
+if [ $# -gt 1 ]; then
+  usage
+else
+  if [ $# -eq 0 ] || [ "$1" == "container" ]; then
+    notif "Running in docker container (DEFAULT)"
+    blank_line
+    export LOCAL=false
+    [ $# -gt 1 ] && shift
+  elif [ "$1" == "-h" ] || [ "$1" == "--help" ]; then
+    usage
+  elif [ "$1" == "local" ]; then
+    notif "Running with LOCAL install, .kontrolrc CI version ENFORCED"
+    if [ "$(kontrol version | awk -F': ' '{print$2}')" == "${KONTROLRC}" ]; then
+      notif "Kontrol version matches ${KONTROLRC}"
+      blank_line
+      export LOCAL=true
+      shift
+      pushd "${WORKSPACE_DIR}" > /dev/null
+    else
+      notif "Kontrol version does NOT match ${KONTROLRC}"
+      notif "Please run 'kup install kontrol --version ${KONTROLRC}'"
+      blank_line
+      exit 1
+    fi
+  elif [ "$1" == "dev" ]; then
+    notif "Running with LOCAL install, IGNORING .kontrolrc version"
+    blank_line
+    export LOCAL=true
+    shift
+    pushd "${WORKSPACE_DIR}" > /dev/null
+  else
+    # Unexpected argument passed
+    usage
+  fi
+fi
 
 #############
 # Functions #
@@ -32,7 +80,7 @@ export KONTROL_RELEASE=${KONTROLRC}
 kontrol_build() {
     notif "Kontrol Build"
     # shellcheck disable=SC2086
-    docker_exec kontrol build                       \
+    run kontrol build                       \
                         --verbose                   \
                         --require ${lemmas}         \
                         --module-import ${module}   \
@@ -42,7 +90,7 @@ kontrol_build() {
 kontrol_prove() {
     notif "Kontrol Prove"
     # shellcheck disable=SC2086
-    docker_exec kontrol prove                              \
+    run kontrol prove                              \
                         --max-depth ${max_depth}           \
                         --max-iterations ${max_iterations} \
                         --smt-timeout ${smt_timeout}       \
@@ -72,47 +120,67 @@ start_docker () {
 }
 
 docker_exec () {
-    docker exec --workdir /home/user/workspace ${CONTAINER_NAME} "${@}"
+    docker exec --user user --workdir /home/user/workspace ${CONTAINER_NAME} "${@}"
 }
 
-dump_log_results(){
-  trap clean_docker ERR
-
-  notif "Something went wrong. Running cleanup..."
-  blank_line
-
-  notif "Creating Tar of Proof Results"
-  docker exec ${CONTAINER_NAME} tar -czvf results.tar.gz kout/proofs
-  RESULTS_LOG="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
-  notif "Copying Tests Results to Host"
-  docker cp ${CONTAINER_NAME}:/home/user/workspace/results.tar.gz "${RESULTS_LOG}"
-  if [ -f "${RESULTS_LOG}" ]; then
-    cp "${RESULTS_LOG}" kontrol-results_latest.tar.gz
+run () {
+  if [ "${LOCAL}" = true ]; then
+    notif "Running local"
+    # shellcheck disable=SC2086
+    "${@}"
   else
-    notif "Results Log: ${RESULTS_LOG} not found, did not pull from container."
+  notif "Running in docker"
+    docker_exec "${@}"
   fi
-  blank_line
+}
 
-  notif "Dump RUN Logs"
-  RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
-  docker logs ${CONTAINER_NAME} > "${RUN_LOG}"
+dump_log_results(){
+    trap clean_docker ERR
+    RESULTS_LOG="results-$(date +'%Y-%m-%d-%H-%M-%S').tar.gz"
+
+    notif "Generating Results Log: ${RESULTS_LOG}"
+    blank_line
+
+    run tar -czvf results.tar.gz kout-proofs/ > /dev/null 2>&1
+    if [ "${LOCAL}" = true ]; then
+      cp results.tar.gz "${RESULTS_LOG}"
+    else
+      docker cp ${CONTAINER_NAME}:/home/user/workspace/results.tar.gz "${RESULTS_LOG}"
+    fi
+    if [ -f "${RESULTS_LOG}" ]; then
+      cp "${RESULTS_LOG}" kontrol-results_latest.tar.gz
+    else
+      notif "Results Log: ${RESULTS_LOG} not found, skipping.."
+      blank_line
+    fi
+    # Report where the file was generated and placed
+    notif "Results Log: $(dirname "${RESULTS_LOG}") generated"
+
+    if [ "${LOCAL}" = false ]; then
+      notif "Results Log: ${RESULTS_LOG} generated"
+      blank_line
+      RUN_LOG="run-kontrol-$(date +'%Y-%m-%d-%H-%M-%S').log"
+      docker logs ${CONTAINER_NAME} > "${RUN_LOG}"
+    fi
 }
 
 clean_docker(){
-  notif "Stopping Docker Container"
-  docker stop ${CONTAINER_NAME}
-  blank_line
+    notif "Stopping Docker Container"
+    docker stop ${CONTAINER_NAME}
+    blank_line
 }
 
 # Define the function to run on failure
 on_failure() {
-  dump_log_results
+    dump_log_results
 
-  clean_docker
+    if [ "${LOCAL}" = false ]; then
+      clean_docker
+    fi
 
-  notif "Cleanup complete."
-  blank_line
-  exit 1
+    notif "Cleanup complete."
+    blank_line
+    exit 1
 }
 
 # Set up the trap to run the function on failure
@@ -125,20 +193,23 @@ trap on_failure ERR INT
 # such as `rekompile`. Such a pattern is intended for easy use while locally
 # developing and executing the proofs via this script. Comment/uncomment the
 # empty assignment to activate/deactivate the corresponding flag
-lemmas=test/kontrol/kontrol/pausability-lemmas.k
+lemmas=test/kontrol/pausability-lemmas.k
 base_module=PAUSABILITY-LEMMAS
-module=CounterTest:${base_module}
+module=OptimismPortalKontrol:${base_module}
 rekompile=--rekompile
 rekompile=
+regen=--regen
+# shellcheck disable=SC2034
+regen=
 
 #########################
 # kontrol prove options #
 #########################
-max_depth=10000
-max_iterations=10000
+max_depth=1000000
+max_iterations=1000000
 smt_timeout=100000
 bmc_depth=10
-workers=2
+workers=1
 reinit=--reinit
 reinit=
 break_on_calls=--no-break-on-calls
@@ -155,27 +226,32 @@ use_booster=--use-booster
 #########################################
 tests=""
 tests+="--match-test CounterTest.test_SetNumber "
+#tests+="--match-test OptimismPortalKontrol.prove_proveWithdrawalTransaction_paused "
+#tests+="--match-test OptimismPortalKontrol.prove_finalizeWithdrawalTransaction_paused "
 
 #############
 # RUN TESTS #
 #############
-
-# Is old docker container running?
-if [ "$(docker ps -q -f name=${CONTAINER_NAME})" ]; then
-    # Stop old docker container
-    notif "Stopping old docker container"
-    clean_docker
-    blank_line
+if [ "${LOCAL}" == false ]; then
+  # Is old docker container running?
+  if [ "$(docker ps -q -f name=${CONTAINER_NAME})" ]; then
+      # Stop old docker container
+      notif "Stopping old docker container"
+      clean_docker
+      blank_line
+  fi
+  start_docker
 fi
 
-start_docker
-
 kontrol_build
 kontrol_prove
 
 dump_log_results
 
-clean_docker
+if [ "${LOCAL}" == false ]; then
+    notif "Stopping docker container"
+    clean_docker
+fi
 
 blank_line
 notif "DONE"

versions.json

@@ -4,5 +4,5 @@
   "geth": "v1.13.4",
   "nvm": "v20.9.0",
   "slither": "0.10.0",
-  "kontrol": "0.1.74"
+  "kontrol": "0.1.117"
 }