From c29990e01457bd1d1d25b9e006635efa5cef1566 Mon Sep 17 00:00:00 2001 From: 0xDiscotech <131301107+0xDiscotech@users.noreply.github.com> Date: Sun, 1 Sep 2024 14:06:21 -0300 Subject: [PATCH] feat: external computation diff state wip --- packages/contracts-bedrock/.gitignore | 3 + packages/contracts-bedrock/foundry.toml | 8 +- .../supererc20-state-diff/AddressNames.json | 6 + .../supererc20-state-diff/StateDiff.json | 585 ++++++++++++++++++ .../test/properties/kontrol/KontrolBase.sol | 65 ++ ...in.k.sol => OptimismSuperchainERC20.k.sol} | 62 +- .../kontrol/deployments/InitialState.sol | 90 +++ .../kontrol/deployments/InitialStateCode.sol | 15 + .../kontrol/helpers/LibStateDiff.sol | 136 ++++ .../kontrol/helpers/RecordStateDiff.sol | 74 +++ .../kontrol/optimism-superchain-lemmas.md | 33 + .../kontrol/utils/record-state-diff.sh | 55 ++ 12 files changed, 1090 insertions(+), 42 deletions(-) create mode 100644 packages/contracts-bedrock/supererc20-state-diff/AddressNames.json create mode 100644 packages/contracts-bedrock/supererc20-state-diff/StateDiff.json create mode 100644 packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol rename packages/contracts-bedrock/test/properties/kontrol/{OptimismSuperchain.k.sol => OptimismSuperchainERC20.k.sol} (82%) create mode 100644 packages/contracts-bedrock/test/properties/kontrol/deployments/InitialState.sol create mode 100644 packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol create mode 100644 packages/contracts-bedrock/test/properties/kontrol/helpers/LibStateDiff.sol create mode 100644 packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol create mode 100644 packages/contracts-bedrock/test/properties/kontrol/optimism-superchain-lemmas.md create mode 100644 packages/contracts-bedrock/test/properties/kontrol/utils/record-state-diff.sh diff --git a/packages/contracts-bedrock/.gitignore b/packages/contracts-bedrock/.gitignore index 6ecdd53bc7b6..e0676cfa0fd5 100644 --- a/packages/contracts-bedrock/.gitignore +++ b/packages/contracts-bedrock/.gitignore @@ -42,3 +42,6 @@ deploy-config/devnetL1.json # Getting Started guide deploy config deploy-config/getting-started.json + +# Supererc20 kontrol +out-kontrol-properties/ \ No newline at end of file diff --git a/packages/contracts-bedrock/foundry.toml b/packages/contracts-bedrock/foundry.toml index 0c82189413ce..db14a7f6bb8b 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -112,4 +112,10 @@ script = 'test/properties/halmos/' src = "test/properties/kontrol" test = "test/properties/kontrol" script = "test/properties/kontrol" -out = 'out' \ No newline at end of file +out = 'out-kontrol-properties' +# Make sure to export the variables $STATE_DIFF_DIR and $STATE_DIFF_NAME in your shell +fs_permissions = [ + { access = 'read', path = './supererc20-state-diff' }, + { access = 'read-write', path = './supererc20-state-diff/StateDiff.json' }, + { access = 'read-write', path = './supererc20-state-diff/AddressNames.json' } +] \ No newline at end of file diff --git a/packages/contracts-bedrock/supererc20-state-diff/AddressNames.json b/packages/contracts-bedrock/supererc20-state-diff/AddressNames.json new file mode 100644 index 000000000000..d94c12b6939f --- /dev/null +++ b/packages/contracts-bedrock/supererc20-state-diff/AddressNames.json @@ -0,0 +1,6 @@ +{ + "0x2e234DAe75C793f67A35089C9d99245E1C58470b": "sourceToken", + "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f": "superchainERC20Impl", + "0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9": "mockL2ToL2Messenger", + "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a": "destToken" +} \ No newline at end of file diff --git a/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json b/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json new file mode 100644 index 000000000000..f1dba0541bbf --- /dev/null +++ b/packages/contracts-bedrock/supererc20-state-diff/StateDiff.json @@ -0,0 +1,585 @@ +{ + "accountAccesses": [ + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x6080604052348015600e575f80fd5b5060156019565b60c9565b7ff0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00805468010000000000000000900460ff161560685760405163f92ee8a960e01b815260040160405180910390fd5b80546001600160401b039081161460c65780546001600160401b0319166001600160401b0390811782556040519081527fc7f505b2f371ae2175ee4913f4499e1f2633a7b5936321eed1cdaeb6115181d29060200160405180910390a15b50565b6117bd806100d65f395ff3fe608060405234801561000f575f80fd5b5060043610610163575f3560e01c806378a3727b116100c7578063d505accf1161007d578063d9f5004611610063578063d9f5004614610356578063dd62ed3e14610369578063f6d2ee8614610391575f80fd5b8063d505accf146102fc578063d6c0b2c41461030f575f80fd5b806395d89b41116100ad57806395d89b41146102ce5780639dc29fac146102d6578063a9059cbb146102e9575f80fd5b806378a3727b146102965780637ecebe00146102a9575f80fd5b8063313ce5671161011c57806340c10f191161010257806340c10f191461022057806354fd4d501461023557806370a0823114610271575f80fd5b8063313ce567146101e45780633644e51514610218575f80fd5b8063095ea7b31161014c578063095ea7b3146101a457806318160ddd146101b757806323b872dd146101d1575f80fd5b806301ffc9a71461016757806306fdde031461018f575b5f80fd5b61017a610175366004611201565b6103a4565b60405190151581526020015b60405180910390f35b61019761043c565b6040516101869190611293565b61017a6101b23660046112c9565b6104ee565b6805345cdf77eb68f44c545b604051908152602001610186565b61017a6101df3660046112f3565b61053d565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb035460405160ff9091168152602001610186565b6101c36105f7565b61023361022e3660046112c9565b610673565b005b6101976040518060400160405280600c81526020017f312e302e302d626574612e31000000000000000000000000000000000000000081525081565b6101c361027f366004611331565b6387a211a2600c9081525f91909152602090205490565b6102336102a436600461134c565b61076b565b6101c36102b7366004611331565b6338377508600c9081525f91909152602090205490565b610197610923565b6102336102e43660046112c9565b610954565b61017a6102f73660046112c9565b610a40565b61023361030a366004611393565b610ab7565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb005460405173ffffffffffffffffffffffffffffffffffffffff9091168152602001610186565b6102336103643660046112f3565b610c4a565b6101c36103773660046113fc565b602052637f5e9f20600c9081525f91909152603490205490565b61023361039f366004611507565b610ebf565b5f7fffffffff0000000000000000000000000000000000000000000000000000000082167f0bc3227100000000000000000000000000000000000000000000000000000000148061043657507f01ffc9a7000000000000000000000000000000000000000000000000000000007fffffffff000000000000000000000000000000000000000000000000000000008316145b92915050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600101805461046d90611589565b80601f016020809104026020016040519081016040528092919081815260200182805461049990611589565b80156104e45780601f106104bb576101008083540402835291602001916104e4565b820191905f5260205f20905b8154815290600101906020018083116104c757829003601f168201915b5050505050905090565b5f82602052637f5e9f20600c52335f52816034600c2055815f52602c5160601c337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560205fa350600192915050565b5f8360601b33602052637f5e9f208117600c526034600c208054600181011561057b5780851115610575576313be252b5f526004601cfd5b84810382555b50506387a211a28117600c526020600c208054808511156105a35763f4d678b85f526004601cfd5b84810382555050835f526020600c208381540181555082602052600c5160601c8160601c7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a3505060019392505050565b5f8061060161043c565b8051906020012090506040517f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f81528160208201527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604082015246606082015230608082015260a081209250505090565b33734200000000000000000000000000000000000010146106c0576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff821661070d576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107178282611104565b8173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d41213968858260405161075f91815260200190565b60405180910390a25050565b73ffffffffffffffffffffffffffffffffffffffff83166107b8576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107c23383611180565b6040805133602482015273ffffffffffffffffffffffffffffffffffffffff85166044820152606480820185905282518083039091018152608490910182526020810180517bffffffffffffffffffffffffffffffffffffffffffffffffffffffff167fd9f500460000000000000000000000000000000000000000000000000000000017905290517f7056f41f00000000000000000000000000000000000000000000000000000000815273420000000000000000000000000000000000002390637056f41f9061089c908590309086906004016115da565b5f604051808303815f87803b1580156108b3575f80fd5b505af11580156108c5573d5f803e3d5ffd5b5050604080518681526020810186905273ffffffffffffffffffffffffffffffffffffffff881693503392507ffcea3600a13c757f2758710b089cc9752781c35d2a9d6804370ed18cd82f0bb691015b60405180910390a350505050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600201805461046d90611589565b33734200000000000000000000000000000000000010146109a1576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff82166109ee576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6109f88282611180565b8173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca58260405161075f91815260200190565b5f6387a211a2600c52335f526020600c20805480841115610a685763f4d678b85f526004601cfd5b83810382555050825f526020600c208281540181555081602052600c5160601c337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a350600192915050565b5f610ac061043c565b80519060200120905084421115610ade57631a15a3cc5f526004601cfd5b6040518860601b60601c98508760601b60601c975065383775081901600e52885f526020600c2080547f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f83528360208401527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604084015246606084015230608084015260a08320602e527f6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c983528a60208401528960408401528860608401528060808401528760a084015260c08320604e526042602c205f528660ff16602052856040528460605260208060805f60015afa8b3d5114610be65763ddafbaef5f526004601cfd5b019055777f5e9f20000000000000000000000000000000000000000088176040526034602c2087905587897f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925602060608501a360405250505f606052505050505050565b73ffffffffffffffffffffffffffffffffffffffff8216610c97576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3373420000000000000000000000000000000000002314610ce4576040517f065d515000000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3073ffffffffffffffffffffffffffffffffffffffff1673420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff166338ffde186040518163ffffffff1660e01b8152600401602060405180830381865afa158015610d58573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610d7c9190611617565b73ffffffffffffffffffffffffffffffffffffffff1614610dc9576040517fbc22e2aa00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b5f73420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff1663247944626040518163ffffffff1660e01b8152600401602060405180830381865afa158015610e27573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610e4b9190611632565b9050610e578383611104565b8273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fc75e22a0b57fb7740dbfc0caa5c6b7a82a2139964e7f1b7be7ac4e8be0f719ba8484604051610915929190918252602082015260400190565b7ff0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00805468010000000000000000810460ff16159067ffffffffffffffff165f81158015610f095750825b90505f8267ffffffffffffffff166001148015610f255750303b155b905081158015610f33575080155b15610f6a576040517ff92ee8a900000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b84547fffffffffffffffffffffffffffffffffffffffffffffffff00000000000000001660011785558315610fcb5784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff16680100000000000000001785555b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb0080547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff8b161781557f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb016110558a82611694565b50600281016110648982611694565b5060030180547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff001660ff881617905583156110f45784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff168555604051600181527fc7f505b2f371ae2175ee4913f4499e1f2633a7b5936321eed1cdaeb6115181d29060200160405180910390a15b505050505050505050565b505050565b6805345cdf77eb68f44c54818101818110156111275763e5cfe9575f526004601cfd5b806805345cdf77eb68f44c5550506387a211a2600c52815f526020600c208181540181555080602052600c5160601c5f7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a35050565b6387a211a2600c52815f526020600c208054808311156111a75763f4d678b85f526004601cfd5b82900390556805345cdf77eb68f44c805482900390555f81815273ffffffffffffffffffffffffffffffffffffffff83167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602083a35050565b5f60208284031215611211575f80fd5b81357fffffffff0000000000000000000000000000000000000000000000000000000081168114611240575f80fd5b9392505050565b5f81518084528060208401602086015e5f6020828601015260207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011685010191505092915050565b602081525f6112406020830184611247565b73ffffffffffffffffffffffffffffffffffffffff811681146112c6575f80fd5b50565b5f80604083850312156112da575f80fd5b82356112e5816112a5565b946020939093013593505050565b5f805f60608486031215611305575f80fd5b8335611310816112a5565b92506020840135611320816112a5565b929592945050506040919091013590565b5f60208284031215611341575f80fd5b8135611240816112a5565b5f805f6060848603121561135e575f80fd5b8335611369816112a5565b95602085013595506040909401359392505050565b803560ff8116811461138e575f80fd5b919050565b5f805f805f805f60e0888a0312156113a9575f80fd5b87356113b4816112a5565b965060208801356113c4816112a5565b955060408801359450606088013593506113e06080890161137e565b925060a0880135915060c0880135905092959891949750929550565b5f806040838503121561140d575f80fd5b8235611418816112a5565b91506020830135611428816112a5565b809150509250929050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52604160045260245ffd5b5f82601f83011261146f575f80fd5b813567ffffffffffffffff8082111561148a5761148a611433565b604051601f83017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0908116603f011681019082821181831017156114d0576114d0611433565b816040528381528660208588010111156114e8575f80fd5b836020870160208301375f602085830101528094505050505092915050565b5f805f806080858703121561151a575f80fd5b8435611525816112a5565b9350602085013567ffffffffffffffff80821115611541575f80fd5b61154d88838901611460565b94506040870135915080821115611562575f80fd5b5061156f87828801611460565b92505061157e6060860161137e565b905092959194509250565b600181811c9082168061159d57607f821691505b6020821081036115d4577f4e487b71000000000000000000000000000000000000000000000000000000005f52602260045260245ffd5b50919050565b83815273ffffffffffffffffffffffffffffffffffffffff83166020820152606060408201525f61160e6060830184611247565b95945050505050565b5f60208284031215611627575f80fd5b8151611240816112a5565b5f60208284031215611642575f80fd5b5051919050565b601f8211156110ff57805f5260205f20601f840160051c8101602085101561166e5750805b601f840160051c820191505b8181101561168d575f815560010161167a565b5050505050565b815167ffffffffffffffff8111156116ae576116ae611433565b6116c2816116bc8454611589565b84611649565b602080601f831160018114611714575f84156116de5750858301515b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600386901b1c1916600185901b1785556117a8565b5f858152602081207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe08616915b8281101561176057888601518255948401946001909101908401611741565b508582101561179c57878501517fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600388901b60f8161c191681555b505060018460011b0185555b50505050505056fea164736f6c6343000819000a", + "deployedCode": "0x608060405234801561000f575f80fd5b5060043610610163575f3560e01c806378a3727b116100c7578063d505accf1161007d578063d9f5004611610063578063d9f5004614610356578063dd62ed3e14610369578063f6d2ee8614610391575f80fd5b8063d505accf146102fc578063d6c0b2c41461030f575f80fd5b806395d89b41116100ad57806395d89b41146102ce5780639dc29fac146102d6578063a9059cbb146102e9575f80fd5b806378a3727b146102965780637ecebe00146102a9575f80fd5b8063313ce5671161011c57806340c10f191161010257806340c10f191461022057806354fd4d501461023557806370a0823114610271575f80fd5b8063313ce567146101e45780633644e51514610218575f80fd5b8063095ea7b31161014c578063095ea7b3146101a457806318160ddd146101b757806323b872dd146101d1575f80fd5b806301ffc9a71461016757806306fdde031461018f575b5f80fd5b61017a610175366004611201565b6103a4565b60405190151581526020015b60405180910390f35b61019761043c565b6040516101869190611293565b61017a6101b23660046112c9565b6104ee565b6805345cdf77eb68f44c545b604051908152602001610186565b61017a6101df3660046112f3565b61053d565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb035460405160ff9091168152602001610186565b6101c36105f7565b61023361022e3660046112c9565b610673565b005b6101976040518060400160405280600c81526020017f312e302e302d626574612e31000000000000000000000000000000000000000081525081565b6101c361027f366004611331565b6387a211a2600c9081525f91909152602090205490565b6102336102a436600461134c565b61076b565b6101c36102b7366004611331565b6338377508600c9081525f91909152602090205490565b610197610923565b6102336102e43660046112c9565b610954565b61017a6102f73660046112c9565b610a40565b61023361030a366004611393565b610ab7565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb005460405173ffffffffffffffffffffffffffffffffffffffff9091168152602001610186565b6102336103643660046112f3565b610c4a565b6101c36103773660046113fc565b602052637f5e9f20600c9081525f91909152603490205490565b61023361039f366004611507565b610ebf565b5f7fffffffff0000000000000000000000000000000000000000000000000000000082167f0bc3227100000000000000000000000000000000000000000000000000000000148061043657507f01ffc9a7000000000000000000000000000000000000000000000000000000007fffffffff000000000000000000000000000000000000000000000000000000008316145b92915050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600101805461046d90611589565b80601f016020809104026020016040519081016040528092919081815260200182805461049990611589565b80156104e45780601f106104bb576101008083540402835291602001916104e4565b820191905f5260205f20905b8154815290600101906020018083116104c757829003601f168201915b5050505050905090565b5f82602052637f5e9f20600c52335f52816034600c2055815f52602c5160601c337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560205fa350600192915050565b5f8360601b33602052637f5e9f208117600c526034600c208054600181011561057b5780851115610575576313be252b5f526004601cfd5b84810382555b50506387a211a28117600c526020600c208054808511156105a35763f4d678b85f526004601cfd5b84810382555050835f526020600c208381540181555082602052600c5160601c8160601c7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a3505060019392505050565b5f8061060161043c565b8051906020012090506040517f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f81528160208201527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604082015246606082015230608082015260a081209250505090565b33734200000000000000000000000000000000000010146106c0576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff821661070d576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107178282611104565b8173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d41213968858260405161075f91815260200190565b60405180910390a25050565b73ffffffffffffffffffffffffffffffffffffffff83166107b8576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107c23383611180565b6040805133602482015273ffffffffffffffffffffffffffffffffffffffff85166044820152606480820185905282518083039091018152608490910182526020810180517bffffffffffffffffffffffffffffffffffffffffffffffffffffffff167fd9f500460000000000000000000000000000000000000000000000000000000017905290517f7056f41f00000000000000000000000000000000000000000000000000000000815273420000000000000000000000000000000000002390637056f41f9061089c908590309086906004016115da565b5f604051808303815f87803b1580156108b3575f80fd5b505af11580156108c5573d5f803e3d5ffd5b5050604080518681526020810186905273ffffffffffffffffffffffffffffffffffffffff881693503392507ffcea3600a13c757f2758710b089cc9752781c35d2a9d6804370ed18cd82f0bb691015b60405180910390a350505050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600201805461046d90611589565b33734200000000000000000000000000000000000010146109a1576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff82166109ee576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6109f88282611180565b8173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca58260405161075f91815260200190565b5f6387a211a2600c52335f526020600c20805480841115610a685763f4d678b85f526004601cfd5b83810382555050825f526020600c208281540181555081602052600c5160601c337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a350600192915050565b5f610ac061043c565b80519060200120905084421115610ade57631a15a3cc5f526004601cfd5b6040518860601b60601c98508760601b60601c975065383775081901600e52885f526020600c2080547f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f83528360208401527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604084015246606084015230608084015260a08320602e527f6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c983528a60208401528960408401528860608401528060808401528760a084015260c08320604e526042602c205f528660ff16602052856040528460605260208060805f60015afa8b3d5114610be65763ddafbaef5f526004601cfd5b019055777f5e9f20000000000000000000000000000000000000000088176040526034602c2087905587897f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925602060608501a360405250505f606052505050505050565b73ffffffffffffffffffffffffffffffffffffffff8216610c97576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3373420000000000000000000000000000000000002314610ce4576040517f065d515000000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3073ffffffffffffffffffffffffffffffffffffffff1673420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff166338ffde186040518163ffffffff1660e01b8152600401602060405180830381865afa158015610d58573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610d7c9190611617565b73ffffffffffffffffffffffffffffffffffffffff1614610dc9576040517fbc22e2aa00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b5f73420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff1663247944626040518163ffffffff1660e01b8152600401602060405180830381865afa158015610e27573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610e4b9190611632565b9050610e578383611104565b8273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fc75e22a0b57fb7740dbfc0caa5c6b7a82a2139964e7f1b7be7ac4e8be0f719ba8484604051610915929190918252602082015260400190565b7ff0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00805468010000000000000000810460ff16159067ffffffffffffffff165f81158015610f095750825b90505f8267ffffffffffffffff166001148015610f255750303b155b905081158015610f33575080155b15610f6a576040517ff92ee8a900000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b84547fffffffffffffffffffffffffffffffffffffffffffffffff00000000000000001660011785558315610fcb5784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff16680100000000000000001785555b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb0080547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff8b161781557f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb016110558a82611694565b50600281016110648982611694565b5060030180547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff001660ff881617905583156110f45784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff168555604051600181527fc7f505b2f371ae2175ee4913f4499e1f2633a7b5936321eed1cdaeb6115181d29060200160405180910390a15b505050505050505050565b505050565b6805345cdf77eb68f44c54818101818110156111275763e5cfe9575f526004601cfd5b806805345cdf77eb68f44c5550506387a211a2600c52815f526020600c208181540181555080602052600c5160601c5f7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a35050565b6387a211a2600c52815f526020600c208054808311156111a75763f4d678b85f526004601cfd5b82900390556805345cdf77eb68f44c805482900390555f81815273ffffffffffffffffffffffffffffffffffffffff83167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602083a35050565b5f60208284031215611211575f80fd5b81357fffffffff0000000000000000000000000000000000000000000000000000000081168114611240575f80fd5b9392505050565b5f81518084528060208401602086015e5f6020828601015260207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011685010191505092915050565b602081525f6112406020830184611247565b73ffffffffffffffffffffffffffffffffffffffff811681146112c6575f80fd5b50565b5f80604083850312156112da575f80fd5b82356112e5816112a5565b946020939093013593505050565b5f805f60608486031215611305575f80fd5b8335611310816112a5565b92506020840135611320816112a5565b929592945050506040919091013590565b5f60208284031215611341575f80fd5b8135611240816112a5565b5f805f6060848603121561135e575f80fd5b8335611369816112a5565b95602085013595506040909401359392505050565b803560ff8116811461138e575f80fd5b919050565b5f805f805f805f60e0888a0312156113a9575f80fd5b87356113b4816112a5565b965060208801356113c4816112a5565b955060408801359450606088013593506113e06080890161137e565b925060a0880135915060c0880135905092959891949750929550565b5f806040838503121561140d575f80fd5b8235611418816112a5565b91506020830135611428816112a5565b809150509250929050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52604160045260245ffd5b5f82601f83011261146f575f80fd5b813567ffffffffffffffff8082111561148a5761148a611433565b604051601f83017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0908116603f011681019082821181831017156114d0576114d0611433565b816040528381528660208588010111156114e8575f80fd5b836020870160208301375f602085830101528094505050505092915050565b5f805f806080858703121561151a575f80fd5b8435611525816112a5565b9350602085013567ffffffffffffffff80821115611541575f80fd5b61154d88838901611460565b94506040870135915080821115611562575f80fd5b5061156f87828801611460565b92505061157e6060860161137e565b905092959194509250565b600181811c9082168061159d57607f821691505b6020821081036115d4577f4e487b71000000000000000000000000000000000000000000000000000000005f52602260045260245ffd5b50919050565b83815273ffffffffffffffffffffffffffffffffffffffff83166020820152606060408201525f61160e6060830184611247565b95945050505050565b5f60208284031215611627575f80fd5b8151611240816112a5565b5f60208284031215611642575f80fd5b5051919050565b601f8211156110ff57805f5260205f20601f840160051c8101602085101561166e5750805b601f840160051c820191505b8181101561168d575f815560010161167a565b5050505050565b815167ffffffffffffffff8111156116ae576116ae611433565b6116c2816116bc8454611589565b84611649565b602080601f831160018114611714575f84156116de5750858301515b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600386901b1c1916600185901b1785556117a8565b5f858152602081207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe08616915b8281101561176057888601518255948401946001909101908401611741565b508582101561179c57878501517fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600388901b60f8161c191681555b505060018460011b0185555b50505050505056fea164736f6c6343000819000a", + "initialized": true, + "kind": "Create", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [ + { + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "isWrite": true, + "newValue": "0x000000000000000000000000000000000000000000000000ffffffffffffffff", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + } + ], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x60806040526040516103ae3803806103ae8339810160408190526100229161023c565b61002c8282610033565b505061031b565b61003c82610091565b6040516001600160a01b038316907fbc7cd75a20ee27fd9adebab32041f755214dbc6bffa90cc0225b39da2e5c2d3b905f90a280511561008557610080828261010c565b505050565b61008d61017f565b5050565b806001600160a01b03163b5f036100cb57604051634c9c8ce360e01b81526001600160a01b03821660048201526024015b60405180910390fd5b7f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc80546001600160a01b0319166001600160a01b0392909216919091179055565b60605f80846001600160a01b0316846040516101289190610305565b5f60405180830381855af49150503d805f8114610160576040519150601f19603f3d011682016040523d82523d5f602084013e610165565b606091505b5090925090506101768583836101a0565b95945050505050565b341561019e5760405163b398979f60e01b815260040160405180910390fd5b565b6060826101b5576101b0826101ff565b6101f8565b81511580156101cc57506001600160a01b0384163b155b156101f557604051639996b31560e01b81526001600160a01b03851660048201526024016100c2565b50805b9392505050565b80511561020f5780518082602001fd5b604051630a12f52160e11b815260040160405180910390fd5b634e487b7160e01b5f52604160045260245ffd5b5f806040838503121561024d575f80fd5b82516001600160a01b0381168114610263575f80fd5b60208401519092506001600160401b038082111561027f575f80fd5b818501915085601f830112610292575f80fd5b8151818111156102a4576102a4610228565b604051601f8201601f19908116603f011681019083821181831017156102cc576102cc610228565b816040528281528860208487010111156102e4575f80fd5b8260208601602083015e5f6020848301015280955050505050509250929050565b5f82518060208501845e5f920191825250919050565b6087806103275f395ff3fe6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f00000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000000000104f6d2ee86000000000000000000000000237a66474b7b934b22574359500212977b656d9f000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000000000000000c00000000000000000000000000000000000000000000000000000000000000012000000000000000000000000000000000000000000000000000000000000000f5375706572636861696e455243323000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005535550455200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "deployedCode": "0x6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a", + "initialized": true, + "kind": "Create", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [ + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc" + } + ], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0xf6d2ee86000000000000000000000000237a66474b7b934b22574359500212977b656d9f000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000000000000000c00000000000000000000000000000000000000000000000000000000000000012000000000000000000000000000000000000000000000000000000000000000f5375706572636861696e4552433230000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000055355504552000000000000000000000000000000000000000000000000000000", + "deployedCode": "0x", + "initialized": true, + "kind": "DelegateCall", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [ + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x000000000000000000000000237a66474b7b934b22574359500212977b656d9f", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x5375706572636861696e4552433230000000000000000000000000000000001e", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x535550455200000000000000000000000000000000000000000000000000000a", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000012", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + } + ], + "value": 0 + }, + { + "accessor": "0x2e234DAe75C793f67A35089C9d99245E1C58470b", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x60806040526040516103ae3803806103ae8339810160408190526100229161023c565b61002c8282610033565b505061031b565b61003c82610091565b6040516001600160a01b038316907fbc7cd75a20ee27fd9adebab32041f755214dbc6bffa90cc0225b39da2e5c2d3b905f90a280511561008557610080828261010c565b505050565b61008d61017f565b5050565b806001600160a01b03163b5f036100cb57604051634c9c8ce360e01b81526001600160a01b03821660048201526024015b60405180910390fd5b7f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc80546001600160a01b0319166001600160a01b0392909216919091179055565b60605f80846001600160a01b0316846040516101289190610305565b5f60405180830381855af49150503d805f8114610160576040519150601f19603f3d011682016040523d82523d5f602084013e610165565b606091505b5090925090506101768583836101a0565b95945050505050565b341561019e5760405163b398979f60e01b815260040160405180910390fd5b565b6060826101b5576101b0826101ff565b6101f8565b81511580156101cc57506001600160a01b0384163b155b156101f557604051639996b31560e01b81526001600160a01b03851660048201526024016100c2565b50805b9392505050565b80511561020f5780518082602001fd5b604051630a12f52160e11b815260040160405180910390fd5b634e487b7160e01b5f52604160045260245ffd5b5f806040838503121561024d575f80fd5b82516001600160a01b0381168114610263575f80fd5b60208401519092506001600160401b038082111561027f575f80fd5b818501915085601f830112610292575f80fd5b8151818111156102a4576102a4610228565b604051601f8201601f19908116603f011681019083821181831017156102cc576102cc610228565b816040528281528860208487010111156102e4575f80fd5b8260208601602083015e5f6020848301015280955050505050509250929050565b5f82518060208501845e5f920191825250919050565b6087806103275f395ff3fe6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f00000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000000000104f6d2ee86000000000000000000000000237a66474b7b934b22574359500212977b656d9f000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000000000000000c00000000000000000000000000000000000000000000000000000000000000012000000000000000000000000000000000000000000000000000000000000000f5375706572636861696e455243323000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005535550455200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "deployedCode": "0x6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a", + "initialized": true, + "kind": "Create", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [ + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc" + } + ], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0xf6d2ee86000000000000000000000000237a66474b7b934b22574359500212977b656d9f000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000000000000000c00000000000000000000000000000000000000000000000000000000000000012000000000000000000000000000000000000000000000000000000000000000f5375706572636861696e4552433230000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000055355504552000000000000000000000000000000000000000000000000000000", + "deployedCode": "0x", + "initialized": true, + "kind": "DelegateCall", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [ + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x000000000000000000000000237a66474b7b934b22574359500212977b656d9f", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x5375706572636861696e4552433230000000000000000000000000000000001e", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x535550455200000000000000000000000000000000000000000000000000000a", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000012", + "previousValue": "0x0000000000000000000000000000000000000000000000000000000000000000", + "reverted": false, + "slot": "0x07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": false, + "newValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + }, + { + "account": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "isWrite": true, + "newValue": "0x0000000000000000000000000000000000000000000000000000000000000001", + "previousValue": "0x0000000000000000000000000000000000000000000000010000000000000001", + "reverted": false, + "slot": "0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00" + } + ], + "value": 0 + }, + { + "accessor": "0xF62849F9A0B5Bf2913b396098F7c7019b51A820a", + "account": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x610100604052348015610010575f80fd5b5060405161070538038061070583398101604081905261002f9161006a565b6001600160a01b0393841660805291831660a05260c0521660e0526100b4565b80516001600160a01b0381168114610065575f80fd5b919050565b5f805f806080858703121561007d575f80fd5b6100868561004f565b93506100946020860161004f565b9250604085015191506100a96060860161004f565b905092959194509250565b60805160a05160c05160e0516106036101025f395f6102ab01525f818160a901526102cf01525f818161025d0152818161028601526102fa01525f81816101fb015261022401526106035ff3fe608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000081565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000000000000000000000000000000000000000000016330361024657507f000000000000000000000000000000000000000000000000000000000000000090565b73ffffffffffffffffffffffffffffffffffffffff7f00000000000000000000000000000000000000000000000000000000000000001633036102a857507f000000000000000000000000000000000000000000000000000000000000000090565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000084036103e6575f6103557f00000000000000000000000000000000000000000000000000000000000000005f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000", + "deployedCode": "0x608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000281565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361024657507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036102a857507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000284036103e6575f6103557f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a", + "initialized": true, + "kind": "Create", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x7109709ECfa91a80626fF3989D68f67F5b1DD12D", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x7109709ECfa91a80626fF3989D68f67F5b1DD12D", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x7109709ECfa91a80626fF3989D68f67F5b1DD12D", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + }, + { + "accessor": "0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496", + "account": "0x7109709ECfa91a80626fF3989D68f67F5b1DD12D", + "chainInfo": { + "chainId": 31337, + "forkId": 0 + }, + "data": "0x", + "deployedCode": "0x", + "initialized": true, + "kind": "Resume", + "newBalance": 0, + "oldBalance": 0, + "reverted": false, + "storageAccesses": [], + "value": 0 + } + ] +} \ No newline at end of file diff --git a/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol b/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol new file mode 100644 index 000000000000..283c4e639113 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol @@ -0,0 +1,65 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; +import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol"; +import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol"; +import { RecordStateDiff } from "./helpers/RecordStateDiff.sol"; +import { Test } from "forge-std/Test.sol"; + +contract KontrolBase is Test, KontrolCheats, RecordStateDiff { + uint256 internal constant CURRENT_CHAIN_ID = 1; + uint256 internal constant DESTINATION_CHAIN_ID = 2; + uint256 internal constant ZERO_AMOUNT = 0; + + MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); + + address internal remoteToken = address(bytes20(keccak256("remoteToken"))); + string internal name = "SuperchainERC20"; + string internal symbol = "SUPER"; + uint8 internal decimals = 18; + + OptimismSuperchainERC20 public superchainERC20Impl; + OptimismSuperchainERC20 internal sourceToken; + OptimismSuperchainERC20 internal destToken; + MockL2ToL2Messenger internal mockL2ToL2Messenger; + + // The second function to get the state diff saving the addresses with their names + function setUpNamed() public virtual recordStateDiff { + // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used + superchainERC20Impl = new OptimismSuperchainERC20(); + sourceToken = OptimismSuperchainERC20( + address( + // TODO: Update to beacon proxy + new ERC1967Proxy( + address(superchainERC20Impl), + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) + ) + ) + ); + + destToken = OptimismSuperchainERC20( + address( + // TODO: Update to beacon proxy + new ERC1967Proxy( + address(superchainERC20Impl), + abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) + ) + ) + ); + + mockL2ToL2Messenger = + new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0)); + + save_address(address(superchainERC20Impl), "superchainERC20Impl"); + save_address(address(sourceToken), "sourceToken"); + save_address(address(destToken), "destToken"); + save_address(address(mockL2ToL2Messenger), "mockL2ToL2Messenger"); + } + + function eqStrings(string memory a, string memory b) internal pure returns (bool) { + return keccak256(abi.encode(a)) == keccak256(abi.encode(b)); + } +} diff --git a/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchain.k.sol b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol similarity index 82% rename from packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchain.k.sol rename to packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol index 94116cf536e2..ca73d5586123 100644 --- a/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchain.k.sol +++ b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol @@ -3,52 +3,22 @@ pragma solidity 0.8.25; import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; import { Predeploys } from "src/libraries/Predeploys.sol"; -import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; import { MockL2ToL2Messenger } from "test/properties/halmos/MockL2ToL2Messenger.sol"; -import { HalmosBase } from "test/properties/helpers/HalmosBase.sol"; -import { KontrolCheats } from "kontrol-cheatcodes/KontrolCheats.sol"; - -contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase { - MockL2ToL2Messenger internal constant MESSENGER = MockL2ToL2Messenger(Predeploys.L2_TO_L2_CROSS_DOMAIN_MESSENGER); - - OptimismSuperchainERC20 public superchainERC20Impl; - OptimismSuperchainERC20 internal sourceToken; - OptimismSuperchainERC20 internal destToken; - - function setUp() public { - // Deploy the OptimismSuperchainERC20 contract implementation and the proxy to be used - superchainERC20Impl = new OptimismSuperchainERC20(); - sourceToken = OptimismSuperchainERC20( - address( - // TODO: Update to beacon proxy - new ERC1967Proxy( - address(superchainERC20Impl), - abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) - ) - ) - ); - - destToken = OptimismSuperchainERC20( - address( - // TODO: Update to beacon proxy - new ERC1967Proxy( - address(superchainERC20Impl), - abi.encodeCall(OptimismSuperchainERC20.initialize, (remoteToken, name, symbol, decimals)) - ) - ) - ); - - // Etch the mocked L2 to L2 Messenger since the messenger logic is out of scope for these test suite. Also, we - // avoid issues such as `TSTORE` opcode not being supported, or issues with `encodeVersionedNonce()` - address _mockL2ToL2CrossDomainMessenger = - address(new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, address(0))); - vm.etch(address(MESSENGER), _mockL2ToL2CrossDomainMessenger.code); - // NOTE: We need to set the crossDomainMessageSender as an immutable or otherwise storage vars and not taken - // into account when etching on halmos. Setting a constant slot with setters and getters didn't work neither. +import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol"; +import { InitialState } from "./deployments/InitialState.sol"; + +contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { + function setUpInlined() public { + superchainERC20Impl = OptimismSuperchainERC20(superchainERC20ImplAddress); + sourceToken = OptimismSuperchainERC20(sourceTokenAddress); + destToken = OptimismSuperchainERC20(destTokenAddress); + vm.etch(address(MESSENGER), mockL2ToL2MessengerAddress.code); } /// @notice Check setup works as expected function prove_setup() public { + setUpInlined(); + // Source token assert(sourceToken.remoteToken() == remoteToken); assert(eqStrings(sourceToken.name(), name)); @@ -68,6 +38,8 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase { // Custom cross domain sender assert(MESSENGER.crossDomainMessageSender() == address(0)); + + assert(block.chainid >= 0); } /// @custom:property-id 6 @@ -81,10 +53,15 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase { ) public { + setUpInlined(); + /* Preconditions */ vm.assume(_to != address(0)); vm.assume(_from != address(0)); + notBuiltinAddress(_from); + notBuiltinAddress(_to); + // Can't deal to unsupported cheatcode vm.prank(Predeploys.L2_STANDARD_BRIDGE); sourceToken.mint(_from, _initialBalance); @@ -136,6 +113,9 @@ contract OptimismSuperchainERC20Kontrol is KontrolCheats, HalmosBase { vm.assume(_to != address(0)); vm.assume(_to != address(Predeploys.CROSS_L2_INBOX) && _to != address(MESSENGER)); + notBuiltinAddress(_from); + notBuiltinAddress(_to); + uint256 _totalSupplyBefore = sourceToken.totalSupply(); uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); uint256 _toBalanceBefore = sourceToken.balanceOf(_to); diff --git a/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialState.sol b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialState.sol new file mode 100644 index 000000000000..cb47c362f4f6 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialState.sol @@ -0,0 +1,90 @@ +// SPDX-License-Identifier: UNLICENSED +// This file was autogenerated by running `kontrol load-state`. Do not edit this file manually. + +pragma solidity ^0.8.13; + +import { Vm } from "forge-std/Vm.sol"; + +import { InitialStateCode } from "./InitialStateCode.sol"; + +contract InitialState is InitialStateCode { + // Test contract address, 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 + address private constant FOUNDRY_TEST_ADDRESS = 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496; + // Cheat code address, 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D + address private constant VM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); + Vm private constant vm = Vm(VM_ADDRESS); + + address internal constant sourceTokenAddress = 0x2e234DAe75C793f67A35089C9d99245E1C58470b; + address internal constant superchainERC20ImplAddress = 0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f; + address internal constant mockL2ToL2MessengerAddress = 0x5991A2dF15A8F6A256D3Ec51E99254Cd3fb576A9; + address internal constant destTokenAddress = 0xF62849F9A0B5Bf2913b396098F7c7019b51A820a; + + function recreateState() public { + bytes32 slot; + bytes32 value; + vm.etch(superchainERC20ImplAddress, superchainERC20ImplCode); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"000000000000000000000000000000000000000000000000ffffffffffffffff"; + vm.store(superchainERC20ImplAddress, slot, value); + vm.etch(sourceTokenAddress, sourceTokenCode); + slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc"; + value = hex"0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000000000000000000001"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000010000000000000001"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00"; + value = hex"000000000000000000000000237a66474b7b934b22574359500212977b656d9f"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01"; + value = hex"5375706572636861696e4552433230000000000000000000000000000000001e"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02"; + value = hex"535550455200000000000000000000000000000000000000000000000000000a"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03"; + value = hex"0000000000000000000000000000000000000000000000000000000000000012"; + vm.store(sourceTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000000000000000000001"; + vm.store(sourceTokenAddress, slot, value); + vm.etch(destTokenAddress, destTokenCode); + slot = hex"360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc"; + value = hex"0000000000000000000000005615deb798bb3e4dfa0139dfa1b3d433cc23b72f"; + vm.store(destTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000000000000000000001"; + vm.store(destTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000010000000000000001"; + vm.store(destTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00"; + value = hex"000000000000000000000000237a66474b7b934b22574359500212977b656d9f"; + vm.store(destTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb01"; + value = hex"5375706572636861696e4552433230000000000000000000000000000000001e"; + vm.store(destTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb02"; + value = hex"535550455200000000000000000000000000000000000000000000000000000a"; + vm.store(destTokenAddress, slot, value); + slot = hex"07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb03"; + value = hex"0000000000000000000000000000000000000000000000000000000000000012"; + vm.store(destTokenAddress, slot, value); + slot = hex"f0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00"; + value = hex"0000000000000000000000000000000000000000000000000000000000000001"; + vm.store(destTokenAddress, slot, value); + vm.etch(mockL2ToL2MessengerAddress, mockL2ToL2MessengerCode); + } + + function _notExternalAddress(address user) public pure { + vm.assume(user != FOUNDRY_TEST_ADDRESS); + vm.assume(user != VM_ADDRESS); + vm.assume(user != sourceTokenAddress); + vm.assume(user != superchainERC20ImplAddress); + vm.assume(user != mockL2ToL2MessengerAddress); + vm.assume(user != destTokenAddress); + } +} diff --git a/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol new file mode 100644 index 000000000000..e4c80facdabf --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/deployments/InitialStateCode.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: UNLICENSED +// This file was autogenerated by running `kontrol load-state`. Do not edit this file manually. + +pragma solidity ^0.8.13; + +contract InitialStateCode { + bytes internal constant superchainERC20ImplCode = + hex"608060405234801561000f575f80fd5b5060043610610163575f3560e01c806378a3727b116100c7578063d505accf1161007d578063d9f5004611610063578063d9f5004614610356578063dd62ed3e14610369578063f6d2ee8614610391575f80fd5b8063d505accf146102fc578063d6c0b2c41461030f575f80fd5b806395d89b41116100ad57806395d89b41146102ce5780639dc29fac146102d6578063a9059cbb146102e9575f80fd5b806378a3727b146102965780637ecebe00146102a9575f80fd5b8063313ce5671161011c57806340c10f191161010257806340c10f191461022057806354fd4d501461023557806370a0823114610271575f80fd5b8063313ce567146101e45780633644e51514610218575f80fd5b8063095ea7b31161014c578063095ea7b3146101a457806318160ddd146101b757806323b872dd146101d1575f80fd5b806301ffc9a71461016757806306fdde031461018f575b5f80fd5b61017a610175366004611201565b6103a4565b60405190151581526020015b60405180910390f35b61019761043c565b6040516101869190611293565b61017a6101b23660046112c9565b6104ee565b6805345cdf77eb68f44c545b604051908152602001610186565b61017a6101df3660046112f3565b61053d565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb035460405160ff9091168152602001610186565b6101c36105f7565b61023361022e3660046112c9565b610673565b005b6101976040518060400160405280600c81526020017f312e302e302d626574612e31000000000000000000000000000000000000000081525081565b6101c361027f366004611331565b6387a211a2600c9081525f91909152602090205490565b6102336102a436600461134c565b61076b565b6101c36102b7366004611331565b6338377508600c9081525f91909152602090205490565b610197610923565b6102336102e43660046112c9565b610954565b61017a6102f73660046112c9565b610a40565b61023361030a366004611393565b610ab7565b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb005460405173ffffffffffffffffffffffffffffffffffffffff9091168152602001610186565b6102336103643660046112f3565b610c4a565b6101c36103773660046113fc565b602052637f5e9f20600c9081525f91909152603490205490565b61023361039f366004611507565b610ebf565b5f7fffffffff0000000000000000000000000000000000000000000000000000000082167f0bc3227100000000000000000000000000000000000000000000000000000000148061043657507f01ffc9a7000000000000000000000000000000000000000000000000000000007fffffffff000000000000000000000000000000000000000000000000000000008316145b92915050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600101805461046d90611589565b80601f016020809104026020016040519081016040528092919081815260200182805461049990611589565b80156104e45780601f106104bb576101008083540402835291602001916104e4565b820191905f5260205f20905b8154815290600101906020018083116104c757829003601f168201915b5050505050905090565b5f82602052637f5e9f20600c52335f52816034600c2055815f52602c5160601c337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b92560205fa350600192915050565b5f8360601b33602052637f5e9f208117600c526034600c208054600181011561057b5780851115610575576313be252b5f526004601cfd5b84810382555b50506387a211a28117600c526020600c208054808511156105a35763f4d678b85f526004601cfd5b84810382555050835f526020600c208381540181555082602052600c5160601c8160601c7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a3505060019392505050565b5f8061060161043c565b8051906020012090506040517f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f81528160208201527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604082015246606082015230608082015260a081209250505090565b33734200000000000000000000000000000000000010146106c0576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff821661070d576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107178282611104565b8173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d41213968858260405161075f91815260200190565b60405180910390a25050565b73ffffffffffffffffffffffffffffffffffffffff83166107b8576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6107c23383611180565b6040805133602482015273ffffffffffffffffffffffffffffffffffffffff85166044820152606480820185905282518083039091018152608490910182526020810180517bffffffffffffffffffffffffffffffffffffffffffffffffffffffff167fd9f500460000000000000000000000000000000000000000000000000000000017905290517f7056f41f00000000000000000000000000000000000000000000000000000000815273420000000000000000000000000000000000002390637056f41f9061089c908590309086906004016115da565b5f604051808303815f87803b1580156108b3575f80fd5b505af11580156108c5573d5f803e3d5ffd5b5050604080518681526020810186905273ffffffffffffffffffffffffffffffffffffffff881693503392507ffcea3600a13c757f2758710b089cc9752781c35d2a9d6804370ed18cd82f0bb691015b60405180910390a350505050565b60607f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb00600201805461046d90611589565b33734200000000000000000000000000000000000010146109a1576040517f38da3b1500000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b73ffffffffffffffffffffffffffffffffffffffff82166109ee576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b6109f88282611180565b8173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca58260405161075f91815260200190565b5f6387a211a2600c52335f526020600c20805480841115610a685763f4d678b85f526004601cfd5b83810382555050825f526020600c208281540181555081602052600c5160601c337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a350600192915050565b5f610ac061043c565b80519060200120905084421115610ade57631a15a3cc5f526004601cfd5b6040518860601b60601c98508760601b60601c975065383775081901600e52885f526020600c2080547f8b73c3c69bb8fe3d512ecc4cf759cc79239f7b179b0ffacaa9a75d522b39400f83528360208401527fc89efdaa54c0f20c7adf612882df0950f5a951637e0307cdcb4c672f298b8bc6604084015246606084015230608084015260a08320602e527f6e71edae12b1b97f4d1f60370fef10105fa2faae0126114a169c64845d6126c983528a60208401528960408401528860608401528060808401528760a084015260c08320604e526042602c205f528660ff16602052856040528460605260208060805f60015afa8b3d5114610be65763ddafbaef5f526004601cfd5b019055777f5e9f20000000000000000000000000000000000000000088176040526034602c2087905587897f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925602060608501a360405250505f606052505050505050565b73ffffffffffffffffffffffffffffffffffffffff8216610c97576040517fd92e233d00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3373420000000000000000000000000000000000002314610ce4576040517f065d515000000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b3073ffffffffffffffffffffffffffffffffffffffff1673420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff166338ffde186040518163ffffffff1660e01b8152600401602060405180830381865afa158015610d58573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610d7c9190611617565b73ffffffffffffffffffffffffffffffffffffffff1614610dc9576040517fbc22e2aa00000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b5f73420000000000000000000000000000000000002373ffffffffffffffffffffffffffffffffffffffff1663247944626040518163ffffffff1660e01b8152600401602060405180830381865afa158015610e27573d5f803e3d5ffd5b505050506040513d601f19601f82011682018060405250810190610e4b9190611632565b9050610e578383611104565b8273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fc75e22a0b57fb7740dbfc0caa5c6b7a82a2139964e7f1b7be7ac4e8be0f719ba8484604051610915929190918252602082015260400190565b7ff0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00805468010000000000000000810460ff16159067ffffffffffffffff165f81158015610f095750825b90505f8267ffffffffffffffff166001148015610f255750303b155b905081158015610f33575080155b15610f6a576040517ff92ee8a900000000000000000000000000000000000000000000000000000000815260040160405180910390fd5b84547fffffffffffffffffffffffffffffffffffffffffffffffff00000000000000001660011785558315610fcb5784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff16680100000000000000001785555b7f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb0080547fffffffffffffffffffffffff00000000000000000000000000000000000000001673ffffffffffffffffffffffffffffffffffffffff8b161781557f07f04e84143df95a6373fcf376312ae41da81a193a3089073a54f47a74d8fb016110558a82611694565b50600281016110648982611694565b5060030180547fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff001660ff881617905583156110f45784547fffffffffffffffffffffffffffffffffffffffffffffff00ffffffffffffffff168555604051600181527fc7f505b2f371ae2175ee4913f4499e1f2633a7b5936321eed1cdaeb6115181d29060200160405180910390a15b505050505050505050565b505050565b6805345cdf77eb68f44c54818101818110156111275763e5cfe9575f526004601cfd5b806805345cdf77eb68f44c5550506387a211a2600c52815f526020600c208181540181555080602052600c5160601c5f7fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602080a35050565b6387a211a2600c52815f526020600c208054808311156111a75763f4d678b85f526004601cfd5b82900390556805345cdf77eb68f44c805482900390555f81815273ffffffffffffffffffffffffffffffffffffffff83167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602083a35050565b5f60208284031215611211575f80fd5b81357fffffffff0000000000000000000000000000000000000000000000000000000081168114611240575f80fd5b9392505050565b5f81518084528060208401602086015e5f6020828601015260207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011685010191505092915050565b602081525f6112406020830184611247565b73ffffffffffffffffffffffffffffffffffffffff811681146112c6575f80fd5b50565b5f80604083850312156112da575f80fd5b82356112e5816112a5565b946020939093013593505050565b5f805f60608486031215611305575f80fd5b8335611310816112a5565b92506020840135611320816112a5565b929592945050506040919091013590565b5f60208284031215611341575f80fd5b8135611240816112a5565b5f805f6060848603121561135e575f80fd5b8335611369816112a5565b95602085013595506040909401359392505050565b803560ff8116811461138e575f80fd5b919050565b5f805f805f805f60e0888a0312156113a9575f80fd5b87356113b4816112a5565b965060208801356113c4816112a5565b955060408801359450606088013593506113e06080890161137e565b925060a0880135915060c0880135905092959891949750929550565b5f806040838503121561140d575f80fd5b8235611418816112a5565b91506020830135611428816112a5565b809150509250929050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52604160045260245ffd5b5f82601f83011261146f575f80fd5b813567ffffffffffffffff8082111561148a5761148a611433565b604051601f83017fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0908116603f011681019082821181831017156114d0576114d0611433565b816040528381528660208588010111156114e8575f80fd5b836020870160208301375f602085830101528094505050505092915050565b5f805f806080858703121561151a575f80fd5b8435611525816112a5565b9350602085013567ffffffffffffffff80821115611541575f80fd5b61154d88838901611460565b94506040870135915080821115611562575f80fd5b5061156f87828801611460565b92505061157e6060860161137e565b905092959194509250565b600181811c9082168061159d57607f821691505b6020821081036115d4577f4e487b71000000000000000000000000000000000000000000000000000000005f52602260045260245ffd5b50919050565b83815273ffffffffffffffffffffffffffffffffffffffff83166020820152606060408201525f61160e6060830184611247565b95945050505050565b5f60208284031215611627575f80fd5b8151611240816112a5565b5f60208284031215611642575f80fd5b5051919050565b601f8211156110ff57805f5260205f20601f840160051c8101602085101561166e5750805b601f840160051c820191505b8181101561168d575f815560010161167a565b5050505050565b815167ffffffffffffffff8111156116ae576116ae611433565b6116c2816116bc8454611589565b84611649565b602080601f831160018114611714575f84156116de5750858301515b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600386901b1c1916600185901b1785556117a8565b5f858152602081207fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe08616915b8281101561176057888601518255948401946001909101908401611741565b508582101561179c57878501517fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600388901b60f8161c191681555b505060018460011b0185555b50505050505056fea164736f6c6343000819000a"; + bytes internal constant sourceTokenCode = + hex"6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a"; + bytes internal constant destTokenCode = + hex"6080604052600a600c565b005b60186014601a565b605d565b565b5f60587f360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc5473ffffffffffffffffffffffffffffffffffffffff1690565b905090565b365f80375f80365f845af43d5f803e8080156076573d5ff35b3d5ffdfea164736f6c6343000819000a"; + bytes internal constant mockL2ToL2MessengerCode = + hex"608060405260043610610058575f3560e01c80632ea02369116100415780632ea023691461009857806338ffde18146100cb5780637056f41f14610104575f80fd5b80631ecd26f21461005c5780632479446214610071575b5f80fd5b61006f61006a366004610484565b610117565b005b34801561007c575f80fd5b506100856101d2565b6040519081526020015b60405180910390f35b3480156100a3575f80fd5b506100857f000000000000000000000000000000000000000000000000000000000000000281565b3480156100d6575f80fd5b506100df6101e3565b60405173ffffffffffffffffffffffffffffffffffffffff909116815260200161008f565b61006f610112366004610500565b6102cd565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610141929190610556565b5f6040518083038185875af1925050503d805f811461017b576040519150601f19603f3d011682016040523d82523d5f602084013e610180565b606091505b5091509150816101c757806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016101be9190610565565b60405180910390fd5b505050505050505050565b5f6101de4660016105b8565b905090565b5f73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361024657507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036102a857507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a90565b507f000000000000000000000000000000000000000000000000000000000000000090565b7f000000000000000000000000000000000000000000000000000000000000000284036103e6575f6103557f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f920191909152506103ec92505050565b9050806103e4576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016101be565b505b50505050565b5f6103f9845a8585610401565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff8116811461043a575f80fd5b919050565b5f8083601f84011261044f575f80fd5b50813567ffffffffffffffff811115610466575f80fd5b60208301915083602082850101111561047d575f80fd5b9250929050565b5f805f805f805f60c0888a03121561049a575f80fd5b8735965060208801359550604088013594506104b860608901610417565b93506104c660808901610417565b925060a088013567ffffffffffffffff8111156104e1575f80fd5b6104ed8a828b0161043f565b989b979a50959850939692959293505050565b5f805f8060608587031215610513575f80fd5b8435935061052360208601610417565b9250604085013567ffffffffffffffff81111561053e575f80fd5b61054a8782880161043f565b95989497509550505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f83011684010191505092915050565b808201808211156105f0577f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b9291505056fea164736f6c6343000819000a"; +} diff --git a/packages/contracts-bedrock/test/properties/kontrol/helpers/LibStateDiff.sol b/packages/contracts-bedrock/test/properties/kontrol/helpers/LibStateDiff.sol new file mode 100644 index 000000000000..d5269b082604 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/helpers/LibStateDiff.sol @@ -0,0 +1,136 @@ +// SPDX-License-Identifier: MIT +// (The MIT License) + +// Copyright 2020-2024 Optimism + +// Permission is hereby granted, free of charge, to any person obtaining +// a copy of this software and associated documentation files (the +// "Software"), to deal in the Software without restriction, including +// without limitation the rights to use, copy, modify, merge, publish, +// distribute, sublicense, and/or sell copies of the Software, and to +// permit persons to whom the Software is furnished to do so, subject to +// the following conditions: + +// The above copyright notice and this permission notice shall be +// included in all copies or substantial portions of the Software. + +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +// IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +// CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +// TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +// SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +pragma solidity 0.8.25; + +import { stdJson } from "forge-std/StdJson.sol"; +import { VmSafe } from "forge-std/Vm.sol"; + +/// @title LibStateDiff +/// @author refcell +/// @notice Library to write StateDiff output to json. +library LibStateDiff { + /// @notice Accepts an array of AccountAccess structs from the Vm and encodes them as a json string. + /// @param _accountAccesses Array of AccountAccess structs. + /// @return serialized_ string + function encodeAccountAccesses(VmSafe.AccountAccess[] memory _accountAccesses) + internal + returns (string memory serialized_) + { + string[] memory accountAccesses = new string[](_accountAccesses.length); + for (uint256 i = 0; i < _accountAccesses.length; i++) { + accountAccesses[i] = serializeAccountAccess(_accountAccesses[i]); + } + serialized_ = stdJson.serialize("accountAccessElem", "accountAccesses", accountAccesses); + } + + /// @notice Turns an AccountAccess into a json serialized string + /// @param _accountAccess The AccountAccess to serialize + /// @return serialized_ The json serialized string + function serializeAccountAccess(VmSafe.AccountAccess memory _accountAccess) + internal + returns (string memory serialized_) + { + string memory json = "foo"; + json = stdJson.serialize("accountAccess", "chainInfo", serializeChainInfo(_accountAccess.chainInfo)); + json = stdJson.serialize("accountAccess", "kind", serializeAccountAccessKind(_accountAccess.kind)); + json = stdJson.serialize("accountAccess", "account", _accountAccess.account); + json = stdJson.serialize("accountAccess", "accessor", _accountAccess.accessor); + json = stdJson.serialize("accountAccess", "initialized", _accountAccess.initialized); + json = stdJson.serialize("accountAccess", "oldBalance", _accountAccess.oldBalance); + json = stdJson.serialize("accountAccess", "newBalance", _accountAccess.newBalance); + json = stdJson.serialize("accountAccess", "deployedCode", _accountAccess.deployedCode); + json = stdJson.serialize("accountAccess", "value", _accountAccess.value); + json = stdJson.serialize("accountAccess", "data", _accountAccess.data); + json = stdJson.serialize("accountAccess", "reverted", _accountAccess.reverted); + json = stdJson.serialize( + "accountAccess", "storageAccesses", serializeStorageAccesses(_accountAccess.storageAccesses) + ); + serialized_ = json; + } + + /// @notice Accepts a VmSafe.ChainInfo struct and encodes it as a json string. + /// @param _chainInfo The ChainInfo struct to serialize + /// @return serialized_ string + function serializeChainInfo(VmSafe.ChainInfo memory _chainInfo) internal returns (string memory serialized_) { + string memory json = ""; + json = stdJson.serialize("chainInfo", "forkId", _chainInfo.forkId); + json = stdJson.serialize("chainInfo", "chainId", _chainInfo.chainId); + serialized_ = json; + } + + /// @notice Turns an AccountAccessKind into a string. + /// @param _kind The AccountAccessKind to serialize + /// @return serialized_ The string representation of the AccountAccessKind + function serializeAccountAccessKind(VmSafe.AccountAccessKind _kind) + internal + pure + returns (string memory serialized_) + { + if (_kind == VmSafe.AccountAccessKind.Call) { + serialized_ = "Call"; + } else if (_kind == VmSafe.AccountAccessKind.DelegateCall) { + serialized_ = "DelegateCall"; + } else if (_kind == VmSafe.AccountAccessKind.CallCode) { + serialized_ = "CallCode"; + } else if (_kind == VmSafe.AccountAccessKind.StaticCall) { + serialized_ = "StaticCall"; + } else if (_kind == VmSafe.AccountAccessKind.Create) { + serialized_ = "Create"; + } else if (_kind == VmSafe.AccountAccessKind.SelfDestruct) { + serialized_ = "SelfDestruct"; + } else { + serialized_ = "Resume"; + } + } + + /// @notice Accepts an array of StorageAccess structs from the Vm and encodes each as a json string. + /// @param _storageAccesses Array of StorageAccess structs. + /// @return serialized_ The list of json serialized StorageAccess structs. + function serializeStorageAccesses(VmSafe.StorageAccess[] memory _storageAccesses) + internal + returns (string[] memory serialized_) + { + serialized_ = new string[](_storageAccesses.length); + for (uint256 i = 0; i < _storageAccesses.length; i++) { + serialized_[i] = serializeStorageAccess(_storageAccesses[i]); + } + } + + /// @notice Turns a StorageAccess into a json serialized string + /// @param _storageAccess The StorageAccess to serialize + /// @return serialized_ The json serialized string + function serializeStorageAccess(VmSafe.StorageAccess memory _storageAccess) + internal + returns (string memory serialized_) + { + string memory json = ""; + json = stdJson.serialize("storageAccess", "account", _storageAccess.account); + json = stdJson.serialize("storageAccess", "slot", _storageAccess.slot); + json = stdJson.serialize("storageAccess", "isWrite", _storageAccess.isWrite); + json = stdJson.serialize("storageAccess", "previousValue", _storageAccess.previousValue); + json = stdJson.serialize("storageAccess", "newValue", _storageAccess.newValue); + json = stdJson.serialize("storageAccess", "reverted", _storageAccess.reverted); + serialized_ = json; + } +} diff --git a/packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol b/packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol new file mode 100644 index 000000000000..a49cb41b6545 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol @@ -0,0 +1,74 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import { console2 as console } from "forge-std/console2.sol"; +import { stdJson } from "forge-std/StdJson.sol"; +import { Vm } from "forge-std/Vm.sol"; +import { VmSafe } from "forge-std/Vm.sol"; +import { LibStateDiff } from "./LibStateDiff.sol"; + +struct Contract { + string contractName; + address contractAddress; +} + +abstract contract RecordStateDiff { + Vm private constant vm = Vm(address(uint160(uint256(keccak256("hevm cheat code"))))); + + /// @notice Executes a function recording its state updates and saves it to the + /// the file $STATE_DIFF_DIR/$STATE_DIFF_FILE + /// @dev STATE_DIFF_DIR env var with file folder relative to the foundry root dir + /// @dev STATE_DIFF_NAME env var with state diff file name + modifier recordStateDiff() { + // Check if the specified JSON file exists and create it if not + string memory statediffFile = check_file(vm.envString("STATE_DIFF_DIR"), vm.envString("STATE_DIFF_NAME")); + vm.startStateDiffRecording(); + _; + VmSafe.AccountAccess[] memory accesses = vm.stopAndReturnStateDiff(); + string memory json = LibStateDiff.encodeAccountAccesses(accesses); + vm.writeJson({ json: json, path: statediffFile }); + } + + /// @notice Saves a an address with a name to $STATE_DIFF_DIR/$STATE_DIFF_NAMES + /// @dev STATE_DIFF_DIR env var with file folder relative to the foundry root dir + /// @dev ADDR_NAMES env var with named addresses file name + /// TODO: Investigate/fix why the resulting order of the strings in the json seems to not preseve the order + /// in which `save_address` is called when saving multiple addresses + function save_address(address addr, string memory name) public { + string memory address_names_file = check_file(vm.envString("STATE_DIFF_DIR"), vm.envString("ADDR_NAMES")); + vm.writeJson({ json: vm.serializeString("", vm.toString(addr), name), path: address_names_file }); + } + + /// @notice Checks if dir_name/file_name exists and creates it if not + function check_file(string memory dir_name, string memory file_name) public returns (string memory) { + string memory dirname = string.concat(vm.projectRoot(), "/", dir_name); + string memory filename = string.concat(vm.projectRoot(), "/", dir_name, "/", file_name); + if (vm.exists(filename)) return filename; + if (!vm.isDir(dirname)) ffi_two_arg("mkdir", "-p", dirname); // Create directory if doesn't exist + ffi_one_arg("touch", filename); // Create file. Might be redundant, but better make sure + return filename; + } + + /// @notice Execute one bash command with one argument + /// @dev Will revert if the command returns any output + /// TODO: abstract number of arguments per function + function ffi_one_arg(string memory command, string memory arg) public { + string[] memory inputs = new string[](2); + inputs[0] = command; + inputs[1] = arg; + bytes memory res = vm.ffi(inputs); + require(res.length == 0, "RecordStateDiff: Command execution failed"); + } + + /// @notice Execute one bash command with one argument + /// @dev Will revert if the command returns any output + /// TODO: abstract number of arguments per function + function ffi_two_arg(string memory command, string memory arg1, string memory arg2) public { + string[] memory inputs = new string[](3); + inputs[0] = command; + inputs[1] = arg1; + inputs[2] = arg2; + bytes memory res = vm.ffi(inputs); + require(res.length == 0, "RecordStateDiff: Command execution failed"); + } +} diff --git a/packages/contracts-bedrock/test/properties/kontrol/optimism-superchain-lemmas.md b/packages/contracts-bedrock/test/properties/kontrol/optimism-superchain-lemmas.md new file mode 100644 index 000000000000..6cb29280402f --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/optimism-superchain-lemmas.md @@ -0,0 +1,33 @@ +```k +requires "foundry.md" + +module OPTIMISM-SUPERCHAIN-LEMMAS + imports BOOL + imports FOUNDRY + imports INT-SYMBOLIC + + // Convert booleans to their word equivalents + rule bool2Word(true) => 1 + rule bool2Word(false) => 0 + + // Associativity and Commutativity Rules: + rule A +Int (B +Int C) => (A +Int B) +Int C + rule A *Int B => B *Int A + + // Comparison Normalization: + rule A +Int B A A false requires 0 <=Int B + rule A false requires 0 <=Int B + + rule A -Int A => 0 + rule 0 +Int A => A + rule A +Int 0 => A + rule A -Int 0 => A + + rule chop(I) => I requires #rangeUInt(256, I) + rule chop (chop (X:Int) +Int Y:Int) => chop (X +Int Y) + rule chop (X:Int +Int chop (Y:Int)) => chop (X +Int Y) +endmodule +``` diff --git a/packages/contracts-bedrock/test/properties/kontrol/utils/record-state-diff.sh b/packages/contracts-bedrock/test/properties/kontrol/utils/record-state-diff.sh new file mode 100644 index 000000000000..f2e242e913ea --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/utils/record-state-diff.sh @@ -0,0 +1,55 @@ +#!/bin/bash +set -euo pipefail + +################################################################################ +# WARNING: This script is meant to be run from the foundry root directory # +# bash ./test/properties/kontrol/utils/record-state-diff.sh to run it # +################################################################################ + +########################## +# ENVIRNONMENT VARIABLES # +########################## + +# JSON-related variables +export STATE_DIFF_DIR=supererc20-state-diff # Relative to the Foundry root directory +export STATE_DIFF_NAME=StateDiff.json +export ADDR_NAMES=AddressNames.json +CLEAN_JSON_PATH=test/kontrol/scripts/json/clean_json.py + +# Where the contract and function that produces the jsons live +RECORDING_CONTRACT_DIR=test/properties/kontrol # Relative to the Foundry root directory +RECORDING_CONTRACT_FILE=KontrolBase.sol # Name of the Solidity file +RECORDING_CONTRACT_NAME=KontrolBase # Name of the actual contract +RECORDING_CONTRACT_FUNCTION=setUpNamed # Name of the function with the recordStateDiff modifier + +RECORDING_CONTRACT_PATH="$RECORDING_CONTRACT_DIR/$RECORDING_CONTRACT_FILE:$RECORDING_CONTRACT_NAME" + +# Kontrol-related variables +GENERATED_CONTRACT_NAME=InitialState +GENERATED_CONTRACT_DIR=test/properties/kontrol/deployments # Relative to the Foundry root directory +GENERATED_CONTRACT_LICENSE=UNLICENSED + +#################### +# RECORD EXECUTION # +#################### + +# Run the function with the recordStateDiff modifier +forge script $RECORDING_CONTRACT_PATH --sig "$RECORDING_CONTRACT_FUNCTION" --ffi -vv +# state diff JSON comes out scaped from the last command +# We execute this script to unscape it so that it can be fed to Kontrol +python3 "$CLEAN_JSON_PATH" "$STATE_DIFF_DIR/$STATE_DIFF_NAME" + +############################### +# GENERATE SOLIDITY CONTRACTS # +############################### + +# Give the appropriate files to Kontrol to create the contracts +kontrol load-state "$GENERATED_CONTRACT_NAME" "$STATE_DIFF_DIR/$STATE_DIFF_NAME" \ + --contract-names "$STATE_DIFF_DIR/$ADDR_NAMES" \ + --output-dir "$GENERATED_CONTRACT_DIR" \ + --license "$GENERATED_CONTRACT_LICENSE" \ + --from-state-diff + +# Format the code to ensure compatibility with any CI checks +forge fmt "$GENERATED_CONTRACT_DIR/$GENERATED_CONTRACT_NAME.sol" +forge fmt "$GENERATED_CONTRACT_DIR/${GENERATED_CONTRACT_NAME}Code.sol" \ No newline at end of file